wip

examples/all.quox

@@ -1,6 +1,7 @@
 load "misc.quox"
 load "bool.quox"
 load "either.quox"
+load "maybe.quox"
 load "nat.quox"
 load "pair.quox"
 load "list.quox"

examples/maybe.quox

@@ -0,0 +1,69 @@
+load "misc.quox"
+load "either.quox"
+
+namespace maybe {
+
+def0 Tag : ★ = {nothing, just}
+
+def0 Payload : ω.Tag → ω.★ → ★ =
+  λ tag A ⇒ caseω tag return ★ of { 'nothing ⇒ True; 'just ⇒ A }
+
+def0 Maybe : ω.★ → ★ =
+  λ A ⇒ (t : Tag) × Payload t A
+
+def tag : 0.(A : ★) → ω.(Maybe A) → Tag =
+  λ _ x ⇒ caseω x return Tag of { (tag, _) ⇒ tag }
+
+def Nothing : 0.(A : ★) → Maybe A =
+  λ _ ⇒ ('nothing, 'true)
+
+def Just : 0.(A : ★) → 1.A → Maybe A =
+  λ _ x ⇒ ('just, x)
+
+def0 IsJustTag : ω.Tag → ★ =
+  λ t ⇒ caseω t return ★ of { 'just ⇒ True; 'nothing ⇒ False }
+
+def0 IsJust : 0.(A : ★) → ω.(Maybe A) → ★ =
+  λ A x ⇒ IsJustTag (tag A x)
+
+def is-just? : 0.(A : ★) → ω.(x : Maybe A) → Dec (IsJust A x) =
+  λ A x ⇒
+  caseω tag A x return t ⇒ Dec (IsJustTag t) of {
+    'just    ⇒ Yes True  'true;
+    'nothing ⇒ No  False (λ x ⇒ x)
+  }
+
+def0 nothing-unique :
+    0.(A : ★) → ω.(x : True) → ('nothing, x) ≡ Nothing A : Maybe A =
+  λ A x ⇒
+  caseω x return x' ⇒ ('nothing, x') ≡ Nothing A : Maybe A of {
+    'true ⇒ δ _ ⇒ ('nothing, 'true)
+  }
+
+def elim :
+    0.(A : ★) →
+    0.(P : 0.(Maybe A) → ★) →
+    ω.(P (Nothing A)) →
+    ω.(ω.(x : A) → P (Just A x)) →
+    1.(x : Maybe A) → P x =
+  λ A P n j x ⇒
+  caseω x return x' ⇒ P x' of {
+    (tag, payload) ⇒
+      (caseω tag
+       return t ⇒
+         0.(eq : tag ≡ t : Tag) → P (t, coe (i ⇒ Payload (eq @i) A) payload)
+       of {
+         'nothing ⇒
+            λ eq ⇒
+            caseω coe (i ⇒ Payload (eq @i) A) payload
+            return p ⇒ P ('nothing, p)
+            of { 'true ⇒ n };
+         'just ⇒ λ eq ⇒ j (coe (i ⇒ Payload (eq @i) A) payload)
+       }) (δ _ ⇒ tag)
+  }
+
+}
+
+def0 Maybe   = maybe.Maybe
+def0 Just    = maybe.Just
+def0 Nothing = maybe.Nothing

lib/Quox/Context.idr

@@ -6,12 +6,16 @@ import Quox.Name
 
 import Data.DPair
 import Data.Nat
+import Data.Fin
+import Data.Singleton
 import Data.SnocList
 import Data.SnocVect
 import Data.Vect
 import Control.Monad.Identity
+import Derive.Prelude
 
 %default total
+%language ElabReflection
 
 
 ||| a sequence of bindings under an existing context. each successive element
@@ -83,6 +87,13 @@ export %inline
 toSnocList' : Telescope' a _ _ -> SnocList a
 toSnocList' = toSnocListWith id
 
+export %inline
+toSnocListRelevant : {n1 : Nat} -> Telescope tm n1 n2 -> SnocList (n ** tm n)
+toSnocListRelevant tel = toSnocList' $ snd $ go tel where
+  go : Telescope tm n1 n2' -> (Singleton n2', Telescope' (n ** tm n) n1 n2')
+  go [<]        = (Val n1, [<])
+  go (tel :< x) = let (Val n, tel) = go tel in (Val (S n), tel :< (n ** x))
+
 export %inline
 toList : Telescope tm _ _ -> List (Exists tm)
 toList = toListWith (Evidence _)
@@ -136,34 +147,34 @@ tel ++ (sx :< x) = (tel ++ sx) :< x
 
 public export
 getShiftWith : (forall from, to. tm from -> Shift from to -> tm to) ->
-               Shift len out -> Context tm len -> Var len -> tm out
-getShiftWith shft by (ctx :< t) VZ     = t `shft` ssDown by
-getShiftWith shft by (ctx :< t) (VS i) = getShiftWith shft (ssDown by) ctx i
+               Shift len out -> Context tm len -> Fin len -> tm out
+getShiftWith shft by (ctx :< t) FZ     = t `shft` ssDown by
+getShiftWith shft by (ctx :< t) (FS i) = getShiftWith shft (ssDown by) ctx i
 
 public export %inline
-getShift : CanShift tm => Shift len out -> Context tm len -> Var len -> tm out
+getShift : CanShift tm => Shift len out -> Context tm len -> Fin len -> tm out
 getShift = getShiftWith (//)
 
 public export %inline
 getWith : (forall from, to. tm from -> Shift from to -> tm to) ->
-          Context tm len -> Var len -> tm len
+          Context tm len -> Fin len -> tm len
 getWith shft = getShiftWith shft SZ
 
 infixl 8 !!
 public export %inline
-(!!) : CanShift tm => Context tm len -> Var len -> tm len
+(!!) : CanShift tm => Context tm len -> Fin len -> tm len
 (!!) = getWith (//)
 
 infixl 8 !!!
 public export %inline
-(!!!) : Context' tm len -> Var len -> tm
+(!!!) : Context' tm len -> Fin len -> tm
 (!!!) = getWith const
 
 public export
 find : Alternative f =>
-       (forall n. tm n -> Bool) -> Context tm len -> f (Var len)
+       (forall n. tm n -> Bool) -> Context tm len -> f (Fin len)
 find p [<]        = empty
-find p (ctx :< x) = (guard (p x) $> VZ) <|> (VS <$> find p ctx)
+find p (ctx :< x) = (guard (p x) $> FZ) <|> (FS <$> find p ctx)
 
 
 export
@@ -320,6 +331,14 @@ export %inline
     where Show (Exists tm) where showPrec d t = showPrec d t.snd
 
 
+export
+implementation [ShowTelRelevant]
+  {n1 : Nat} -> ({n : Nat} -> Show (f n)) => Show (Telescope f n1 n2)
+where
+  showPrec d = showPrec d . toSnocListRelevant
+    where Show (n : Nat ** f n) where showPrec d (_ ** t) = showPrec d t
+
+
 parameters {opts : LayoutOpts} {0 tm : Nat -> Type}
            (nameHL : HL)
            (pterm : forall n. BContext n -> tm n -> Eff Pretty (Doc opts))

lib/Quox/FinExtra.idr

@@ -0,0 +1,44 @@
+module Quox.FinExtra
+
+import public Data.Fin
+import Quox.Decidable
+
+public export
+data LT : Rel (Fin n) where
+  LTZ : FZ `LT` FS i
+  LTS : i `LT` j -> FS i `LT` FS j
+%builtin Natural FinExtra.LT
+%name FinExtra.LT lt
+
+public export %inline
+GT : Rel (Fin n)
+GT = flip LT
+
+export
+Transitive (Fin n) LT where
+  transitive LTZ     (LTS _) = LTZ
+  transitive (LTS p) (LTS q) = LTS $ transitive p q
+
+export Uninhabited (i `FinExtra.LT` i) where uninhabited (LTS p) = uninhabited p
+export Uninhabited (FS i `LT` FZ) where uninhabited _ impossible
+
+
+public export
+data Compare : Rel (Fin n) where
+  IsLT : (lt : i `LT` j) -> Compare i j
+  IsEQ :                    Compare i i
+  IsGT : (gt : i `GT` j) -> Compare i j
+%name Compare cmp
+
+export
+compareS : Compare i j -> Compare (FS i) (FS j)
+compareS (IsLT lt) = IsLT (LTS lt)
+compareS IsEQ      = IsEQ
+compareS (IsGT gt) = IsGT (LTS gt)
+
+export
+compareP : (i, j : Fin n) -> Compare i j
+compareP FZ     FZ     = IsEQ
+compareP FZ     (FS j) = IsLT LTZ
+compareP (FS i) FZ     = IsGT LTZ
+compareP (FS i) (FS j) = compareS $ compareP i j

lib/Quox/NatExtra.idr

@@ -1,12 +1,19 @@
 module Quox.NatExtra
 
 import public Data.Nat
+import public Data.Nat.Views
 import Data.Nat.Division
 import Data.SnocList
 import Data.Vect
+import Syntax.PreorderReasoning
 
 %default total
 
+infixl 8 `shiftL`, `shiftR`
+infixl 7 .&.
+infixl 6 `xor`
+infixl 5 .|.
+
 
 public export
 data LTE' : Nat -> Nat -> Type where
@@ -55,3 +62,148 @@ parameters {base : Nat} {auto 0 _ : base `GTE` 2} (chars : Vect base Char)
 export
 showHex : Nat -> String
 showHex = showAtBase $ fromList $ unpack "0123456789ABCDEF"
+
+
+export
+0 notEvenOdd : (a, b : Nat) -> Not (a + a = S (b + b))
+notEvenOdd 0     b prf = absurd prf
+notEvenOdd (S a) b prf =
+  notEvenOdd b a $ Calc $
+    |~ b + b
+    ~~ a + S a   ..<(inj S prf)
+    ~~ S (a + a) ..<(plusSuccRightSucc {})
+
+export
+0 doubleInj : (m, n : Nat) -> m + m = n + n -> m = n
+doubleInj 0     0     _   = Refl
+doubleInj (S m) (S n) prf =
+  cong S $ doubleInj m n $
+  inj S $ Calc $
+    |~ S (m + m)
+    ~~ m + S m   ...(plusSuccRightSucc {})
+    ~~ n + S n   ...(inj S prf)
+    ~~ S (n + n) ..<(plusSuccRightSucc {})
+
+export
+0 halfDouble : (n : Nat) -> half (n + n) = HalfEven n
+halfDouble n with (half (n + n)) | (n + n) proof nn
+  _ | HalfOdd  k | S (k + k) = void $ notEvenOdd n k nn
+  _ | HalfEven k | k + k     = rewrite doubleInj n k nn in Refl
+
+export
+floorHalf : Nat -> Nat
+floorHalf k = case half k of
+  HalfOdd  n => n
+  HalfEven n => n
+
+
+||| like in intercal ☺
+|||
+||| take all the bits of `subj` that are set in `mask`, and squish them down
+||| towards the lsb
+public export
+select : (mask, subj : Nat) -> Nat
+select mask subj = go 1 (halfRec mask) subj 0 where
+  go : forall mask. Nat -> HalfRec mask -> Nat -> Nat -> Nat
+  go bit HalfRecZ            subj res = res
+  go bit (HalfRecEven _ rec) subj res = go bit rec (floorHalf subj) res
+  go bit (HalfRecOdd  _ rec) subj res = case half subj of
+    HalfOdd  subj => go (bit + bit) rec subj (res + bit)
+    HalfEven subj => go (bit + bit) rec subj res
+
+||| take the i least significant bits of subj (where i = popCount mask),
+||| and place them where mask's set bits are
+|||
+||| left inverse of select if mask .|. subj = mask
+public export
+spread : (mask, subj : Nat) -> Nat
+spread mask subj = go 1 (halfRec mask) subj 0 where
+  go : forall mask. Nat -> HalfRec mask -> Nat -> Nat -> Nat
+  go bit HalfRecZ            subj res = res
+  go bit (HalfRecEven _ rec) subj res = go (bit + bit) rec subj res
+  go bit (HalfRecOdd  _ rec) subj res = case half subj of
+    HalfOdd  subj => go (bit + bit) rec subj (res + bit)
+    HalfEven subj => go (bit + bit) rec subj res
+
+
+
+public export
+data BitwiseRec : Nat -> Nat -> Type where
+  BwDone : BitwiseRec 0 0
+  Bw00   : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
+           BitwiseRec (m + m) (n + n)
+  Bw01   : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
+           BitwiseRec (m + m) (S (n + n))
+  Bw10   : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
+           BitwiseRec (S (m + m)) (n + n)
+  Bw11   : (m, n : Nat) -> Lazy (BitwiseRec m n) ->
+           BitwiseRec (S (m + m)) (S (n + n))
+
+export
+bitwiseRec : (m, n : Nat) -> BitwiseRec m n
+bitwiseRec m n = go (halfRec m) (halfRec n) where
+  go : forall m, n. HalfRec m -> HalfRec n -> BitwiseRec m n
+  go HalfRecZ           HalfRecZ           = BwDone
+  go HalfRecZ           (HalfRecEven n nr) = Bw00 0 n $ go HalfRecZ nr
+  go HalfRecZ           (HalfRecOdd  n nr) = Bw01 0 n $ go HalfRecZ nr
+  go (HalfRecEven m mr) HalfRecZ           = Bw00 m 0 $ go mr HalfRecZ
+  go (HalfRecEven m mr) (HalfRecEven n nr) = Bw00 m n $ go mr nr
+  go (HalfRecEven m mr) (HalfRecOdd  n nr) = Bw01 m n $ go mr nr
+  go (HalfRecOdd  m mr) HalfRecZ           = Bw10 m 0 $ go mr HalfRecZ
+  go (HalfRecOdd  m mr) (HalfRecEven n nr) = Bw10 m n $ go mr nr
+  go (HalfRecOdd  m mr) (HalfRecOdd  n nr) = Bw11 m n $ go mr nr
+
+public export
+bitwise : (Bool -> Bool -> Bool) -> Nat -> Nat -> Nat
+bitwise f m n = go 1 (bitwiseRec m n) 0 where
+  one : Bool -> Bool -> Nat -> Nat -> Nat
+  one p q bit res = if f p q then bit + res else res
+  go : forall m, n. Nat -> BitwiseRec m n -> Nat -> Nat
+  go bit BwDone         res = res
+  go bit (Bw00 m n rec) res = go (bit + bit) rec $ one False False bit res
+  go bit (Bw01 m n rec) res = go (bit + bit) rec $ one False True  bit res
+  go bit (Bw10 m n rec) res = go (bit + bit) rec $ one True  False bit res
+  go bit (Bw11 m n rec) res = go (bit + bit) rec $ one True  True  bit res
+
+public export
+(.&.) : Nat -> Nat -> Nat
+(.&.) = bitwise $ \p, q => p && q
+
+private %foreign "scheme:blodwen-and"
+primAnd : Nat -> Nat -> Nat
+%transform "NatExtra.(.&.)" NatExtra.(.&.) m n = primAnd m n
+
+public export
+(.|.) : Nat -> Nat -> Nat
+(.|.) = bitwise $ \p, q => p || q
+
+private %foreign "scheme:blodwen-or"
+primOr : Nat -> Nat -> Nat
+%transform "NatExtra.(.|.)" NatExtra.(.|.) m n = primOr m n
+
+public export
+xor : Nat -> Nat -> Nat
+xor = bitwise (/=)
+
+private %foreign "scheme:blodwen-xor"
+primXor : Nat -> Nat -> Nat
+%transform "NatExtra.xor" NatExtra.xor m n = primXor m n
+
+
+public export
+shiftL : Nat -> Nat -> Nat
+shiftL n 0     = n
+shiftL n (S i) = shiftL (n + n) i
+
+private %foreign "scheme:blodwen-shl"
+primShiftL : Nat -> Nat -> Nat
+%transform "NatExtra.shiftL" NatExtra.shiftL n i = primShiftL n i
+
+public export
+shiftR : Nat -> Nat -> Nat
+shiftR n 0     = n
+shiftR n (S i) = shiftL (floorHalf n) i
+
+private %foreign "scheme:blodwen-shr"
+primShiftR : Nat -> Nat -> Nat
+%transform "NatExtra.shiftR" NatExtra.shiftR n i = primShiftR n i

lib/Quox/Syntax/Dim.idr

@@ -1,15 +1,18 @@
 module Quox.Syntax.Dim
 
-import Quox.Loc
-import Quox.Name
+import Quox.Thin
 import Quox.Syntax.Var
 import Quox.Syntax.Subst
 import Quox.Pretty
+import Quox.Name
+import Quox.Loc
 import Quox.Context
 
 import Decidable.Equality
 import Control.Function
 import Derive.Prelude
+import Data.DPair
+import Data.SnocVect
 
 %default total
 %language ElabReflection
@@ -39,38 +42,48 @@ DecEq DimConst where
 
 public export
 data Dim : Nat -> Type where
-  K : DimConst -> Loc -> Dim d
-  B : Var d -> Loc -> Dim d
+  K : DimConst -> Loc -> Dim 0
+  B : Loc -> Dim 1
 %name Dim.Dim p, q
 %runElab deriveIndexed "Dim" [Eq, Ord, Show]
 
 
+public export
+DimT : Nat -> Type
+DimT = Thinned Dim
+
+public export %inline
+KT : DimConst -> Loc -> DimT d
+KT e loc = Th zero $ K e loc
+
+
 ||| `endsOr l r x p` returns `ends l r ε` if `p` is a constant ε, and
 ||| `x` otherwise.
 public export
 endsOr : Lazy a -> Lazy a -> Lazy a -> Dim n -> a
 endsOr l r x (K e _) = ends l r e
-endsOr l r x (B _ _) = x
+endsOr l r x (B _)   = x
 
 
 export
 Located (Dim d) where
   (K _ loc).loc = loc
-  (B _ loc).loc = loc
+  (B loc).loc   = loc
 
 export
 Relocatable (Dim d) where
   setLoc loc (K e _) = K e loc
-  setLoc loc (B i _) = B i loc
+  setLoc loc (B _)   = B loc
 
-export
-prettyDimConst : {opts : _} -> DimConst -> Eff Pretty (Doc opts)
-prettyDimConst = hl Dim . text . ends "0" "1"
+parameters {opts : LayoutOpts}
+  export
+  prettyDimConst : DimConst -> Eff Pretty (Doc opts)
+  prettyDimConst = hl Dim . text . ends "0" "1"
 
-export
-prettyDim : {opts : _} -> BContext d -> Dim d -> Eff Pretty (Doc opts)
-prettyDim names (K e _) = prettyDimConst e
-prettyDim names (B i _) = prettyDBind $ names !!! i
+  export
+  prettyDim : {d : Nat} -> BContext d -> DimT d -> Eff Pretty (Doc opts)
+  prettyDim names (Th _ (K e _)) = prettyDimConst e
+  prettyDim names (Th i (B _)) = prettyDBind $ names !!! i.fin
 
 
 public export %inline
@@ -83,57 +96,54 @@ DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim
 
 
-public export FromVar Dim where fromVarLoc = B
+-- public export FromVar Dim where fromVarLoc = B
 
 
-export
-CanShift Dim where
-  K e loc // _  = K e loc
-  B i loc // by = B (i // by) loc
+-- export
+-- CanShift Dim where
+--   K e loc // _  = K e loc
+--   B i loc // by = B (i // by) loc
 
-export
+export %inline FromVar Dim where var = B
+
+export %inline
 CanSubstSelf Dim where
-  K e loc // _  = K e loc
-  B i loc // th = getLoc th i loc
+  Th _ (K e loc) // _  = KT e loc
+  Th i (B loc)   // th = get th i.fin
 
 
-export Uninhabited (B i loc1 = K e loc2) where uninhabited _ impossible
-export Uninhabited (K e loc1 = B i loc2) where uninhabited _ impossible
+export Uninhabited (B loc1   = K e loc2) where uninhabited _ impossible
+export Uninhabited (K e loc1 = B loc2)   where uninhabited _ impossible
 
-public export
-data Eqv : Dim d1 -> Dim d2 -> Type where
-  EK : K e _ `Eqv` K e _
-  EB : i `Eqv` j -> B i _ `Eqv` B j _
+-- public export
+-- data Eqv : Dim d1 -> Dim d2 -> Type where
+--   EK : K e _ `Eqv` K e _
+--   EB : i `Eqv` j -> B i _ `Eqv` B j _
 
-export Uninhabited (K e l1 `Eqv` B i l2) where uninhabited _ impossible
-export Uninhabited (B i l1 `Eqv` K e l2) where uninhabited _ impossible
+-- export Uninhabited (K e l1 `Eqv` B i l2) where uninhabited _ impossible
+-- export Uninhabited (B i l1 `Eqv` K e l2) where uninhabited _ impossible
 
-export
-injectiveB : B i loc1 `Eqv` B j loc2 -> i `Eqv` j
-injectiveB (EB e) = e
+-- export
+-- injectiveB : B i loc1 `Eqv` B j loc2 -> i `Eqv` j
+-- injectiveB (EB e) = e
 
-export
-injectiveK : K e loc1 `Eqv` K f loc2 -> e = f
-injectiveK EK = Refl
+-- export
+-- injectiveK : K e loc1 `Eqv` K f loc2 -> e = f
+-- injectiveK EK = Refl
 
-public export
-decEqv : Dec2 Dim.Eqv
-decEqv (K e _) (K f _) = case decEq e f of
-  Yes Refl => Yes EK
-  No  n    => No $ n . injectiveK
-decEqv (B i _) (B j _) = case decEqv i j of
-  Yes y => Yes $ EB y
-  No  n => No  $ \(EB y) => n y
-decEqv (B _ _) (K _ _) = No absurd
-decEqv (K _ _) (B _ _) = No absurd
+-- public export
+-- decEqv : Dec2 Dim.Eqv
+-- decEqv (K e _) (K f _) = case decEq e f of
+--   Yes Refl => Yes EK
+--   No  n    => No $ n . injectiveK
+-- decEqv (B i _) (B j _) = case decEqv i j of
+--   Yes y => Yes $ EB y
+--   No  n => No  $ \(EB y) => n y
+-- decEqv (B _ _) (K _ _) = No absurd
+-- decEqv (K _ _) (B _ _) = No absurd
 
 ||| abbreviation for a bound variable like `BV 4` instead of
 ||| `B (VS (VS (VS (VS VZ))))`
 public export %inline
-BV : (i : Nat) -> (0 _ : LT i d) => (loc : Loc) -> Dim d
-BV i loc = B (V i) loc
-
-
-export
-weakD : (by : Nat) -> Dim d -> Dim (by + d)
-weakD by p = p // shift by
+BV : (i : Fin d) -> (loc : Loc) -> DimT d
+BV i loc = Th (one' i) $ B loc

lib/Quox/Syntax/DimEq.idr

@@ -6,11 +6,14 @@ import public Quox.Syntax.Subst
 import public Quox.Context
 import Quox.Pretty
 import Quox.Name
+import Quox.Thin
+import Quox.FinExtra
 
 import Data.Maybe
 import Data.Nat
 import Data.DPair
 import Data.Fun.Graph
+import Data.SnocVect
 import Decidable.Decidable
 import Decidable.Equality
 import Derive.Prelude
@@ -21,7 +24,7 @@ import Derive.Prelude
 
 public export
 DimEq' : Nat -> Type
-DimEq' = Context (Maybe . Dim)
+DimEq' = Context (Maybe . DimT)
 
 
 public export
@@ -29,7 +32,12 @@ data DimEq : Nat -> Type where
   ZeroIsOne : DimEq d
   C         : (eqs : DimEq' d) -> DimEq d
 %name DimEq eqs
-%runElab deriveIndexed "DimEq" [Eq, Ord, Show]
+%runElab deriveIndexed "DimEq" [Eq]
+
+export
+Show (DimEq d) where
+  showPrec d ZeroIsOne = "ZeroIsOne"
+  showPrec d (C eq')   = showCon d "C" $ showArg eq' @{ShowTelRelevant}
 
 
 public export
@@ -72,7 +80,7 @@ toMaybe (Just x) = Just x
 export
 fromGround' : Context' DimConst d -> DimEq' d
 fromGround' [<]        = [<]
-fromGround' (ctx :< e) = fromGround' ctx :< Just (K e noLoc)
+fromGround' (ctx :< e) = fromGround' ctx :< Just (KT e noLoc)
 
 export
 fromGround : Context' DimConst d -> DimEq d
@@ -94,39 +102,40 @@ new = C new'
 
 
 public export %inline
-get' : DimEq' d -> Var d -> Maybe (Dim d)
+get' : DimEq' d -> Fin d -> Maybe (DimT d)
 get' = getWith $ \p, by => map (// by) p
 
 public export %inline
-getVar : DimEq' d -> Var d -> Loc -> Dim d
-getVar eqs i loc = fromMaybe (B i loc) $ get' eqs i
-
-public export %inline
-getShift' : Shift len out -> DimEq' len -> Var len -> Maybe (Dim out)
+getShift' : Shift len out -> DimEq' len -> Fin len -> Maybe (DimT out)
 getShift' = getShiftWith $ \p, by => map (// by) p
 
 public export %inline
-get : DimEq' d -> Dim d -> Dim d
-get _   (K e loc) = K e loc
-get eqs (B i loc) = getVar eqs i loc
+get : {d : Nat} -> DimEq' d -> DimT d -> DimT d
+get eqs p@(Th _ (K {})) = p
+get eqs p@(Th i (B _))  = fromMaybe p $ get' eqs i.fin
 
 
 public export %inline
-equal : DimEq d -> (p, q : Dim d) -> Bool
+equal : {d : Nat} -> DimEq d -> (p, q : DimT d) -> Bool
 equal ZeroIsOne p q = True
 equal (C eqs)   p q = get eqs p == get eqs q
 
 
 infixl 7 :<?
 export %inline
-(:<?) : DimEq d -> Maybe (Dim d) -> DimEq (S d)
+(:<?) : {d : Nat} -> DimEq d -> Maybe (DimT d) -> DimEq (S d)
 ZeroIsOne :<? d = ZeroIsOne
 C eqs     :<? d = C $ eqs :< map (get eqs) d
 
 
 private %inline
-ifVar : Var d -> Dim d -> Maybe (Dim d) -> Maybe (Dim d)
-ifVar i p = map $ \q => if q == B i noLoc then p else q
+isVar : {d : Nat} -> Fin d -> DimT d -> Bool
+isVar i (Th j (B _))  = i == j.fin
+isVar i (Th _ (K {})) = False
+
+private %inline
+ifVar : {d : Nat} -> Fin d -> DimT d -> Maybe (DimT d) -> Maybe (DimT d)
+ifVar i p = map $ \q => if isVar i q then p else q
 
 -- (using decEq instead of (==) because of the proofs below)
 private %inline
@@ -135,43 +144,45 @@ checkConst e f eqs = if isYes $ e `decEq` f then C eqs else ZeroIsOne
 
 
 export
-setConst : Var d -> DimConst -> Loc -> DimEq' d -> DimEq d
-setConst VZ e loc (eqs :< Nothing) =
-  C $ eqs :< Just (K e loc)
-setConst VZ e _ (eqs :< Just (K f loc)) =
-  checkConst e f $ eqs :< Just (K f loc)
-setConst VZ e loc (eqs :< Just (B i _)) =
-  setConst i e loc eqs :<? Just (K e loc)
-setConst (VS i) e loc (eqs :< p) =
-  setConst i e loc eqs :<? ifVar i (K e loc) p
+setConst : {d : Nat} -> Fin d -> DimConst -> Loc -> DimEq' d -> DimEq d
+setConst FZ e loc (eqs :< Nothing) =
+  C $ eqs :< Just (KT e loc)
+setConst FZ e _ (eqs :< Just (Th _ (K f loc))) =
+  checkConst e f $ eqs :< Just (KT f loc)
+setConst FZ e loc (eqs :< Just (Th j (B _))) =
+  setConst j.fin e loc eqs :<? Just (KT e loc)
+setConst (FS i) e loc (eqs :< p) =
+  setConst i e loc eqs :<? ifVar i (KT e loc) p
 
 mutual
   private
-  setVar' : (i, j : Var d) -> (0 _ : i `LT` j) -> Loc -> DimEq' d -> DimEq d
-  setVar' VZ (VS i) LTZ loc (eqs :< Nothing) =
-    C eqs :<? Just (B i loc)
-  setVar' VZ (VS i) LTZ loc (eqs :< Just (K e eloc)) =
-    setConst i e loc eqs :<? Just (K e eloc)
-  setVar' VZ (VS i) LTZ loc (eqs :< Just (B j jloc)) =
-    setVar i j loc jloc eqs :<? Just (if j > i then B j jloc else B i loc)
-  setVar' (VS i) (VS j) (LTS lt) loc (eqs :< p) =
-    setVar' i j lt loc eqs :<? ifVar i (B j loc) p
+  setVar' : {d : Nat} ->
+            (i, j : Fin d) -> (0 _ : i `LT` j) -> Loc -> DimEq' d -> DimEq d
+  setVar' FZ (FS i) LTZ loc (eqs :< Nothing) =
+    C eqs :<? Just (BV i loc)
+  setVar' FZ (FS i) LTZ loc (eqs :< Just (Th _ (K e eloc))) =
+    setConst i e loc eqs :<? Just (KT e eloc)
+  setVar' FZ (FS i) LTZ loc (eqs :< Just (Th j (B jloc))) =
+    let j = j.fin in
+    setVar i j loc jloc eqs :<? Just (if j > i then BV j jloc else BV i loc)
+  setVar' (FS i) (FS j) (LTS lt) loc (eqs :< p) =
+    setVar' i j lt loc eqs :<? ifVar i (BV j loc) p
 
   export %inline
-  setVar : (i, j : Var d) -> Loc -> Loc -> DimEq' d -> DimEq d
-  setVar i j li lj eqs with (compareP i j) | (compare i.nat j.nat)
-    setVar i j li lj eqs | IsLT lt | LT = setVar' i j lt lj eqs
-    setVar i i li lj eqs | IsEQ    | EQ = C eqs
-    setVar i j li lj eqs | IsGT gt | GT = setVar' j i gt li eqs
+  setVar : {d : Nat} -> (i, j : Fin d) -> Loc -> Loc -> DimEq' d -> DimEq d
+  setVar i j li lj eqs with (compareP i j)
+    setVar i j li lj eqs | IsLT lt = setVar' i j lt lj eqs
+    setVar i i li lj eqs | IsEQ    = C eqs
+    setVar i j li lj eqs | IsGT gt = setVar' j i gt li eqs
 
 
 export %inline
-set : (p, q : Dim d) -> DimEq d -> DimEq d
+set : {d : Nat} -> (p, q : DimT d) -> DimEq d -> DimEq d
 set _ _ ZeroIsOne = ZeroIsOne
-set (K e eloc) (K f floc) (C eqs) = checkConst e f eqs
-set (K e eloc) (B i iloc) (C eqs) = setConst i e eloc eqs
-set (B i iloc) (K e eloc) (C eqs) = setConst i e eloc eqs
-set (B i iloc) (B j jloc) (C eqs) = setVar   i j iloc jloc eqs
+set (Th _ (K e _))  (Th _ (K f _))  (C eqs) = checkConst e f eqs
+set (Th _ (K e el)) (Th j (B _))    (C eqs) = setConst j.fin e el eqs
+set (Th i (B _))    (Th _ (K e el)) (C eqs) = setConst i.fin e el eqs
+set (Th i (B il))   (Th j (B jl))   (C eqs) = setVar i.fin j.fin il jl eqs
 
 
 public export %inline
@@ -179,97 +190,99 @@ Split : Nat -> Type
 Split d = (DimEq' d, DSubst (S d) d)
 
 export %inline
-split1 : DimConst -> Loc -> DimEq' (S d) -> Maybe (Split d)
-split1 e loc eqs = case setConst VZ e loc eqs of
+split1 : {d : Nat} -> DimConst -> Loc -> DimEq' (S d) -> Maybe (Split d)
+split1 e loc eqs = case setConst 0 e loc eqs of
   ZeroIsOne    => Nothing
-  C (eqs :< _) => Just (eqs, K e loc ::: id)
+  C (eqs :< _) => Just (eqs, id (B loc) :< KT e loc)
 
 export %inline
-split : Loc -> DimEq' (S d) -> List (Split d)
+split : {d : Nat} -> Loc -> DimEq' (S d) -> List (Split d)
 split loc eqs = toList (split1 Zero loc eqs) <+> toList (split1 One loc eqs)
 
 export
-splits' : Loc -> DimEq' d -> List (DSubst d 0)
-splits' _   [<]          = [id]
+splits' : {d : Nat} -> Loc -> DimEq' d -> List (DSubst d 0)
+splits' _   [<]          = [[<]]
 splits' loc eqs@(_ :< _) =
   [th . ph | (eqs', th) <- split loc eqs, ph <- splits' loc eqs']
 
 ||| the Loc is put into each of the DimConsts
 export %inline
-splits : Loc -> DimEq d -> List (DSubst d 0)
+splits : {d : Nat} -> Loc -> DimEq d -> List (DSubst d 0)
 splits _   ZeroIsOne = []
 splits loc (C eqs)   = splits' loc eqs
 
 
-private
-0 newGetShift : (d : Nat) -> (i : Var d) -> (by : Shift d d') ->
-                getShift' by (new' {d}) i = Nothing
-newGetShift (S d) VZ     by = Refl
-newGetShift (S d) (VS i) by = newGetShift d i (ssDown by)
+-- private
+-- 0 newGetShift : (d : Nat) -> (i : Fin d) -> (by : Shift d d') ->
+--                 getShift' by (new' {d}) i = Nothing
+-- newGetShift (S d) FZ     by = Refl
+-- newGetShift (S d) (FS i) by = newGetShift d i (ssDown by)
 
-export
-0 newGet' : (d : Nat) -> (i : Var d) -> get' (new' {d}) i = Nothing
-newGet' d i = newGetShift d i SZ
+-- export
+-- 0 newGet' : (d : Nat) -> (i : Fin d) -> get' (new' {d}) i = Nothing
+-- newGet' d i = newGetShift d i SZ
 
-export
-0 newGet : (d : Nat) -> (p : Dim d) -> get (new' {d}) p = p
-newGet d (K e _) = Refl
-newGet d (B i _) = rewrite newGet' d i in Refl
+-- export
+-- 0 newGet : (d : Nat) -> (p : Dim d) -> get (new' {d}) p = p
+-- newGet d (K e _) = Refl
+-- newGet d (B i _) = rewrite newGet' d i in Refl
 
 
-export
-0 setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
-setSelf p ZeroIsOne = Refl
-setSelf (K Zero _) (C eqs) = Refl
-setSelf (K One _)  (C eqs) = Refl
-setSelf (B i _)    (C eqs) with (compareP i i) | (compare i.nat i.nat)
-  _ | IsLT lt | LT = absurd lt
-  _ | IsEQ    | EQ = Refl
-  _ | IsGT gt | GT = absurd gt
+-- export
+-- 0 setSelf : (p : Dim d) -> (eqs : DimEq d) -> set p p eqs = eqs
+-- setSelf p ZeroIsOne = Refl
+-- setSelf (K Zero _) (C eqs) = Refl
+-- setSelf (K One _)  (C eqs) = Refl
+-- setSelf (B i _)    (C eqs) with (compareP i i) | (compare i.nat i.nat)
+--   _ | IsLT lt | LT = absurd lt
+--   _ | IsEQ    | EQ = Refl
+--   _ | IsGT gt | GT = absurd gt
 
 
-private
-prettyDVars : {opts : _} -> BContext d -> Eff Pretty (SnocList (Doc opts))
-prettyDVars = traverse prettyDBind . toSnocList'
+parameters {opts : LayoutOpts}
+  private
+  prettyDVars : {d : Nat} -> BContext d -> Eff Pretty (SnocList (Doc opts))
+  prettyDVars = traverse prettyDBind . toSnocList'
 
-private
-prettyCst : {opts : _} -> BContext d -> Dim d -> Dim d -> Eff Pretty (Doc opts)
-prettyCst dnames p q =
-  hsep <$> sequence [prettyDim dnames p, cstD, prettyDim dnames q]
+  private
+  prettyCst : {d : Nat} -> BContext d -> DimT d -> DimT d -> Eff Pretty (Doc opts)
+  prettyCst dnames p q =
+    hsep <$> sequence [prettyDim dnames p, cstD, prettyDim dnames q]
 
-private
-prettyCsts : {opts : _} -> BContext d -> DimEq' d ->
-             Eff Pretty (SnocList (Doc opts))
-prettyCsts [<] [<] = pure [<]
-prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs
-prettyCsts dnames (eqs :< Just q)  =
-  [|prettyCsts (tail dnames) eqs :< prettyCst dnames (BV 0 noLoc) (weakD 1 q)|]
+  private
+  prettyCsts : {d : Nat} -> BContext d -> DimEq' d ->
+               Eff Pretty (SnocList (Doc opts))
+  prettyCsts [<] [<] = pure [<]
+  prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs
+  prettyCsts dnames (eqs :< Just q)  =
+    [|prettyCsts (tail dnames) eqs :<
+      prettyCst dnames (BV 0 noLoc) (weak 1 q)|]
 
-export
-prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
-prettyDimEq' dnames eqs = do
-  vars <- prettyDVars dnames
-  eqs  <- prettyCsts dnames eqs
-  let prec = if length vars <= 1 && null eqs then Arg else Outer
-  parensIfM prec $ fillSeparateTight !commaD $ toList vars ++ toList eqs
+  export
+  prettyDimEq' : {d : Nat} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
+  prettyDimEq' dnames eqs = do
+    vars <- prettyDVars dnames
+    eqs  <- prettyCsts dnames eqs
+    let prec = if length vars <= 1 && null eqs then Arg else Outer
+    parensIfM prec $ fillSeparateTight !commaD $ toList vars ++ toList eqs
 
-export
-prettyDimEq : {opts : _} -> BContext d -> DimEq d -> Eff Pretty (Doc opts)
-prettyDimEq dnames ZeroIsOne = do
-  vars <- prettyDVars dnames
-  cst  <- prettyCst [<] (K Zero noLoc) (K One noLoc)
-  pure $ separateTight !commaD $ vars :< cst
-prettyDimEq dnames (C eqs) = prettyDimEq' dnames eqs
+  export
+  prettyDimEq : {d : Nat} -> BContext d -> DimEq d -> Eff Pretty (Doc opts)
+  prettyDimEq dnames ZeroIsOne = do
+    vars <- prettyDVars dnames
+    cst  <- prettyCst [<] (KT Zero noLoc) (KT One noLoc)
+    pure $ separateTight !commaD $ vars :< cst
+  prettyDimEq dnames (C eqs) = prettyDimEq' dnames eqs
 
 
 public export
-wf' : DimEq' d -> Bool
-wf' [<]                   = True
-wf' (eqs :< Nothing)      = wf' eqs
-wf' (eqs :< Just (K e _)) = wf' eqs
-wf' (eqs :< Just (B i _)) = isNothing (get' eqs i) && wf' eqs
+wf' : {d : Nat} -> DimEq' d -> Bool
+wf' [<]                         = True
+wf' (eqs :< Nothing)            = wf' eqs
+wf' (eqs :< Just (Th _ (K {}))) = wf' eqs
+wf' (eqs :< Just (Th i (B _)))  = isNothing (get' eqs i.fin) && wf' eqs
 
 public export
-wf : DimEq d -> Bool
+wf : {d : Nat} -> DimEq d -> Bool
 wf ZeroIsOne = True
 wf (C eqs)   = wf' eqs

lib/Quox/Syntax/Shift.idr

@@ -1,9 +1,11 @@
 module Quox.Syntax.Shift
 
 import public Quox.Syntax.Var
+import public Quox.Thin
 
 import Data.Nat
 import Data.So
+import Data.DPair
 
 %default total
 
@@ -220,3 +222,15 @@ namespace CanShift
 
   public export %inline
   [Const] CanShift (\_ => a) where x // _ = x
+
+
+export
+shiftOPE : {mask : Nat} -> (0 ope : OPE m n mask) ->
+           Shift n n' -> Subset Nat (OPE m n')
+shiftOPE ope SZ      = Element _ ope
+shiftOPE ope (SS by) =
+  let Element _ ope = shiftOPE ope by in Element _ $ drop ope
+
+export
+CanShift (Thinned f) where
+  Th ope tm // by = Th (shiftOPE ope by).snd tm

lib/Quox/Syntax/Subst.idr

@@ -1,10 +1,9 @@
 module Quox.Syntax.Subst
 
-import public Quox.Syntax.Shift
-import Quox.Syntax.Var
-import Quox.Name
+import Quox.Thin
+import Quox.Loc
 
-import Data.Nat
+import Data.DPair
 import Data.List
 import Data.SnocVect
 import Derive.Prelude
@@ -14,149 +13,159 @@ import Derive.Prelude
 
 
 public export
-data Subst : (Nat -> Type) -> Nat -> Nat -> Type where
-  Shift : Shift from to -> Subst env from to
-  (:::) : (t : Lazy (env to)) -> Subst env from to -> Subst env (S from) to
-%name Subst th, ph, ps
+Subst : (Nat -> Type) -> Nat -> Nat -> Type
+Subst env from to = SnocVect from (Lazy (Thinned env to))
 
-infixr 7 !:::
-||| in case the automatic laziness insertion gets confused
 public export
-(!:::) : env to -> Subst env from to -> Subst env (S from) to
-t !::: ts = t ::: ts
+Subst2 : (Nat -> Nat -> Type) -> Nat -> Nat -> Nat -> Type
+Subst2 env d from to = SnocVect from (Lazy (Thinned2 env d to))
 
 
-private
-Repr : (Nat -> Type) -> Nat -> Type
-Repr f to = (List (f to), Nat)
-
-private
-repr : Subst f from to -> Repr f to
-repr (Shift by) = ([], by.nat)
-repr (t ::: th) = let (ts, i) = repr th in (t::ts, i)
+public export
+get : Subst env f t -> Fin f -> Thinned env t
+get (sx :< x) FZ     = x
+get (sx :< x) (FS i) = get sx i
 
 
-export Eq   (f to) => Eq   (Subst f from to) where (==) = (==) `on` repr
-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
+public export
+interface FromVar (0 term : Nat -> Type) where
+  var : Loc -> term 1
 
+public export
+0 FromVar2 : (Nat -> Nat -> Type) -> Type
+FromVar2 t = FromVar (t 0)
+
+public export
+varT : FromVar term => Fin n -> Loc -> Thinned term n
+varT i loc = Th (one' i) (var loc)
+
+public export
+varT2 : FromVar2 term => Fin n -> Loc -> Thinned2 term d n
+varT2 i loc = Th2 zero (one' i) (var loc)
 
 infixl 8 //
+namespace CanSubstSelf
+  public export
+  interface FromVar term => CanSubstSelf term where
+    (//) : {f : Nat} -> Thinned term f -> Subst term f t -> Thinned term t
+
+namespace CanSubstSelf2
+  public export
+  interface FromVar2 term => CanSubstSelf2 term where
+    (//) : {f : Nat} -> Thinned2 term d f ->
+           Subst2 term d f t -> Thinned2 term d t
+
 public export
-interface FromVar term => CanSubstSelf term where
-  (//) : term from -> Lazy (Subst term from to) -> term to
+(.) : {mid : Nat} -> CanSubstSelf f =>
+      Subst f from mid -> Subst f mid to -> Subst f from to
+th . ph = map (\(Delay x) => x // ph) th
+
+infixr 9 .%
+
+public export
+(.%) : {mid : Nat} -> CanSubstSelf2 f =>
+       Subst2 f d from mid -> Subst2 f d mid to -> Subst2 f d from to
+th .% ph = map (\(Delay x) => x // ph) th
 
 
 public export
-getLoc : FromVar term => Subst term from to -> Var from -> Loc -> term to
-getLoc (Shift by) i      loc = fromVarLoc (shift by i) loc
-getLoc (t ::: th) VZ     _   = t
-getLoc (t ::: th) (VS i) loc = getLoc th i loc
-
+tabulate : (n : Nat) -> SnocVect n (Fin n)
+tabulate n = go n id where
+  go : (n : Nat) -> (Fin n -> Fin n') -> SnocVect n (Fin n')
+  go 0     f = [<]
+  go (S n) f = go n (f . FS) :< f FZ
 
 public export
-CanSubstSelf Var where
-  i    // Shift by   = shift by i
-  VZ   // (t ::: th) = t
-  VS i // (t ::: th) = i // th
-
-
-public export %inline
-shift : (by : Nat) -> Subst env from (by + from)
-shift by = Shift $ fromNat by
-
-public export %inline
-shift0 : (by : Nat) -> Subst env 0 by
-shift0 by = rewrite sym $ plusZeroRightNeutral by in Shift $ fromNat by
-
+id : FromVar term => {n : Nat} -> (under : Nat) -> Loc ->
+     Subst term n (n + under)
+id under loc =
+  map (\i => delay $ varT (weakenN under i) loc) (tabulate n)
 
 public export
-(.) : CanSubstSelf f => 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)
+id2 : FromVar2 term => {n : Nat} -> Loc -> Subst2 term d n n
+id2 loc = map (\i => delay $ varT2 i loc) $ tabulate n
 
-public export %inline
-id : Subst f n n
-id = shift 0
-
-public export
-traverse : Applicative m =>
-           (f to -> m (g to)) -> Subst f from to -> m (Subst g from to)
-traverse f (Shift by) = pure $ Shift by
-traverse f (t ::: th) = [|f t !::: traverse f th|]
-
--- not in terms of traverse because this map can maintain laziness better
-public export
-map : (f to -> g to) -> Subst f from to -> Subst g from to
-map f (Shift by) = Shift by
-map f (t ::: th) = f t ::: map f th
-
-
-public export %inline
-push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to)
-push th = fromVar VZ ::: (th . shift 1)
-
--- [fixme] a better way to do this?
-public export
-pushN : CanSubstSelf f => (s : Nat) ->
-        Subst f from to -> Subst f (s + from) (s + to)
-pushN 0     th = th
-pushN (S s) th =
-  rewrite plusSuccRightSucc s from in
-  rewrite plusSuccRightSucc s to in
-  pushN s $ fromVar VZ ::: (th . shift 1)
-
-public export
-drop1 : Subst f (S from) to -> Subst f from to
-drop1 (Shift by) = Shift $ ssDown by
-drop1 (t ::: th) = th
-
-
-public export
-fromSnocVect : SnocVect s (f n) -> Subst f (s + n) n
-fromSnocVect [<]       = id
-fromSnocVect (xs :< x) = x ::: fromSnocVect xs
-
-public export %inline
-one : f n -> Subst f (S n) n
-one x = fromSnocVect [< x]
-
-
-||| whether two substitutions with the same codomain have the same shape
-||| (the same number of terms and the same shift at the end). if so, they
-||| also have the same domain
 export
-cmpShape : Subst env from1 to -> Subst env from2 to ->
-           Either Ordering (from1 = from2)
-cmpShape (Shift by) (Shift bz) = cmpLen by bz
-cmpShape (Shift _)  (_ ::: _)  = Left LT
-cmpShape (_ ::: _)  (Shift _)  = Left GT
-cmpShape (_ ::: th) (_ ::: ph) = cong S <$> cmpShape th ph
+select : {n, mask : Nat} -> (0 ope : OPE m n mask) ->
+         SnocVect n a -> SnocVect m a
+select ope sx with %syntactic (view ope)
+  select _ [<]       | StopV       = [<]
+  select _ (sx :< x) | DropV _ ope = select ope sx
+  select _ (sx :< x) | KeepV _ ope = select ope sx :< x
+
+export
+opeToFins : {n, mask : Nat} ->
+            (0 ope : OPE m n mask) -> SnocVect m (Fin n)
+opeToFins ope = select ope $ tabulate n
+
+export
+shift : FromVar term => {from : Nat} ->
+        (n : Nat) -> Loc -> Subst term from (n + from)
+shift n loc = map (\i => delay $ varT (shift n i) loc) $ tabulate from
+
+public export
+pushN : CanSubstSelf term => {to : Nat} -> (by : Nat) ->
+        Subst term from to -> Loc -> Subst term (by + from) (by + to)
+pushN by th loc =
+  rewrite plusCommutative by from in
+  (th . shift by loc) ++ id to loc
+
+public export %inline
+push : CanSubstSelf f => {to : Nat} ->
+       Subst f from to -> Loc -> Subst f (S from) (S to)
+push = pushN 1
+
+
+public export %inline
+one : Thinned f n -> Subst f 1 n
+one x = [< x]
+
+
+||| whether two substitutions with the same codomain have the same domain
+export
+cmpShape : SnocVect m a -> SnocVect n a -> Either Ordering (m = n)
+cmpShape [<]       [<]       = Right Refl
+cmpShape [<]       (sx :< _) = Left LT
+cmpShape (sx :< _) [<]       = Left GT
+cmpShape (sx :< _) (sy :< _) = cong S <$> cmpShape sx sy
 
 
 public export
 record WithSubst tm env n where
   constructor Sub
   term  : tm from
-  subst : Lazy (Subst env from n)
+  subst : Subst env from n
 
+{-
 export
-(Eq (env n), forall n. Eq (tm n)) => Eq (WithSubst tm env n) where
+(forall n. Eq (env n), forall n. Eq (tm n)) =>
+Eq (WithSubst tm env n) where
   Sub t1 s1 == Sub t2 s2 =
     case cmpShape s1 s2 of
       Left  _    => False
-      Right Refl => t1 == t2 && s1 == s2
+      Right Refl =>
+        t1 == t2 && concat @{All} (zipWith ((==) `on` force) s1 s2)
 
 export
-(Ord (env n), forall n. Ord (tm n)) => Ord (WithSubst tm env n) where
+(forall n. Ord (env n), forall n. Ord (tm n)) =>
+Ord (WithSubst tm env n) where
   Sub t1 s1 `compare` Sub t2 s2 =
     case cmpShape s1 s2 of
       Left  o    => o
-      Right Refl => compare (t1, s1) (t2, s2)
+      Right Refl =>
+        compare t1 t2 <+> concat (zipWith (compare `on` force) s1 s2)
 
 export %hint
-ShowWithSubst : (Show (env n), forall n. Show (tm n)) =>
+ShowWithSubst : {n : Nat} ->
+                (forall n. Show (env n), forall n. Show (tm n)) =>
                 Show (WithSubst tm env n)
-ShowWithSubst = deriveShow
+ShowWithSubst = deriveShow where
+  Show (Lazy (Thinned env n)) where showPrec d = showPrec d . force
+-}
+
+
+public export
+record WithSubst2 tm env d n where
+  constructor Sub2
+  term  : tm d from
+  subst : Subst2 env d from n

lib/Quox/Syntax/Term/Base.idr

@@ -1,5 +1,6 @@
 module Quox.Syntax.Term.Base
 
+import public Quox.Thin
 import public Quox.Syntax.Var
 import public Quox.Syntax.Shift
 import public Quox.Syntax.Subst
@@ -18,9 +19,6 @@ import Data.Maybe
 import Data.Nat
 import public Data.So
 import Data.String
-import public Data.SortedMap
-import public Data.SortedMap.Dependent
-import public Data.SortedSet
 import Derive.Prelude
 
 %default total
@@ -46,345 +44,300 @@ TagVal : Type
 TagVal = String
 
 
+||| type-checkable terms, which consists of types and constructor forms.
+|||
+||| first argument `d` is dimension scope size; second `n` is term scope size
 public export
-data ScopedBody : Nat -> (Nat -> Type) -> Nat -> Type where
-  Y : (body : f (s + n)) -> ScopedBody s f n
-  N : (body : f n)       -> ScopedBody s f n
-%name ScopedBody body
+data Term : (d, n : Nat) -> Type
+%name Term s, t, r
 
-export %inline %hint
-EqScopedBody : (forall n. Eq (f n)) => Eq (ScopedBody s f n)
-EqScopedBody = deriveEq
-
-export %inline %hint
-ShowScopedBody : (forall n. Show (f n)) => Show (ScopedBody s f n)
-ShowScopedBody = deriveShow
-
-||| a scoped term with names
+||| inferrable terms, which consists of elimination forms like application and
+||| `case` (as well as other terms with an annotation)
+|||
+||| first argument `d` is dimension scope size; second `n` is term scope size
 public export
-record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
-  constructor S
-  names : BContext s
-  body  : ScopedBody s f n
-%name Scoped body
-
-export %inline
-(forall n. Eq (f n)) => Eq (Scoped s f n) where
-  s == t = s.body == t.body
-
-export %inline %hint
-ShowScoped : (forall n. Show (f n)) => Show (Scoped s f n)
-ShowScoped = deriveShow
+data Elim : (d, n : Nat) -> Type
+%name Elim e, f
 
 
-infixl 8 :#
-infixl 9 :@, :%
-mutual
-  public export
-  TSubst : TSubstLike
-  TSubst d = Subst $ \n => Elim d n
+public export
+ScopeTermN : Nat -> TermLike
+ScopeTermN s d n = ScopedN s (\n => Term d n) n
 
-  ||| first argument `d` is dimension scope size;
-  ||| second `n` is term scope size
-  public export
-  data Term : (d, n : Nat) -> Type where
-    ||| type of types
-    TYPE : (l : Universe) -> (loc : Loc) -> Term d n
+public export
+DScopeTermN : Nat -> TermLike
+DScopeTermN s d n = ScopedN s (\d => Term d n) d
 
-    ||| function type
-    Pi  : (qty : Qty) -> (arg : Term d n) ->
-          (res : ScopeTerm d n) -> (loc : Loc) -> Term d n
-    ||| function term
-    Lam : (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
+public export
+ScopeTerm : TermLike
+ScopeTerm = ScopeTermN 1
 
-    ||| pair type
-    Sig : (fst : Term d n) -> (snd : ScopeTerm d n) -> (loc : Loc) -> Term d n
-    ||| pair value
-    Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
-
-    ||| enumeration type
-    Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n
-    ||| enumeration value
-    Tag : (tag : TagVal) -> (loc : Loc) -> Term d n
-
-    ||| equality type
-    Eq : (ty : DScopeTerm d n) -> (l, r : Term d n) -> (loc : Loc) -> Term d n
-    ||| equality term
-    DLam : (body : DScopeTerm d n) -> (loc : Loc) -> Term d n
-
-    ||| natural numbers (temporary until 𝐖 gets added)
-    Nat  : (loc : Loc) -> Term d n
-    -- [todo] can these be elims?
-    Zero : (loc : Loc) -> Term d n
-    Succ : (p : Term d n) -> (loc : Loc) -> Term d n
-
-    ||| "box" (package a value up with a certain quantity)
-    BOX : (qty : Qty) -> (ty : Term d n) -> (loc : Loc) -> Term d n
-    Box : (val : Term d n) -> (loc : Loc) -> Term d n
-
-    ||| elimination
-    E : (e : Elim d n) -> Term d n
-
-    ||| term closure/suspended substitution
-    CloT  : WithSubst (Term d) (Elim d) n -> Term d n
-    ||| dimension closure/suspended substitution
-    DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
-  %name Term s, t, r
-
-  ||| first argument `d` is dimension scope size, second `n` is term scope size
-  public export
-  data Elim : (d, n : Nat) -> Type where
-    ||| free variable, possibly with a displacement (see @crude, or @mugen for a
-    ||| more abstract and formalised take)
-    |||
-    ||| e.g. if f : ★₀ → ★₁, then f¹ : ★₁ → ★₂
-    F : (x : Name) -> (u : Universe) -> (loc : Loc) -> Elim d n
-    ||| bound variable
-    B : (i : Var n) -> (loc : Loc) -> Elim d n
-
-    ||| term application
-    App : (fun : Elim d n) -> (arg : Term d n) -> (loc : Loc) -> Elim d n
-
-    ||| pair destruction
-    |||
-    ||| `CasePair 𝜋 𝑒 ([𝑟], 𝐴) ([𝑥, 𝑦], 𝑡)` is
-    ||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
-    CasePair : (qty : Qty) -> (pair : Elim d n) ->
-               (ret : ScopeTerm d n) ->
-               (body : ScopeTermN 2 d n) ->
-               (loc : Loc) ->
-               Elim d n
-
-    ||| enum matching
-    CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
-               (ret : ScopeTerm d n) ->
-               (arms : CaseEnumArms d n) ->
-               (loc : Loc) ->
-               Elim d n
-
-    ||| nat matching
-    CaseNat : (qty, qtyIH : Qty) -> (nat : Elim d n) ->
-              (ret : ScopeTerm d n) ->
-              (zero : Term d n) ->
-              (succ : ScopeTermN 2 d n) ->
-              (loc : Loc) ->
-              Elim d n
-
-    ||| unboxing
-    CaseBox : (qty : Qty) -> (box : Elim d n) ->
-              (ret : ScopeTerm d n) ->
-              (body : ScopeTerm d n) ->
-              (loc : Loc) ->
-              Elim d n
-
-    ||| dim application
-    DApp : (fun : Elim d n) -> (arg : Dim d) -> (loc : Loc) -> Elim d n
-
-    ||| type-annotated term
-    Ann : (tm, ty : Term d n) -> (loc : Loc) -> Elim d n
-
-    ||| coerce a value along a type equality, or show its coherence
-    ||| [@xtt; §2.1.1]
-    Coe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
-          (val : Term d n) -> (loc : Loc) -> Elim d n
-
-    ||| "generalised composition" [@xtt; §2.1.2]
-    Comp : (ty : Term d n) -> (p, q : Dim d) ->
-           (val : Term d n) -> (r : Dim d) ->
-           (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
-
-    ||| match on types. needed for b.s. of coercions [@xtt; §2.2]
-    TypeCase : (ty : Elim d n) -> (ret : Term d n) ->
-               (arms : TypeCaseArms d n) -> (def : Term d n) ->
-               (loc : Loc) ->
-               Elim d n
-
-    ||| term closure/suspended substitution
-    CloE  : WithSubst (Elim d) (Elim d) n -> Elim d n
-    ||| dimension closure/suspended substitution
-    DCloE : WithSubst (\d => Elim d n) Dim d -> Elim d n
-  %name Elim e, f
-
-  public export
-  CaseEnumArms : TermLike
-  CaseEnumArms d n = SortedMap TagVal (Term d n)
-
-  public export
-  TypeCaseArms : TermLike
-  TypeCaseArms d n = SortedDMap TyConKind (\k => TypeCaseArmBody k d n)
-
-  public export
-  TypeCaseArm : TermLike
-  TypeCaseArm d n = (k ** TypeCaseArmBody k d n)
-
-  public export
-  TypeCaseArmBody : TyConKind -> TermLike
-  TypeCaseArmBody k = ScopeTermN (arity k)
+public export
+DScopeTerm : TermLike
+DScopeTerm = DScopeTermN 1
 
 
-  public export
-  ScopeTermN, DScopeTermN : Nat -> TermLike
-  ScopeTermN  s d n = Scoped s (Term d) n
-  DScopeTermN s d n = Scoped s (\d => Term d n) d
+public export
+TermT : TermLike
+TermT = Thinned2 (\d, n => Term d n)
 
-  public export
-  ScopeTerm, DScopeTerm : TermLike
-  ScopeTerm  = ScopeTermN 1
-  DScopeTerm = DScopeTermN 1
+public export
+ElimT : TermLike
+ElimT = Thinned2 (\d, n => Elim d n)
 
-mutual
-  export %hint
-  EqTerm : Eq (Term d n)
-  EqTerm = assert_total {a = Eq (Term d n)} deriveEq
 
-  export %hint
-  EqElim : Eq (Elim d n)
-  EqElim = assert_total {a = Eq (Elim d n)} deriveEq
+public export
+DimArg : TermLike
+DimArg d n = Dim d
 
-mutual
-  export %hint
-  ShowTerm : Show (Term d n)
-  ShowTerm = assert_total {a = Show (Term d n)} deriveShow
 
-  export %hint
-  ShowElim : Show (Elim d n)
-  ShowElim = assert_total {a = Show (Elim d n)} deriveShow
+data Term where
+  ||| type of types
+  TYPE : (l : Universe) -> (loc : Loc) -> Term 0 0
 
-||| scope which ignores all its binders
-public export %inline
-SN : {s : Nat} -> f n -> Scoped s f n
-SN = S (replicate s $ BN Unused noLoc) . N
+  ||| function type
+  Pi : Qty -> Subterms [Term, ScopeTerm] d n -> Loc -> Term d n
+  ||| function value
+  Lam : ScopeTerm d n -> Loc -> Term d n
 
-||| scope which uses its binders
-public export %inline
-SY : BContext s -> f (s + n) -> Scoped s f n
-SY ns = S ns . Y
+  ||| pair type
+  Sig : Subterms [Term, ScopeTerm] d n -> Loc -> Term d n
+  ||| pair value
+  Pair : Subterms [Term, Term] d n -> Loc -> Term d n
 
-public export %inline
-name : Scoped 1 f n -> BindName
-name (S [< x] _) = x
+  ||| enum type
+  Enum : List TagVal -> Loc -> Term 0 0
+  ||| enum value
+  Tag : TagVal -> Loc -> Term 0 0
 
-public export %inline
-(.name) : Scoped 1 f n -> BindName
-s.name = name s
+  ||| equality type
+  Eq : Subterms [DScopeTerm, Term, Term] d n -> Loc -> Term d n
+  ||| equality value
+  DLam : DScopeTerm d n -> Loc -> Term d n
 
-||| more convenient Pi
-public export %inline
-PiY : (qty : Qty) -> (x : BindName) ->
-      (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
-PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
+  ||| natural numbers (temporary until 𝐖 gets added)
+  Nat  : Loc -> Term 0 0
+  Zero : Loc -> Term 0 0
+  Succ : Term d n -> Loc -> Term 0 0
 
-||| more convenient Lam
-public export %inline
-LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
-LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
+  ||| package a value with a quantity
+  ||| e.g. a value of [ω. A], when unpacked, can be used ω times,
+  ||| even if the box itself is linear
+  BOX : Qty -> Term d n -> Loc -> Term d n
+  Box : Term d n -> Loc -> Term d n
 
-public export %inline
-LamN : (body : Term d n) -> (loc : Loc) -> Term d n
-LamN {body, loc} = Lam {body = SN body, loc}
+  E : Elim d n -> Term d n
 
-||| non dependent function type
-public export %inline
-Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
-Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
+  ||| term closure/suspended substitution
+  CloT  : WithSubst2 Term Elim d n -> Term d n
+  ||| dimension closure/suspended substitution
+  DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
 
-||| more convenient Sig
-public export %inline
-SigY : (x : BindName) -> (fst : Term d n) ->
-       (snd : Term d (S n)) -> (loc : Loc) -> Term d n
-SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
+public export
+data Elim where
+  ||| free variable, possibly with a displacement (see @crude, or @mugen for a
+  ||| more abstract and formalised take)
+  |||
+  ||| e.g. if f : ★₀ → ★₁, then f¹ : ★₁ → ★₂
+  F : Name -> Universe -> Loc -> Elim 0 0
+  ||| bound variable
+  B : Loc -> Elim 0 1
 
-||| non dependent pair type
-public export %inline
-And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
-And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
+  ||| term application
+  App : Subterms [Elim, Term] d n -> Loc -> Elim d n
 
-||| more convenient Eq
-public export %inline
-EqY : (i : BindName) -> (ty : Term (S d) n) ->
-      (l, r : Term d n) -> (loc : Loc) -> Term d n
-EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
+  ||| pair match
+  ||| - the subterms are, in order: [head, return type, body]
+  ||| - the quantity is that of the head, and since pairs only have one
+  |||   constructor, can be 0
+  CasePair : Qty -> Subterms [Elim, ScopeTerm, ScopeTermN 2] d n ->
+             Loc -> Elim d n
 
-||| more convenient DLam
-public export %inline
-DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
-DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
+  ||| enum match
+  CaseEnum : Qty -> (arms : List TagVal) ->
+             Subterms (Elim :: ScopeTerm :: (Term <$ arms)) d n ->
+             Loc -> Elim d n
 
-public export %inline
-DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
-DLamN {body, loc} = DLam {body = SN body, loc}
+  ||| nat match
+  CaseNat : Qty -> Qty ->
+            Subterms [Elim, ScopeTerm, Term, ScopeTermN 2] d n ->
+            Loc -> Elim d n
+
+  ||| box match
+  CaseBox : Qty -> Subterms [Elim, ScopeTerm, ScopeTerm] d n -> Loc -> Elim d n
+
+  ||| dim application
+  DApp : Subterms [Elim, DimArg] d n -> Loc -> Elim d n
+
+  ||| type-annotated term
+  Ann : Subterms [Term, Term] d n -> Loc -> Elim d n
+
+  ||| coerce a value along a type equality, or show its coherence
+  ||| [@xtt; §2.1.1]
+  Coe : Subterms [DScopeTerm, DimArg, DimArg, Term] d n ->
+        Loc -> Elim d n
+
+  ||| "generalised composition" [@xtt; §2.1.2]
+  Comp : Subterms [Term, DimArg, DimArg, Term,
+                   DimArg, DScopeTerm, DScopeTerm] d n ->
+         Loc -> Elim d n
+
+  ||| match on types. needed for b.s. of coercions [@xtt; §2.2]
+  TypeCase : Subterms [Elim, Term,   -- head, type
+                       Term,         -- ★
+                       ScopeTermN 2, -- pi
+                       ScopeTermN 2, -- sig
+                       Term,         -- enum
+                       ScopeTermN 5, -- eq
+                       Term,         -- nat
+                       ScopeTerm     -- box
+                      ] d n -> Loc -> Elim d n
+
+  ||| term closure/suspended substitution
+  CloE  : WithSubst2 Elim Elim d n -> Elim d n
+  ||| dimension closure/suspended substitution
+  DCloE : WithSubst (\d => Elim d n) Dim d -> Elim d n
+
+
+-- this kills the idris ☹
+-- export %hint
+-- EqTerm : Eq (Term d n)
+
+-- export %hint
+-- EqElim : Eq (Elim d n)
+
+-- EqTerm = deriveEq
+-- EqElim = deriveEq
+
+
+-- mutual
+--   export %hint
+--   ShowTerm : Show (Term d n)
+--   ShowTerm = assert_total {a = Show (Term d n)} deriveShow
+
+--   export %hint
+--   ShowElim : Show (Elim d n)
+--   ShowElim = assert_total {a = Show (Elim d n)} deriveShow
+
+-- ||| scope which ignores all its binders
+-- public export %inline
+-- SN : {s : Nat} -> f n -> Scoped s f n
+-- SN = S (replicate s $ BN Unused noLoc) . N
+
+-- ||| scope which uses its binders
+-- public export %inline
+-- SY : BContext s -> f (s + n) -> Scoped s f n
+-- SY ns = S ns . Y
+
+-- public export %inline
+-- name : Scoped 1 f n -> BindName
+-- name (S [< x] _) = x
+
+-- public export %inline
+-- (.name) : Scoped 1 f n -> BindName
+-- s.name = name s
+
+-- ||| more convenient Pi
+-- public export %inline
+-- PiY : (qty : Qty) -> (x : BindName) ->
+--       (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
+-- PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
+
+-- ||| more convenient Lam
+-- public export %inline
+-- LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
+-- LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
+
+-- public export %inline
+-- LamN : (body : Term d n) -> (loc : Loc) -> Term d n
+-- LamN {body, loc} = Lam {body = SN body, loc}
+
+-- ||| non dependent function type
+-- public export %inline
+-- Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
+-- Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
+
+-- ||| more convenient Sig
+-- public export %inline
+-- SigY : (x : BindName) -> (fst : Term d n) ->
+--        (snd : Term d (S n)) -> (loc : Loc) -> Term d n
+-- SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
+
+-- ||| non dependent pair type
+-- public export %inline
+-- And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
+-- And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
+
+-- ||| more convenient Eq
+-- public export %inline
+-- EqY : (i : BindName) -> (ty : Term (S d) n) ->
+--       (l, r : Term d n) -> (loc : Loc) -> Term d n
+-- EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
+
+-- ||| more convenient DLam
+-- public export %inline
+-- DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
+-- DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
+
+-- public export %inline
+-- DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
+-- DLamN {body, loc} = DLam {body = SN body, loc}
+
+-- ||| non dependent equality type
+-- public export %inline
+-- Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
+-- Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
 
-||| non dependent equality type
-public export %inline
-Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
-Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
 
 ||| same as `F` but as a term
 public export %inline
-FT : Name -> Universe -> Loc -> Term d n
+FT : Name -> Universe -> Loc -> Term 0 0
 FT x u loc = E $ F x u loc
 
 ||| abbreviation for a bound variable like `BV 4` instead of
 ||| `B (VS (VS (VS (VS VZ))))`
 public export %inline
-BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n
-BV i loc = B (V i) loc
+BV : (i : Fin n) -> (loc : Loc) -> ElimT d n
+BV i loc = Th2 zero (one' i) $ B loc
 
 ||| same as `BV` but as a term
 public export %inline
-BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
-BVT i loc = E $ BV i loc
+BVT : (i : Fin n) -> (loc : Loc) -> TermT d n
+BVT i loc = Th2 zero (one' i) $ E $ B loc
 
 public export
-makeNat : Nat -> Loc -> Term d n
-makeNat 0 loc = Zero loc
+makeNat : Nat -> Loc -> Term 0 0
+makeNat 0     loc = Zero loc
 makeNat (S k) loc = Succ (makeNat k loc) loc
 
-public export %inline
-enum : List TagVal -> Loc -> Term d n
-enum ts loc = Enum (SortedSet.fromList ts) loc
-
-public export %inline
-typeCase : Elim d n -> Term d n ->
-           List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
-typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc
-
-public export %inline
-typeCase1Y : Elim d n -> Term d n ->
-             (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
-             (loc : Loc) ->
-             {default (Nat loc) def : Term d n} ->
-             Elim d n
-typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
-
 
 export
 Located (Elim d n) where
-  (F _ _ loc).loc               = loc
-  (B _ loc).loc                 = loc
-  (App _ _ loc).loc             = loc
-  (CasePair _ _ _ _ loc).loc    = loc
-  (CaseEnum _ _ _ _ loc).loc    = loc
-  (CaseNat _ _ _ _ _ _ loc).loc = loc
-  (CaseBox _ _ _ _ loc).loc     = loc
-  (DApp _ _ loc).loc            = loc
-  (Ann _ _ loc).loc             = loc
-  (Coe _ _ _ _ loc).loc         = loc
-  (Comp _ _ _ _ _ _ _ loc).loc  = loc
-  (TypeCase _ _ _ _ loc).loc    = loc
-  (CloE (Sub e _)).loc          = e.loc
-  (DCloE (Sub e _)).loc         = e.loc
+  (F _ _ loc).loc          = loc
+  (B loc).loc              = loc
+  (App _ loc).loc          = loc
+  (CasePair _ _ loc).loc   = loc
+  (CaseEnum _ _ _ loc).loc = loc
+  (CaseNat _ _ _ loc).loc  = loc
+  (CaseBox _ _ loc).loc    = loc
+  (DApp _ loc).loc         = loc
+  (Ann _ loc).loc          = loc
+  (Coe _ loc).loc          = loc
+  (Comp _ loc).loc         = loc
+  (TypeCase _ loc).loc     = loc
+  (CloE (Sub2 e _)).loc    = e.loc
+  (DCloE (Sub e _)).loc    = e.loc
 
 export
 Located (Term d n) where
   (TYPE _ loc).loc      = loc
-  (Pi _ _ _ loc).loc    = loc
+  (Pi _ _ loc).loc      = loc
   (Lam _ loc).loc       = loc
-  (Sig _ _ loc).loc     = loc
-  (Pair _ _ loc).loc    = loc
+  (Sig _ loc).loc       = loc
+  (Pair _ loc).loc      = loc
   (Enum _ loc).loc      = loc
   (Tag _ loc).loc       = loc
-  (Eq _ _ _ loc).loc    = loc
+  (Eq _ loc).loc        = loc
   (DLam _ loc).loc      = loc
   (Nat loc).loc         = loc
   (Zero loc).loc        = loc
@@ -392,72 +345,43 @@ Located (Term d n) where
   (BOX _ _ loc).loc     = loc
   (Box _ loc).loc       = loc
   (E e).loc             = e.loc
-  (CloT (Sub t _)).loc  = t.loc
+  (CloT (Sub2 t _)).loc = t.loc
   (DCloT (Sub t _)).loc = t.loc
 
-export
-Located1 f => Located (ScopedBody s f n) where
-  (Y t).loc = t.loc
-  (N t).loc = t.loc
-
-export
-Located1 f => Located (Scoped s f n) where
-  t.loc = t.body.loc
-
 
 export
 Relocatable (Elim d n) where
-  setLoc loc (F x u _) = F x u loc
-  setLoc loc (B i _) = B i loc
-  setLoc loc (App fun arg _) = App fun arg loc
-  setLoc loc (CasePair qty pair ret body _) =
-    CasePair qty pair ret body loc
-  setLoc loc (CaseEnum qty tag ret arms _) =
-    CaseEnum qty tag ret arms loc
-  setLoc loc (CaseNat qty qtyIH nat ret zero succ _) =
-    CaseNat qty qtyIH nat ret zero succ loc
-  setLoc loc (CaseBox qty box ret body _) =
-    CaseBox qty box ret body loc
-  setLoc loc (DApp fun arg _) =
-    DApp fun arg loc
-  setLoc loc (Ann tm ty _) =
-    Ann tm ty loc
-  setLoc loc (Coe ty p q val _) =
-    Coe ty p q val loc
-  setLoc loc (Comp ty p q val r zero one _) =
-    Comp ty p q val r zero one loc
-  setLoc loc (TypeCase ty ret arms def _) =
-    TypeCase ty ret arms def loc
-  setLoc loc (CloE (Sub term subst)) =
-    CloE $ Sub (setLoc loc term) subst
-  setLoc loc (DCloE (Sub term subst)) =
-    DCloE $ Sub (setLoc loc term) subst
+  setLoc loc (F x u _)                = F x u loc
+  setLoc loc (B _)                    = B loc
+  setLoc loc (App ts _)               = App ts loc
+  setLoc loc (CasePair qty ts _)      = CasePair qty ts loc
+  setLoc loc (CaseEnum qty arms ts _) = CaseEnum qty arms ts loc
+  setLoc loc (CaseNat qty qtyIH ts _) = CaseNat qty qtyIH ts loc
+  setLoc loc (CaseBox qty ts _)       = CaseBox qty ts loc
+  setLoc loc (DApp ts _)              = DApp ts loc
+  setLoc loc (Ann ts _)               = Ann ts loc
+  setLoc loc (Coe ts _)               = Coe ts loc
+  setLoc loc (Comp ts _)              = Comp ts loc
+  setLoc loc (TypeCase ts _)          = TypeCase ts loc
+  setLoc loc (CloE (Sub2 term subst)) = CloE $ Sub2 (setLoc loc term) subst
+  setLoc loc (DCloE (Sub term subst)) = DCloE $ Sub (setLoc loc term) subst
 
 export
 Relocatable (Term d n) where
-  setLoc loc (TYPE l _) = TYPE l loc
-  setLoc loc (Pi qty arg res _) = Pi qty arg res loc
-  setLoc loc (Lam body _) = Lam body loc
-  setLoc loc (Sig fst snd _) = Sig fst snd loc
-  setLoc loc (Pair fst snd _) = Pair fst snd loc
-  setLoc loc (Enum cases _) = Enum cases loc
-  setLoc loc (Tag tag _) = Tag tag loc
-  setLoc loc (Eq ty l r _) = Eq ty l r loc
-  setLoc loc (DLam body _) = DLam body loc
-  setLoc loc (Nat _) = Nat loc
-  setLoc loc (Zero _) = Zero loc
-  setLoc loc (Succ p _) = Succ p loc
-  setLoc loc (BOX qty ty _) = BOX qty ty loc
-  setLoc loc (Box val _) = Box val loc
-  setLoc loc (E e) = E $ setLoc loc e
-  setLoc loc (CloT (Sub term subst)) = CloT $ Sub (setLoc loc term) subst
+  setLoc loc (TYPE l _)               = TYPE l loc
+  setLoc loc (Pi qty ts _)            = Pi qty ts loc
+  setLoc loc (Lam body _)             = Lam body loc
+  setLoc loc (Sig ts _)               = Sig ts loc
+  setLoc loc (Pair ts _)              = Pair ts loc
+  setLoc loc (Enum cases _)           = Enum cases loc
+  setLoc loc (Tag tag _)              = Tag tag loc
+  setLoc loc (Eq ts _)                = Eq ts loc
+  setLoc loc (DLam body _)            = DLam body loc
+  setLoc loc (Nat _)                  = Nat loc
+  setLoc loc (Zero _)                 = Zero loc
+  setLoc loc (Succ p _)               = Succ p loc
+  setLoc loc (BOX qty ty _)           = BOX qty ty loc
+  setLoc loc (Box val _)              = Box val loc
+  setLoc loc (E e)                    = E $ setLoc loc e
+  setLoc loc (CloT (Sub2 term subst)) = CloT $ Sub2 (setLoc loc term) subst
   setLoc loc (DCloT (Sub term subst)) = DCloT $ Sub (setLoc loc term) subst
-
-export
-Relocatable1 f => Relocatable (ScopedBody s f n) where
-  setLoc loc (Y body) = Y $ setLoc loc body
-  setLoc loc (N body) = N $ setLoc loc body
-
-export
-Relocatable1 f => Relocatable (Scoped s f n) where
-  setLoc loc (S names body) = S (setLoc loc <$> names) (setLoc loc body)

lib/Quox/Syntax/Term/Pretty.idr

@@ -18,11 +18,11 @@ prettyUniverse = hl Universe . text . show
 
 
 export
-prettyTerm : {opts : _} -> BContext d -> BContext n -> Term d n ->
+prettyTerm : {opts : _} -> BContext d -> BContext n -> TermT d n ->
              Eff Pretty (Doc opts)
 
 export
-prettyElim : {opts : _} -> BContext d -> BContext n -> Elim d n ->
+prettyElim : {opts : _} -> BContext d -> BContext n -> ElimT d n ->
              Eff Pretty (Doc opts)
 
 private

lib/Quox/Syntax/Term/Subst.idr

@@ -2,374 +2,462 @@ module Quox.Syntax.Term.Subst
 
 import Quox.No
 import Quox.Syntax.Term.Base
-import Quox.Syntax.Term.Tighten
+import Quox.Syntax.Subst
+
 import Data.SnocVect
+import Data.Singleton
 
 %default total
 
-namespace CanDSubst
-  public export
-  interface CanDSubst (0 tm : TermLike) where
-    (//) : tm d1 n -> Lazy (DSubst d1 d2) -> tm d2 n
 
-||| does the minimal reasonable work:
-||| - deletes the closure around an atomic constant like `TYPE`
-||| - deletes an identity substitution
-||| - composes (lazily) with an existing top-level dim-closure
-||| - otherwise, wraps in a new closure
-export
-CanDSubst Term where
-  s                // Shift SZ = s
-  TYPE l loc       // _        = TYPE l loc
-  DCloT (Sub s ph) // th       = DCloT $ Sub s $ ph . th
-  s                // th       = DCloT $ Sub s th
+infixl 8 ///
 
-private
-subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n
-subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
-subDArgs e              th = DCloE $ Sub e th
+parameters {0 f : Nat -> Nat -> Type}
+  private
+  th0 : f 0 0 -> Thinned2 f d n
+  th0 = Th2 zero zero
 
-||| does the minimal reasonable work:
-||| - deletes the closure around a term variable
-||| - deletes an identity substitution
-||| - composes (lazily) with an existing top-level dim-closure
-||| - immediately looks up bound variables in a
-|||   top-level sequence of dimension applications
-||| - otherwise, wraps in a new closure
-export
-CanDSubst Elim where
-  e                // Shift SZ = e
-  F x u loc        // _        = F x u loc
-  B i loc          // _        = B i loc
-  e@(DApp {})      // th       = subDArgs e th
-  DCloE (Sub e ph) // th       = DCloE $ Sub e $ ph . th
-  e                // th       = DCloE $ Sub e th
+  private
+  th1 : {d, n : Nat} -> f d n -> Thinned2 f d n
+  th1 = Th2 id' id'
 
-namespace DSubst.ScopeTermN
-  export %inline
-  (//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
-         ScopeTermN s d2 n
-  S ns (Y body) // th = S ns $ Y $ body // th
-  S ns (N body) // th = S ns $ N $ body // th
+private dsubTerm : {d1, d2, n : Nat} -> Term d1 n -> DSubst d1 d2 -> TermT d2 n
+private dsubElim : {d1, d2, n : Nat} -> Elim d1 n -> DSubst d1 d2 -> ElimT d2 n
 
-namespace DSubst.DScopeTermN
-  export %inline
-  (//) : {s : Nat} ->
-         DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
-         DScopeTermN s d2 n
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
-  S ns (N body) // th = S ns $ N $ body // th
+dsubTerm (TYPE l loc) th = th0 $ TYPE l loc
+dsubTerm (Enum strs loc) th = th0 $ Enum strs loc
+dsubTerm (Tag str loc) th = th0 $ Tag str loc
+dsubTerm (Nat loc) th = th0 $ Nat loc
+dsubTerm (Zero loc) th = th0 $ Zero loc
+dsubTerm (E e) th =
+  let Th2 dope tope e' = dsubElim e th in
+  Th2 dope tope $ E e'
+dsubTerm (DCloT (Sub t ph)) th = th1 $ DCloT $ Sub t $ ph . th
+dsubTerm t th = th1 $ DCloT $ Sub t th
 
-
-export %inline FromVar (Elim d) where fromVarLoc = B
-export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
-
-
-||| does the minimal reasonable work:
-||| - deletes the closure around a *free* name
-||| - deletes an identity substitution
-||| - composes (lazily) with an existing top-level closure
-||| - immediately looks up a bound variable
-||| - otherwise, wraps in a new closure
-export
-CanSubstSelf (Elim d) where
-  F x u loc       // _  = F x u loc
-  B i loc         // th = getLoc 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
-
-namespace CanTSubst
-  public export
-  interface CanTSubst (0 tm : TermLike) where
-    (//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2
-
-||| does the minimal reasonable work:
-||| - deletes the closure around an atomic constant like `TYPE`
-||| - deletes an identity substitution
-||| - composes (lazily) with an existing top-level closure
-||| - goes inside `E` in case it is a simple variable or something
-||| - otherwise, wraps in a new closure
-export
-CanTSubst Term where
-  TYPE l loc      // _  = TYPE l loc
-  E e             // th = E $ e // th
-  CloT (Sub s ph) // th = CloT $ Sub s $ ph . th
-  s               // th = case force th of
-                               Shift SZ => s
-                               th       => CloT $ Sub s th
-
-namespace ScopeTermN
-  export %inline
-  (//) : {s : Nat} ->
-         ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
-         ScopeTermN s d n2
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
-  S ns (N body) // th = S ns $ N $ body // th
-
-namespace DScopeTermN
-  export %inline
-  (//) : {s : Nat} ->
-         DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
-  S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
-  S ns (N body) // th = S ns $ N $ body // th
-
-export %inline CanShift (Term d) where s // by = s // Shift by
-export %inline CanShift (Elim d) where e // by = e // Shift by
-
-export %inline
-{s : Nat} -> CanShift (ScopeTermN s d) where
-  b // by = b // Shift by
-
-
-export %inline
-comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
-comp th ps ph = map (// th) ps . ph
-
-
-public export %inline
-dweakT : (by : Nat) -> Term d n -> Term (by + d) n
-dweakT by t = t // shift by
-
-public export %inline
-dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n
-dweakE by t = t // shift by
-
-
-public export %inline
-weakT : (by : Nat) -> Term d n -> Term d (by + n)
-weakT by t = t // shift by
-
-public export %inline
-weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
-weakE by t = t // shift by
-
-
-parameters {s : Nat}
-  namespace ScopeTermBody
-    export %inline
-    (.term) : ScopedBody s (Term d) n -> Term d (s + n)
-    (Y b).term = b
-    (N b).term = weakT s b
-
-  namespace ScopeTermN
-    export %inline
-    (.term) : ScopeTermN s d n -> Term d (s + n)
-    t.term = t.body.term
-
-  namespace DScopeTermBody
-    export %inline
-    (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
-    (Y b).term = b
-    (N b).term = dweakT s b
-
-  namespace DScopeTermN
-    export %inline
-    (.term) : DScopeTermN s d n -> Term (s + d) n
-    t.term = t.body.term
-
-
-export %inline
-subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n
-subN (S _ (Y body)) es = body // fromSnocVect es
-subN (S _ (N body)) _  = body
-
-export %inline
-sub1 : ScopeTerm d n -> Elim d n -> Term d n
-sub1 t e = subN t [< e]
-
-export %inline
-dsubN : DScopeTermN s d n -> SnocVect s (Dim d) -> Term d n
-dsubN (S _ (Y body)) ps = body // fromSnocVect ps
-dsubN (S _ (N body)) _  = body
-
-export %inline
-dsub1 : DScopeTerm d n -> Dim d -> Term d n
-dsub1 t p = dsubN t [< p]
-
-
-public export %inline
-(.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
-body.zero = dsub1 body $ K Zero loc
-
-public export %inline
-(.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
-body.one = dsub1 body $ K One loc
-
-
-public export
-0 CloTest : TermLike -> Type
-CloTest tm = forall d, n. tm d n -> Bool
-
-interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
-  pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
-                   tm d1 n1 -> Subset (tm d2 n2) (No . isClo)
-
-public export
-0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
-NotClo = No . isClo
-
-public export
-0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} ->
-           PushSubsts tm isClo => TermLike
-NonClo tm d n = Subset (tm d n) NotClo
-
-public export %inline
-nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) =>
-       (t : tm d n) -> (0 nc : NotClo t) => NonClo tm d n
-nclo t = Element t nc
-
-parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
-  ||| if the input term has any top-level closures, push them under one layer of
-  ||| syntax
-  export %inline
-  pushSubsts : tm d n -> NonClo tm d n
-  pushSubsts s = pushSubstsWith id id s
-
-  export %inline
-  pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
-  pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
-
-  export %inline
-  pushSubsts' : tm d n -> tm d n
-  pushSubsts' s = fst $ pushSubsts s
+dsubElim (F x l loc) th = th0 $ F x l loc
+dsubElim (B loc) th = Th2 zero id' $ B loc
+dsubElim (DCloE (Sub e ph)) th = th1 $ DCloE $ Sub e $ ph . th
+dsubElim e th = th1 $ DCloE $ Sub e th
 
 mutual
-  public export
-  isCloT : CloTest Term
-  isCloT (CloT  {}) = True
-  isCloT (DCloT {}) = True
-  isCloT (E e)      = isCloE e
-  isCloT _          = False
+  namespace Term
+    export
+    (///) : {d1, d2, n : Nat} -> TermT d1 n -> DSubst d1 d2 -> TermT d2 n
+    Th2 dope tope term /// th =
+      let Val tscope = appOpe n tope; Val dscope = appOpe d1 dope
+          Th2 dope' tope' term' = dsubTerm term (select dope th)
+      in
+      Th2 dope' (tope . tope') term'
 
-  public export
-  isCloE : CloTest Elim
-  isCloE (CloE  {}) = True
-  isCloE (DCloE {}) = True
-  isCloE _          = False
-
-mutual
-  export
-  PushSubsts Term Subst.isCloT where
-    pushSubstsWith th ph (TYPE l loc) =
-      nclo $ TYPE l loc
-    pushSubstsWith th ph (Pi qty a body loc) =
-      nclo $ Pi qty (a // th // ph) (body // th // ph) loc
-    pushSubstsWith th ph (Lam body loc) =
-      nclo $ Lam (body // th // ph) loc
-    pushSubstsWith th ph (Sig a b loc) =
-      nclo $ Sig (a // th // ph) (b // th // ph) loc
-    pushSubstsWith th ph (Pair s t loc) =
-      nclo $ Pair (s // th // ph) (t // th // ph) loc
-    pushSubstsWith th ph (Enum tags loc) =
-      nclo $ Enum tags loc
-    pushSubstsWith th ph (Tag tag loc) =
-      nclo $ Tag tag loc
-    pushSubstsWith th ph (Eq ty l r loc) =
-      nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
-    pushSubstsWith th ph (DLam body loc) =
-      nclo $ DLam (body // th // ph) loc
-    pushSubstsWith _ _ (Nat loc) =
-      nclo $ Nat loc
-    pushSubstsWith _ _ (Zero loc) =
-      nclo $ Zero loc
-    pushSubstsWith th ph (Succ n loc) =
-      nclo $ Succ (n // th // ph) loc
-    pushSubstsWith th ph (BOX pi ty loc) =
-      nclo $ BOX pi (ty // th // ph) loc
-    pushSubstsWith th ph (Box val loc) =
-      nclo $ Box (val // th // ph) loc
-    pushSubstsWith th ph (E e) =
-      let Element e nc = pushSubstsWith th ph e in nclo $ E e
-    pushSubstsWith th ph (CloT (Sub s ps)) =
-      pushSubstsWith th (comp th ps ph) s
-    pushSubstsWith th ph (DCloT (Sub s ps)) =
-      pushSubstsWith (ps . th) ph s
-
-  export
-  PushSubsts Elim Subst.isCloE where
-    pushSubstsWith th ph (F x u loc) =
-      nclo $ F x u loc
-    pushSubstsWith th ph (B i loc) =
-      let res = getLoc ph i loc in
-      case nchoose $ isCloE res of
-        Left  yes => assert_total pushSubsts res
-        Right no  => Element res no
-    pushSubstsWith th ph (App f s loc) =
-      nclo $ App (f // th // ph) (s // th // ph) loc
-    pushSubstsWith th ph (CasePair pi p r b loc) =
-      nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
-    pushSubstsWith th ph (CaseEnum pi t r arms loc) =
-      nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
-               (map (\b => b // th // ph) arms) loc
-    pushSubstsWith th ph (CaseNat pi pi' n r z s loc) =
-      nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
-               (z // th // ph) (s // th // ph) loc
-    pushSubstsWith th ph (CaseBox pi x r b loc) =
-      nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc
-    pushSubstsWith th ph (DApp f d loc) =
-      nclo $ DApp (f // th // ph) (d // th) loc
-    pushSubstsWith th ph (Ann s a loc) =
-      nclo $ Ann (s // th // ph) (a // th // ph) loc
-    pushSubstsWith th ph (Coe ty p q val loc) =
-      nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc
-    pushSubstsWith th ph (Comp ty p q val r zero one loc) =
-      nclo $ Comp (ty // th // ph) (p // th) (q // th)
-                  (val // th // ph) (r // th)
-                  (zero // th // ph) (one // th // ph) loc
-    pushSubstsWith th ph (TypeCase ty ret arms def loc) =
-      nclo $ TypeCase (ty // th // ph) (ret  // th // ph)
-        (map (\t => t // th // ph) arms) (def // th // ph) loc
-    pushSubstsWith th ph (CloE (Sub e ps)) =
-      pushSubstsWith th (comp th ps ph) e
-    pushSubstsWith th ph (DCloE (Sub e ps)) =
-      pushSubstsWith (ps . th) ph e
+  namespace Elim
+    export
+    (///) : {d1, d2, n : Nat} -> ElimT d1 n -> DSubst d1 d2 -> ElimT d2 n
+    Th2 dope tope elim /// th =
+      let Val tscope = appOpe n tope; Val dscope = appOpe d1 dope
+          Th2 dope' tope' elim' = dsubElim elim (select dope th)
+      in
+      Th2 dope' (tope . tope') elim'
 
 
-private %inline
-CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
-         (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
-CompHY {ty, p, q, val, r, zero, one, loc} =
-  let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
-  Comp {
-    ty = dsub1 ty q, p, q,
-    val = E $ Coe ty p q val val.loc, r,
-    -- [fixme] better locations for these vars?
-    zero = SY zero.names $ E $
-      Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
-    one = SY one.names $ E $
-      Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
-    loc
-  }
+public export
+TSubst : Nat -> Nat -> Nat -> Type
+TSubst = Subst2 Elim
 
-public export %inline
-CompH' : (ty : DScopeTerm d n) ->
-         (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
-         (zero : DScopeTerm d n) ->
-         (one : DScopeTerm d n) ->
-         (loc : Loc) ->
-         Elim d n
-CompH' {ty, p, q, val, r, zero, one, loc} =
-  case dsqueeze ty of
-    S _ (N ty) => Comp   {ty, p, q, val, r, zero, one, loc}
-    S _ (Y _)  => CompHY {ty, p, q, val, r, zero, one, loc}
 
-||| heterogeneous composition, using Comp and Coe (and subst)
-|||
-||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ }
-||| ≔
-||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r {
-|||   0 j ⇒ coe [i ⇒ A] @j @q t₀;
-|||   1 j ⇒ coe [i ⇒ A] @j @q t₁
-||| }
-public export %inline
-CompH : (i : BindName) -> (ty : Term (S d) n) ->
-        (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
-        (j0 : BindName) -> (zero : Term (S d) n) ->
-        (j1 : BindName) -> (one : Term (S d) n) ->
-        (loc : Loc) ->
-        Elim d n
-CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
-  CompH' {ty = SY [< i] ty, p, q, val, r,
-          zero = SY [< j0] zero, one = SY [< j0] one, loc}
+public export %inline FromVar (Elim 0) where var = B
+
+export CanSubstSelf2 Elim
+
+private subTerm : {d, n1, n2 : Nat} -> Term d n1 -> TSubst d n1 n2 -> TermT d n2
+private subElim : {d, n1, n2 : Nat} -> Elim d n1 -> TSubst d n1 n2 -> ElimT d n2
+
+subTerm (TYPE l loc) th = th0 $ TYPE l loc
+subTerm (Nat loc) th = th0 $ Nat loc
+subTerm (Zero loc) th = th0 $ Zero loc
+subTerm (E e) th = let Th2 dope tope e' = subElim e th in Th2 dope tope $ E e'
+subTerm (CloT (Sub2 s ph)) th = th1 $ CloT $ Sub2 s $ ph .% th
+subTerm s th = th1 $ CloT $ Sub2 s th
+
+subElim (F x k loc) th = th0 $ F x k loc
+subElim (B loc) [< e] = e
+subElim (CloE (Sub2 e ph)) th = th1 $ CloE $ Sub2 e $ ph .% th
+subElim e th = th1 $ CloE $ Sub2 e th
+
+
+
+export
+CanSubstSelf2 Elim where
+  Th2 dope tope elim // th =
+    let
+        th' = select tope th
+    in
+    ?sube2
+
+-- namespace CanDSubst
+--   public export
+--   interface CanDSubst (0 tm : TermLike) where
+--     (//) : {d1 : Nat} -> Thinned2 tm d1 n -> Lazy (DSubst d1 d2) ->
+--            Thinned2 tm d2 n
+
+-- ||| does the minimal reasonable work:
+-- ||| - deletes the closure around an atomic constant like `TYPE`
+-- ||| - deletes an identity substitution
+-- ||| - composes (lazily) with an existing top-level dim-closure
+-- ||| - otherwise, wraps in a new closure
+-- export
+-- CanDSubst Term where
+--   Th2 _ _ (TYPE l loc)       // _        = Th2 zero zero $ TYPE l loc
+--   Th2 i j (DCloT (Sub s ph)) // th       =
+--     Th2 ?i' j $ DCloT $ Sub s $ ph . ?th'
+--   Th2 i j s                  // th       = ?sdf -- DCloT $ Sub s th
+
+-- -- private
+-- -- subDArgs : Elim d1 n -> DSubst d1 d2 -> Elim d2 n
+-- -- subDArgs (DApp f d loc) th = DApp (subDArgs f th) (d // th) loc
+-- -- subDArgs e              th = DCloE $ Sub e th
+
+-- -- ||| does the minimal reasonable work:
+-- -- ||| - deletes the closure around a term variable
+-- -- ||| - deletes an identity substitution
+-- -- ||| - composes (lazily) with an existing top-level dim-closure
+-- -- ||| - immediately looks up bound variables in a
+-- -- |||   top-level sequence of dimension applications
+-- -- ||| - otherwise, wraps in a new closure
+-- -- export
+-- -- CanDSubst Elim where
+-- --   e                // Shift SZ = e
+-- --   F x u loc        // _        = F x u loc
+-- --   B i loc          // _        = B i loc
+-- --   e@(DApp {})      // th       = subDArgs e th
+-- --   DCloE (Sub e ph) // th       = DCloE $ Sub e $ ph . th
+-- --   e                // th       = DCloE $ Sub e th
+
+-- -- namespace DSubst.ScopeTermN
+-- --   export %inline
+-- --   (//) : ScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
+-- --          ScopeTermN s d2 n
+-- --   S ns (Y body) // th = S ns $ Y $ body // th
+-- --   S ns (N body) // th = S ns $ N $ body // th
+
+-- -- namespace DSubst.DScopeTermN
+-- --   export %inline
+-- --   (//) : {s : Nat} ->
+-- --          DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
+-- --          DScopeTermN s d2 n
+-- --   S ns (Y body) // th = S ns $ Y $ body // pushN s th
+-- --   S ns (N body) // th = S ns $ N $ body // th
+
+
+-- -- export %inline FromVar (Elim d) where fromVarLoc = B
+-- -- export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
+
+
+-- -- ||| does the minimal reasonable work:
+-- -- ||| - deletes the closure around a *free* name
+-- -- ||| - deletes an identity substitution
+-- -- ||| - composes (lazily) with an existing top-level closure
+-- -- ||| - immediately looks up a bound variable
+-- -- ||| - otherwise, wraps in a new closure
+-- -- export
+-- -- CanSubstSelf (Elim d) where
+-- --   F x u loc       // _  = F x u loc
+-- --   B i loc         // th = getLoc 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
+
+-- -- namespace CanTSubst
+-- --   public export
+-- --   interface CanTSubst (0 tm : TermLike) where
+-- --     (//) : tm d n1 -> Lazy (TSubst d n1 n2) -> tm d n2
+
+-- -- ||| does the minimal reasonable work:
+-- -- ||| - deletes the closure around an atomic constant like `TYPE`
+-- -- ||| - deletes an identity substitution
+-- -- ||| - composes (lazily) with an existing top-level closure
+-- -- ||| - goes inside `E` in case it is a simple variable or something
+-- -- ||| - otherwise, wraps in a new closure
+-- -- export
+-- -- CanTSubst Term where
+-- --   TYPE l loc      // _  = TYPE l loc
+-- --   E e             // th = E $ e // th
+-- --   CloT (Sub s ph) // th = CloT $ Sub s $ ph . th
+-- --   s               // th = case force th of
+-- --                                Shift SZ => s
+-- --                                th       => CloT $ Sub s th
+
+-- -- namespace ScopeTermN
+-- --   export %inline
+-- --   (//) : {s : Nat} ->
+-- --          ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
+-- --          ScopeTermN s d n2
+-- --   S ns (Y body) // th = S ns $ Y $ body // pushN s th
+-- --   S ns (N body) // th = S ns $ N $ body // th
+
+-- -- namespace DScopeTermN
+-- --   export %inline
+-- --   (//) : {s : Nat} ->
+-- --          DScopeTermN s d n1 -> Lazy (TSubst d n1 n2) -> DScopeTermN s d n2
+-- --   S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
+-- --   S ns (N body) // th = S ns $ N $ body // th
+
+-- -- export %inline CanShift (Term d) where s // by = s // Shift by
+-- -- export %inline CanShift (Elim d) where e // by = e // Shift by
+
+-- -- export %inline
+-- -- {s : Nat} -> CanShift (ScopeTermN s d) where
+-- --   b // by = b // Shift by
+
+
+-- -- export %inline
+-- -- comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
+-- -- comp th ps ph = map (// th) ps . ph
+
+
+-- -- public export %inline
+-- -- dweakT : (by : Nat) -> Term d n -> Term (by + d) n
+-- -- dweakT by t = t // shift by
+
+-- -- public export %inline
+-- -- dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n
+-- -- dweakE by t = t // shift by
+
+
+-- -- public export %inline
+-- -- weakT : (by : Nat) -> Term d n -> Term d (by + n)
+-- -- weakT by t = t // shift by
+
+-- -- public export %inline
+-- -- weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
+-- -- weakE by t = t // shift by
+
+
+-- -- parameters {s : Nat}
+-- --   namespace ScopeTermBody
+-- --     export %inline
+-- --     (.term) : ScopedBody s (Term d) n -> Term d (s + n)
+-- --     (Y b).term = b
+-- --     (N b).term = weakT s b
+
+-- --   namespace ScopeTermN
+-- --     export %inline
+-- --     (.term) : ScopeTermN s d n -> Term d (s + n)
+-- --     t.term = t.body.term
+
+-- --   namespace DScopeTermBody
+-- --     export %inline
+-- --     (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
+-- --     (Y b).term = b
+-- --     (N b).term = dweakT s b
+
+-- --   namespace DScopeTermN
+-- --     export %inline
+-- --     (.term) : DScopeTermN s d n -> Term (s + d) n
+-- --     t.term = t.body.term
+
+
+-- -- export %inline
+-- -- subN : ScopeTermN s d n -> SnocVect s (Elim d n) -> Term d n
+-- -- subN (S _ (Y body)) es = body // fromSnocVect es
+-- -- subN (S _ (N body)) _  = body
+
+-- -- export %inline
+-- -- sub1 : ScopeTerm d n -> Elim d n -> Term d n
+-- -- sub1 t e = subN t [< e]
+
+-- -- export %inline
+-- -- dsubN : DScopeTermN s d n -> SnocVect s (Dim d) -> Term d n
+-- -- dsubN (S _ (Y body)) ps = body // fromSnocVect ps
+-- -- dsubN (S _ (N body)) _  = body
+
+-- -- export %inline
+-- -- dsub1 : DScopeTerm d n -> Dim d -> Term d n
+-- -- dsub1 t p = dsubN t [< p]
+
+
+-- -- public export %inline
+-- -- (.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+-- -- body.zero = dsub1 body $ K Zero loc
+
+-- -- public export %inline
+-- -- (.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+-- -- body.one = dsub1 body $ K One loc
+
+
+-- -- public export
+-- -- 0 CloTest : TermLike -> Type
+-- -- CloTest tm = forall d, n. tm d n -> Bool
+
+-- -- interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
+-- --   pushSubstsWith : DSubst d1 d2 -> TSubst d2 n1 n2 ->
+-- --                    tm d1 n1 -> Subset (tm d2 n2) (No . isClo)
+
+-- -- public export
+-- -- 0 NotClo : {isClo : CloTest tm} -> PushSubsts tm isClo => Pred (tm d n)
+-- -- NotClo = No . isClo
+
+-- -- public export
+-- -- 0 NonClo : (tm : TermLike) -> {isClo : CloTest tm} ->
+-- --            PushSubsts tm isClo => TermLike
+-- -- NonClo tm d n = Subset (tm d n) NotClo
+
+-- -- public export %inline
+-- -- nclo : {isClo : CloTest tm} -> (0 _ : PushSubsts tm isClo) =>
+-- --        (t : tm d n) -> (0 nc : NotClo t) => NonClo tm d n
+-- -- nclo t = Element t nc
+
+-- -- parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
+-- --   ||| if the input term has any top-level closures, push them under one layer of
+-- --   ||| syntax
+-- --   export %inline
+-- --   pushSubsts : tm d n -> NonClo tm d n
+-- --   pushSubsts s = pushSubstsWith id id s
+
+-- --   export %inline
+-- --   pushSubstsWith' : DSubst d1 d2 -> TSubst d2 n1 n2 -> tm d1 n1 -> tm d2 n2
+-- --   pushSubstsWith' th ph x = fst $ pushSubstsWith th ph x
+
+-- --   export %inline
+-- --   pushSubsts' : tm d n -> tm d n
+-- --   pushSubsts' s = fst $ pushSubsts s
+
+-- -- mutual
+-- --   public export
+-- --   isCloT : CloTest Term
+-- --   isCloT (CloT  {}) = True
+-- --   isCloT (DCloT {}) = True
+-- --   isCloT (E e)      = isCloE e
+-- --   isCloT _          = False
+
+-- --   public export
+-- --   isCloE : CloTest Elim
+-- --   isCloE (CloE  {}) = True
+-- --   isCloE (DCloE {}) = True
+-- --   isCloE _          = False
+
+-- -- mutual
+-- --   export
+-- --   PushSubsts Term Subst.isCloT where
+-- --     pushSubstsWith th ph (TYPE l loc) =
+-- --       nclo $ TYPE l loc
+-- --     pushSubstsWith th ph (Pi qty a body loc) =
+-- --       nclo $ Pi qty (a // th // ph) (body // th // ph) loc
+-- --     pushSubstsWith th ph (Lam body loc) =
+-- --       nclo $ Lam (body // th // ph) loc
+-- --     pushSubstsWith th ph (Sig a b loc) =
+-- --       nclo $ Sig (a // th // ph) (b // th // ph) loc
+-- --     pushSubstsWith th ph (Pair s t loc) =
+-- --       nclo $ Pair (s // th // ph) (t // th // ph) loc
+-- --     pushSubstsWith th ph (Enum tags loc) =
+-- --       nclo $ Enum tags loc
+-- --     pushSubstsWith th ph (Tag tag loc) =
+-- --       nclo $ Tag tag loc
+-- --     pushSubstsWith th ph (Eq ty l r loc) =
+-- --       nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
+-- --     pushSubstsWith th ph (DLam body loc) =
+-- --       nclo $ DLam (body // th // ph) loc
+-- --     pushSubstsWith _ _ (Nat loc) =
+-- --       nclo $ Nat loc
+-- --     pushSubstsWith _ _ (Zero loc) =
+-- --       nclo $ Zero loc
+-- --     pushSubstsWith th ph (Succ n loc) =
+-- --       nclo $ Succ (n // th // ph) loc
+-- --     pushSubstsWith th ph (BOX pi ty loc) =
+-- --       nclo $ BOX pi (ty // th // ph) loc
+-- --     pushSubstsWith th ph (Box val loc) =
+-- --       nclo $ Box (val // th // ph) loc
+-- --     pushSubstsWith th ph (E e) =
+-- --       let Element e nc = pushSubstsWith th ph e in nclo $ E e
+-- --     pushSubstsWith th ph (CloT (Sub s ps)) =
+-- --       pushSubstsWith th (comp th ps ph) s
+-- --     pushSubstsWith th ph (DCloT (Sub s ps)) =
+-- --       pushSubstsWith (ps . th) ph s
+
+-- --   export
+-- --   PushSubsts Elim Subst.isCloE where
+-- --     pushSubstsWith th ph (F x u loc) =
+-- --       nclo $ F x u loc
+-- --     pushSubstsWith th ph (B i loc) =
+-- --       let res = getLoc ph i loc in
+-- --       case nchoose $ isCloE res of
+-- --         Left  yes => assert_total pushSubsts res
+-- --         Right no  => Element res no
+-- --     pushSubstsWith th ph (App f s loc) =
+-- --       nclo $ App (f // th // ph) (s // th // ph) loc
+-- --     pushSubstsWith th ph (CasePair pi p r b loc) =
+-- --       nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
+-- --     pushSubstsWith th ph (CaseEnum pi t r arms loc) =
+-- --       nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
+-- --                (map (\b => b // th // ph) arms) loc
+-- --     pushSubstsWith th ph (CaseNat pi pi' n r z s loc) =
+-- --       nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
+-- --                (z // th // ph) (s // th // ph) loc
+-- --     pushSubstsWith th ph (CaseBox pi x r b loc) =
+-- --       nclo $ CaseBox pi (x // th // ph) (r // th // ph) (b // th // ph) loc
+-- --     pushSubstsWith th ph (DApp f d loc) =
+-- --       nclo $ DApp (f // th // ph) (d // th) loc
+-- --     pushSubstsWith th ph (Ann s a loc) =
+-- --       nclo $ Ann (s // th // ph) (a // th // ph) loc
+-- --     pushSubstsWith th ph (Coe ty p q val loc) =
+-- --       nclo $ Coe (ty // th // ph) (p // th) (q // th) (val // th // ph) loc
+-- --     pushSubstsWith th ph (Comp ty p q val r zero one loc) =
+-- --       nclo $ Comp (ty // th // ph) (p // th) (q // th)
+-- --                   (val // th // ph) (r // th)
+-- --                   (zero // th // ph) (one // th // ph) loc
+-- --     pushSubstsWith th ph (TypeCase ty ret arms def loc) =
+-- --       nclo $ TypeCase (ty // th // ph) (ret  // th // ph)
+-- --         (map (\t => t // th // ph) arms) (def // th // ph) loc
+-- --     pushSubstsWith th ph (CloE (Sub e ps)) =
+-- --       pushSubstsWith th (comp th ps ph) e
+-- --     pushSubstsWith th ph (DCloE (Sub e ps)) =
+-- --       pushSubstsWith (ps . th) ph e
+
+
+-- -- private %inline
+-- -- CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
+-- --          (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
+-- -- CompHY {ty, p, q, val, r, zero, one, loc} =
+-- --   let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
+-- --   Comp {
+-- --     ty = dsub1 ty q, p, q,
+-- --     val = E $ Coe ty p q val val.loc, r,
+-- --     -- [fixme] better locations for these vars?
+-- --     zero = SY zero.names $ E $
+-- --       Coe ty' (B VZ zero.loc) (weakD 1 q) zero.term zero.loc,
+-- --     one = SY one.names $ E $
+-- --       Coe ty' (B VZ one.loc) (weakD 1 q) one.term one.loc,
+-- --     loc
+-- --   }
+
+-- -- public export %inline
+-- -- CompH' : (ty : DScopeTerm d n) ->
+-- --          (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
+-- --          (zero : DScopeTerm d n) ->
+-- --          (one : DScopeTerm d n) ->
+-- --          (loc : Loc) ->
+-- --          Elim d n
+-- -- CompH' {ty, p, q, val, r, zero, one, loc} =
+-- --   case dsqueeze ty of
+-- --     S _ (N ty) => Comp   {ty, p, q, val, r, zero, one, loc}
+-- --     S _ (Y _)  => CompHY {ty, p, q, val, r, zero, one, loc}
+
+-- -- ||| heterogeneous composition, using Comp and Coe (and subst)
+-- -- |||
+-- -- ||| comp [i ⇒ A] @p @q s @r { 0 j ⇒ t₀; 1 j ⇒ t₁ }
+-- -- ||| ≔
+-- -- ||| comp [A‹q/i›] @p @q (coe [i ⇒ A] @p @q s) @r {
+-- -- |||   0 j ⇒ coe [i ⇒ A] @j @q t₀;
+-- -- |||   1 j ⇒ coe [i ⇒ A] @j @q t₁
+-- -- ||| }
+-- -- public export %inline
+-- -- CompH : (i : BindName) -> (ty : Term (S d) n) ->
+-- --         (p, q : Dim d) -> (val : Term d n) -> (r : Dim d) ->
+-- --         (j0 : BindName) -> (zero : Term (S d) n) ->
+-- --         (j1 : BindName) -> (one : Term (S d) n) ->
+-- --         (loc : Loc) ->
+-- --         Elim d n
+-- -- CompH {i, ty, p, q, val, r, j0, zero, j1, one, loc} =
+-- --   CompH' {ty = SY [< i] ty, p, q, val, r,
+-- --           zero = SY [< j0] zero, one = SY [< j0] one, loc}

lib/Quox/Syntax/Var.idr

@@ -138,15 +138,6 @@ export
 weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
 
 
-public export
-interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n
-
-public export %inline
-fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n
-fromVar x = fromVarLoc x loc
-
-public export FromVar Var where fromVarLoc x _ = x
-
 export
 tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->
             (n : Nat) -> Vect n (tm n)

lib/Quox/Thin.idr

@@ -0,0 +1,13 @@
+module Quox.Thin
+
+import public Quox.Thin.Base
+import public Quox.Thin.View
+import public Quox.Thin.Eqv
+import public Quox.Thin.Cons
+import public Quox.Thin.List
+import public Quox.Thin.Append
+import public Quox.Thin.Comp
+import public Quox.Thin.Cover
+import public Quox.Thin.Coprod
+import public Quox.Thin.Split
+import public Quox.Thin.Term

lib/Quox/Thin/Append.idr

@@ -0,0 +1,27 @@
+module Quox.Thin.Append
+
+import public Quox.Thin.Base
+import public Quox.Thin.View
+import Data.DPair
+
+%default total
+
+public export
+app' : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Exists (OPE (m1 + m2) (n1 + n2))
+app' Stop             ope2 = Evidence _ ope2
+app' (Drop ope1 Refl) ope2 = Evidence _ $ Drop (app' ope1 ope2).snd Refl
+app' (Keep ope1 Refl) ope2 = Evidence _ $ Keep (app' ope1 ope2).snd Refl
+
+public export
+(++) : {n1, n2, mask1, mask2 : Nat} ->
+       (0 ope1 : OPE m1 n1 mask1) -> (0 ope2 : OPE m2 n2 mask2) ->
+       Subset Nat (OPE (m1 + m2) (n1 + n2))
+ope1 ++ ope2 with %syntactic (view ope1)
+  Stop           ++ ope2 | StopV = Element _ ope2
+  Drop ope1 Refl ++ ope2 | DropV mask ope1 =
+    Element _ $ Drop (ope1 ++ ope2).snd Refl
+  Keep ope1 Refl ++ ope2 | KeepV mask ope1 =
+    Element _ $ Keep (ope1 ++ ope2).snd Refl
+
+-- [todo] this mask is just (mask1 << n2) | mask2
+-- prove it and add %transform

lib/Quox/Thin/Base.idr

@@ -0,0 +1,81 @@
+module Quox.Thin.Base
+
+import Data.Fin
+import Data.DPair
+
+%default total
+
+||| "order preserving embeddings", for recording a correspondence between a
+||| smaller scope and part of a larger one. the third argument is a bitmask
+||| representing this OPE, unique for a given `n`.
+public export
+data OPE : (m, n, mask : Nat) -> Type where
+  [search m n]
+  Stop : OPE 0 0 0
+  Drop : OPE m n mask -> mask' = mask + mask       -> OPE m     (S n) mask'
+  Keep : OPE m n mask -> mask' = (S (mask + mask)) -> OPE (S m) (S n) mask'
+%name OPE ope
+
+export
+Show (OPE m n mask) where
+  showPrec d Stop            = "Stop"
+  showPrec d (Drop ope Refl) = showCon d "Drop" $ showArg ope ++ " Refl"
+  showPrec d (Keep ope Refl) = showCon d "Keep" $ showArg ope ++ " Refl"
+
+public export %inline
+drop : OPE m n mask -> OPE m (S n) (mask + mask)
+drop ope = Drop ope Refl
+
+public export %inline
+keep : OPE m n mask -> OPE (S m) (S n) (S (mask + mask))
+keep ope = Keep ope Refl
+
+
+public export
+data IsStop : OPE m n mask -> Type where ItIsStop : IsStop Stop
+
+public export
+data IsDrop : OPE m n mask -> Type where ItIsDrop : IsDrop (Drop ope eq)
+
+public export
+data IsKeep : OPE m n mask -> Type where ItIsKeep : IsKeep (Keep ope eq)
+
+
+export
+0 zeroIsStop : (ope : OPE m 0 mask) -> IsStop ope
+zeroIsStop Stop = ItIsStop
+
+
+||| everything selected
+public export
+id : {m : Nat} -> Subset Nat (OPE m m)
+id {m = 0}   = Element _ Stop
+id {m = S m} = Element _ $ Keep id.snd Refl
+
+public export %inline
+0 id' : {m : Nat} -> OPE m m (fst (Base.id {m}))
+id' = id.snd
+
+||| nothing selected
+public export
+zero : {m : Nat} -> OPE 0 m 0
+zero {m = 0}   = Stop
+zero {m = S m} = Drop zero Refl
+
+||| a single slot selected
+public export
+one : Fin n -> Subset Nat (OPE 1 n)
+one FZ     = Element _ $ keep zero
+one (FS i) = Element _ $ drop (one i).snd
+
+public export %inline
+0 one' : (i : Fin n) -> OPE 1 n (one i).fst
+one' i = (one i).snd
+
+
+public export
+record SomeOPE n where
+  constructor MkOPE
+  {0 scope : Nat}
+  {mask : Nat}
+  0 ope : OPE scope n mask

lib/Quox/Thin/Comp.idr

@@ -0,0 +1,55 @@
+module Quox.Thin.Comp
+
+import public Quox.Thin.Base
+import public Quox.Thin.View
+import Quox.NatExtra
+import Data.Singleton
+
+%default total
+
+||| inductive definition of OPE composition
+public export
+data Comp : (l : OPE n p mask1) -> (r : OPE m n mask2) ->
+            (res : OPE m p mask3) -> Type where
+  [search l r]
+  StopZ : Comp Stop Stop Stop
+  DropZ : Comp a b c -> Comp (Drop a Refl) b (Drop c Refl)
+  KeepZ : Comp a b c -> Comp (Keep a Refl) (Keep b Refl) (Keep c Refl)
+  KDZ   : Comp a b c -> Comp (Keep a Refl) (Drop b Refl) (Drop c Refl)
+
+public export
+record CompResult (ope1 : OPE n p mask1) (ope2 : OPE m n mask2) where
+  constructor MkComp
+  {mask : Nat}
+  {0 ope : OPE m p mask}
+  0 comp : Comp ope1 ope2 ope
+%name CompResult comp
+
+||| compose two OPEs, if the middle scope size is already known at runtime
+export
+comp' : {n, p, mask1, mask2 : Nat} ->
+        (0 ope1 : OPE n p mask1) -> (0 ope2 : OPE m n mask2) ->
+        CompResult ope1 ope2
+comp' ope1 ope2 with %syntactic (view ope1) | (view ope2)
+  comp' Stop Stop | StopV | StopV =
+    MkComp StopZ
+  comp' (Drop ope1 Refl) ope2 | DropV _ ope1 | _ =
+    MkComp $ DropZ (comp' ope1 ope2).comp
+  comp' (Keep ope1 Refl) (Drop ope2 Refl) | KeepV _ ope1 | DropV _ ope2 =
+    MkComp $ KDZ (comp' ope1 ope2).comp
+  comp' (Keep ope1 Refl) (Keep ope2 Refl) | KeepV _ ope1 | KeepV _ ope2 =
+    MkComp $ KeepZ (comp' ope1 ope2).comp
+
+||| compose two OPEs, after recomputing the middle scope size using `appOpe`
+export
+comp : {p, mask1, mask2 : Nat} ->
+       (0 ope1 : OPE n p mask1) -> (0 ope2 : OPE m n mask2) ->
+       CompResult ope1 ope2
+comp ope1 ope2 = let Val n = appOpe p ope1 in comp' ope1 ope2
+
+-- [todo] is there a quick way to compute the mask of comp?
+
+export
+0 (.) : (ope1 : OPE n p mask1) -> (ope2 : OPE m n mask2) ->
+        OPE m p (comp ope1 ope2).mask
+ope1 . ope2 = (comp ope1 ope2).ope

lib/Quox/Thin/Cons.idr

@@ -0,0 +1,74 @@
+module Quox.Thin.Cons
+
+import public Quox.Thin.Base
+import Quox.Thin.Eqv
+import Quox.Thin.View
+import Data.DPair
+import Control.Relation
+
+%default total
+
+
+public export
+data IsHead : (ope : OPE m (S n) mask) -> Bool -> Type where
+  [search ope]
+  DropH : IsHead (Drop ope eq) False
+  KeepH : IsHead (Keep ope eq) True
+
+public export
+data IsTail : (full : OPE m (S n) mask) -> OPE m' n mask' -> Type where
+  [search full]
+  DropT : IsTail (Drop ope eq) ope
+  KeepT : IsTail (Keep ope eq) ope
+
+public export
+record Uncons (ope : OPE m (S n) mask) where
+  constructor MkUncons
+  0 head : Bool
+  {tailMask : Nat}
+  0 tail : OPE scope n tailMask
+  {auto isHead : IsHead ope head}
+  {auto 0 isTail : IsTail ope tail}
+
+public export
+uncons : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Uncons ope
+uncons ope with %syntactic (view ope)
+  uncons (Drop ope Refl) | DropV _ ope = MkUncons False ope
+  uncons (Keep ope Refl) | KeepV _ ope = MkUncons True  ope
+
+public export
+head : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Exists $ IsHead ope
+head ope = Evidence _ (uncons ope).isHead
+
+public export
+record Tail (ope : OPE m (S n) mask) where
+  constructor MkTail
+  {tailMask : Nat}
+  0 tail : OPE scope n tailMask
+  {auto 0 isTail : IsTail ope tail}
+
+public export
+tail : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Tail ope
+tail ope = let u = uncons ope in MkTail u.tail @{u.isTail}
+
+
+export
+cons : {mask : Nat} -> (head : Bool) -> (0 tail : OPE m n mask) ->
+       Subset Nat (OPE (if head then S m else m) (S n))
+cons False tail = Element _ $ drop tail
+cons True  tail = Element _ $ keep tail
+
+export
+0 consEquiv' : (self : OPE m' (S n) mask') ->
+               (head : Bool) -> (tail : OPE m n mask) ->
+               IsHead self head -> IsTail self tail ->
+               (cons head tail).snd `Eqv` self
+consEquiv' (Drop tail _) False tail DropH DropT = EqvDrop reflexive
+consEquiv' (Keep tail _) True  tail KeepH KeepT = EqvKeep reflexive
+
+export
+0 consEquiv : (full : OPE m' (S n) mask') ->
+              (cons (uncons full).head (uncons full).tail).snd `Eqv` full
+consEquiv full with %syntactic (uncons full)
+  _ | MkUncons head tail {isHead, isTail} =
+    consEquiv' full head tail isHead isTail

lib/Quox/Thin/Coprod.idr

@@ -0,0 +1,171 @@
+module Quox.Thin.Coprod
+
+import public Quox.Thin.Base
+import public Quox.Thin.Comp
+import public Quox.Thin.View
+import public Quox.Thin.List
+import public Quox.Thin.Cover
+import Data.DPair
+import Data.Nat
+import Control.Function
+
+%default total
+
+
+namespace Coprod
+  public export
+  data Comps : OPE scope n scopeMask ->
+               OPEList scope -> OPEList n -> Type where
+    Nil  : Comps sub [] []
+    (::) : Comp  sub inner  full ->
+           Comps sub inners fulls ->
+           Comps sub (inner :: inners) (full :: fulls)
+  %name Comps comps
+
+  public export
+  record Coprod (fulls : OPEList n) where
+    constructor MkCoprod
+    {scopeMask : Nat}
+    {0 sub : OPE scope n scopeMask}
+    inners : OPEList scope
+    0 comps : Comps sub inners fulls
+    0 cov : Cover inners
+  %name Coprod cop
+
+export
+0 compsLength : Comps s ts us -> length ts = length us
+compsLength []           = Refl
+compsLength (_ :: comps) = cong S $ compsLength comps
+
+
+export
+coprodNil : Coprod []
+coprodNil = MkCoprod [] [] [] {sub = zero}
+
+private
+coprodHead : {n : Nat} -> (opes : OPEList (S n)) ->
+             Either (Cover1 opes) (All IsDrop opes)
+coprodHead [] = Right []
+coprodHead (ope :: opes) = case view ope of
+  DropV {} => case coprodHead opes of
+    Left  cov1  => Left  $ There cov1
+    Right drops => Right $ ItIsDrop :: drops
+  KeepV {} => Left Here
+
+
+private
+0 compsConsDrop : (opes : OPEList (S n)) ->
+                  All IsDrop opes ->
+                  All2 IsTail opes tails ->
+                  Comps sub inners tails -> Comps (drop sub) inners opes
+compsConsDrop [] [] [] [] = []
+compsConsDrop (Drop ope Refl :: opes) (ItIsDrop :: ds) (DropT :: ts) (c :: cs) =
+  DropZ c :: compsConsDrop opes ds ts cs
+compsConsDrop (_ :: _) [] _ _ impossible
+
+private
+coprodConsDrop : (0 opes : OPEList (S n)) ->
+                 (0 ds : All IsDrop opes) ->
+                 (0 ts : All2 IsTail opes tails) ->
+                 Coprod tails -> Coprod opes
+coprodConsDrop opes ds ts (MkCoprod inners comps cov) =
+  MkCoprod inners (compsConsDrop opes ds ts comps) cov
+
+
+private
+copyHeads : {m : Nat} ->
+            (src : OPEList (S m)) -> (tgt : OPEList n) ->
+            (0 eq : length src = length tgt) => OPEList (S n)
+copyHeads [] [] = []
+copyHeads (s :: ss) (t :: ts) =
+  case view s of
+    DropV mask ope => drop t :: copyHeads ss ts @{inj S eq}
+    KeepV mask ope => keep t :: copyHeads ss ts @{inj S eq}
+
+private
+0 copyHeadsComps : (eq : length outers = length inners) ->
+                   All2 IsTail outers tails ->
+                   Comps sub inners tails ->
+                   Comps (keep sub) (copyHeads outers inners) outers
+copyHeadsComps _ [] [] = []
+copyHeadsComps eq (DropT {eq = eq2} :: ps) ((c :: cs) {full}) =
+  let (Refl) = eq2 in -- coverage checker weirdness
+  rewrite viewDrop full Refl in
+  KDZ c :: copyHeadsComps (inj S eq) ps cs
+copyHeadsComps eq (KeepT {eq = eq2} :: ps) ((c :: cs) {full}) =
+  let (Refl) = eq2 in
+  rewrite viewKeep full Refl in
+  KeepZ c :: copyHeadsComps (inj S eq) ps cs
+
+-- should be erased (coverage checker weirdness)
+-- it is possibly https://github.com/idris-lang/Idris2/issues/1417 that keeps
+-- happening. not 100% sure
+private
+cover1CopyHeads : {m : Nat} ->
+                  (ss : OPEList (S m)) -> (ts : OPEList n) ->
+                  (eq : length ss = length ts) ->
+                  (cov1 : Cover1 ss) -> Cover1 (copyHeads ss ts)
+cover1CopyHeads (Keep s Refl :: ss) (t :: ts) eq Here =
+  rewrite viewKeep s Refl in Here
+cover1CopyHeads (s :: ss) (t :: ts) eq (There c) with (view s)
+  cover1CopyHeads (Drop {} :: ss) (t :: ts) eq (There c) | DropV {} =
+    There $ cover1CopyHeads ss ts (inj S eq) c
+  cover1CopyHeads (Keep {} :: ss) (t :: ts) eq (There c) | KeepV {} =
+    Here
+
+private
+copyHeadsTails : {m : Nat} ->
+                 (ss : OPEList (S m)) -> (ts : OPEList n) ->
+                 (eq : length ss = length ts) ->
+                 All2 IsTail (copyHeads ss ts) ts
+copyHeadsTails [] [] eq = []
+copyHeadsTails (s :: ss) (t :: ts) eq with (view s)
+  copyHeadsTails (Drop ope Refl :: ss) (t :: ts) eq | DropV mask ope =
+    DropT :: copyHeadsTails ss ts (inj S eq)
+  copyHeadsTails (Keep ope Refl :: ss) (t :: ts) eq | KeepV mask ope =
+    KeepT :: copyHeadsTails ss ts (inj S eq)
+
+private
+coprodConsKeep : {n : Nat} ->
+                 (opes : OPEList (S n)) ->
+                 {0 tails : OPEList n} ->
+                 (cov1 : Cover1 opes) ->
+                 (0 ts : All2 IsTail opes tails) ->
+                 Coprod tails -> Coprod opes
+coprodConsKeep opes cov1 ts (MkCoprod inners comps cov) =
+  MkCoprod
+    (copyHeads opes inners @{all2Length ts `trans` sym (compsLength comps)})
+    (copyHeadsComps _ ts comps)
+    ((cover1CopyHeads {cov1, _} :: cov) @{copyHeadsTails {}})
+
+
+export
+coprod : {n : Nat} -> (opes : OPEList n) -> Coprod opes
+
+private
+coprod0 : (opes : OPEList 0) -> Coprod opes
+
+private
+coprodS : {n : Nat} -> (opes : OPEList (S n)) -> Coprod opes
+
+coprod {n = 0}   opes = coprod0 opes
+coprod {n = S n} opes = coprodS opes
+
+coprod0 [] = coprodNil
+coprod0 (ope :: opes) with %syntactic 0 (zeroIsStop ope) | (coprod opes)
+  coprod0 (Stop :: opes)
+      | ItIsStop | MkCoprod {sub} inners comps cov
+      with %syntactic 0 (zeroIsStop sub)
+    coprod0 (Stop :: opes)
+      | ItIsStop | MkCoprod {sub = Stop} inners comps cov | ItIsStop
+      = MkCoprod (Stop :: inners) (StopZ :: comps) []
+
+coprodS [] = coprodNil
+coprodS opes =
+  let hs              = heads opes
+      Element ts tprf = tails_ opes
+      tcop            = coprod $ assert_smaller opes ts
+  in
+  case coprodHead opes of
+    Left  cov1  => coprodConsKeep opes cov1 tprf tcop
+    Right drops => coprodConsDrop opes drops tprf tcop

lib/Quox/Thin/Cover.idr

@@ -0,0 +1,27 @@
+module Quox.Thin.Cover
+
+import public Quox.Thin.Base
+import public Quox.Thin.List
+
+%default total
+
+||| an OPE list is a cover if at least one of the OPEs has `Keep` as the head,
+||| and the tails are also a cover
+|||
+||| in @egtbs it is a binary relation which is fine for ×ᵣ but i don't want to
+||| write my AST in universe-of-syntaxes style. sorry
+public export data Cover : OPEList n -> Type
+
+||| the "`Keep` in the head" condition of a cover
+public export data Cover1 : OPEList n -> Type
+
+data Cover where
+  Nil  : Cover opes {n = 0}
+  (::) : Cover1 opes -> All2 IsTail opes tails => Cover tails -> Cover opes
+%name Cover cov
+
+data Cover1 where
+  Here  : Cover1 (Keep ope eq :: opes)
+  There : Cover1 opes -> Cover1 (ope :: opes)
+%name Cover1 cov1
+%builtin Natural Cover1

lib/Quox/Thin/Eqv.idr

@@ -0,0 +1,128 @@
+module Quox.Thin.Eqv
+
+import public Quox.Thin.Base
+import public Quox.Thin.View
+import Quox.NatExtra
+import Syntax.PreorderReasoning
+
+%default total
+
+infix 6 `Eqv`
+
+private
+uip : (p, q : a = b) -> p = q
+uip Refl Refl = Refl
+
+
+public export
+data Eqv : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Type where
+  EqvStop : Eqv Stop Stop
+  EqvDrop : {0 p : OPE m1 n1 mask1} ->
+            {0 q : OPE m2 n2 mask2} ->
+            Eqv p q -> Eqv (Drop p eq1) (Drop q eq2)
+  EqvKeep : {0 p : OPE m1 n1 mask1} ->
+            {0 q : OPE m2 n2 mask2} ->
+            Eqv p q -> Eqv (Keep p eq1) (Keep q eq2)
+%name Eqv eqv
+
+export Uninhabited (Stop     `Eqv` Drop p e) where uninhabited _ impossible
+export Uninhabited (Stop     `Eqv` Keep p e) where uninhabited _ impossible
+export Uninhabited (Drop p e `Eqv` Stop)     where uninhabited _ impossible
+export Uninhabited (Drop p e `Eqv` Keep q f) where uninhabited _ impossible
+export Uninhabited (Keep p e `Eqv` Stop)     where uninhabited _ impossible
+export Uninhabited (Keep p e `Eqv` Drop q f) where uninhabited _ impossible
+
+export
+Reflexive (OPE m n mask) Eqv where
+  reflexive {x = Stop}    = EqvStop
+  reflexive {x = Drop {}} = EqvDrop reflexive
+  reflexive {x = Keep {}} = EqvKeep reflexive
+
+export
+symmetric : p `Eqv` q -> q `Eqv` p
+symmetric EqvStop       = EqvStop
+symmetric (EqvDrop eqv) = EqvDrop $ symmetric eqv
+symmetric (EqvKeep eqv) = EqvKeep $ symmetric eqv
+
+export
+transitive : p `Eqv` q -> q `Eqv` r -> p `Eqv` r
+transitive EqvStop        EqvStop        = EqvStop
+transitive (EqvDrop eqv1) (EqvDrop eqv2) = EqvDrop (transitive eqv1 eqv2)
+transitive (EqvKeep eqv1) (EqvKeep eqv2) = EqvKeep (transitive eqv1 eqv2)
+
+
+private
+recompute' : {mask1, mask2, n1, n2 : Nat} ->
+             (0 p : OPE m1 n1 mask1) -> (0 q : OPE m2 n2 mask2) ->
+             (0 eqv : p `Eqv` q) -> p `Eqv` q
+recompute' p q eqv with %syntactic (view p) | (view q)
+  recompute' Stop Stop _ | StopV | StopV = EqvStop
+  recompute' (Drop p _) (Drop q _) eqv | DropV _ p | DropV _ q =
+    EqvDrop $ recompute' {eqv = let EqvDrop e = eqv in e, _}
+  recompute' (Keep p _) (Keep q _) eqv | KeepV _ p | KeepV _ q =
+    EqvKeep $ recompute' {eqv = let EqvKeep e = eqv in e, _}
+  recompute' (Drop p _) (Keep q _) eqv | DropV _ p | KeepV _ q =
+    void $ absurd eqv
+  recompute' (Keep p _) (Drop q _) eqv | KeepV _ p | DropV _ q =
+    void $ absurd eqv
+
+private
+recompute : {mask1, mask2, n1, n2 : Nat} ->
+            {0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
+            (0 _ : p `Eqv` q) -> p `Eqv` q
+recompute eqv = recompute' {eqv, _}
+
+
+export
+eqvIndices : {0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
+             p `Eqv` q -> (m1 = m2, n1 = n2, mask1 = mask2)
+eqvIndices EqvStop = (Refl, Refl, Refl)
+eqvIndices (EqvDrop eqv {eq1 = Refl, eq2 = Refl}) =
+  let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
+eqvIndices (EqvKeep eqv {eq1 = Refl, eq2 = Refl}) =
+  let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
+
+export
+0 eqvMask : (p : OPE m1 n mask1) -> (q : OPE m2 n mask2) ->
+            mask1 = mask2 -> p `Eqv` q
+eqvMask Stop Stop _ = EqvStop
+eqvMask (Drop ope1 Refl) (Drop {mask = mm2} ope2 eq2) Refl =
+  EqvDrop $ eqvMask ope1 ope2 (doubleInj _ _ eq2)
+eqvMask (Drop ope1 Refl) (Keep ope2 eq2) Refl =
+  void $ notEvenOdd _ _ eq2
+eqvMask (Keep ope1 eq1) (Keep ope2 eq2) Refl =
+  EqvKeep $ eqvMask ope1 ope2 (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
+eqvMask (Keep ope1 eq1) (Drop ope2 eq2) Refl =
+  void $ notEvenOdd _ _ $ trans (sym eq2) eq1
+
+export
+0 eqvEq : (p, q : OPE m n mask) -> p `Eqv` q -> p === q
+eqvEq Stop Stop EqvStop = Refl
+eqvEq (Drop p eq1) (Drop q eq2) (EqvDrop eqv)
+    with %syntactic (doubleInj _ _ $ trans (sym eq1) eq2)
+  _ | Refl = cong2 Drop (eqvEq p q eqv) (uip eq1 eq2)
+eqvEq (Keep p eq1) (Keep q eq2) (EqvKeep eqv)
+    with %syntactic (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
+  _ | Refl = cong2 Keep (eqvEq p q eqv) (uip eq1 eq2)
+
+export
+0 eqvEq' : (p : OPE m1 n1 mask1) -> (q : OPE m2 n2 mask2) ->
+           p `Eqv` q -> p ~=~ q
+eqvEq' p q eqv = let (Refl, Refl, Refl) = eqvIndices eqv in eqvEq p q eqv
+
+export
+0 maskEqInner : (0 ope1 : OPE m1 n mask1) -> (0 ope2 : OPE m2 n mask2) ->
+                mask1 = mask2 -> m1 = m2
+maskEqInner Stop Stop _ = Refl
+maskEqInner (Drop ope1 Refl) (Drop ope2 Refl) eq =
+  maskEqInner ope1 ope2 (doubleInj _ _ eq)
+maskEqInner (Keep ope1 Refl) (Keep ope2 Refl) eq =
+  cong S $ maskEqInner ope1 ope2 $ doubleInj _ _ $ inj S eq
+maskEqInner (Drop ope1 Refl) (Keep ope2 Refl) eq = void $ notEvenOdd _ _ eq
+maskEqInner (Keep {mask = mask1'} ope1 eq1) (Drop {mask = mask2'} ope2 eq2) eq =
+  -- matching on eq1, eq2, or eq here triggers that weird coverage bug ☹
+  void $ notEvenOdd _ _ $ Calc $
+    |~ mask2' + mask2'
+    ~~ mask2               ..<(eq2)
+    ~~ mask1               ..<(eq)
+    ~~ S (mask1' + mask1') ...(eq1)

lib/Quox/Thin/List.idr

@@ -0,0 +1,127 @@
+module Quox.Thin.List
+
+import public Quox.Thin.Base
+import public Quox.Thin.Cons
+import Data.DPair
+import Data.Nat
+import Control.Function
+
+%default total
+
+||| a list of OPEs of a given outer scope size
+||| (at runtime just the masks)
+public export
+data OPEList : Nat -> Type where
+  Nil  : OPEList n
+  (::) : {mask : Nat} -> (0 ope : OPE m n mask) -> OPEList n -> OPEList n
+%name OPEList opes
+
+public export
+length : OPEList n -> Nat
+length []          = 0
+length (_ :: opes) = S $ length opes
+
+public export
+toList : OPEList n -> List (SomeOPE n)
+toList []            = []
+toList (ope :: opes) = MkOPE ope :: toList opes
+
+public export
+fromList : List (SomeOPE n) -> OPEList n
+fromList []                = []
+fromList (MkOPE ope :: xs) = ope :: fromList xs
+
+
+public export
+0 Pred : Nat -> Type
+Pred n = forall m, mask. OPE m n mask -> Type
+
+public export
+0 Rel : Nat -> Nat -> Type
+Rel n1 n2 = forall m1, m2, mask1, mask2.
+            OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Type
+
+namespace All
+  public export
+  data All : Pred n -> OPEList n -> Type where
+    Nil  : {0 p : Pred n} -> All p []
+    (::) : {0 p : Pred n} -> p ope -> All p opes -> All p (ope :: opes)
+  %name All.All ps, qs
+
+namespace All2
+  public export
+  data All2 : Rel n1 n2 -> OPEList n1 -> OPEList n2 -> Type where
+    Nil  : {0 p : Rel n1 n2} -> All2 p [] []
+    (::) : {0 p : Rel n1 n2} -> p a b -> All2 p as bs ->
+           All2 p (a :: as) (b :: bs)
+  %name All2.All2 ps, qs
+
+export
+0 all2Length : {p : Rel m n} -> All2 p ss ts -> length ss = length ts
+all2Length []        = Refl
+all2Length (p :: ps) = cong S $ all2Length ps
+
+namespace Any
+  public export
+  data Any : Pred n -> OPEList n -> Type where
+    Here  : {0 p : Pred n} -> p ope -> Any p (ope :: opes)
+    There : {0 p : Pred n} -> Any p opes -> Any p (ope :: opes)
+  %name Any.Any p, q
+
+export
+{0 p : Pred n} -> Uninhabited (Any p []) where uninhabited _ impossible
+
+export
+all : {0 p : Pred n} ->
+      (forall m. {mask : Nat} -> (0 ope : OPE m n mask) -> p ope) ->
+      (opes : OPEList n) -> All p opes
+all f []            = []
+all f (ope :: opes) = f ope :: all f opes
+
+export
+allDec : {0 p : Pred n} ->
+         (forall m. {mask : Nat} -> (0 ope : OPE m n mask) -> Dec (p ope)) ->
+         (opes : OPEList n) -> Dec (All p opes)
+allDec f [] = Yes []
+allDec f (ope :: opes) = case f ope of
+  Yes y => case allDec f opes of
+    Yes ys => Yes $ y :: ys
+    No  k  => No  $ \(_ :: ps) => k ps
+  No k => No $ \(p :: _) => k p
+
+export
+anyDec : {0 p : Pred n} ->
+         (forall m. {mask : Nat} -> (0 ope : OPE m n mask) -> Dec (p ope)) ->
+         (opes : OPEList n) -> Dec (Any p opes)
+anyDec f [] = No absurd
+anyDec f (ope :: opes) = case f ope of
+  Yes y  => Yes $ Here y
+  No  nh => case anyDec f opes of
+    Yes y  => Yes $ There y
+    No  nt => No  $ \case Here h => nh h; There t => nt t
+
+
+export
+unconses : {n : Nat} -> (opes : OPEList (S n)) -> All Uncons opes
+unconses = all uncons
+
+export
+heads : {n : Nat} -> (opes : OPEList (S n)) -> All (Exists . IsHead) opes
+heads = all head
+
+export
+tails : {n : Nat} -> (opes : OPEList (S n)) -> All Tail opes
+tails = all tail
+
+export
+tails_ : {n : Nat} -> (opes : OPEList (S n)) ->
+         Subset (OPEList n) (All2 IsTail opes)
+tails_ []            = Element [] []
+tails_ (ope :: opes) = Element _ $ (tail ope).isTail :: (tails_ opes).snd
+
+export
+conses : (heads : List Bool) -> (tails : OPEList n) ->
+         (0 len : length heads = length tails) =>
+         OPEList (S n)
+conses []        []        = []
+conses (h :: hs) (t :: ts) = snd (cons h t) :: conses hs ts @{inj S len}

lib/Quox/Thin/Split.idr

@@ -0,0 +1,57 @@
+module Quox.Thin.Split
+
+import public Quox.Thin.Base
+import public Quox.Thin.View
+import public Quox.Thin.Eqv
+import public Quox.Thin.Append
+import public Quox.Thin.Cover
+import Data.DPair
+import Control.Relation
+
+%default total
+
+public export
+record Chunks m n where
+  constructor MkChunks
+  {leftMask  : Nat}
+  {rightMask : Nat}
+  0 left  : OPE m (m + n) leftMask
+  0 right : OPE n (m + n) rightMask
+  {auto 0 isCover : Cover [left, right]}
+%name Chunks chunks
+
+export
+chunks : (m, n : Nat) -> Chunks m n
+chunks 0 0 = MkChunks Stop Stop
+chunks 0 (S n) =
+  let MkChunks l r = chunks 0 n in
+  MkChunks (Drop l Refl) (Keep r Refl)
+chunks (S m) n =
+  let MkChunks l r = chunks m n in
+  MkChunks (Keep l Refl) (Drop r Refl)
+
+-- [todo] the masks here are just ((2 << m) - 1) << n and (2 << n) - 1
+
+
+public export
+record SplitAt m n1 n2 (ope : OPE m (n1 + n2) mask) where
+  constructor MkSplitAt
+  {leftMask, rightMask : Nat}
+  {0 leftScope, rightScope : Nat}
+  0 left     : OPE leftScope n1 leftMask
+  0 right    : OPE rightScope n2 rightMask
+  0 scopePrf : m = leftScope + rightScope
+  0 opePrf   : ope `Eqv` (left `app'` right).snd
+%name SplitAt split
+
+export
+splitAt : (n1 : Nat) -> {n2, mask : Nat} -> (0 ope : OPE m (n1 + n2) mask) ->
+          SplitAt m n1 n2 ope
+splitAt 0     ope = MkSplitAt zero ope Refl reflexive
+splitAt (S n1) ope with %syntactic (view ope)
+  splitAt (S n1) (Drop ope Refl) | DropV _ ope with %syntactic (splitAt n1 ope)
+    _ | MkSplitAt left right scopePrf opePrf =
+      MkSplitAt (Drop left Refl) right scopePrf (EqvDrop opePrf)
+  splitAt (S n1) (Keep ope Refl) | KeepV _ ope with %syntactic (splitAt n1 ope)
+    _ | MkSplitAt left right scopePrf opePrf =
+      MkSplitAt (Keep left Refl) right (cong S scopePrf) (EqvKeep opePrf)

lib/Quox/Thin/Term.idr

@@ -0,0 +1,216 @@
+module Quox.Thin.Term
+
+import public Quox.Thin.Base
+import public Quox.Thin.Comp
+import public Quox.Thin.List
+import Quox.Thin.Eqv
+import public Quox.Thin.Cover
+import Quox.Thin.Append
+import Quox.Name
+import Quox.Loc
+import Data.DPair
+import public Data.List.Quantifiers
+import Data.Vect
+import Data.Singleton
+import Decidable.Equality
+
+%default total
+
+private
+cmpMask : (m, n : Nat) -> Either Ordering (m = n)
+cmpMask 0     0     = Right Refl
+cmpMask 0     (S n) = Left  LT
+cmpMask (S m) 0     = Left  GT
+cmpMask (S m) (S n) = map (cong S) $ cmpMask m n
+
+public export
+record Thinned f n where
+  constructor Th
+  {0 scope   : Nat}
+  {scopeMask : Nat}
+  0 ope : OPE scope n scopeMask
+  term  : f scope
+%name Thinned s, t, u
+
+export
+(forall n. Eq (f n)) => Eq (Thinned f n) where
+  s == t = case cmpMask s.scopeMask t.scopeMask of
+    Left  _  => False
+    Right eq => s.term == (rewrite maskEqInner s.ope t.ope eq in t.term)
+
+export
+(forall n. Ord (f n)) => Ord (Thinned f n) where
+  compare s t = case cmpMask s.scopeMask t.scopeMask of
+    Left  o  => o
+    Right eq => compare s.term (rewrite maskEqInner s.ope t.ope eq in t.term)
+
+export
+{n : Nat} -> (forall s. Show (f s)) => Show (Thinned f n) where
+  showPrec d (Th ope term) =
+    showCon d "Th" $ showArg (unVal $ maskToOpe ope) ++ showArg term
+
+export
+(forall n. Located (f n)) => Located (Thinned f n) where
+  term.loc = term.term.loc
+
+export
+(forall n. Relocatable (f n)) => Relocatable (Thinned f n) where
+  setLoc loc = {term $= setLoc loc}
+
+namespace Thinned
+  export
+  pure : {n : Nat} -> f n -> Thinned f n
+  pure term = Th id.snd term
+
+  export
+  join : {n : Nat} -> Thinned (Thinned f) n -> Thinned f n
+  join (Th ope1 (Th ope2 term)) = Th (ope1 . ope2) term
+
+  export
+  weak : {n : Nat} -> (by : Nat) -> Thinned f n -> Thinned f (by + n)
+  weak by (Th ope term) = Th (zero ++ ope).snd term
+
+
+public export
+record ScopedN (s : Nat) (f : Nat -> Type) (n : Nat) where
+  constructor S
+  names : Vect s BindName
+  {0 scope : Nat}
+  {mask : Nat}
+  0 ope : OPE scope s mask
+  body : f (scope + n)
+
+export
+(forall n. Eq (f n)) => Eq (ScopedN s f n) where
+  s1 == s2 = case decEq s1.mask s2.mask of
+    Yes eq =>
+      s1.names == s2.names &&
+      s1.body == (rewrite maskEqInner s1.ope s2.ope eq in s2.body)
+    No _ => False
+
+export
+{s : Nat} -> (forall n. Show (f n)) => Show (ScopedN s f n) where
+  showPrec d (S ns ope body) = showCon d "S" $
+    showArg ns ++ showArg (unVal $ maskToOpe ope) ++ showArg body
+
+public export
+Scoped : (Nat -> Type) -> Nat -> Type
+Scoped d n = ScopedN 1 d n
+
+(.name) : Scoped f n -> BindName
+(S {names = [x], _}).name = x
+
+export
+(forall n. Located (f n)) => Located (ScopedN s f n) where
+  s.loc = s.body.loc
+
+export
+(forall n. Relocatable (f n)) => Relocatable (ScopedN s f n) where
+  setLoc loc = {body $= setLoc loc}
+
+
+public export
+record Thinned2 f d n where
+  constructor Th2
+  {0 dscope, tscope : Nat}
+  {dmask, tmask : Nat}
+  0 dope : OPE dscope d dmask
+  0 tope : OPE tscope n tmask
+  term : f dscope tscope
+%name Thinned2 term
+
+export
+(forall d, n. Eq (f d n)) => Eq (Thinned2 f d n) where
+  s == t = case (decEq s.dmask t.dmask, decEq s.tmask t.tmask) of
+    (Yes deq, Yes teq) =>
+      s.term == (rewrite maskEqInner s.dope t.dope deq in
+                 rewrite maskEqInner s.tope t.tope teq in t.term)
+    _ => False
+
+export
+{d, n : Nat} -> (forall sd, sn. Show (f sd sn)) => Show (Thinned2 f d n) where
+  showPrec d (Th2 dope tope term) =
+    showCon d "Th2" $
+      showArg (unVal $ maskToOpe dope) ++
+      showArg (unVal $ maskToOpe tope) ++
+      showArg term
+
+export
+(forall d, n. Located (f d n)) => Located (Thinned2 f d n) where
+  term.loc = term.term.loc
+
+export
+(forall d, n. Relocatable (f d n)) => Relocatable (Thinned2 f d n) where
+  setLoc loc = {term $= setLoc loc}
+
+namespace Thinned2
+  export
+  pure : {d, n : Nat} -> f d n -> Thinned2 f d n
+  pure term = Th2 id.snd id.snd term
+
+  export
+  join : {d, n : Nat} -> Thinned2 (Thinned2 f) d n -> Thinned2 f d n
+  join (Th2 dope1 tope1 (Th2 dope2 tope2 term)) =
+    Th2 (dope1 . dope2) (tope1 . tope2) term
+
+  export
+  weak : {d, n : Nat} -> (dby, nby : Nat) ->
+         Thinned2 f d n -> Thinned2 f (dby + d) (nby + n)
+  weak dby nby (Th2 dope tope term) =
+    Th2 (zero ++ dope).snd (zero ++ tope).snd term
+
+
+namespace TermList
+  public export
+  data Element : (Nat -> Nat -> Type) ->
+                 OPE dscope d dmask -> OPE tscope n tmask -> Type where
+    T : f dscope tscope ->
+        {dmask : Nat} -> (0 dope : OPE dscope d dmask) ->
+        {tmask : Nat} -> (0 tope : OPE tscope n tmask) ->
+        Element f dope tope
+  %name TermList.Element s, t, u
+
+  export
+  elementEq : (forall d, n. Eq (f d n)) =>
+              Element {d, n} f dope1 tope1 -> Element {d, n} f dope2 tope2 ->
+              Bool
+  elementEq (T s dope1 tope1 {dmask = dm1, tmask = tm1})
+            (T t dope2 tope2 {dmask = dm2, tmask = tm2}) =
+    case (decEq dm1 dm2, decEq tm1 tm2) of
+      (Yes deq, Yes teq) =>
+        s == (rewrite maskEqInner dope1 dope2 deq in
+              rewrite maskEqInner tope1 tope2 teq in t)
+      _ => False
+
+  public export
+  data TermList : List (Nat -> Nat -> Type) ->
+                  OPEList d -> OPEList n -> Type where
+    Nil  : TermList [] [] []
+    (::) : Element f dope tope ->
+           TermList fs dopes topes ->
+           TermList (f :: fs) (dope :: dopes) (tope :: topes)
+  %name TermList ss, ts, us
+
+  export
+  termListEq : All (\f => forall d, n. Eq (f d n)) fs =>
+               TermList {d, n} fs dopes1 topes1 ->
+               TermList {d, n} fs dopes2 topes2 ->
+               Bool
+  termListEq [] [] = True
+  termListEq (s :: ss) (t :: ts) @{eq :: eqs} =
+    elementEq s t && termListEq ss ts
+
+
+public export
+record Subterms (fs : List (Nat -> Nat -> Type)) d n where
+  constructor Sub
+  {0 dopes : OPEList d}
+  {0 topes : OPEList n}
+  terms : TermList fs dopes topes
+  0 dcov : Cover dopes
+  0 tcov : Cover topes
+%name Subterms ss, ts, us
+
+export
+All (\f => forall d, n. Eq (f d n)) fs => Eq (Subterms fs d n) where
+  ss == ts = ss.terms `termListEq` ts.terms

lib/Quox/Thin/View.idr

@@ -0,0 +1,100 @@
+module Quox.Thin.View
+
+import public Quox.Thin.Base
+import Quox.NatExtra
+import Data.Singleton
+import Data.SnocVect
+import Data.Fin
+
+%default total
+
+public export
+data View : OPE m n mask -> Type where
+  StopV : View Stop
+  DropV : (mask : Nat) -> (0 ope : OPE m n mask) -> View (Drop ope Refl)
+  KeepV : (mask : Nat) -> (0 ope : OPE m n mask) -> View (Keep ope Refl)
+%name View.View v
+
+private
+0 stopEqs : OPE m 0 mask -> (m = 0, mask = 0)
+stopEqs Stop = (Refl, Refl)
+
+private
+0 fromStop : (ope : OPE 0 0 0) -> ope = Stop
+fromStop Stop = Refl
+
+private
+0 fromDrop : (ope : OPE m (S n) (k + k)) ->
+             (inner : OPE m n k ** ope === Drop inner Refl)
+fromDrop (Drop ope eq) with %syntactic (doubleInj _ _ eq)
+  fromDrop (Drop ope Refl) | Refl = (ope ** Refl)
+fromDrop (Keep ope eq) = void $ notEvenOdd _ _ eq
+
+private
+0 fromKeep : (ope : OPE (S m) (S n) (S (k + k))) ->
+             (inner : OPE m n k ** ope === Keep inner Refl)
+fromKeep (Drop ope eq) = void $ notEvenOdd _ _ $ sym eq
+fromKeep (Keep ope eq) with %syntactic (doubleInj _ _ $ inj S eq)
+  fromKeep (Keep ope Refl) | Refl = (ope ** Refl)
+
+private
+0 keepIsSucc : (ope : OPE m n (S (k + k))) -> IsSucc m
+keepIsSucc (Drop ope eq) = void $ notEvenOdd _ _ $ sym eq
+keepIsSucc (Keep ope _)  = ItIsSucc
+
+export
+view : {0 m : Nat} -> {n, mask : Nat} -> (0 ope : OPE m n mask) -> View ope
+view {n = 0} ope with %syntactic 0 (fst $ stopEqs ope) | 0 (snd $ stopEqs ope)
+  _ | Refl | Refl = rewrite fromStop ope in StopV
+view {n = S n} ope with %syntactic (half mask)
+  _ | HalfOdd mask' with %syntactic 0 (keepIsSucc ope)
+    _ | ItIsSucc with %syntactic 0 (fromKeep ope)
+      _ | (ope' ** eq) = rewrite eq in KeepV mask' ope'
+  _ | HalfEven mask' with %syntactic 0 (fromDrop ope)
+    _ | (ope' ** eq) = rewrite eq in DropV mask' ope'
+
+export
+(.fin) : {n, mask : Nat} -> (0 ope : OPE 1 n mask) -> Fin n
+ope.fin with (view ope)
+  _.fin | DropV _ ope = FS ope.fin
+  _.fin | KeepV _ ope = FZ
+
+
+export
+appOpe : {0 m : Nat} -> (n : Nat) -> {mask : Nat} ->
+         (0 ope : OPE m n mask) -> Singleton m
+appOpe n ope with %syntactic (view ope)
+  appOpe 0     Stop          | StopV        = Val 0
+  appOpe (S n) (Drop ope' _) | DropV _ ope' = appOpe n ope'
+  appOpe (S n) (Keep ope' _) | KeepV _ ope' = [|S $ appOpe n ope'|]
+
+export
+maskToOpe : {n, mask : Nat} -> (0 ope : OPE m n mask) -> Singleton ope
+maskToOpe ope with %syntactic (view ope)
+  maskToOpe Stop            | StopV       = [|Stop|]
+  maskToOpe (Drop ope Refl) | DropV k ope = [|drop $ maskToOpe ope|]
+  maskToOpe (Keep ope Refl) | KeepV k ope = [|keep $ maskToOpe ope|]
+
+export
+0 outerInnerZero : OPE m 0 mask -> m = 0
+outerInnerZero Stop = Refl
+
+export
+0 outerMaskZero : OPE m 0 mask -> mask = 0
+outerMaskZero Stop = Refl
+
+export
+0 viewStop : view Stop = StopV
+viewStop = Refl
+
+export
+0 viewDrop : (ope : OPE m n mask) -> (eq : mask2 = mask + mask) ->
+             view (Drop {mask} ope eq) = DropV mask ope
+viewDrop ope eq with %syntactic (view (Drop ope eq))
+  viewDrop ope Refl | DropV _ ope = Refl
+
+export
+0 viewKeep : (ope : OPE m n mask) -> (eq : mask2 = S (mask + mask)) ->
+             view (Keep {mask} ope eq) = KeepV mask ope
+viewKeep ope eq with %syntactic (view (Keep ope eq))
+  viewKeep ope Refl | KeepV _ ope = Refl

lib/quox-lib.ipkg

@@ -16,8 +16,19 @@ modules =
   Quox.Decidable,
   Quox.No,
   Quox.Loc,
-  Quox.OPE,
   Quox.Pretty,
+  Quox.Thin.Base,
+  Quox.Thin.View,
+  Quox.Thin.Eqv,
+  Quox.Thin.Cons,
+  Quox.Thin.List,
+  Quox.Thin.Append,
+  Quox.Thin.Comp,
+  Quox.Thin.Cover,
+  Quox.Thin.Coprod,
+  Quox.Thin.Split,
+  Quox.Thin.Term,
+  Quox.Thin,
   Quox.Syntax,
   Quox.Syntax.Dim,
   Quox.Syntax.DimEq,

quox.bib

@@ -366,3 +366,16 @@
   url       = {https://www.cs.bham.ac.uk/~pbl/papers/hosc05.pdf},
   doi       = {10.1007/s10990-006-0480-6},
 }
+
+@article{egtbs,
+  doi = {10.4204/eptcs.275.6},
+  url = {https://doi.org/10.4204%2Feptcs.275.6},
+  year = 2018,
+  month = {jul},
+  publisher = {Open Publishing Association},
+  volume = {275},
+  pages = {53--69},
+  author = {Conor McBride},
+  title = {Everybody's Got To Be Somewhere},
+  journal = {Electronic Proceedings in Theoretical Computer Science}
+}