diff --git a/.envrc b/.envrc index 3550a30..a1d3540 100644 --- a/.envrc +++ b/.envrc @@ -1 +1 @@ -use flake +use flake . -Lv diff --git a/app/Agda/Core/ToCore.hs b/app/Agda/Core/ToCore.hs index d433b33..06c278e 100644 --- a/app/Agda/Core/ToCore.hs +++ b/app/Agda/Core/ToCore.hs @@ -33,15 +33,15 @@ import Agda.Syntax.Internal qualified as I import Agda.Core.Syntax (Term(..), Sort(..)) import Agda.Core.Syntax qualified as Core -import Scope.In (In) +import Scope.In (Index) import Scope.In qualified as Scope -- | Global definitions are represented as a mapping from @QName@s -- to proofs of global def scope membership. -type Defs = Map QName In +type Defs = Map QName Index -- | Same for constructors, for the global scope of all constructors. -type Cons = Map QName In +type Cons = Map QName Index -- TODO(flupe): move this to Agda.Core.Syntax @@ -68,13 +68,13 @@ asksCons = asks . (. snd) -- | Lookup a definition name in the current module. -- Fails if the definition cannot be found. -lookupDef :: QName -> ToCoreM In +lookupDef :: QName -> ToCoreM Index lookupDef qn = fromMaybeM complain $ asksDef (Map.!? qn) where complain = throwError $ "Trying to access a definition from another module: " <+> pretty qn -- -- | Lookup a constructor name in the current module. -- Fails if the constructor cannot be found. -lookupCons :: QName -> ToCoreM In +lookupCons :: QName -> ToCoreM Index lookupCons qn = fromMaybeM complain $ asksCons (Map.!? qn) where complain = throwError $ "Trying to access a constructor from another module: " <+> pretty qn @@ -96,7 +96,7 @@ instance ToCore I.Term where type CoreOf I.Term = Term toCore (I.Var k es) = (TVar (var k) `tApp`) <$> toCore es - where var :: Int -> In + where var :: Int -> Index var !n | n <= 0 = Scope.inHere var !n = Scope.inThere (var (n - 1)) diff --git a/flake.lock b/flake.lock index 2aadd8b..5457098 100644 --- a/flake.lock +++ b/flake.lock @@ -77,11 +77,11 @@ ] }, "locked": { - "lastModified": 1727185459, - "narHash": "sha256-qN5pBs5qNnnb6XbkmQepF3GgugjcyNti6he/9XZJZ9M=", + "lastModified": 1737561457, + "narHash": "sha256-/ku69k+Sgkkwhd9Ve4obffFX+HUWq4HyIfMfk56M0P8=", "owner": "jespercockx", "repo": "scope", - "rev": "c0542fae948ee3cbb98c2f880629ad70c225f79d", + "rev": "1176300aac78cf81500ca15a097d9ed98863c383", "type": "github" }, "original": { diff --git a/src/Agda/Core/Name.agda b/src/Agda/Core/Name.agda index 4251b29..9131d61 100644 --- a/src/Agda/Core/Name.agda +++ b/src/Agda/Core/Name.agda @@ -1,7 +1,10 @@ +open import Haskell.Prim +open import Haskell.Prim.Ord open import Haskell.Prelude open import Haskell.Extra.Dec open import Haskell.Extra.Erase +open import Haskell.Extra.Refinement open import Scope module Agda.Core.Name where @@ -29,3 +32,79 @@ nameInEmptyCase x = inEmptyCase (proj₂ x) nameInBindCase : ∀ {@0 y α} (x : NameIn (y ◃ α)) → (@0 proj₁ x ≡ y → a) → (proj₁ x ∈ α → a) → a nameInBindCase x = inBindCase (proj₂ x) {-# COMPILE AGDA2HS nameInBindCase inline #-} + +private variable + @0 α : Scope Name + +indexToNat : Index → Nat +indexToNat Zero = zero +indexToNat (Suc n) = suc (indexToNat n) + +natToIndex : Nat → Index +natToIndex zero = Zero +natToIndex (suc n) = Suc (natToIndex n) + +instance + iEqForIndex : Eq Index + iEqForIndex ._==_ = λ n m → (indexToNat n) == (indexToNat m) + +instance + iOrdFromLessThanIndex : OrdFromLessThan Index + iOrdFromLessThanIndex .OrdFromLessThan._<_ = λ n m → (indexToNat n) < (indexToNat m) + + iOrdIndex : Ord Index + iOrdIndex = record + { OrdFromLessThan iOrdFromLessThanIndex + ; max = λ n m → natToIndex (max (indexToNat n) (indexToNat m)) + ; min = λ n m → natToIndex (min (indexToNat n) (indexToNat m)) + } + + + +eqNameIn : NameIn α → NameIn α → Bool +eqNameIn (⟨ _ ⟩ (n ⟨ _ ⟩)) (⟨ _ ⟩ (m ⟨ _ ⟩)) = n == m + +ltNameIn : NameIn α → NameIn α → Bool +ltNameIn (⟨ _ ⟩ (n ⟨ _ ⟩)) (⟨ _ ⟩ (m ⟨ _ ⟩)) = n < m + +maxNameIn : NameIn α → NameIn α → NameIn α +maxNameIn (⟨ x ⟩ (n ⟨ xp ⟩)) (⟨ y ⟩ (m ⟨ yp ⟩)) with ((max n m) == n) +... | True = ⟨ x ⟩ (n ⟨ xp ⟩) +... | False = ⟨ y ⟩ (m ⟨ yp ⟩) + +minNameIn : NameIn α → NameIn α → NameIn α +minNameIn (⟨ x ⟩ (n ⟨ xp ⟩)) (⟨ y ⟩ (m ⟨ yp ⟩)) with ((min n m) == n) +... | True = ⟨ x ⟩ (n ⟨ xp ⟩) +... | False = ⟨ y ⟩ (m ⟨ yp ⟩) + +instance + iEqForNameIn : Eq (NameIn α) + iEqForNameIn ._==_ = eqNameIn + +instance + iOrdFromLessThanNameIn : OrdFromLessThan (NameIn α) + iOrdFromLessThanNameIn .OrdFromLessThan._<_ = ltNameIn + + iOrdNameIn : Ord (NameIn α) + iOrdNameIn = record + { OrdFromLessThan iOrdFromLessThanNameIn + ; max = maxNameIn + ; min = minNameIn + } + +------------------------------------------------------------------------------- +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) ⟩ +------------------------------------------------------------------------------- +{- +data CaseComparaison : NameIn α → NameIn α → Set where + GT : {x y : NameIn α} → @0 {{x ≡ Vzero }} → CaseComparaison x y + EQ : {x y : NameIn α} → compare x y ≡ EQ → CaseComparaison x y + LT : {x y : NameIn α} → compare x y ≡ LT → CaseComparaison x y + + +caseCompare : (x y : NameIn α) → CaseComparaison x y +caseCompare = ? +-- -} diff --git a/src/Agda/Core/Notations.md b/src/Agda/Core/Notations.md new file mode 100644 index 0000000..307fa69 --- /dev/null +++ b/src/Agda/Core/Notations.md @@ -0,0 +1,46 @@ +Notations used in Agda Core (updated on 24/11/2025) + +--------------------------------------------------------------------------------------------------- +symbols input via agda latex +≡ == \equiv +⊢ |- \vdash +ˢ ^s ^s +∶ : \vdotdot +◃ tw \smalltriangleleft +∈ in \in +⊆ sub= \subseteq +⋈ join \bowtie +⇒ => \Rightarrow +⌈ cuL \lceil +⌉ cuR \rceil +↦ r-| \mapsto +≟ ?= +↣ r-> \rightarrowtail +ᵤ _u _u +--------------------------------------------------------------------------------------------------- + +For Scopes : +α <> β α <> β Concatenation of scope α at the end of scope β +~ α revScope α scope α reversed +α ⊆ β Sub α β α is a sub-scope of β +[ x ] singleton x Scope of one element x +x ∈ α In x α singleton x ⊆ α +x ◃ α bind x α Adds element x to scope α +α ⋈ β ≡ γ Split α β γ scope γ is a mix of elements of α and β + +For context +Γ , x ∶ t CtxExtend Γ x t extension of context Γ where x is of type t (a type) + +For substitution and telescope : +α ⇒ β Subst α β substitution from α to β +⌈⌉ SNil/EmptyTel empty substitution/telescope +⌈ x ↦ u ◃ σ ⌉ SCons {x = x} u σ extension of substitution σ where x is changed to u (a term) +⌈ x ∶ t ◃ Δ ⌉ ExtendTel x t Δ extension of telescope Δ where x is of type t (a type) +δ₁ ≟ δ₂ ∶ Δ TelEq δ₁ δ₂ Δ telescopic equality between the scopes δ₁ = δ₂ of type Δ + +For types : +Γ ⊢ u ∶ t TyTerm Γ u t In context Γ, u (a term) is of type t (a type) +Γ ⊢ˢ δ ∶ Δ TySubst Γ δ Δ In context Γ, δ (a substitution) is of type Δ (a telescope) + +Unification : +Γ , ΔEq ↣ᵤ Γ' , ΔEq' UnificationStep Γ ΔEq Γ' ΔEq' diff --git a/src/Agda/Core/ScopeUtils.agda b/src/Agda/Core/ScopeUtils.agda new file mode 100644 index 0000000..80f44ca --- /dev/null +++ b/src/Agda/Core/ScopeUtils.agda @@ -0,0 +1,52 @@ +open import Haskell.Prelude +open import Haskell.Extra.Erase +open import Haskell.Law.Equality + +open import Scope + + +open import Agda.Core.Name + +module Agda.Core.ScopeUtils where + +module Shrink where + private variable + @0 α β : Scope Name + x : Name + + data Shrink : (@0 α β : Scope Name) → Set where + ShNil : Shrink mempty β + ShKeep : (@0 x : Name) → Shrink α β → Shrink (x ◃ α) (x ◃ β) + ShCons : (@0 x : Name) → Shrink α β → Shrink α (x ◃ β) + + opaque + unfolding Scope + idShrink : Rezz α → Shrink α α + idShrink (rezz []) = ShNil + idShrink (rezz (Erased x ∷ α)) = ShKeep x (idShrink (rezz α)) + + ShrinkToSub : Shrink α β → α ⊆ β + ShrinkToSub ShNil = subEmpty + ShrinkToSub (ShKeep x s) = subBindKeep (ShrinkToSub s) + ShrinkToSub (ShCons x s) = subBindDrop (ShrinkToSub s) + + opaque + unfolding Sub Split + SubToShrink : Rezz β → α ⊆ β → Shrink α β + SubToShrink _ (⟨ γ ⟩ EmptyL) = ShNil + SubToShrink βRun (⟨ γ ⟩ EmptyR) = idShrink βRun + SubToShrink βRun (⟨ γ ⟩ ConsL x p) = ShKeep x (SubToShrink (rezzUnbind βRun) < p >) + SubToShrink βRun (⟨ γ ⟩ ConsR y p) = ShCons y (SubToShrink (rezzUnbind βRun) < p >) + {- + opaque + unfolding Sub Split SubToShrink splitEmptyLeft + ShrinkEquivLeft : (βRun : Rezz β) (s : Shrink α β) → SubToShrink βRun (ShrinkToSub s) ≡ s + ShrinkEquivLeft βRun ShNil = refl + ShrinkEquivLeft βRun (ShKeep x s) = do + let e = ShrinkEquivLeft (rezzUnbind βRun) s + subst (λ z → SubToShrink βRun (ShrinkToSub (ShKeep x s)) ≡ ShKeep x z ) e {! !} + ShrinkEquivLeft βRun (ShCons x s) = do + let e = ShrinkEquivLeft (rezzUnbind βRun) s + subst (λ z → SubToShrink βRun (ShrinkToSub (ShCons x s)) ≡ ShCons x z ) e {! !} + -} +{- End of module Shrink -} \ No newline at end of file diff --git a/src/Agda/Core/Signature.agda b/src/Agda/Core/Signature.agda index f7ce4da..243e8b3 100644 --- a/src/Agda/Core/Signature.agda +++ b/src/Agda/Core/Signature.agda @@ -4,7 +4,9 @@ open import Haskell.Prelude hiding (All; s; t) open import Haskell.Extra.Dec using (ifDec) open import Haskell.Extra.Erase open import Haskell.Law.Equality -open import Haskell.Law.Monoid +open import Haskell.Law.Semigroup.Def +open import Haskell.Law.Monoid.Def + open import Utils.Tactics using (auto) open import Agda.Core.Name @@ -27,20 +29,24 @@ data Telescope (@0 α : Scope Name) : @0 Scope Name → Set where EmptyTel : Telescope α mempty ExtendTel : (@0 x : Name) → Type α → Telescope (x ◃ α) β → Telescope α (x ◃ β) +pattern ⌈⌉ = EmptyTel +infix 6 ⌈_∶_◃_⌉ +pattern ⌈_∶_◃_⌉ x t Δ = ExtendTel x t Δ + {-# COMPILE AGDA2HS Telescope #-} opaque unfolding Scope caseTelEmpty : (tel : Telescope α mempty) - → (@0 {{tel ≡ EmptyTel}} → d) + → (@0 {{tel ≡ ⌈⌉}} → d) → d - caseTelEmpty EmptyTel f = f + caseTelEmpty ⌈⌉ f = f caseTelBind : (tel : Telescope α (x ◃ β)) → ((a : Type α) (rest : Telescope (x ◃ α) β) → @0 {{tel ≡ ExtendTel x a rest}} → d) → d - caseTelBind (ExtendTel _ a tel) f = f a tel + caseTelBind ⌈ _ ∶ a ◃ tel ⌉ f = f a tel {-# COMPILE AGDA2HS caseTelEmpty #-} {-# COMPILE AGDA2HS caseTelBind #-} @@ -116,8 +122,8 @@ getConstructor c d = {-# COMPILE AGDA2HS getConstructor #-} weakenTel : α ⊆ γ → Telescope α β → Telescope γ β -weakenTel p EmptyTel = EmptyTel -weakenTel p (ExtendTel x ty t) = ExtendTel x (weaken p ty) (weakenTel (subBindKeep p) t) +weakenTel p ⌈⌉ = ⌈⌉ +weakenTel p ⌈ x ∶ ty ◃ t ⌉ = ⌈ x ∶ (weaken p ty) ◃ (weakenTel (subBindKeep p) t) ⌉ {-# COMPILE AGDA2HS weakenTel #-} @@ -127,19 +133,51 @@ instance {-# COMPILE AGDA2HS iWeakenTel #-} rezzTel : Telescope α β → Rezz β -rezzTel EmptyTel = rezz _ -rezzTel (ExtendTel x ty t) = rezzCong (λ t → singleton x <> t) (rezzTel t) +rezzTel ⌈⌉ = rezz _ +rezzTel ⌈ x ∶ ty ◃ t ⌉ = rezzCong (λ t → singleton x <> t) (rezzTel t) {-# COMPILE AGDA2HS rezzTel #-} +opaque + addTel : Telescope α β → Telescope ((~ β) <> α) γ → Telescope α (β <> γ) + addTel {α = α} {γ = γ} ⌈⌉ tel0 = do + let Δ₁ : Telescope (mempty <> α) γ + Δ₁ = subst0 (λ ∅ → Telescope (∅ <> α) γ) revsIdentity tel0 + Δ₂ : Telescope α γ + Δ₂ = subst0 (λ α₀ → Telescope α₀ γ) (leftIdentity α) Δ₁ + subst0 (λ γ₀ → Telescope α γ₀) (sym (leftIdentity γ)) Δ₂ + addTel {α = α} {γ = γ} ⌈ x ∶ ty ◃ s ⌉ tel0 = do + let Δ₁ : Telescope ((~ _ ▹ x) <> α) γ + Δ₁ = subst0 (λ β₀ → Telescope (β₀ <> α) γ) (revsBindComp _ x) tel0 + Δ₂ : Telescope (~ _ <> (x ◃ α)) γ + Δ₂ = subst0 (λ α₀ → Telescope α₀ γ) (sym (associativity (~ _) [ x ] α)) Δ₁ + Ξ : Telescope (x ◃ α) (_ <> γ) + Ξ = addTel s Δ₂ + Ξ' : Telescope α (x ◃ (_ <> γ)) + Ξ' = ⌈ x ∶ ty ◃ Ξ ⌉ + @0 e : x ◃ (_ <> γ) ≡ (x ◃ _) <> γ + e = associativity [ x ] _ γ + subst0 (λ γ₀ → Telescope α γ₀) e Ξ' + + {-# COMPILE AGDA2HS addTel #-} + + addTelrev : Telescope α (~ β) → Telescope (β <> α) γ → Telescope α ((~ β) <> γ) + addTelrev {α = α} {β = β} {γ = γ} sigma delta = do + let Δ₁ : Telescope (~ ~ β <> α) γ + Δ₁ = subst0 (λ β₀ → Telescope (β₀ <> α) γ) (sym (revsInvolution β)) delta + addTel sigma Δ₁ + + {-# COMPILE AGDA2HS addTelrev #-} + {- -addTel : Telescope α β → Telescope ((revScope β) <> α) γ → Telescope α (β <> γ) -addTel EmptyTel t = - subst0 (Telescope _) - (sym (leftIdentity _)) - (subst0 (λ s → Telescope s _) - (trans (cong (λ t → t <> _) - revScopeMempty) - (leftIdentity _)) - t) -addTel (ExtendTel x ty s) t = {!!} -} +opaque + unfolding revScope + addTel : Telescope α β → Telescope ((~ β) <> α) γ → Telescope α (β <> γ) + addTel ⌈⌉ Δ = Δ + addTel {α = α} {β = _ ∷ β} {γ = γ} ⌈ x ∶ ty ◃ Σ ⌉ Δ = do + let Δ₁ : Telescope ((~ β ▹ x) <> α) γ + Δ₁ = subst0 (λ β₀ → Telescope (β₀ <> α) γ) (revsBindComp β x) Δ + Δ₂ : Telescope (~ β <> (x ◃ α)) γ + Δ₂ = subst0 (λ α₀ → Telescope α₀ γ) (sym (associativity (~ β) [ x ] α)) Δ₁ + ⌈ x ∶ ty ◃ addTel Σ Δ₂ ⌉ +-} \ No newline at end of file diff --git a/src/Agda/Core/Syntax.agda b/src/Agda/Core/Syntax.agda index a344e59..63474f1 100644 --- a/src/Agda/Core/Syntax.agda +++ b/src/Agda/Core/Syntax.agda @@ -368,6 +368,10 @@ revIdSubst : {@0 α : Scope Name} → Rezz α → α ⇒ ~ α revIdSubst {α} r = subst0 (λ s → s ⇒ (~ α)) (revsInvolution α) (revSubst (idSubst (rezz~ r))) {-# COMPILE AGDA2HS revIdSubst #-} +revIdSubst' : {@0 α : Scope Name} → Rezz α → ~ α ⇒ α +revIdSubst' {α} r = subst0 (λ s → (~ α) ⇒ s) (revsInvolution α) (revIdSubst (rezz~ r)) +{-# COMPILE AGDA2HS revIdSubst' #-} + raise : {@0 α β : Scope Name} → Rezz α → Term β → Term (α <> β) raise r = weakenTerm (subJoinDrop r subRefl) {-# COMPILE AGDA2HS raise #-} @@ -445,3 +449,50 @@ instance {-# COMPILE AGDA2HS iStrengthenBranch #-} {-# COMPILE AGDA2HS iStrengthenBranches #-} {-# COMPILE AGDA2HS iStrengthenSubst #-} + +opaque + unfolding Scope + liftBindListNameIn : List (NameIn (x ◃ α)) → List (NameIn α) + liftBindListNameIn [] = [] + liftBindListNameIn ((⟨ x ⟩ (Zero ⟨ p ⟩)) ∷ l) = liftBindListNameIn l + liftBindListNameIn ((⟨ x ⟩ (Suc n ⟨ IsSuc p ⟩)) ∷ l) = < n ⟨ p ⟩ > ∷ (liftBindListNameIn l) + + liftListNameIn : Rezz γ → List (NameIn (γ <> α)) → List (NameIn α) + liftListNameIn _ [] = [] + liftListNameIn γRun ((⟨ x ⟩ xInγα) ∷ l) = + inJoinCase γRun xInγα + (λ _ → liftListNameIn γRun l) + (λ xInα → < xInα > ∷ (liftListNameIn γRun l)) + +{- TODO: create merge function for sorted lists of var as replacing <> by it would **greatly** decrease complexity -} +varInTerm : Term α → List (NameIn α) +varInSubst : Subst α β → List (NameIn β) +varInType : Type α → List (NameIn α) +varInBranches : Branches α cs → List (NameIn α) +varInBranch : Branch α c → List (NameIn α) + +varInTerm (TVar x) = x ∷ [] +varInTerm (TDef d) = [] +varInTerm (TData d ps is) = varInSubst is <> (varInSubst ps) +varInTerm (TCon c vs) = varInSubst vs +varInTerm (TLam x v) = liftBindListNameIn (varInTerm v) +varInTerm (TApp t₀ t₁) = varInTerm t₀ <> (varInTerm t₁) +varInTerm (TProj t x) = varInTerm t +varInTerm (TCase d r u bs m) = + varInTerm u <> + (varInBranches bs) <> + (liftListNameIn (rezz~ r) (liftBindListNameIn (varInType m))) +varInTerm (TPi x a b) = varInType a <> (liftBindListNameIn (varInType b)) +varInTerm (TSort x) = [] +varInTerm (TLet x t t₁) = varInTerm t <> (liftBindListNameIn (varInTerm t₁)) +varInTerm (TAnn u t) = varInTerm u <> varInType t + +varInSubst ⌈⌉ = [] +varInSubst ⌈ x ↦ u ◃ σ ⌉ = (varInTerm u) <> (varInSubst σ) + +varInType (El _ u) = varInTerm u + +varInBranches BsNil = [] +varInBranches (BsCons b bs) = varInBranch b <> (varInBranches bs) + +varInBranch (BBranch c r v) = liftListNameIn (rezz~ r) (varInTerm v) diff --git a/src/Agda/Core/Tests.agda b/src/Agda/Core/Tests.agda index f7d7149..fe1be00 100644 --- a/src/Agda/Core/Tests.agda +++ b/src/Agda/Core/Tests.agda @@ -21,13 +21,15 @@ open import Agda.Core.Context open import Agda.Core.TCM open import Agda.Core.Typing open import Agda.Core.Typechecker +open import Agda.Core.Unification +open import Agda.Core.Unifier private variable x y : Name α : Scope Name instance - top : In x (x ◃ α) + top : x ∈ (x ◃ α) top = inHere pop : {{x ∈ α}} → x ∈ (y ◃ α) @@ -133,5 +135,65 @@ module TestTypechecker (@0 x y z : Name) where testProp₁ = testTC₁ ≡ Right _ test₁ = refl +module TestUnifierSwap where + open Swap + opaque private + basicTerm : Term α + basicTerm = TLam "x" (TVar < inHere >) + ℕ : Type α + ℕ = El (STyp zero) basicTerm + A : Type α + A = El (STyp zero) basicTerm + vec : Type α → Term α → Type α + vec A _ = A + + -- (n₀ : ℕ) (v : vec A n) (m₀ : ℕ) (v' : vec A n₀) (w : vec A m₀) (w' : vec A m₀) + Scope-n₀ = "n₀" ◃ mempty + Scope-v = "v" ◃ Scope-n₀ + Scope-m₀ = "m₀" ◃ Scope-v + Scope-v' = "v'" ◃ Scope-m₀ + Scope-w = "w" ◃ Scope-v' + Scope-w' = "w'" ◃ Scope-w + + Context-n₀ = CtxEmpty , "n₀" ∶ ℕ + Context-v : Context Scope-v + Context-v = Context-n₀ , "v" ∶ vec A (TVar (⟨ "n₀" ⟩ inHere)) + Context-m₀ : Context Scope-m₀ + Context-m₀ = Context-v , "m₀" ∶ ℕ + Context-v' : Context Scope-v' + Context-v' = Context-m₀ , "v'" ∶ vec A (TVar (⟨ "n₀" ⟩ inThere (inThere inHere))) + Context-w : Context Scope-w + Context-w = Context-v' , "w" ∶ vec A (TVar (⟨ "m₀" ⟩ inThere inHere)) + Context-w' : Context Scope-w' + Context-w' = Context-w , "w'" ∶ vec A (TVar (⟨ "m₀" ⟩ inThere (inThere (inHere)))) + + w : NameIn Scope-w + w = ⟨ "w" ⟩ inHere + + v' : NameIn Scope-w + v' = ⟨ "v'" ⟩ (inThere inHere) + + m₀ : NameIn Scope-w + m₀ = ⟨ "m₀" ⟩ (inThere (inThere inHere)) + + givenfuel = Suc (Suc (Suc (Suc Zero))) + opaque + unfolding ScopeThings swapHighest vec + + @0 testSwapHighestBaseCaseProp : Set + testSwapHighestBaseCase : testSwapHighestBaseCaseProp + + testSwapHighestBaseCaseProp = (swapHighest {{fl = Zero}} Context-w' w ≡ Just _ ) + testSwapHighestBaseCase = refl + + @0 testSwapHighest1Prop : Set + testSwapHighest1 : testSwapHighest1Prop + + testSwapHighest1Prop = (swapHighest {{fl = Suc Zero}} Context-w' v' ≡ Just _ ) + testSwapHighest1 = refl + + @0 testSwapHighest2Prop : Set + testSwapHighest2 : testSwapHighest1Prop --- -} + testSwapHighest2Prop = (swapHighest {{fl = Suc (Suc (Suc (Suc Zero)))}} Context-w' m₀ ≡ Nothing ) + testSwapHighest2 = refl diff --git a/src/Agda/Core/Typechecker.agda b/src/Agda/Core/Typechecker.agda index 931a7c1..44684bb 100644 --- a/src/Agda/Core/Typechecker.agda +++ b/src/Agda/Core/Typechecker.agda @@ -244,7 +244,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 (subWeaken subRefl) ty) + dtv ← checkType (ctx , x ∶ 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 f2adff4..7978054 100644 --- a/src/Agda/Core/Typing.agda +++ b/src/Agda/Core/Typing.agda @@ -165,7 +165,7 @@ data TyTerm {α} Γ where TyLet : Γ ⊢ u ∶ a - → Γ , x ∶ a ⊢ v ∶ weakenType (subWeaken subRefl) b + → Γ , x ∶ a ⊢ v ∶ weakenType (subBindDrop subRefl) b ---------------------------------------------- → Γ ⊢ TLet x u v ∶ b @@ -234,12 +234,12 @@ data TyBranch {α} {x} Γ {pScope} {iScope} dt pSubst return where data TySubst {α} Γ where TyNil : ----------------------------------------------------------- - Γ ⊢ˢ ⌈⌉ ∶ EmptyTel + Γ ⊢ˢ ⌈⌉ ∶ ⌈⌉ TyCons : Γ ⊢ u ∶ a → Γ ⊢ˢ us ∶ (substTelescope ⌈ x ↦ u ◃ idSubst (rezz α) ⌉ tel) ----------------------------------------------------------- - → Γ ⊢ˢ ⌈ x ↦ u ◃ us ⌉ ∶ (ExtendTel x a tel) + → Γ ⊢ˢ ⌈ x ↦ u ◃ us ⌉ ∶ ⌈ x ∶ a ◃ tel ⌉ {-# COMPILE AGDA2HS TySubst #-} @@ -318,6 +318,6 @@ tyCons' : {@0 Γ : Context α} {@0 αRun : Rezz α} → Γ ⊢ u ∶ a → Γ ⊢ˢ us ∶ (substTelescope ⌈ x ↦ u ◃ idSubst αRun ⌉ tel) ----------------------------------------------------------- - → Γ ⊢ˢ ⌈ x ↦ u ◃ us ⌉ ∶ (ExtendTel x a tel) + → Γ ⊢ˢ ⌈ x ↦ u ◃ us ⌉ ∶ ⌈ x ∶ a ◃ tel ⌉ tyCons' {αRun = α ⟨ refl ⟩} tyu tyus = TyCons tyu tyus -{-# COMPILE AGDA2HS tyCon' #-} \ No newline at end of file +{-# COMPILE AGDA2HS tyCons' #-} \ No newline at end of file diff --git a/src/Agda/Core/Unification.agda b/src/Agda/Core/Unification.agda new file mode 100644 index 0000000..f679c0c --- /dev/null +++ b/src/Agda/Core/Unification.agda @@ -0,0 +1,459 @@ +open import Scope + +open import Haskell.Prelude hiding (All; s; t; a; coerce) +open import Haskell.Extra.Erase +open import Haskell.Law.Equality renaming (subst to transport) +open import Haskell.Law.Monoid.Def + +open import Agda.Core.Name +open import Agda.Core.GlobalScope using (Globals) +open import Agda.Core.Utils +open import Agda.Core.Syntax +open import Agda.Core.Signature +open import Agda.Core.Substitute +open import Agda.Core.Context +open import Agda.Core.TCM +open import Agda.Core.TCMInstances + +module Agda.Core.Unification + {{@0 globals : Globals}} + {{@0 sig : Signature}} + where + +private open module @0 G = Globals globals + +renamingExtend : ∀ {@0 α β : Scope Name} {@0 x : Name} → Renaming α β → x ∈ β → Renaming (x ◃ α) β +renamingExtend σ xInβ = λ zInx◃α → inBindCase zInx◃α (λ where refl → xInβ) σ + +opaque + unfolding Scope + renamingWeaken : ∀ {@0 α β γ : Scope Name} → Rezz γ → Renaming α β → Renaming α (γ <> β) + renamingWeaken (rezz []) σ = σ + renamingWeaken (rezz (_ ∷ α)) σ = inThere ∘ (renamingWeaken (rezz α) σ) + +renamingWeakenVar : ∀ {@0 α β : Scope Name} {@0 x : Name} → Renaming α β → Renaming α (x ◃ β) +renamingWeakenVar σ = inThere ∘ σ + +opaque + unfolding Scope + renamingToSubst : ∀ {@0 α β : Scope Name} → Rezz α → Renaming α β → α ⇒ β + renamingToSubst (rezz []) _ = ⌈⌉ + renamingToSubst (rezz (Erased x ∷ α)) r = + let r' : Renaming α _ + r' = λ xp → r (coerce (subBindDrop subRefl) xp) in + ⌈ x ↦ TVar < r (Zero ⟨ IsZero refl ⟩) > ◃ renamingToSubst (rezz α) r' ⌉ + + + +--------------------------------------------------------------------------------------------------- + {- PART ONE : Shrinking -} +--------------------------------------------------------------------------------------------------- +module Shrinking where + {- A module where shrinking, an operation to remove some variables of a scope while + preserving dependancies is defined -} + + private variable + @0 x : Name + @0 α β : Scope Name + + data ShrinkSubst : (@0 α β : Scope Name) → Set where + RNil : ShrinkSubst mempty mempty + RKeep : ShrinkSubst α β → ShrinkSubst (x ◃ α) (x ◃ β) + RCons : Term β → ShrinkSubst α β → ShrinkSubst (x ◃ α) β + {-# COMPILE AGDA2HS ShrinkSubst deriving Show #-} + + opaque + unfolding Scope + idShrinkSubst : Rezz α → ShrinkSubst α α + idShrinkSubst (rezz []) = RNil + idShrinkSubst (rezz (Erased x ∷ α)) = RKeep (idShrinkSubst (rezz α)) + + + ShrinkSubstToSubst : ShrinkSubst α β → α ⇒ β + ShrinkSubstToSubst RNil = ⌈⌉ + ShrinkSubstToSubst (RKeep {x = x} σ) = + ⌈ x ↦ TVar (⟨ x ⟩ inHere) ◃ weaken (subBindDrop subRefl) (ShrinkSubstToSubst σ) ⌉ + ShrinkSubstToSubst (RCons {x = x} u σ) = ⌈ x ↦ u ◃ ShrinkSubstToSubst σ ⌉ + + ShrinkSubstToSub : ShrinkSubst α β → β ⊆ α + ShrinkSubstToSub RNil = subEmpty + ShrinkSubstToSub (RKeep {x = x} σ) = subBindKeep (ShrinkSubstToSub σ) + ShrinkSubstToSub (RCons {x = x} u σ) = subBindDrop (ShrinkSubstToSub σ) + + 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 Γ σ + + opaque + unfolding cut + shrinkFromCut : Rezz α → (xp : x ∈ α) → Term (cutDrop xp) → ShrinkSubst α (cutTake xp <> cutDrop xp) + shrinkFromCut (rezz (_ ∷ α')) (Zero ⟨ IsZero refl ⟩) u = RCons u (idShrinkSubst (rezz α')) + shrinkFromCut (rezz (_ ∷ α')) (Suc n ⟨ IsSuc p ⟩) u = RKeep (shrinkFromCut (rezz α') (n ⟨ p ⟩) u) + +{- End of module Shrinking -} +open Shrinking + +--------------------------------------------------------------------------------------------------- + {- PART TWO : Definition of telescopic equality -} +--------------------------------------------------------------------------------------------------- +module TelescopeEq where + {- A module where : + - two equivalent versions of the telescopic equality are defined + - auxiliary datatypes are defined for the two telescopic equality + - equivalence between the auxiliary datatypes for telescopic equality is proved + - some transport and substitution auxiliary functions for telescopic equality are implemented + Read it if you want to understand the structure behind telescopic equality. + -} + + private variable + @0 x : Name + @0 α α₀ α' β β' : Scope Name + + --------------------------------------------------------------------------------------------------- + {- Expanded version of telescopic equality, where both parts of the equality are already constructed -} + record TelescopicEq (@0 α β : Scope Name) : Set where + constructor TelEq + field + left : β ⇒ α + right : β ⇒ α + telescope : Telescope α β + + infixr 6 _≟_∶_ + pattern _≟_∶_ δ₁ δ₂ Δ = TelEq δ₁ δ₂ Δ + + --------------------------------------------------------------------------------------------------- + {- Compact version of telescopic equality, where both parts of the equality are constructed step by step -} + data Compact (@0 α₀ : Scope Name) : (@0 α β : Scope Name) → Set where + EmptyEq : Compact α₀ α mempty + ExtendEq : {@0 β : Scope Name} (@0 x : Name) + (u v : Term α₀) (A : Type (α <> α₀)) + → Compact α₀ (x ◃ α) β + → Compact α₀ α (x ◃ β) + + telescopicEq' : (@0 α β : Scope Name) → Set + telescopicEq' α β = Compact α mempty β + + --------------------------------------------------------------------------------------------------- + {- auxiliary datatype for telescopicEq as independant scopes are needed + to go from one representation to the other -} + private + record Expanded (@0 α₀ α β : Scope Name) : Set where + constructor TelExp + field + left : β ⇒ α₀ + right : β ⇒ α₀ + telescope : Telescope (α <> α₀) β + + --------------------------------------------------------------------------------------------------- + {- definition of an equivalence -} + private opaque + unfolding Scope + {- Functions to go from one auxiliary datatype to the other -} + compactToExpanded : Compact α₀ α β → Expanded α₀ α β + compactToExpanded EmptyEq = TelExp ⌈⌉ ⌈⌉ EmptyTel + compactToExpanded (ExtendEq x u v a ΔEq) = do + let TelExp δ₁ δ₂ Δ = compactToExpanded ΔEq + TelExp ⌈ x ↦ u ◃ δ₁ ⌉ ⌈ x ↦ v ◃ δ₂ ⌉ ⌈ x ∶ a ◃ Δ ⌉ + + expandedToCompact : Expanded α₀ α β → Compact α₀ α β + expandedToCompact (TelExp ⌈⌉ ⌈⌉ EmptyTel) = EmptyEq + expandedToCompact (TelExp ⌈ x ↦ u ◃ δ₁ ⌉ ⌈ x ↦ v ◃ δ₂ ⌉ ⌈ x ∶ a ◃ Δ ⌉) = do + let ΔEq = expandedToCompact (TelExp δ₁ δ₂ Δ) + ExtendEq x u v a ΔEq + + {- The functions above form an equivalence -} + equivLeft : (ΔEq : Compact α₀ α β) + → expandedToCompact (compactToExpanded ΔEq) ≡ ΔEq + equivLeft EmptyEq = refl + equivLeft (ExtendEq x u v a ΔEq) = do + let eH = equivLeft ΔEq + cong (λ ΔEq → ExtendEq x u v a ΔEq) eH + + equivRight : (ΔEq' : Expanded α₀ α β) + → compactToExpanded (expandedToCompact ΔEq') ≡ ΔEq' + equivRight (TelExp ⌈⌉ ⌈⌉ ⌈⌉) = refl + equivRight (TelExp ⌈ x ↦ u ◃ δ₁ ⌉ ⌈ x ↦ v ◃ δ₂ ⌉ ⌈ x ∶ a ◃ Δ ⌉) = do + let eH = equivRight (TelExp δ₁ δ₂ Δ) + cong (λ (TelExp δ₁ δ₂ Δ) → TelExp ⌈ x ↦ u ◃ δ₁ ⌉ ⌈ x ↦ v ◃ δ₂ ⌉ ⌈ x ∶ a ◃ Δ ⌉) eH + + equivalenceAux : Equivalence (Compact α₀ α β) (Expanded α₀ α β) + equivalenceAux = Equiv compactToExpanded expandedToCompact equivLeft equivRight + + telescopicEq'ToEq : telescopicEq' α β → TelescopicEq α β + telescopicEq'ToEq ΔEq' = do + let TelExp σ₁ σ₂ Δ = compactToExpanded ΔEq' + TelEq σ₁ σ₂ Δ + + telescopicEqToEq' : TelescopicEq α β → telescopicEq' α β + telescopicEqToEq' (TelEq σ₁ σ₂ Δ) = expandedToCompact (TelExp σ₁ σ₂ Δ) + + equivLeftTelEq : (ΔEq' : telescopicEq' α β) → telescopicEqToEq' (telescopicEq'ToEq ΔEq') ≡ ΔEq' + equivLeftTelEq EmptyEq = refl + equivLeftTelEq (ExtendEq x u v a ΔEq) = do + let eH = equivLeft ΔEq + cong (λ ΔEq → ExtendEq x u v a ΔEq) eH + + equivRightTelEq : (ΔEq : TelescopicEq α β) → telescopicEq'ToEq (telescopicEqToEq' ΔEq) ≡ ΔEq + equivRightTelEq (TelEq ⌈⌉ ⌈⌉ ⌈⌉) = refl + equivRightTelEq (TelEq ⌈ x ↦ u ◃ δ₁ ⌉ ⌈ x ↦ v ◃ δ₂ ⌉ ⌈ x ∶ a ◃ Δ ⌉) = do + let eH = equivRight (TelExp δ₁ δ₂ Δ) + cong (λ (TelExp δ₁ δ₂ Δ) → TelEq ⌈ x ↦ u ◃ δ₁ ⌉ ⌈ x ↦ v ◃ δ₂ ⌉ ⌈ x ∶ a ◃ Δ ⌉) eH + + equivalenceTelEq : {α β : Scope Name} → Equivalence (telescopicEq' α β) (TelescopicEq α β) + equivalenceTelEq = Equiv telescopicEq'ToEq telescopicEqToEq' equivLeftTelEq equivRightTelEq + + --------------------------------------------------------------------------------------------------- + {- helpful functions -} + + substTelescopicEq : (α₀ ⇒ α) → TelescopicEq α₀ β → TelescopicEq α β + substTelescopicEq σ (TelEq δ₁ δ₂ Δ) = TelEq (subst σ δ₁) (subst σ δ₂) (subst σ Δ) + {-# COMPILE AGDA2HS substTelescopicEq #-} + + instance + iSubstTelescopicEq : Substitute (λ α → TelescopicEq α β) + iSubstTelescopicEq .subst = substTelescopicEq + {-# COMPILE AGDA2HS iSubstTelescopicEq #-} + + opaque + unfolding Scope + telescopeDrop : Rezz α → Telescope α (x ◃ β) → Term α → Telescope α β + telescopeDrop αRun ⌈ x ∶ a ◃ Δ ⌉ w = + subst (concatSubst ⌈ x ↦ w ◃⌉ (idSubst αRun)) Δ + + telescopicEqDrop : Rezz α → TelescopicEq α (x ◃ β) → Term α → TelescopicEq α β + telescopicEqDrop αRun (TelEq ⌈ x ↦ u ◃ δ₁ ⌉ ⌈ x ↦ v ◃ δ₂ ⌉ Δ) w = TelEq δ₁ δ₂ (telescopeDrop αRun Δ w) + +{- End of module TelescopeEq -} +open TelescopeEq + +--------------------------------------------------------------------------------------------------- + {- PART THREE : Unification Step By Step -} +--------------------------------------------------------------------------------------------------- +module UnificationStepAndStop where + private variable + @0 e₀ x : Name + @0 α α' α'' β β' β'' : Scope Name + δ₁ δ₂ : β ⇒ α + ds : Sort α + + data UnificationStep (Γ : Context α) : TelescopicEq α β → Context α' → TelescopicEq α' β' → Set + data UnificationStop (Γ : Context α) : TelescopicEq α β → Set + infix 3 _,_↣ᵤ_,_ + infix 3 _,_↣ᵤ⊥ + _,_↣ᵤ_,_ = UnificationStep + _,_↣ᵤ⊥ = UnificationStop + + @0 Strengthened : ∀ {@0 α β : Scope Name} → Term β → Term α → Set + Strengthened {α = α} {β = β} u u₀ = (∃[ p ∈ α ⊆ β ] Just u₀ ≡ strengthen p u) + + data UnificationStep {α = α} Γ where + + {- remove equalities of the form t = t -} + Deletion : + {t : Term α} + {Ξ : Telescope α (e₀ ◃ β)} + (let Δ : Telescope α β + Δ = telescopeDrop (rezz α) Ξ t) -- replace e₀ by t in the telescope + ------------------------------------------------------------ + → Γ , ⌈ e₀ ↦ t ◃ δ₁ ⌉ ≟ ⌈ e₀ ↦ t ◃ δ₂ ⌉ ∶ Ξ ↣ᵤ Γ , δ₁ ≟ δ₂ ∶ Δ + + {- solve equalities of the form x = u when x is a variable -} + SolutionL : + {xp : x ∈ α} + (let α₀ , α₁ = cut xp + α' = α₁ <> α₀) -- new scope without x + {u : Term α} + {u₀ : Term α₀} -- u₀ is independant from x as x ∉ α₀ + {Ξ : Telescope α (e₀ ◃ β)} + (let rσ = shrinkFromCut (rezz α) xp u₀ -- an order preserving substitution to remove x + Γ' : Context α' + Γ' = shrinkContext Γ rσ -- new context where x is removed + ΔEq : TelescopicEq α β + ΔEq = δ₁ ≟ δ₂ ∶ telescopeDrop (rezz α) Ξ u -- replace e₀ by u in the telescopic equality + ΔEq' : TelescopicEq α' β + ΔEq' = substTelescopicEq (ShrinkSubstToSubst rσ) ΔEq) -- replace x by u + → Strengthened u u₀ + ------------------------------------------------------------ + → Γ , ⌈ e₀ ↦ TVar (⟨ x ⟩ xp) ◃ δ₁ ⌉ ≟ ⌈ e₀ ↦ u ◃ δ₂ ⌉ ∶ Ξ ↣ᵤ Γ' , ΔEq' + SolutionR : + {xp : x ∈ α} + (let α₀ , α₁ = cut xp + α' = α₁ <> α₀) -- new scope without x + {u : Term α} + {u₀ : Term α₀} -- u₀ is independant from x as x ∉ α₀ + {Ξ : Telescope α (e₀ ◃ β)} + (let rσ = shrinkFromCut (rezz α) xp u₀ -- an order preserving substitution to remove x + Γ' : Context α' + Γ' = shrinkContext Γ rσ -- new context where x is removed + ΔEq : TelescopicEq α β + ΔEq = δ₁ ≟ δ₂ ∶ telescopeDrop (rezz α) Ξ u -- replace e₀ by u in the telescopic equality + ΔEq' : TelescopicEq α' β + ΔEq' = substTelescopicEq (ShrinkSubstToSubst rσ) ΔEq) -- replace x by u + → Strengthened u u₀ + ------------------------------------------------------------ + → Γ , ⌈ e₀ ↦ u ◃ δ₂ ⌉ ≟ ⌈ e₀ ↦ TVar (⟨ x ⟩ xp) ◃ δ₁ ⌉ ∶ Ξ ↣ᵤ Γ' , ΔEq' + + {- solve equalities of the form c i = c j for a constructor c of a datatype d -} + {- this only work with K -} + Injectivity : + {d : NameIn dataScope} -- the datatype + (let dt = sigData sig d) -- representation of the datatype d + {pSubst : dataParScope d ⇒ α} -- value of the parameters of d + {iSubst : dataIxScope d ⇒ α} -- value of the indices of d + {Δe₀ : Telescope (e₀ ◃ α) β} + ( (⟨ c₀ ⟩ cFromd) : NameIn (dataConstructorScope dt)) -- c is a constructor of dt + (let cFromCon , con = dataConstructors dt (⟨ c₀ ⟩ cFromd) + c = (⟨ c₀ ⟩ cFromCon) -- c is a constructor of a datatype + γ : Scope Name + γ = fieldScope c) -- name of the arguments of c + {σ₁ σ₂ : γ ⇒ α} + (let Σ : Telescope α γ + Σ = subst pSubst (conTelescope con) -- type of the arguments of c + σe : γ ⇒ (~ γ <> α) + σe = weaken (subJoinHere (rezz _) subRefl) (revIdSubst (rezz γ)) -- names of the new equalities to replace e₀ + τ₀ : [ e₀ ] ⇒ (~ γ <> α) + τ₀ = subst0 (λ ξ₀ → ξ₀ ⇒ (~ γ <> α)) (rightIdentity _) ⌈ e₀ ↦ TCon c σe ◃⌉ + τ : (e₀ ◃ α) ⇒ (~ γ <> α) + τ = concatSubst τ₀ (weaken (subJoinDrop (rezz _) subRefl) (idSubst (rezz α))) + Δγ : Telescope (~ γ <> α) β -- telescope using ~ γ instead of e₀ + Δγ = subst τ Δe₀) + ------------------------------------------------------------------- ⚠ NOT a rewrite rule ⚠ (c = (⟨ c₀ ⟩ cFromCon)) + → Γ , ⌈ e₀ ↦ TCon c σ₁ ◃ δ₁ ⌉ ≟ ⌈ e₀ ↦ TCon c σ₂ ◃ δ₂ ⌉ ∶ ⌈ e₀ ∶ El ds (TData d pSubst iSubst) ◃ Δe₀ ⌉ + ↣ᵤ Γ , concatSubst σ₁ δ₁ ≟ concatSubst σ₂ δ₂ ∶ addTel Σ Δγ + + {- solve equalities of the form c i = c j for a constructor c of a datatype d -} + InjectivityDep : + {- from β = ixs <> (e₀ ◃ β₀) to β' = γ <> β₀ -} + {β₀ : Scope Name} + {δ₁ δ₂ : β₀ ⇒ α} + {d : NameIn dataScope} -- the datatype + (let dt = sigData sig d + pars = dataParScope d + ixs = dataIxScope d) + {ds : Sort (~ ixs <> α)} + {pSubst : pars ⇒ α} -- value of the parameters of d + {iSubst₁ iSubst₂ : ixs ⇒ α} -- value of the indices of d + {Δe₀ixs : Telescope (e₀ ◃ (~ ixs <> α)) β₀} + { (⟨ c₀ ⟩ cFromd) : NameIn (dataConstructorScope dt)} -- c is a constructor of dt + (let cFromCon , con = dataConstructors dt (⟨ c₀ ⟩ cFromd) + c = (⟨ c₀ ⟩ cFromCon) -- c is a constructor of a datatype + γ : Scope Name + γ = fieldScope c) -- name of the arguments of c + {σ₁ σ₂ : γ ⇒ α} + (let Σ : Telescope α γ + Σ = subst pSubst (conTelescope con) -- type of the arguments of c + + iTel : Telescope α ixs + iTel = subst pSubst (dataIndexTel dt) + + iSubste : ixs ⇒ (~ ixs <> α) + iSubste = weakenSubst (subJoinHere (rezz _) subRefl) (revIdSubst (rezz ixs)) + weakenα : α ⇒ (~ ixs <> α) + weakenα = weaken (subJoinDrop (rezz _) subRefl) (idSubst (rezz α)) + + σe : γ ⇒ (~ γ <> α) + σe = weaken (subJoinHere (rezz _) subRefl) (revIdSubst (rezz γ)) + τ₀ : [ e₀ ] ⇒ (~ γ <> α) + τ₀ = subst0 (λ ξ₀ → ξ₀ ⇒ (~ γ <> α)) (rightIdentity _) ⌈ e₀ ↦ TCon c σe ◃⌉ + τ₁ : ~ ixs ⇒ (~ γ <> α) + τ₁ = subst (subst (liftSubst (rezz _) pSubst) (conIndices con)) (revIdSubst' (rezz _)) + τ₂ : α ⇒ (~ γ <> α) + τ₂ = weaken (subJoinDrop (rezz _) subRefl) (idSubst (rezz α)) + τ : (e₀ ◃ (~ ixs <> α)) ⇒ (~ γ <> α) + τ = concatSubst τ₀ (concatSubst τ₁ τ₂) + Δγ : Telescope (~ γ <> α) β₀ + Δγ = subst τ Δe₀ixs) + ------------------------------------------------------------------- ⚠ NOT a rewrite rule ⚠ + → Γ , concatSubst iSubst₁ ⌈ e₀ ↦ TCon c σ₁ ◃ δ₁ ⌉ ≟ concatSubst iSubst₂ ⌈ e₀ ↦ TCon c σ₂ ◃ δ₂ ⌉ + ∶ addTel iTel ⌈ e₀ ∶ El ds (TData d (subst weakenα pSubst) iSubste) ◃ Δe₀ixs ⌉ + ↣ᵤ Γ , concatSubst σ₁ δ₁ ≟ concatSubst σ₂ δ₂ ∶ addTel Σ Δγ + {- TODO: replace Injectivity and InjectivityDep by better rule from article proof relevant Unification (2018) J. Cockx & D. Devriese -} + {- if possible change definition of constructors and datatypes to make Injectivity a rewrite rule -} + {- End of UnificationStep -} + + data InSubst (t : Term β) : α ⇒ β → Set + data InSubst {β = β} t where + DirectInSubst : + {σ : α ⇒ β} + → InSubst t ⌈ x ↦ t ◃ σ ⌉ + RecInSubst : + {σ : α ⇒ β} + {u : Term β} + → InSubst t σ + → InSubst t ⌈ x ↦ u ◃ σ ⌉ + + data CycleProof (x : NameIn α) : Term α → Set + data CycleProof {α = α} x where + BasicCycle : + {c : NameIn conScope} + {σ : fieldScope c ⇒ α} + → InSubst (TVar x) σ + → CycleProof x (TCon c σ) + SubCycle : + {u v : Term α} + {c : NameIn conScope} + {σ : fieldScope c ⇒ α} + → CycleProof x v + → InSubst v σ + → CycleProof x (TCon c σ) + + data UnificationStop {α = α} Γ where + Conflict : + {nameC nameC' : Name} + {proofC : nameC ∈ conScope} + {proofC' : nameC' ∈ conScope} + (let c = ⟨ nameC ⟩ proofC + c' = ⟨ nameC' ⟩ proofC') + {σ₁ : fieldScope c ⇒ α} + {σ₂ : fieldScope c' ⇒ α} + {Ξ : Telescope α (e₀ ◃ β)} + → nameC ≠ nameC' + ------------------------------------------------------------ + → Γ , ⌈ e₀ ↦ TCon c σ₁ ◃ δ₁ ⌉ ≟ ⌈ e₀ ↦ TCon c' σ₂ ◃ δ₂ ⌉ ∶ Ξ ↣ᵤ⊥ + {- cycle right now isn't as strict as it should be to correspond to the + proof where pattern matching is reduced to eliminator in Jesper Cockx thesis + it would be nice to rewrite it + cycle can go through a non inductive argument position a constructor + (no proof that it can happen but no proof that it cannot) -} + CycleL : + {x : NameIn α} + (u : Term α) + {Ξ : Telescope α (e₀ ◃ β)} + → CycleProof x u + ------------------------------------------------------------ + → Γ , ⌈ e₀ ↦ TVar x ◃ δ₁ ⌉ ≟ ⌈ e₀ ↦ u ◃ δ₂ ⌉ ∶ Ξ ↣ᵤ⊥ + CycleR : + {x : NameIn α} + (u : Term α) + {Ξ : Telescope α (e₀ ◃ β)} + → CycleProof x u + ------------------------------------------------------------ + → Γ , ⌈ e₀ ↦ u ◃ δ₂ ⌉ ≟ ⌈ e₀ ↦ TVar x ◃ δ₁ ⌉ ∶ Ξ ↣ᵤ⊥ + {- End of UnificationStop -} + + + data UnificationSteps : Context α → TelescopicEq α β → Context α' → TelescopicEq α' β' → Set where + StepCons : + (Γ : Context α) (Γ' : Context α') (Γ'' : Context α'') + → (Ξ : TelescopicEq α β) (Ξ' : TelescopicEq α' β') (Ξ'' : TelescopicEq α'' β'') + → UnificationStep Γ Ξ Γ' Ξ' → UnificationSteps Γ' Ξ' Γ'' Ξ'' + → UnificationSteps Γ Ξ Γ'' Ξ'' + StepId : (Γ : Context α) (Ξ : TelescopicEq α β) → UnificationSteps Γ Ξ Γ Ξ + + data UnificationStops : Context α → TelescopicEq α β → Set where + StopCons : + (Γ : Context α) (Γ' : Context α') + → (Ξ : TelescopicEq α β) (Ξ' : TelescopicEq α' β') + → UnificationSteps Γ Ξ Γ' Ξ' → UnificationStop Γ' Ξ' + → UnificationStops Γ Ξ + + infix 3 _,_↣ᵤ⋆_,_ + infix 3 _,_↣ᵤ⋆⊥ + _,_↣ᵤ⋆_,_ = UnificationSteps + _,_↣ᵤ⋆⊥ = UnificationStops +{- End of module UnificationStepAndStop -} +open UnificationStepAndStop diff --git a/src/Agda/Core/Unifier.agda b/src/Agda/Core/Unifier.agda new file mode 100644 index 0000000..9404796 --- /dev/null +++ b/src/Agda/Core/Unifier.agda @@ -0,0 +1,229 @@ +open import Scope + +open import Haskell.Prelude hiding (All; s; t; a) +open import Haskell.Extra.Erase +open import Haskell.Law.Equality renaming (subst to transport) +open import Haskell.Law.Monoid.Def +open import Haskell.Law.List + +open import Agda.Core.Name +open import Agda.Core.GlobalScope using (Globals) +open import Agda.Core.Utils +open import Agda.Core.Syntax +open import Agda.Core.Signature +open import Agda.Core.Substitute +open import Agda.Core.Context +open import Agda.Core.TCM +open import Agda.Core.TCMInstances +open import Agda.Core.Unification +open UnificationStepAndStop +open TelescopeEq + +module Agda.Core.Unifier + {{@0 globals : Globals}} + {{@0 sig : Signature}} + where + +private open module @0 G = Globals globals + + +--------------------------------------------------------------------------------------------------- + {- PART ONE : Context reordering -} +--------------------------------------------------------------------------------------------------- + +module Swap where + private variable + @0 x y : Name + @0 α : Scope Name + + data SwapError : Set where + CantSwapVarWithItSelf : SwapError + VarInWrongOrder : SwapError + + 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') + + + {- Idea of swapHighest (x, z, Γ) y: + - terminaison condition : you swap x and y or fail + - case 1: if you can swap the two first vars of (x, z, Γ) then + do it and let Γ1Aux be the result of a recursive call on (x, Γ) + return (z, Γ1Aux) + - case 2: if case 1 fails then let Γ' be the result of the + 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) + let σ : Renaming (x ◃ y ◃ α) (y ◃ x ◃ α) + σ = renamingExtend (renamingExtend (renamingWeaken (rezz (_ ∷ _ ∷ [])) id) inHere) (inThere inHere) + return < Γ' , σ > + swapHighest {x = x} {α = Erased z ∷ α} {{Suc fl}} (CtxExtend (CtxExtend Γ0 z az) x ax) (⟨ y ⟩ (Suc value ⟨ IsSuc proof ⟩)) = + let Γ : Context (x ◃ z ◃ α) + Γ = (CtxExtend (CtxExtend Γ0 z az) x ax) + yInα : y ∈ α + yInα = value ⟨ proof ⟩ in + let areTheTwoLastVarsSwapable = do + (CtxExtend Γ₁ .z az') ← swapTwoLast Γ + ⟨ α₀' ⟩ (Γ₀' , σ₀ ) ← swapHighest {{fl}} Γ₁ < yInα > + -- σ₀ : Renaming (x ◃ α) α₀' + let σ : Renaming (x ◃ z ◃ α) (z ◃ α₀') + σ = renamingExtend (renamingExtend ((renamingWeakenVar σ₀) ∘ inThere) inHere) (inThere (σ₀ inHere)) + az' : Type α₀' + az' = subst (renamingToSubst (rezzScope Γ₁) σ₀) (weaken (subBindDrop subRefl) az) + res1 : Σ0 _ λ α' → Context α' × Renaming (x ◃ z ◃ α) α' + res1 = < CtxExtend Γ₀' z az' , σ > + return res1 in + let otherCase = do + ⟨ γ₀ ⟩ (Δ₀ , τ₀) ← swapHighest {{fl}} (CtxExtend Γ0 z az) < yInα > + -- τ₀ : Renaming (z ◃ α) γ₀ + let ax' : Type γ₀ + ax' = subst (renamingToSubst (rezzScope (CtxExtend Γ0 z az)) τ₀) ax + σ₁ : Renaming (x ◃ z ◃ α) (x ◃ γ₀) + σ₁ = renamingExtend (renamingWeakenVar τ₀) inHere + ⟨ α' ⟩ (Γ' , σ₂) ← swapHighest {{fl}} (CtxExtend Δ₀ x ax') < τ₀ (inThere yInα) > + -- σ₂ : Renaming (x ◃ α₀') α' + let res2 : Σ0 _ λ α' → Context α' × Renaming (x ◃ z ◃ α) α' + 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 + + swap : Context α → (x y : NameIn α) → Either SwapError (Maybe (Σ0 _ λ α' → Context α' × Renaming α α')) + 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 ⟩)) + 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 > -} + + swapVarListFuel : (fl : Nat) → Context α → (x : NameIn α) → (l : List (NameIn α)) → Maybe (Σ0 _ λ α' → Context α' × Renaming α α') + swapVarListFuel (suc fl) Γ (⟨ x ⟩ xp) ((⟨ y ⟩ yp) ∷ l) = do + ⟨ _ ⟩ (Γ0' , σ₀) ← try_swap Γ (⟨ x ⟩ xp) (⟨ y ⟩ yp) + ⟨ _ ⟩ (Γ' , σ) ← swapVarListFuel fl Γ0' (⟨ x ⟩ σ₀ xp) (map (λ z → < σ₀ (proj₂ z) >) l) + 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 + swapVarListFuel zero Γ x [] = Just < Γ , id > + swapVarListFuel _ _ _ _ = Nothing + + swapVarList : Context α → (x : NameIn α) → List (NameIn α) → Maybe (Σ0 _ λ α' → Context α' × Renaming α α') + swapVarList Γ x l = swapVarListFuel (lengthNat l) Γ x l + + swapVarTerm : (Γ : Context α) → ((⟨ x ⟩ xp) : NameIn α) → (u : Term α) + → Maybe (Σ0 _ λ α' → Context α' × Renaming α α') + swapVarTerm Γ x u = swapVarList Γ x (varInTerm u) + + opaque + swapVarTermStrengthened : (Γ : Context α) → ((⟨ x ⟩ xp) : NameIn α) → (u : Term α) + → Maybe (Σ0 _ λ α' → Context α' × (Σ[ σ ∈ Renaming α α' ] + (Σ[ u₀ ∈ Term (cutDrop (σ xp)) ] Strengthened (subst (renamingToSubst (rezzScope Γ) σ) u) u₀))) + swapVarTermStrengthened Γ (⟨ x ⟩ xp) u = + caseMaybe (swapVarTerm Γ (⟨ x ⟩ xp) u) + (λ (⟨ α' ⟩ (Γ' , σ)) → + let u' : Term α' + u' = subst (renamingToSubst (rezzScope Γ) σ) u in + caseMaybe (strengthen subCutDrop u') + (λ u₀ {{e}} → Just (⟨ α' ⟩ (Γ' , (σ , (u₀ , (subCutDrop ⟨ e ⟩)))))) + Nothing) + Nothing + +{- End of module Swap -} +open Swap + +--------------------------------------------------------------------------------------------------- + {- PART TWO : Unification algorithm -} +--------------------------------------------------------------------------------------------------- +{- +private variable + @0 α β : Scope Name + @0 x : Name + Γ : Context α + Ξ : TelescopicEq α β + +data UnificationFailure (Γ : Context α) (Ξ : TelescopicEq α β) : Set where + Stop : UnificationStops Γ Ξ → UnificationFailure Γ Ξ + Error : String → UnificationFailure Γ Ξ + Crash : String → UnificationFailure Γ Ξ + +UnificationResult : (Γ : Context α) (Ξ : TelescopicEq α β) → Set +UnificationResult Γ Ξ = Either + (UnificationFailure Γ Ξ) + (Σ0[ γ ∈ Scope Name ] ∃[ Γ' ∈ Context γ ] UnificationSteps Γ Ξ Γ' (⌈⌉ ≟ ⌈⌉ ∶ ⌈⌉)) + +record UnificationValidStep (Γ : Context α) (Ξ : TelescopicEq α β) : Set where + constructor UStep + field + @0 α' : Scope Name + @0 β' : Scope Name + Γ' : Context α' + Ξ' : TelescopicEq α' β' + step : UnificationStep Γ Ξ Γ' Ξ' + +UnificationStepResult : (Γ : Context α) (Ξ : TelescopicEq α β) → Set +UnificationStepResult Γ Ξ = Either (UnificationFailure Γ Ξ) (UnificationValidStep Γ Ξ) + +opaque + unfolding Scope + unifDeletion : (Γ : Context α) (Ξ : TelescopicEq α β) → UnificationStepResult Γ Ξ + unifDeletion Γ (⌈ e ↦ aₗ ◃ σₗ ⌉ ≟ ⌈ e ↦ aᵣ ◃ σᵣ ⌉ ∶ ⌈ e ∶ t ◃ Δ ⌉) = {! !} + unifDeletion _ _ = Left (Error "deletion step not valid") + + unifSolution : (Γ : Context α) (Ξ : TelescopicEq α β) → UnificationStepResult Γ Ξ + unifSolution Γ (⌈ e ↦ TVar x ◃ σₗ ⌉ ≟ ⌈ e ↦ TVar y ◃ σᵣ ⌉ ∶ ⌈ e ∶ t ◃ Δ ⌉) with compare x y + ... | GT = + let @0 α' : Scope Name + α' = cutTake (proj₂ x) <> cutDrop (proj₂ x) + yInα' : Maybe (_ ∈ α') + yInα' = do {! !} in + caseMaybe yInα' {! !} (Left (Crash "should be impossible")) + +-- in Right (UStep _ _ {! !} {! !} {! !}) + ... | EQ = Left (Error "solution step not valid") + ... | LT = Right (UStep _ _ {! !} {! !} {! !}) + unifSolution Γ (⌈ e ↦ TVar x ◃ σₗ ⌉ ≟ ⌈ e ↦ aᵣ ◃ σᵣ ⌉ ∶ ⌈ e ∶ t ◃ Δ ⌉) with (swapVarTerm Γ x aᵣ) + ... | Nothing = Left (Error "check for CycleL") + ... | Just (⟨ α' ⟩ (Γ' , aaa)) = {! s !} + unifSolution Γ (⌈ e ↦ αᵣ ◃ σₗ ⌉ ≟ ⌈ e ↦ TVar y ◃ σᵣ ⌉ ∶ ⌈ e ∶ t ◃ Δ ⌉) = {! !} + unifSolution _ _ = Left (Error "solution step not valid") + + +opaque + unfolding Scope + unification : (Γ : Context α) → (Ξ : TelescopicEq α β) → UnificationResult Γ Ξ + unification Γ (⌈⌉ ≟ ⌈⌉ ∶ ⌈⌉) = Right < Γ ⟨ StepId Γ _ ⟩ > + unification Γ (⌈ x ↦ aₗ ◃ σₗ ⌉ ≟ ⌈ x ↦ aᵣ ◃ σᵣ ⌉ ∶ ⌈ x ∶ t ◃ Δ ⌉) = {! !} +-- -} + \ No newline at end of file diff --git a/src/Agda/Core/Utils.agda b/src/Agda/Core/Utils.agda index 76401a5..95581e1 100644 --- a/src/Agda/Core/Utils.agda +++ b/src/Agda/Core/Utils.agda @@ -59,3 +59,20 @@ record Instance (a : Set) : Set where {{inst}} : a {-# COMPILE AGDA2HS Instance unboxed #-} + +record Equivalence (a b : Set) : Set where + constructor Equiv + field + σ : a → b + τ : b → a + @0 left : (x : a) → τ (σ x) ≡ x + @0 right : (y : b) → σ (τ y) ≡ y + +open Equivalence public + +{-# COMPILE AGDA2HS Equivalence #-} + + +caseMaybe : ∀ {@0 ℓ₁ ℓ₂} {@0 a : Set ℓ₁} {@0 b : Set ℓ₂} → (mb : Maybe a) → ((x : a) → @0 {{Just x ≡ mb}} → b) → (@0 {{Nothing ≡ mb}} → b) → b +caseMaybe Nothing j n = n +caseMaybe (Just x) j n = j x