From bcb7b35f2284cdd9023e14d7d815e0ae3f28bb59 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 25 Oct 2025 12:29:10 +0200 Subject: [PATCH 01/18] feat: remove the agda-stdlib submodule We will require the manual installation of the Agda standard library in order to have a single source of truth (Nix) of the Agda standard library version. --- .gitmodules | 3 --- agda-stdlib | 1 - makefile | 6 +++--- 3 files changed, 3 insertions(+), 7 deletions(-) delete mode 100644 .gitmodules delete mode 160000 agda-stdlib diff --git a/.gitmodules b/.gitmodules deleted file mode 100644 index c015d4d2..00000000 --- a/.gitmodules +++ /dev/null @@ -1,3 +0,0 @@ -[submodule "agda-stdlib"] - path = agda-stdlib - url = https://github.com/agda/agda-stdlib.git diff --git a/agda-stdlib b/agda-stdlib deleted file mode 160000 index 2b8fff10..00000000 --- a/agda-stdlib +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 2b8fff10f4033b91a6df4007e4a65cb10047c89c diff --git a/makefile b/makefile index ab294578..d19aaff9 100644 --- a/makefile +++ b/makefile @@ -3,16 +3,16 @@ andrun : build run check: - env AGDA_DIR="./libs" agda src/Vatras/Main.agda + agda src/Vatras/Main.agda check-all: ./scripts/check-all.sh check-everything: src/Vatras/Everything.agda - env AGDA_DIR="./libs" agda src/Vatras/Everything.agda + agda src/Vatras/Everything.agda build: - env AGDA_DIR="./libs" agda --compile src/Vatras/Main.agda + agda --compile src/Vatras/Main.agda build-2.6.4.3: env AGDA_DIR="./libs" agda-2.6.4.3 --compile src/Vatras/Main.agda From a23bc430f1d8844c4ed1666d3432f6cc74ea8402 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Tue, 14 Oct 2025 10:37:53 +0200 Subject: [PATCH 02/18] feat: update Agda to 2.8.0 --- Vatras.agda-lib | 2 +- makefile | 5 +---- nix/sources.json | 6 +++--- 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/Vatras.agda-lib b/Vatras.agda-lib index 2475cba4..1cfea5f3 100644 --- a/Vatras.agda-lib +++ b/Vatras.agda-lib @@ -1,4 +1,4 @@ name: Vatras -depend: standard-library-2.0 +depend: standard-library-2.3 include: src flags: --sized-types diff --git a/makefile b/makefile index d19aaff9..6398a474 100644 --- a/makefile +++ b/makefile @@ -1,4 +1,4 @@ -.PHONY: andrun check check-all check-everything build build-2.6.4.3 run clean +.PHONY: andrun check check-all check-everything build run clean andrun : build run @@ -14,9 +14,6 @@ check-everything: src/Vatras/Everything.agda build: agda --compile src/Vatras/Main.agda -build-2.6.4.3: - env AGDA_DIR="./libs" agda-2.6.4.3 --compile src/Vatras/Main.agda - run: ./src/Main diff --git a/nix/sources.json b/nix/sources.json index 05a914cc..6e47a00a 100644 --- a/nix/sources.json +++ b/nix/sources.json @@ -5,10 +5,10 @@ "homepage": null, "owner": "NixOS", "repo": "nixpkgs", - "rev": "fd281bd6b7d3e32ddfa399853946f782553163b5", - "sha256": "1hy81yj2dcg6kfsm63xcqf8kvigxglim1rcg1xpmy2rb6a8vqvsj", + "rev": "cf3f5c4def3c7b5f1fc012b3d839575dbe552d43", + "sha256": "0rvzsqn8qk46mw80apwr14m9crc6a1rv404r7zshy1aq82plmbsc", "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/fd281bd6b7d3e32ddfa399853946f782553163b5.tar.gz", + "url": "https://github.com/NixOS/nixpkgs/archive/cf3f5c4def3c7b5f1fc012b3d839575dbe552d43.tar.gz", "url_template": "https://github.com///archive/.tar.gz" } } From efb02f2608f46351f5b6348b28553c83e58b20d6 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 25 Oct 2025 12:31:18 +0200 Subject: [PATCH 03/18] fix: warning in OC-to-2CC --- src/Vatras/Translation/Lang/OC-to-2CC.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Vatras/Translation/Lang/OC-to-2CC.lagda.md b/src/Vatras/Translation/Lang/OC-to-2CC.lagda.md index 5287217e..54efcf83 100644 --- a/src/Vatras/Translation/Lang/OC-to-2CC.lagda.md +++ b/src/Vatras/Translation/Lang/OC-to-2CC.lagda.md @@ -397,7 +397,7 @@ preservesₒ c (T-artifact {a = a} {b = b} {ls = ls} {es = es} {rs = rs} {e₁ = preservesₒ c (T-option {a = a} {O = O} {e = e} {ls = ls} {rs = rs} {eᵒ⁻ʸ = ey} {eᵒ⁻ⁿ = en} ⟶ey ⟶en) with c O ... | true = begin Artifactᵥ a (map (flip ⟦_⟧₂ c) ls ++ (catMaybes (⟦ e ⟧ₒ c ∷ map (flip ⟦_⟧ₒ c) (toList rs)))) - ≡⟨ preservesₒ-option-size e ⟩ -- prove that size constraint on e does not matter for ⟦_⟧ₒ + ≡⟨ preservesₒ-option-size {rs = rs} e ⟩ -- prove that size constraint on e does not matter for ⟦_⟧ₒ ⟦ a -< ls ≪ e ∷ rs >- ⟧ₜ c ≡⟨ preservesₒ c ⟶ey ⟩ -- apply induction hypothesis ⟦ ey ⟧₂ c From a6c3a902147b3a5f3b56580da7c2a735bc8f6a6f Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 14 Oct 2025 12:57:56 +0200 Subject: [PATCH 04/18] fix: deprecation warnings --- src/Vatras/Framework/Variants.agda | 2 +- src/Vatras/Show/Lines.agda | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Vatras/Framework/Variants.agda b/src/Vatras/Framework/Variants.agda index b1c2780b..3e910f8d 100644 --- a/src/Vatras/Framework/Variants.agda +++ b/src/Vatras/Framework/Variants.agda @@ -146,7 +146,7 @@ module _ (V : 𝕍) (A : 𝔸) {L : VariabilityLanguage V} (encoder : VariantEnc -- atom containment open import Relation.Nullary.Decidable using (yes; no) open import Data.Bool using (Bool; true) -open import Data.List using (or) +open import Data.Bool.ListAction using (or) has-atom : ∀ {A i} → atoms A → Rose i A → Bool has-atom {A , _≟_} a (b -< cs >-) with a ≟ b diff --git a/src/Vatras/Show/Lines.agda b/src/Vatras/Show/Lines.agda index e39eb457..d118ecb9 100644 --- a/src/Vatras/Show/Lines.agda +++ b/src/Vatras/Show/Lines.agda @@ -7,6 +7,7 @@ open import Data.Bool using (true; false; if_then_else_; _∧_) open import Data.Char as Char using (Char) open import Data.Nat using (ℕ; _*_; _∸_; ⌊_/2⌋; ⌈_/2⌉; _≤ᵇ_) open import Data.List as List using (List; _∷_; [_]; concat; splitAt; _∷ʳ_) +open import Data.Nat.ListAction using (sum) open import Data.Maybe using (nothing; just) open import Data.String using (String; _++_; _==_; replicate; fromChar; toList; fromList; Alignment; fromAlignment) open import Data.Product as Prod using (_,_; proj₁; map₁) @@ -48,7 +49,7 @@ charWidth c = codePoint = Char.toℕ c stringLength : String → ℕ -stringLength line = List.sum (List.map charWidth (Data.String.toList line)) +stringLength line = sum (List.map charWidth (Data.String.toList line)) length : Line → ℕ length line = stringLength (content line) From 6c692234389a11b0cfa27d0f8feed035cddc443a Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 14 Oct 2025 14:16:04 +0200 Subject: [PATCH 05/18] fix: warning in FST-to-OC MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Eq.cong₂ was not able to infer the second argument automatically anymore. We had to spell it out explicitly. --- src/Vatras/Translation/Lang/FST-to-OC.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Vatras/Translation/Lang/FST-to-OC.lagda.md b/src/Vatras/Translation/Lang/FST-to-OC.lagda.md index 9a960eba..f8fa33b1 100644 --- a/src/Vatras/Translation/Lang/FST-to-OC.lagda.md +++ b/src/Vatras/Translation/Lang/FST-to-OC.lagda.md @@ -282,10 +282,10 @@ induction (e@(_ ❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | just _ | jus 0 -< [] >- ∷ OC.⟦ cs ⟧ₒ-recurse (c₁ ∧ c₂) ≡⟨⟩ catMaybes (just (0 -< [] >-) ∷ List.map (flip OC.⟦_⟧ₒ (c₁ ∧ c₂)) cs) - ≡⟨ Eq.cong catMaybes (Eq.cong₂ _∷_ (shared-artifact e c₁ c₂ - (Eq.trans (Eq.cong just (List.∷-injectiveˡ p₁)) (Eq.sym ⟦e⟧c₁)) - (Eq.trans (Eq.cong just (List.∷-injectiveˡ p₂)) (Eq.sym ⟦e⟧c₂))) - refl) ⟩ + ≡⟨ Eq.cong (λ eq → catMaybes (eq ∷ (List.map (flip OC.⟦_⟧ₒ (c₁ ∧ c₂)) cs))) + (shared-artifact e c₁ c₂ + (Eq.trans (Eq.cong just (List.∷-injectiveˡ p₁)) (Eq.sym ⟦e⟧c₁)) + (Eq.trans (Eq.cong just (List.∷-injectiveˡ p₂)) (Eq.sym ⟦e⟧c₂))) ⟩ catMaybes (OC.⟦ e ⟧ₒ (c₁ ∧ c₂) ∷ List.map (flip OC.⟦_⟧ₒ (c₁ ∧ c₂)) cs) ≡⟨⟩ OC.⟦ e ∷ cs ⟧ₒ-recurse (c₁ ∧ c₂) From c2faec60384e3955d7381920b695f25db3a8996e Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 14 Oct 2025 14:39:37 +0200 Subject: [PATCH 06/18] fix: broken proof in FST-to-OC after STL upgrade --- src/Vatras/Translation/Lang/FST-to-OC.lagda.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/Vatras/Translation/Lang/FST-to-OC.lagda.md b/src/Vatras/Translation/Lang/FST-to-OC.lagda.md index f8fa33b1..6a7f30ba 100644 --- a/src/Vatras/Translation/Lang/FST-to-OC.lagda.md +++ b/src/Vatras/Translation/Lang/FST-to-OC.lagda.md @@ -278,17 +278,15 @@ induction (e@(_ ❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | just _ | jus induction (e@(_ ❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | just _ | just _ | nothing | _ with OC.⟦ cs ⟧ₒ-recurse (c₁ ∧ c₂) in ⟦cs⟧c₁∧c₂ | OC.⟦ cs ⟧ₒ-recurse c₁ | subtreeₒ-recurse cs (c₁ ∧ c₂) c₁ implies-∧₁ induction (e@(_ ❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | just _ | just _ | nothing | _ | .[] | .[] | [] = inj₂ ( 0 -< [] >- ∷ [] - ≡⟨ Eq.cong₂ _∷_ refl ⟦cs⟧c₁∧c₂ ⟨ - 0 -< [] >- ∷ OC.⟦ cs ⟧ₒ-recurse (c₁ ∧ c₂) ≡⟨⟩ - catMaybes (just (0 -< [] >-) ∷ List.map (flip OC.⟦_⟧ₒ (c₁ ∧ c₂)) cs) - ≡⟨ Eq.cong (λ eq → catMaybes (eq ∷ (List.map (flip OC.⟦_⟧ₒ (c₁ ∧ c₂)) cs))) + catMaybes (just (0 -< [] >-) ∷ []) + ≡⟨ Eq.cong (λ eq → catMaybes (eq ∷ [])) (shared-artifact e c₁ c₂ (Eq.trans (Eq.cong just (List.∷-injectiveˡ p₁)) (Eq.sym ⟦e⟧c₁)) (Eq.trans (Eq.cong just (List.∷-injectiveˡ p₂)) (Eq.sym ⟦e⟧c₂))) ⟩ - catMaybes (OC.⟦ e ⟧ₒ (c₁ ∧ c₂) ∷ List.map (flip OC.⟦_⟧ₒ (c₁ ∧ c₂)) cs) + catMaybes (OC.⟦ e ⟧ₒ (c₁ ∧ c₂) ∷ []) ≡⟨⟩ - OC.⟦ e ∷ cs ⟧ₒ-recurse (c₁ ∧ c₂) + OC.⟦ e ∷ [] ⟧ₒ-recurse (c₁ ∧ c₂) ∎) ``` From 9fe328f019b83bae65ce101e59402e30c4deae1a Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 14 Oct 2025 15:08:12 +0200 Subject: [PATCH 07/18] reuse if-then-else lemmata merged into STL --- src/Vatras/Lang/ADT/Merge.agda | 2 - src/Vatras/Translation/Lang/ADT-to-VT.agda | 4 +- .../Translation/Lang/ADT/ADT-vs-PropADT.agda | 12 ++--- src/Vatras/Translation/Lang/VT/Rename.agda | 18 +++---- src/Vatras/Util/AuxProofs.agda | 51 +------------------ 5 files changed, 18 insertions(+), 69 deletions(-) diff --git a/src/Vatras/Lang/ADT/Merge.agda b/src/Vatras/Lang/ADT/Merge.agda index eb82a526..01a1d54f 100644 --- a/src/Vatras/Lang/ADT/Merge.agda +++ b/src/Vatras/Lang/ADT/Merge.agda @@ -9,8 +9,6 @@ open import Data.Bool.Properties using (if-float) open import Relation.Binary.PropositionalEquality using (refl; _≡_; _≗_) open Relation.Binary.PropositionalEquality.≡-Reasoning -open import Vatras.Util.AuxProofs using (if-cong) - import Vatras.Lang.ADT module Named (F : 𝔽) where diff --git a/src/Vatras/Translation/Lang/ADT-to-VT.agda b/src/Vatras/Translation/Lang/ADT-to-VT.agda index 59565235..60804850 100644 --- a/src/Vatras/Translation/Lang/ADT-to-VT.agda +++ b/src/Vatras/Translation/Lang/ADT-to-VT.agda @@ -6,6 +6,7 @@ open import Vatras.Framework.Definitions using (𝔽) module Vatras.Translation.Lang.ADT-to-VT (F : 𝔽) where open import Data.Bool using (if_then_else_) +open import Data.Bool.Properties using (if-cong₂) open import Data.List using (List; []; _∷_; _++_) open import Data.List.Properties using (++-identityʳ) open import Function using (id; _∘_) @@ -25,7 +26,6 @@ open import Vatras.Lang.VT.Encode F using (encode-forest; encode-forest-preserve open import Vatras.Framework.Relation.Expressiveness Forest using (_≽_; expressiveness-from-compiler) open import Vatras.Translation.Lang.ADT.ADT-vs-PropADT F Forest using (lift-compiler; ADT≽PropADT) -open import Vatras.Util.AuxProofs using (if-cong) translate' : ∀ {A} → PropADT A → List (UnrootedVT A) translate' (leaf v) = encode-forest v @@ -40,7 +40,7 @@ preserves (D ⟨ l , r ⟩) c = ⟦ D ⟨ l , r ⟩ ⟧ₚ c ≡⟨⟩ (if eval D c then ⟦ l ⟧ₚ c else ⟦ r ⟧ₚ c) - ≡⟨ if-cong (eval D c) (preserves l c) (preserves r c) ⟩ + ≡⟨ if-cong₂ (eval D c) (preserves l c) (preserves r c) ⟩ (if eval D c then configure-all (translate' l) c else configure-all (translate' r) c) ≡⟨ ++-identityʳ _ ⟨ (if eval D c then configure-all (translate' l) c else configure-all (translate' r) c) ++ [] diff --git a/src/Vatras/Translation/Lang/ADT/ADT-vs-PropADT.agda b/src/Vatras/Translation/Lang/ADT/ADT-vs-PropADT.agda index 27c31417..81a875d9 100644 --- a/src/Vatras/Translation/Lang/ADT/ADT-vs-PropADT.agda +++ b/src/Vatras/Translation/Lang/ADT/ADT-vs-PropADT.agda @@ -2,6 +2,7 @@ open import Vatras.Framework.Definitions using (𝔽; 𝕍; 𝔸) module Vatras.Translation.Lang.ADT.ADT-vs-PropADT (F : 𝔽) (V : 𝕍) where open import Data.Bool using (if_then_else_; not) renaming (_∧_ to _and_) +open import Data.Bool.Properties using (if-not; if-∧; if-cong₂; if-cong-then) open import Data.Product using (_,_) open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (_≗_; refl) @@ -15,7 +16,6 @@ open ADT hiding (⟦_⟧) open import Vatras.Data.EqIndexedSet using (≗→≅[]) open import Vatras.Data.Prop open import Vatras.Lang.ADT.Prop F V using (⟦_⟧ₚ; PropADTL) -open import Vatras.Util.AuxProofs using (if-flip; if-∧; if-cong; if-congˡ) open import Vatras.Framework.Compiler using (LanguageCompiler) open import Vatras.Framework.Relation.Expressiveness V using (_≋_; _≽_; expressiveness-from-compiler) @@ -57,7 +57,7 @@ elim-sem P l r c = if eval P c then ⟦ l ⟧ c else ⟦ r ⟧ c elim-sem (¬ P) l r c ≡⟨⟩ (if not (eval P c) then ⟦ l ⟧ c else ⟦ r ⟧ c) - ≡⟨ if-flip (eval P c) _ _ ⟩ + ≡⟨ if-not (eval P c) ⟩ (if eval P c then ⟦ r ⟧ c else ⟦ l ⟧ c) ≡⟨⟩ elim-sem P r l c @@ -70,11 +70,11 @@ elim-sem P l r c = if eval P c then ⟦ l ⟧ c else ⟦ r ⟧ c elim-sem (P ∧ Q) l r c ≡⟨⟩ (if eval P c and eval Q c then ⟦ l ⟧ c else ⟦ r ⟧ c) - ≡⟨ if-∧ (eval P c) (eval Q c) _ _ ⟩ + ≡⟨ if-∧ (eval P c) ⟩ (if eval P c then (if eval Q c then ⟦ l ⟧ c else ⟦ r ⟧ c) else ⟦ r ⟧ c) ≡⟨⟩ (if eval P c then elim-sem Q l r c else ⟦ r ⟧ c) - ≡⟨ if-congˡ (eval P c) (↓-presʳ Q l r c) ⟩ + ≡⟨ if-cong-then (eval P c) (↓-presʳ Q l r c) ⟩ (if eval P c then ⟦ ↓ Q ⟨ l , r ⟩ ⟧ c else ⟦ r ⟧ c) ≡⟨⟩ elim-sem P (↓ Q ⟨ l , r ⟩) r c @@ -85,7 +85,7 @@ elim-sem P l r c = if eval P c then ⟦ l ⟧ c else ⟦ r ⟧ c mutual ↓-presˡ : ∀ {A} (P : Prop F) (l r : ADT (Prop F) A) → ⟦ P ⟨ l , r ⟩ ⟧ₚ ≗ elim-sem P (elim-formulas l) (elim-formulas r) - ↓-presˡ P l r c = if-cong _ (preserves l c) (preserves r c) + ↓-presˡ P l r c = if-cong₂ _ (preserves l c) (preserves r c) preserves : ∀ {A} @@ -120,7 +120,7 @@ lift (D ⟨ l , r ⟩) = var D ⟨ lift l , lift r ⟩ lift-preserves : ∀ {A} → (e : ADT F A) → ⟦ e ⟧ ≗ ⟦ lift e ⟧ₚ lift-preserves (leaf x) c = refl -lift-preserves (D ⟨ l , r ⟩) c = if-cong (c D) (lift-preserves l c) (lift-preserves r c) +lift-preserves (D ⟨ l , r ⟩) c = if-cong₂ (c D) (lift-preserves l c) (lift-preserves r c) lift-compiler : LanguageCompiler (ADTL F) PropADTL lift-compiler = record diff --git a/src/Vatras/Translation/Lang/VT/Rename.agda b/src/Vatras/Translation/Lang/VT/Rename.agda index 0b6e491e..0bf591ab 100644 --- a/src/Vatras/Translation/Lang/VT/Rename.agda +++ b/src/Vatras/Translation/Lang/VT/Rename.agda @@ -11,12 +11,12 @@ variants. module Vatras.Translation.Lang.VT.Rename where open import Data.Bool using (if_then_else_) +open import Data.Bool.Properties using (if-cong; if-cong-then; if-cong₂) open import Data.List as List using (List; []; _∷_; _++_) open import Data.Product using (_,_) open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (refl; _≗_) -open import Vatras.Util.AuxProofs using (if-congˡ; if-cong) open import Vatras.Data.EqIndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) open import Vatras.Framework.Compiler using (LanguageCompiler) open import Vatras.Framework.Definitions using (𝔸; 𝔽) @@ -79,9 +79,9 @@ module _ {D₁ D₂ : 𝔽} {A : 𝔸} (f : D₁ → D₂) where VT.configure (rename' f (if[ p ]then[ l ])) config ≡⟨⟩ (if Prop.eval (Prop.rename f p) config then VT.configure-all (rename'-all f l) config else []) - ≡⟨ Eq.cong (if_then _ else []) (Prop.rename-spec f p config) ⟩ + ≡⟨ if-cong (Prop.rename-spec f p config) ⟩ (if Prop.eval p (config ∘ f) then VT.configure-all (rename'-all f l) config else []) - ≡⟨ if-congˡ (Prop.eval p (config ∘ f)) (preserves-⊆-all l config) ⟩ + ≡⟨ if-cong-then (Prop.eval p (config ∘ f)) (preserves-⊆-all l config) ⟩ (if Prop.eval p (config ∘ f) then VT.configure-all l (config ∘ f) else []) ≡⟨⟩ VT.configure (if[ p ]then[ l ]) (config ∘ f) @@ -90,9 +90,9 @@ module _ {D₁ D₂ : 𝔽} {A : 𝔸} (f : D₁ → D₂) where VT.configure (rename' f (if[ p ]then[ l ]else[ r ])) config ≡⟨⟩ (if Prop.eval (Prop.rename f p) config then VT.configure-all (rename'-all f l) config else VT.configure-all (rename'-all f r) config) - ≡⟨ Eq.cong (if_then _ else _) (Prop.rename-spec f p config) ⟩ + ≡⟨ if-cong (Prop.rename-spec f p config) ⟩ (if Prop.eval p (config ∘ f) then VT.configure-all (rename'-all f l) config else VT.configure-all (rename'-all f r) config) - ≡⟨ if-cong _ (preserves-⊆-all l config) (preserves-⊆-all r config) ⟩ + ≡⟨ if-cong₂ _ (preserves-⊆-all l config) (preserves-⊆-all r config) ⟩ (if Prop.eval p (config ∘ f) then VT.configure-all l (config ∘ f) else VT.configure-all r (config ∘ f)) ≡⟨⟩ VT.configure (if[ p ]then[ l ]else[ r ]) (config ∘ f) @@ -121,9 +121,9 @@ module _ {D₁ D₂ : 𝔽} {A : 𝔸} (f : D₁ → D₂) (f⁻¹ : D₂ → D VT.configure (if[ p ]then[ l ]) config ≡⟨⟩ (if Prop.eval p config then VT.configure-all l config else []) - ≡⟨ if-congˡ (Prop.eval p config) (preserves-⊇-all l config) ⟩ + ≡⟨ if-cong-then (Prop.eval p config) (preserves-⊇-all l config) ⟩ (if Prop.eval p config then VT.configure-all (rename'-all f l) (config ∘ f⁻¹) else []) - ≡⟨ Eq.cong (if_then _ else []) (Prop.rename-preserves f f⁻¹ f∘f⁻¹≗id p config) ⟨ + ≡⟨ if-cong (Prop.rename-preserves f f⁻¹ f∘f⁻¹≗id p config) ⟨ (if Prop.eval (Prop.rename f p) (config ∘ f⁻¹) then VT.configure-all (rename'-all f l) (config ∘ f⁻¹) else []) ≡⟨⟩ VT.configure (rename' f (if[ p ]then[ l ])) (config ∘ f⁻¹) @@ -132,9 +132,9 @@ module _ {D₁ D₂ : 𝔽} {A : 𝔸} (f : D₁ → D₂) (f⁻¹ : D₂ → D VT.configure (if[ p ]then[ l ]else[ r ]) config ≡⟨⟩ (if Prop.eval p config then VT.configure-all l config else VT.configure-all r config) - ≡⟨ if-cong _ (preserves-⊇-all l config) (preserves-⊇-all r config) ⟩ + ≡⟨ if-cong₂ _ (preserves-⊇-all l config) (preserves-⊇-all r config) ⟩ (if Prop.eval p config then VT.configure-all (rename'-all f l) (config ∘ f⁻¹) else VT.configure-all (rename'-all f r) (config ∘ f⁻¹)) - ≡⟨ Eq.cong (if_then _ else _) (Prop.rename-preserves f f⁻¹ f∘f⁻¹≗id p config) ⟨ + ≡⟨ if-cong (Prop.rename-preserves f f⁻¹ f∘f⁻¹≗id p config) ⟨ (if Prop.eval (Prop.rename f p) (config ∘ f⁻¹) then VT.configure-all (rename'-all f l) (config ∘ f⁻¹) else VT.configure-all (rename'-all f r) (config ∘ f⁻¹)) ≡⟨⟩ VT.configure (rename' f (if[ p ]then[ l ]else[ r ])) (config ∘ f⁻¹) diff --git a/src/Vatras/Util/AuxProofs.agda b/src/Vatras/Util/AuxProofs.agda index 23090122..d82ab5ae 100644 --- a/src/Vatras/Util/AuxProofs.agda +++ b/src/Vatras/Util/AuxProofs.agda @@ -3,7 +3,7 @@ module Vatras.Util.AuxProofs where open import Level using (Level) open import Function using (id; _∘_) -open import Data.Bool using (Bool; false; true; if_then_else_; not; _∧_) +open import Data.Bool using (Bool; false; true) open import Data.Fin using (Fin; zero; suc; fromℕ<) open import Data.Nat using (ℕ; zero; suc; NonZero; _≡ᵇ_; _⊓_; _+_; _∸_; _<_; _≤_; s≤s; z≤n) open import Data.Nat.Properties using (n<1+n; m⊓n≤m; +-comm; +-∸-comm; n∸n≡0; m≤n+m; +-∸-assoc) @@ -57,55 +57,6 @@ n∸1+m Date: Tue, 14 Oct 2025 15:08:40 +0200 Subject: [PATCH 08/18] remove an unused AuxProof function --- src/Vatras/Util/AuxProofs.agda | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/src/Vatras/Util/AuxProofs.agda b/src/Vatras/Util/AuxProofs.agda index d82ab5ae..439c2734 100644 --- a/src/Vatras/Util/AuxProofs.agda +++ b/src/Vatras/Util/AuxProofs.agda @@ -43,16 +43,6 @@ n Date: Tue, 14 Oct 2025 15:08:57 +0200 Subject: [PATCH 09/18] remove resolved AuxProof todo --- src/Vatras/Util/AuxProofs.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Vatras/Util/AuxProofs.agda b/src/Vatras/Util/AuxProofs.agda index 439c2734..fdd918d9 100644 --- a/src/Vatras/Util/AuxProofs.agda +++ b/src/Vatras/Util/AuxProofs.agda @@ -26,7 +26,6 @@ true≢false : ∀ {a : Bool} true≢false refl () ----- Some arithmetic properties --- TODO: Contribute some of these functions to STL ≡ᵇ-refl : ∀ (n : ℕ) → (n ≡ᵇ n) ≡ true ≡ᵇ-refl zero = refl From e28b6048e02ad41a8593ebb2bc4927beefb3d125 Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 14 Oct 2025 15:09:08 +0200 Subject: [PATCH 10/18] clean imports in AuxProofs.agda --- src/Vatras/Util/AuxProofs.agda | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/Vatras/Util/AuxProofs.agda b/src/Vatras/Util/AuxProofs.agda index fdd918d9..b803fefb 100644 --- a/src/Vatras/Util/AuxProofs.agda +++ b/src/Vatras/Util/AuxProofs.agda @@ -4,11 +4,8 @@ open import Level using (Level) open import Function using (id; _∘_) open import Data.Bool using (Bool; false; true) -open import Data.Fin using (Fin; zero; suc; fromℕ<) -open import Data.Nat using (ℕ; zero; suc; NonZero; _≡ᵇ_; _⊓_; _+_; _∸_; _<_; _≤_; s≤s; z≤n) -open import Data.Nat.Properties using (n<1+n; m⊓n≤m; +-comm; +-∸-comm; n∸n≡0; m≤n+m; +-∸-assoc) -open import Data.Fin using (Fin; zero; suc; fromℕ<) -open import Data.List.Properties using (length-++) +open import Data.Nat using (ℕ; zero; suc; _≡ᵇ_; _+_; _∸_; _<_; _≤_; s≤s; z≤n) +open import Data.Nat.Properties using (n<1+n; n∸n≡0; m≤n+m) open import Data.Product using (_×_; _,_) open import Relation.Binary using (DecidableEquality) open import Relation.Nullary.Decidable using (yes; no) From 2db714fc88c871a0e3f5005d7419a2ac14c3193d Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 14 Oct 2025 15:18:46 +0200 Subject: [PATCH 11/18] refactor: use if-then-else lemmas where applicable this simplified two proof steps significantly --- src/Vatras/Lang/ADT/Pushdown.agda | 2 +- src/Vatras/Translation/Lang/2CC-to-ADT.agda | 3 ++- src/Vatras/Translation/Lang/2CC/Idempotence.agda | 2 +- src/Vatras/Translation/Lang/2CC/Rename.agda | 8 +++----- src/Vatras/Translation/Lang/ADT-to-2CC.agda | 2 +- src/Vatras/Translation/Lang/ADT-to-NADT.agda | 4 ++-- src/Vatras/Translation/Lang/ADT/Rename.agda | 6 +++--- src/Vatras/Translation/Lang/ADT/WalkSemantics.agda | 3 ++- src/Vatras/Translation/Lang/NCC-to-2CC.agda | 5 +++-- 9 files changed, 18 insertions(+), 17 deletions(-) diff --git a/src/Vatras/Lang/ADT/Pushdown.agda b/src/Vatras/Lang/ADT/Pushdown.agda index de90b147..654aadf9 100644 --- a/src/Vatras/Lang/ADT/Pushdown.agda +++ b/src/Vatras/Lang/ADT/Pushdown.agda @@ -48,7 +48,7 @@ push-down-artifact {A = A} a cs = go cs [] (if config d then ⟦ go a cs (c₁ ∷ cs') vs ⟧ config else ⟦ go a cs (c₂ ∷ cs') vs ⟧ config) - ≡⟨ Eq.cong₂ (if config d then_else_) (go' (c₁ ∷ cs') vs) (go' (c₂ ∷ cs') vs) ⟩ + ≡⟨ Bool.if-cong₂ _ (go' (c₁ ∷ cs') vs) (go' (c₂ ∷ cs') vs) ⟩ (if config d then a -< vs ʳ++ List.map (λ e → ⟦ e ⟧ config) (c₁ ∷ cs') >- else a -< vs ʳ++ List.map (λ e → ⟦ e ⟧ config) (c₂ ∷ cs') >-) diff --git a/src/Vatras/Translation/Lang/2CC-to-ADT.agda b/src/Vatras/Translation/Lang/2CC-to-ADT.agda index ba43781e..1d740206 100644 --- a/src/Vatras/Translation/Lang/2CC-to-ADT.agda +++ b/src/Vatras/Translation/Lang/2CC-to-ADT.agda @@ -10,6 +10,7 @@ module Vatras.Translation.Lang.2CC-to-ADT where open import Size using (Size; ∞) import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Bool as Bool using (if_then_else_) +import Data.Bool.Properties as Bool open import Data.List as List using (List; []; _∷_; _ʳ++_) import Data.List.Properties as List open import Vatras.Framework.Compiler using (LanguageCompiler) @@ -59,7 +60,7 @@ preserves-≗ (d ⟨ l , r ⟩) config = ADT.⟦ d ⟨ translate l , translate r ⟩ ⟧ config ≡⟨⟩ (if config d then ADT.⟦ translate l ⟧ config else ADT.⟦ translate r ⟧ config) - ≡⟨ Eq.cong₂ (if config d then_else_) (preserves-≗ l config) (preserves-≗ r config) ⟩ + ≡⟨ Bool.if-cong₂ _ (preserves-≗ l config) (preserves-≗ r config) ⟩ 2CC.⟦ d ⟨ l , r ⟩ ⟧ config ∎ diff --git a/src/Vatras/Translation/Lang/2CC/Idempotence.agda b/src/Vatras/Translation/Lang/2CC/Idempotence.agda index de305e44..4efc6f1b 100644 --- a/src/Vatras/Translation/Lang/2CC/Idempotence.agda +++ b/src/Vatras/Translation/Lang/2CC/Idempotence.agda @@ -60,7 +60,7 @@ eliminate-idempotent-choices-preserves (a -< cs >-) c = eliminate-idempotent-choices-preserves (D ⟨ l , r ⟩) c with eliminate-idempotent-choices l ≟ eliminate-idempotent-choices r eliminate-idempotent-choices-preserves (D ⟨ l , r ⟩) c | no l≢r = (if c D then ⟦ eliminate-idempotent-choices l ⟧ c else ⟦ eliminate-idempotent-choices r ⟧ c) - ≡⟨ Eq.cong₂ (if c D then_else_) (eliminate-idempotent-choices-preserves l c) (eliminate-idempotent-choices-preserves r c) ⟩ + ≡⟨ Bool.if-cong₂ _ (eliminate-idempotent-choices-preserves l c) (eliminate-idempotent-choices-preserves r c) ⟩ (if c D then ⟦ l ⟧ c else ⟦ r ⟧ c) ≡⟨⟩ ⟦ D ⟨ l , r ⟩ ⟧ c diff --git a/src/Vatras/Translation/Lang/2CC/Rename.agda b/src/Vatras/Translation/Lang/2CC/Rename.agda index bfa07749..2cbbfa4a 100644 --- a/src/Vatras/Translation/Lang/2CC/Rename.agda +++ b/src/Vatras/Translation/Lang/2CC/Rename.agda @@ -67,7 +67,7 @@ preserves-⊆ f (d ⟨ l , r ⟩) config = 2CC.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ config ≡⟨⟩ (if config (f d) then 2CC.⟦ rename f l ⟧ config else 2CC.⟦ rename f r ⟧ config) - ≡⟨ Eq.cong₂ (if config (f d) then_else_) (preserves-⊆ f l config) (preserves-⊆ f r config) ⟩ + ≡⟨ Bool.if-cong₂ _ (preserves-⊆ f l config) (preserves-⊆ f r config) ⟩ (if config (f d) then 2CC.⟦ l ⟧ (config ∘ f) else 2CC.⟦ r ⟧ (config ∘ f)) ≡⟨⟩ 2CC.⟦ d ⟨ l , r ⟩ ⟧ (config ∘ f) @@ -96,11 +96,9 @@ preserves-⊇ f f⁻¹ is-inverse (d ⟨ l , r ⟩) config = 2CC.⟦ d ⟨ l , r ⟩ ⟧ config ≡⟨⟩ (if config d then 2CC.⟦ l ⟧ config else 2CC.⟦ r ⟧ config) - ≡⟨ Eq.cong₂ (if config d then_else_) (preserves-⊇ f f⁻¹ is-inverse l config) (preserves-⊇ f f⁻¹ is-inverse r config) ⟩ + ≡⟨ Bool.if-cong₂ _ (preserves-⊇ f f⁻¹ is-inverse l config) (preserves-⊇ f f⁻¹ is-inverse r config) ⟩ (if config d then 2CC.⟦ rename f l ⟧ (config ∘ f⁻¹) else 2CC.⟦ rename f r ⟧ (config ∘ f⁻¹)) - ≡⟨ Eq.cong (if_then 2CC.⟦ rename f l ⟧ (config ∘ f⁻¹) else 2CC.⟦ rename f r ⟧ (config ∘ f⁻¹)) - (Eq.cong config - (Eq.sym (is-inverse d))) ⟩ + ≡⟨ Bool.if-cong (Eq.cong config (Eq.sym (is-inverse d))) ⟩ (if (config ∘ f⁻¹) (f d) then 2CC.⟦ rename f l ⟧ (config ∘ f⁻¹) else 2CC.⟦ rename f r ⟧ (config ∘ f⁻¹)) ≡⟨⟩ 2CC.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ (config ∘ f⁻¹) diff --git a/src/Vatras/Translation/Lang/ADT-to-2CC.agda b/src/Vatras/Translation/Lang/ADT-to-2CC.agda index e92517fa..8ea0050a 100644 --- a/src/Vatras/Translation/Lang/ADT-to-2CC.agda +++ b/src/Vatras/Translation/Lang/ADT-to-2CC.agda @@ -47,7 +47,7 @@ preserves-≗ Variant→2CC (f ⟨ l , r ⟩) config = 2CC.⟦ f ⟨ translate Variant→2CC l , translate Variant→2CC r ⟩ ⟧ config ≡⟨⟩ (if config f then 2CC.⟦ translate Variant→2CC l ⟧ config else 2CC.⟦ translate Variant→2CC r ⟧ config) - ≡⟨ Eq.cong₂ (if config f then_else_) (preserves-≗ Variant→2CC l config) (preserves-≗ Variant→2CC r config) ⟩ + ≡⟨ Bool.if-cong₂ _ (preserves-≗ Variant→2CC l config) (preserves-≗ Variant→2CC r config) ⟩ (if config f then ADT.⟦ l ⟧ config else ADT.⟦ r ⟧ config) ≡⟨⟩ ADT.⟦ f ⟨ l , r ⟩ ⟧ config diff --git a/src/Vatras/Translation/Lang/ADT-to-NADT.agda b/src/Vatras/Translation/Lang/ADT-to-NADT.agda index 7e5d1fbb..31559c37 100644 --- a/src/Vatras/Translation/Lang/ADT-to-NADT.agda +++ b/src/Vatras/Translation/Lang/ADT-to-NADT.agda @@ -54,7 +54,7 @@ preserves-⊆ (f ⟨ l , r ⟩) config = NADT.⟦ if fnoc config f then translate l else translate r ⟧ config ≡⟨ Bool.if-float (λ e → NADT.⟦ e ⟧ config) (fnoc config f) ⟩ (if fnoc config f then NADT.⟦ translate l ⟧ config else NADT.⟦ translate r ⟧ config) - ≡⟨ Eq.cong₂ (if fnoc config f then_else_) (preserves-⊆ l config) (preserves-⊆ r config) ⟩ + ≡⟨ Bool.if-cong₂ _ (preserves-⊆ l config) (preserves-⊆ r config) ⟩ (if fnoc config f then ADT.⟦ l ⟧ (fnoc config) else ADT.⟦ r ⟧ (fnoc config)) ≡⟨⟩ ADT.⟦ f ⟨ l , r ⟩ ⟧ (fnoc config) @@ -71,7 +71,7 @@ preserves-⊇ (f ⟨ l , r ⟩) config = ADT.⟦ f ⟨ l , r ⟩ ⟧ config ≡⟨⟩ (if config f then ADT.⟦ l ⟧ config else ADT.⟦ r ⟧ config) - ≡⟨ Eq.cong₂ (if config f then_else_) (preserves-⊇ l config) (preserves-⊇ r config) ⟩ + ≡⟨ Bool.if-cong₂ _ (preserves-⊇ l config) (preserves-⊇ r config) ⟩ (if config f then NADT.⟦ translate l ⟧ (conf config) else NADT.⟦ translate r ⟧ (conf config)) ≡⟨ Bool.if-float (λ e → NADT.⟦ e ⟧ (conf config)) (config f) ⟨ NADT.⟦ if config f then translate l else translate r ⟧ (conf config) diff --git a/src/Vatras/Translation/Lang/ADT/Rename.agda b/src/Vatras/Translation/Lang/ADT/Rename.agda index 04dbd854..829923b8 100644 --- a/src/Vatras/Translation/Lang/ADT/Rename.agda +++ b/src/Vatras/Translation/Lang/ADT/Rename.agda @@ -56,7 +56,7 @@ preserves-⊆ f (d ⟨ l , r ⟩) config = ADT.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ config ≡⟨⟩ (if config (f d) then ADT.⟦ rename f l ⟧ config else ADT.⟦ rename f r ⟧ config) - ≡⟨ Eq.cong₂ (if config (f d) then_else_) (preserves-⊆ f l config) (preserves-⊆ f r config) ⟩ + ≡⟨ Bool.if-cong₂ _ (preserves-⊆ f l config) (preserves-⊆ f r config) ⟩ (if config (f d) then ADT.⟦ l ⟧ (config ∘ f) else ADT.⟦ r ⟧ (config ∘ f)) ≡⟨⟩ ADT.⟦ d ⟨ l , r ⟩ ⟧ (config ∘ f) @@ -73,9 +73,9 @@ preserves-⊇ f f⁻¹ is-inverse (d ⟨ l , r ⟩) config = ADT.⟦ d ⟨ l , r ⟩ ⟧ config ≡⟨⟩ (if config d then ADT.⟦ l ⟧ config else ADT.⟦ r ⟧ config) - ≡⟨ Eq.cong₂ (if config d then_else_) (preserves-⊇ f f⁻¹ is-inverse l config) (preserves-⊇ f f⁻¹ is-inverse r config) ⟩ + ≡⟨ Bool.if-cong₂ _ (preserves-⊇ f f⁻¹ is-inverse l config) (preserves-⊇ f f⁻¹ is-inverse r config) ⟩ (if config d then ADT.⟦ rename f l ⟧ (config ∘ f⁻¹) else ADT.⟦ rename f r ⟧ (config ∘ f⁻¹)) - ≡⟨ Eq.cong-app (Eq.cong-app (Eq.cong if_then_else_ (Eq.cong config (is-inverse d))) (ADT.⟦ rename f l ⟧ (config ∘ f⁻¹))) (ADT.⟦ rename f r ⟧ (config ∘ f⁻¹)) ⟨ + ≡⟨ Bool.if-cong (Eq.cong config (is-inverse d)) ⟨ (if config (f⁻¹ (f d)) then ADT.⟦ rename f l ⟧ (config ∘ f⁻¹) else ADT.⟦ rename f r ⟧ (config ∘ f⁻¹)) ≡⟨⟩ ADT.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ (config ∘ f⁻¹) diff --git a/src/Vatras/Translation/Lang/ADT/WalkSemantics.agda b/src/Vatras/Translation/Lang/ADT/WalkSemantics.agda index 6a0d77a3..8c953449 100644 --- a/src/Vatras/Translation/Lang/ADT/WalkSemantics.agda +++ b/src/Vatras/Translation/Lang/ADT/WalkSemantics.agda @@ -14,6 +14,7 @@ module Vatras.Translation.Lang.ADT.WalkSemantics where open import Data.Bool using (Bool; true; false; not; if_then_else_) +open import Data.Bool.Properties using (if-cong) open import Data.Empty using (⊥-elim) open import Data.List using (List; []; _∷_) open import Data.List.Relation.Unary.Any using (Any; here; there) @@ -169,7 +170,7 @@ path-to-fun-step-l-inner D l r lp (D' ⟨ a , b ⟩) ((.D' ↣ .true) ∷ ep) tl ⟦ D' ⟨ a , b ⟩ ⟧ c-big ≡⟨⟩ (if c-big D' then ⟦ a ⟧ c-big else ⟦ b ⟧ c-big) - ≡⟨ Eq.cong (if_then ⟦ a ⟧ c-big else ⟦ b ⟧ c-big) (path-to-fun-step-l-inner2 D l r lp tlp x D' (endswith-Any sub (here (fromWitness refl)))) ⟩ + ≡⟨ if-cong (path-to-fun-step-l-inner2 D l r lp tlp x D' (endswith-Any sub (here (fromWitness refl)))) ⟩ (if c-sml D' then ⟦ a ⟧ c-big else ⟦ b ⟧ c-big) ≡⟨ lem ⟩ (if c-sml D' then ⟦ a ⟧ c-sml else ⟦ b ⟧ c-sml) diff --git a/src/Vatras/Translation/Lang/NCC-to-2CC.agda b/src/Vatras/Translation/Lang/NCC-to-2CC.agda index 579bf9ed..d9cbe8fb 100644 --- a/src/Vatras/Translation/Lang/NCC-to-2CC.agda +++ b/src/Vatras/Translation/Lang/NCC-to-2CC.agda @@ -7,6 +7,7 @@ module Vatras.Translation.Lang.NCC-to-2CC where open import Size using (Size; ∞) open import Data.Bool using (true; false; if_then_else_) +import Data.Bool.Properties as Bool import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Fin as Fin using (Fin; zero; suc) open import Data.List as List using (List) @@ -70,7 +71,7 @@ module 2Ary where 2CC.⟦ d ⟨ translate l , translate r ⟩ ⟧ config ≡⟨⟩ (if config d then 2CC.⟦ translate l ⟧ config else 2CC.⟦ translate r ⟧ config) - ≡⟨ Eq.cong₂ (if_then_else_ (config d)) (preserves-⊆ l config) (preserves-⊆ r config) ⟩ + ≡⟨ Bool.if-cong₂ _ (preserves-⊆ l config) (preserves-⊆ r config) ⟩ (if config d then NCC.⟦ l ⟧ (fnoc config) else NCC.⟦ r ⟧ (fnoc config)) ≡⟨ lemma ⟩ Vec.lookup (NCC.⟦ l ⟧ (fnoc config) ∷ NCC.⟦ r ⟧ (fnoc config) ∷ []) (fnoc config d) @@ -109,7 +110,7 @@ module 2Ary where Vec.lookup (NCC.⟦ l ⟧ config ∷ NCC.⟦ r ⟧ config ∷ []) (config d) ≡⟨ lemma ⟩ (if conf config d then NCC.⟦ l ⟧ config else NCC.⟦ r ⟧ config) - ≡⟨ Eq.cong₂ (if_then_else_ (conf config d)) (preserves-⊇ l config) (preserves-⊇ r config) ⟩ + ≡⟨ Bool.if-cong₂ _ (preserves-⊇ l config) (preserves-⊇ r config) ⟩ (if conf config d then 2CC.⟦ translate l ⟧ (conf config) else 2CC.⟦ translate r ⟧ (conf config)) ≡⟨⟩ 2CC.⟦ translate (d ⟨ l ∷ r ∷ [] ⟩) ⟧ (conf config) From f3b3032d6c54b1dfdc4c9e11ac3394a940847c9d Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 14 Oct 2025 15:29:11 +0200 Subject: [PATCH 12/18] reuse lemmas for non-empty lists merged into STL --- src/Vatras/Translation/Lang/ADT-to-VariantList.agda | 7 ++++--- .../Translation/Lang/VariantList-to-CCC.lagda.md | 4 ++-- src/Vatras/Util/List.agda | 13 ------------- 3 files changed, 6 insertions(+), 18 deletions(-) diff --git a/src/Vatras/Translation/Lang/ADT-to-VariantList.agda b/src/Vatras/Translation/Lang/ADT-to-VariantList.agda index 2ef24b1c..e79d59c3 100644 --- a/src/Vatras/Translation/Lang/ADT-to-VariantList.agda +++ b/src/Vatras/Translation/Lang/ADT-to-VariantList.agda @@ -17,6 +17,7 @@ open import Function using (_∘_) open import Data.List using (List; []; _∷_) open import Data.List.NonEmpty using (List⁺; _∷_; _⁺++⁺_; length) +open import Data.List.NonEmpty.Properties using (length-⁺++⁺; length-⁺++⁺-≤ˡ) open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _<_; _≤?_; z≤n; s≤s) open import Data.Nat.Properties using (≤-trans; ≰⇒>; m≤m+n; +-monoʳ-<) open import Data.Product using (_,_) @@ -42,7 +43,7 @@ open import Vatras.Lang.ADT.Path F V _==_ open import Vatras.Translation.Lang.ADT.DeadElim F V _==_ as DeadElim using (node; kill-dead; ⟦_⟧ᵤ; UndeadADT; UndeadADTL) open import Vatras.Translation.Lang.ADT.WalkSemantics F V _==_ as Walk using () -open import Vatras.Util.List using (find-or-last; ⁺++⁺-length; ⁺++⁺-length-≤; find-or-last-append; find-or-last-prepend-+; find-or-last-prepend-∸) +open import Vatras.Util.List using (find-or-last; find-or-last-append; find-or-last-prepend-+; find-or-last-prepend-∸) {- This translates a ADT to a VariantList. @@ -81,7 +82,7 @@ conf-bounded : ∀ {A} → (c : PathConfig e) → conf e c < length (tr e) conf-bounded (leaf v) (.[] is-valid tleaf) = s≤s z≤n -conf-bounded (D ⟨ l , r ⟩) ((.D ↣ true ∷ p) is-valid walk-left t) = ≤-trans (conf-bounded l (p is-valid t)) (⁺++⁺-length-≤ (tr l) (tr r)) +conf-bounded (D ⟨ l , r ⟩) ((.D ↣ true ∷ p) is-valid walk-left t) = ≤-trans (conf-bounded l (p is-valid t)) (length-⁺++⁺-≤ˡ (tr l) (tr r)) conf-bounded (D ⟨ l , r ⟩) ((.D ↣ false ∷ p) is-valid walk-right t) = go where c = p is-valid t @@ -96,7 +97,7 @@ conf-bounded (D ⟨ l , r ⟩) ((.D ↣ false ∷ p) is-valid walk-right t) = go -- use the sum rule for ⁺++⁺ on the right hand side go : length (tr l) + conf r c < length (tr l ⁺++⁺ tr r) - go rewrite ⁺++⁺-length (tr l) (tr r) = gox + go rewrite length-⁺++⁺ (tr l) (tr r) = gox preservation-walk-to-list-conf : ∀ {A : 𝔸} → (e : ADT A) diff --git a/src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md b/src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md index 8a5b3a98..6e99541c 100644 --- a/src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md +++ b/src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md @@ -18,7 +18,7 @@ module Vatras.Translation.Lang.VariantList-to-CCC open import Data.Nat using (ℕ; zero; suc) open import Data.List using ([]; _∷_; map) open import Data.List.NonEmpty using (List⁺; _∷_) renaming (map to map⁺) -open import Data.List.NonEmpty.Properties using () renaming (map-∘ to map⁺-∘; map-cong to map⁺-cong) +open import Data.List.NonEmpty.Properties using () renaming (map-id to map⁺-id; map-∘ to map⁺-∘; map-cong to map⁺-cong) open import Data.Product using (_,_; proj₁) open import Function using (id; flip; _∘_; _$_) @@ -34,7 +34,7 @@ open import Vatras.Lang.All.Fixed Dimension (Rose ∞) open VariantList using (VariantList; VariantListL) open CCC using (CCC; CCCL; _⟨_⟩) -open import Vatras.Util.List using (find-or-last; map-find-or-last; map⁺-id) +open import Vatras.Util.List using (find-or-last; map-find-or-last) ``` ## Translation diff --git a/src/Vatras/Util/List.agda b/src/Vatras/Util/List.agda index bcc5981e..2525ce92 100644 --- a/src/Vatras/Util/List.agda +++ b/src/Vatras/Util/List.agda @@ -8,7 +8,6 @@ open import Data.Fin using (Fin) open import Data.Nat using (ℕ; suc; zero; NonZero; _+_; _∸_; _⊔_; _≤_; _<_; s≤s; z≤n) open import Data.Nat.Properties using (m≤m+n) open import Data.List as List using (List; []; _∷_; lookup; foldr; _++_) -open import Data.List.Properties using (map-id; length-++) open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; toList; _⁺++⁺_) renaming (map to map⁺) open import Data.Vec as Vec using (Vec; []; _∷_) open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) @@ -25,14 +24,6 @@ empty? (_ ∷ _) = false max : List ℕ → ℕ max = foldr _⊔_ zero --- TODO: Contribute to stl -⁺++⁺-length : ∀ {ℓ} {A : Set ℓ} (xs ys : List⁺ A) - → List⁺.length (xs ⁺++⁺ ys) ≡ List⁺.length xs + List⁺.length ys -⁺++⁺-length (x ∷ xs) (y ∷ ys) = length-++ (x ∷ xs) - -⁺++⁺-length-≤ : ∀ {ℓ} {A : Set ℓ} (xs ys : List⁺ A) → List⁺.length xs ≤ List⁺.length (xs ⁺++⁺ ys) -⁺++⁺-length-≤ xs ys rewrite ⁺++⁺-length xs ys = m≤m+n (List⁺.length xs) (List⁺.length ys) - ++-tail : ∀ {ℓ} {A : Set ℓ} (y : A) (ys xs : List A) → (xs ++ y ∷ []) ++ ys ≡ xs ++ y ∷ ys ++-tail y ys [] = refl @@ -128,7 +119,3 @@ find-or-last-prepend-∸ {n = suc n} (x ∷ z ∷ zs) ys (s≤s smol) = ≡⟨⟩ find-or-last (suc n ∸ List⁺.length (x ∷ z ∷ zs)) ys ∎ - --- Todo: Contribute this to Agda stdlib -map⁺-id : ∀ {ℓ} {A : Set ℓ} → map⁺ id ≗ id {A = List⁺ A} -map⁺-id (head ∷ tail) = Eq.cong (head ∷_) (map-id tail) From 555e97437e872aa6ce95fafe327b45881c16e1c5 Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 14 Oct 2025 15:29:31 +0200 Subject: [PATCH 13/18] clean imports in List.agda --- src/Vatras/Util/List.agda | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Vatras/Util/List.agda b/src/Vatras/Util/List.agda index 2525ce92..f1109d8c 100644 --- a/src/Vatras/Util/List.agda +++ b/src/Vatras/Util/List.agda @@ -4,14 +4,12 @@ Utilities for lists. module Vatras.Util.List where open import Data.Bool using (Bool; true; false) -open import Data.Fin using (Fin) -open import Data.Nat using (ℕ; suc; zero; NonZero; _+_; _∸_; _⊔_; _≤_; _<_; s≤s; z≤n) -open import Data.Nat.Properties using (m≤m+n) +open import Data.Nat using (ℕ; suc; zero; _+_; _∸_; _⊔_; _≤_; _<_; s≤s; z≤n) open import Data.List as List using (List; []; _∷_; lookup; foldr; _++_) -open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; toList; _⁺++⁺_) renaming (map to map⁺) +open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; _⁺++⁺_) renaming (map to map⁺) open import Data.Vec as Vec using (Vec; []; _∷_) open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) -open import Function using (id; _∘_; flip) +open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; refl) open Eq.≡-Reasoning From 0af277b3fc118c2d61616c6688f164b4378d936b Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 21 Oct 2025 11:44:31 +0200 Subject: [PATCH 14/18] fixup: update README to removal of stl submodule --- README.md | 36 +++++------------------------------- 1 file changed, 5 insertions(+), 31 deletions(-) diff --git a/README.md b/README.md index c241a715..b4c817eb 100644 --- a/README.md +++ b/README.md @@ -153,8 +153,8 @@ In general, we **recommend Nix** because it creates a sandbox environment with a - For **Mac** users, we recommend Nix or Docker. (We experienced problems with installing Agda manually.) - For **Linux** users, any alternative is fine but we recommend Nix for the reasons mentioned above. -There are no other software requirements apart from having either Nix, Docker, or Agda installed, depending on which alternative you choose.. -The only dependency of our library is the Agda standard library which is shipped as a git submodule within the `agda-stdlib` directory and is taken care of automatically by our [makefile](makefile). +There are no other software requirements apart from having either Nix, Docker, or Agda installed, depending on which alternative you choose. +The only dependency of our library is the Agda standard library which is automatically taken care of by our Nix and Docker setups. Note that building for the first time (or running `nix-shell`) will take a while because Agda has to build the required dependencies from the standard library (expect ~5-10min and a lot of terminal output). @@ -253,24 +253,8 @@ make which will compile the library and run its small demo. The expected output is explained in detail in the Step-by-Step guide below. -## Step-by-Step Guide -The "Kick-The-Tires" section above basically explains all necessary steps to get the library up and running. -Here, we give additional instructions on the expected output and how to play with other demo inputs. -For using the library once you finished the setup, please have a look at the later _Reusability Guide_, which, among other -information, includes an overview of the library, notes on our mechanized proofs, and tutorials for getting to know the library. - -### How does the demo know which standard library to use? - -Agda looks for its dependencies in a directory specified by the environment variable `AGDA_DIR`. The provided [makefile](makefile) sets this environment variable temporarily and locally during the build process to the `.libs` directory within this repository. (Your global setup will not be affected). If you want to run `agda` manually, or if you want to work on this project in an editor (e.g., emacs) then you have to set this environment variable to the libs directory in this repository. - -```shell -export AGDA_DIR="path/to/this/repository/libs" -``` - -Beware that setting the variable will overwrite any previously set directory. In that case you might want to overwrite the variable only temporarily while working on this project. - -### Expected Output +#### Expected Output The demo will print a long terminal output of about 1250 lines. A copy of the expected output can be found in the [expected-output.txt](expected-output.txt). @@ -593,23 +577,13 @@ during a Docker build, you might have encountered an out of memory issue. Try to rerun the same command after closing other applications which might comsume a lot of RAM. In some cases it may also be necessary to disable some kind of out-of-memory killer (also known as OOM killer or OOM deamon) but use this option with caution. -### Failed to read library file ./libs/../agda-stdlib/standard-library.agda-lib. -The following error may occur when executing `make` after a manual setup: -``` -Failed to read library file ./libs/../agda-stdlib/standard-library.agda-lib. -Reason: ./libs/../agda-stdlib/standard-library.agda-lib: openBinaryFile: does not exist (No such file or directory) -make: *** [makefile:15: build] Error 42 -``` -This error indicates that the `agda-stdlib` git submodule has not been set up correctly. -Executing `git submodule update --init` in the root of the repository should fix the problem. - ## Where does the library name 'Vatras' come from? The name Vatras is (of course) an acronym, which stands for _VAriability language TRAnslationS_. Besides, Vatras is a water mage in the classic german RPG [Gothic II](https://almanach.worldofgothic.de/index.php/Vatras), who stems from the city of Varant, which almost sounds like _Variant_. Vatras is praying to the god Adanos, who brings some kind of equality or balance loosely speaking. -[agda-badge-version-svg]: https://img.shields.io/badge/agda-v2.6.4.3-blue.svg -[agda-badge-version-url]: https://github.com/agda/agda/releases/tag/v2.6.4.3 +[agda-badge-version-svg]: https://img.shields.io/badge/agda-v2.8.0-blue.svg +[agda-badge-version-url]: https://github.com/agda/agda/releases/tag/v2.8.0 [ghcup]: https://www.haskell.org/ghcup/ [plfa]: https://plfa.github.io/GettingStarted/ From 81cf52a86b2f5b1e91124d85866fe405ced99478 Mon Sep 17 00:00:00 2001 From: pmbittner Date: Tue, 21 Oct 2025 11:50:50 +0200 Subject: [PATCH 15/18] README: typo fix --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index b4c817eb..3a11fa54 100644 --- a/README.md +++ b/README.md @@ -31,7 +31,7 @@ When run in a terminal, our demo will show a translation roundtrip, showcasing t Vatras is a library to study and compare meta-languages for specifying variability in source code and data. Some software systems are configurable _before_ they are compiled, i.e., statically. -A common way example for implementing static variability is by conditional compilation, as for example possible with the C preprocessor. +A common way to implement static variability is by conditional compilation, as for example possible with the C preprocessor. For instance, the following [code snippet from the Linux kernel](https://github.com/torvalds/linux/blob/e271ed52b344ac02d4581286961d0c40acc54c03/include/linux/console.h#L479-L486) ```C From 93f730ab7cdf3c55a6cd76b8e6a144c2377f2ed3 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Fri, 24 Oct 2025 23:50:53 +0200 Subject: [PATCH 16/18] docs: update the setup instructions --- README.md | 61 ++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 38 insertions(+), 23 deletions(-) diff --git a/README.md b/README.md index 3a11fa54..2c505b5e 100644 --- a/README.md +++ b/README.md @@ -140,9 +140,9 @@ We tested our setup on Manjaro, NixOS, Windows Subsystem for Linux (WSL2), and w > In case of problems, there is a "Troubleshooting" section at the bottom of this file. ### Setup -Clone the library and its submodules to a directory of your choice: +Clone the library to a directory of your choice: ```shell -git clone --recursive https://github.com/VariantSync/Vatras.git +git clone https://github.com/VariantSync/Vatras.git ``` There are **three alternative ways** to compile the library and run its small demo. @@ -160,7 +160,7 @@ Note that building for the first time (or running `nix-shell`) will take a while #### Alternative 1: Setup via Nix -The installation of Nix depends on your operating system. Head to the [NixOS website](https://nixos.org/download/) and follow the installation instructions for your system. Follow the download instructions for `Nix: the package manager`, not `NixOS: the Linux distribution`! Note that Nix is not directly available for Windows but it can be used from within Windows Subsystem for Linux (WSL2). When you open a WSL2 terminal terminal, you can install Nix by following the instructions for installing Nix on linux from the [NixOS website](https://nixos.org/download/). +The installation of Nix depends on your operating system. Head to the [NixOS website](https://nixos.org/download/) and follow the installation instructions for your system. Follow the download instructions for `Nix: the package manager`, not `NixOS: the Linux distribution`! Note that Nix is not directly available for Windows but it can be used from within Windows Subsystem for Linux (WSL2). When you open a WSL2 terminal, you can install Nix by following the instructions for installing Nix on Linux from the [NixOS website](https://nixos.org/download/). When you have Nix installed on your system, open a terminal, navigate to this directory, and then simply open a Nix shell by typing ```shell @@ -189,7 +189,7 @@ How to install Docker depends on your operating system. **For Windows or Mac**, Once you have installed Docker, start the Docker daemon. **On Windows**, open the search bar using the 'Windows Key' and search for 'Docker' or 'Docker Desktop'. **On Linux**, the docker daemon typically runs automatically, so there is nothing to do; otherwise, start Docker's service using your service manager (e.g., with `systemd`, execute `sudo systemctl start docker`). -More detailed instructions on starting the deamon are given [here](https://docs.docker.com/config/daemon/start/) on the docker website. +More detailed instructions on starting the deamon are given [on the docker website](https://docs.docker.com/config/daemon/start/). Afterwards, open a terminal and navigate to this repository's directory (the directory containing this README.md). First, you must create the docker image: @@ -210,7 +210,7 @@ docker run -t vatras #### Alternative 3: Manual Setup -The library needs Agda version 2.6.4.3 (newer version should also work but we did not test them). +The library needs Agda version 2.8.0 (newer version should also work but we did not test them). There are different ways to install Agda. Following the [Agda book's installation instructions], we recommend using [GHCup][ghcup] to install GHC, Cabal, and Agda as follows (You may skip steps for tools you have already installed but there might be compatibility errors with some versions): @@ -222,10 +222,10 @@ Following the [Agda book's installation instructions], we recommend using [GHCup 1. Install the GHC compiler and the cabal build tool with [GHCup][ghcup]. ```shell - ghcup install ghc 9.2.4 + ghcup install ghc 9.12.2 ghcup install cabal recommended - ghcup set ghc 9.2.4 + ghcup set ghc 9.12.2 ghcup set cabal recommended ``` @@ -233,16 +233,25 @@ Following the [Agda book's installation instructions], we recommend using [GHCup ```shell cabal update - cabal install Agda-2.6.4.3 + cabal install Agda-2.8.0 ``` To test whether the installation worked or whether your existing installation of Agda has the right version you can check the following command's output: ```shell > agda --version - Agda version 2.6.4.3 + Agda version 2.8.0 ``` + +3. Install the [Agda standard library](https://github.com/agda/agda-stdlib) version 2.3. + + ```shell + wget -O agda-stdlib.tar.gz https://github.com/agda/agda-stdlib/archive/v2.3.tar.gz + tar -xzf agda-stdlib.tar.gz + mkdir -p "$(agda --print-agda-app-dir)" + realpath agda-stdlib-2.3/standard-library.agda-lib >> "$(agda --print-agda-app-dir)/libraries" + ``` -In case of confusion or trouble, we recommend to check the [official installation instructions](https://agda.readthedocs.io/en/v2.6.4.3/getting-started/installation.html), or follow the Getting-Started guide in the [Programming Language Foundations in Agda][plfa] book, or use the Nix setup, or check the troubleshooting instructions at the bottom of this file. +In case of confusion or trouble, we recommend to check the [official installation instructions](https://agda.readthedocs.io/en/v2.8.0/getting-started/installation.html), or follow the Getting-Started guide in the [Programming Language Foundations in Agda][plfa] book, or use the Nix setup, or check the troubleshooting instructions at the bottom of this file. To test whether your setup is correct, and to run the demo you may use our makefile. Make sure your terminal is in full-screen because the demo assumes to have at least 100 characters of horizontal space in the terminal for pretty-printing. @@ -342,9 +351,21 @@ Then add your new list to the `examples` list at the bottom of the file. ### Using our library in your own Agda projects +In order to use Vatras in your project, you need to state `Vatras` as a dependency in your Agda library file. +An Agda library file has the suffix `.agda-lib` and is usually contained in the root directory of your project. +Its content, including the dependency to Vatras, should include the following: +``` +name: YOUR-PROJECT-NAME +depend: Vatras +include: SOME/PATH/IN/YOUR/PROJECT +``` +For details about Agda's library management, please have a look at [Agda's packaging guide](https://agda.readthedocs.io/en/v2.8.0/tools/package-system.html). + +Afterwards, you need to follow one of the following alternatives to let Agda know where to find Vatras. + #### Alternative 1: Installation via Nix -When using Nix, you can use this repository as a library in you own project, by using `agda.withPackages`: +When using Nix, you can install this repository as an Agda library by using `agda.withPackages`: ```nix agda = nixpkgs.agda.withPackages [ nixpkgs.agdaPackages.standard-library @@ -357,19 +378,13 @@ Though, not required, we recommend to use the [nixpkgs pin](nix/sources.json) cr #### Alternative 2: Manual installation -After downloading this library, you can register it by appending the path of [Vatras.agda-lib](Vatras.agda-lib) to the file `$AGDA_DIR/libraries`, creating it if necessary. -If the environment variable `AGDA_DIR` is unset, it defaults to `~/.agda` on unix-like systems and `C:\Users\USERNAME\AppData\Roaming\agda` or similar on Windows. -After registering this library on your system, you can use it in your project by stating `Vatras` as a dependency in your Agda library file. -An Agda library file has the suffix `.agda-lib` and is usually contained in the root directory of your project. -Its content, including the dependency to Vatras, should include the following: - -``` -name: YOUR-PROJECT-NAME -depend: Vatras -include: SOME/PATH/IN/YOUR/PROJECT +After downloading this library, you can register it using the following commands: +```shell +mkdir -p "$(agda --print-agda-app-dir)" +realpath Vatras.agda-lib >> "$(agda --print-agda-app-dir)/libraries" ``` - -For details about Agda's library management, please have a look at [Agda's packaging guide](https://agda.readthedocs.io/en/v2.6.4.3/tools/package-system.html). +Make sure that you also have the Agda standard library version 2.3 installed. +See step 3 in the [manual setup](#alternative-3-manual-setup) for details on how to install ths Agda standard library. ### Notes on Mechanized Proofs From 0902db047c7d3a5864d100627ead8ae79a69c56c Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 25 Oct 2025 12:14:32 +0200 Subject: [PATCH 17/18] docs: update the expected output --- README.md | 6 +- expected-output.txt | 1028 +++++++++++++------------------------------ 2 files changed, 299 insertions(+), 735 deletions(-) diff --git a/README.md b/README.md index 2c505b5e..15fbbf19 100644 --- a/README.md +++ b/README.md @@ -171,7 +171,7 @@ To compile the library and run the demo, simply run make: ```shell make ``` -The expected output is explained in detail in the Step-by-Step guide below. +The expected output is explained in detail in the [Expected Output section](#expected-output) below. Alternatively, the demo can be compiled locally to `./result/bin`. ```shell @@ -260,12 +260,12 @@ Then run make ``` which will compile the library and run its small demo. -The expected output is explained in detail in the Step-by-Step guide below. +The expected output is explained in detail in the [Expected Output section](#expected-output) below. #### Expected Output -The demo will print a long terminal output of about 1250 lines. +The demo will print a long terminal output of very rougly 1000 lines. A copy of the expected output can be found in the [expected-output.txt](expected-output.txt). First, the demo prints unicode characters to terminal, as a test for you to see whether your terminal supports unicode. diff --git a/expected-output.txt b/expected-output.txt index ea0c7728..fb4c732f 100644 --- a/expected-output.txt +++ b/expected-output.txt @@ -1,4 +1,5 @@ -It's dangerous to go alone! Take this unicode to see whether your terminal supports it: + +It's dangerous to go alone! Take this unicode to see whether your terminal supports it: ₙ ₁ ₂ 𝕃 ℂ 𝔸 ⟦ ⟧ ⟨ ⟩ ❲❳ ... but now on to the demo. @@ -280,7 +281,7 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo │ │ ╰──────────────────────────────────────────────────────────────────────────────────────────────────╯ - ╭─────────────────────────────── Experiment: Configure FST example ────────────────────────────────╮ + ╭───────────────────────────── Experiment: Configuration FST example ──────────────────────────────╮ │ │ │ ╭───────────────────────────────────── Example: add-sub ─────────────────────────────────────╮ │ │ │ │ │ @@ -410,6 +411,19 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo │ │ │ translate │ │ │ │ ↓ │ │ │ │ │ │ + │ │ 2CC w/o idempotent choices │ │ + │ │ ╭────────╮ │ │ + │ │ │ 0.D⟨ │ │ │ + │ │ │ l, │ │ │ + │ │ │ r │ │ │ + │ │ │ ⟩ │ │ │ + │ │ ╰────────╯ │ │ + │ │ proven to have the same semantics as the previous expression │ │ + │ │ │ │ + │ │ │ │ │ + │ │ │ translate │ │ + │ │ ↓ │ │ + │ │ │ │ │ │ ADT │ │ │ │ ╭────────╮ │ │ │ │ │ 0.D⟨ │ │ │ @@ -451,54 +465,54 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo │ ╭───────────────────────────────── Example: Sandwich Recipe ─────────────────────────────────╮ │ │ │ │ │ │ │ CCC, original expression │ │ - │ │ ╭────────────────────╮ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ Salad?⟨ │ │ │ - │ │ │ salad, │ │ │ - │ │ │ ε │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ Patty?⟨ │ │ │ - │ │ │ meat, │ │ │ - │ │ │ tofu │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ Sauce?⟨ │ │ │ - │ │ │ ε, │ │ │ - │ │ │ mayo, │ │ │ - │ │ │ ketchup, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ >- │ │ │ - │ │ ╰────────────────────╯ │ │ + │ │ ╭─────────────╮ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ Salad?⟨ │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ ε │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ Patty?⟨ │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 🧆 │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ Sauce?⟨ │ │ │ + │ │ │ ε, │ │ │ + │ │ │ 🥚, │ │ │ + │ │ │ 🍅, │ │ │ + │ │ │ 🍅🥚 │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ >- │ │ │ + │ │ ╰─────────────╯ │ │ │ │ │ │ │ │ │ │ │ │ │ │ translate │ │ │ │ ↓ │ │ │ │ │ │ │ │ NCC │ │ - │ │ ╭────────────────────╮ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ Salad?⟨ │ │ │ - │ │ │ salad, │ │ │ - │ │ │ ε, │ │ │ - │ │ │ ε, │ │ │ - │ │ │ ε │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ Patty?⟨ │ │ │ - │ │ │ meat, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ tofu │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ Sauce?⟨ │ │ │ - │ │ │ ε, │ │ │ - │ │ │ mayo, │ │ │ - │ │ │ ketchup, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ >- │ │ │ - │ │ ╰────────────────────╯ │ │ + │ │ ╭─────────────╮ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ Salad?⟨ │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ ε, │ │ │ + │ │ │ ε, │ │ │ + │ │ │ ε │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ Patty?⟨ │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 🧆 │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ Sauce?⟨ │ │ │ + │ │ │ ε, │ │ │ + │ │ │ 🥚, │ │ │ + │ │ │ 🍅, │ │ │ + │ │ │ 🍅🥚 │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ >- │ │ │ + │ │ ╰─────────────╯ │ │ │ │ proven to have the same semantics as the previous expression │ │ │ │ │ │ │ │ │ │ │ @@ -506,41 +520,41 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo │ │ ↓ │ │ │ │ │ │ │ │ NCC │ │ - │ │ ╭────────────────────────╮ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ 0.Salad?⟨ │ │ │ - │ │ │ salad, │ │ │ - │ │ │ 1.Salad?⟨ │ │ │ - │ │ │ ε, │ │ │ - │ │ │ 2.Salad?⟨ │ │ │ - │ │ │ ε, │ │ │ - │ │ │ ε │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ 0.Patty?⟨ │ │ │ - │ │ │ meat, │ │ │ - │ │ │ 1.Patty?⟨ │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ 2.Patty?⟨ │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ tofu │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ ε, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ mayo, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ ketchup, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ >- │ │ │ - │ │ ╰────────────────────────╯ │ │ + │ │ ╭───────────────────╮ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 0.Salad?⟨ │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ 1.Salad?⟨ │ │ │ + │ │ │ ε, │ │ │ + │ │ │ 2.Salad?⟨ │ │ │ + │ │ │ ε, │ │ │ + │ │ │ ε │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 0.Patty?⟨ │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 1.Patty?⟨ │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 2.Patty?⟨ │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 🧆 │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 0.Sauce?⟨ │ │ │ + │ │ │ ε, │ │ │ + │ │ │ 1.Sauce?⟨ │ │ │ + │ │ │ 🥚, │ │ │ + │ │ │ 2.Sauce?⟨ │ │ │ + │ │ │ 🍅, │ │ │ + │ │ │ 🍅🥚 │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ >- │ │ │ + │ │ ╰───────────────────╯ │ │ │ │ proven to have the same semantics as the previous expression │ │ │ │ │ │ │ │ │ │ │ @@ -548,41 +562,71 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo │ │ ↓ │ │ │ │ │ │ │ │ 2CC │ │ - │ │ ╭────────────────────────╮ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ 0.Salad?⟨ │ │ │ - │ │ │ salad, │ │ │ - │ │ │ 1.Salad?⟨ │ │ │ - │ │ │ ε, │ │ │ - │ │ │ 2.Salad?⟨ │ │ │ - │ │ │ ε, │ │ │ - │ │ │ ε │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ 0.Patty?⟨ │ │ │ - │ │ │ meat, │ │ │ - │ │ │ 1.Patty?⟨ │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ 2.Patty?⟨ │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ tofu │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ ε, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ mayo, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ ketchup, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ >- │ │ │ - │ │ ╰────────────────────────╯ │ │ + │ │ ╭───────────────────╮ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 0.Salad?⟨ │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ 1.Salad?⟨ │ │ │ + │ │ │ ε, │ │ │ + │ │ │ 2.Salad?⟨ │ │ │ + │ │ │ ε, │ │ │ + │ │ │ ε │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 0.Patty?⟨ │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 1.Patty?⟨ │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 2.Patty?⟨ │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 🧆 │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 0.Sauce?⟨ │ │ │ + │ │ │ ε, │ │ │ + │ │ │ 1.Sauce?⟨ │ │ │ + │ │ │ 🥚, │ │ │ + │ │ │ 2.Sauce?⟨ │ │ │ + │ │ │ 🍅, │ │ │ + │ │ │ 🍅🥚 │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ >- │ │ │ + │ │ ╰───────────────────╯ │ │ + │ │ proven to have the same semantics as the previous expression │ │ + │ │ │ │ + │ │ │ │ │ + │ │ │ translate │ │ + │ │ ↓ │ │ + │ │ │ │ + │ │ 2CC w/o idempotent choices │ │ + │ │ ╭───────────────────╮ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 0.Salad?⟨ │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ ε │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 0.Patty?⟨ │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 🧆 │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 0.Sauce?⟨ │ │ │ + │ │ │ ε, │ │ │ + │ │ │ 1.Sauce?⟨ │ │ │ + │ │ │ 🥚, │ │ │ + │ │ │ 2.Sauce?⟨ │ │ │ + │ │ │ 🍅, │ │ │ + │ │ │ 🍅🥚 │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ >- │ │ │ + │ │ ╰───────────────────╯ │ │ │ │ proven to have the same semantics as the previous expression │ │ │ │ │ │ │ │ │ │ │ @@ -590,198 +634,54 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo │ │ ↓ │ │ │ │ │ │ │ │ ADT │ │ - │ │ ╭────────────────────────────────────────────────────────────╮ │ │ - │ │ │ 0.Salad?⟨ │ │ │ - │ │ │ 0.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ Bread-- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 1.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ Bread-- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 2.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ Bread-- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread--, │ │ │ - │ │ │ Bread-- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 1.Salad?⟨ │ │ │ - │ │ │ 0.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, meat, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, meat, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, meat, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, meat, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 1.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 2.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 2.Salad?⟨ │ │ │ - │ │ │ 0.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, meat, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, meat, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, meat, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, meat, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 1.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 2.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 0.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, meat, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, meat, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, meat, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, meat, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 1.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 2.Patty?⟨ │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩, │ │ │ - │ │ │ 0.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ε>-, │ │ │ - │ │ │ 1.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo>-, │ │ │ - │ │ │ 2.Sauce?⟨ │ │ │ - │ │ │ Bread-<ε, cheese, tofu, ketchup>-, │ │ │ - │ │ │ Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ │ ⟩ │ │ │ - │ │ ╰────────────────────────────────────────────────────────────╯ │ │ + │ │ ╭────────────────────────────────────╮ │ │ + │ │ │ 0.Salad?⟨ │ │ │ + │ │ │ 0.Patty?⟨ │ │ │ + │ │ │ 0.Sauce?⟨ │ │ │ + │ │ │ 🍞-<🥗, 🧀, 🍖, ε>-, │ │ │ + │ │ │ 1.Sauce?⟨ │ │ │ + │ │ │ 🍞-<🥗, 🧀, 🍖, 🥚>-, │ │ │ + │ │ │ 2.Sauce?⟨ │ │ │ + │ │ │ 🍞-<🥗, 🧀, 🍖, 🍅>-, │ │ │ + │ │ │ 🍞-<🥗, 🧀, 🍖, 🍅🥚>- │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 0.Sauce?⟨ │ │ │ + │ │ │ 🍞-<🥗, 🧀, 🧆, ε>-, │ │ │ + │ │ │ 1.Sauce?⟨ │ │ │ + │ │ │ 🍞-<🥗, 🧀, 🧆, 🥚>-, │ │ │ + │ │ │ 2.Sauce?⟨ │ │ │ + │ │ │ 🍞-<🥗, 🧀, 🧆, 🍅>-, │ │ │ + │ │ │ 🍞-<🥗, 🧀, 🧆, 🍅🥚>- │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 0.Patty?⟨ │ │ │ + │ │ │ 0.Sauce?⟨ │ │ │ + │ │ │ 🍞-<ε, 🧀, 🍖, ε>-, │ │ │ + │ │ │ 1.Sauce?⟨ │ │ │ + │ │ │ 🍞-<ε, 🧀, 🍖, 🥚>-, │ │ │ + │ │ │ 2.Sauce?⟨ │ │ │ + │ │ │ 🍞-<ε, 🧀, 🍖, 🍅>-, │ │ │ + │ │ │ 🍞-<ε, 🧀, 🍖, 🍅🥚>- │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩, │ │ │ + │ │ │ 0.Sauce?⟨ │ │ │ + │ │ │ 🍞-<ε, 🧀, 🧆, ε>-, │ │ │ + │ │ │ 1.Sauce?⟨ │ │ │ + │ │ │ 🍞-<ε, 🧀, 🧆, 🥚>-, │ │ │ + │ │ │ 2.Sauce?⟨ │ │ │ + │ │ │ 🍞-<ε, 🧀, 🧆, 🍅>-, │ │ │ + │ │ │ 🍞-<ε, 🧀, 🧆, 🍅🥚>- │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ │ ⟩ │ │ │ + │ │ ╰────────────────────────────────────╯ │ │ │ │ proven to have the same semantics as the previous expression │ │ │ │ │ │ │ │ │ │ │ @@ -789,73 +689,25 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo │ │ ↓ │ │ │ │ │ │ │ │ VariantList │ │ - │ │ ╭────────────────────────────────────────────────╮ │ │ - │ │ │ [ Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, meat, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ε>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, ketchup>- │ │ │ - │ │ │ , Bread-<ε, cheese, tofu, mayo+ketchup>- │ │ │ - │ │ │ ] │ │ │ - │ │ ╰────────────────────────────────────────────────╯ │ │ + │ │ ╭────────────────────────────╮ │ │ + │ │ │ [ 🍞-<🥗, 🧀, 🍖, ε>- │ │ │ + │ │ │ , 🍞-<🥗, 🧀, 🍖, 🥚>- │ │ │ + │ │ │ , 🍞-<🥗, 🧀, 🍖, 🍅>- │ │ │ + │ │ │ , 🍞-<🥗, 🧀, 🍖, 🍅🥚>- │ │ │ + │ │ │ , 🍞-<🥗, 🧀, 🧆, ε>- │ │ │ + │ │ │ , 🍞-<🥗, 🧀, 🧆, 🥚>- │ │ │ + │ │ │ , 🍞-<🥗, 🧀, 🧆, 🍅>- │ │ │ + │ │ │ , 🍞-<🥗, 🧀, 🧆, 🍅🥚>- │ │ │ + │ │ │ , 🍞-<ε, 🧀, 🍖, ε>- │ │ │ + │ │ │ , 🍞-<ε, 🧀, 🍖, 🥚>- │ │ │ + │ │ │ , 🍞-<ε, 🧀, 🍖, 🍅>- │ │ │ + │ │ │ , 🍞-<ε, 🧀, 🍖, 🍅🥚>- │ │ │ + │ │ │ , 🍞-<ε, 🧀, 🧆, ε>- │ │ │ + │ │ │ , 🍞-<ε, 🧀, 🧆, 🥚>- │ │ │ + │ │ │ , 🍞-<ε, 🧀, 🧆, 🍅>- │ │ │ + │ │ │ , 🍞-<ε, 🧀, 🧆, 🍅🥚>- │ │ │ + │ │ │ ] │ │ │ + │ │ ╰────────────────────────────╯ │ │ │ │ proven to have the same semantics as the previous expression │ │ │ │ │ │ │ │ │ │ │ @@ -865,389 +717,101 @@ It's dangerous to go alone! Take this unicode to see whether your terminal suppo │ │ CCC │ │ │ │ ╭────────────────────╮ │ │ │ │ │ default feature⟨ │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ salad, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🍖, │ │ │ │ │ │ ε │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 🥚 │ │ │ + │ │ │ >-, │ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 🍅 │ │ │ + │ │ │ >-, │ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 🍅🥚 │ │ │ + │ │ │ >-, │ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🧆, │ │ │ │ │ │ ε │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ mayo+ketchup │ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 🥚 │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 🍅 │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ meat, │ │ │ - │ │ │ mayo+ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ε │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ - │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ - │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ + │ │ │ 🍞-< │ │ │ + │ │ │ 🥗, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 🍅🥚 │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ + │ │ │ 🍞-< │ │ │ │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🍖, │ │ │ │ │ │ ε │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ + │ │ │ 🍞-< │ │ │ │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 🥚 │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ + │ │ │ 🍞-< │ │ │ │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 🍅 │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ + │ │ │ 🍞-< │ │ │ │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🍖, │ │ │ + │ │ │ 🍅🥚 │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ + │ │ │ 🍞-< │ │ │ │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🧆, │ │ │ │ │ │ ε │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ + │ │ │ 🍞-< │ │ │ │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 🥚 │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ + │ │ │ 🍞-< │ │ │ │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ ketchup │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 🍅 │ │ │ │ │ │ >-, │ │ │ - │ │ │ Bread-< │ │ │ + │ │ │ 🍞-< │ │ │ │ │ │ ε, │ │ │ - │ │ │ cheese, │ │ │ - │ │ │ tofu, │ │ │ - │ │ │ mayo+ketchup │ │ │ + │ │ │ 🧀, │ │ │ + │ │ │ 🧆, │ │ │ + │ │ │ 🍅🥚 │ │ │ │ │ │ >- │ │ │ │ │ │ ⟩ │ │ │ │ │ ╰────────────────────╯ │ │ From b66dcead0f79b09479c63b505cfd0bd8744cb62a Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 25 Oct 2025 12:14:47 +0200 Subject: [PATCH 18/18] docs: add an error I encountered during testing --- README.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/README.md b/README.md index 15fbbf19..b735455c 100644 --- a/README.md +++ b/README.md @@ -592,6 +592,25 @@ during a Docker build, you might have encountered an out of memory issue. Try to rerun the same command after closing other applications which might comsume a lot of RAM. In some cases it may also be necessary to disable some kind of out-of-memory killer (also known as OOM killer or OOM deamon) but use this option with caution. +### Docker fails to open Git repository + +If you see an error like +``` +error: opening Git repository '"/home/user"': failed to resolve path '/home/your-user-name/some/path/.git/worktrees/Vatras': No such file or directory +------ +Dockerfile:19 +-------------------- + 17 | + 18 | # Verify all proofs and build the demo. + 19 | >>> RUN nix-build + 20 | + 21 | # Copy the demo with all runtime dependencies (ignoring build-time dependencies) +-------------------- +ERROR: failed to solve: process "/bin/sh -c nix-build" did not complete successfully: exit code: 1 +``` +you may be in a Git worktree or your Git directory is out of place for some other reason. +Ensure that `git rev-parse --path-format=absolute --git-common-dir` (the path of the Git repository's data) is in your current working directory by creating a fresh non-bare clone without creating a second Git worktree. + ## Where does the library name 'Vatras' come from? The name Vatras is (of course) an acronym, which stands for _VAriability language TRAnslationS_.