blob: 933b3bbd2b8677cd230f5fbb2cf288978a2bd4e3 (
plain)
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
|
{-# OPTIONS --without-K --safe #-}
open import Relation.Binary using (REL; Setoid)
module Cfe.Expression.Base
{c ℓ} (over : Setoid c ℓ)
where
open Setoid over using () renaming (Carrier to C)
open import Cfe.Language over renaming (_∙_ to _∙ˡ_; _≈_ to _≈ˡ_)
open import Data.Fin hiding (_+_; _<_)
open import Data.Nat hiding (_≟_; _⊔_)
open import Data.Vec
open import Function using (_on_)
open import Relation.Nullary using (yes; no)
private
variable
m n : ℕ
------------------------------------------------------------------------
-- Definition
infix 8 μ_
infix 7 _∙_
infix 6 _∨_
data Expression : ℕ → Set c where
⊥ : Expression n
ε : Expression n
Char : (c : C) → Expression n
_∨_ : Expression n → Expression n → Expression n
_∙_ : Expression n → Expression n → Expression n
Var : (j : Fin n) → Expression n
μ_ : Expression (suc n) → Expression n
------------------------------------------------------------------------
-- Semantics
infix 4 _≈_
⟦_⟧ : Expression n → Vec (Language _) n → Language _
⟦ ⊥ ⟧ _ = ∅
⟦ ε ⟧ _ = ｛ε｝ {ℓ}
⟦ Char x ⟧ _ = ｛ x ｝
⟦ e₁ ∨ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∪ ⟦ e₂ ⟧ γ
⟦ e₁ ∙ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∙ˡ ⟦ e₂ ⟧ γ
⟦ Var j ⟧ γ = lookup γ j
⟦ μ e ⟧ γ = ⋃ (λ X → ⟦ e ⟧ (X ∷ γ))
_≈_ : {n : ℕ} → Expression n → Expression n → Set _
e₁ ≈ e₂ = ∀ γ → ⟦ e₁ ⟧ γ ≈ˡ ⟦ e₂ ⟧ γ
------------------------------------------------------------------------
-- Syntax manipulation
infix 10 _[_/_]
wkn : Expression n → Fin (suc n) → Expression (suc n)
wkn ⊥ i = ⊥
wkn ε i = ε
wkn (Char c) i = Char c
wkn (e₁ ∨ e₂) i = wkn e₁ i ∨ wkn e₂ i
wkn (e₁ ∙ e₂) i = wkn e₁ i ∙ wkn e₂ i
wkn (Var j) i = Var (punchIn i j)
wkn (μ e) i = μ wkn e (suc i)
_[_/_] : Expression (suc n) → Expression n → Fin (suc n) → Expression n
⊥ [ e′ / i ] = ⊥
ε [ e′ / i ] = ε
Char x [ e′ / i ] = Char x
(e₁ ∨ e₂) [ e′ / i ] = e₁ [ e′ / i ] ∨ e₂ [ e′ / i ]
(e₁ ∙ e₂) [ e′ / i ] = e₁ [ e′ / i ] ∙ e₂ [ e′ / i ]
Var j [ e′ / i ] with i ≟ j
... | yes i≡j = e′
... | no i≢j = Var (punchOut i≢j)
(μ e) [ e′ / i ] = μ e [ wkn e′ zero / suc i ]
------------------------------------------------------------------------
-- Syntax properties
infix 4 _<ᵣₐₙₖ_
rank : Expression n → ℕ
rank ⊥ = 0
rank ε = 0
rank (Char _) = 0
rank (e₁ ∨ e₂) = suc (rank e₁ + rank e₂)
rank (e₁ ∙ _) = suc (rank e₁)
rank (Var _) = 0
rank (μ e) = suc (rank e)
_<ᵣₐₙₖ_ : REL (Expression m) (Expression n) _
e <ᵣₐₙₖ e′ = rank e < rank e′
|
