Unification

.envrc

@@ -1 +1 @@
-use flake
+use flake . -Lv

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))
 

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 = ?
+-- -}

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'

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 -}

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 Σ Δ₂ ⌉
+-}