Skip to content

Commit 4bc1084

Browse files
pmbittnerpmbittner
committed
fix: argument order in VT semantics
1 parent 5e5e984 commit 4bc1084

4 files changed

Lines changed: 37 additions & 37 deletions

File tree

‎src/Vatras/Lang/VT.agda‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -40,29 +40,29 @@ mutual
4040
To prove termination and to simplify proofs, this definition is an inlined variant of
4141
configure-all c ts = concatMap (configure c) ts
4242
-}
43-
configure-all : ∀ {A} → Configuration → List (UnrootedVT A) → Forest A
44-
configure-all c [] = []
45-
configure-all c (x ∷ xs) = configure c x ++ configure-all c xs
43+
configure-all : ∀ {A} → List (UnrootedVT A) → Configuration → Forest A
44+
configure-all [] c = []
45+
configure-all (x ∷ xs) c = configure x c ++ configure-all xs c
4646

4747
{-|
4848
Corresponds to ⟦_⟧ on artifacts, options, and choices from the dissertation of Paul Bittner.
4949
-}
50-
configure : ∀ {A} → Configuration → UnrootedVT A → Forest A
51-
configure c (a -< cs >-) = a -< configure-all c cs >- ∷ []
52-
configure c (if[ p ]then[ t ]) =
50+
configure : ∀ {A} → UnrootedVT A → Configuration → Forest A
51+
configure (a -< cs >-) c = a -< configure-all cs c >- ∷ []
52+
configure (if[ p ]then[ t ]) c =
5353
if (eval p c)
54-
then configure-all c t
54+
then configure-all t c
5555
else []
56-
configure c (if[ p ]then[ t ]else[ e ]) =
56+
configure (if[ p ]then[ t ]else[ e ]) c =
5757
if (eval p c)
58-
then configure-all c t
59-
else configure-all c e
58+
then configure-all t c
59+
else configure-all e c
6060

6161
{-|
6262
Corresponds to ⟦_⟧ on the root term from the dissertation of Paul Bittner.
6363
-}
6464
⟦_⟧ : ∀ {A} → VT A → Configuration → Forest A
65-
⟦ if-true[ x ] ⟧ c = configure-all c x
65+
⟦ if-true[ x ] ⟧ = configure-all x
6666

6767
VTL : VariabilityLanguage Forest
6868
VTL = ⟪ VT , Configuration , ⟦_⟧ ⟫

‎src/Vatras/Lang/VT/Encode.agda‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -40,17 +40,17 @@ encode x = if-true[ encode-forest x ]
4040

4141
mutual
4242
encode-tree-preserves : ∀ {A} → (T : Rose ∞ A) (c : Configuration)
43-
→ configure c (encode-tree T) ≡ T ∷ []
43+
→ configure (encode-tree T) c ≡ T ∷ []
4444
encode-tree-preserves (a -< xs >-) c = Eq.cong (λ x → (a -< x >- ∷ [])) (encode-forest-preserves xs c)
4545

4646
encode-forest-preserves : ∀ {A} (V : Forest A) (c : Configuration)
47-
→ configure-all c (encode-forest V) ≡ V
47+
→ configure-all (encode-forest V) c ≡ V
4848
encode-forest-preserves [] _ = refl
4949
encode-forest-preserves (x ∷ xs) c =
5050
begin
51-
configure-all c (encode-forest (x ∷ xs))
51+
configure-all (encode-forest (x ∷ xs)) c
5252
≡⟨⟩
53-
configure c (encode-tree x) ++ configure-all c (encode-forest xs)
53+
configure (encode-tree x) c ++ configure-all (encode-forest xs) c
5454
≡⟨ cong₂ _++_ (encode-tree-preserves x c) (encode-forest-preserves xs c) ⟩
5555
(x ∷ []) ++ xs
5656
≡⟨⟩

‎src/Vatras/Translation/Lang/VT-to-ADT.agda‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -71,22 +71,22 @@ translate if-true[ xs ] = translate-all xs
7171

7272
-- Preservation Proofs --
7373

