From 9dbb2c5a56bd833262c1a946d56ecce8523b040c Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Mon, 20 Jan 2025 16:50:07 +0100 Subject: [PATCH 1/6] Permutations and Renaming --- src/Scope/Diff.agda | 5 ++++ src/Scope/Renaming.agda | 51 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 56 insertions(+) create mode 100644 src/Scope/Renaming.agda diff --git a/src/Scope/Diff.agda b/src/Scope/Diff.agda index 2b0e9be..f2e43f9 100644 --- a/src/Scope/Diff.agda +++ b/src/Scope/Diff.agda @@ -19,6 +19,11 @@ opaque @0 diff : ∀ {α β : Scope name} → α ⊆ β → Scope name diff (⟨ p ⟩ _) = p + @0 diffVar : ∀ {α : Scope name} → x ∈ α → Scope name + diffVar xp = diff (inToSub xp) + + syntax diffVar {α = α} xp = α \[ xp ] + diff-left : (p : α ⋈ β ≡ γ) → diff (subLeft p) ≡ β diff-left p = refl diff --git a/src/Scope/Renaming.agda b/src/Scope/Renaming.agda new file mode 100644 index 0000000..de83b6f --- /dev/null +++ b/src/Scope/Renaming.agda @@ -0,0 +1,51 @@ +module Scope.Renaming where + +open import Haskell.Prelude hiding (coerce) + +-- open import Haskell.Extra.Dec +open import Haskell.Extra.Erase +open import Haskell.Extra.Refinement +-- open import Haskell.Law.Equality + +open import Scope.Core +open import Scope.Split +open import Scope.Sub +open import Scope.In +open import Scope.Diff + + +private variable + @0 name : Set + @0 α β : Scope name + +NameIn : (@0 α : Scope name) → Set +NameIn α = Σ0 _ λ x → x ∈ α +{-# COMPILE AGDA2HS NameIn inline #-} + +data Permutation {@0 name : Set} : (α β : Scope name) → Set where + PNil : Permutation mempty mempty + PCons : + ((⟨ x ⟩ xp) : NameIn α) + → Permutation (α \[ xp ]) β + → Permutation α (x ◃ β) + +pattern ⌈⌉ = PNil +infix 6 ⌈_◃_⌉ +pattern ⌈_◃_⌉ x σ = PCons x σ +infix 4 ⌈_◃⌉ +pattern ⌈_◃⌉ x = ⌈ x ◃ ⌈⌉ ⌉ + +Renaming : Scope name → Scope name → Set +Renaming α β = NameIn α → NameIn β + +opaque + unfolding Scope diff + + permutationToRenaming : ∀ {@0 α β : Scope name} → Permutation α β → Renaming α β + permutationToRenaming ⌈⌉ = id + permutationToRenaming ⌈ xVar ◃ p ⌉ yVar = + let ⟨ _ ⟩ xp = xVar in + let ⟨ _ ⟩ yp = yVar in + diffCase (inToSub xp) yp + (λ _ → < Zero ⟨ IsZero refl ⟩ >) + (λ yp' → let ⟨ _ ⟩ res = permutationToRenaming p < yp' > in < inThere res >) \ No newline at end of file From 8668539bc6072f4e7bb9b50abe32572084dfe712 Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Tue, 21 Jan 2025 09:56:14 +0100 Subject: [PATCH 2/6] agda2HS annotations modified: src/Scope/Renaming.agda modified: src/Scope.agda modified: src/Scope/Renaming.agda modified: src/Scope.agda Date: Tue Jan 21 09:56:14 2025 +0100 Changes to be committed: modified: src/Scope.agda modified: src/Scope/Renaming.agda Untracked files: result Changes to be committed: modified: src/Scope.agda modified: src/Scope/Renaming.agda --- src/Scope.agda | 1 + src/Scope/Renaming.agda | 40 ++++++++++++++++++++-------------------- 2 files changed, 21 insertions(+), 20 deletions(-) diff --git a/src/Scope.agda b/src/Scope.agda index cf5d12f..294e52c 100644 --- a/src/Scope.agda +++ b/src/Scope.agda @@ -7,6 +7,7 @@ open import Scope.Sub public open import Scope.In public open import Scope.Cut public open import Scope.Diff public +open import Scope.Renaming public open import Scope.All public opaque diff --git a/src/Scope/Renaming.agda b/src/Scope/Renaming.agda index de83b6f..c4be75b 100644 --- a/src/Scope/Renaming.agda +++ b/src/Scope/Renaming.agda @@ -2,14 +2,10 @@ module Scope.Renaming where open import Haskell.Prelude hiding (coerce) --- open import Haskell.Extra.Dec open import Haskell.Extra.Erase open import Haskell.Extra.Refinement --- open import Haskell.Law.Equality open import Scope.Core -open import Scope.Split -open import Scope.Sub open import Scope.In open import Scope.Diff @@ -22,12 +18,14 @@ NameIn : (@0 α : Scope name) → Set NameIn α = Σ0 _ λ x → x ∈ α {-# COMPILE AGDA2HS NameIn inline #-} -data Permutation {@0 name : Set} : (α β : Scope name) → Set where - PNil : Permutation mempty mempty - PCons : - ((⟨ x ⟩ xp) : NameIn α) - → Permutation (α \[ xp ]) β - → Permutation α (x ◃ β) +data Permutation {@0 name : Set} : (@0 α β : Scope name) → Set where + PNil : Permutation mempty mempty + PCons : + ((⟨ x ⟩ xp) : NameIn α) + → Permutation (α \[ xp ]) β + → Permutation α (x ◃ β) +{-# COMPILE AGDA2HS Permutation deriving Show #-} + pattern ⌈⌉ = PNil infix 6 ⌈_◃_⌉ @@ -37,15 +35,17 @@ pattern ⌈_◃⌉ x = ⌈ x ◃ ⌈⌉ ⌉ Renaming : Scope name → Scope name → Set Renaming α β = NameIn α → NameIn β +{-# COMPILE AGDA2HS Renaming inline #-} opaque - unfolding Scope diff - - permutationToRenaming : ∀ {@0 α β : Scope name} → Permutation α β → Renaming α β - permutationToRenaming ⌈⌉ = id - permutationToRenaming ⌈ xVar ◃ p ⌉ yVar = - let ⟨ _ ⟩ xp = xVar in - let ⟨ _ ⟩ yp = yVar in - diffCase (inToSub xp) yp - (λ _ → < Zero ⟨ IsZero refl ⟩ >) - (λ yp' → let ⟨ _ ⟩ res = permutationToRenaming p < yp' > in < inThere res >) \ No newline at end of file + unfolding Scope diff + + permutationToRenaming : ∀ {@0 α β : Scope name} → Permutation α β → Renaming α β + permutationToRenaming ⌈⌉ = id + permutationToRenaming ⌈ xVar ◃ p ⌉ yVar = + let ⟨ _ ⟩ xp = xVar in + let ⟨ _ ⟩ yp = yVar in + diffCase (inToSub xp) yp + (λ _ → < Zero ⟨ IsZero refl ⟩ >) + (λ yp' → let ⟨ _ ⟩ res = permutationToRenaming p < yp' > in < inThere res >) + {-# COMPILE AGDA2HS permutationToRenaming #-} \ No newline at end of file From 7fa752b79f91b7f66b030a821268d72f7de739f1 Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Tue, 21 Jan 2025 13:08:32 +0100 Subject: [PATCH 3/6] =?UTF-8?q?Permutation=20indexed=20on=20=CE=B1=20inste?= =?UTF-8?q?ad=20of=20=CE=B2=20to=20be=20similar=20to=20Subst?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Changes to be committed: modified: src/Scope/Renaming.agda Changes to be committed: modified: src/Scope/Renaming.agda Changes to be ignored: modified: src/Scope/Diff.agda --- src/Scope/Renaming.agda | 38 +++++++++++++++++++++++++++----------- 1 file changed, 27 insertions(+), 11 deletions(-) diff --git a/src/Scope/Renaming.agda b/src/Scope/Renaming.agda index c4be75b..d5364d4 100644 --- a/src/Scope/Renaming.agda +++ b/src/Scope/Renaming.agda @@ -9,7 +9,6 @@ open import Scope.Core open import Scope.In open import Scope.Diff - private variable @0 name : Set @0 α β : Scope name @@ -18,14 +17,24 @@ NameIn : (@0 α : Scope name) → Set NameIn α = Σ0 _ λ x → x ∈ α {-# COMPILE AGDA2HS NameIn inline #-} + data Permutation {@0 name : Set} : (@0 α β : Scope name) → Set where PNil : Permutation mempty mempty PCons : - ((⟨ x ⟩ xp) : NameIn α) - → Permutation (α \[ xp ]) β - → Permutation α (x ◃ β) + ((⟨ x ⟩ xp) : NameIn β) + → Permutation α (β \[ xp ]) + → Permutation (x ◃ α) β {-# COMPILE AGDA2HS Permutation deriving Show #-} +{- +data PermutationOld {@0 name : Set} : (@0 α β : Scope name) → Set where + PNil : PermutationOld mempty mempty + PCons : + ((⟨ x ⟩ xp) : NameIn α) + → PermutationOld (α \[ xp ]) β + → PermutationOld α (x ◃ β) +{-# COMPILE AGDA2HS PermutationOld deriving Show #-} +-} pattern ⌈⌉ = PNil infix 6 ⌈_◃_⌉ @@ -38,14 +47,21 @@ Renaming α β = NameIn α → NameIn β {-# COMPILE AGDA2HS Renaming inline #-} opaque - unfolding Scope diff - + unfolding Scope permutationToRenaming : ∀ {@0 α β : Scope name} → Permutation α β → Renaming α β permutationToRenaming ⌈⌉ = id - permutationToRenaming ⌈ xVar ◃ p ⌉ yVar = - let ⟨ _ ⟩ xp = xVar in - let ⟨ _ ⟩ yp = yVar in + permutationToRenaming ⌈ xVar ◃ _ ⌉ (⟨ _ ⟩ (Zero ⟨ IsZero refl ⟩)) = xVar + permutationToRenaming ⌈ ⟨ _ ⟩ xp ◃ p ⌉ (⟨ _ ⟩ (Suc n ⟨ IsSuc np ⟩)) = + let ⟨ _ ⟩ res = permutationToRenaming p < n ⟨ np ⟩ > in + < coerce (diffSub (inToSub xp)) res > + {-# COMPILE AGDA2HS permutationToRenaming #-} + +opaque + unfolding diff + permutationToRenamingRev : ∀ {@0 α β : Scope name} → Permutation α β → Renaming β α + permutationToRenamingRev ⌈⌉ = id + permutationToRenamingRev ⌈ ⟨ _ ⟩ xp ◃ p ⌉ (⟨ _ ⟩ yp) = diffCase (inToSub xp) yp (λ _ → < Zero ⟨ IsZero refl ⟩ >) - (λ yp' → let ⟨ _ ⟩ res = permutationToRenaming p < yp' > in < inThere res >) - {-# COMPILE AGDA2HS permutationToRenaming #-} \ No newline at end of file + (λ yp' → let ⟨ _ ⟩ res = permutationToRenamingRev p < yp' > in < inThere res >) + {-# COMPILE AGDA2HS permutationToRenamingRev #-} \ No newline at end of file From ba368741873662cefbd6dd8aa6dc943ab55da3e5 Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Tue, 21 Jan 2025 13:15:34 +0100 Subject: [PATCH 4/6] fix typo --- src/Scope/Renaming.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Scope/Renaming.agda b/src/Scope/Renaming.agda index d5364d4..16ba9c4 100644 --- a/src/Scope/Renaming.agda +++ b/src/Scope/Renaming.agda @@ -47,7 +47,7 @@ Renaming α β = NameIn α → NameIn β {-# COMPILE AGDA2HS Renaming inline #-} opaque - unfolding Scope + unfolding Scope diff permutationToRenaming : ∀ {@0 α β : Scope name} → Permutation α β → Renaming α β permutationToRenaming ⌈⌉ = id permutationToRenaming ⌈ xVar ◃ _ ⌉ (⟨ _ ⟩ (Zero ⟨ IsZero refl ⟩)) = xVar From 9b5002af3ffd0ed410d609fc5770d059c15b74f5 Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Tue, 21 Jan 2025 13:20:53 +0100 Subject: [PATCH 5/6] removed inline in subRight definition as it caused a bug --- src/Scope/Sub.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Scope/Sub.agda b/src/Scope/Sub.agda index 4fcf2d8..8b80ad9 100644 --- a/src/Scope/Sub.agda +++ b/src/Scope/Sub.agda @@ -30,7 +30,7 @@ opaque subRight : α ⋈ β ≡ γ → β ⊆ γ subRight p = < splitComm p > - {-# COMPILE AGDA2HS subRight inline #-} + {-# COMPILE AGDA2HS subRight #-} subWeaken : α ⊆ β → α ⊆ (bind x β) subWeaken < p > = < splitBindRight p > From d8b99a9ef79b02666210c3ec38f9657a311d8a3a Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Wed, 22 Jan 2025 16:22:10 +0100 Subject: [PATCH 6/6] erase non essential datatypes --- src/Scope/Diff.agda | 15 ++++++--- src/Scope/In.agda | 1 + src/Scope/Renaming.agda | 72 ++++++++++++++++++++++------------------- 3 files changed, 49 insertions(+), 39 deletions(-) diff --git a/src/Scope/Diff.agda b/src/Scope/Diff.agda index f2e43f9..5d900ae 100644 --- a/src/Scope/Diff.agda +++ b/src/Scope/Diff.agda @@ -19,11 +19,6 @@ opaque @0 diff : ∀ {α β : Scope name} → α ⊆ β → Scope name diff (⟨ p ⟩ _) = p - @0 diffVar : ∀ {α : Scope name} → x ∈ α → Scope name - diffVar xp = diff (inToSub xp) - - syntax diffVar {α = α} xp = α \[ xp ] - diff-left : (p : α ⋈ β ≡ γ) → diff (subLeft p) ≡ β diff-left p = refl @@ -43,6 +38,16 @@ opaque diffCase p = inSplitCase (splitDiff p) {-# COMPILE AGDA2HS diffCase inline #-} +@0 diffVar : ∀ {α : Scope name} → x ∈ α → Scope name +diffVar xp = diff (inToSub xp) + +infix 10 diffVar +syntax diffVar {α = α} xp = α \[ xp ] + +diffVarCase : (xp : x ∈ α) → (yp : y ∈ α) + → (@0 x ≡ y → a) → (x ∈ α \[ yp ] → a) → a +diffVarCase xp yp ce cd = diffCase (inToSub yp) xp (λ p → inSingCase p ce) cd + opaque unfolding diff diff --git a/src/Scope/In.agda b/src/Scope/In.agda index a7573d4..c7b0673 100644 --- a/src/Scope/In.agda +++ b/src/Scope/In.agda @@ -32,6 +32,7 @@ In : @0 name → @0 Scope name → Set In x α = ∃ Index (λ n → IsNth x α n) {-# COMPILE AGDA2HS In inline #-} +infix 6 In syntax In x α = x ∈ α inToSub : x ∈ α → [ x ] ⊆ α diff --git a/src/Scope/Renaming.agda b/src/Scope/Renaming.agda index 16ba9c4..5b40d27 100644 --- a/src/Scope/Renaming.agda +++ b/src/Scope/Renaming.agda @@ -4,8 +4,10 @@ open import Haskell.Prelude hiding (coerce) open import Haskell.Extra.Erase open import Haskell.Extra.Refinement +open import Haskell.Law.Equality open import Scope.Core +open import Scope.Sub open import Scope.In open import Scope.Diff @@ -13,55 +15,57 @@ private variable @0 name : Set @0 α β : Scope name -NameIn : (@0 α : Scope name) → Set -NameIn α = Σ0 _ λ x → x ∈ α -{-# COMPILE AGDA2HS NameIn inline #-} - - +{- data Permutation {@0 name : Set} : (@0 α β : Scope name) → Set where PNil : Permutation mempty mempty - PCons : - ((⟨ x ⟩ xp) : NameIn β) + PCons : {@0 x : name} + (xp : x ∈ β) → Permutation α (β \[ xp ]) → Permutation (x ◃ α) β {-# COMPILE AGDA2HS Permutation deriving Show #-} -{- -data PermutationOld {@0 name : Set} : (@0 α β : Scope name) → Set where - PNil : PermutationOld mempty mempty - PCons : - ((⟨ x ⟩ xp) : NameIn α) - → PermutationOld (α \[ xp ]) β - → PermutationOld α (x ◃ β) -{-# COMPILE AGDA2HS PermutationOld deriving Show #-} --} - pattern ⌈⌉ = PNil -infix 6 ⌈_◃_⌉ -pattern ⌈_◃_⌉ x σ = PCons x σ -infix 4 ⌈_◃⌉ -pattern ⌈_◃⌉ x = ⌈ x ◃ ⌈⌉ ⌉ +infix 6 ⌈_~>_◃_⌉ +pattern ⌈_~>_◃_⌉ x xp σ = PCons {x = x} xp σ +infix 4 ⌈_~>_◃⌉ +pattern ⌈_~>_◃⌉ x xp = ⌈ x ~> xp ◃ ⌈⌉ ⌉ +-} -Renaming : Scope name → Scope name → Set -Renaming α β = NameIn α → NameIn β +Renaming : (@0 α β : Scope name) → Set +Renaming {name = name} α β = {@0 x : name} → x ∈ α → x ∈ β {-# COMPILE AGDA2HS Renaming inline #-} opaque - unfolding Scope diff + unfolding Scope + @0 RenamingInEmpty : ∀ {@0 α : Scope name} → Renaming α mempty → α ≡ mempty + RenamingInEmpty {α = []} r = refl + RenamingInEmpty {α = x ∷ α} r = inEmptyCase (r inHere) + +{- +opaque + unfolding Scope permutationToRenaming : ∀ {@0 α β : Scope name} → Permutation α β → Renaming α β permutationToRenaming ⌈⌉ = id - permutationToRenaming ⌈ xVar ◃ _ ⌉ (⟨ _ ⟩ (Zero ⟨ IsZero refl ⟩)) = xVar - permutationToRenaming ⌈ ⟨ _ ⟩ xp ◃ p ⌉ (⟨ _ ⟩ (Suc n ⟨ IsSuc np ⟩)) = - let ⟨ _ ⟩ res = permutationToRenaming p < n ⟨ np ⟩ > in - < coerce (diffSub (inToSub xp)) res > + permutationToRenaming ⌈ x ~> xp ◃ _ ⌉ (Zero ⟨ IsZero refl ⟩) = xp + permutationToRenaming ⌈ x ~> xp ◃ p ⌉ (Suc n ⟨ IsSuc np ⟩) = + let res = permutationToRenaming p (n ⟨ np ⟩) in + (coerce (diffSub (inToSub xp)) res) {-# COMPILE AGDA2HS permutationToRenaming #-} opaque - unfolding diff permutationToRenamingRev : ∀ {@0 α β : Scope name} → Permutation α β → Renaming β α permutationToRenamingRev ⌈⌉ = id - permutationToRenamingRev ⌈ ⟨ _ ⟩ xp ◃ p ⌉ (⟨ _ ⟩ yp) = - diffCase (inToSub xp) yp - (λ _ → < Zero ⟨ IsZero refl ⟩ >) - (λ yp' → let ⟨ _ ⟩ res = permutationToRenamingRev p < yp' > in < inThere res >) - {-# COMPILE AGDA2HS permutationToRenamingRev #-} \ No newline at end of file + permutationToRenamingRev ⌈ x ~> xp ◃ p ⌉ yp = + diffVarCase yp xp + (λ refl → Zero ⟨ IsZero refl ⟩ ) + (λ yp' → let res = permutationToRenamingRev p yp' in (inThere res)) + {-# COMPILE AGDA2HS permutationToRenamingRev #-} + +opaque + unfolding Scope diff + idPerm : Rezz α → Permutation α α + idPerm (rezz []) = ⌈⌉ + idPerm (rezz (Erased x ∷ α)) = ⌈ x ~> Zero ⟨ IsZero refl ⟩ ◃ idPerm (rezz α) ⌉ + {-# COMPILE AGDA2HS idPerm inline #-} + +-}