partial refactoring using RScope

Author: EwenBC

src/Agda/Core/Context.agda

@@ -20,6 +20,7 @@ module Agda.Core.Context
 private variable
   @0 x y : Name
   @0 α β : Scope Name
+  @0 rβ : RScope Name
   @0 s t u v : Term α
 
 data Context : @0 Scope Name → Set where
@@ -64,16 +65,11 @@ 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 ] β α) Γ'
+addContextTypeS : Context α → TypeS α rβ → Context (extScope α rβ)
+addContextTypeS Γ ⌈⌉ = Γ
+addContextTypeS {α = α} Γ (YCons {rβ = rβ₀} {x = x} ty Δ) =
+  let Γ' : Context (extScope (x ◃ α) rβ₀)
+      Γ' = addContextTypeS (Γ , x ∶ weaken {!   !} ty) {! Δ !}
+      in {!   !}

src/Agda/Core/GlobalScope.agda

@@ -11,10 +11,10 @@ record Globals : Set where
   field
     defScope     : Scope Name
     dataScope    : Scope Name
-    dataParScope : NameIn dataScope → Scope Name
-    dataIxScope  : NameIn dataScope → Scope Name
+    dataParScope : NameIn dataScope → RScope Name
+    dataIxScope  : NameIn dataScope → RScope Name
     conScope     : Scope Name
