5 changed files with 199 additions and 69 deletions
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@ -84,7 +84,11 @@ DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim


-public export FromVar Dim where fromVar = B
+public export
+FromVarR Dim where fromVarR = B
+
+public export
+FromVar Dim where fromVar = B; fromVarSame _ _ = Refl


 export
@ -92,10 +96,16 @@ CanShift Dim where
  K e loc // _  = K e loc
  B i loc // by = B (i // by) loc

+private
+substDim : Dim from -> Lazy (DSubst from to) -> Dim to
+substDim (K e loc) _  = K e loc
+substDim (B i loc) th = get th i loc
+
 export
-CanSubstSelf Dim where
-  K e loc // _  = K e loc
-  B i loc // th = get th i loc
+CanSubstSelfR Dim where (//?) = substDim
+
+export
+CanSubstSelf Dim where (//) = substDim; substSame _ _ = Refl


 export Uninhabited (B i loc1 = K e loc2) where uninhabited _ impossible
--- a/lib/Quox/Syntax/Subst.idr
+++ b/lib/Quox/Syntax/Subst.idr
@ -42,12 +42,28 @@ export Ord  (f to) => Ord  (Subst f from to) where compare = compare `on` repr
 export Show (f to) => Show (Subst f from to) where show = show . repr


-export infixl 8 //
-public export
-interface FromVar term => CanSubstSelf term where
-  (//) : term from -> Lazy (Subst term from to) -> term to
+export infixl 8 //?, //


+public export
+interface FromVarR term => CanSubstSelfR term where
+  (//?) : {from, to : Nat} ->
+          term from -> Lazy (Subst term from to) -> term to
+
+public export
+interface (FromVar term, CanSubstSelfR term) => CanSubstSelf term where
+  (//) : term from -> Lazy (Subst term from to) -> term to
+  0 substSame : (t : term from) -> (th : Subst term from to) ->
+                t //? th === t // th
+
+
+public export
+getR : {to : Nat} -> FromVarR term =>
+       Subst term from to -> Var from -> Loc -> term to
+getR (Shift by) i      loc = fromVarR (shift by i) loc
+getR (t ::: th) VZ     _   = t
+getR (t ::: th) (VS i) loc = getR th i loc
+
 public export
 get : FromVar term => Subst term from to -> Var from -> Loc -> term to
 get (Shift by) i      loc = fromVar (shift by i) loc
@ -56,10 +72,16 @@ get (t ::: th) (VS i) loc = get th i loc


 public export
-CanSubstSelf Var where
-  i    // Shift by   = shift by i
-  VZ   // (t ::: th) = t
-  VS i // (t ::: th) = i // th
+substVar : Var from -> Lazy (Subst Var from to) -> Var to
+substVar i      (Shift by) = shift by i
+substVar VZ     (t ::: th) = t
+substVar (VS i) (t ::: th) = substVar i th
+
+public export
+CanSubstSelfR Var where (//?) = substVar
+
+public export
+CanSubstSelf Var where (//) = substVar; substSame _ _ = Refl


 public export %inline
@ -71,6 +93,16 @@ shift0 : (by : Nat) -> Subst env 0 by
 shift0 by = rewrite sym $ plusZeroRightNeutral by in Shift $ fromNat by


+export infixr 9 .?
+
+public export
+(.?) : CanSubstSelfR f => {from, mid, to : Nat} ->
+       Subst f from mid -> Subst f mid to -> Subst f from to
+Shift by      .? Shift bz   = Shift $ by . bz
+Shift SZ      .? ph         = ph
+Shift (SS by) .? (t ::: th) = Shift by .? th
+(t ::: th)    .? ph         = (t //? ph) ::: (th .? ph)
+
 public export
 (.) : CanSubstSelf f => Subst f from mid -> Subst f mid to -> Subst f from to
 Shift by      . Shift bz   = Shift $ by . bz
@ -78,6 +110,7 @@ Shift SZ      . ph         = ph
 Shift (SS by) . (t ::: th) = Shift by . th
 (t ::: th)    . ph         = (t // ph) ::: (th . ph)

+
 public export %inline
 id : Subst f n n
 id = shift 0
@ -95,11 +128,20 @@ map f (Shift by) = Shift by
 map f (t ::: th) = f t ::: map f th


-public export %inline
-push : CanSubstSelf f => Loc -> Subst f from to -> Subst f (S from) (S to)
-push loc th = fromVar VZ loc ::: (th . shift 1)
+public export
+pushNR : {from, to : Nat} -> CanSubstSelfR f => (s : Nat) -> Loc ->
+         Subst f from to -> Subst f (s + from) (s + to)
+pushNR 0     _   th = th
+pushNR (S s) loc th =
+  rewrite plusSuccRightSucc s from in
+  rewrite plusSuccRightSucc s to in
+  pushNR s loc $ fromVarR VZ loc ::: (th .? shift 1)
+
+public export %inline
+pushR : {from, to : Nat} -> CanSubstSelfR f =>
+        Loc -> Subst f from to -> Subst f (S from) (S to)
+pushR = pushNR 1

-- [fixme] a better way to do this?
 public export
 pushN : CanSubstSelf f => (s : Nat) -> Loc ->
        Subst f from to -> Subst f (s + from) (s + to)
@ -109,6 +151,10 @@ pushN (S s) loc th =
  rewrite plusSuccRightSucc s to in
  pushN s loc $ fromVar VZ loc ::: (th . shift 1)

+public export %inline
+push : CanSubstSelf f => Loc -> Subst f from to -> Subst f (S from) (S to)
+push = pushN 1
+
 public export
 drop1 : Subst f (S from) to -> Subst f from to
 drop1 (Shift by) = Shift $ ssDown by
@ -167,3 +213,30 @@ export %hint
 ShowWithSubst : (Show (env n), forall n. Show (tm n)) =>
                Show (WithSubst tm env n)
 ShowWithSubst = deriveShow
+
+public export
+record WithSubstR tm env n where
+  constructor SubR
+  {from : Nat}
+  term  : tm from
+  subst : Lazy (Subst env from n)
+
+export
+(Eq (env n), forall n. Eq (tm n)) => Eq (WithSubstR tm env n) where
+  SubR {from = m1} t1 s1 == SubR {from = m2} t2 s2 =
+    case decEq m1 m2 of
+      Yes Refl => t1 == t2 && s1 == s2
+      No  _    => False
+
+export
+(Ord (env n), forall n. Ord (tm n)) => Ord (WithSubstR tm env n) where
+  SubR {from = m1} t1 s1 `compare` SubR {from = m2} t2 s2 =
+    case cmp m1 m2 of
+      CmpLT _ => LT
+      CmpEQ   => compare (t1, s1) (t2, s2)
+      CmpGT _ => GT
+
+export %hint
+ShowWithSubstR : (Show (env n), forall n. Show (tm n)) =>
+                 Show (WithSubstR tm env n)
+ShowWithSubstR = deriveShow
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@ -60,9 +60,31 @@ namespace DSubst.DScopeTermN
  S ns (N body) // th = S ns $ N $ body // th


-export %inline FromVar (Elim d) where fromVar = B
-export %inline FromVar (Term d) where fromVar = E .: fromVar
+export %inline
+FromVarR (Elim d) where fromVarR = B

+export %inline
+FromVar (Elim d) where fromVar = B; fromVarSame _ _ = Refl
+
+export %inline
+FromVarR (Term d) where fromVarR = E .: fromVarR
+
+export %inline
+FromVar (Term d) where fromVar = E .: fromVar; fromVarSame _ _ = Refl
+
+
+export
+CanSubstSelf (Elim d)
+
+private
+tsubstElim : Elim d from -> Lazy (TSubst d from to) -> Elim d to
+tsubstElim (F x u loc)       _  = F x u loc
+tsubstElim (B i loc)         th = get th i loc
+tsubstElim (CloE (Sub e ph)) th = assert_total CloE $ Sub e $ ph . th
+tsubstElim e                 th =
+  case force th of
+       Shift SZ => e
+       th       => CloE $ Sub e th

 ||| does the minimal reasonable work:
 ||| - deletes the closure around a *free* name
@ -70,14 +92,10 @@ export %inline FromVar (Term d) where fromVar = E .: fromVar
 ||| - composes (lazily) with an existing top-level closure
 ||| - immediately looks up a bound variable
 ||| - otherwise, wraps in a new closure
+CanSubstSelfR (Elim d) where (//?) = tsubstElim
+
 export
-CanSubstSelf (Elim d) where
-  F x u loc       // _  = F x u loc
-  B i loc         // th = get th i loc
-  CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th
-  e               // th = case force th of
-                               Shift SZ => e
-                               th       => CloE $ Sub e th
+CanSubstSelf (Elim d) where (//) = tsubstElim; substSame _ _ = Refl

 namespace CanTSubst
  public export
--- a/lib/Quox/Untyped/Syntax.idr
+++ b/lib/Quox/Untyped/Syntax.idr
@ -255,49 +255,66 @@ USubst : Nat -> Nat -> Type
 USubst = Subst Term


-public export FromVar Term where fromVar = B
+public export %inline
+FromVarR Term where fromVarR = B
+
+public export %inline
+FromVar Term where fromVar = B; fromVarSame _ _ = Refl


-public export
-CanSubstSelf Term where
-  s // th = case s of
-    F x loc =>
-      F x loc
-    B i loc =>
-      get th i loc
-    Lam x body loc =>
-      Lam x (assert_total $ body // push x.loc th) loc
-    App fun arg loc =>
-      App (fun // th) (arg // th) loc
-    Pair fst snd loc =>
-      Pair (fst // th) (snd // th) loc
-    Fst pair loc =>
-      Fst (pair // th) loc
-    Snd pair loc =>
-      Snd (pair // th) loc
-    Tag tag loc =>
-      Tag tag loc
-    CaseEnum tag cases loc =>
-      CaseEnum (tag // th) (map (assert_total mapSnd (// th)) cases) loc
-    Absurd loc =>
-      Absurd loc
-    Nat n loc =>
-      Nat n loc
-    Succ nat loc =>
-      Succ (nat // th) loc
-    CaseNat nat zer suc loc =>
-      CaseNat (nat // th) (zer // th) (assert_total substSuc suc th) loc
-    Str s loc =>
-      Str s loc
-    Let u x rhs body loc =>
-      Let u x (rhs // th) (assert_total $ body // push x.loc th) loc
-    Erased loc =>
-      Erased loc
-  where
-    substSuc : forall from, to.
-               CaseNatSuc from -> USubst from to -> CaseNatSuc to
-    substSuc (NSRec    x ih t) th = NSRec    x ih $ t // pushN 2 x.loc th
-    substSuc (NSNonrec x    t) th = NSNonrec x    $ t // push    x.loc th
+export
+CanSubstSelf Term
+
+substTerm : Term from -> Lazy (USubst from to) -> Term to
+substTerm s th = case s of
+  F x loc =>
+    F x loc
+  B i loc =>
+    get th i loc
+  Lam x body loc =>
+    Lam x (assert_total substTerm body $ push x.loc th) loc
+  App fun arg loc =>
+    App (substTerm fun th) (substTerm arg th) loc
+  Pair fst snd loc =>
+    Pair (substTerm fst th) (substTerm snd th) loc
+  Fst pair loc =>
+    Fst (substTerm pair th) loc
+  Snd pair loc =>
+    Snd (substTerm pair th) loc
+  Tag tag loc =>
+    Tag tag loc
+  CaseEnum tag cases loc =>
+    CaseEnum (substTerm tag th)
+             (map (mapSnd (\b => assert_total substTerm b th)) cases) loc
+  Absurd loc =>
+    Absurd loc
+  Nat n loc =>
+    Nat n loc
+  Succ nat loc =>
+    Succ (substTerm nat th) loc
+  CaseNat nat zer suc loc =>
+    CaseNat (substTerm nat th)
+            (substTerm zer th)
+            (assert_total substSuc suc th) loc
+  Str s loc =>
+    Str s loc
+  Let u x rhs body loc =>
+    Let u x (substTerm rhs th)
+            (assert_total substTerm body $ push x.loc th) loc
+  Erased loc =>
+    Erased loc
+where
+  substSuc : forall from, to.
+             CaseNatSuc from -> Lazy (USubst from to) -> CaseNatSuc to
+  substSuc (NSRec    x ih t) th = NSRec    x ih $ substTerm t $ pushN 2 x.loc th
+  substSuc (NSNonrec x    t) th = NSNonrec x    $ substTerm t $ push    x.loc th
+
+export
+CanSubstSelfR Term where (//?) = substTerm
+
+export
+CanSubstSelf Term where (//) = substTerm; substSame _ _ = Refl
+

 public export
 subN : SnocVect s (Term n) -> Term (s + n) -> Term n
--- a/lib/Quox/Var.idr
+++ b/lib/Quox/Var.idr
@ -138,13 +138,25 @@ export
 weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)


+||| inject a variable (with a source location) into some kind of term. in this
+||| case, the scope size may be needed at run time
 public export
-interface FromVar f where %inline fromVar : Var n -> Loc -> f n
+interface FromVarR f where
+  %inline fromVarR : {n : Nat} -> Var n -> Loc -> f n
+
+||| inject a variable (with a source location) into some kind of term, without
+||| needing the scope size
+public export
+interface FromVarR f => FromVar f where
+  %inline fromVar : Var n -> Loc -> f n
+  0 fromVarSame : (i : Var n) -> (l : Loc) -> fromVarR i l === fromVar i l


-public export FromVar Var where fromVar x _ = x
-
+public export
+FromVarR Var where fromVarR x _ = x

+public export
+FromVar Var where fromVar x _ = x; fromVarSame _ _ = Refl


 public export