Typing rules changes (#47)

* Simplify typing rule for App * name changes * remove datatype argument in typing rules * modifié : src/Agda/Core/Typechecker.agda modifié : src/Agda/Core/Typing.agda * Typingrules almost without Rezz * Typingrules without Rezz * Notation for Subst and TySubst and removed _ in var names * fix tyApp' comilation * notation update * white spaces * no Rezz in TyCons and helper for TyDef
jespercockx · Nov 4, 2024 · d7ebe3c · d7ebe3c
1 parent 08ef0f5
commit d7ebe3c
Show file tree

Hide file tree

Showing 3 changed files with 234 additions and 133 deletions.
diff --git a/src/Agda/Core/Syntax.agda b/src/Agda/Core/Syntax.agda
@@ -42,12 +42,21 @@ open Type public
 
 data Subst : (@0 α β : Scope Name) → Set where
   SNil  : Subst mempty β
-  SCons : Term β → Subst α β → Subst (x ◃ α) β
+  SCons :  Term β → Subst α β → Subst (x ◃ α) β
 {-# COMPILE AGDA2HS Subst deriving Show #-}
 
 infix 5 Subst
 syntax Subst α β = α ⇒ β
 
+pattern ⌈⌉ = SNil
+infix 6 ⌈_↦_◃_⌉
+pattern ⌈_↦_◃_⌉ x u σ = SCons {x = x} u σ
+infix 4 ⌈_↦_◃⌉
+pattern ⌈_↦_◃⌉ x u = ⌈ x ↦ u ◃ ⌈⌉ ⌉
+
+
+
+
 -- This should ideally be the following:
 --   Subst α β = All (λ _ → Term β) α
 -- but All being opaque prevents the positivity checker to do its job
@@ -145,8 +154,8 @@ applys {γ = γ} v (u ∷ us) = applys (TApp v u) us
 {-# COMPILE AGDA2HS applys #-}
 
 applySubst : Term γ → (β ⇒ γ) → Term γ
-applySubst {γ = γ} v SNil = v
-applySubst {γ = γ} v (SCons u us) = applySubst (TApp v u) us
+applySubst {γ = γ} v ⌈⌉ = v
+applySubst {γ = γ} v ⌈ _ ↦ u ◃ us ⌉ = applySubst (TApp v u) us
 {-# COMPILE AGDA2HS applySubst #-}
 
 
@@ -197,18 +206,18 @@ lookupSubst : α ⇒ β
             → (@0 x : Name)
             → x ∈ α
             → Term β
-lookupSubst SNil x q = inEmptyCase q
-lookupSubst (SCons u f) x q = inBindCase q (λ _ → u) (lookupSubst f x)
+lookupSubst ⌈⌉ x q = inEmptyCase q
+lookupSubst ⌈ _ ↦ u ◃ f ⌉ x q = inBindCase q (λ _ → u) (lookupSubst f x)
 
 {-# COMPILE AGDA2HS lookupSubst #-}
 
 opaque
   unfolding Scope
 
-  caseSubstBind : (s : Subst (x ◃ α) β)
-                → ((t : Term β) → (s' : Subst α β) → @0 {{s ≡ SCons t s'}} → d)
+  caseSubstBind : (s : (x ◃ α) ⇒ β)
+                → ((t : Term β) → (s' : α ⇒ β) → @0 {{s ≡ ⌈ x ↦ t ◃ s' ⌉}} → d)
                 → d
-  caseSubstBind (SCons x s) f = f x s
+  caseSubstBind ⌈ _ ↦ x ◃ s ⌉ f = f x s
 
   {-# COMPILE AGDA2HS caseSubstBind #-}
 
@@ -227,7 +236,7 @@ weakenSort     : α ⊆ β → Sort α → Sort β
 weakenType     : α ⊆ β → Type α → Type β
 weakenBranch   : α ⊆ β → Branch α c → Branch β c
 weakenBranches : α ⊆ β → Branches α cs → Branches β cs
-weakenSubst    : β ⊆ γ → Subst α β → Subst α γ
+weakenSubst    : β ⊆ γ → α ⇒ β → α ⇒ γ
 
 weakenTerm p (TVar (⟨ x ⟩ k))  = TVar (⟨ x ⟩ coerce p k)
 weakenTerm p (TDef d)          = TDef d
@@ -256,8 +265,8 @@ weakenBranches p BsNil         = BsNil
 weakenBranches p (BsCons b bs) = BsCons (weakenBranch p b) (weakenBranches p bs)
 {-# COMPILE AGDA2HS weakenBranches #-}
 
-weakenSubst p SNil = SNil
-weakenSubst p (SCons u e) = SCons (weakenTerm p u) (weakenSubst p e)
+weakenSubst p ⌈⌉ = ⌈⌉
+weakenSubst p ⌈ _ ↦ u ◃ e ⌉ = ⌈ _ ↦ (weakenTerm p u) ◃ (weakenSubst p e) ⌉
 {-# COMPILE AGDA2HS weakenSubst #-}
 
 record Weaken (t : @0 Scope Name → Set) : Set where
@@ -303,34 +312,34 @@ listSubst (rezz β) (v ∷ vs) =
 {-# COMPILE AGDA2HS listSubst #-}
 
 concatSubst : α ⇒ γ → β ⇒ γ → (α <> β) ⇒ γ
-concatSubst SNil q =
-  subst0 (λ α → Subst α _) (sym (leftIdentity _)) q
-concatSubst (SCons v p) q =
-  subst0 (λ α → Subst α _) (associativity _ _ _) (SCons v (concatSubst p q))
+concatSubst ⌈⌉ q =
+  subst0 (λ α → α ⇒ _) (sym (leftIdentity _)) q
+concatSubst ⌈ _ ↦ v ◃ p ⌉ q =
+  subst0 (λ α → α ⇒ _) (associativity _ _ _) ⌈ _ ↦ v ◃ concatSubst p q ⌉
 
 {-# COMPILE AGDA2HS concatSubst #-}
 
 opaque
   unfolding Scope Sub
 
   subToSubst : Rezz α → α ⊆ β → α ⇒ β
-  subToSubst (rezz []) p = SNil
+  subToSubst (rezz []) p = ⌈⌉
   subToSubst (rezz (Erased x ∷ α)) p =
-    SCons (TVar (⟨ x ⟩ coerce p inHere))
-          (subToSubst (rezz α) (joinSubRight (rezz _) p))
+    ⌈ x ↦ (TVar (⟨ x ⟩ coerce p inHere)) ◃ (subToSubst (rezz α) (joinSubRight (rezz _) p)) ⌉
+
 
 {-# COMPILE AGDA2HS subToSubst #-}
 
 opaque
   unfolding Scope revScope
 
   revSubstAcc : {@0 α β γ : Scope Name} → α ⇒ γ → β ⇒ γ → (revScopeAcc α β) ⇒ γ
-  revSubstAcc SNil p = p
-  revSubstAcc (SCons x s) p = revSubstAcc s (SCons x p)
+  revSubstAcc ⌈⌉ p = p
+  revSubstAcc ⌈ y ↦ x ◃ s ⌉ p = revSubstAcc s ⌈ y ↦ x ◃ p ⌉
   {-# COMPILE AGDA2HS revSubstAcc #-}
 
   revSubst : {@0 α β : Scope Name} → α ⇒ β → ~ α ⇒ β
-  revSubst = flip revSubstAcc SNil
+  revSubst = flip revSubstAcc ⌈⌉
   {-# COMPILE AGDA2HS revSubst #-}
 
 liftSubst : {@0 α β γ : Scope Name} → Rezz α → β ⇒ γ → (α <> β) ⇒ (α <> γ)
@@ -340,19 +349,19 @@ liftSubst r f =
 {-# COMPILE AGDA2HS liftSubst #-}
 
 idSubst : {@0 β : Scope Name} → Rezz β → β ⇒ β
-idSubst r = subst0 (λ β → Subst β β) (rightIdentity _) (liftSubst r SNil)
+idSubst r = subst0 (λ β → β ⇒ β) (rightIdentity _) (liftSubst r ⌈⌉)
 {-# COMPILE AGDA2HS idSubst #-}
 
 liftBindSubst : {@0 α β : Scope Name} {@0 x y : Name} → α ⇒ β → (bind x α) ⇒ (bind y β)
-liftBindSubst {y = y} e = SCons (TVar (⟨ y ⟩ inHere)) (weakenSubst (subBindDrop subRefl) e)
+liftBindSubst {y = y} e = ⌈ _ ↦ (TVar (⟨ y ⟩ inHere)) ◃ (weakenSubst (subBindDrop subRefl) e) ⌉
 {-# COMPILE AGDA2HS liftBindSubst #-}
 
 raiseSubst : {@0 α β : Scope Name} → Rezz β → α ⇒ β → (α <> β) ⇒ β
-raiseSubst {β = β} r SNil = subst (λ α → α ⇒ β) (sym (leftIdentity β)) (idSubst r)
+raiseSubst {β = β} r ⌈⌉ = subst (λ α → α ⇒ β) (sym (leftIdentity β)) (idSubst r)
 raiseSubst {β = β} r (SCons {α = α} u e) =
   subst (λ α → α ⇒ β)
     (associativity (singleton _) α β)
-    (SCons u (raiseSubst r e))
+    ⌈ _ ↦ u ◃ raiseSubst r e ⌉
 {-# COMPILE AGDA2HS raiseSubst #-}
 
 revIdSubst : {@0 α : Scope Name} → Rezz α → α ⇒ ~ α
@@ -400,8 +409,8 @@ strengthenBranch p (BBranch c r v) = BBranch c r <$> strengthenTerm (subJoinKeep
 strengthenBranches p BsNil = Just BsNil
 strengthenBranches p (BsCons b bs) = BsCons <$> strengthenBranch p b <*> strengthenBranches p bs
 
-strengthenSubst p SNil = Just SNil
-strengthenSubst p (SCons v vs) = SCons <$> strengthenTerm p v <*> strengthenSubst p vs
+strengthenSubst p ⌈⌉ = Just ⌈⌉
+strengthenSubst p ⌈ x ↦ v ◃ vs ⌉ = SCons <$> strengthenTerm p v <*> strengthenSubst p vs
 
 {-# COMPILE AGDA2HS strengthenTerm #-}
 {-# COMPILE AGDA2HS strengthenType #-}

diff --git a/src/Agda/Core/Typechecker.agda b/src/Agda/Core/Typechecker.agda
@@ -79,7 +79,7 @@ checkCoverage dt bs =
 {-# COMPILE AGDA2HS checkCoverage #-}
 
 inferVar : ∀ Γ (x : NameIn α) → TCM (Σ[ t ∈ Type α ] Γ ⊢ TVar x ∶ t)
-inferVar ctx x = return $ _ , TyTVar x
+inferVar ctx x = return $ _ , TyTVar
 {-# COMPILE AGDA2HS inferVar #-}
 
 inferSort : (Γ : Context α) (t : Term α) → TCM (Σ[ s ∈ Sort α ] Γ ⊢ t ∶ sortType s)
@@ -104,7 +104,7 @@ inferApp ctx u v = do
   let tytype = substTop r v rt
       gc = CRedL rtp CRefl
       gtu' =  TyConv {b = El (typeSort tu) (TPi x at rt)} gtu gc
-  return (tytype , TyApp gtu' gtv)
+  return (tytype , tyApp' gtu' gtv)
 {-# COMPILE AGDA2HS inferApp #-}
 
 inferCase : ∀ {@0 cs} Γ d r u bs rt → TCM (Σ[ t ∈ Type α ] Γ ⊢ TCase {x = x} d r u bs rt ∶ t)
@@ -124,7 +124,7 @@ inferCase ctx d rixs u bs rt = do
   Erased refl ← checkCoverage df bs
   cb ← checkBranches ctx (rezzBranches bs) bs df params rt
 
-  return (_ , TyCase {k = ds} {r = r} d df deq rixs bs rt grt cb gtu')
+  return (_ , tyCase' {k = ds} df deq {αRun = r} {iRun = rixs} grt cb gtu')
 
 {-# COMPILE AGDA2HS inferCase #-}
 
@@ -148,23 +148,23 @@ inferDef : ∀ Γ (f : NameIn defScope)
          → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TDef f ∶ ty)
 inferDef ctx f = do
   ty ⟨ eq ⟩ ← tcmGetType f
-  return $ _ , subst0 (λ ty → TyTerm ctx (TDef f) (weakenType subEmpty ty)) eq (TyDef f)
+  return $ _ , tyDef' ty eq
 {-# COMPILE AGDA2HS inferDef #-}
 
 checkSubst : ∀ {@0 α β} Γ (t : Telescope α β) (s : β ⇒ α) → TCM (TySubst Γ s t)
 checkSubst ctx t SNil =
   caseTelEmpty t λ where ⦃ refl ⦄ → return TyNil
-checkSubst ctx t (SCons x s) =
+checkSubst ctx t ⌈ _ ↦ x ◃ s ⌉ =
   caseTelBind t λ where ty rest ⦃ refl ⦄ → do
     tyx ← checkType ctx x ty
     let
       r = rezzScope ctx
       sstel = subst0 (λ (@0 β) → Subst β β)
                 (IsLawfulMonoid.rightIdentity iLawfulMonoidScope _)
                 (concatSubst (subToSubst r (subJoinHere _ subRefl)) SNil)
-      stel = substTelescope (SCons x sstel) rest
+      stel = substTelescope ⌈ _ ↦ x ◃ sstel ⌉ rest
     tyrest ← checkSubst ctx stel s
-    return (TyCons tyx tyrest)
+    return (tyCons' tyx tyrest)
 {-# COMPILE AGDA2HS checkSubst #-}
 
 inferData : (Γ : Context α) (d : NameIn dataScope)
@@ -174,7 +174,7 @@ inferData ctx d pars ixs = do
   dt ⟨ deq ⟩ ← tcmGetDatatype d
   typars ← checkSubst ctx (weaken subEmpty (dataParameterTel dt)) pars
   tyixs ← checkSubst ctx (substTelescope pars (dataIndexTel dt)) ixs
-  return (sortType (subst pars (dataSort dt)) , TyData d dt deq typars tyixs)
+  return (sortType (subst pars (dataSort dt)) , tyData' dt deq typars tyixs)
 {-# COMPILE AGDA2HS inferData #-}
 
 checkBranch : ∀ {@0 con : Name} (Γ : Context α)
@@ -188,7 +188,7 @@ checkBranch ctx (BBranch c r rhs) dt ps rt = do
   cid ⟨ refl ⟩  ← liftMaybe (getConstructor c dt)
     "can't find a constructor with such a name"
   crhs ← checkType _ _ _
-  return (TyBBranch (⟨ _ ⟩ cid) {rα = ra} rhs crhs)
+  return (TyBBranch (⟨ _ ⟩ cid) {αRun = ra} rhs crhs)
 {-# COMPILE AGDA2HS checkBranch #-}
 
 checkBranches ctx (rezz cons) bs dt ps rt =
@@ -209,14 +209,14 @@ checkCon ctx c cargs (El s ty) = do
   let r = rezzScope ctx
   d , (params , ixs) ⟨ rp ⟩ ← reduceToData r ty
     "can't typecheck a constrctor with a type that isn't a def application"
-  df ⟨ deq ⟩ ← tcmGetDatatype d
-  cid ⟨ refl ⟩  ← liftMaybe (getConstructor c df)
+  dt ⟨ deq ⟩ ← tcmGetDatatype d
+  cid ⟨ refl ⟩  ← liftMaybe (getConstructor c dt)
     "can't find a constructor with such a name"
-  let con = snd (dataConstructors df (⟨ _ ⟩ cid))
+  let con = snd (dataConstructors dt (⟨ _ ⟩ cid))
       ctel = substTelescope params (conTelescope con)
-      ctype = constructorType d c con (subst params (dataSort df)) params cargs
+      ctype = constructorType d c con (subst params (dataSort dt)) params cargs
   tySubst ← checkSubst ctx ctel cargs
-  checkCoerce ctx (TCon c cargs) (ctype , TyCon d df deq (⟨ _ ⟩ cid) tySubst) (El s ty)
+  checkCoerce ctx (TCon c cargs) (ctype , tyCon' dt deq (⟨ _ ⟩ cid) tySubst) (El s ty)
 {-# COMPILE AGDA2HS checkCon #-}
 
 checkLambda : ∀ Γ (@0 x : Name)
@@ -233,7 +233,7 @@ checkLambda ctx x u (El s ty) = do
 
   d ← checkType (ctx , x ∶ tu) u (renameTopType (rezzScope ctx) tv)
 
-  return $ TyConv (TyLam {k = sp} {r = r} d) gc
+  return $ TyConv (TyLam {k = sp} d) gc
 
 {-# COMPILE AGDA2HS checkLambda #-}
 
@@ -245,7 +245,7 @@ checkLet : ∀ Γ (@0 x : Name)
 checkLet ctx x u v ty = do
   tu , dtu  ← inferType ctx u
   dtv       ← checkType (ctx , x ∶ tu) v (weaken (subWeaken subRefl) ty)
-  return $ TyLet {r = rezzScope ctx} dtu dtv
+  return $ TyLet dtu dtv
 {-# COMPILE AGDA2HS checkLet #-}