74-
preserves-all : ∀ {A} (vts : List (UnrootedVT A)) → flip configure-all vts ≗ ⟦ translate-all vts ⟧ₚ
74+
preserves-all : ∀ {A} (vts : List (UnrootedVT A)) → configure-all vts ≗ ⟦ translate-all vts ⟧ₚ
7575
preserves-all [] c = refl
7676
preserves-all (a -< l >- ∷ xs) c =
77-
flip configure-all (a -< l >- ∷ xs) c
77+
configure-all (a -< l >- ∷ xs) c
7878
≡⟨⟩
79-
a -< configure-all c l >- ∷ configure-all c xs
79+
a -< configure-all l c >- ∷ configure-all xs c
8080
≡⟨ cong (_ ∷_) (preserves-all xs c) ⟩
81-
a -< configure-all c l >- ∷ ⟦ translate-all xs ⟧ₚ c
81+
a -< configure-all l c >- ∷ ⟦ translate-all xs ⟧ₚ c
8282
≡⟨ cong (λ z → a -< z >- ∷ _) (preserves-all l c) ⟩
8383
a -< ⟦ translate-all l ⟧ₚ c >- ∷ ⟦ translate-all xs ⟧ₚ c
8484
≡⟨ push-down-left-spec a (translate-all l) (translate-all xs) c ⟨
8585
⟦ push-down-left a (translate-all l) (translate-all xs) ⟧ₚ c
8686
∎
8787
preserves-all (if[ p ]then[ l ] ∷ xs) c with eval p c
8888
... | true =
89-
configure-all c l ++ configure-all c xs
89+
configure-all l c ++ configure-all xs c
9090
≡⟨ cong₂ _++_ (preserves-all l c) (preserves-all xs c) ⟩
9191
⟦ translate-all l ⟧ₚ c ++ ⟦ translate-all xs ⟧ₚ c
9292
≡⟨ ⊕-specₚ (translate-all l) (translate-all xs) c ⟨

‎src/Vatras/Translation/Lang/VariantList-to-VT.agda‎

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -92,32 +92,32 @@ fnoci-invariant x xs n (suc m) (suc i) c (s≤s i≤m)
9292

