Changes in Typing rules

Author: EwenBC

src/Agda/Core/Context.agda

@@ -64,4 +64,16 @@ addContextTel {α} (ExtendTel {β = β} x ty telt) c =
          (trans (associativity (~ β) [ x ] α)
                 (cong (λ t → t <> α) (sym $ revsBindComp β x)))
          (addContextTel telt (c , x ∶ ty))
+
 {-# COMPILE AGDA2HS addContextTel #-}
+
+addContextTypeS : Context α → TypeS β α → Context (β <> α)
+addContextTypeS {α} Γ ⌈⌉ =
+  subst0 Context
+         (sym $ trans (cong (λ x → x <> α) refl)
+                      (leftIdentity α))
+          Γ
+addContextTypeS {α = α} Γ (YCons {α = β} {x = x} ty Δ) =
+  let Γ' : Context (x ◃ (β <> α))
+      Γ' = addContextTypeS Γ Δ , x ∶ weaken (subJoinDrop (rezzTypeS Δ) subRefl) ty in
+  subst0 Context (associativity [ x ] β α) Γ'

src/Agda/Core/Conversion.agda

@@ -77,8 +77,8 @@ data Conv {α} where
            (bs bp : Branches α cs)
            (ms : Type _) (mp : Type _)
          → u ≅ u'
-         →   renameTop {y = z} (rezz<> (rezz~ r1) r) (unType ms)
-           ≅ renameTop {y = z} (rezz<> (rezz~ r2) r) (unType mp)
+         →   renameTop {y = z} (rezz<> r1 r) (unType ms)
+           ≅ renameTop {y = z} (rezz<> r2 r) (unType mp)
          → ConvBranches bs bp
          → TCase {x = x} d r1 u bs ms ≅ TCase {x = y} d r2 u' bp mp
   -- TODO: CProj : {!   !}
@@ -101,7 +101,7 @@ data Conv {α} where
 
 data ConvBranch {α} where
   CBBranch : (c : NameIn conScope) (r1 r2 : _)
-             (t1 t2 : Term (~ fieldScope c <> α))
+             (t1 t2 : Term (fieldScope c <> α))
            → t1 ≅ t2
            → ConvBranch (BBranch c r1 t1) (BBranch c r2 t2)
 

src/Agda/Core/Reduce.agda

@@ -60,7 +60,7 @@ data Frame (@0 α : Scope Name) : Set where
   FApp  : (u : Term α) → Frame α
   FProj : (x : NameIn defScope) → Frame α
   FCase : (d : NameIn dataScope) (r : Rezz (dataIxScope d))
-          (bs : Branches α cs) (m : Type (x ◃ (~ dataIxScope d <> α))) → Frame α
+          (bs : Branches α cs) (m : Type (x ◃ (dataIxScope d <> α))) → Frame α
 
 {-# COMPILE AGDA2HS Frame #-}
 
@@ -77,7 +77,7 @@ weakenFrame s (FProj f) = FProj f
 weakenFrame s (FCase d r bs m) =
   FCase d r
     (weaken s bs)
-    (weaken (subBindKeep (subJoinKeep (rezz~ r) s)) m)
+    (weaken (subBindKeep (subJoinKeep r s)) m)
 
 {-# COMPILE AGDA2HS weakenFrame #-}
 
@@ -122,7 +122,7 @@ unState r (MkState e v s) = subst (envToSubst r e) (unStack s v)
 
 lookupBranch : Branches α cs → (c : NameIn conScope)
              → Maybe ( Rezz (fieldScope c)
-                     × Term (~ fieldScope c <> α))
+                     × Term (fieldScope c <> α))
 lookupBranch BsNil c = Nothing
 lookupBranch (BsCons (BBranch c' aty u) bs) c =
   case decNamesIn c' c of λ where
@@ -178,9 +178,9 @@ step (rezz sig) (MkState e (TDef d) s) =
 step rsig (MkState e (TCon c vs) (FCase d r bs _ ∷ s)) =
   case lookupBranch bs c of λ where
     (Just (r , v)) → Just (MkState
-      (extendEnvironment (revSubst vs) e)
+      (extendEnvironment vs e)
       v
-      (weakenStack (subJoinDrop (rezz~ r) subRefl) s))
+      (weakenStack (subJoinDrop r subRefl) s))
     Nothing  → Nothing
 step rsig (MkState e (TData d ps is) s) = Nothing
 step rsig (MkState e (TCon c vs) (FProj f ∷ s)) = Nothing -- TODO

src/Agda/Core/Signature.agda

@@ -53,8 +53,8 @@ opaque
 
 record Constructor (@0 pars : Scope Name) (@0 ixs : Scope Name) (@0 c : NameIn conScope) : Set where
   field
-    conTelescope : Telescope pars (fieldScope c)
-    conIndices   : ixs ⇒ (revScope (fieldScope c) <> pars)
+    conIndTypeS : TypeS (fieldScope c) pars                          -- the TypeS of the indexes of c
+    conIx   : ixs ⇒ (fieldScope c) <> pars                          -- how the indexes are constructred given parameters and c indices
 open Constructor public
 
 {-# COMPILE AGDA2HS Constructor #-}
@@ -63,8 +63,8 @@ record Datatype (@0 pars : Scope Name) (@0 ixs : Scope Name) : Set where
   field
     dataConstructorScope : Scope Name
     dataSort             : Sort pars
-    dataParameterTel     : Telescope mempty pars
-    dataIndexTel         : Telescope pars ixs
+    dataParTypeS         : TypeS pars mempty
+    dataIxTypeS         : TypeS ixs pars
     dataConstructors     : ((⟨ c ⟩ cp) : NameIn  dataConstructorScope)
                          → Σ (c ∈ conScope) (λ p → Constructor pars ixs (⟨ c ⟩ p))
 open Datatype public

src/Agda/Core/Substitute.agda

@@ -27,6 +27,7 @@ substType     : α ⇒ β → Type α → Type β
 substBranch   : α ⇒ β → Branch α c → Branch β c
 substBranches : α ⇒ β → Branches α cs → Branches β cs
 substSubst    : α ⇒ β → γ ⇒ α → γ ⇒ β
+substTypeS   : α ⇒ β → γ ⇛ α → γ ⇛ β
 
 substSort f (STyp x) = STyp x
 {-# COMPILE AGDA2HS substSort #-}
@@ -45,14 +46,14 @@ substTerm f (TCase {x = x} d r u bs m) =
   TCase {x = x} d r
     (substTerm f u)
     (substBranches f bs)
-    (substType (liftBindSubst (liftSubst (rezz~ r) f)) m)
+    (substType (liftBindSubst (liftSubst r f)) m)
 substTerm f (TPi x a b)       = TPi x (substType f a) (substType (liftBindSubst f) b)
 substTerm f (TSort s)         = TSort (substSort f s)
 substTerm f (TLet x u v)      = TLet x (substTerm f u) (substTerm (liftBindSubst f) v)
 substTerm f (TAnn u t)        = TAnn (substTerm f u) (substType f t)
 {-# COMPILE AGDA2HS substTerm #-}
 
-substBranch f (BBranch c r u) = BBranch c r (substTerm (liftSubst (rezz~ r) f) u)
+substBranch f (BBranch c r u) = BBranch c r (substTerm (liftSubst r f) u)
 {-# COMPILE AGDA2HS substBranch #-}
 
 substBranches f BsNil = BsNil
@@ -63,6 +64,10 @@ substSubst f SNil = SNil
 substSubst f (SCons x e) = SCons (substTerm f x) (substSubst f e)
 {-# COMPILE AGDA2HS substSubst #-}
 
+substTypeS f ⌈⌉ = ⌈⌉
+substTypeS f ⌈ e ◃ _ ∶ x ⌉ = YCons (substType f x) (substTypeS f e)
+{-# COMPILE AGDA2HS substTypeS #-}
+
 record Substitute (t : @0 Scope Name → Set) : Set where
   field subst : (α ⇒ β) → t α → t β
 open Substitute {{...}} public
@@ -81,12 +86,15 @@ instance
   iSubstBranches .subst = substBranches
   iSubstSubst : Substitute (Subst α)
   iSubstSubst .subst = substSubst
+  iSubstTypeS : Substitute (TypeS α)
+  iSubstTypeS .subst = substTypeS
 {-# COMPILE AGDA2HS iSubstTerm #-}
 {-# COMPILE AGDA2HS iSubstType #-}
 {-# COMPILE AGDA2HS iSubstSort #-}
 {-# COMPILE AGDA2HS iSubstBranch #-}
 {-# COMPILE AGDA2HS iSubstBranches #-}
 {-# COMPILE AGDA2HS iSubstSubst #-}
+{-# COMPILE AGDA2HS iSubstTypeS #-}
 
 substTop : {{Substitute t}} → Rezz α → Term α → t (x ◃ α) → t α
 substTop r u = subst (SCons u (idSubst r))

src/Agda/Core/Syntax.agda

@@ -54,12 +54,19 @@ infix 5 Subst
 syntax Subst α β = α ⇒ β
 
 pattern ⌈⌉ = SNil
-infix 6 ⌈_↦_◃_⌉
-pattern ⌈_↦_◃_⌉ x u σ = SCons {x = x} u σ
-infix 4 ⌈_↦_◃⌉
-pattern ⌈_↦_◃⌉ x u = ⌈ x ↦ u ◃ ⌈⌉ ⌉
+infix 6 ⌈_◃_↦_⌉
+pattern ⌈_◃_↦_⌉ σ x u = SCons {x = x} u σ
+infix 4 ⌈◃_↦_⌉
+pattern ⌈◃_↦_⌉ x u = ⌈ ⌈⌉ ◃ x ↦ u ⌉
 
+infix 5 TypeS
+syntax TypeS α β = α ⇛ β
 
+pattern ⌈⌉ = YNil
+infix 6 ⌈_◃_∶_⌉
+pattern ⌈_◃_∶_⌉ Δ x u = YCons {x = x} u Δ
+infix 4 ⌈_◃_∶⌉
+pattern ⌈_◃_∶⌉ x u = ⌈ x ◃ u ∶ ⌈⌉ ⌉
 
 
 -- This should ideally be the following:
@@ -83,7 +90,7 @@ data Term α where
         → Rezz (dataIxScope d)                     -- Run-time representation of index scope
         → (u : Term α)                             -- Term we are casing on
         → (bs : Branches α cs)                     -- Branches (one for each constructor of d)
-        → (m : Type (x ◃ (~ dataIxScope d <> α)))  -- Return type
+        → (m : Type (x ◃ (dataIxScope d <> α)))  -- Return type
         → Term α
   TPi   : (@0 x : Name) (u : Type α) (v : Type (x ◃ α)) → Term α
   TSort : Sort α → Term α
@@ -116,7 +123,7 @@ sortType s = El (sucSort s) (TSort s)
 data Branch α where
   BBranch : (c : NameIn conScope)
           → Rezz (fieldScope c)
-          → Term (~ fieldScope c <> α) → Branch α (proj₁ c)
+          → Term (fieldScope c <> α) → Branch α (proj₁ c)
 {-# COMPILE AGDA2HS Branch deriving Show #-}
 
 data Branches α where
@@ -144,6 +151,10 @@ rezzBranches BsNil = rezz mempty
 rezzBranches (BsCons {c = c} bh bt) = rezzCong (λ cs → c ◃ cs) (rezzBranches bt)
 {-# COMPILE AGDA2HS rezzBranches #-}
 
+rezzTypeS : TypeS α β → Rezz α
+rezzTypeS ⌈⌉ = rezz _
+rezzTypeS ⌈ t ◃ x ∶ ty ⌉ = rezzCong (λ t → singleton x <> t) (rezzTypeS t)
+
 allBranches : Branches α β → All (λ c → c ∈ conScope) β
 allBranches BsNil = allEmpty
 allBranches (BsCons (BBranch (⟨ _ ⟩ ci) _ _) bs) = allJoin (allSingl ci) (allBranches bs)
@@ -160,7 +171,7 @@ applys {γ = γ} v (u ∷ us) = applys (TApp v u) us
 
 applySubst : Term γ → (β ⇒ γ) → Term γ
 applySubst {γ = γ} v ⌈⌉ = v
-applySubst {γ = γ} v ⌈ _ ↦ u ◃ us ⌉ = applySubst (TApp v u) us
+applySubst {γ = γ} v ⌈ us ◃ _ ↦ u ⌉ = applySubst (TApp v u) us
 {-# COMPILE AGDA2HS applySubst #-}
 
 
@@ -212,17 +223,17 @@ lookupSubst : α ⇒ β
             → x ∈ α
             → Term β
 lookupSubst ⌈⌉ x q = inEmptyCase q
-lookupSubst ⌈ _ ↦ u ◃ f ⌉ x q = inBindCase q (λ _ → u) (lookupSubst f x)
+lookupSubst ⌈ f ◃ _ ↦ u ⌉ x q = inBindCase q (λ _ → u) (lookupSubst f x)
 
 {-# COMPILE AGDA2HS lookupSubst #-}
 
 opaque
   unfolding Scope
 
   caseSubstBind : (s : (x ◃ α) ⇒ β)
-                → ((t : Term β) → (s' : α ⇒ β) → @0 {{s ≡ ⌈ x ↦ t ◃ s' ⌉}} → d)
+                → ((t : Term β) → (s' : α ⇒ β) → @0 {{s ≡ ⌈ s' ◃ x ↦ t ⌉}} → d)
                 → d
-  caseSubstBind ⌈ _ ↦ x ◃ s ⌉ f = f x s
+  caseSubstBind ⌈ s ◃ _ ↦ x ⌉ f = f x s
 
   {-# COMPILE AGDA2HS caseSubstBind #-}
 
@@ -242,6 +253,7 @@ weakenType     : α ⊆ β → Type α → Type β
 weakenBranch   : α ⊆ β → Branch α c → Branch β c
 weakenBranches : α ⊆ β → Branches α cs → Branches β cs
 weakenSubst    : β ⊆ γ → α ⇒ β → α ⇒ γ
+weakenTypeS    : β ⊆ γ → α ⇛ β → α ⇛ γ
 
 weakenTerm p (TVar (⟨ x ⟩ k))  = TVar (⟨ x ⟩ coerce p k)
 weakenTerm p (TDef d)          = TDef d
@@ -250,7 +262,7 @@ weakenTerm p (TCon c vs)       = TCon c (weakenSubst p vs)
 weakenTerm p (TLam x v)        = TLam x (weakenTerm (subBindKeep p) v)
 weakenTerm p (TApp u e)        = TApp (weakenTerm p u) (weakenTerm p e)
 weakenTerm p (TProj u x)       = TProj (weakenTerm p u) x
-weakenTerm p (TCase d r u bs m) = TCase d r (weakenTerm p u) (weakenBranches p bs) (weakenType (subBindKeep (subJoinKeep (rezz~ r) p)) m)
+weakenTerm p (TCase d r u bs m) = TCase d r (weakenTerm p u) (weakenBranches p bs) (weakenType (subBindKeep (subJoinKeep r p)) m)
 weakenTerm p (TPi x a b)       = TPi x (weakenType p a) (weakenType (subBindKeep p) b)
 weakenTerm p (TSort α)         = TSort (weakenSort p α)
 weakenTerm p (TLet x v t)      = TLet x (weakenTerm p v) (weakenTerm (subBindKeep p) t)
@@ -263,17 +275,21 @@ weakenSort p (STyp x) = STyp x
 weakenType p (El st t) = El (weakenSort p st) (weakenTerm p t)
 {-# COMPILE AGDA2HS weakenType #-}
 
-weakenBranch p (BBranch c r x) = BBranch c r (weakenTerm (subJoinKeep (rezz~ r) p) x)
+weakenBranch p (BBranch c r x) = BBranch c r (weakenTerm (subJoinKeep r p) x)
 {-# COMPILE AGDA2HS weakenBranch #-}
 
 weakenBranches p BsNil         = BsNil
 weakenBranches p (BsCons b bs) = BsCons (weakenBranch p b) (weakenBranches p bs)
 {-# COMPILE AGDA2HS weakenBranches #-}
 
 weakenSubst p ⌈⌉ = ⌈⌉
-weakenSubst p ⌈ _ ↦ u ◃ e ⌉ = ⌈ _ ↦ (weakenTerm p u) ◃ (weakenSubst p e) ⌉
+weakenSubst p ⌈ e ◃ _ ↦ u ⌉ = ⌈ (weakenSubst p e) ◃ _ ↦ (weakenTerm p u) ⌉
 {-# COMPILE AGDA2HS weakenSubst #-}
 
+weakenTypeS p ⌈⌉ = ⌈⌉
+weakenTypeS p ⌈ e ◃ _ ∶ u ⌉ = ⌈ (weakenTypeS p e) ◃ _ ∶ (weakenType p u) ⌉
+{-# COMPILE AGDA2HS weakenTypeS #-}
+
 record Weaken (t : @0 Scope Name → Set) : Set where
   field
     weaken : α ⊆ β → t α → t β
@@ -293,12 +309,15 @@ instance
   iWeakenBranches .weaken = weakenBranches
   iWeakenSubst : Weaken (Subst β)
   iWeakenSubst .weaken = weakenSubst
+  iWeakenTypeS : Weaken (TypeS β)
+  iWeakenTypeS .weaken = weakenTypeS
 {-# COMPILE AGDA2HS iWeakenTerm #-}
 {-# COMPILE AGDA2HS iWeakenSort #-}
 {-# COMPILE AGDA2HS iWeakenType #-}
 {-# COMPILE AGDA2HS iWeakenBranch #-}
 {-# COMPILE AGDA2HS iWeakenBranches #-}
 {-# COMPILE AGDA2HS iWeakenSubst #-}
+{-# COMPILE AGDA2HS iWeakenTypeS #-}
 
 
 dropSubst : {@0 α β : Scope Name} {@0 x : Name} → (x ◃ α) ⇒ β → α ⇒ β
@@ -319,8 +338,8 @@ listSubst (rezz β) (v ∷ vs) =
 concatSubst : α ⇒ γ → β ⇒ γ → (α <> β) ⇒ γ
 concatSubst ⌈⌉ q =
   subst0 (λ α → α ⇒ _) (sym (leftIdentity _)) q
-concatSubst ⌈ _ ↦ v ◃ p ⌉ q =
-  subst0 (λ α → α ⇒ _) (associativity _ _ _) ⌈ _ ↦ v ◃ concatSubst p q ⌉
+concatSubst ⌈ p ◃ _ ↦ v ⌉ q =
+  subst0 (λ α → α ⇒ _) (associativity _ _ _) ⌈ concatSubst p q ◃ _ ↦ v ⌉
 
 {-# COMPILE AGDA2HS concatSubst #-}
 
@@ -330,7 +349,7 @@ opaque
   subToSubst : Rezz α → α ⊆ β → α ⇒ β
   subToSubst (rezz []) p = ⌈⌉
   subToSubst (rezz (Erased x ∷ α)) p =
-    ⌈ x ↦ (TVar (⟨ x ⟩ coerce p inHere)) ◃ (subToSubst (rezz α) (joinSubRight (rezz _) p)) ⌉
+    ⌈ (subToSubst (rezz α) (joinSubRight (rezz _) p)) ◃ x ↦ (TVar (⟨ x ⟩ coerce p inHere)) ⌉
 
 
 {-# COMPILE AGDA2HS subToSubst #-}
@@ -340,7 +359,7 @@ opaque
 
   revSubstAcc : {@0 α β γ : Scope Name} → α ⇒ γ → β ⇒ γ → (revScopeAcc α β) ⇒ γ
   revSubstAcc ⌈⌉ p = p
-  revSubstAcc ⌈ y ↦ x ◃ s ⌉ p = revSubstAcc s ⌈ y ↦ x ◃ p ⌉
+  revSubstAcc ⌈ s ◃ y ↦ x ⌉ p = revSubstAcc s ⌈ p ◃ y ↦ x ⌉
   {-# COMPILE AGDA2HS revSubstAcc #-}
 
   revSubst : {@0 α β : Scope Name} → α ⇒ β → ~ α ⇒ β
@@ -358,15 +377,15 @@ 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 = ⌈ _ ↦ (TVar (⟨ y ⟩ inHere)) ◃ (weakenSubst (subBindDrop subRefl) e) ⌉
+liftBindSubst {y = y} e = ⌈ (weakenSubst (subBindDrop subRefl) e) ◃ _ ↦ (TVar (⟨ y ⟩ inHere)) ⌉
 {-# COMPILE AGDA2HS liftBindSubst #-}
 
 raiseSubst : {@0 α β : Scope Name} → Rezz β → α ⇒ β → (α <> β) ⇒ β
 raiseSubst {β = β} r ⌈⌉ = subst (λ α → α ⇒ β) (sym (leftIdentity β)) (idSubst r)
 raiseSubst {β = β} r (SCons {α = α} u e) =
   subst (λ α → α ⇒ β)
     (associativity (singleton _) α β)
-    ⌈ _ ↦ u ◃ raiseSubst r e ⌉
+    ⌈ raiseSubst r e ◃ _ ↦ u ⌉
 {-# COMPILE AGDA2HS raiseSubst #-}
 
 revIdSubst : {@0 α : Scope Name} → Rezz α → α ⇒ ~ α
@@ -402,7 +421,7 @@ strengthenTerm p (TProj u f) = (λ v → TProj v f) <$> strengthenTerm p u
 strengthenTerm p (TCase d r u bs m) =
   TCase d r <$> strengthenTerm p u
             <*> strengthenBranches p bs
-            <*> strengthenType (subBindKeep (subJoinKeep (rezz~ r) p)) m
+            <*> strengthenType (subBindKeep (subJoinKeep r p)) m
 strengthenTerm p (TPi x a b) =
   TPi x <$> strengthenType p a <*> strengthenType (subBindKeep p) b
 strengthenTerm p (TSort s) = TSort <$> strengthenSort p s
@@ -413,13 +432,13 @@ strengthenSort p (STyp n) = Just (STyp n)
 
 strengthenType p (El st t) = El <$> strengthenSort p st <*> strengthenTerm p t
 
-strengthenBranch p (BBranch c r v) = BBranch c r <$> strengthenTerm (subJoinKeep (rezz~ r) p) v
+strengthenBranch p (BBranch c r v) = BBranch c r <$> strengthenTerm (subJoinKeep r p) v
 
 strengthenBranches p BsNil = Just BsNil
 strengthenBranches p (BsCons b bs) = BsCons <$> strengthenBranch p b <*> strengthenBranches p bs
 
 strengthenSubst p ⌈⌉ = Just ⌈⌉
-strengthenSubst p ⌈ x ↦ v ◃ vs ⌉ = SCons <$> strengthenTerm p v <*> strengthenSubst p vs
+strengthenSubst p ⌈ vs ◃ x ↦ v ⌉ = SCons <$> strengthenTerm p v <*> strengthenSubst p vs
 
 {-# COMPILE AGDA2HS strengthenTerm #-}
 {-# COMPILE AGDA2HS strengthenType #-}
@@ -486,18 +505,18 @@ varInTerm (TProj t x) = varInTerm t
 varInTerm (TCase d r u bs m) =
   varInTerm u <>
   (varInBranches bs) <>
-  (liftListNameIn (rezz~ r) (liftBindListNameIn (varInType m)))
+  (liftListNameIn 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 σ)
+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)
+varInBranch (BBranch c r v) = liftListNameIn r (varInTerm v)