From 30426dc5f98a03efefaa4d4d14bcf800356296d7 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Fri, 6 Oct 2023 18:42:44 +0200 Subject: [PATCH 01/13] Use the public URL of the agda-stdlib submodule This will allow cloning of this repository (once it's public) without having to authenticate to GitHub. --- .gitmodules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitmodules b/.gitmodules index ec7fde19..c015d4d2 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,3 @@ [submodule "agda-stdlib"] path = agda-stdlib - url = git@github.com:agda/agda-stdlib.git + url = https://github.com/agda/agda-stdlib.git From 8fa5f9f3c1bb787464cacdc0c766e1b2cb5c15cf Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 6 Apr 2024 14:11:52 +0200 Subject: [PATCH 02/13] nix: Fix the description of the Nix package --- default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/default.nix b/default.nix index 52683bac..a5f57a9f 100644 --- a/default.nix +++ b/default.nix @@ -36,5 +36,5 @@ pkgs.agdaPackages.mkDerivation { install -D src/Main "$out/bin/$pname" ''; - meta = {description = "On the Expressive Power of Programming Languages";}; + meta = {description = "On the Expressive Power of Languages for Static Variability";}; } From 9e73035b83432cb209c035f1eabc0117e407bb29 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 6 Apr 2024 14:09:51 +0200 Subject: [PATCH 03/13] Implement pretty printing for OC --- src/Lang/OC.lagda.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/Lang/OC.lagda.md b/src/Lang/OC.lagda.md index 1afaaea3..e7607704 100644 --- a/src/Lang/OC.lagda.md +++ b/src/Lang/OC.lagda.md @@ -233,6 +233,7 @@ Another way is to enrich the annotation language, for example using propositiona ## Show ```agda +open import Show.Lines hiding (map) open String using (_++_; intersperse) open import Function using (_∘_) @@ -244,4 +245,19 @@ module Show (Option : 𝔽) (print-opt : Option → String) where show-wfoc : ∀ {i : Size} → WFOC Option i (String , String._≟_) → String show-wfoc = show-oc ∘ forgetWF + + pretty-oc : ∀ {i : Size} → OC Option i (String , String._≟_) → Lines + pretty-oc (s -< [] >-) = > s + pretty-oc (s -< es@(_ ∷ _) >-) = do + > s ++ "-<" + indent 2 do + intersperseCommas (map pretty-oc es) + > ">-" + pretty-oc (O ❲ e ❳) = do + > print-opt O ++ "❲" + indent 2 (pretty-oc e) + > "❳" + + pretty-wfoc : ∀ {i : Size} → WFOC Option i (String , String._≟_) → Lines + pretty-wfoc = pretty-oc ∘ forgetWF ``` From 512c3ea27471aa19c9a6ac20ba4c6a6c38e7250f Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 6 Apr 2024 20:11:25 +0200 Subject: [PATCH 04/13] Rename NADTVL to NADTL for consistency All other `VariabilityLanguage`s use a single `L` prefix and it was already renamed in the reexport of `Lang.All`. --- src/Lang/All/Generic.agda | 2 +- src/Lang/NADT.agda | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lang/All/Generic.agda b/src/Lang/All/Generic.agda index 29b6097e..930d8e56 100644 --- a/src/Lang/All/Generic.agda +++ b/src/Lang/All/Generic.agda @@ -22,7 +22,7 @@ module 2CC where open Lang.2CC.Sem Variant Artifact∈ₛVariant public module NADT where - open import Lang.NADT renaming (NADTVL to NADTL) public + open import Lang.NADT public module ADT where open import Lang.ADT public diff --git a/src/Lang/NADT.agda b/src/Lang/NADT.agda index 0843695e..c16d6b72 100644 --- a/src/Lang/NADT.agda +++ b/src/Lang/NADT.agda @@ -18,9 +18,9 @@ data NADT (V : 𝕍) (F : 𝔽) : Size → 𝔼 where NADTChoice : ∀ {i A} → VLChoice.Syntax F (NADT V F i) A → NADT V F (↑ i) A mutual - NADTVL : ∀ {i : Size} (V : 𝕍) (F : 𝔽) → VariabilityLanguage V - NADTVL {i} V F = ⟪ NADT V F i , Choice.Config F , ⟦_⟧ ⟫ + NADTL : ∀ {i : Size} (V : 𝕍) (F : 𝔽) → VariabilityLanguage V + NADTL {i} V F = ⟪ NADT V F i , Choice.Config F , ⟦_⟧ ⟫ ⟦_⟧ : ∀ {i : Size} {V : 𝕍} {F : 𝔽} → 𝔼-Semantics V (Choice.Config F) (NADT V F i) ⟦_⟧ (NADTAsset (leaf v)) _ = v - ⟦_⟧ {i} {V} {F} (NADTChoice chc) = VLChoice.Semantics V F (NADTVL V F) id chc + ⟦_⟧ {i} {V} {F} (NADTChoice chc) = VLChoice.Semantics V F (NADTL V F) id chc From cca73a269d7e0494491e89915b6be1fe1116e28d Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 6 Apr 2024 20:28:45 +0200 Subject: [PATCH 05/13] Replace `if-cong` by `push-function-into-if` from agda-stdlib --- src/Construct/Choices.agda | 5 ++--- src/Lang/2CC.lagda.md | 1 - src/Util/AuxProofs.agda | 8 -------- 3 files changed, 2 insertions(+), 12 deletions(-) diff --git a/src/Construct/Choices.agda b/src/Construct/Choices.agda index a9535280..0ebf9716 100644 --- a/src/Construct/Choices.agda +++ b/src/Construct/Choices.agda @@ -2,6 +2,7 @@ module Construct.Choices where open import Data.Bool using (Bool; if_then_else_) +open import Data.Bool.Properties using (push-function-into-if) open import Data.String using (String; _<+>_; intersperse) open import Level using (Level; _⊔_) open import Function using (_∘_) @@ -11,8 +12,6 @@ open Eq.≡-Reasoning open import Data.EqIndexedSet as ISet -open import Util.AuxProofs using (if-cong) - module NChoice where open import Data.Fin using (Fin) open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥) @@ -102,7 +101,7 @@ module 2Choice where ⟦ map f (D ⟨ l , r ⟩) ⟧ c ≡⟨⟩ (if c D then f l else f r) - ≡⟨ if-cong (c D) f ⟩ + ≡˘⟨ push-function-into-if f (c D) ⟩ f (if c D then l else r) ≡⟨⟩ f (⟦ D ⟨ l , r ⟩ ⟧ c) diff --git a/src/Lang/2CC.lagda.md b/src/Lang/2CC.lagda.md index cd59afaa..e6c7f5d7 100644 --- a/src/Lang/2CC.lagda.md +++ b/src/Lang/2CC.lagda.md @@ -80,7 +80,6 @@ module _ {Dimension : 𝔽} where Some transformation rules: ```agda - open import Util.AuxProofs using (if-idemp; if-cong) open Data.List using ([_]) open import Data.Nat using (ℕ) open import Data.Vec using (Vec; toList; zipWith) diff --git a/src/Util/AuxProofs.agda b/src/Util/AuxProofs.agda index fe430a55..89b850ae 100644 --- a/src/Util/AuxProofs.agda +++ b/src/Util/AuxProofs.agda @@ -106,14 +106,6 @@ if-idemp' : ∀ {ℓ} {A : Set ℓ} → ∀ {c} → (if c then a else a) ≡ a if-idemp' _ {b} = if-idemp b -if-cong : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} {a b : A} - → (c : Bool) - → (P : A → B) - ------------------------------------------------- - → (if c then P a else P b) ≡ P (if c then a else b) -if-cong false _ = refl -if-cong true _ = refl - if-swap : ∀ {A : Set} (x y : Bool) (a b : A) → (if x then a else (if y then a else b)) ≡ (if y then a else (if x then a else b)) From 9d66bdd4630ce221139d79a2ae8b11a9dbdb4a47 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Sat, 6 Apr 2024 20:58:30 +0200 Subject: [PATCH 06/13] Remove `clampAt` and `minFinFromLimit` in favor of `cappedFin` The interface of `cappedFin` using an implicit parameter which also doesn't represent the predecessor of the maximum value is very nice to use. Most uses in the code are already using `cappedFin`. `minFinFromLimit` also implements the same functionality but is currently unused and it seems like proofs about it are harder than for `cappedFin`. --- src/Lang/VariantList.lagda.md | 4 ++-- src/Util/AuxProofs.agda | 22 ---------------------- src/Util/List.agda | 8 -------- src/Util/Nat/AtLeast.agda | 1 - 4 files changed, 2 insertions(+), 33 deletions(-) diff --git a/src/Lang/VariantList.lagda.md b/src/Lang/VariantList.lagda.md index 6ccddfd5..9a07af3d 100644 --- a/src/Lang/VariantList.lagda.md +++ b/src/Lang/VariantList.lagda.md @@ -52,7 +52,7 @@ VariantListL = ⟪ VariantList , Configuration , ⟦_⟧ ⟫ ```agda -- prove completeness via inference rules -open import Util.AuxProofs using (clampAt) +open import Util.Nat.AtLeast using (cappedFin) private open import Framework.VariantMap V @@ -115,7 +115,7 @@ vl-conf : Fin (suc n) → Configuration vl-conf i = toℕ i vl-fnoc : Configuration → Fin (suc n) -vl-fnoc {n} c = clampAt n c +vl-fnoc c = cappedFin c preserves-∈ : ∀ {V} → n ⊢ V ⟶ e diff --git a/src/Util/AuxProofs.agda b/src/Util/AuxProofs.agda index 89b850ae..5c879b25 100644 --- a/src/Util/AuxProofs.agda +++ b/src/Util/AuxProofs.agda @@ -69,28 +69,6 @@ n∸1+m Date: Sun, 7 Apr 2024 00:16:19 +0200 Subject: [PATCH 07/13] Update Agda and the standard library In some places the new option `--large-indices` is required because an inconsistency with `--forced-argument-recursion` (which is enabled by default) was discovered. --- agda-stdlib | 2 +- default.nix | 11 +--- nix/sources.json | 6 +- src/Construct/Choices.agda | 6 +- src/Construct/NestedChoice.agda | 1 + src/Data/IndexedSet.lagda.md | 65 ++++++++++--------- src/Framework/Composition/FeatureAlgebra.agda | 12 ++-- src/Framework/Properties/Finity.agda | 1 + src/Framework/Variants.agda | 5 +- src/Lang/2CC.lagda.md | 1 + src/Lang/ADT.agda | 2 + src/Lang/ADT/Path.agda | 2 + src/Lang/CCC.lagda.md | 5 +- src/Lang/Gruler.agda | 1 + src/Lang/NADT.agda | 1 + src/Lang/NCC.lagda.md | 1 + src/Lang/OC.lagda.md | 1 + src/Lang/VariantList.lagda.md | 4 ++ src/Translation/Lang/2CC-to-ADT.agda | 12 ++-- src/Translation/Lang/2CC-to-NCC.agda | 6 +- src/Translation/Lang/2CC/Rename.agda | 12 ++-- src/Translation/Lang/ADT-to-2CC.agda | 4 +- src/Translation/Lang/ADT-to-NADT.agda | 4 +- src/Translation/Lang/ADT-to-VariantList.agda | 4 +- src/Translation/Lang/ADT/Rename.agda | 4 +- src/Translation/Lang/ADT/WalkSemantics.agda | 2 +- src/Translation/Lang/CCC-to-NCC.agda | 30 ++++----- src/Translation/Lang/NADT-to-CCC.agda | 4 +- src/Translation/Lang/NCC-to-2CC.agda | 10 +-- src/Translation/Lang/NCC-to-CCC.agda | 10 +-- src/Translation/Lang/NCC/Grow.agda | 14 ++-- src/Translation/Lang/NCC/NCC-to-NCC.agda | 3 - src/Translation/Lang/NCC/Rename.agda | 8 +-- src/Translation/Lang/NCC/ShrinkTo2.agda | 54 +++++++-------- src/Translation/Lang/OC-to-2CC.lagda.md | 1 + .../Lang/VariantList-to-CCC.lagda.md | 8 +-- src/Util/String.agda | 4 +- src/Util/Suffix.agda | 2 + 38 files changed, 167 insertions(+), 156 deletions(-) diff --git a/agda-stdlib b/agda-stdlib index 177dc9e9..2b8fff10 160000 --- a/agda-stdlib +++ b/agda-stdlib @@ -1 +1 @@ -Subproject commit 177dc9e983606b653a3c6af2ae2162bbc87882ad +Subproject commit 2b8fff10f4033b91a6df4007e4a65cb10047c89c diff --git a/default.nix b/default.nix index a5f57a9f..6af76f86 100644 --- a/default.nix +++ b/default.nix @@ -14,16 +14,7 @@ pkgs.agdaPackages.mkDerivation { src = ./.; buildInputs = [ - (pkgs.agdaPackages.standard-library.overrideAttrs - (oldAttrs: { - version = "1.7.2"; - src = pkgs.fetchFromGitHub { - repo = "agda-stdlib"; - owner = "agda"; - rev = "177dc9e"; - hash = "sha256-ovnhL5otoaACpqHZnk/ucivwtEfBQtGRu4/xw4+Ws+c="; - }; - })) + pkgs.agdaPackages.standard-library ]; buildPhase = '' diff --git a/nix/sources.json b/nix/sources.json index bdc4c657..05a914cc 100644 --- a/nix/sources.json +++ b/nix/sources.json @@ -5,10 +5,10 @@ "homepage": null, "owner": "NixOS", "repo": "nixpkgs", - "rev": "4ecab3273592f27479a583fb6d975d4aba3486fe", - "sha256": "10wn0l08j9lgqcw8177nh2ljrnxdrpri7bp0g7nvrsn9rkawvlbf", + "rev": "fd281bd6b7d3e32ddfa399853946f782553163b5", + "sha256": "1hy81yj2dcg6kfsm63xcqf8kvigxglim1rcg1xpmy2rb6a8vqvsj", "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/4ecab3273592f27479a583fb6d975d4aba3486fe.tar.gz", + "url": "https://github.com/NixOS/nixpkgs/archive/fd281bd6b7d3e32ddfa399853946f782553163b5.tar.gz", "url_template": "https://github.com///archive/.tar.gz" } } diff --git a/src/Construct/Choices.agda b/src/Construct/Choices.agda index 0ebf9716..e13ffb99 100644 --- a/src/Construct/Choices.agda +++ b/src/Construct/Choices.agda @@ -2,7 +2,7 @@ module Construct.Choices where open import Data.Bool using (Bool; if_then_else_) -open import Data.Bool.Properties using (push-function-into-if) +open import Data.Bool.Properties using (if-float) open import Data.String using (String; _<+>_; intersperse) open import Level using (Level; _⊔_) open import Function using (_∘_) @@ -101,7 +101,7 @@ module 2Choice where ⟦ map f (D ⟨ l , r ⟩) ⟧ c ≡⟨⟩ (if c D then f l else f r) - ≡˘⟨ push-function-into-if f (c D) ⟩ + ≡⟨ if-float f (c D) ⟨ f (if c D then l else r) ≡⟨⟩ f (⟦ D ⟨ l , r ⟩ ⟧ c) @@ -151,7 +151,7 @@ module Choice where ⟦ map f (D ⟨ as ⟩) ⟧ c ≡⟨⟩ find-or-last (c D) (map-list⁺ f as) - ≡˘⟨ map-find-or-last f (c D) as ⟩ + ≡⟨ map-find-or-last f (c D) as ⟨ f (find-or-last (c D) as) ≡⟨⟩ f (⟦ D ⟨ as ⟩ ⟧ c) diff --git a/src/Construct/NestedChoice.agda b/src/Construct/NestedChoice.agda index 912ece3d..1e03cb6e 100644 --- a/src/Construct/NestedChoice.agda +++ b/src/Construct/NestedChoice.agda @@ -1,4 +1,5 @@ {-# OPTIONS --sized-types #-} +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} open import Framework.Definitions diff --git a/src/Data/IndexedSet.lagda.md b/src/Data/IndexedSet.lagda.md index 71a6566f..09902d55 100644 --- a/src/Data/IndexedSet.lagda.md +++ b/src/Data/IndexedSet.lagda.md @@ -289,7 +289,7 @@ module ⊆-Reasoning where module ≅-Reasoning where infix 3 _≅-∎ - infixr 2 _≅⟨⟩_ step-≅ step-≅˘ step-≐ step-≐˘ --step-≅-by-index-translation + infixr 2 _≅⟨⟩_ step-≅-⟨ step-≅-⟩ step-≐-⟨ step-≐-⟩ --step-≅-by-index-translation infix 1 ≅-begin_ ≅-begin_ : ∀{I J} {A : IndexedSet I} {B : IndexedSet J} → A ≅ B → A ≅ B @@ -298,11 +298,11 @@ module ≅-Reasoning where _≅⟨⟩_ : ∀ {I J} (A : IndexedSet I) {B : IndexedSet J} → A ≅ B → A ≅ B _ ≅⟨⟩ A≅B = A≅B - step-≅ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} + step-≅-⟩ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} → B ≅ C → A ≅ B → A ≅ C - step-≅ _ B≅C A≅B = ≅-trans A≅B B≅C + step-≅-⟩ _ B≅C A≅B = ≅-trans A≅B B≅C -- step-≅-by-index-translation : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} -- → (i→j : I → J) @@ -313,36 +313,36 @@ module ≅-Reasoning where -- → A ≅ C -- step-≅-by-index-translation _ i→j j→i ti tj B≅C = ≅-trans (⊆-by-index-translation i→j ti , ⊆-by-index-translation j→i tj) B≅C - step-≅˘ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} + step-≅-⟨ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} → B ≅ C → B ≅ A → A ≅ C - step-≅˘ A B≅C B≅A = step-≅ A B≅C (≅-sym B≅A) + step-≅-⟨ A B≅C B≅A = step-≅-⟩ A B≅C (≅-sym B≅A) - step-≐ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} + step-≐-⟩ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} → B ≅ C → A ≐ B → A ≅ C - step-≐ _ B≅C A≐B = ≅-trans (≐→≅ A≐B) B≅C + step-≐-⟩ _ B≅C A≐B = ≅-trans (≐→≅ A≐B) B≅C - step-≐˘ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} + step-≐-⟨ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} → B ≅ C → B ≐ A → A ≅ C - step-≐˘ A B≅C B≐A = step-≐ A B≅C (≐-sym B≐A) + step-≐-⟨ A B≅C B≐A = step-≐-⟩ A B≅C (≐-sym B≐A) _≅-∎ : ∀ {I} (A : IndexedSet I) → A ≅ A _≅-∎ _ = ≅-refl - syntax step-≅ A B≅C A≅B = A ≅⟨ A≅B ⟩ B≅C - syntax step-≅˘ A B≅C B≅A = A ≅˘⟨ B≅A ⟩ B≅C - syntax step-≐ A B≅C (λ i → Ai≈Bi) = A ≐[ i ]⟨ Ai≈Bi ⟩ B≅C - syntax step-≐˘ A B≅C (λ i → Bi≈Ai) = A ≐˘[ i ]⟨ Bi≈Ai ⟩ B≅C + syntax step-≅-⟩ A B≅C A≅B = A ≅⟨ A≅B ⟩ B≅C + syntax step-≅-⟨ A B≅C B≅A = A ≅⟨ B≅A ⟨ B≅C + syntax step-≐-⟩ A B≅C (λ i → Ai≈Bi) = A ≐[ i ]⟨ Ai≈Bi ⟩ B≅C + syntax step-≐-⟨ A B≅C (λ i → Bi≈Ai) = A ≐[ i ]⟨ Bi≈Ai ⟨ B≅C -- syntax step-≅-by-index-translation A i→j j→i ti tj B≅C = A ≅[ i→j ]⟨ ti ⟩[ j→i ]⟨ tj ⟩ B≅C module ≅[]-Reasoning where infix 3 _≅[]-∎ - infixr 2 _≅[]⟨⟩_ step-≅[] step-≅[]˘ step-≐[] step-≐[]˘ + infixr 2 _≅[]⟨⟩_ step-≅[]-⟨ step-≅[]-⟩ step-≐[]-⟨ step-≐[]-⟩ infix 1 ≅[]-begin_ ≅[]-begin_ : ∀{I J} {A : IndexedSet I} {B : IndexedSet J} {f : I → J} {g : J → I} @@ -355,42 +355,42 @@ module ≅[]-Reasoning where → A ≅[ f ][ g ] B _ ≅[]⟨⟩ A≅B = A≅B - step-≅[] : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} + step-≅[]-⟩ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} {f : I → J} {f⁻¹ : J → I} {g : J → K} {g⁻¹ : K → J} → B ≅[ g ][ g⁻¹ ] C → A ≅[ f ][ f⁻¹ ] B → A ≅[ g ∘ f ][ f⁻¹ ∘ g⁻¹ ] C - step-≅[] _ B≅C A≅B = ≅[]-trans A≅B B≅C + step-≅[]-⟩ _ B≅C A≅B = ≅[]-trans A≅B B≅C - step-≅[]˘ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} + step-≅[]-⟨ : ∀ {I J K} (A : IndexedSet I) {B : IndexedSet J} {C : IndexedSet K} {f : I → J} {f⁻¹ : J → I} {g : J → K} {g⁻¹ : K → J} → B ≅[ g ][ g⁻¹ ] C → B ≅[ f⁻¹ ][ f ] A → A ≅[ g ∘ f ][ f⁻¹ ∘ g⁻¹ ] C - step-≅[]˘ A B≅C B≅A = step-≅[] A B≅C (≅[]-sym B≅A) + step-≅[]-⟨ A B≅C B≅A = step-≅[]-⟩ A B≅C (≅[]-sym B≅A) - step-≐[] : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} + step-≐[]-⟩ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} {g : I → J} {ginv : J → I} → B ≅[ g ][ ginv ] C → A ≐ B → A ≅[ g ][ ginv ] C - step-≐[] _ B≅C A≐B = ≅[]-trans (≐→≅[] A≐B) B≅C + step-≐[]-⟩ _ B≅C A≐B = ≅[]-trans (≐→≅[] A≐B) B≅C - step-≐[]˘ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} + step-≐[]-⟨ : ∀ {I J} (A {B} : IndexedSet I) {C : IndexedSet J} {g : I → J} {ginv : J → I} → B ≅[ g ][ ginv ] C → B ≐ A → A ≅[ g ][ ginv ] C - step-≐[]˘ A B≅C B≐A = step-≐[] A B≅C (≐-sym B≐A) + step-≐[]-⟨ A B≅C B≐A = step-≐[]-⟩ A B≅C (≐-sym B≐A) _≅[]-∎ : ∀ {I} (A : IndexedSet I) → A ≅[ id ][ id ] A _≅[]-∎ _ = ≅[]-refl - syntax step-≅[] A B≅C A≅B = A ≅[]⟨ A≅B ⟩ B≅C - syntax step-≅[]˘ A B≅C B≅A = A ≅[]˘⟨ B≅A ⟩ B≅C - syntax step-≐[] A B≅C (λ i → Ai≈Bi) = A ≐[ i ]⟨ Ai≈Bi ⟩ B≅C - syntax step-≐[]˘ A B≅C (λ i → Bi≈Ai) = A ≐˘[ i ]⟨ Bi≈Ai ⟩ B≅C + syntax step-≅[]-⟩ A B≅C A≅B = A ≅[]⟨ A≅B ⟩ B≅C + syntax step-≅[]-⟨ A B≅C B≅A = A ≅[]⟨ B≅A ⟨ B≅C + syntax step-≐[]-⟩ A B≅C (λ i → Ai≈Bi) = A ≐[ i ]⟨ Ai≈Bi ⟩ B≅C + syntax step-≐[]-⟨ A B≅C (λ i → Bi≈Ai) = A ≐[ i ]⟨ Bi≈Ai ⟨ B≅C ``` ## Common sets and relations @@ -476,6 +476,7 @@ We do not require that both relations are indeed equivalence relations but only - equivalence of original indices `_≈ᵇ_` - Equal original indices index equal source elements. This means that the equality of original indices `_≈ᵇ_` has to be congruent with respect to equivalence `_≈_` of the source elements. + - `Symmetric _≈ᵃ_`: reflexivity over renamed indices is required for a detail in the proof. - `Symmetric _≈ᵇ_`: symmetry over original indices is required for a detail in the proof. ```agda re-indexʳ : ∀ {A B : Index} @@ -484,20 +485,21 @@ re-indexʳ : ∀ {A B : Index} → (rename : A → B) → (M : IndexedSet B) → Surjective _≈ᵃ_ _≈ᵇ_ rename + → RB.Reflexive _≈ᵃ_ → RB.Symmetric _≈ᵇ_ → Congruent _≈ᵇ_ _≈_ M --------------------- → M ⊆ (M ∘ rename) -re-indexʳ {A} {B} {_} {_≈ᵇ_} rename M rename-is-surjective ≈ᵇ-sym M-is-congruent b = +re-indexʳ {A} {B} {_≈ᵃ_} {_≈ᵇ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-sym M-is-congruent b = a , same-picks - where suitable-a : Σ[ a ∈ A ] (rename a ≈ᵇ b) + where suitable-a : Σ[ a ∈ A ] ({z : A} → z ≈ᵃ a → rename z ≈ᵇ b) suitable-a = rename-is-surjective b a : A a = proj₁ suitable-a same-picks : M b ≈ M (rename a) - same-picks = M-is-congruent (≈ᵇ-sym (proj₂ suitable-a)) + same-picks = M-is-congruent (≈ᵇ-sym (proj₂ suitable-a ≈ᵃ-refl)) re-index : ∀ {A B : Index} {_≈ᵃ_ : Rel A c} -- Equality of renamed indices @@ -505,13 +507,14 @@ re-index : ∀ {A B : Index} → (rename : A → B) → (M : IndexedSet B) → Surjective _≈ᵃ_ _≈ᵇ_ rename + → RB.Reflexive _≈ᵃ_ → RB.Symmetric _≈ᵇ_ → Congruent _≈ᵇ_ _≈_ M --------------------------- → (M ∘ rename) ≅ M -re-index {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵇ-sym M-is-congruent = +re-index {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-sym M-is-congruent = re-indexˡ rename M - , re-indexʳ {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵇ-sym M-is-congruent + , re-indexʳ {_≈ᵃ_ = _≈ᵃ_} rename M rename-is-surjective ≈ᵃ-refl ≈ᵇ-sym M-is-congruent ``` ## Examples diff --git a/src/Framework/Composition/FeatureAlgebra.agda b/src/Framework/Composition/FeatureAlgebra.agda index 7fae83c6..a6911b14 100644 --- a/src/Framework/Composition/FeatureAlgebra.agda +++ b/src/Framework/Composition/FeatureAlgebra.agda @@ -31,7 +31,7 @@ record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) w direct-idempotence i = begin i ⊕ i - ≡˘⟨ Eq.cong (i ⊕_) (proj₁ identity i) ⟩ + ≡⟨ Eq.cong (i ⊕_) (proj₁ identity i) ⟨ i ⊕ 𝟘 ⊕ i ≡⟨ distant-idempotence 𝟘 i ⟩ 𝟘 ⊕ i @@ -51,13 +51,13 @@ record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) w ≤-trans {i} {j} {k} i≤j j≤k = begin i ⊕ k - ≡˘⟨ Eq.cong (i ⊕_) j≤k ⟩ + ≡⟨ Eq.cong (i ⊕_) j≤k ⟨ i ⊕ (j ⊕ k) - ≡˘⟨ Eq.cong (λ x → i ⊕ x ⊕ k) i≤j ⟩ + ≡⟨ Eq.cong (λ x → i ⊕ x ⊕ k) i≤j ⟨ i ⊕ ((i ⊕ j) ⊕ k) - ≡˘⟨ assoc i (i ⊕ j) k ⟩ + ≡⟨ assoc i (i ⊕ j) k ⟨ (i ⊕ (i ⊕ j)) ⊕ k - ≡˘⟨ Eq.cong (_⊕ k) (assoc i i j) ⟩ + ≡⟨ Eq.cong (_⊕ k) (assoc i i j) ⟨ ((i ⊕ i) ⊕ j) ⊕ k ≡⟨ Eq.cong (_⊕ k) (Eq.cong (_⊕ j) (direct-idempotence i)) ⟩ (i ⊕ j) ⊕ k @@ -136,7 +136,7 @@ record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) w (i₂ ⊕ i₁) ⊕ i₁ ⊕ i₂ ≡⟨⟩ (i₂ ⊕ i₁) ⊕ (i₁ ⊕ i₂) - ≡˘⟨ assoc (i₂ ⊕ i₁) i₁ i₂ ⟩ + ≡⟨ assoc (i₂ ⊕ i₁) i₁ i₂ ⟨ ((i₂ ⊕ i₁) ⊕ i₁) ⊕ i₂ ≡⟨ Eq.cong (_⊕ i₂) (assoc i₂ i₁ i₁) ⟩ (i₂ ⊕ (i₁ ⊕ i₁)) ⊕ i₂ diff --git a/src/Framework/Properties/Finity.agda b/src/Framework/Properties/Finity.agda index db4b7cb8..7e407832 100644 --- a/src/Framework/Properties/Finity.agda +++ b/src/Framework/Properties/Finity.agda @@ -30,6 +30,7 @@ soundness-from-enumerability {L} L-has-finite-semantics {A} e = enumerate-configuration ⟦ e ⟧ (enumerate-is-surjective fin) + (Eq._≡_.refl) (IsEquivalence.sym (≣ⁱ-IsEquivalence L e)) (≣ⁱ-congruent L e) where ⟦_⟧ = Semantics L diff --git a/src/Framework/Variants.agda b/src/Framework/Variants.agda index b00d158b..872cef4b 100644 --- a/src/Framework/Variants.agda +++ b/src/Framework/Variants.agda @@ -1,5 +1,6 @@ {-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} module Framework.Variants where @@ -81,7 +82,7 @@ module _ (V : 𝕍) (A : 𝔸) {Γ : VariabilityLanguage V} (encoder : VariantEn ⟦ compile encoder v ⟧ c ≡⟨ irrelevant-index (encoded-variant-is-singleton-set v) ⟩ ⟦ compile encoder v ⟧ (conf encoder v tt) - ≡˘⟨ proj₁ (preserves encoder v) tt ⟩ + ≡⟨ proj₁ (preserves encoder v) tt ⟨ ⟦ v ⟧ᵥ tt ≡⟨⟩ v @@ -172,7 +173,7 @@ rose-encoder Γ has c = record -- rose x -- ≡⟨ {!!} ⟩ -- (cons (C∈ₛV has) ∘ pcong ArtifactC Γ (map-children t x)) (confi i) - -- ≡˘⟨ resistant has (map-children t x) (confi i) ⟩ + -- ≡⟨ resistant has (map-children t x) (confi i) ⟨ -- ⟦ cons (C∈ₛΓ has) (map-children t x) ⟧ (confi i) -- ∎ diff --git a/src/Lang/2CC.lagda.md b/src/Lang/2CC.lagda.md index e6c7f5d7..1cbe0fea 100644 --- a/src/Lang/2CC.lagda.md +++ b/src/Lang/2CC.lagda.md @@ -5,6 +5,7 @@ ```agda {-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} ``` ## Module diff --git a/src/Lang/ADT.agda b/src/Lang/ADT.agda index 86c69f1f..a625a1b3 100644 --- a/src/Lang/ADT.agda +++ b/src/Lang/ADT.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} + open import Framework.Definitions module Lang.ADT where diff --git a/src/Lang/ADT/Path.agda b/src/Lang/ADT/Path.agda index d22aad6f..4a5debe0 100644 --- a/src/Lang/ADT/Path.agda +++ b/src/Lang/ADT/Path.agda @@ -1,3 +1,5 @@ +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} + open import Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼) open import Relation.Binary using (DecidableEquality; Rel) module Lang.ADT.Path diff --git a/src/Lang/CCC.lagda.md b/src/Lang/CCC.lagda.md index 4499766d..6f027e00 100644 --- a/src/Lang/CCC.lagda.md +++ b/src/Lang/CCC.lagda.md @@ -6,6 +6,7 @@ For termination checking, we have to use sized types (i.e., types that are bound We use sizes to constrain the maximum tree-depth of an expression. ```agda {-# OPTIONS --sized-types #-} +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} ``` ## Module @@ -152,8 +153,8 @@ Maybe its smarter to do this for ADDs and then to conclude by transitivity of tr ⟦ encode v ⟧ c ≡⟨⟩ rose (a At.-< map (λ x → ⟦ x ⟧ c) (map encode cs) >-) - ≡˘⟨ Eq.cong rose $ - Eq.cong (a At.-<_>-) (map-∘ cs) ⟩ + ≡⟨ Eq.cong rose $ + Eq.cong (a At.-<_>-) (map-∘ cs) ⟨ rose (a At.-< map (λ x → ⟦ encode x ⟧ c) cs >-) ≡⟨ Eq.cong rose $ Eq.cong (a At.-<_>-) (go cs) ⟩ diff --git a/src/Lang/Gruler.agda b/src/Lang/Gruler.agda index 0989297e..59eb1839 100644 --- a/src/Lang/Gruler.agda +++ b/src/Lang/Gruler.agda @@ -1,4 +1,5 @@ {-# OPTIONS --sized-types #-} +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} open import Framework.Definitions module Lang.Gruler (F : 𝔽) where diff --git a/src/Lang/NADT.agda b/src/Lang/NADT.agda index c16d6b72..295c26f0 100644 --- a/src/Lang/NADT.agda +++ b/src/Lang/NADT.agda @@ -1,4 +1,5 @@ {-# OPTIONS --sized-types #-} +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} open import Framework.Definitions module Lang.NADT where diff --git a/src/Lang/NCC.lagda.md b/src/Lang/NCC.lagda.md index f037c5d6..744b4605 100644 --- a/src/Lang/NCC.lagda.md +++ b/src/Lang/NCC.lagda.md @@ -5,6 +5,7 @@ ```agda {-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} ``` ## Module diff --git a/src/Lang/OC.lagda.md b/src/Lang/OC.lagda.md index e7607704..aaec966e 100644 --- a/src/Lang/OC.lagda.md +++ b/src/Lang/OC.lagda.md @@ -5,6 +5,7 @@ ```agda {-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} ``` ## Module diff --git a/src/Lang/VariantList.lagda.md b/src/Lang/VariantList.lagda.md index 9a07af3d..8bf7cb20 100644 --- a/src/Lang/VariantList.lagda.md +++ b/src/Lang/VariantList.lagda.md @@ -1,3 +1,7 @@ +```agda +{-# OPTIONS --large-indices --no-forced-argument-recursion #-} +``` + # Lists of Variants are Also Variability Languages ## Module diff --git a/src/Translation/Lang/2CC-to-ADT.agda b/src/Translation/Lang/2CC-to-ADT.agda index 132b7dd8..7a64bec5 100644 --- a/src/Translation/Lang/2CC-to-ADT.agda +++ b/src/Translation/Lang/2CC-to-ADT.agda @@ -18,7 +18,7 @@ open import Function using (id) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≗_) open import Size using (Size) -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[]) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -57,7 +57,7 @@ translate (d 2CC.⟨ l , r ⟩) = d ⟨ translate l , translate r ⟩ → (vs : List (Variant A)) → ADT.⟦ go a cs cs' vs ⟧ config ≡ artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) cs') go' [] vs = Eq.sym (Eq.cong₂ artifact refl (Eq.trans (List.ʳ++-defn vs) (List.++-identityʳ (List.reverse vs)))) - go' (leaf v ∷ cs') vs = Eq.trans (go' cs' (v ∷ vs)) (Eq.cong₂ artifact refl (List.ʳ++-++ List.[ v ] {ys = vs})) + go' (leaf v ∷ cs') vs = Eq.trans (go' cs' (v ∷ vs)) (Eq.cong₂ artifact refl (List.++-ʳ++ List.[ v ] {ys = vs})) go' ((d ⟨ c₁ , c₂ ⟩) ∷ cs') vs = ADT.⟦ d ⟨ go a cs (c₁ ∷ cs') vs , go a cs (c₂ ∷ cs') vs ⟩ ⟧ config ≡⟨⟩ @@ -68,11 +68,11 @@ translate (d 2CC.⟨ l , r ⟩) = d ⟨ translate l , translate r ⟩ (if config d then artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (c₁ ∷ cs')) else artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (c₂ ∷ cs'))) - ≡˘⟨ Bool.push-function-into-if (λ c → artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (c ∷ cs'))) (config d) ⟩ + ≡⟨ Bool.if-float (λ c → artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (c ∷ cs'))) (config d) ⟨ artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) ((if config d then c₁ else c₂) ∷ cs')) ≡⟨⟩ artifact a (vs ʳ++ ADT.⟦ if config d then c₁ else c₂ ⟧ config ∷ List.map (λ e → ADT.⟦ e ⟧ config) cs') - ≡⟨ Eq.cong₂ artifact refl (Eq.cong₂ _ʳ++_ {x = vs} refl (Eq.cong₂ _∷_ (Bool.push-function-into-if (λ e → ADT.⟦ e ⟧ config) (config d)) refl)) ⟩ + ≡⟨ Eq.cong₂ artifact refl (Eq.cong₂ _ʳ++_ {x = vs} refl (Eq.cong₂ _∷_ (Bool.if-float (λ e → ADT.⟦ e ⟧ config) (config d)) refl)) ⟩ artifact a (vs ʳ++ (if config d then ADT.⟦ c₁ ⟧ config else ADT.⟦ c₂ ⟧ config) ∷ List.map (λ e → ADT.⟦ e ⟧ config) cs') ≡⟨⟩ artifact a (vs ʳ++ ADT.⟦ d ⟨ c₁ , c₂ ⟩ ⟧ config ∷ List.map (λ e → ADT.⟦ e ⟧ config) cs') @@ -89,7 +89,7 @@ preserves-≗ {D = D} {A = A} (a 2CC.-< cs >-) config = ADT.⟦ push-down-artifact a (List.map translate cs) ⟧ config ≡⟨ ⟦push-down-artifact⟧ a (List.map translate cs) config ⟩ artifact a (List.map (λ e → ADT.⟦ e ⟧ config) (List.map translate cs)) - ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟨ artifact a (List.map (λ e → ADT.⟦ translate e ⟧ config) cs) ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-≗ e config) cs) ⟩ artifact a (List.map (λ e → 2CC.⟦ e ⟧ config) cs) @@ -102,7 +102,7 @@ preserves-≗ (d 2CC.⟨ l , r ⟩) config = ADT.⟦ d ⟨ translate l , translate r ⟩ ⟧ config ≡⟨⟩ (if config d then ADT.⟦ translate l ⟧ config else ADT.⟦ translate r ⟧ config) - ≡˘⟨ Bool.push-function-into-if (λ e → ADT.⟦ translate e ⟧ config) (config d) ⟩ + ≡⟨ Bool.if-float (λ e → ADT.⟦ translate e ⟧ config) (config d) ⟨ ADT.⟦ translate (if config d then l else r) ⟧ config ≡⟨ preserves-≗ (if config d then l else r) config ⟩ 2CC.⟦ if config d then l else r ⟧ config diff --git a/src/Translation/Lang/2CC-to-NCC.agda b/src/Translation/Lang/2CC-to-NCC.agda index 039454f7..9be6b868 100644 --- a/src/Translation/Lang/2CC-to-NCC.agda +++ b/src/Translation/Lang/2CC-to-NCC.agda @@ -23,7 +23,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open import Size using (Size) open import Util.Nat.AtLeast using (ℕ≥; sucs) -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -62,7 +62,7 @@ module 2Ary where NCC.⟦ a -< List.map translate cs >- ⟧ config ≡⟨⟩ artifact a (List.map (λ e → NCC.⟦ e ⟧ config) (List.map translate cs)) - ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟨ artifact a (List.map (λ e → NCC.⟦ translate e ⟧ config) cs) ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ e config) cs) ⟩ artifact a (List.map (λ e → 2CC.⟦ e ⟧ (fnoc config)) cs) @@ -114,7 +114,7 @@ module 2Ary where 2CC.⟦ if config d then l else r ⟧ config ≡⟨ preserves-⊇ (if config d then l else r) config ⟩ NCC.⟦ translate (if config d then l else r) ⟧ (conf config) - ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Bool.push-function-into-if (translate) (config d)) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Bool.if-float (translate) (config d)) refl ⟩ NCC.⟦ if config d then translate l else translate r ⟧ (conf config) ≡⟨ Eq.cong₂ NCC.⟦_⟧ lemma refl ⟩ NCC.⟦ Vec.lookup (translate l ∷ translate r ∷ []) (conf config d) ⟧ (conf config) diff --git a/src/Translation/Lang/2CC/Rename.agda b/src/Translation/Lang/2CC/Rename.agda index 8785c85d..422a5d1c 100644 --- a/src/Translation/Lang/2CC/Rename.agda +++ b/src/Translation/Lang/2CC/Rename.agda @@ -10,7 +10,7 @@ This module renames dimensions in binary choice calculus expressions. module Translation.Lang.2CC.Rename (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where open import Data.Bool using (if_then_else_) -open import Data.Bool.Properties as Bool +import Data.Bool.Properties as Bool import Data.EqIndexedSet as IndexedSet open import Data.List as List using (List) import Data.List.Properties as List @@ -23,7 +23,7 @@ open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (refl; _≗_) open import Size using (Size) -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -56,7 +56,7 @@ preserves-⊆ f f⁻¹ (a -< cs >-) config = 2CC.⟦ a -< List.map (rename f) cs >- ⟧ config ≡⟨⟩ artifact a (List.map (λ e → 2CC.⟦ e ⟧ config) (List.map (rename f) cs)) - ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟨ artifact a (List.map (λ e → 2CC.⟦ rename f e ⟧ config) cs) ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ f f⁻¹ e config) cs) ⟩ artifact a (List.map (λ e → 2CC.⟦ e ⟧ (config ∘ f)) cs) @@ -69,7 +69,7 @@ preserves-⊆ f f⁻¹ (d ⟨ l , r ⟩) config = 2CC.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ config ≡⟨⟩ 2CC.⟦ if config (f d) then rename f l else rename f r ⟧ config - ≡˘⟨ Eq.cong₂ 2CC.⟦_⟧ (Bool.push-function-into-if (rename f) (config (f d))) refl ⟩ + ≡⟨ Eq.cong₂ 2CC.⟦_⟧ (Bool.if-float (rename f) (config (f d))) refl ⟨ 2CC.⟦ rename f (if config (f d) then l else r) ⟧ config ≡⟨ preserves-⊆ f f⁻¹ (if config (f d) then l else r) config ⟩ 2CC.⟦ if config (f d) then l else r ⟧ (config ∘ f) @@ -104,9 +104,9 @@ preserves-⊇ f f⁻¹ is-inverse (d ⟨ l , r ⟩) config = 2CC.⟦ if config d then l else r ⟧ config ≡⟨ preserves-⊇ f f⁻¹ is-inverse (if config d then l else r) config ⟩ 2CC.⟦ rename f (if config d then l else r) ⟧ (config ∘ f⁻¹) - ≡⟨ Eq.cong₂ 2CC.⟦_⟧ (push-function-into-if (rename f) (config d)) refl ⟩ + ≡⟨ Eq.cong₂ 2CC.⟦_⟧ (Bool.if-float (rename f) (config d)) refl ⟩ 2CC.⟦ if config d then rename f l else rename f r ⟧ (config ∘ f⁻¹) - ≡˘⟨ Eq.cong₂ 2CC.⟦_⟧ (Eq.cong-app (Eq.cong-app (Eq.cong if_then_else_ (Eq.cong config (is-inverse d))) (rename f l)) (rename f r)) refl ⟩ + ≡⟨ Eq.cong₂ 2CC.⟦_⟧ (Eq.cong-app (Eq.cong-app (Eq.cong if_then_else_ (Eq.cong config (is-inverse d))) (rename f l)) (rename f r)) refl ⟨ 2CC.⟦ if config (f⁻¹ (f d)) then rename f l else rename f r ⟧ (config ∘ f⁻¹) ≡⟨⟩ 2CC.⟦ f d ⟨ rename f l , rename f r ⟩ ⟧ (config ∘ f⁻¹) diff --git a/src/Translation/Lang/ADT-to-2CC.agda b/src/Translation/Lang/ADT-to-2CC.agda index 60c68416..1c29c271 100644 --- a/src/Translation/Lang/ADT-to-2CC.agda +++ b/src/Translation/Lang/ADT-to-2CC.agda @@ -20,7 +20,7 @@ open import Function using (id) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≗_) open import Size using (Size; ∞) -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[]) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -51,7 +51,7 @@ preserves-≗ Variant→2CC (f ADT.⟨ l , r ⟩) config = 2CC.⟦ f 2CC.⟨ translate Variant→2CC l , translate Variant→2CC r ⟩ ⟧ config ≡⟨⟩ 2CC.⟦ if config f then translate Variant→2CC l else translate Variant→2CC r ⟧ config - ≡⟨ Bool.push-function-into-if (λ e → 2CC.⟦ e ⟧ config) (config f) ⟩ + ≡⟨ Bool.if-float (λ e → 2CC.⟦ e ⟧ config) (config f) ⟩ (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) ⟩ (if config f then ADT.⟦ l ⟧ config else ADT.⟦ r ⟧ config) diff --git a/src/Translation/Lang/ADT-to-NADT.agda b/src/Translation/Lang/ADT-to-NADT.agda index 6c90aa55..0ede2dee 100644 --- a/src/Translation/Lang/ADT-to-NADT.agda +++ b/src/Translation/Lang/ADT-to-NADT.agda @@ -68,7 +68,7 @@ preserves-⊆ (f ADT.⟨ l , r ⟩) config = NADT.⟦ List.find-or-last (config f) (translate l ∷ translate r ∷ []) ⟧ config ≡⟨ Eq.cong₂ NADT.⟦_⟧ lemma refl ⟩ NADT.⟦ if fnoc config f then translate l else translate r ⟧ config - ≡⟨ Bool.push-function-into-if (λ e → NADT.⟦ e ⟧ config) (fnoc config f) ⟩ + ≡⟨ 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) ⟩ (if fnoc config f then ADT.⟦ l ⟧ (fnoc config) else ADT.⟦ r ⟧ (fnoc config)) @@ -89,7 +89,7 @@ preserves-⊇ (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) ⟩ (if config f then NADT.⟦ translate l ⟧ (conf config) else NADT.⟦ translate r ⟧ (conf config)) - ≡˘⟨ Bool.push-function-into-if (λ e → NADT.⟦ e ⟧ (conf config)) (config f) ⟩ + ≡⟨ Bool.if-float (λ e → NADT.⟦ e ⟧ (conf config)) (config f) ⟨ NADT.⟦ if config f then translate l else translate r ⟧ (conf config) ≡⟨ Eq.cong₂ NADT.⟦_⟧ lemma refl ⟩ NADT.⟦ List.find-or-last (conf config f) (translate l ∷ translate r ∷ []) ⟧ (conf config) diff --git a/src/Translation/Lang/ADT-to-VariantList.agda b/src/Translation/Lang/ADT-to-VariantList.agda index 643aef12..e9336ddd 100644 --- a/src/Translation/Lang/ADT-to-VariantList.agda +++ b/src/Translation/Lang/ADT-to-VariantList.agda @@ -106,7 +106,7 @@ preservation-walk-to-list-conf (D ⟨ l , r ⟩) ((_ ∷ pl) is-valid walk-left walk l c ≡⟨ preservation-walk-to-list-conf l c ⟩ ⟦ tr l ⟧ₗ (conf l c) - ≡˘⟨ find-or-last-append (tr l) (tr r) (conf-bounded l c) ⟩ + ≡⟨ find-or-last-append (tr l) (tr r) (conf-bounded l c) ⟨ ⟦ tr l ⁺++⁺ tr r ⟧ₗ (conf l c) ∎ preservation-walk-to-list-conf (D ⟨ l , r ⟩) ((_ ∷ pr) is-valid walk-right t) = @@ -116,7 +116,7 @@ preservation-walk-to-list-conf (D ⟨ l , r ⟩) ((_ ∷ pr) is-valid walk-right walk r c ≡⟨ preservation-walk-to-list-conf r c ⟩ ⟦ tr r ⟧ₗ (conf r c) - ≡˘⟨ find-or-last-prepend-+ (conf r c) (tr l) (tr r) ⟩ + ≡⟨ find-or-last-prepend-+ (conf r c) (tr l) (tr r) ⟨ ⟦ tr l ⁺++⁺ tr r ⟧ₗ (length (tr l) + (conf r c)) ∎ diff --git a/src/Translation/Lang/ADT/Rename.agda b/src/Translation/Lang/ADT/Rename.agda index c0ed63a7..6e476447 100644 --- a/src/Translation/Lang/ADT/Rename.agda +++ b/src/Translation/Lang/ADT/Rename.agda @@ -23,7 +23,7 @@ open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (refl; _≗_) open import Size using (Size) -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -76,7 +76,7 @@ preserves-⊇ f f⁻¹ is-inverse (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) ⟩ (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⁻¹)) ⟩ + ≡⟨ 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⁻¹)) ⟨ (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/Translation/Lang/ADT/WalkSemantics.agda b/src/Translation/Lang/ADT/WalkSemantics.agda index fb0c41ae..e8ac0a83 100644 --- a/src/Translation/Lang/ADT/WalkSemantics.agda +++ b/src/Translation/Lang/ADT/WalkSemantics.agda @@ -282,7 +282,7 @@ preservation-path-configs-fnoc (D ⟨ l , r ⟩) u c@((.(D ↣ true ) ∷ p) is- walk l (p is-valid t) ≡⟨ preservation-path-configs-fnoc l (undead-left u) (p is-valid t) ⟩ ⟦ l ⟧ (path-to-fun l (p is-valid t)) - ≡˘⟨ path-to-fun-step-l D l r u p t ⟩ + ≡⟨ path-to-fun-step-l D l r u p t ⟨ ⟦ l ⟧ (path-to-fun (D ⟨ l , r ⟩) ((D ↣ true ∷ p) is-valid walk-left t)) ≡⟨⟩ ⟦ l ⟧ (λ D' → if isYes (D == D') then true else path-to-fun l (p is-valid t) D') diff --git a/src/Translation/Lang/CCC-to-NCC.agda b/src/Translation/Lang/CCC-to-NCC.agda index ee48e1e7..9a1309ec 100644 --- a/src/Translation/Lang/CCC-to-NCC.agda +++ b/src/Translation/Lang/CCC-to-NCC.agda @@ -25,9 +25,9 @@ open import Util.List using (find-or-last; map-find-or-last; find-or-last⇒look open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs; _⊔_) import Util.Vec as Vec -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open IndexedSet.≅[]-Reasoning using (step-≅[]; step-≅[]˘; _≅[]⟨⟩_; _≅[]-∎) +open IndexedSet.≅[]-Reasoning using (step-≅[]-⟨; step-≅[]-⟩; _≅[]⟨⟩_; _≅[]-∎) open import Lang.All.Generic Variant Artifact∈ₛVariant open CCC using (CCC; CCCL; _-<_>-; _⟨_⟩) @@ -219,7 +219,7 @@ module Exact where NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (Fin.cast (Eq.sym (Eq.cong suc (length-zipWith (sucs n) cs max-cs))) (ℕ≥.cappedFin (Fin.toℕ (config d)))) ⟧ config ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)}) (ℕ≥.cast-cappedFin (Fin.toℕ (config d)) (Eq.sym (Eq.cong suc (length-zipWith (sucs n) cs max-cs))))) refl ⟩ NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (ℕ≥.cappedFin (Fin.toℕ (config d))) ⟧ config - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (find-or-last⇒lookup (translate (sucs n) c max-c) (zipWith (sucs n) (translate (sucs n)) cs max-cs)) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (find-or-last⇒lookup (translate (sucs n) c max-c) (zipWith (sucs n) (translate (sucs n)) cs max-cs)) refl ⟨ NCC.⟦ find-or-last (Fin.toℕ (config d)) (translate (sucs n) c max-c ∷ zipWith (sucs n) (translate (sucs n)) cs max-cs) ⟧ config ≡⟨ map-find-or-last (λ e → NCC.⟦ e ⟧ config) (Fin.toℕ (config d)) (translate (sucs n) c max-c ∷ zipWith (sucs n) (translate (sucs n)) cs max-cs) ⟩ find-or-last (Fin.toℕ (config d)) (NCC.⟦ translate (sucs n) c max-c ⟧ config ∷ List.map (λ e → NCC.⟦ e ⟧ config) (zipWith (sucs n) (translate (sucs n)) cs max-cs)) @@ -231,7 +231,7 @@ module Exact where find-or-last (Fin.toℕ (config d)) (CCC.⟦ c ⟧ (fnoc (sucs n) config) ∷ List.map (λ e → CCC.⟦ e ⟧ (fnoc (sucs n) config)) cs) ≡⟨⟩ find-or-last (Fin.toℕ (config d)) (List⁺.map (λ e → CCC.⟦ e ⟧ (fnoc (sucs n) config)) (c ∷ cs)) - ≡˘⟨ map-find-or-last (λ e → CCC.⟦ e ⟧ (fnoc (sucs n) config)) (fnoc (sucs n) config d) (c ∷ cs) ⟩ + ≡⟨ map-find-or-last (λ e → CCC.⟦ e ⟧ (fnoc (sucs n) config)) (fnoc (sucs n) config d) (c ∷ cs) ⟨ CCC.⟦ find-or-last (fnoc (sucs n) config d) (c ∷ cs) ⟧ (fnoc (sucs n) config) ≡⟨⟩ CCC.⟦ d ⟨ c ∷ cs ⟩ ⟧ (fnoc (sucs n) config) @@ -246,11 +246,11 @@ module Exact where CCC.⟦ a -< cs >- ⟧ config ≡⟨⟩ artifact a (List.map (λ e → CCC.⟦ e ⟧ config) cs) - ≡˘⟨ Eq.cong₂ artifact refl (zipWith⇒map n (λ e → CCC.⟦ e ⟧ config) cs max-cs) ⟩ + ≡⟨ Eq.cong₂ artifact refl (zipWith⇒map n (λ e → CCC.⟦ e ⟧ config) cs max-cs) ⟨ artifact a (zipWith n (λ e max-e → CCC.⟦ e ⟧ config) cs max-cs) ≡⟨ Eq.cong₂ artifact refl (zipWith-cong n (λ e max-e → preserves-⊇ n e max-e config) cs max-cs) ⟩ artifact a (zipWith n (λ e max-e → NCC.⟦ translate n e max-e ⟧ (conf n config)) cs max-cs) - ≡˘⟨ Eq.cong₂ artifact refl (map∘zipWith n cs max-cs) ⟩ + ≡⟨ Eq.cong₂ artifact refl (map∘zipWith n cs max-cs) ⟨ artifact a (List.map (λ e → NCC.⟦ e ⟧ (conf n config)) (zipWith n (translate n) cs max-cs)) ≡⟨⟩ NCC.⟦ a -< zipWith n (translate n) cs max-cs >- ⟧ (conf n config) @@ -265,25 +265,25 @@ module Exact where find-or-last (config d) (List⁺.map (λ e → CCC.⟦ e ⟧ config) (c ∷ cs)) ≡⟨⟩ find-or-last (config d) (CCC.⟦ c ⟧ config ∷ List.map (λ e → CCC.⟦ e ⟧ config) cs) - ≡˘⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ refl (zipWith⇒map (sucs n) (λ e → CCC.⟦ e ⟧ config) cs max-cs)) ⟩ + ≡⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ refl (zipWith⇒map (sucs n) (λ e → CCC.⟦ e ⟧ config) cs max-cs)) ⟨ find-or-last (config d) (CCC.⟦ c ⟧ config ∷ zipWith (sucs n) (λ e max-e → CCC.⟦ e ⟧ config) cs max-cs) ≡⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ (preserves-⊇ (sucs n) c max-c config) (zipWith-cong (sucs n) (λ e max-e → preserves-⊇ (sucs n) e max-e config) cs max-cs)) ⟩ find-or-last (config d) (NCC.⟦ translate (sucs n) c max-c ⟧ (conf (sucs n) config) ∷ zipWith (sucs n) (λ e max-e → NCC.⟦ translate (sucs n) e max-e ⟧ (conf (sucs n) config)) cs max-cs) - ≡˘⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ refl (map∘zipWith (sucs n) cs max-cs)) ⟩ + ≡⟨ Eq.cong₂ find-or-last refl (Eq.cong₂ _∷_ refl (map∘zipWith (sucs n) cs max-cs)) ⟨ find-or-last (config d) (NCC.⟦ translate (sucs n) c max-c ⟧ (conf (sucs n) config) ∷ List.map (λ e → NCC.⟦ e ⟧ (conf (sucs n) config)) (zipWith (sucs n) (translate (sucs n)) cs max-cs)) - ≡˘⟨ map-find-or-last (λ e → NCC.⟦ e ⟧ (conf (sucs n) config)) (config d) (translate (sucs n) c max-c ∷ zipWith (sucs n) (translate (sucs n)) cs max-cs) ⟩ + ≡⟨ map-find-or-last (λ e → NCC.⟦ e ⟧ (conf (sucs n) config)) (config d) (translate (sucs n) c max-c ∷ zipWith (sucs n) (translate (sucs n)) cs max-cs) ⟨ NCC.⟦ find-or-last (config d) (translate (sucs n) c max-c ∷ zipWith (sucs n) (translate (sucs n)) cs max-cs) ⟧ (conf (sucs n) config) ≡⟨ Eq.cong₂ NCC.⟦_⟧ (find-or-last⇒lookup (translate (sucs n) c max-c) (zipWith (sucs n) (translate (sucs n)) cs max-cs)) refl ⟩ NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (ℕ≥.cappedFin (config d)) ⟧ (conf (sucs n) config) - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)}) (ℕ≥.cast-cappedFin (config d) (Eq.sym (Eq.cong suc (length-zipWith (sucs n) cs max-cs))))) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)}) (ℕ≥.cast-cappedFin (config d) (Eq.sym (Eq.cong suc (length-zipWith (sucs n) cs max-cs))))) refl ⟨ NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (Fin.cast (Eq.sym (Eq.cong suc (length-zipWith (sucs n) cs max-cs))) (ℕ≥.cappedFin (config d))) ⟧ (conf (sucs n) config) - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-cast₁ (Eq.cong suc (length-zipWith (sucs n) cs max-cs)) (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (ℕ≥.cappedFin (config d))) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-cast₁ (Eq.cong suc (length-zipWith (sucs n) cs max-cs)) (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)) (ℕ≥.cappedFin (config d))) refl ⟨ NCC.⟦ Vec.lookup (Vec.cast (Eq.cong suc (length-zipWith (sucs n) cs max-cs)) (translate (sucs n) c max-c ∷ Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (ℕ≥.cappedFin (config d)) ⟧ (conf (sucs n) config) ≡⟨⟩ NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (ℕ≥.cappedFin (config d)) ⟧ (conf (sucs n) config) - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))}) (ℕ≥.cappedFin-idempotent max≤n (config d))) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))}) (ℕ≥.cappedFin-idempotent max≤n (config d))) refl ⟨ NCC.⟦ Vec.lookup (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (ℕ≥.cappedFin (Fin.toℕ (conf (sucs n) config d))) ⟧ (conf (sucs n) config) - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-saturate (s≤s max≤n) (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (conf (sucs n) config d)) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-saturate (s≤s max≤n) (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) (conf (sucs n) config d)) refl ⟨ NCC.⟦ Vec.lookup (Vec.saturate (s≤s max≤n) (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs)))) (conf (sucs n) config d) ⟧ (conf (sucs n) config) ≡⟨⟩ NCC.⟦ d ⟨ Vec.saturate (s≤s max≤n) (translate (sucs n) c max-c ∷ Vec.cast (length-zipWith (sucs n) cs max-cs) (Vec.fromList (zipWith (sucs n) (translate (sucs n)) cs max-cs))) ⟩ ⟧ (conf (sucs n) config) @@ -361,9 +361,9 @@ preserves (sucs n) expr = NCC.⟦ translate (sucs n) expr ⟧ ≅[]⟨⟩ NCC.⟦ NCC-rename.compile (sucs n) (Fin→ℕ ⌈ expr ⌉) (Fin→ℕ⁻¹ ⌈ expr ⌉) (Fin→ℕ⁻¹-Fin→ℕ ⌈ expr ⌉) (NCC→NCC.compile ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) ⟧ - ≅[]˘⟨ NCC-rename.preserves (sucs n) (Fin→ℕ ⌈ expr ⌉) (Fin→ℕ⁻¹ ⌈ expr ⌉) (Fin→ℕ⁻¹-Fin→ℕ ⌈ expr ⌉) (NCC→NCC.compile ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) ⟩ + ≅[]⟨ NCC-rename.preserves (sucs n) (Fin→ℕ ⌈ expr ⌉) (Fin→ℕ⁻¹ ⌈ expr ⌉) (Fin→ℕ⁻¹-Fin→ℕ ⌈ expr ⌉) (NCC→NCC.compile ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) ⟨ NCC.⟦ NCC→NCC.compile ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr)) ⟧ - ≅[]˘⟨ (NCC→NCC.preserves ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) ⟩ + ≅[]⟨ (NCC→NCC.preserves ⌈ expr ⌉ (sucs n) (Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr))) ⟨ NCC.⟦ Exact.translate ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr) ⟧ ≅[]⟨ Exact.preserves ⌈ expr ⌉ expr (numberOfAlternatives≤⌈_⌉ expr) ⟩ CCC.⟦ expr ⟧ diff --git a/src/Translation/Lang/NADT-to-CCC.agda b/src/Translation/Lang/NADT-to-CCC.agda index e8106a0b..778ee0af 100644 --- a/src/Translation/Lang/NADT-to-CCC.agda +++ b/src/Translation/Lang/NADT-to-CCC.agda @@ -20,7 +20,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (refl; _≗_) open import Size using (Size; ∞) import Util.List as List -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[]) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -48,7 +48,7 @@ preserves-≗ Variant→CCC (NADTChoice (f Choice.⟨ alternatives ⟩)) config CCC.⟦ f ⟨ List⁺.map (translate Variant→CCC) alternatives ⟩ ⟧ config ≡⟨⟩ CCC.⟦ List.find-or-last (config f) (List⁺.map (translate Variant→CCC) alternatives) ⟧ config - ≡˘⟨ Eq.cong₂ CCC.⟦_⟧ (List.map-find-or-last (translate Variant→CCC) (config f) alternatives) refl ⟩ + ≡⟨ Eq.cong₂ CCC.⟦_⟧ (List.map-find-or-last (translate Variant→CCC) (config f) alternatives) refl ⟨ CCC.⟦ translate Variant→CCC (List.find-or-last (config f) alternatives) ⟧ config ≡⟨ preserves-≗ Variant→CCC (List.find-or-last (config f) alternatives) config ⟩ NADT.⟦ List.find-or-last (config f) alternatives ⟧ config diff --git a/src/Translation/Lang/NCC-to-2CC.agda b/src/Translation/Lang/NCC-to-2CC.agda index a50ec8fe..86c85da4 100644 --- a/src/Translation/Lang/NCC-to-2CC.agda +++ b/src/Translation/Lang/NCC-to-2CC.agda @@ -23,7 +23,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open import Size using (Size; ∞) open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -60,7 +60,7 @@ module 2Ary where 2CC.⟦ (a -< List.map translate cs >-) ⟧ config ≡⟨⟩ artifact a (List.map (λ e → 2CC.⟦ e ⟧ config) (List.map translate cs)) - ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟨ artifact a (List.map (λ e → 2CC.⟦ translate e ⟧ config) cs) ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ e config) cs) ⟩ artifact a (List.map (λ e → NCC.⟦ e ⟧ (fnoc config)) cs) @@ -73,7 +73,7 @@ module 2Ary where 2CC.⟦ d ⟨ translate l , translate r ⟩ ⟧ config ≡⟨⟩ 2CC.⟦ if config d then translate l else translate r ⟧ config - ≡⟨ Bool.push-function-into-if (λ e → 2CC.⟦ e ⟧ config) (config d) ⟩ + ≡⟨ Bool.if-float (λ e → 2CC.⟦ e ⟧ config) (config d) ⟩ (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) ⟩ (if config d then NCC.⟦ l ⟧ (fnoc config) else NCC.⟦ r ⟧ (fnoc config)) @@ -110,13 +110,13 @@ module 2Ary where NCC.⟦ d ⟨ l ∷ r ∷ [] ⟩ ⟧ config ≡⟨⟩ NCC.⟦ Vec.lookup (l ∷ r ∷ []) (config d) ⟧ config - ≡˘⟨ Vec.lookup-map (config d) (λ e → NCC.⟦ e ⟧ config) (l ∷ r ∷ []) ⟩ + ≡⟨ Vec.lookup-map (config d) (λ e → NCC.⟦ e ⟧ config) (l ∷ r ∷ []) ⟨ 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) ⟩ (if conf config d then 2CC.⟦ translate l ⟧ (conf config) else 2CC.⟦ translate r ⟧ (conf config)) - ≡˘⟨ Bool.push-function-into-if (λ e → 2CC.⟦ e ⟧ (conf config)) (conf config d) ⟩ + ≡⟨ Bool.if-float (λ e → 2CC.⟦ e ⟧ (conf config)) (conf config d) ⟨ 2CC.⟦ if conf config d then translate l else translate r ⟧ (conf config) ≡⟨⟩ 2CC.⟦ d ⟨ translate l , translate r ⟩ ⟧ (conf config) diff --git a/src/Translation/Lang/NCC-to-CCC.agda b/src/Translation/Lang/NCC-to-CCC.agda index b1a19c32..72cbb828 100644 --- a/src/Translation/Lang/NCC-to-CCC.agda +++ b/src/Translation/Lang/NCC-to-CCC.agda @@ -22,7 +22,7 @@ open import Size using (Size; ∞) open import Util.List using (find-or-last; lookup⇒find-or-last) open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -63,7 +63,7 @@ preserves-⊆ n (a -< cs >-) config = CCC.⟦ a -< List.map (translate n) cs >- ⟧ config ≡⟨⟩ artifact a (List.map (λ e → CCC.⟦ e ⟧ config) (List.map (translate n) cs)) - ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ {g = (λ e → CCC.⟦ e ⟧ config)} {f = translate n} cs) ⟩ + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ {g = (λ e → CCC.⟦ e ⟧ config)} {f = translate n} cs) ⟨ artifact a (List.map (λ e → CCC.⟦ translate n e ⟧ config) cs) ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ n e config) cs) ⟩ artifact a (List.map (λ e → NCC.⟦ e ⟧ (fnoc n config)) cs) @@ -76,7 +76,7 @@ preserves-⊆ (sucs n) (d ⟨ c ∷ cs ⟩) config = CCC.⟦ d ⟨ List⁺.fromVec (Vec.map (translate (sucs n)) (c ∷ cs)) ⟩ ⟧ config ≡⟨⟩ CCC.⟦ find-or-last (config d) (List⁺.fromVec (Vec.map (translate (sucs n)) (c ∷ cs))) ⟧ config - ≡˘⟨ Eq.cong₂ CCC.⟦_⟧ (lookup⇒find-or-last {m = config d} (translate (sucs n) c ∷ Vec.map (translate (sucs n)) cs)) refl ⟩ + ≡⟨ Eq.cong₂ CCC.⟦_⟧ (lookup⇒find-or-last {m = config d} (translate (sucs n) c ∷ Vec.map (translate (sucs n)) cs)) refl ⟨ CCC.⟦ Vec.lookup (Vec.map (translate (sucs n)) (c ∷ cs)) (ℕ≥.cappedFin (config d)) ⟧ config ≡⟨ Eq.cong₂ CCC.⟦_⟧ (Vec.lookup-map (ℕ≥.cappedFin (config d)) (translate (sucs n)) (c ∷ cs)) refl ⟩ CCC.⟦ translate (sucs n) (Vec.lookup (c ∷ cs) (ℕ≥.cappedFin (config d))) ⟧ config @@ -109,9 +109,9 @@ preserves-⊇ {D} {A} (sucs n) (d ⟨ c ∷ cs ⟩) config = NCC.⟦ Vec.lookup (c ∷ cs) (config d) ⟧ config ≡⟨ preserves-⊇ (sucs n) (Vec.lookup (c ∷ cs) (config d)) config ⟩ CCC.⟦ translate (sucs n) (Vec.lookup (c ∷ cs) (config d)) ⟧ (conf (sucs n) config) - ≡˘⟨ Eq.cong₂ CCC.⟦_⟧ (Vec.lookup-map (config d) (translate (sucs n)) (c ∷ cs)) refl ⟩ + ≡⟨ Eq.cong₂ CCC.⟦_⟧ (Vec.lookup-map (config d) (translate (sucs n)) (c ∷ cs)) refl ⟨ CCC.⟦ Vec.lookup (Vec.map (translate (sucs n)) (c ∷ cs)) (config d) ⟧ (conf (sucs n) config) - ≡˘⟨ Eq.cong₂ CCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = Vec.map (translate (sucs n)) (c ∷ cs)}) (ℕ≥.cappedFin-toℕ (config d))) refl ⟩ + ≡⟨ Eq.cong₂ CCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = Vec.map (translate (sucs n)) (c ∷ cs)}) (ℕ≥.cappedFin-toℕ (config d))) refl ⟨ CCC.⟦ Vec.lookup (Vec.map (translate (sucs n)) (c ∷ cs)) (ℕ≥.cappedFin (Fin.toℕ (config d))) ⟧ (conf (sucs n) config) ≡⟨ Eq.cong₂ CCC.⟦_⟧ (lookup⇒find-or-last {m = Fin.toℕ (config d)} (translate (sucs n) c ∷ Vec.map (translate (sucs n)) cs)) refl ⟩ CCC.⟦ find-or-last (Fin.toℕ (config d)) (List⁺.fromVec (Vec.map (translate (sucs n)) (c ∷ cs))) ⟧ (conf (sucs n) config) diff --git a/src/Translation/Lang/NCC/Grow.agda b/src/Translation/Lang/NCC/Grow.agda index e2e768c2..5c395bc4 100644 --- a/src/Translation/Lang/NCC/Grow.agda +++ b/src/Translation/Lang/NCC/Grow.agda @@ -33,7 +33,7 @@ import Util.AuxProofs as ℕ open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) import Util.Vec as Vec -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -78,7 +78,7 @@ preserves-⊆ n m n≤m (a -< cs >-) config = NCC.⟦ a -< List.map (grow n m n≤m) cs >- ⟧ config ≡⟨⟩ artifact a (List.map (λ e → NCC.⟦ e ⟧ config) (List.map (grow n m n≤m) cs)) - ≡˘⟨ Eq.cong₂ artifact Eq.refl (List.map-∘ cs) ⟩ + ≡⟨ Eq.cong₂ artifact Eq.refl (List.map-∘ cs) ⟨ artifact a (List.map (λ e → NCC.⟦ grow n m n≤m e ⟧ config) cs) ≡⟨ Eq.cong₂ artifact Eq.refl (List.map-cong (λ e → preserves-⊆ n m n≤m e config) cs) ⟩ artifact a (List.map (λ e → NCC.⟦ e ⟧ (fnoc n m n≤m config)) cs) @@ -121,19 +121,19 @@ preserves-⊇ (sucs n) (sucs m) n≤m (d ⟨ cs ⟩) config = NCC.⟦ d ⟨ cs ⟩ ⟧ config ≡⟨⟩ NCC.⟦ Vec.lookup cs (config d) ⟧ config - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = cs}) (ℕ≥.cappedFin-toℕ (config d))) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = cs}) (ℕ≥.cappedFin-toℕ (config d))) refl ⟨ NCC.⟦ Vec.lookup cs (ℕ≥.cappedFin (Fin.toℕ (config d))) ⟧ config - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = cs}) (Eq.cong ℕ≥.cappedFin (Fin.toℕ-inject≤ (config d) n≤m))) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (refl {x = cs}) (Eq.cong ℕ≥.cappedFin (Fin.toℕ-inject≤ (config d) n≤m))) refl ⟨ NCC.⟦ Vec.lookup cs (ℕ≥.cappedFin (Fin.toℕ (Fin.inject≤ (config d) n≤m))) ⟧ config - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-saturate n≤m cs (Fin.inject≤ (config d) n≤m)) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-saturate n≤m cs (Fin.inject≤ (config d) n≤m)) refl ⟨ NCC.⟦ Vec.lookup (Vec.saturate n≤m cs) (Fin.inject≤ (config d) n≤m) ⟧ config ≡⟨⟩ NCC.⟦ Vec.lookup (Vec.saturate n≤m cs) (conf (sucs n) (sucs m) n≤m config d) ⟧ config ≡⟨ preserves-⊇ (sucs n) (sucs m) n≤m (Vec.lookup (Vec.saturate n≤m cs) (conf (sucs n) (sucs m) n≤m config d)) config ⟩ NCC.⟦ (grow (sucs n) (sucs m) n≤m) (Vec.lookup (Vec.saturate n≤m cs) (conf (sucs n) (sucs m) n≤m config d)) ⟧ (conf (sucs n) (sucs m) n≤m config) - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (conf (sucs n) (sucs m) n≤m config d) (grow (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (conf (sucs n) (sucs m) n≤m config d) (grow (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) refl ⟨ NCC.⟦ Vec.lookup (Vec.map (grow (sucs n) (sucs m) n≤m) (Vec.saturate n≤m cs)) (conf (sucs n) (sucs m) n≤m config d) ⟧ (conf (sucs n) (sucs m) n≤m config) - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (Vec.saturate-map n≤m (grow (sucs n) (sucs m) n≤m) cs) refl) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup (Vec.saturate-map n≤m (grow (sucs n) (sucs m) n≤m) cs) refl) refl ⟨ NCC.⟦ Vec.lookup (Vec.saturate n≤m (Vec.map (grow (sucs n) (sucs m) n≤m) cs)) (conf (sucs n) (sucs m) n≤m config d) ⟧ (conf (sucs n) (sucs m) n≤m config) ≡⟨⟩ NCC.⟦ d ⟨ Vec.saturate n≤m (Vec.map (grow (sucs n) (sucs m) n≤m) cs) ⟩ ⟧ (conf (sucs n) (sucs m) n≤m config) diff --git a/src/Translation/Lang/NCC/NCC-to-NCC.agda b/src/Translation/Lang/NCC/NCC-to-NCC.agda index 6eca2398..e23d1fe2 100644 --- a/src/Translation/Lang/NCC/NCC-to-NCC.agda +++ b/src/Translation/Lang/NCC/NCC-to-NCC.agda @@ -37,9 +37,6 @@ import Util.AuxProofs as ℕ open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) import Util.Vec as Vec -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) -open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) - open import Lang.All.Generic Variant Artifact∈ₛVariant open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) diff --git a/src/Translation/Lang/NCC/Rename.agda b/src/Translation/Lang/NCC/Rename.agda index d831d835..de4c97c3 100644 --- a/src/Translation/Lang/NCC/Rename.agda +++ b/src/Translation/Lang/NCC/Rename.agda @@ -32,7 +32,7 @@ import Util.AuxProofs as ℕ open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) import Util.Vec as Vec -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -68,7 +68,7 @@ preserves-⊆ n f f⁻¹ (a -< cs >-) config = NCC.⟦ a -< List.map (rename n f) cs >- ⟧ config ≡⟨⟩ artifact a (List.map (λ e → NCC.⟦ e ⟧ config) (List.map (rename n f) cs)) - ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟨ artifact a (List.map (λ e → NCC.⟦ rename n f e ⟧ config) cs) ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ n f f⁻¹ e config) cs) ⟩ artifact a (List.map (λ e → NCC.⟦ e ⟧ (config ∘ f)) cs) @@ -115,9 +115,9 @@ preserves-⊇ n f f⁻¹ is-inverse (d ⟨ cs ⟩) config = NCC.⟦ Vec.lookup cs (config d) ⟧ config ≡⟨ preserves-⊇ n f f⁻¹ is-inverse (Vec.lookup cs (config d)) config ⟩ NCC.⟦ rename n f (Vec.lookup cs (config d)) ⟧ (config ∘ f⁻¹) - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (config d) (rename n f) cs) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Vec.lookup-map (config d) (rename n f) cs) refl ⟨ NCC.⟦ Vec.lookup (Vec.map (rename n f) cs) (config d) ⟧ (config ∘ f⁻¹) - ≡˘⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = Vec.map (rename n f) cs} refl (Eq.cong config (is-inverse d))) refl ⟩ + ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = Vec.map (rename n f) cs} refl (Eq.cong config (is-inverse d))) refl ⟨ NCC.⟦ Vec.lookup (Vec.map (rename n f) cs) (config ((f⁻¹ ∘ f) d)) ⟧ (config ∘ f⁻¹) ≡⟨⟩ NCC.⟦ f d ⟨ Vec.map (rename n f) cs ⟩ ⟧ (config ∘ f⁻¹) diff --git a/src/Translation/Lang/NCC/ShrinkTo2.agda b/src/Translation/Lang/NCC/ShrinkTo2.agda index a23b0bac..e2f1c1cb 100644 --- a/src/Translation/Lang/NCC/ShrinkTo2.agda +++ b/src/Translation/Lang/NCC/ShrinkTo2.agda @@ -38,7 +38,7 @@ import Util.AuxProofs as ℕ open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) import Util.Vec as Vec -open Eq.≡-Reasoning using (step-≡; step-≡˘; _≡⟨⟩_; _∎) +open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) open import Lang.All.Generic Variant Artifact∈ₛVariant @@ -138,7 +138,7 @@ module FnocLemmas where → (∀ {k} → k Fin.< Fin.opposite (Fin.fromℕ< { m} (<-trans (ℕ.n<1+n m) m-) config = NCC.⟦ a -< List.map (shrinkTo2 (sucs n)) cs >- ⟧ config ≡⟨⟩ artifact a (List.map (λ e → NCC.⟦ e ⟧ config) (List.map (shrinkTo2 (sucs n)) cs)) - ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩ + ≡⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟨ artifact a (List.map (λ e → NCC.⟦ shrinkTo2 (sucs n) e ⟧ config) cs) ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-⊆ (sucs n) e config) cs) ⟩ artifact a (List.map (λ e → NCC.⟦ e ⟧ (fnoc (sucs n) config)) cs) @@ -229,7 +229,7 @@ preserves-⊆ {D = D} {A = A} (sucs n) (d ⟨ cs ⟩) config = n ≤.<⟨ ℕ.n<1+n n ⟩ suc n - ≤.≡˘⟨ m+config-d≡j+n ⟩ + ≤.≡⟨ m+config-d≡j+n ⟨ Fin.toℕ (fnoc (sucs n) config d) ≤.∎ ))) refl ⟩ @@ -241,15 +241,15 @@ preserves-⊆ {D = D} {A = A} (sucs n) (d ⟨ cs ⟩) config = NCC.⟦ (d , Fin.opposite (Fin.fromℕ< m≤n)) ⟨ shrinkTo2 (sucs n) c ∷ go n d cs m (<-trans (ℕ.n<1+n m) m≤n) cs' ∷ [] ⟩ ⟧ config ≡⟨ Eq.cong₂ NCC.⟦_⟧ (Eq.cong₂ Vec.lookup {x = shrinkTo2 (sucs n) c ∷ go n d cs m (<-trans (ℕ.n<1+n m) m≤n) cs' ∷ []} refl (FnocLemmas.config≡0 config (Fin.opposite (Fin.fromℕ< {suc m} m≤n)) (Fin.toℕ-injective ( Fin.toℕ (fnoc (sucs n) config d) - ≡˘⟨ ℕ.m+n∸m≡n (suc m) (Fin.toℕ (fnoc (sucs n) config d)) ⟩ + ≡⟨ ℕ.m+n∸m≡n (suc m) (Fin.toℕ (fnoc (sucs n) config d)) ⟨ suc m + Fin.toℕ (fnoc (sucs n) config d) ∸ suc m ≡⟨ Eq.cong (λ n → n ∸ suc m) m+config-d≡j+n ⟩ n ∸ suc m - ≡˘⟨ Eq.cong₂ _∸_ refl (Fin.toℕ-fromℕ< m≤n) ⟩ + ≡⟨ Eq.cong₂ _∸_ {x = n} refl (Fin.toℕ-fromℕ< m≤n) ⟨ n ∸ (Fin.toℕ (Fin.fromℕ< m≤n)) - ≡˘⟨ Fin.opposite-prop (Fin.fromℕ< m≤n) ⟩ + ≡⟨ Fin.opposite-prop (Fin.fromℕ< m≤n) ⟨ Fin.toℕ (Fin.opposite (Fin.fromℕ< m≤n)) - ≡˘⟨ Fin.toℕ-inject₁ (Fin.opposite (Fin.fromℕ< m≤n)) ⟩ + ≡⟨ Fin.toℕ-inject₁ (Fin.opposite (Fin.fromℕ< m≤n)) ⟨ Fin.toℕ (Fin.inject₁ (Fin.opposite (Fin.fromℕ< m≤n))) ∎ )))) refl ⟩ @@ -271,11 +271,11 @@ preserves-⊆ {D = D} {A = A} (sucs n) (d ⟨ cs ⟩) config = n ∸ suc m ≤.<⟨ ℕ.m≤n⇒m≤o+n (Fin.toℕ j) (ℕ.m∸n≢0⇒nn⇒m∸n≢0 (ℕ.n∸1+mn⇒m∸n≢0 (ℕ.n∸1+m Date: Wed, 17 Apr 2024 18:59:21 +0200 Subject: [PATCH 08/13] nix: Filter untracked file Untracked files shouldn't influence the build. Hence, it's a good idea to ensure that they can't. --- default.nix | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/default.nix b/default.nix index 6af76f86..f17ed226 100644 --- a/default.nix +++ b/default.nix @@ -11,7 +11,11 @@ pkgs.agdaPackages.mkDerivation { version = "1.0"; pname = "EPVL"; - src = ./.; + src = with pkgs.lib.fileset; + toSource { + root = ./.; + fileset = gitTracked ./.; + }; buildInputs = [ pkgs.agdaPackages.standard-library From 9cbebf7e26da3c62cc90de51585ee9b689e9b192 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Wed, 17 Apr 2024 19:01:35 +0200 Subject: [PATCH 09/13] nix: Allow usage in `agda.withPackages` This also installs all Agda and Agda interface files instead of, like before, only keeping the executable. --- default.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/default.nix b/default.nix index f17ed226..110540d2 100644 --- a/default.nix +++ b/default.nix @@ -27,7 +27,7 @@ pkgs.agdaPackages.mkDerivation { make build ''; - installPhase = '' + postInstall = '' install -D src/Main "$out/bin/$pname" ''; From e9cbc03effbf256fc96086209f2412289c2b6749 Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Wed, 17 Apr 2024 19:43:08 +0200 Subject: [PATCH 10/13] nix: Create a flake.nix file This is currently an experimental Nix feature. However, it's already widely used so it makes sense to offer such a standardized interface. --- flake.nix | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 flake.nix diff --git a/flake.nix b/flake.nix new file mode 100644 index 00000000..ed1b58ff --- /dev/null +++ b/flake.nix @@ -0,0 +1,12 @@ +{ + outputs = inputs: let + EVPL = import inputs.self {system = "x86_64-linux";}; + in { + packages.x86_64-linux.default = EVPL; + overlays.default = final: prev: { + agdaPackages = prev.agdaPackages.overrideScope' (self: super: { + inherit EVPL; + }); + }; + }; +} From 35c2ab1ac9f99b5cc05c349afe67a1f3820877de Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Fri, 19 Apr 2024 18:31:52 +0200 Subject: [PATCH 11/13] Factor out common Agda options The only exception is `--allow-unsolved-metas` because it's useful to know where unsolved problems might hide. --- EPVL.agda-lib | 3 ++- src/Construct/GrulerArtifacts.agda | 2 -- src/Construct/NestedChoice.agda | 3 --- src/Data/IndexedSet.lagda.md | 2 -- src/Framework/Variants.agda | 2 -- src/Lang/2CC.lagda.md | 2 -- src/Lang/ADT.agda | 2 -- src/Lang/ADT/Path.agda | 2 -- src/Lang/All.agda | 2 -- src/Lang/All/Generic.agda | 2 -- src/Lang/CCC.lagda.md | 9 --------- src/Lang/FST.agda | 1 - src/Lang/Gruler.agda | 3 --- src/Lang/NADT.agda | 3 --- src/Lang/NCC.lagda.md | 2 -- src/Lang/OC.lagda.md | 2 -- src/Lang/VariantList.lagda.md | 4 ---- src/Main.agda | 2 +- src/Show/Eval.agda | 2 -- src/Test/Examples/CCC.agda | 1 - src/Test/Examples/OC.agda | 2 -- src/Test/Examples/Variants.agda | 2 -- src/Test/Experiments/CCC-to-2CC.agda | 2 -- src/Test/Experiments/FST-Experiments.agda | 1 - src/Test/Experiments/OC-to-2CC.agda | 2 -- src/Test/Experiments/RoundTrip.agda | 2 -- src/Test/Test/VariantList-Completeness.agda | 1 - src/Test/UnitTest.agda | 2 -- src/Translation/Construct/Choice-to-2Choice.agda | 1 - src/Translation/Construct/NestedChoice-to-2Choice.agda | 1 - .../Experiments/Choice-to-2Choice-Experiment.agda | 2 -- src/Translation/Lang/2CC-to-ADT.agda | 2 -- src/Translation/Lang/2CC-to-NCC.agda | 2 -- src/Translation/Lang/2CC/Rename.agda | 2 -- src/Translation/Lang/ADT-to-2CC.agda | 2 -- src/Translation/Lang/ADT-to-NADT.agda | 2 -- src/Translation/Lang/ADT/Rename.agda | 2 -- src/Translation/Lang/CCC-to-NCC.agda | 2 -- src/Translation/Lang/FST-to-OC.agda | 2 -- src/Translation/Lang/NADT-to-CCC.agda | 2 -- src/Translation/Lang/NCC-to-2CC.agda | 2 -- src/Translation/Lang/NCC-to-CCC.agda | 2 -- src/Translation/Lang/NCC/Grow.agda | 2 -- src/Translation/Lang/NCC/NCC-to-NCC.agda | 2 -- src/Translation/Lang/NCC/Rename.agda | 2 -- src/Translation/Lang/NCC/ShrinkTo2.agda | 2 -- src/Translation/Lang/OC-to-2CC.lagda.md | 2 -- src/Translation/Lang/Transitive/2CC-to-CCC.agda | 2 -- src/Translation/Lang/Transitive/CCC-to-2CC.agda | 2 -- src/Translation/Lang/VariantList-to-CCC.lagda.md | 6 ------ src/Translation/LanguageMap.lagda.md | 6 ------ src/Util/Existence.agda | 2 -- src/Util/List.agda | 2 -- src/Util/SizeJuggle.agda | 2 -- src/Util/Suffix.agda | 2 -- 55 files changed, 3 insertions(+), 122 deletions(-) diff --git a/EPVL.agda-lib b/EPVL.agda-lib index 0e6ba9a3..7c0e6583 100644 --- a/EPVL.agda-lib +++ b/EPVL.agda-lib @@ -1,3 +1,4 @@ name: EPVL depend: standard-library-2.0 -include: src \ No newline at end of file +include: src +flags: --large-indices --no-forced-argument-recursion --sized-types diff --git a/src/Construct/GrulerArtifacts.agda b/src/Construct/GrulerArtifacts.agda index 278bc26c..69da3955 100644 --- a/src/Construct/GrulerArtifacts.agda +++ b/src/Construct/GrulerArtifacts.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - module Construct.GrulerArtifacts where open import Data.Maybe using (just; nothing) diff --git a/src/Construct/NestedChoice.agda b/src/Construct/NestedChoice.agda index 1e03cb6e..bac0f0a7 100644 --- a/src/Construct/NestedChoice.agda +++ b/src/Construct/NestedChoice.agda @@ -1,6 +1,3 @@ -{-# OPTIONS --sized-types #-} -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} - open import Framework.Definitions module Construct.NestedChoice (F : 𝔽) where diff --git a/src/Data/IndexedSet.lagda.md b/src/Data/IndexedSet.lagda.md index 09902d55..f3e2500a 100644 --- a/src/Data/IndexedSet.lagda.md +++ b/src/Data/IndexedSet.lagda.md @@ -3,8 +3,6 @@ ## Module ```agda -{-# OPTIONS --allow-unsolved-metas #-} - open import Level using (Level; suc; _⊔_) open import Relation.Binary as RB using ( Rel; diff --git a/src/Framework/Variants.agda b/src/Framework/Variants.agda index 872cef4b..385390cf 100644 --- a/src/Framework/Variants.agda +++ b/src/Framework/Variants.agda @@ -1,6 +1,4 @@ -{-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} module Framework.Variants where diff --git a/src/Lang/2CC.lagda.md b/src/Lang/2CC.lagda.md index 1cbe0fea..aa24d81a 100644 --- a/src/Lang/2CC.lagda.md +++ b/src/Lang/2CC.lagda.md @@ -3,9 +3,7 @@ ## Options ```agda -{-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} ``` ## Module diff --git a/src/Lang/ADT.agda b/src/Lang/ADT.agda index a625a1b3..86c69f1f 100644 --- a/src/Lang/ADT.agda +++ b/src/Lang/ADT.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} - open import Framework.Definitions module Lang.ADT where diff --git a/src/Lang/ADT/Path.agda b/src/Lang/ADT/Path.agda index 4a5debe0..d22aad6f 100644 --- a/src/Lang/ADT/Path.agda +++ b/src/Lang/ADT/Path.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} - open import Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼) open import Relation.Binary using (DecidableEquality; Rel) module Lang.ADT.Path diff --git a/src/Lang/All.agda b/src/Lang/All.agda index 8479c23d..33bae471 100644 --- a/src/Lang/All.agda +++ b/src/Lang/All.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - module Lang.All where open import Size using (∞) diff --git a/src/Lang/All/Generic.agda b/src/Lang/All/Generic.agda index 930d8e56..c7beb0ec 100644 --- a/src/Lang/All/Generic.agda +++ b/src/Lang/All/Generic.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Definitions using (𝕍) open import Framework.Construct using (_∈ₛ_) open import Construct.Artifact using () renaming (Syntax to Artifact) diff --git a/src/Lang/CCC.lagda.md b/src/Lang/CCC.lagda.md index 6f027e00..65ef2310 100644 --- a/src/Lang/CCC.lagda.md +++ b/src/Lang/CCC.lagda.md @@ -1,14 +1,5 @@ # Core Choice Calculus -## Options - -For termination checking, we have to use sized types (i.e., types that are bounded by a certain size). -We use sizes to constrain the maximum tree-depth of an expression. -```agda -{-# OPTIONS --sized-types #-} -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} -``` - ## Module ```agda diff --git a/src/Lang/FST.agda b/src/Lang/FST.agda index d8474e99..300f0bbc 100644 --- a/src/Lang/FST.agda +++ b/src/Lang/FST.agda @@ -1,5 +1,4 @@ {-# OPTIONS --allow-unsolved-metas #-} -{-# OPTIONS --sized-types #-} open import Framework.Definitions diff --git a/src/Lang/Gruler.agda b/src/Lang/Gruler.agda index 59eb1839..dcbdc67b 100644 --- a/src/Lang/Gruler.agda +++ b/src/Lang/Gruler.agda @@ -1,6 +1,3 @@ -{-# OPTIONS --sized-types #-} -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} - open import Framework.Definitions module Lang.Gruler (F : 𝔽) where diff --git a/src/Lang/NADT.agda b/src/Lang/NADT.agda index 295c26f0..e30c84f0 100644 --- a/src/Lang/NADT.agda +++ b/src/Lang/NADT.agda @@ -1,6 +1,3 @@ -{-# OPTIONS --sized-types #-} -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} - open import Framework.Definitions module Lang.NADT where diff --git a/src/Lang/NCC.lagda.md b/src/Lang/NCC.lagda.md index 744b4605..657e0471 100644 --- a/src/Lang/NCC.lagda.md +++ b/src/Lang/NCC.lagda.md @@ -3,9 +3,7 @@ ## Options ```agda -{-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} ``` ## Module diff --git a/src/Lang/OC.lagda.md b/src/Lang/OC.lagda.md index aaec966e..29313f8c 100644 --- a/src/Lang/OC.lagda.md +++ b/src/Lang/OC.lagda.md @@ -3,9 +3,7 @@ ## Options ```agda -{-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} ``` ## Module diff --git a/src/Lang/VariantList.lagda.md b/src/Lang/VariantList.lagda.md index 8bf7cb20..9a07af3d 100644 --- a/src/Lang/VariantList.lagda.md +++ b/src/Lang/VariantList.lagda.md @@ -1,7 +1,3 @@ -```agda -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} -``` - # Lists of Variants are Also Variability Languages ## Module diff --git a/src/Main.agda b/src/Main.agda index 93d8ba79..46ae4ca5 100644 --- a/src/Main.agda +++ b/src/Main.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --sized-types --guardedness --allow-unsolved-metas #-} +{-# OPTIONS --guardedness --allow-unsolved-metas #-} module Main where diff --git a/src/Show/Eval.agda b/src/Show/Eval.agda index 784b83b6..740369bc 100644 --- a/src/Show/Eval.agda +++ b/src/Show/Eval.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - module Show.Eval where open import Data.Bool using (Bool) diff --git a/src/Test/Examples/CCC.agda b/src/Test/Examples/CCC.agda index 5e68323c..8480c1b5 100644 --- a/src/Test/Examples/CCC.agda +++ b/src/Test/Examples/CCC.agda @@ -1,4 +1,3 @@ -{-# OPTIONS --sized-types #-} module Test.Examples.CCC where open import Data.String as String using (String) diff --git a/src/Test/Examples/OC.agda b/src/Test/Examples/OC.agda index 52cf71a0..c724ad3c 100644 --- a/src/Test/Examples/OC.agda +++ b/src/Test/Examples/OC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - module Test.Examples.OC where open import Data.List using (List; []; _∷_; [_]) diff --git a/src/Test/Examples/Variants.agda b/src/Test/Examples/Variants.agda index 34b848fa..8149a455 100644 --- a/src/Test/Examples/Variants.agda +++ b/src/Test/Examples/Variants.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - module Test.Examples.Variants where open import Data.Fin using (zero; suc) diff --git a/src/Test/Experiments/CCC-to-2CC.agda b/src/Test/Experiments/CCC-to-2CC.agda index 9e689123..99542ebf 100644 --- a/src/Test/Experiments/CCC-to-2CC.agda +++ b/src/Test/Experiments/CCC-to-2CC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - module Test.Experiments.CCC-to-2CC where open import Data.Bool diff --git a/src/Test/Experiments/FST-Experiments.agda b/src/Test/Experiments/FST-Experiments.agda index 673173ae..aaae9d19 100644 --- a/src/Test/Experiments/FST-Experiments.agda +++ b/src/Test/Experiments/FST-Experiments.agda @@ -1,5 +1,4 @@ {-# OPTIONS --allow-unsolved-metas #-} -{-# OPTIONS --sized-types #-} open import Framework.Definitions module Test.Experiments.FST-Experiments where diff --git a/src/Test/Experiments/OC-to-2CC.agda b/src/Test/Experiments/OC-to-2CC.agda index 781089cb..26adf87c 100644 --- a/src/Test/Experiments/OC-to-2CC.agda +++ b/src/Test/Experiments/OC-to-2CC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - module Test.Experiments.OC-to-2CC where open import Data.Bool using (Bool; true; false) diff --git a/src/Test/Experiments/RoundTrip.agda b/src/Test/Experiments/RoundTrip.agda index 1d686614..9e2ba1bf 100644 --- a/src/Test/Experiments/RoundTrip.agda +++ b/src/Test/Experiments/RoundTrip.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - module Test.Experiments.RoundTrip where open import Data.Bool using (Bool; true; false) diff --git a/src/Test/Test/VariantList-Completeness.agda b/src/Test/Test/VariantList-Completeness.agda index fb7d5d54..d3322a51 100644 --- a/src/Test/Test/VariantList-Completeness.agda +++ b/src/Test/Test/VariantList-Completeness.agda @@ -1,4 +1,3 @@ -{-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} module Test.Test.VariantList-Completeness where diff --git a/src/Test/UnitTest.agda b/src/Test/UnitTest.agda index 842f5eef..07cb4733 100644 --- a/src/Test/UnitTest.agda +++ b/src/Test/UnitTest.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - module Test.UnitTest where open import Data.List using (List) diff --git a/src/Translation/Construct/Choice-to-2Choice.agda b/src/Translation/Construct/Choice-to-2Choice.agda index 3e63e509..1d1c407a 100644 --- a/src/Translation/Construct/Choice-to-2Choice.agda +++ b/src/Translation/Construct/Choice-to-2Choice.agda @@ -1,4 +1,3 @@ -{-# OPTIONS --sized-types #-} module Translation.Construct.Choice-to-2Choice {Q : Set} where open import Data.Bool using (Bool; false; true) renaming (_≟_ to _≟ᵇ_) diff --git a/src/Translation/Construct/NestedChoice-to-2Choice.agda b/src/Translation/Construct/NestedChoice-to-2Choice.agda index 5ae4433b..07e56117 100644 --- a/src/Translation/Construct/NestedChoice-to-2Choice.agda +++ b/src/Translation/Construct/NestedChoice-to-2Choice.agda @@ -1,4 +1,3 @@ -{-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} module Translation.Construct.NestedChoice-to-2Choice where diff --git a/src/Translation/Experiments/Choice-to-2Choice-Experiment.agda b/src/Translation/Experiments/Choice-to-2Choice-Experiment.agda index f1c6d1a3..bfd9e450 100644 --- a/src/Translation/Experiments/Choice-to-2Choice-Experiment.agda +++ b/src/Translation/Experiments/Choice-to-2Choice-Experiment.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Definitions module Translation.Experiments.Choice-to-2Choice-Experiment where diff --git a/src/Translation/Lang/2CC-to-ADT.agda b/src/Translation/Lang/2CC-to-ADT.agda index 7a64bec5..6940f1b5 100644 --- a/src/Translation/Lang/2CC-to-ADT.agda +++ b/src/Translation/Lang/2CC-to-ADT.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Construct using (_∈ₛ_; cons) open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms) open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/2CC-to-NCC.agda b/src/Translation/Lang/2CC-to-NCC.agda index 9be6b868..561e8433 100644 --- a/src/Translation/Lang/2CC-to-NCC.agda +++ b/src/Translation/Lang/2CC-to-NCC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Construct using (_∈ₛ_; cons) open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms) open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/2CC/Rename.agda b/src/Translation/Lang/2CC/Rename.agda index 422a5d1c..2d97d612 100644 --- a/src/Translation/Lang/2CC/Rename.agda +++ b/src/Translation/Lang/2CC/Rename.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Definitions using (𝕍; atoms) open import Framework.Construct using (_∈ₛ_; cons) open import Construct.Artifact using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/ADT-to-2CC.agda b/src/Translation/Lang/ADT-to-2CC.agda index 1c29c271..4b30284b 100644 --- a/src/Translation/Lang/ADT-to-2CC.agda +++ b/src/Translation/Lang/ADT-to-2CC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Construct using (_∈ₛ_; cons) open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms) open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/ADT-to-NADT.agda b/src/Translation/Lang/ADT-to-NADT.agda index 0ede2dee..bc5274b0 100644 --- a/src/Translation/Lang/ADT-to-NADT.agda +++ b/src/Translation/Lang/ADT-to-NADT.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Definitions open import Framework.Construct using (_∈ₛ_; cons) diff --git a/src/Translation/Lang/ADT/Rename.agda b/src/Translation/Lang/ADT/Rename.agda index 6e476447..eec81ccf 100644 --- a/src/Translation/Lang/ADT/Rename.agda +++ b/src/Translation/Lang/ADT/Rename.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Definitions using (𝕍; atoms) open import Framework.Construct using (_∈ₛ_; cons) open import Construct.Artifact using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/CCC-to-NCC.agda b/src/Translation/Lang/CCC-to-NCC.agda index 9a1309ec..aa4e8518 100644 --- a/src/Translation/Lang/CCC-to-NCC.agda +++ b/src/Translation/Lang/CCC-to-NCC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Construct using (_∈ₛ_; cons) open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms) open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/FST-to-OC.agda b/src/Translation/Lang/FST-to-OC.agda index 0ed1cf40..7e77e072 100644 --- a/src/Translation/Lang/FST-to-OC.agda +++ b/src/Translation/Lang/FST-to-OC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Definitions module Translation.Lang.FST-to-OC (F : 𝔽) where diff --git a/src/Translation/Lang/NADT-to-CCC.agda b/src/Translation/Lang/NADT-to-CCC.agda index 778ee0af..6aac7cd3 100644 --- a/src/Translation/Lang/NADT-to-CCC.agda +++ b/src/Translation/Lang/NADT-to-CCC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Construct using (_∈ₛ_) open import Framework.Definitions open import Construct.Artifact using () renaming (Syntax to Artifact) diff --git a/src/Translation/Lang/NCC-to-2CC.agda b/src/Translation/Lang/NCC-to-2CC.agda index 86c85da4..acab8086 100644 --- a/src/Translation/Lang/NCC-to-2CC.agda +++ b/src/Translation/Lang/NCC-to-2CC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Construct using (_∈ₛ_; cons) open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms) open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/NCC-to-CCC.agda b/src/Translation/Lang/NCC-to-CCC.agda index 72cbb828..e93bd43e 100644 --- a/src/Translation/Lang/NCC-to-CCC.agda +++ b/src/Translation/Lang/NCC-to-CCC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Construct using (_∈ₛ_; cons) open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms) open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/NCC/Grow.agda b/src/Translation/Lang/NCC/Grow.agda index 5c395bc4..179c8c26 100644 --- a/src/Translation/Lang/NCC/Grow.agda +++ b/src/Translation/Lang/NCC/Grow.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Definitions using (𝕍; atoms) open import Framework.Construct using (_∈ₛ_; cons) open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/NCC/NCC-to-NCC.agda b/src/Translation/Lang/NCC/NCC-to-NCC.agda index e23d1fe2..202eefb2 100644 --- a/src/Translation/Lang/NCC/NCC-to-NCC.agda +++ b/src/Translation/Lang/NCC/NCC-to-NCC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Definitions using (𝕍) open import Framework.Construct using (_∈ₛ_; cons) open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/NCC/Rename.agda b/src/Translation/Lang/NCC/Rename.agda index de4c97c3..4af73cd1 100644 --- a/src/Translation/Lang/NCC/Rename.agda +++ b/src/Translation/Lang/NCC/Rename.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Definitions using (𝕍; atoms) open import Framework.Construct using (_∈ₛ_; cons) open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/NCC/ShrinkTo2.agda b/src/Translation/Lang/NCC/ShrinkTo2.agda index e2f1c1cb..f7502140 100644 --- a/src/Translation/Lang/NCC/ShrinkTo2.agda +++ b/src/Translation/Lang/NCC/ShrinkTo2.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Definitions using (𝕍; atoms) open import Framework.Construct using (_∈ₛ_; cons) open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor) diff --git a/src/Translation/Lang/OC-to-2CC.lagda.md b/src/Translation/Lang/OC-to-2CC.lagda.md index 4597fc15..b1f80617 100644 --- a/src/Translation/Lang/OC-to-2CC.lagda.md +++ b/src/Translation/Lang/OC-to-2CC.lagda.md @@ -3,9 +3,7 @@ ## Options ```agda -{-# OPTIONS --sized-types #-} {-# OPTIONS --allow-unsolved-metas #-} -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} ``` ## Module diff --git a/src/Translation/Lang/Transitive/2CC-to-CCC.agda b/src/Translation/Lang/Transitive/2CC-to-CCC.agda index dd82afc2..7a2dca96 100644 --- a/src/Translation/Lang/Transitive/2CC-to-CCC.agda +++ b/src/Translation/Lang/Transitive/2CC-to-CCC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Construct using (_∈ₛ_) open import Framework.Definitions using (𝔽; 𝕍) open import Construct.Artifact using () renaming (Syntax to Artifact) diff --git a/src/Translation/Lang/Transitive/CCC-to-2CC.agda b/src/Translation/Lang/Transitive/CCC-to-2CC.agda index be053153..67821832 100644 --- a/src/Translation/Lang/Transitive/CCC-to-2CC.agda +++ b/src/Translation/Lang/Transitive/CCC-to-2CC.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - open import Framework.Construct using (_∈ₛ_) open import Framework.Definitions using (𝔽; 𝕍) open import Construct.Artifact as At using () renaming (Syntax to Artifact) diff --git a/src/Translation/Lang/VariantList-to-CCC.lagda.md b/src/Translation/Lang/VariantList-to-CCC.lagda.md index fa6ba6f8..73f96544 100644 --- a/src/Translation/Lang/VariantList-to-CCC.lagda.md +++ b/src/Translation/Lang/VariantList-to-CCC.lagda.md @@ -1,11 +1,5 @@ # Encoding Lists of Variants in Core Choice Calculus -## Options - -```agda -{-# OPTIONS --sized-types #-} -``` - ## Module ```agda diff --git a/src/Translation/LanguageMap.lagda.md b/src/Translation/LanguageMap.lagda.md index 47a7da80..1a1ea7d3 100644 --- a/src/Translation/LanguageMap.lagda.md +++ b/src/Translation/LanguageMap.lagda.md @@ -1,11 +1,5 @@ # Overview of Language Relations -## Options - -```agda -{-# OPTIONS --sized-types #-} -``` - ## Module ```agda diff --git a/src/Util/Existence.agda b/src/Util/Existence.agda index b6513078..df886144 100644 --- a/src/Util/Existence.agda +++ b/src/Util/Existence.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - module Util.Existence where open import Agda.Primitive using (Level; _⊔_) diff --git a/src/Util/List.agda b/src/Util/List.agda index c5ddfdb0..8c9efae2 100644 --- a/src/Util/List.agda +++ b/src/Util/List.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --allow-unsolved-metas #-} - {-| Utilities for lists. -} diff --git a/src/Util/SizeJuggle.agda b/src/Util/SizeJuggle.agda index 2ea0f9df..936a355f 100644 --- a/src/Util/SizeJuggle.agda +++ b/src/Util/SizeJuggle.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --sized-types #-} - {- Module with functions for assisting Agda's type checker when it comes to checking sized types. diff --git a/src/Util/Suffix.agda b/src/Util/Suffix.agda index b8208ed8..956d2e08 100644 --- a/src/Util/Suffix.agda +++ b/src/Util/Suffix.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --large-indices --no-forced-argument-recursion #-} - module Util.Suffix where open import Data.Empty using (⊥-elim) From f4240f55bd811f0fedad4cd6b8ef6cb2f55b6f2a Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Fri, 19 Apr 2024 19:03:27 +0200 Subject: [PATCH 12/13] nix: Don't introduce our own nixpkgs in the nixpkgs overlay --- flake.nix | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/flake.nix b/flake.nix index ed1b58ff..afe8f7fb 100644 --- a/flake.nix +++ b/flake.nix @@ -1,11 +1,12 @@ { - outputs = inputs: let - EVPL = import inputs.self {system = "x86_64-linux";}; - in { - packages.x86_64-linux.default = EVPL; + outputs = inputs: { + packages.x86_64-linux.default = import inputs.self {system = "x86_64-linux";}; overlays.default = final: prev: { agdaPackages = prev.agdaPackages.overrideScope' (self: super: { - inherit EVPL; + (import inputs.self { + system = "x86_64-linux"; + pkgs = final; + };) }); }; }; From 0acd639f174646edc3161163184b625cad57522b Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Fri, 19 Apr 2024 19:05:13 +0200 Subject: [PATCH 13/13] Provide an example for how to use `agda.withPackages` --- README.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/README.md b/README.md index 309c4edd..99c609ff 100644 --- a/README.md +++ b/README.md @@ -26,6 +26,17 @@ nix-build ./result/bin/EPVL ``` +To use this repository as a library in you own project, you can use `agda.withPackages`: +```nix +agda = nixpkgs.agda.withPackages [ + nixpkgs.agdaPackages.standard-library + (import /path/to/this/git/repository { + pkgs = nixpkgs; + }) +]; +``` +Though, not required, we recommend to use the [nixpkgs pin](nix/sources.json) created using [niv](https://github.com/nmattia/niv) provided in this respository to minimize version conflicts. + #### Manual Installation We recommend following the installation instructions from the [Programming Language Foundations in Agda](https://plfa.github.io/GettingStarted/) book to install GHC, Cabal, and Agda (no need to install the book and the standard-library, which is shipped in the right version in the subdirectory `agda-stdlib` here).