From 372809bd0e3625fcf71415d3cecc7512d2f3e4ca Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Fri, 4 Apr 2025 10:51:04 +0200 Subject: [PATCH 1/5] adding let in context --- src/Agda/Core/Context.agda | 27 +++++++------ src/Agda/Core/Name.agda | 8 ++-- src/Agda/Core/Typechecker.agda | 2 +- src/Agda/Core/Typing.agda | 2 +- src/Agda/Core/Unification.agda | 11 ++++-- src/Agda/Core/Unifier.agda | 70 +++++++++++++++++++--------------- 6 files changed, 67 insertions(+), 53 deletions(-) diff --git a/src/Agda/Core/Context.agda b/src/Agda/Core/Context.agda index c0f34fe..c46441b 100644 --- a/src/Agda/Core/Context.agda +++ b/src/Agda/Core/Context.agda @@ -11,7 +11,6 @@ open import Haskell.Prelude hiding (All; s; t) open import Agda.Core.Name open import Agda.Core.GlobalScope using (Globals) open import Agda.Core.Syntax -open import Agda.Core.Signature module Agda.Core.Context {{@0 globals : Globals}} @@ -26,32 +25,36 @@ private variable data Context : @0 Scope Name → Set where CtxEmpty : Context mempty CtxExtend : Context α → (@0 x : Name) → Type α → Context (α ▸ x) - + CtxExtendLet : Context α → (@0 x : Name) → Term α → Type α → Context (α ▸ x) {-# COMPILE AGDA2HS Context #-} -_,_∶_ : Context α → (@0 x : Name) → Type α → Context (α ▸ x) -_,_∶_ = CtxExtend - -infix 4 _,_∶_ +pattern ⌈⌉ = CtxEmpty +pattern _,_∶_ g x ty = CtxExtend g x ty +pattern _,_≔_∶_ g x u ty = CtxExtendLet g x u ty -{-# COMPILE AGDA2HS _,_∶_ inline #-} +infixl 4 _,_∶_ +infixl 4 _,_≔_∶_ private variable @0 Γ : Context α lookupVar : (Γ : Context α) (x : NameIn α) → Type α -lookupVar CtxEmpty x = nameInEmptyCase x -lookupVar (CtxExtend g y s) x = raiseType (rezz _) (nameInBindCase x +lookupVar ⌈⌉ x = nameInEmptyCase x +lookupVar (g , y ∶ s) x = raiseType (rezz _) (nameInBindCase x + (λ q → lookupVar g (⟨ _ ⟩ q)) + (λ _ → s)) +lookupVar (g , y ≔ u ∶ s) x = raiseType (rezz _) (nameInBindCase x (λ q → lookupVar g (⟨ _ ⟩ q)) (λ _ → s)) {-# COMPILE AGDA2HS lookupVar #-} rezzScope : (Γ : Context α) → Rezz α -rezzScope CtxEmpty = rezz _ -rezzScope (CtxExtend g x _) = +rezzScope ⌈⌉ = rezz _ +rezzScope (g , x ∶ _) = + rezzCong (λ t → t <> (singleton x)) (rezzScope g) +rezzScope (g , x ≔ _ ∶ _) = rezzCong (λ t → t <> (singleton x)) (rezzScope g) - {-# COMPILE AGDA2HS rezzScope #-} addContextTel : Context α → Telescope α rβ → Context (extScope α rβ) diff --git a/src/Agda/Core/Name.agda b/src/Agda/Core/Name.agda index a9d90e5..faffbb0 100644 --- a/src/Agda/Core/Name.agda +++ b/src/Agda/Core/Name.agda @@ -97,8 +97,8 @@ instance } ------------------------------------------------------------------------------- -pattern Vsuc n p = ⟨ _ ⟩ (Suc n ⟨ IsSuc p ⟩) -pattern V2suc n p = ⟨ _ ⟩ (Suc (Suc n) ⟨ IsSuc (IsSuc p) ⟩) -pattern Vzero = ⟨ _ ⟩ Zero ⟨ IsZero refl ⟩ -pattern Vone = ⟨ _ ⟩ (Suc Zero) ⟨ IsSuc (IsZero refl) ⟩ +pattern Vsuc x n p = ⟨ x ⟩ (Suc n ⟨ IsSuc p ⟩) +pattern V2suc x n p = ⟨ x ⟩ (Suc (Suc n) ⟨ IsSuc (IsSuc p) ⟩) +pattern Vzero x = ⟨ x ⟩ Zero ⟨ IsZero refl ⟩ +pattern Vone x = ⟨ x ⟩ (Suc Zero) ⟨ IsSuc (IsZero refl) ⟩ ------------------------------------------------------------------------------- diff --git a/src/Agda/Core/Typechecker.agda b/src/Agda/Core/Typechecker.agda index 433a978..cc24593 100644 --- a/src/Agda/Core/Typechecker.agda +++ b/src/Agda/Core/Typechecker.agda @@ -261,7 +261,7 @@ checkLet : ∀ Γ (@0 x : Name) → TCM (Γ ⊢ TLet x u v ∶ ty) checkLet ctx x u v ty = do tu , dtu ← inferType ctx u - dtv ← checkType (ctx , x ∶ tu) v (weaken (subBindDrop subRefl) ty) + dtv ← checkType (ctx , x ≔ u ∶ tu) v (weaken (subBindDrop subRefl) ty) return $ TyLet dtu dtv {-# COMPILE AGDA2HS checkLet #-} diff --git a/src/Agda/Core/Typing.agda b/src/Agda/Core/Typing.agda index cb32c24..c124d11 100644 --- a/src/Agda/Core/Typing.agda +++ b/src/Agda/Core/Typing.agda @@ -166,7 +166,7 @@ data TyTerm {α} Γ where TyLet : Γ ⊢ u ∶ a - → Γ , x ∶ a ⊢ v ∶ weakenType (subBindDrop subRefl) b + → Γ , x ≔ u ∶ a ⊢ v ∶ weakenType (subBindDrop subRefl) b ---------------------------------------------- → Γ ⊢ TLet x u v ∶ b diff --git a/src/Agda/Core/Unification.agda b/src/Agda/Core/Unification.agda index 91e374e..6871f75 100644 --- a/src/Agda/Core/Unification.agda +++ b/src/Agda/Core/Unification.agda @@ -60,10 +60,13 @@ module Shrinking where opaque unfolding Scope shrinkContext : Context α → ShrinkSubst α β → Context β - shrinkContext CtxEmpty RNil = CtxEmpty - shrinkContext (CtxExtend Γ x a) (RKeep σ) = - CtxExtend (shrinkContext Γ σ) x (subst (ShrinkSubstToSubst σ) a) - shrinkContext (CtxExtend Γ x a) (RCons u σ) = shrinkContext Γ σ + shrinkContext ⌈⌉ RNil = ⌈⌉ + shrinkContext (Γ , x ∶ a) (RKeep σ) = + shrinkContext Γ σ , x ∶ subst (ShrinkSubstToSubst σ) a + shrinkContext (Γ , x ≔ u ∶ a) (RKeep σ) = + shrinkContext Γ σ , x ≔ subst (ShrinkSubstToSubst σ) u ∶ subst (ShrinkSubstToSubst σ) a + shrinkContext (Γ , _ ∶ _) (RCons u σ) = shrinkContext Γ σ + shrinkContext (Γ , _ ≔ _ ∶ _) (RCons u σ) = shrinkContext Γ σ opaque unfolding cut diff --git a/src/Agda/Core/Unifier.agda b/src/Agda/Core/Unifier.agda index 5106480..eeb51b7 100644 --- a/src/Agda/Core/Unifier.agda +++ b/src/Agda/Core/Unifier.agda @@ -65,10 +65,26 @@ module Swap where opaque unfolding Scope swapTwoLast : Context (α ▸ x ▸ y) → Maybe (Context (α ▸ y ▸ x)) - swapTwoLast (CtxExtend (CtxExtend Γ y ay) x ax) = do + swapTwoLast (Γ , y ∶ ay , x ∶ ax) = do ax' ← strengthen (subBindDrop subRefl) ax let ay' = weaken (subBindDrop subRefl) ay - return ((Γ , x ∶ ax' ) , y ∶ ay') + return (Γ , x ∶ ax' , y ∶ ay') + swapTwoLast (Γ , y ≔ v ∶ ay , x ≔ u ∶ ax) = do + ax' ← strengthen (subBindDrop subRefl) ax + u' ← strengthen (subBindDrop subRefl) u + let ay' = weaken (subBindDrop subRefl) ay + v' = weaken (subBindDrop subRefl) v + return (Γ , x ≔ u' ∶ ax' , y ≔ v' ∶ ay') + swapTwoLast (Γ , y ∶ ay , x ≔ u ∶ ax) = do + ax' ← strengthen (subBindDrop subRefl) ax + u' ← strengthen (subBindDrop subRefl) u + let ay' = weaken (subBindDrop subRefl) ay + return (Γ , x ≔ u' ∶ ax' , y ∶ ay') + swapTwoLast (Γ , y ≔ v ∶ ay , x ∶ ax) = do + ax' ← strengthen (subBindDrop subRefl) ax + let ay' = weaken (subBindDrop subRefl) ay + v' = weaken (subBindDrop subRefl) v + return (Γ , x ∶ ax' , y ≔ v' ∶ ay') {- Idea of swapHighest (x, z, Γ) y: @@ -82,15 +98,13 @@ module Swap where used in recursive calls is decreasing.) -} swapHighest : {{fl : Index}} → Context (α ▸ x) → ((⟨ y ⟩ yp) : NameIn α) → Maybe (Σ0 _ λ α' → Context α' × Renaming (α ▸ x) α') - swapHighest (CtxExtend (CtxExtend Γ0 y ay) x ax) (⟨ y ⟩ (Zero ⟨ IsZero refl ⟩)) = do - Γ' ← swapTwoLast (CtxExtend (CtxExtend Γ0 y ay) x ax) + swapHighest {α = Erased y ∷ α} {x = x} Γ (Vzero y) = do + Γ' ← swapTwoLast Γ let σ : Renaming (α ▸ y ▸ x) (α ▸ x ▸ y) - σ = renamingExtend (renamingExtend (renamingWeaken (rezz (_ ∷ _ ∷ [])) id) inHere) (inThere inHere) + σ = renamingExtend (renamingExtend (renamingWeaken (rezz ([] ▸ x ▸ y)) id) inHere) (inThere inHere) return < Γ' , σ > - swapHighest {α = Erased z ∷ α} {x = x} {{Suc fl}} (CtxExtend (CtxExtend Γ0 z az) x ax) (⟨ y ⟩ (Suc value ⟨ IsSuc proof ⟩)) = - let Γ : Context (α ▸ z ▸ x) - Γ = (CtxExtend (CtxExtend Γ0 z az) x ax) - yInα : y ∈ α + swapHighest {α = Erased z ∷ α} {x = x} {{Suc fl}} Γ@(CtxExtend (CtxExtend Γ0 z az) x ax) (Vsuc y value proof) = + let yInα : y ∈ α yInα = value ⟨ proof ⟩ in let areTheTwoLastVarsSwapable = do (CtxExtend Γ₁ .z az') ← swapTwoLast Γ @@ -119,34 +133,28 @@ module Swap where swapHighest {{Zero}} (CtxExtend (CtxExtend _ _ _) _ _) (⟨ _ ⟩ (Suc _ ⟨ _ ⟩)) = Nothing -- this shouldn't happens as at all times fl ≥ position of y in the scope swap : Context α → (x y : NameIn α) → Either SwapError (Maybe (Σ0 _ λ α' → Context α' × Renaming α α')) - swap _ Vzero Vzero = Left CantSwapVarWithItSelf - swap Γ Vzero (Vsuc value proof) = do + swap _ (Vzero _) (Vzero _) = Left CantSwapVarWithItSelf + swap Γ (Vzero _) (Vsuc _ value proof) = do Right (swapHighest {{value}} Γ < (value ⟨ proof ⟩) >) - swap _ (Vsuc _ _) Vzero = Left VarInWrongOrder - swap _ Vone Vone = Left CantSwapVarWithItSelf - swap _ (V2suc _ _) Vone = Left VarInWrongOrder - swap (CtxExtend Γ z az) (Vsuc vx px) (V2suc vy py) = do - Just (⟨ α₀' ⟩ (Γ0' , σ₀)) ← swap Γ (⟨ _ ⟩ (vx ⟨ px ⟩)) (⟨ _ ⟩ ((Suc vy) ⟨ IsSuc py ⟩)) + swap _ (Vsuc _ _ _) (Vzero _) = Left VarInWrongOrder + swap _ (Vone _) (Vone _) = Left CantSwapVarWithItSelf + swap _ (V2suc _ _ _) (Vone _) = Left VarInWrongOrder + swap (Γ , z ∶ az) (Vsuc x vx px) (V2suc y vy py) = do + Just (⟨ α₀' ⟩ (Γ0' , σ₀)) ← swap Γ (⟨ x ⟩ (vx ⟨ px ⟩)) (⟨ y ⟩ ((Suc vy) ⟨ IsSuc py ⟩)) + where Nothing → Right Nothing + -- σ₀ : Renaming _ α₀' + let τ₀ = renamingToSubst (rezzScope Γ) σ₀ + σ : Renaming (_ ▸ z) (α₀' ▸ z) + σ = renamingExtend (renamingWeakenVar σ₀) inHere + Right (Just < Γ0' , z ∶ (subst τ₀ az), σ >) + swap (Γ , z ≔ u ∶ az) (Vsuc x vx px) (V2suc y vy py) = do + Just (⟨ α₀' ⟩ (Γ0' , σ₀)) ← swap Γ (⟨ x ⟩ (vx ⟨ px ⟩)) (⟨ y ⟩ ((Suc vy) ⟨ IsSuc py ⟩)) where Nothing → Right Nothing -- σ₀ : Renaming _ α₀' let τ₀ = renamingToSubst (rezzScope Γ) σ₀ σ : Renaming (_ ▸ z) (α₀' ▸ z) σ = renamingExtend (renamingWeakenVar σ₀) inHere - Right (Just < CtxExtend Γ0' z (subst τ₀ az), σ >) - {- - swapVarListFuel2 : Context α → (x : NameIn α) → (l : List (NameIn α)) → (fl : Nat) → @0 {{lengthNat l ≡ fl}} → Maybe (Σ0 _ λ α' → Context α' × Renaming α α') - swapVarListFuel2 Γ (⟨ x ⟩ xp) ((⟨ y ⟩ yp) ∷ l) (suc fl) {{e}} = {! !} -- do - -- ⟨ _ ⟩ (Γ0' , σ₀) ← try_swap Γ (⟨ x ⟩ xp) (⟨ y ⟩ yp) - -- let e : lengthNat (map (λ z → < σ₀ (proj₂ z) >) l) ≡ fl - -- e = lengthMap ((λ z → < σ₀ (proj₂ z) >)) l - -- ⟨ _ ⟩ (Γ' , σ) ← swapVarListFuel2 fl Γ0' (⟨ x ⟩ σ₀ xp) (map (λ z → < σ₀ (proj₂ z) >) l) {{e}} - -- return < Γ' , σ ∘ σ₀ > - -- where try_swap : Context α → (x y : NameIn α) → Maybe (Σ0 _ λ α' → Context α' × Renaming α α') - -- try_swap Γ x y with (swap Γ x y) - -- ... | Left CantSwapVarWithItSelf = Nothing - -- ... | Left VarInWrongOrder = Just < Γ , id > - -- ... | Right val = val - swapVarListFuel2 Γ x [] zero = Just < Γ , id > -} + Right (Just < Γ0' , z ≔ (subst τ₀ u) ∶ (subst τ₀ az), σ >) swapVarListFuel : (fl : Nat) → Context α → (x : NameIn α) → (l : List (NameIn α)) → Maybe (Σ0 _ λ α' → Context α' × Renaming α α') swapVarListFuel (suc fl) Γ (⟨ x ⟩ xp) ((⟨ y ⟩ yp) ∷ l) = do From e9b434a6584624559cabc022bc60e1f705f24faf Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Fri, 4 Apr 2025 12:58:47 +0200 Subject: [PATCH 2/5] CtxView --- src/Agda/Core/Context.agda | 60 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) diff --git a/src/Agda/Core/Context.agda b/src/Agda/Core/Context.agda index c46441b..a9ca3aa 100644 --- a/src/Agda/Core/Context.agda +++ b/src/Agda/Core/Context.agda @@ -9,6 +9,7 @@ open import Haskell.Law.Monoid open import Haskell.Prelude hiding (All; s; t) open import Agda.Core.Name +open import Agda.Core.Utils open import Agda.Core.GlobalScope using (Globals) open import Agda.Core.Syntax @@ -63,3 +64,62 @@ addContextTel {α} c ⌈⌉ = addContextTel {α} c (ExtendTel {rβ = rβ} x ty telt) = subst0 Context (sym extScopeBind) (addContextTel (c , x ∶ ty) telt) {-# COMPILE AGDA2HS addContextTel #-} + +opaque + maybeLet : @0 Scope Name → Set + maybeLet α = (Maybe (Term α)) × Type α + {-# COMPILE AGDA2HS maybeLet inline #-} + + weakenMaybeLet : α ⊆ β → maybeLet α → maybeLet β + weakenMaybeLet s (Nothing , ty) = (Nothing , weaken s ty) + weakenMaybeLet s (Just u , ty) = (Just (weaken s u) , weaken s ty) + {-# COMPILE AGDA2HS weakenMaybeLet inline #-} + + instance + iWeakenMaybeLet : Weaken maybeLet + iWeakenMaybeLet .weaken = weakenMaybeLet + {-# COMPILE AGDA2HS iWeakenMaybeLet inline #-} + + strengthenMaybeLet : α ⊆ β → maybeLet β → Maybe (maybeLet α) + strengthenMaybeLet s (Nothing , ty) with strengthenType s ty + ... | Nothing = Nothing + ... | Just ty' = Just (Nothing , ty') + strengthenMaybeLet s (Just u , ty) with strengthen s u | strengthen s ty + ... | Nothing | _ = Nothing + ... | Just _ | Nothing = Nothing + ... | Just u' | Just ty' = Just (Just u' , ty') + {-# COMPILE AGDA2HS strengthenMaybeLet inline #-} + + instance + iStrengthenMaybeLet : Strengthen maybeLet + iStrengthenMaybeLet .strengthen = strengthenMaybeLet + {-# COMPILE AGDA2HS iStrengthenMaybeLet inline #-} + +data CtxView : @0 Scope Name → Set where + CtxViewEmpty : CtxView mempty + CtxViewExtend : CtxView α → (@0 x : Name) → maybeLet α → CtxView (α ▸ x) + +private opaque + unfolding maybeLet + contextToCtxView : Context α → CtxView α + contextToCtxView ⌈⌉ = CtxViewEmpty + contextToCtxView (Γ , x ∶ ty) = CtxViewExtend (contextToCtxView Γ) x (Nothing , ty) + contextToCtxView (Γ , x ≔ u ∶ ty) = CtxViewExtend (contextToCtxView Γ) x (Just u , ty) + + ctxViewToContext : CtxView α → Context α + ctxViewToContext CtxViewEmpty = ⌈⌉ + ctxViewToContext (CtxViewExtend Γ x (Nothing , ty)) = ctxViewToContext Γ , x ∶ ty + ctxViewToContext (CtxViewExtend Γ x (Just u , ty)) = ctxViewToContext Γ , x ≔ u ∶ ty + + equivLeft : (Γ : Context α) → ctxViewToContext (contextToCtxView Γ) ≡ Γ + equivLeft ⌈⌉ = refl + equivLeft (Γ , x ∶ ty) = cong (λ Γ₀ → Γ₀ , x ∶ ty) (equivLeft Γ) + equivLeft (Γ , x ≔ u ∶ ty) = cong (λ Γ₀ → Γ₀ , x ≔ u ∶ ty) (equivLeft Γ) + + equivRight : (Γ : CtxView α) → contextToCtxView (ctxViewToContext Γ) ≡ Γ + equivRight CtxViewEmpty = refl + equivRight (CtxViewExtend Γ x (Nothing , ty)) = cong (λ Γ₀ → CtxViewExtend Γ₀ x (Nothing , ty)) (equivRight Γ) + equivRight (CtxViewExtend Γ x (Just u , ty)) = cong (λ Γ₀ → CtxViewExtend Γ₀ x (Just u , ty)) (equivRight Γ) + +equivalenceContext : Equivalence (Context α) (CtxView α) +equivalenceContext = Equiv contextToCtxView ctxViewToContext equivLeft equivRight From d55d62a55dcb2b550b47a0b20ad3e9839efdbc2e Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Fri, 4 Apr 2025 16:49:13 +0200 Subject: [PATCH 3/5] fix Unifier --- src/Agda/Core/Context.agda | 21 ++++++++++- src/Agda/Core/Unifier.agda | 71 ++++++++++++++++++-------------------- 2 files changed, 53 insertions(+), 39 deletions(-) diff --git a/src/Agda/Core/Context.agda b/src/Agda/Core/Context.agda index a9ca3aa..fcfcac0 100644 --- a/src/Agda/Core/Context.agda +++ b/src/Agda/Core/Context.agda @@ -4,7 +4,7 @@ open import Utils.Either open import Utils.Tactics using (auto) open import Haskell.Extra.Dec open import Haskell.Extra.Erase -open import Haskell.Law.Equality +open import Haskell.Law.Equality hiding (subst) open import Haskell.Law.Monoid open import Haskell.Prelude hiding (All; s; t) @@ -12,6 +12,7 @@ open import Agda.Core.Name open import Agda.Core.Utils open import Agda.Core.GlobalScope using (Globals) open import Agda.Core.Syntax +open import Agda.Core.Substitute module Agda.Core.Context {{@0 globals : Globals}} @@ -95,9 +96,21 @@ opaque iStrengthenMaybeLet .strengthen = strengthenMaybeLet {-# COMPILE AGDA2HS iStrengthenMaybeLet inline #-} + substMaybeLet : α ⇒ β → maybeLet α → maybeLet β + substMaybeLet s (Nothing , ty) = (Nothing , subst s ty) + substMaybeLet s (Just u , ty) = (Just (subst s u) , subst s ty) + {-# COMPILE AGDA2HS substMaybeLet inline #-} + + instance + iSubstMaybeLet : Substitute maybeLet + iSubstMaybeLet .subst = substMaybeLet + {-# COMPILE AGDA2HS iSubstMaybeLet inline #-} + + data CtxView : @0 Scope Name → Set where CtxViewEmpty : CtxView mempty CtxViewExtend : CtxView α → (@0 x : Name) → maybeLet α → CtxView (α ▸ x) +{-# COMPILE AGDA2HS CtxView #-} private opaque unfolding maybeLet @@ -123,3 +136,9 @@ private opaque equivalenceContext : Equivalence (Context α) (CtxView α) equivalenceContext = Equiv contextToCtxView ctxViewToContext equivLeft equivRight +{-# COMPILE AGDA2HS equivalenceContext #-} + +rezzScope' : (Γ : CtxView α) → Rezz α +rezzScope' CtxViewEmpty = rezz _ +rezzScope' (CtxViewExtend g x _) = rezzCong (λ t → t <> (singleton x)) (rezzScope' g) +{-# COMPILE AGDA2HS rezzScope' #-} diff --git a/src/Agda/Core/Unifier.agda b/src/Agda/Core/Unifier.agda index eeb51b7..3c009e0 100644 --- a/src/Agda/Core/Unifier.agda +++ b/src/Agda/Core/Unifier.agda @@ -64,28 +64,16 @@ module Swap where opaque unfolding Scope - swapTwoLast : Context (α ▸ x ▸ y) → Maybe (Context (α ▸ y ▸ x)) - swapTwoLast (Γ , y ∶ ay , x ∶ ax) = do - ax' ← strengthen (subBindDrop subRefl) ax - let ay' = weaken (subBindDrop subRefl) ay - return (Γ , x ∶ ax' , y ∶ ay') - swapTwoLast (Γ , y ≔ v ∶ ay , x ≔ u ∶ ax) = do - ax' ← strengthen (subBindDrop subRefl) ax - u' ← strengthen (subBindDrop subRefl) u - let ay' = weaken (subBindDrop subRefl) ay - v' = weaken (subBindDrop subRefl) v - return (Γ , x ≔ u' ∶ ax' , y ≔ v' ∶ ay') - swapTwoLast (Γ , y ∶ ay , x ≔ u ∶ ax) = do - ax' ← strengthen (subBindDrop subRefl) ax - u' ← strengthen (subBindDrop subRefl) u - let ay' = weaken (subBindDrop subRefl) ay - return (Γ , x ≔ u' ∶ ax' , y ∶ ay') - swapTwoLast (Γ , y ≔ v ∶ ay , x ∶ ax) = do - ax' ← strengthen (subBindDrop subRefl) ax - let ay' = weaken (subBindDrop subRefl) ay - v' = weaken (subBindDrop subRefl) v - return (Γ , x ∶ ax' , y ≔ v' ∶ ay') + swapTwoLast' : CtxView (α ▸ x ▸ y) → Maybe (CtxView (α ▸ y ▸ x)) + swapTwoLast' (CtxViewExtend (CtxViewExtend Γ x a) y b) = do + b' ← strengthenMaybeLet (subBindDrop subRefl) b + let a' = weaken (subBindDrop subRefl) a + return (CtxViewExtend (CtxViewExtend Γ y b') x a') + swapTwoLast : Context (α ▸ x ▸ y) → Maybe (Context (α ▸ y ▸ x)) + swapTwoLast Γ = do + res ← swapTwoLast' (σ equivalenceContext Γ) + return (τ equivalenceContext res) {- Idea of swapHighest (x, z, Γ) y: - terminaison condition : you swap x and y or fail @@ -96,41 +84,48 @@ module Swap where recursive call on (z, Γ) and return swapHighest (x, Γ') y (recursion terminates because the depth of y in the contexts used in recursive calls is decreasing.) -} - swapHighest : {{fl : Index}} → Context (α ▸ x) → ((⟨ y ⟩ yp) : NameIn α) - → Maybe (Σ0 _ λ α' → Context α' × Renaming (α ▸ x) α') - swapHighest {α = Erased y ∷ α} {x = x} Γ (Vzero y) = do - Γ' ← swapTwoLast Γ + swapHighest' : {{fl : Index}} → CtxView (α ▸ x) → ((⟨ y ⟩ yp) : NameIn α) + → Maybe (Σ0 _ λ α' → CtxView α' × Renaming (α ▸ x) α') + swapHighest' {α = Erased y ∷ α} {x = x} Γ (Vzero y) = do + Γ' ← swapTwoLast' Γ let σ : Renaming (α ▸ y ▸ x) (α ▸ x ▸ y) σ = renamingExtend (renamingExtend (renamingWeaken (rezz ([] ▸ x ▸ y)) id) inHere) (inThere inHere) return < Γ' , σ > - swapHighest {α = Erased z ∷ α} {x = x} {{Suc fl}} Γ@(CtxExtend (CtxExtend Γ0 z az) x ax) (Vsuc y value proof) = + swapHighest' {α = Erased z ∷ α} {x = x} {{Suc fl}} Γ@(CtxViewExtend (CtxViewExtend Γ0 z az) x ax) (Vsuc y value proof) = let yInα : y ∈ α yInα = value ⟨ proof ⟩ in let areTheTwoLastVarsSwapable = do - (CtxExtend Γ₁ .z az') ← swapTwoLast Γ - ⟨ α₀' ⟩ (Γ₀' , σ₀ ) ← swapHighest {{fl}} Γ₁ < yInα > + (CtxViewExtend Γ₁ .z az') ← swapTwoLast' Γ + ⟨ α₀' ⟩ (Γ₀' , σ₀ ) ← swapHighest' {{fl}} Γ₁ < yInα > -- σ₀ : Renaming (α ▸ x) α₀' let σ : Renaming (α ▸ z ▸ x) (α₀' ▸ z) σ = renamingExtend (renamingExtend ((renamingWeakenVar σ₀) ∘ inThere) inHere) (inThere (σ₀ inHere)) - az' : Type α₀' - az' = subst (renamingToSubst (rezzScope Γ₁) σ₀) (weaken (subBindDrop subRefl) az) - res1 : Σ0 _ λ α' → Context α' × Renaming (α ▸ z ▸ x) α' - res1 = < CtxExtend Γ₀' z az' , σ > + az' : maybeLet α₀' + az' = subst (renamingToSubst (rezzScope' Γ₁) σ₀) (weaken (subBindDrop subRefl) az) + res1 : Σ0 _ λ α' → CtxView α' × Renaming (α ▸ z ▸ x) α' + res1 = < CtxViewExtend Γ₀' z az' , σ > return res1 in let otherCase = do - ⟨ γ₀ ⟩ (Δ₀ , τ₀) ← swapHighest {{fl}} (CtxExtend Γ0 z az) < yInα > + ⟨ γ₀ ⟩ (Δ₀ , τ₀) ← swapHighest' {{fl}} (CtxViewExtend Γ0 z az) < yInα > -- τ₀ : Renaming (z ◃ α) γ₀ - let ax' : Type γ₀ - ax' = subst (renamingToSubst (rezzScope (CtxExtend Γ0 z az)) τ₀) ax + let ax' : maybeLet γ₀ + ax' = subst (renamingToSubst (rezzScope' (CtxViewExtend Γ0 z az)) τ₀) ax σ₁ : Renaming (α ▸ z ▸ x) (γ₀ ▸ x) σ₁ = renamingExtend (renamingWeakenVar τ₀) inHere - ⟨ α' ⟩ (Γ' , σ₂) ← swapHighest {{fl}} (CtxExtend Δ₀ x ax') < τ₀ (inThere yInα) > + ⟨ α' ⟩ (Γ' , σ₂) ← swapHighest' {{fl}} (CtxViewExtend Δ₀ x ax') < τ₀ (inThere yInα) > -- σ₂ : Renaming (x ◃ α₀') α' - let res2 : Σ0 _ λ α' → Context α' × Renaming (α ▸ z ▸ x) α' + let res2 : Σ0 _ λ α' → CtxView α' × Renaming (α ▸ z ▸ x) α' res2 = < Γ' , σ₂ ∘ σ₁ > return res2 in caseMaybe areTheTwoLastVarsSwapable (λ x → Just x) otherCase - swapHighest {{Zero}} (CtxExtend (CtxExtend _ _ _) _ _) (⟨ _ ⟩ (Suc _ ⟨ _ ⟩)) = Nothing -- this shouldn't happens as at all times fl ≥ position of y in the scope + swapHighest' {{Zero}} (CtxViewExtend (CtxViewExtend _ _ _) _ _) (⟨ _ ⟩ (Suc _ ⟨ _ ⟩)) = Nothing -- this shouldn't happens as at all times fl ≥ position of y in the scope + + + swapHighest : {{fl : Index}} → Context (α ▸ x) → ((⟨ y ⟩ yp) : NameIn α) + → Maybe (Σ0 _ λ α' → Context α' × Renaming (α ▸ x) α') + swapHighest {{fl = fl}} Γ v = do + ⟨ α' ⟩ (res , σ) ← swapHighest' {{ fl = fl }} (σ equivalenceContext Γ) v + return (⟨ α' ⟩ (τ equivalenceContext res , σ)) swap : Context α → (x y : NameIn α) → Either SwapError (Maybe (Σ0 _ λ α' → Context α' × Renaming α α')) swap _ (Vzero _) (Vzero _) = Left CantSwapVarWithItSelf From beb1da73fad26ebff3daaaef9a53e69ea0377c66 Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Mon, 7 Apr 2025 11:24:06 +0200 Subject: [PATCH 4/5] fix Haskell --- src/Agda/Core/Context.agda | 120 ++++++++++++++++++------------------- src/Agda/Core/Unifier.agda | 4 +- 2 files changed, 62 insertions(+), 62 deletions(-) diff --git a/src/Agda/Core/Context.agda b/src/Agda/Core/Context.agda index fcfcac0..b84f798 100644 --- a/src/Agda/Core/Context.agda +++ b/src/Agda/Core/Context.agda @@ -67,78 +67,78 @@ addContextTel {α} c (ExtendTel {rβ = rβ} x ty telt) = {-# COMPILE AGDA2HS addContextTel #-} opaque - maybeLet : @0 Scope Name → Set - maybeLet α = (Maybe (Term α)) × Type α - {-# COMPILE AGDA2HS maybeLet inline #-} + MaybeLet : @0 Scope Name → Set + MaybeLet α = (Maybe (Term α)) × Type α + {-# COMPILE AGDA2HS MaybeLet #-} - weakenMaybeLet : α ⊆ β → maybeLet α → maybeLet β + weakenMaybeLet : α ⊆ β → MaybeLet α → MaybeLet β weakenMaybeLet s (Nothing , ty) = (Nothing , weaken s ty) weakenMaybeLet s (Just u , ty) = (Just (weaken s u) , weaken s ty) - {-# COMPILE AGDA2HS weakenMaybeLet inline #-} + {-# COMPILE AGDA2HS weakenMaybeLet #-} instance - iWeakenMaybeLet : Weaken maybeLet + iWeakenMaybeLet : Weaken MaybeLet iWeakenMaybeLet .weaken = weakenMaybeLet - {-# COMPILE AGDA2HS iWeakenMaybeLet inline #-} - - strengthenMaybeLet : α ⊆ β → maybeLet β → Maybe (maybeLet α) - strengthenMaybeLet s (Nothing , ty) with strengthenType s ty - ... | Nothing = Nothing - ... | Just ty' = Just (Nothing , ty') - strengthenMaybeLet s (Just u , ty) with strengthen s u | strengthen s ty - ... | Nothing | _ = Nothing - ... | Just _ | Nothing = Nothing - ... | Just u' | Just ty' = Just (Just u' , ty') - {-# COMPILE AGDA2HS strengthenMaybeLet inline #-} + {-# COMPILE AGDA2HS iWeakenMaybeLet #-} + + strengthenMaybeLet : α ⊆ β → MaybeLet β → Maybe (MaybeLet α) + strengthenMaybeLet s (Nothing , ty) = do + ty' ← strengthenType s ty + return (Nothing , ty') + strengthenMaybeLet s (Just u , ty) = do + u' ← strengthen s u + ty' ← strengthen s ty + return (Just u' , ty') + {-# COMPILE AGDA2HS strengthenMaybeLet #-} instance - iStrengthenMaybeLet : Strengthen maybeLet + iStrengthenMaybeLet : Strengthen MaybeLet iStrengthenMaybeLet .strengthen = strengthenMaybeLet - {-# COMPILE AGDA2HS iStrengthenMaybeLet inline #-} + {-# COMPILE AGDA2HS iStrengthenMaybeLet #-} - substMaybeLet : α ⇒ β → maybeLet α → maybeLet β + substMaybeLet : α ⇒ β → MaybeLet α → MaybeLet β substMaybeLet s (Nothing , ty) = (Nothing , subst s ty) substMaybeLet s (Just u , ty) = (Just (subst s u) , subst s ty) - {-# COMPILE AGDA2HS substMaybeLet inline #-} + {-# COMPILE AGDA2HS substMaybeLet #-} instance - iSubstMaybeLet : Substitute maybeLet + iSubstMaybeLet : Substitute MaybeLet iSubstMaybeLet .subst = substMaybeLet - {-# COMPILE AGDA2HS iSubstMaybeLet inline #-} - - -data CtxView : @0 Scope Name → Set where - CtxViewEmpty : CtxView mempty - CtxViewExtend : CtxView α → (@0 x : Name) → maybeLet α → CtxView (α ▸ x) -{-# COMPILE AGDA2HS CtxView #-} - -private opaque - unfolding maybeLet - contextToCtxView : Context α → CtxView α - contextToCtxView ⌈⌉ = CtxViewEmpty - contextToCtxView (Γ , x ∶ ty) = CtxViewExtend (contextToCtxView Γ) x (Nothing , ty) - contextToCtxView (Γ , x ≔ u ∶ ty) = CtxViewExtend (contextToCtxView Γ) x (Just u , ty) - - ctxViewToContext : CtxView α → Context α - ctxViewToContext CtxViewEmpty = ⌈⌉ - ctxViewToContext (CtxViewExtend Γ x (Nothing , ty)) = ctxViewToContext Γ , x ∶ ty - ctxViewToContext (CtxViewExtend Γ x (Just u , ty)) = ctxViewToContext Γ , x ≔ u ∶ ty - - equivLeft : (Γ : Context α) → ctxViewToContext (contextToCtxView Γ) ≡ Γ - equivLeft ⌈⌉ = refl - equivLeft (Γ , x ∶ ty) = cong (λ Γ₀ → Γ₀ , x ∶ ty) (equivLeft Γ) - equivLeft (Γ , x ≔ u ∶ ty) = cong (λ Γ₀ → Γ₀ , x ≔ u ∶ ty) (equivLeft Γ) - - equivRight : (Γ : CtxView α) → contextToCtxView (ctxViewToContext Γ) ≡ Γ - equivRight CtxViewEmpty = refl - equivRight (CtxViewExtend Γ x (Nothing , ty)) = cong (λ Γ₀ → CtxViewExtend Γ₀ x (Nothing , ty)) (equivRight Γ) - equivRight (CtxViewExtend Γ x (Just u , ty)) = cong (λ Γ₀ → CtxViewExtend Γ₀ x (Just u , ty)) (equivRight Γ) - -equivalenceContext : Equivalence (Context α) (CtxView α) -equivalenceContext = Equiv contextToCtxView ctxViewToContext equivLeft equivRight -{-# COMPILE AGDA2HS equivalenceContext #-} - -rezzScope' : (Γ : CtxView α) → Rezz α -rezzScope' CtxViewEmpty = rezz _ -rezzScope' (CtxViewExtend g x _) = rezzCong (λ t → t <> (singleton x)) (rezzScope' g) -{-# COMPILE AGDA2HS rezzScope' #-} + {-# COMPILE AGDA2HS iSubstMaybeLet #-} + + +-- data CtxView : @0 Scope Name → Set where +-- CtxViewEmpty : CtxView mempty +-- CtxViewExtend : CtxView α → (@0 x : Name) → MaybeLet α → CtxView (α ▸ x) +-- {-# COMPILE AGDA2HS CtxView #-} + +-- private opaque +-- unfolding MaybeLet +-- contextToCtxView : Context α → CtxView α +-- contextToCtxView ⌈⌉ = CtxViewEmpty +-- contextToCtxView (Γ , x ∶ ty) = CtxViewExtend (contextToCtxView Γ) x (Nothing , ty) +-- contextToCtxView (Γ , x ≔ u ∶ ty) = CtxViewExtend (contextToCtxView Γ) x (Just u , ty) + +-- ctxViewToContext : CtxView α → Context α +-- ctxViewToContext CtxViewEmpty = ⌈⌉ +-- ctxViewToContext (CtxViewExtend Γ x (Nothing , ty)) = ctxViewToContext Γ , x ∶ ty +-- ctxViewToContext (CtxViewExtend Γ x (Just u , ty)) = ctxViewToContext Γ , x ≔ u ∶ ty + +-- equivLeft : (Γ : Context α) → ctxViewToContext (contextToCtxView Γ) ≡ Γ +-- equivLeft ⌈⌉ = refl +-- equivLeft (Γ , x ∶ ty) = cong (λ Γ₀ → Γ₀ , x ∶ ty) (equivLeft Γ) +-- equivLeft (Γ , x ≔ u ∶ ty) = cong (λ Γ₀ → Γ₀ , x ≔ u ∶ ty) (equivLeft Γ) + +-- equivRight : (Γ : CtxView α) → contextToCtxView (ctxViewToContext Γ) ≡ Γ +-- equivRight CtxViewEmpty = refl +-- equivRight (CtxViewExtend Γ x (Nothing , ty)) = cong (λ Γ₀ → CtxViewExtend Γ₀ x (Nothing , ty)) (equivRight Γ) +-- equivRight (CtxViewExtend Γ x (Just u , ty)) = cong (λ Γ₀ → CtxViewExtend Γ₀ x (Just u , ty)) (equivRight Γ) + +-- equivalenceContext : Equivalence (Context α) (CtxView α) +-- equivalenceContext = Equiv contextToCtxView ctxViewToContext equivLeft equivRight +-- {-# COMPILE AGDA2HS equivalenceContext #-} + +-- rezzScope' : (Γ : CtxView α) → Rezz α +-- rezzScope' CtxViewEmpty = rezz _ +-- rezzScope' (CtxViewExtend g x _) = rezzCong (λ t → t <> (singleton x)) (rezzScope' g) +-- {-# COMPILE AGDA2HS rezzScope' #-} diff --git a/src/Agda/Core/Unifier.agda b/src/Agda/Core/Unifier.agda index 3c009e0..026acaa 100644 --- a/src/Agda/Core/Unifier.agda +++ b/src/Agda/Core/Unifier.agda @@ -100,7 +100,7 @@ module Swap where -- σ₀ : Renaming (α ▸ x) α₀' let σ : Renaming (α ▸ z ▸ x) (α₀' ▸ z) σ = renamingExtend (renamingExtend ((renamingWeakenVar σ₀) ∘ inThere) inHere) (inThere (σ₀ inHere)) - az' : maybeLet α₀' + az' : MaybeLet α₀' az' = subst (renamingToSubst (rezzScope' Γ₁) σ₀) (weaken (subBindDrop subRefl) az) res1 : Σ0 _ λ α' → CtxView α' × Renaming (α ▸ z ▸ x) α' res1 = < CtxViewExtend Γ₀' z az' , σ > @@ -108,7 +108,7 @@ module Swap where let otherCase = do ⟨ γ₀ ⟩ (Δ₀ , τ₀) ← swapHighest' {{fl}} (CtxViewExtend Γ0 z az) < yInα > -- τ₀ : Renaming (z ◃ α) γ₀ - let ax' : maybeLet γ₀ + let ax' : MaybeLet γ₀ ax' = subst (renamingToSubst (rezzScope' (CtxViewExtend Γ0 z az)) τ₀) ax σ₁ : Renaming (α ▸ z ▸ x) (γ₀ ▸ x) σ₁ = renamingExtend (renamingWeakenVar τ₀) inHere From 37684ddb62c0b04cbbf4e08b8c16dab0a90240ff Mon Sep 17 00:00:00 2001 From: Ewen Broudin-Caradec Date: Thu, 17 Apr 2025 13:49:02 +0200 Subject: [PATCH 5/5] tests using contextViews --- src/Agda/Core/Context.agda | 75 ++++++++++++++++++++------------------ src/Agda/Core/Tests.agda | 4 +- 2 files changed, 42 insertions(+), 37 deletions(-) diff --git a/src/Agda/Core/Context.agda b/src/Agda/Core/Context.agda index b84f798..b2ad086 100644 --- a/src/Agda/Core/Context.agda +++ b/src/Agda/Core/Context.agda @@ -107,38 +107,43 @@ opaque {-# COMPILE AGDA2HS iSubstMaybeLet #-} --- data CtxView : @0 Scope Name → Set where --- CtxViewEmpty : CtxView mempty --- CtxViewExtend : CtxView α → (@0 x : Name) → MaybeLet α → CtxView (α ▸ x) --- {-# COMPILE AGDA2HS CtxView #-} - --- private opaque --- unfolding MaybeLet --- contextToCtxView : Context α → CtxView α --- contextToCtxView ⌈⌉ = CtxViewEmpty --- contextToCtxView (Γ , x ∶ ty) = CtxViewExtend (contextToCtxView Γ) x (Nothing , ty) --- contextToCtxView (Γ , x ≔ u ∶ ty) = CtxViewExtend (contextToCtxView Γ) x (Just u , ty) - --- ctxViewToContext : CtxView α → Context α --- ctxViewToContext CtxViewEmpty = ⌈⌉ --- ctxViewToContext (CtxViewExtend Γ x (Nothing , ty)) = ctxViewToContext Γ , x ∶ ty --- ctxViewToContext (CtxViewExtend Γ x (Just u , ty)) = ctxViewToContext Γ , x ≔ u ∶ ty - --- equivLeft : (Γ : Context α) → ctxViewToContext (contextToCtxView Γ) ≡ Γ --- equivLeft ⌈⌉ = refl --- equivLeft (Γ , x ∶ ty) = cong (λ Γ₀ → Γ₀ , x ∶ ty) (equivLeft Γ) --- equivLeft (Γ , x ≔ u ∶ ty) = cong (λ Γ₀ → Γ₀ , x ≔ u ∶ ty) (equivLeft Γ) - --- equivRight : (Γ : CtxView α) → contextToCtxView (ctxViewToContext Γ) ≡ Γ --- equivRight CtxViewEmpty = refl --- equivRight (CtxViewExtend Γ x (Nothing , ty)) = cong (λ Γ₀ → CtxViewExtend Γ₀ x (Nothing , ty)) (equivRight Γ) --- equivRight (CtxViewExtend Γ x (Just u , ty)) = cong (λ Γ₀ → CtxViewExtend Γ₀ x (Just u , ty)) (equivRight Γ) - --- equivalenceContext : Equivalence (Context α) (CtxView α) --- equivalenceContext = Equiv contextToCtxView ctxViewToContext equivLeft equivRight --- {-# COMPILE AGDA2HS equivalenceContext #-} - --- rezzScope' : (Γ : CtxView α) → Rezz α --- rezzScope' CtxViewEmpty = rezz _ --- rezzScope' (CtxViewExtend g x _) = rezzCong (λ t → t <> (singleton x)) (rezzScope' g) --- {-# COMPILE AGDA2HS rezzScope' #-} +data CtxView : @0 Scope Name → Set where + CtxViewEmpty : CtxView mempty + CtxViewExtend : CtxView α → (@0 x : Name) → MaybeLet α → CtxView (α ▸ x) +{-# COMPILE AGDA2HS CtxView #-} + +private opaque + unfolding MaybeLet + contextToCtxView : Context α → CtxView α + contextToCtxView ⌈⌉ = CtxViewEmpty + contextToCtxView (g , x ∶ ty) = CtxViewExtend (contextToCtxView g) x (Nothing , ty) + contextToCtxView (g , x ≔ u ∶ ty) = CtxViewExtend (contextToCtxView g) x (Just u , ty) + {-# COMPILE AGDA2HS contextToCtxView #-} + + + ctxViewToContext : CtxView α → Context α + ctxViewToContext CtxViewEmpty = ⌈⌉ + ctxViewToContext (CtxViewExtend g x (Nothing , ty)) = ctxViewToContext g , x ∶ ty + ctxViewToContext (CtxViewExtend g x (Just u , ty)) = ctxViewToContext g , x ≔ u ∶ ty + {-# COMPILE AGDA2HS ctxViewToContext #-} + + equivLeft : (g : Context α) → ctxViewToContext (contextToCtxView g) ≡ g + equivLeft ⌈⌉ = refl + equivLeft (g , x ∶ ty) = cong (λ g₀ → g₀ , x ∶ ty) (equivLeft g) + equivLeft (g , x ≔ u ∶ ty) = cong (λ g₀ → g₀ , x ≔ u ∶ ty) (equivLeft g) + + equivRight : (g : CtxView α) → contextToCtxView (ctxViewToContext g) ≡ g + equivRight CtxViewEmpty = refl + equivRight (CtxViewExtend g x (Nothing , ty)) = cong (λ g₀ → CtxViewExtend g₀ x (Nothing , ty)) (equivRight g) + equivRight (CtxViewExtend g x (Just u , ty)) = cong (λ g₀ → CtxViewExtend g₀ x (Just u , ty)) (equivRight g) + +opaque + unfolding contextToCtxView + equivalenceContext : Equivalence (Context α) (CtxView α) + equivalenceContext = Equiv contextToCtxView ctxViewToContext equivLeft equivRight + {-# COMPILE AGDA2HS equivalenceContext #-} + +rezzScope' : (g : CtxView α) → Rezz α +rezzScope' CtxViewEmpty = rezz _ +rezzScope' (CtxViewExtend g x _) = rezzCong (λ t → t <> (singleton x)) (rezzScope' g) +{-# COMPILE AGDA2HS rezzScope' #-} diff --git a/src/Agda/Core/Tests.agda b/src/Agda/Core/Tests.agda index 3f471f8..cbcb197 100644 --- a/src/Agda/Core/Tests.agda +++ b/src/Agda/Core/Tests.agda @@ -182,12 +182,12 @@ module TestUnifierSwap where givenfuel = Suc (Suc (Suc (Suc Zero))) opaque - unfolding ScopeThings swapHighest vec + unfolding ScopeThings swapHighest swapTwoLast vec equivalenceContext @0 testSwapHighestBaseCaseProp : Set testSwapHighestBaseCase : testSwapHighestBaseCaseProp - testSwapHighestBaseCaseProp = (swapHighest {{fl = Zero}} Context-w' w ≡ Just _ ) + testSwapHighestBaseCaseProp = (swapHighest {{fl = Zero}} Context-w' w ≡ Just (⟨ Scope-v' ▸ "w'" ▸ "w" ⟩ (Context-v' , "w'" ∶ _ , "w" ∶ _ , _)) ) testSwapHighestBaseCase = refl @0 testSwapHighest1Prop : Set