paper-2021-language-derivatives/Symbolic.lagda at main · conal/paper-2021-language-derivatives · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
\begin{code}[hide]

open import Relation.Binary.PropositionalEquality using (_≡_) ; open _≡_
open import Decidability hiding (_◂_)

module Symbolic {ℓ} {A : Set ℓ} (_≟_ : Decidable₂ {A = A} _≡_) where

open import Level
open import Data.List using ([]; _∷_)

open import Misc {ℓ}
open import Inverses {ℓ}

module ◇ where
  -- open import Language A public
  open import Predicate public ; open ListOps A public
  open import Calculus A public

open ◇ using (ν⋆; δ⋆; ν☆; δ☆; ν𝟏; δ𝟏; ν`; δ`)

private
  variable
    P Q : ◇.Lang
    s : Set ℓ
\end{code}

%<*api>
{\mathindent0ex
\begin{center}
\begin{code}[hide]
infixr  6 _∪_
infixr  7 _∩_
infixl  7 _⋆_
infixr  7 _·_
infix   9 _◂_
infixl 10 _☆
\end{code}
\begin{code}
data Lang : ◇.Lang → Set (suc ℓ) where
  ∅    : Lang  ◇.∅
  𝒰    : Lang  ◇.𝒰
  _∪_  : Lang  P  → Lang Q  → Lang (P  ◇.∪  Q)
  _∩_  : Lang  P  → Lang Q  → Lang (P  ◇.∩  Q)
  _·_  : Dec   s  → Lang P  → Lang (s  ◇.·  P)
  𝟏    : Lang ◇.𝟏
  _⋆_  : Lang  P  → Lang Q  → Lang (P  ◇.⋆  Q)
  _☆   : Lang  P  → Lang (P ◇.☆)
  `    : (a : A) → Lang (◇.` a)
  _◂_  : (Q ⟷ P) → Lang P → Lang Q
\end{code}
\end{center}
\iftalk
\vspace{-3.5ex}
\fi
\hfill
\begin{minipage}[c]{33ex}
\begin{code}
ν  : Lang P → Dec (◇.ν P)
δ  : Lang P → (a : A) → Lang (◇.δ P a)
\end{code}
\end{minipage}
\hfill
\begin{minipage}[c]{25ex}
\begin{code}
⟦_⟧‽ : Lang P → Decidable P
⟦ p ⟧‽     []    = ν p
⟦ p ⟧‽ (a  ∷ w)  = ⟦ δ p a ⟧‽ w
\end{code}
\end{minipage}
\hfill\;
}
%</api>

%<*semantics>
\begin{code}
⟦_⟧ : Lang P → ◇.Lang
⟦_⟧ {P} r = P
\end{code}
%</semantics>

%<*defs>
{\mathindent0ex
\begin{code}[hide]
private
  variable
    p : Lang P
    q : Lang Q

\end{code}
\setstretch{1.6}
\hfill
%\hspace{-1.2ex}%% To align with Automatic. Why different?
\begin{minipage}{30ex}
\begin{code}
ν ∅ = ⊥‽
ν 𝒰 = ⊤‽
ν (p ∪ q) = ν p ⊎‽ ν q
ν (p ∩ q) = ν p ×‽ ν q
ν (s · p) = s ×‽ ν p
ν 𝟏 = ν𝟏 ◃ ⊤‽
ν (p ⋆ q) = ν⋆ ◃ (ν p ×‽ ν q)
ν (p ☆) = ν☆ ◃ (ν p ✶‽)
ν (` a) = ν` ◃ ⊥‽
ν (f ◂ p) = f ◃ ν p
\end{code}
\end{minipage}
\hfill
\begin{minipage}{38ex}
\begin{code}
δ ∅ a = ∅
δ 𝒰 a = 𝒰
δ (p ∪ q) a = δ p a ∪ δ q a
δ (p ∩ q) a = δ p a ∩ δ q a
δ (s · p) a = s · δ p a
δ 𝟏 a = δ𝟏 ◂ ∅
δ (p ⋆ q) a = δ⋆ ◂ (ν p · δ q a ∪ δ p a ⋆ q)
δ (p ☆) a = δ☆ ◂ (ν p ✶‽ · (δ p a ⋆ p ☆))
δ (` c) a = δ` ◂ ((a ≟ c) · 𝟏)
δ (f ◂ p) a = f ◂ δ p a
\end{code}
\end{minipage}
\hfill\;
}
%</defs>