Unification #48

jespercockx · 2025-03-18T13:33:15Z

My personal taste here would be to omit the ⌈ and ⌉ in the ⌈_∶_◃_⌉ syntax. You can always put regular parenthesis where desired.

Would it be possible to change this notation in the pull request that I started yesterday ? (As doing so here will create a conflict between the two pull request.)

Yes, that's fine with me.

Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		use flake
		use flake . -Lv

-Original file line number
+Diff line change
@@ Expand Up / @@ -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
@@ Expand All / @@ -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
@@ Expand All / @@ -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))
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up / @@ -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.Reduce
     open import Agda.Core.Signature
     module Agda.Core.Context
@@ Expand Down @@

-Original file line number
+Diff line change
@@ Expand Up / @@ -13,8 +13,6 @@ open import Agda.Core.Signature @@
     open import Agda.Core.Syntax
     open import Agda.Core.Substitute
     open import Agda.Core.Reduce
-    open import Agda.Core.Context
-    open import Agda.Core.Utils
     module Agda.Core.Conversion
       {{@0 globals : Globals}}
@@ Expand All / @@ -29,7 +27,6 @@ private variable @@
       @0 s s' t t' u u' v v' w w' : Term α
       @0 k l n sa sb    : Sort α
       @0 a a' b b' c c' : Type α
-      @0 tel            : Telescope α β
       @0 us vs          : α ⇒ β
     data Conv       {@0 α} : @0 Term α → @0 Term α → Set
@@ Expand Down @@

-Original file line number
+Diff line change
@@ -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
@@ Expand Down Expand Up / @@ -29,3 +32,69 @@ 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) ⟩
+    -------------------------------------------------------------------------------

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Unification #48

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

jespercockx Mar 18, 2025

Uh oh!

EwenBC Mar 18, 2025

Uh oh!

jespercockx Mar 18, 2025

Uh oh!

Uh oh!

-Original file line number
+Diff line change
@@ -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'

-Original file line number
+Diff line change
@@ -0,0 +1,40 @@
+    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 >)
+    {- End of module Shrink -}

-Original file line number
+Diff line change
@@ Expand Up / @@ -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
@@ Expand All @@
       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 #-}
@@ Expand Down Expand Up / @@ -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 #-}
@@ Expand All / @@ -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 Σ Δ₂ ⌉
+    -}

Unification #48

Uh oh!

Unification #48

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

jespercockx Mar 18, 2025

Choose a reason for hiding this comment

Uh oh!

EwenBC Mar 18, 2025

Choose a reason for hiding this comment

Uh oh!

jespercockx Mar 18, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!