diff --git a/src/Agda/Core/Context.agda b/src/Agda/Core/Context.agda index c0f34fe..b2ad086 100644 --- a/src/Agda/Core/Context.agda +++ b/src/Agda/Core/Context.agda @@ -4,14 +4,15 @@ 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) 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.Signature +open import Agda.Core.Substitute module Agda.Core.Context {{@0 globals : Globals}} @@ -26,32 +27,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β) @@ -60,3 +65,85 @@ 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 #-} + + 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 #-} + + instance + iWeakenMaybeLet : Weaken MaybeLet + iWeakenMaybeLet .weaken = weakenMaybeLet + {-# 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 = strengthenMaybeLet + {-# COMPILE AGDA2HS iStrengthenMaybeLet #-} + + 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 #-} + + instance + iSubstMaybeLet : Substitute MaybeLet + iSubstMaybeLet .subst = substMaybeLet + {-# 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 (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/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/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 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..026acaa 100644 --- a/src/Agda/Core/Unifier.agda +++ b/src/Agda/Core/Unifier.agda @@ -64,12 +64,16 @@ module Swap where opaque unfolding Scope - swapTwoLast : Context (α ▸ x ▸ y) → Maybe (Context (α ▸ y ▸ x)) - swapTwoLast (CtxExtend (CtxExtend Γ y ay) x ax) = do - ax' ← strengthen (subBindDrop subRefl) ax - let ay' = weaken (subBindDrop subRefl) ay - return ((Γ , x ∶ ax' ) , y ∶ 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 @@ -80,73 +84,72 @@ 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 (CtxExtend (CtxExtend Γ0 y ay) x ax) (⟨ y ⟩ (Zero ⟨ IsZero refl ⟩)) = do - Γ' ← swapTwoLast (CtxExtend (CtxExtend Γ0 y ay) x ax) + 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 (_ ∷ _ ∷ [])) 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}} Γ@(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 - 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