-
Notifications
You must be signed in to change notification settings - Fork 0
/
Grow.agda
153 lines (142 loc) · 8.64 KB
/
Grow.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
147
148
149
150
151
152
153
{-
This module defines a compiler from NCC to NCC where the number N of alternatives per
choice grows. The compiler duplicates the last alternative in each choice to grow the vector
of alternatives to match a desired larger size.
-}
module Vatras.Translation.Lang.NCC.Grow where
open import Data.Empty using (⊥-elim)
import Vatras.Data.EqIndexedSet as IndexedSet
open import Data.Fin as Fin using (Fin; zero; suc)
import Data.Fin.Properties as Fin
open import Data.List as List using (List; []; _∷_)
import Data.List.Properties as List
open import Data.Nat using (ℕ; zero; suc; _<_; s≤s; z≤n; _+_; _∸_)
open import Data.Nat.Properties as ℕ using (≤-refl; ≤-reflexive; ≤-trans; <-trans)
open import Data.Product using (_×_; _,_)
open import Data.Vec as Vec using (Vec; []; _∷_)
import Data.Vec.Properties as Vec
open import Vatras.Framework.Compiler using (LanguageCompiler; _⊕_)
open import Vatras.Framework.Definitions using (𝔸; 𝔽)
open import Vatras.Framework.Relation.Function using (from; to)
open import Vatras.Framework.Variants as V using (Rose)
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≢_; refl; _≗_)
open import Relation.Nullary.Decidable using (yes; no)
open import Size using (Size; ∞)
import Vatras.Util.AuxProofs as ℕ
open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs)
import Vatras.Util.Vec as Vec
open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎)
open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym)
open import Vatras.Lang.All
open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩)
-- Increasing the arity is straightforward. We have to duplicate one element (we choose the last one to be consistent with the saturation semantic of `CCC`, see `find-or-last`) until the arity difference is zero.
-- For symmetry, this module provides a translation from the 2-ary `NCC`, because, for simplicity of the proof, ShrinkTo2 translates to the 2-ary `NCC`.
-- However, the proof of the generalizaton is almost identical so we prove the generalization directly and then specialize the proof.
grow : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
→ (n m : ℕ≥ 2)
→ n ℕ≥.≤ m
→ NCC n D i A
→ NCC m D i A
grow n m n≤m (a -< cs >-) = a -< List.map (grow n m n≤m) cs >-
grow (sucs n) m n≤m (d ⟨ cs ⟩) = d ⟨ Vec.saturate n≤m (Vec.map (grow (sucs n) m n≤m) cs) ⟩
conf : ∀ {D : 𝔽}
→ (n m : ℕ≥ 2)
→ n ℕ≥.≤ m
→ NCC.Configuration n D
→ NCC.Configuration m D
conf (sucs n) (sucs m) n≤m config d = Fin.inject≤ (config d) n≤m
fnoc : ∀ {D : 𝔽}
→ (n m : ℕ≥ 2)
→ n ℕ≥.≤ m
→ NCC.Configuration m D
→ NCC.Configuration n D
fnoc (sucs n) (sucs m) n≤m config d = ℕ≥.cappedFin (Fin.toℕ (config d))
preserves-⊆ : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
→ (n m : ℕ≥ 2)
→ (n≤m : n ℕ≥.≤ m)
→ (expr : NCC n D i A)
→ NCC.⟦ grow n m n≤m expr ⟧ ⊆[ fnoc n m n≤m ] NCC.⟦ expr ⟧
preserves-⊆ n m n≤m (a -< cs >-) config =
NCC.⟦ grow n m n≤m (a -< cs >-) ⟧ config
≡⟨⟩
NCC.⟦ a -< List.map (grow n m n≤m) cs >- ⟧ config
≡⟨⟩
a V.-< List.map (λ e → NCC.⟦ e ⟧ config) (List.map (grow n m n≤m) cs) >-
≡⟨ Eq.cong₂ V._-<_>- Eq.refl (List.map-∘ cs) ⟨
a V.-< List.map (λ e → NCC.⟦ grow n m n≤m e ⟧ config) cs >-
≡⟨ Eq.cong₂ V._-<_>- Eq.refl (List.map-cong (λ e → preserves-⊆ n m n≤m e config) cs) ⟩
a V.-< List.map (λ e → NCC.⟦ e ⟧ (fnoc n m n≤m config)) cs >-
≡⟨⟩
NCC.⟦ a -< cs >- ⟧ (fnoc n m n≤m config)
∎
preserves-⊆ (sucs n) (sucs m) n≤m (d ⟨ cs ⟩) config =
NCC.⟦ grow (sucs n) (sucs m) n≤m (d ⟨ cs ⟩) ⟧ config
≡⟨⟩
NCC.⟦ d ⟨ Vec.saturate n≤m (Vec.map (grow (sucs n) (sucs m) n≤m) cs) ⟩ ⟧ config
≡⟨⟩
NCC.⟦ Vec.lookup (Vec.saturate n≤m (Vec.map (grow (sucs n) (sucs m) n≤m) cs)) (config d) ⟧ config
≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (Vec.saturate-map n≤m (grow (sucs n) (sucs m) n≤m) cs) refl) refl ⟩
NCC.⟦ Vec.lookup (Vec.map (grow (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) (config d) ⟧ config
≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (config d) (grow (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) refl ⟩
NCC.⟦ (grow (sucs n) (sucs m) n≤m) (Vec.lookup (Vec.saturate n≤m cs) (config d)) ⟧ config
≡⟨ preserves-⊆ (sucs n) (sucs m) n≤m (Vec.lookup (Vec.saturate n≤m cs) (config d)) config ⟩
NCC.⟦ Vec.lookup (Vec.saturate n≤m cs) (config d) ⟧ (fnoc (sucs n) (sucs m) n≤m config)
≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-saturate n≤m cs (config d)) refl ⟩
NCC.⟦ Vec.lookup cs (fnoc (sucs n) (sucs m) n≤m config d) ⟧ (fnoc (sucs n) (sucs m) n≤m config)
≡⟨⟩
NCC.⟦ d ⟨ cs ⟩ ⟧ (fnoc (sucs n) (sucs m) n≤m config)
∎
preserves-⊇ : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
→ (n m : ℕ≥ 2)
→ (n≤m : n ℕ≥.≤ m)
→ (expr : NCC n D i A)
→ NCC.⟦ expr ⟧ ⊆[ conf n m n≤m ] NCC.⟦ grow n m n≤m expr ⟧
preserves-⊇ n m n≤m (a -< cs >-) config =
a V.-< List.map (λ e → NCC.⟦ e ⟧ config) cs >-
≡⟨ Eq.cong₂ V._-<_>- Eq.refl (List.map-cong (λ e → preserves-⊇ n m n≤m e config) cs) ⟩
a V.-< List.map (λ e → NCC.⟦ grow n m n≤m e ⟧ (conf n m n≤m config)) cs >-
≡⟨ Eq.cong₂ V._-<_>- Eq.refl (List.map-∘ cs) ⟩
NCC.⟦ a -< List.map (grow n m n≤m) cs >- ⟧ (conf n m n≤m config)
≡⟨⟩
a V.-< List.map (λ e → NCC.⟦ e ⟧ (conf n m n≤m config)) (List.map (grow n m n≤m) cs) >-
∎
preserves-⊇ (sucs n) (sucs m) n≤m (d ⟨ cs ⟩) config =
NCC.⟦ d ⟨ cs ⟩ ⟧ config
≡⟨⟩
NCC.⟦ Vec.lookup cs (config d) ⟧ config
≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = cs}) (ℕ≥.cappedFin-toℕ (config d))) refl ⟨
NCC.⟦ Vec.lookup cs (ℕ≥.cappedFin (Fin.toℕ (config d))) ⟧ config
≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = cs}) (Eq.cong ℕ≥.cappedFin (Fin.toℕ-inject≤ (config d) n≤m))) refl ⟨
NCC.⟦ Vec.lookup cs (ℕ≥.cappedFin (Fin.toℕ (Fin.inject≤ (config d) n≤m))) ⟧ config
≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-saturate n≤m cs (Fin.inject≤ (config d) n≤m)) refl ⟨
NCC.⟦ Vec.lookup (Vec.saturate n≤m cs) (Fin.inject≤ (config d) n≤m) ⟧ config
≡⟨⟩
NCC.⟦ Vec.lookup (Vec.saturate n≤m cs) (conf (sucs n) (sucs m) n≤m config d) ⟧ config
≡⟨ preserves-⊇ (sucs n) (sucs m) n≤m (Vec.lookup (Vec.saturate n≤m cs) (conf (sucs n) (sucs m) n≤m config d)) config ⟩
NCC.⟦ (grow (sucs n) (sucs m) n≤m) (Vec.lookup (Vec.saturate n≤m cs) (conf (sucs n) (sucs m) n≤m config d)) ⟧ (conf (sucs n) (sucs m) n≤m config)
≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (conf (sucs n) (sucs m) n≤m config d) (grow (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) refl ⟨
NCC.⟦ Vec.lookup (Vec.map (grow (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) (conf (sucs n) (sucs m) n≤m config d) ⟧ (conf (sucs n) (sucs m) n≤m config)
≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (Vec.saturate-map n≤m (grow (sucs n) (sucs m) n≤m) cs) refl) refl ⟨
NCC.⟦ Vec.lookup (Vec.saturate n≤m (Vec.map (grow (sucs n) (sucs m) n≤m) cs)) (conf (sucs n) (sucs m) n≤m config d) ⟧ (conf (sucs n) (sucs m) n≤m config)
≡⟨⟩
NCC.⟦ d ⟨ Vec.saturate n≤m (Vec.map (grow (sucs n) (sucs m) n≤m) cs) ⟩ ⟧ (conf (sucs n) (sucs m) n≤m config)
≡⟨⟩
NCC.⟦ grow (sucs n) (sucs m) n≤m (d ⟨ cs ⟩) ⟧ (conf (sucs n) (sucs m) n≤m config)
∎
preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
→ (n m : ℕ≥ 2)
→ (n≤m : n ℕ≥.≤ m)
→ (expr : NCC n D i A)
→ NCC.⟦ grow n m n≤m expr ⟧ ≅[ fnoc n m n≤m ][ conf n m n≤m ] NCC.⟦ expr ⟧
preserves n m n≤m expr = preserves-⊆ n m n≤m expr , preserves-⊇ n m n≤m expr
growCompiler : ∀ {i : Size} {D : 𝔽}
→ (n m : ℕ≥ 2)
→ n ℕ≥.≤ m
→ LanguageCompiler (NCCL {i} n D) (NCCL {i} m D)
growCompiler n m n≤m .LanguageCompiler.compile = grow n m n≤m
growCompiler n m n≤m .LanguageCompiler.config-compiler expr .to = conf n m n≤m
growCompiler n m n≤m .LanguageCompiler.config-compiler expr .from = fnoc n m n≤m
growCompiler n m n≤m .LanguageCompiler.preserves expr = ≅[]-sym (preserves n m n≤m expr)
growFrom2Compiler : ∀ {i : Size} {D : 𝔽} → (n : ℕ≥ 2) → LanguageCompiler (NCCL {i} (sucs zero) D) (NCCL {i} n D)
growFrom2Compiler (sucs n) = growCompiler (sucs zero) (sucs n) (ℕ≥.lift≤ z≤n)