-
Notifications
You must be signed in to change notification settings - Fork 0
/
enclib.agda
146 lines (113 loc) · 5.69 KB
/
enclib.agda
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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
open import core public
size : Ty → ℕ
toBool : Ty → List Ty
decode : (τ : Ty) → Vals (toBool τ) → Ty⟦ τ ⟧
------------------------
toBools : List Ty → List Ty
toBools-∷ : (σ : Ty) (σs : List Ty) (pf : Ω ≡ σ ∷ σs)
→ toBools Ω ≡ toBool σ ++ toBools σs
toBools-++ : (Γ Γ′ : List Ty) (pf : Ω ≡ Γ ++ Γ′)
→ toBools Ω ≡ toBools Γ ++ toBools Γ′
splitVals : (valστ : Vals Ω) (pf : Ω ≡ σs ++ τs)
→ Σ[ valσ ∈ Vals σs ] Σ[ valτ ∈ Vals τs ] (valστ ≡ ++Vlp valσ valτ pf)
------------------------
decodes : (τs : List Ty) → Vals (toBools τs) → Vals τs
encodeVar : σ ∈ Γ → Vars (toBools Γ) (toBool σ)
encodeVars : Vars Γ Δ → Vars (toBools Γ) (toBools Δ)
------------------------
preCirc′ : (Γ′ : List Ty) → Circ Γ Δ → Circ (Γ′ ++ Γ) (Γ′ ++ Δ)
_++Cr_ : Circ Γ Δ → Circ Γ Δ′ → Circ Γ (Δ ++ Δ′)
data Lit Γ : Set
data Cls Γ : Set
data Cnf Γ : Set
litCirc : Lit Γ → Circ (toBools Γ) [ bool ]
clsCirc : Cls Γ → Circ (toBools Γ) [ bool ]
cnfCirc : Cnf Γ → Circ (toBools Γ) [ bool ]
encodeOp : Op Γ τ → Circ (toBools Γ) (toBools [ τ ])
------------------------------------------------
size bool = 1
size tri = 2
toBool τ = replicate (size τ) bool
decode bool [ b ] = b
decode tri [ false , true ] = true
decode tri [ false , false ] = false
decode tri [ true , _ ] = dc
------------------------
toBools = concatMap toBool
toBools-∷ σ σs refl = refl
toBools-++ [] Γ′ refl = refl
toBools-++ (σ ∷ σs) Γ′ refl =
begin
toBools (σ ∷ σs ++ Γ′)
≡⟨⟩
toBool σ ++ toBools (σs ++ Γ′)
≡⟨ cong (toBool σ ++_) (toBools-++ σs Γ′ refl) ⟩
toBool σ ++ (toBools σs ++ toBools Γ′)
≡⟨ sym (++-assoc (toBool σ) (toBools σs) (toBools Γ′)) ⟩
(toBool σ ++ toBools σs) ++ toBools Γ′
≡⟨⟩
toBools (σ ∷ σs) ++ toBools Γ′
∎
splitVals {σs = []} valτ refl = ⟨ _ , ⟨ valτ , refl ⟩ ⟩
splitVals {σs = σ ∷ σs} (val ∷ vals) refl with splitVals {σs = σs} vals refl
... | ⟨ val″ , ⟨ valτ , pf″ ⟩ ⟩ = ⟨ val ∷ val″ , ⟨ valτ , cong (val ∷_) pf″ ⟩ ⟩
------------------------
decodes [] [] = []
decodes (τ ∷ τs) bvals with splitVals {σs = toBool τ} {τs = toBools τs} bvals (toBools-∷ τ τs refl)
decodes (τ ∷ τs) .(++Vlp bvalτ bvalτs (toBools-∷ τ τs refl)) | ⟨ bvalτ , ⟨ bvalτs , refl ⟩ ⟩ = decode τ bvalτ ∷ decodes τs bvalτs
encodeVar {σ} {σ ∷ σs} here = sufVars (toBools σs) (iniVars (toBool σ))
encodeVar {σ} {x ∷ σs} (there l) = preVars (toBool x) (encodeVar {σ} {σs} l)
encodeVars [] = []
encodeVars (vr ∷ vars) = encodeVar vr ++Vr encodeVars vars
------------------------
preCirc′ {Γ} {Δ} Γ′ circ = comp pick₁ circ refl (ret pick₂)
where pick₁ = preVars Γ′ (iniVars Γ)
pick₂₁ = preVars Δ (sufVars Γ (iniVars Γ′))
pick₂₂ = sufVars (Γ′ ++ Γ) (iniVars Δ)
pick₂ = pick₂₁ ++Vr pick₂₂
_++Cr_ {Γ} {Δ} {Δ′} c₁ c₂ = comp (iniVars Γ) c₁ refl (preCirc′ Δ c₂)
data Lit Γ where
pos : bool ∈ toBools Γ → Lit Γ
neg : bool ∈ toBools Γ → Lit Γ
data Cls Γ where
triv : Lit Γ → Cls Γ
disj : Lit Γ → Cls Γ → Cls Γ
data Cnf Γ where
triv : Cls Γ → Cnf Γ
conj : Cls Γ → Cnf Γ → Cnf Γ
litCirc (pos i) = ret [ i ]
litCirc {Γ} (neg i) = comp [ i ] (oper notB) refl (ret pick)
where pick = sufVars (toBools Γ) (iniVars [ bool ])
clsCirc (triv l) = litCirc l
clsCirc {Γ} (disj l c) = comp pick₁ (litCirc l ++Cr clsCirc c) refl (comp pick₂ (oper orB) refl (ret pick₃))
where pick₁ = iniVars (toBools Γ)
pick₂ = sufVars (toBools Γ) (iniVars [ bool , bool ])
pick₃ = sufVars (bool ∷ bool ∷ toBools Γ) (iniVars [ bool ])
cnfCirc (triv c) = clsCirc c
cnfCirc {Γ} (conj c n) = comp pick₁ (clsCirc c ++Cr cnfCirc n) refl (comp pick₂ (oper andB) refl (ret pick₃))
where pick₁ = iniVars (toBools Γ)
pick₂ = sufVars (toBools Γ) (iniVars [ bool , bool ])
pick₃ = sufVars (bool ∷ bool ∷ toBools Γ) (iniVars [ bool ])
------------------------
pattern α = here
pattern a = there here
pattern β = there (there here)
pattern b = there (there (there here))
encodeOp andT = cnfCirc {[ tri , tri ]} γn ++Cr cnfCirc {[ tri , tri ]} cn
where γn = conj (disj (pos α) (triv (pos β)))
(conj (disj (pos α) (triv (pos a)))
(triv (disj (pos β) (triv (pos b)))))
cn = conj (triv (pos a))
(triv (triv (pos b)))
encodeOp orT = cnfCirc {[ tri , tri ]} γn ++Cr cnfCirc {[ tri , tri ]} cn
where γn = conj (disj (pos α) (triv (pos β)))
(conj (disj (pos α) (triv (neg a)))
(triv (disj (pos β) (triv (neg b)))))
cn = triv (disj (pos a) (triv (pos b)))
encodeOp ≡C = cnfCirc {[ tri , tri ]} cn
where cn = conj (disj (pos α) (triv (neg β)))
(conj (disj (pos α) (disj (pos a) (triv (neg b))))
(triv (disj (pos α) (disj (neg a) (triv (pos b))))))
encodeOp andB = oper andB
encodeOp orB = oper orB
encodeOp notB = oper notB