9393
module Preservation (A : 𝔸) where
9494
translate'-preserves-conf : ∀ (x : Forest A) (xs : List (Forest A)) (n : ℕ) (i : ℕ) →
95-
configure-all (conf (i + n)) (translate' n x xs) ≡ VariantList.⟦ x ∷ xs ⟧ i
95+
configure-all (translate' n x xs) (conf (i + n)) ≡ VariantList.⟦ x ∷ xs ⟧ i
9696
translate'-preserves-conf x [] n i =
9797
begin
98-
configure-all (conf (i + n)) (encode-forest x)
98+
configure-all (encode-forest x) (conf (i + n))
9999
≡⟨ encode-idemp Forest A encoder (conf (i + n)) x ⟩
100100
x
101101
≡⟨⟩
102102
VariantList.⟦ x ∷ [] ⟧ i
103103
∎
104104
translate'-preserves-conf x (y ∷ ys) n zero rewrite ≡ᵇ-refl n =
105105
begin
106-
configure-all (conf n) (encode-forest x) ++ []
106+
configure-all (encode-forest x) (conf n) ++ []
107107
≡⟨ ++-identityʳ _ ⟩
108-
configure-all (conf n) (encode-forest x)
108+
configure-all (encode-forest x) (conf n)
109109
≡⟨ encode-idemp Forest A encoder (conf n) x ⟩
110110
x
111111
≡⟨⟩
112112
VariantList.⟦ x ∷ y ∷ ys ⟧ zero
113113
∎
114114
translate'-preserves-conf x (y ∷ ys) n (suc i) rewrite m+n≢ᵇn i n =
115115
begin
116-
configure-all (conf (suc i + n)) (translate' (suc n) y ys) ++ []
116+
configure-all (translate' (suc n) y ys) (conf (suc i + n)) ++ []
117117
≡⟨ ++-identityʳ _ ⟩
118-
configure-all (conf (suc i + n)) (translate' (suc n) y ys)
119-
≡⟨ cong (λ eq → configure-all (conf eq) (translate' (suc n) y ys)) (+-suc i n) ⟨
120-
configure-all (conf (i + suc n)) (translate' (suc n) y ys)
118+
configure-all (translate' (suc n) y ys) (conf (suc i + n))
119+
≡⟨ cong (λ eq → configure-all (translate' (suc n) y ys) (conf eq)) (+-suc i n) ⟨
120+
configure-all (translate' (suc n) y ys) (conf (i + suc n))
121121
≡⟨ translate'-preserves-conf y ys (suc n) i ⟩
122122
VariantList.⟦ y ∷ ys ⟧ i
123123
≡⟨⟩
@@ -130,31 +130,31 @@ module Preservation (A : 𝔸) where
130130
begin
131131
VariantList.⟦ x ∷ xs ⟧ i
132132
≡⟨ translate'-preserves-conf x xs zero i ⟨
133-
configure-all (conf (i + zero)) (translate' zero x xs)
134-
≡⟨ cong (λ eq → configure-all (conf eq) (translate' zero x xs)) (+-identityʳ i) ⟩
135-
configure-all (conf i) (translate' zero x xs)
133+
configure-all (translate' zero x xs) (conf (i + zero))
134+
≡⟨ cong (λ eq → configure-all (translate' zero x xs) (conf eq)) (+-identityʳ i) ⟩
135+
configure-all (translate' zero x xs) (conf i)
136136
≡⟨⟩
137137
⟦ translate (x ∷ xs) ⟧ (conf i)
138138
∎
139139

140140
translate'-preserves-fnoc : ∀ (x : Forest A) (xs : List (Forest A)) (n : ℕ) (c : Configuration) →
141-
configure-all c (translate' n x xs)
141+
configure-all (translate' n x xs) c
142142
≡ VariantList.⟦ x ∷ xs ⟧ (fnoci n (List⁺.length (x ∷ xs)) (List⁺.length (x ∷ xs)) c)
143143
translate'-preserves-fnoc x [] n c = encode-idemp Forest A encoder c x
144144
translate'-preserves-fnoc x (y ∷ ys) n c with c n in eq
145145
... | true rewrite n∸n≡0 (List⁺.length (y ∷ ys)) | +-identityʳ n | eq =
146146
begin
147-
configure-all c (encode-forest x) ++ []
147+
configure-all (encode-forest x) c ++ []
148148
≡⟨ ++-identityʳ _ ⟩
149-
configure-all c (encode-forest x)
149+
configure-all (encode-forest x) c
150150
≡⟨ encode-idemp Forest A encoder c x ⟩
151151
x
152152
∎
153153
... | false rewrite n∸n≡0 (List⁺.length (y ∷ ys)) | +-identityʳ n | eq =
154154
begin
155-
configure-all c (translate' (suc n) y ys) ++ []
155+
configure-all (translate' (suc n) y ys) c ++ []
156156
≡⟨ ++-identityʳ _ ⟩
157-
configure-all c (translate' (suc n) y ys)
157+
configure-all (translate' (suc n) y ys) c
158158
≡⟨ translate'-preserves-fnoc y ys (suc n) c ⟩
159159
VariantList.⟦ y ∷ ys ⟧
160160
(fnoci (suc n) (List⁺.length ( y ∷ ys)) (List⁺.length (y ∷ ys)) c)
@@ -169,7 +169,7 @@ module Preservation (A : 𝔸) where
169169
begin
170170
⟦ translate (x ∷ xs) ⟧ c
171171
≡⟨⟩
172-
configure-all c (translate' zero x xs)
172+
configure-all (translate' zero x xs) c
173173
≡⟨ translate'-preserves-fnoc x xs zero c ⟩
174174
VariantList.⟦ x ∷ xs ⟧ (fnoc (List⁺.length (x ∷ xs)) c)
175175
∎

0 commit comments

Comments
 (0)