-    fieldScope   : NameIn conScope → Scope Name
+    fieldScope   : NameIn conScope → RScope Name
 open Globals public
 {-# COMPILE AGDA2HS Globals #-}
 

src/Agda/Core/Reduce.agda

@@ -26,6 +26,7 @@ private open module @0 G = Globals globals
 private variable
   @0 x c      : Name
   @0 α β γ cs : Scope Name
+  @0 rγ : RScope Name
   @0 u v w    : Term α
 
 data Environment : (@0 α β : Scope Name) → Set where
@@ -60,7 +61,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 ◃ (extScope α (dataIxScope d)))) → Frame α
 
 {-# COMPILE AGDA2HS Frame #-}
 
@@ -77,7 +78,7 @@ weakenFrame s (FProj f) = FProj f
 weakenFrame s (FCase d r bs m) =
   FCase d r
     (weaken s bs)
-    (weaken (subBindKeep (subJoinKeep r s)) m)
+    (weaken (subBindKeep (subExtScopeKeep r s)) m)
 
 {-# COMPILE AGDA2HS weakenFrame #-}
 
@@ -122,7 +123,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 (extScope α (fieldScope c)))
 lookupBranch BsNil c = Nothing
 lookupBranch (BsCons (BBranch c' aty u) bs) c =
   case decNamesIn c' c of λ where
@@ -131,27 +132,21 @@ lookupBranch (BsCons (BBranch c' aty u) bs) c =
 
 {-# COMPILE AGDA2HS lookupBranch #-}
 
-rezzFromEnv : β ⇒ γ → Rezz β
-rezzFromEnv SNil = rezz _
-rezzFromEnv (SCons v vs) = rezzCong2 (λ (Erased x) α → x ◃ α) rezzErase (rezzFromEnv vs)
-{-# COMPILE AGDA2HS rezzFromEnv #-}
 
-extendEnvironment : β ⇒ γ → Environment α γ → Environment α (β <> γ)
-extendEnvironment vs e = aux (rezzFromEnv vs) vs e
+extendEnvironment : TermS β rγ → Environment α β → Environment α (extScope β rγ)
+extendEnvironment vs e = aux (rezzTermS vs) vs e
   where
-    aux : Rezz β → β ⇒ γ → Environment α γ → Environment α (β <> γ)
-    aux r SNil e = subst0 (Environment _) (sym (leftIdentity _)) e
-    aux r (SCons {α = α} {x = x} v vs) e =
-      let r' = rezzUnbind r
-      in  subst0 (Environment _) (associativity _ _ _)
-          (aux r' vs e , x ↦ raise r' v)
+    aux : Rezz rγ → TermS β rγ → Environment α β → Environment α (extScope β rγ)
+    aux r ⌈⌉ e = e
+    aux (rezz (x ◂ rγ₀)) (TSCons {α = β} {rβ = rγ₀} {x = x} v vs) e =
+      aux (rezz rγ₀) (weaken (subBindDrop subRefl) vs) (e , x ↦ v)
 {-# COMPILE AGDA2HS extendEnvironment #-}
 
 lookupEnvironment : Environment α β → x ∈ β → Either (x ∈ α) (Term β)
 lookupEnvironment EnvNil      p = Left p
 lookupEnvironment (e , x ↦ v) p = inBindCase p
-  (λ _ → Right (raise (rezz _) v))
-  (λ p → mapRight (raise (rezz _)) (lookupEnvironment e p))
+  (λ _ → Right (weaken (subBindDrop subRefl) v))
+  (λ p → mapRight (weaken (subBindDrop subRefl)) (lookupEnvironment e p))
 {-# COMPILE AGDA2HS lookupEnvironment #-}
 
 step : (rsig : Rezz sig) (s : State α) → Maybe (State α)
@@ -180,7 +175,7 @@ step rsig (MkState e (TCon c vs) (FCase d r bs _ ∷ s)) =
     (Just (r , v)) → Just (MkState
       (extendEnvironment vs e)
       v
-      (weakenStack (subJoinDrop r subRefl) s))
+      (weakenStack (subExtScope 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
@@ -218,4 +213,3 @@ reduceAppView s (v ⟨ p ⟩) =
   (unApps v) ⟨ subst0 (λ t → ReducesTo s t) (sym $ unAppsView v) p ⟩
 
 {-# COMPILE AGDA2HS reduceAppView #-}
-

src/Agda/Core/Signature.agda

@@ -51,20 +51,20 @@ opaque
 {-# COMPILE AGDA2HS caseTelEmpty #-}
 {-# COMPILE AGDA2HS caseTelBind #-}
 
-record Constructor (@0 pars : Scope Name) (@0 ixs : Scope Name) (@0 c : NameIn conScope) : Set where
+record Constructor (@0 pars : RScope Name) (@0 ixs : RScope Name) (@0 c : NameIn conScope) : Set where
   field
-    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
+    conIndTypeS : TypeS (extScope mempty pars) (fieldScope c)             -- the TypeS of the indexes of c
+    conIx   : TermS (extScope mempty ixs) (concatRScope pars (fieldScope c))                -- how the indexes are constructred given parameters and c indices
 open Constructor public
 
 {-# COMPILE AGDA2HS Constructor #-}
 
-record Datatype (@0 pars : Scope Name) (@0 ixs : Scope Name) : Set where
+record Datatype (@0 pars : RScope Name) (@0 ixs : RScope Name) : Set where
   field
     dataConstructorScope : Scope Name
-    dataSort             : Sort pars
-    dataParTypeS         : TypeS pars mempty
-    dataIxTypeS         : TypeS ixs pars
+    dataSort             : Sort (extScope mempty pars)
+    dataParTypeS         : TypeS mempty pars
+    dataIxTypeS         : TypeS (extScope mempty pars) ixs
     dataConstructors     : ((⟨ c ⟩ cp) : NameIn  dataConstructorScope)
                          → Σ (c ∈ conScope) (λ p → Constructor pars ixs (⟨ c ⟩ p))
 open Datatype public
@@ -181,3 +181,4 @@ opaque
         Δ₂ = subst0 (λ α₀ → Telescope α₀ γ) (sym (associativity (~ β) [ x ] α)) Δ₁
     ⌈ x ∶ ty ◃ addTel Σ Δ₂ ⌉
 -}
+ 

src/Agda/Core/Substitute.agda

@@ -1,7 +1,10 @@
 open import Scope
 
-open import Haskell.Prelude hiding (All; c; t)
+open import Haskell.Prelude hiding (All; coerce; a; b; c; t)
 open import Haskell.Extra.Dec
+open import Haskell.Law.Equality using (subst0; sym; trans)
+open import Haskell.Law.Monoid.Def using (leftIdentity; rightIdentity)
+open import Haskell.Law.Semigroup.Def using (associativity)
 open import Haskell.Extra.Erase
 
 open import Utils.Either
@@ -18,16 +21,118 @@ module Agda.Core.Substitute
 private variable
   @0 x c     : Name
   @0 α β γ cs : Scope Name
+  @0 rγ : RScope Name
   t : @0 Scope Name → Set
 
+data Subst : (@0 α β : Scope Name) → Set where
+  SNil  : Subst mempty β
+  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 ⌉
+
+rezzSubst : α ⇒ β → Rezz α
+rezzSubst ⌈⌉ = rezz mempty
+rezzSubst ⌈ σ ◃ x ↦ u ⌉ = rezzBind (rezzSubst σ)
+
+weakenSubst : α ⊆ β → γ ⇒ α → γ ⇒ β
+weakenSubst p ⌈⌉ = ⌈⌉
+weakenSubst p ⌈ s ◃ x ↦ t ⌉ = ⌈ weakenSubst p s ◃ x ↦ weaken p t ⌉
+
+instance
+  iWeakenSubst : Weaken (Subst γ)
+  iWeakenSubst .weaken = weakenSubst
+  {-# COMPILE AGDA2HS iWeakenSubst #-}
+
+lookupSubst : α ⇒ β
+            → (@0 x : Name)
+            → x ∈ α
+            → Term β
+lookupSubst ⌈⌉ x q = inEmptyCase q
+lookupSubst ⌈ f ◃ _ ↦ u ⌉ x q = inBindCase q (λ _ → u) (lookupSubst f x)
+
+{-# COMPILE AGDA2HS lookupSubst #-}
+
+concatSubst : α ⇒ γ → β ⇒ γ → (α <> β) ⇒ γ
+concatSubst ⌈⌉ q =
+  subst0 (λ α → α ⇒ _) (sym (leftIdentity _)) q
+concatSubst ⌈ p ◃ _ ↦ v ⌉ q =
+  subst0 (λ α → α ⇒ _) (associativity _ _ _) ⌈ concatSubst p q ◃ _ ↦ v ⌉
+
+{-# COMPILE AGDA2HS concatSubst #-}
+
+opaque
+  unfolding Scope Sub
+
+  subToSubst : Rezz α → α ⊆ β → α ⇒ β
+  subToSubst (rezz []) p = ⌈⌉
+  subToSubst (rezz (Erased x ∷ α)) p =
+    ⌈ (subToSubst (rezz α) (joinSubRight (rezz _) p)) ◃ x ↦ (TVar (⟨ x ⟩ coerce p inHere)) ⌉
+
+{-# COMPILE AGDA2HS subToSubst #-}
+
+
+opaque
+  unfolding Scope revScope
+
+  revSubstAcc : {@0 α β γ : Scope Name} → α ⇒ γ → β ⇒ γ → (revScopeAcc α β) ⇒ γ
+  revSubstAcc ⌈⌉ p = p
+  revSubstAcc ⌈ s ◃ y ↦ x ⌉ p = revSubstAcc s ⌈ p ◃ y ↦ x ⌉
+  {-# COMPILE AGDA2HS revSubstAcc #-}
+
+  revSubst : {@0 α β : Scope Name} → α ⇒ β → ~ α ⇒ β
+  revSubst = flip revSubstAcc ⌈⌉
+  {-# COMPILE AGDA2HS revSubst #-}
+
+liftSubst : {@0 α β γ : Scope Name} → Rezz α → β ⇒ γ → (α <> β) ⇒ (α <> γ)
+liftSubst r f =
+  concatSubst (subToSubst r (subJoinHere r subRefl))
+              (weaken (subJoinDrop r subRefl) f)
+{-# COMPILE AGDA2HS liftSubst #-}
+
+{-# COMPILE AGDA2HS liftSubst #-}
+idSubst : {@0 β : Scope Name} → Rezz β → β ⇒ β
+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 = ⌈ (weaken (subBindDrop subRefl) e) ◃ _ ↦ (TVar (⟨ y ⟩ inHere)) ⌉
+{-# COMPILE AGDA2HS liftBindSubst #-}
+
+raiseSubst : {@0 α β : Scope Name} → Rezz β → α ⇒ β → (α <> β) ⇒ β
+raiseSubst {β = β} r ⌈⌉ = subst0 (λ α → α ⇒ β) (sym (leftIdentity β)) (idSubst r)
+raiseSubst {β = β} r (SCons {α = α} u e) =
+  subst0 (λ α → α ⇒ β)
+    (associativity (singleton _) α β)
+    ⌈ raiseSubst r e ◃ _ ↦ u ⌉
+{-# COMPILE AGDA2HS raiseSubst #-}
+
+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' #-}
+
+substExtScope : α ⇒ β → (Rezz rγ) → (extScope α rγ) ⇒ (extScope β rγ)
+substExtScope p (rezz Nil) = p
+substExtScope p (rezz (x ◂ rγ)) = substExtScope (liftBindSubst p) (rezz rγ)
 
 substTerm     : α ⇒ β → Term α → Term β
 substSort     : α ⇒ β → Sort α → Sort β
 substType     : α ⇒ β → Type α → Type β
 substBranch   : α ⇒ β → Branch α c → Branch β c
 substBranches : α ⇒ β → Branches α cs → Branches β cs
-substSubst    : α ⇒ β → γ ⇒ α → γ ⇒ β
-substTypeS   : α ⇒ β → γ ⇛ α → γ ⇛ β
+substTermS   : α ⇒ β → TermS α rγ → TermS β rγ
+substTypeS   : α ⇒ β → TypeS α rγ → TypeS β rγ
 
 substSort f (STyp x) = STyp x
 {-# COMPILE AGDA2HS substSort #-}
@@ -37,35 +142,35 @@ substType f (El st t) = El (substSort f st) (substTerm f t)
 
 substTerm f (TVar (⟨ x ⟩ k))  = lookupSubst f x k
 substTerm f (TDef d)          = TDef d
-substTerm f (TData d ps is)   = TData d (substSubst f ps) (substSubst f is)
-substTerm f (TCon c vs)       = TCon c (substSubst f vs)
+substTerm f (TData d ps is)   = TData d (substTermS f ps) (substTermS f is)
+substTerm f (TCon c vs)       = TCon c (substTermS f vs)
 substTerm f (TLam x v)        = TLam x (substTerm (liftBindSubst f) v)
 substTerm f (TApp u v)        = TApp (substTerm f u) (substTerm f v)
 substTerm f (TProj u p)       = TProj (substTerm f u) p
 substTerm f (TCase {x = x} d r u bs m) =
   TCase {x = x} d r
     (substTerm f u)
     (substBranches f bs)
-    (substType (liftBindSubst (liftSubst r f)) m)
+    (substType (liftBindSubst (substExtScope f r)) 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 r f) u)
+substBranch f (BBranch c r u) = BBranch c r (substTerm (substExtScope f r) u)
 {-# COMPILE AGDA2HS substBranch #-}
 
 substBranches f BsNil = BsNil
 substBranches f (BsCons b bs) = BsCons (substBranch f b) (substBranches f bs)
 {-# COMPILE AGDA2HS substBranches #-}
 
-substSubst f SNil = SNil
-substSubst f (SCons x e) = SCons (substTerm f x) (substSubst f e)
-{-# COMPILE AGDA2HS substSubst #-}
+substTermS f ⌈⌉ = ⌈⌉
+substTermS f (_ ↦ x ◂ e) = TSCons (substTerm f x) (substTermS f e)
+{-# COMPILE AGDA2HS substTermS #-}
 
 substTypeS f ⌈⌉ = ⌈⌉
-substTypeS f ⌈ e ◃ _ ∶ x ⌉ = YCons (substType f x) (substTypeS f e)
+substTypeS {rγ = x ◂ rγ} f (_ ∶ u ◂ e) = YCons (substType (substExtScope {rγ = rγ} f (rezzTypeS e)) u) (substTypeS f e)
 {-# COMPILE AGDA2HS substTypeS #-}
 
 record Substitute (t : @0 Scope Name → Set) : Set where
@@ -84,16 +189,16 @@ instance
   iSubstBranch .subst = substBranch
   iSubstBranches : Substitute (λ α → Branches α cs)
   iSubstBranches .subst = substBranches
-  iSubstSubst : Substitute (Subst α)
-  iSubstSubst .subst = substSubst
-  iSubstTypeS : Substitute (TypeS α)
+  iSubstTermS : Substitute (λ α → TermS α rγ)
+  iSubstTermS .subst = substTermS
+  iSubstTypeS : Substitute (λ α → TypeS α rγ)
   iSubstTypeS .subst = substTypeS
 {-# COMPILE AGDA2HS iSubstTerm #-}
 {-# COMPILE AGDA2HS iSubstType #-}
 {-# COMPILE AGDA2HS iSubstSort #-}
 {-# COMPILE AGDA2HS iSubstBranch #-}
 {-# COMPILE AGDA2HS iSubstBranches #-}
-{-# COMPILE AGDA2HS iSubstSubst #-}
+{-# COMPILE AGDA2HS iSubstTermS #-}
 {-# COMPILE AGDA2HS iSubstTypeS #-}
 
 substTop : {{Substitute t}} → Rezz α → Term α → t (x ◃ α) → t α