add SnocVect.select

examples/bool.quox

@@ -10,7 +10,6 @@ def boolω : 1.Bool → [ω.Bool] =
 def if : 0.(A : ★) → 1.Bool → ω.A → ω.A → A =
   λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f };
 
--- [todo]: universe lifting
 def0 If : 1.Bool → 0.★ → 0.★ → ★ =
   λ b T F ⇒ case1 b return ★ of { 'true ⇒ T; 'false ⇒ F };
 

lib/Quox/Definition.idr

@@ -74,10 +74,6 @@ public export
 DefsState : Type -> Type
 DefsState = StateL DEFS Definitions
 
-export
-defs : Has DefsReader fs => Eff fs Definitions
-defs = askAt DEFS
-
 
 public export %inline
 lookupElim : {d, n : Nat} -> Name -> Definitions -> Maybe (Elim d n)

lib/Quox/Equal.idr

@@ -347,9 +347,10 @@ parameters (defs : Definitions)
       --    Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
       compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
       compareType (extendDim sTy.name One  ctx) sTy.one  tTy.one
+      let ty = case !mode of Super => sTy; _ => tTy
       local_ Equal $ do
-        Term.compare0 ctx sTy.zero sl tl
-        Term.compare0 ctx sTy.one  sr tr
+        Term.compare0 ctx ty.zero sl tl
+        Term.compare0 ctx ty.one  sr tr
 
     compareType' ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
       -- ------------------
@@ -636,7 +637,7 @@ parameters (loc : Loc) (ctx : TyContext d n)
     private
     runCompare : (Definitions -> EqContext n -> DSubst d 0 -> Equal_ ()) ->
                  Equal ()
-    runCompare act = fromEqual_ $ eachFace $ act !defs
+    runCompare act = fromEqual_ $ eachFace $ act !(askAt DEFS)
 
     namespace Term
       export covering

lib/Quox/NatExtra.idr

@@ -9,6 +9,11 @@ import Syntax.PreorderReasoning
 
 %default total
 
+infixl 8 `shiftL`, `shiftR`
+infixl 7 .&.
+infixl 6 `xor`
+infixl 5 .|.
+
 
 public export
 data LTE' : Nat -> Nat -> Type where
@@ -119,3 +124,86 @@ spread mask subj = go 1 (halfRec mask) subj 0 where
   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
+
+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
+
+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
+
+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
+
+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
+
+
+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
+
+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/Parser/FromParser.idr

@@ -255,7 +255,6 @@ mutual
       t   => let ctx = MkNameContexts (map fromPatVar ds) (map fromPatVar ns) in
              throw $ AnnotationNeeded t.loc ctx t
 
-  -- [todo] use SN if the var is named but still unused
   private
   fromPTermTScope : {s : Nat} -> Context' PatVar d -> Context' PatVar n ->
                     SnocVect s PatVar -> PTerm ->

lib/Quox/Parser/FromParser/Error.idr

@@ -6,6 +6,8 @@ import System.File
 
 import Quox.Pretty
 
+%hide Text.PrettyPrint.Prettyprinter.Doc.infixr.(<++>)
+
 
 public export
 TypeError, LexError, ParseError : Type

lib/Quox/Reduce.idr

@@ -14,7 +14,6 @@ import Control.Eff
 %default total
 
 
--- [fixme] rename this to Whnf and the interface to CanWhnf
 public export
 Whnf : List (Type -> Type)
 Whnf = [NameGen, Except Error]

lib/Quox/Syntax/Term/Base.idr

@@ -133,7 +133,6 @@ data Term where
   ||| dimension closure/suspended substitution
   DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
 
-||| first argument `d` is dimension scope size, second `n` is term scope size
 public export
 data Elim where
   ||| free variable, possibly with a displacement (see @crude, or @mugen for a

lib/Quox/Syntax/Term/Pretty.idr

@@ -58,11 +58,12 @@ pbname (_, x, _) = x
 private
 record SplitPi d n where
   constructor MkSplitPi
+  {0 inner : Nat}
   binds : Telescope (PiBind d) n inner
   cod   : Term d inner
 
 private
-splitPi : Telescope (PiBind d) n inner -> Term d inner -> SplitPi d n
+splitPi : Telescope (PiBind d) n n' -> Term d n' -> SplitPi d n
 splitPi binds (Pi qty arg res _) =
   splitPi (binds :< (qty, res.name, arg)) $
     assert_smaller res $ pushSubsts' res.term
@@ -87,7 +88,7 @@ prettyPiBind1 pi x dnames tnames s = hcat <$> sequence
 private
 prettyPiBinds : {opts : _} ->
                 BContext d -> BContext n ->
-                Telescope (PiBind d) n inner ->
+                Telescope (PiBind d) n n' ->
                 Eff Pretty (SnocList (Doc opts))
 prettyPiBinds _ _ [<] = pure [<]
 prettyPiBinds dnames tnames (binds :< (q, x, t)) =
@@ -103,11 +104,12 @@ SigBind d n = (BindName, Term d n)
 private
 record SplitSig d n where
   constructor MkSplitSig
+  {0 inner : Nat}
   binds : Telescope (SigBind d) n inner
   last  : Term d inner
 
 private
-splitSig : Telescope (SigBind d) n inner -> Term d inner -> SplitSig d n
+splitSig : Telescope (SigBind d) n n' -> Term d n' -> SplitSig d n
 splitSig binds (Sig fst snd _) =
   splitSig (binds :< (snd.name, fst)) $
     assert_smaller snd $ pushSubsts' snd.term
@@ -129,7 +131,7 @@ prettySigBind1 x dnames tnames s = hcat <$> sequence
 private
 prettySigBinds : {opts : _} ->
                  BContext d -> BContext n ->
-                 Telescope (SigBind d) n inner ->
+                 Telescope (SigBind d) n n' ->
                  Eff Pretty (SnocList (Doc opts))
 prettySigBinds _ _ [<] = pure [<]
 prettySigBinds dnames tnames (binds :< (x, t)) =
@@ -163,6 +165,7 @@ NameChunks = SnocList (NameSort, SnocList BindName)
 private
 record SplitLams d n where
   constructor MkSplitLams
+  {0 dinner, ninner : Nat}
   dnames : BTelescope d dinner
   tnames : BTelescope n ninner
   chunks : NameChunks
@@ -178,9 +181,9 @@ where
     if s == s' then xss :< (s', xs :< y)
     else xss :< (s', xs) :< (s, [< y])
 
-  go : BTelescope d dinner -> BTelescope n ninner ->
+  go : BTelescope d d' -> BTelescope n n' ->
        SnocList (NameSort, SnocList BindName) ->
-       Term dinner ninner -> SplitLams d n
+       Term d' n' -> SplitLams d n
   go dnames tnames chunks (Lam b _) =
     go dnames (tnames :< b.name) (push T b.name chunks) $
        assert_smaller b $ pushSubsts' b.term
@@ -235,6 +238,7 @@ prettyDTApps dnames tnames f xs = do
 private
 record CaseArm opts d n where
   constructor MkCaseArm
+  {0 dinner, ninner : Nat}
   pat    : Doc opts
   dbinds : BTelescope d dinner -- 🍴
   tbinds : BTelescope n ninner

lib/Quox/Syntax/Term/Subst.idr

@@ -10,7 +10,7 @@ import Data.SnocVect
 namespace CanDSubst
   public export
   interface CanDSubst (0 tm : TermLike) where
-    (//) : tm dfrom n -> Lazy (DSubst dfrom dto) -> tm dto n
+    (//) : tm d1 n -> Lazy (DSubst d1 d2) -> tm d2 n
 
 ||| does the minimal reasonable work:
 ||| - deletes the closure around an atomic constant like `TYPE`
@@ -25,7 +25,7 @@ CanDSubst Term where
   s                // th       = DCloT $ Sub s th
 
 private
-subDArgs : Elim dfrom n -> DSubst dfrom dto -> Elim dto n
+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
 
@@ -47,16 +47,16 @@ CanDSubst Elim where
 
 namespace DSubst.ScopeTermN
   export %inline
-  (//) : ScopeTermN s dfrom n -> Lazy (DSubst dfrom dto) ->
-         ScopeTermN s dto n
+  (//) : 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 dfrom n -> Lazy (DSubst dfrom dto) ->
-         DScopeTermN s dto n
+         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
 
@@ -83,7 +83,7 @@ CanSubstSelf (Elim d) where
 namespace CanTSubst
   public export
   interface CanTSubst (0 tm : TermLike) where
-    (//) : tm d from -> Lazy (TSubst d from to) -> tm d to
+    (//) : 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`
@@ -103,16 +103,15 @@ CanTSubst Term where
 namespace ScopeTermN
   export %inline
   (//) : {s : Nat} ->
-         ScopeTermN s d from -> Lazy (TSubst d from to) ->
-         ScopeTermN s d to
+         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 from -> Lazy (TSubst d from to) ->
-         DScopeTermN s d to
+         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
 
@@ -125,8 +124,7 @@ export %inline
 
 
 export %inline
-comp : DSubst dfrom dto -> TSubst dfrom from mid -> TSubst dto mid to ->
-       TSubst dto from to
+comp : DSubst d1 d2 -> TSubst d1 n1 mid -> TSubst d2 mid n2 -> TSubst d2 n1 n2
 comp th ps ph = map (// th) ps . ph
 
 
@@ -205,8 +203,8 @@ public export
 CloTest tm = forall d, n. tm d n -> Bool
 
 interface PushSubsts (0 tm : TermLike) (0 isClo : CloTest tm) | tm where
-  pushSubstsWith : DSubst dfrom dto -> TSubst dto from to ->
-                   tm dfrom from -> Subset (tm dto to) (No . isClo)
+  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)
@@ -230,8 +228,7 @@ parameters {0 isClo : CloTest tm} {auto _ : PushSubsts tm isClo}
   pushSubsts s = pushSubstsWith id id s
 
   export %inline
-  pushSubstsWith' : DSubst dfrom dto -> TSubst dto from to ->
-                    tm dfrom from -> tm dto to
+  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
@@ -334,8 +331,7 @@ 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} =
-  -- [fixme] maintain location of existing B VZ
-  let ty' = SY ty.names $ ty.term // (B VZ noLoc ::: shift 2) in
+  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,

lib/Quox/Syntax/Term/Tighten.idr

@@ -8,10 +8,10 @@ import public Quox.OPE
 
 
 export
-Tighten (Shift from) where
+Tighten (Shift f) where
   -- `OPE m n` is a spicy `m ≤ n`,
-  -- and `Shift from n` is a (different) spicy `from ≤ n`
-  -- so the value is `from ≤ m` (as a `Shift`), if that is the case
+  -- and `Shift f n` is a (different) spicy `f ≤ n`
+  -- so the value is `f ≤ m` (as a `Shift`), if that is the case
   tighten _        SZ      = Nothing
   tighten Id       by      = Just by
   tighten (Drop p) (SS by) = tighten p by
@@ -26,12 +26,12 @@ Tighten Dim where
 
 export
 tightenSub : (forall m, n. OPE m n -> env n -> Maybe (env m)) ->
-             OPE to1 to2 -> Subst env from to2 -> Maybe (Subst env from to1)
+             OPE t1 t2 -> Subst env f t2 -> Maybe (Subst env f t1)
 tightenSub f p (Shift by) = [|Shift $ tighten p by|]
 tightenSub f p (t ::: th) = [|f p t !::: tightenSub f p th|]
 
 export
-Tighten env => Tighten (Subst env from) where
+Tighten env => Tighten (Subst env f) where
   tighten p th = tightenSub tighten p th
 
 

lib/Quox/Thin/Base.idr

@@ -76,5 +76,6 @@ one' i = (one i).snd
 public export
 record SomeOPE n where
   constructor MkOPE
+  {0 scope : Nat}
   {mask : Nat}
-  0 ope : OPE m n mask
+  0 ope : OPE scope n mask

lib/Quox/Thin/Coprod.idr

@@ -6,36 +6,166 @@ 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
 
-public export
-record Coprod2 (ope1 : OPE m1 n mask1) (ope2 : OPE m2 n mask2) where
-  constructor MkCoprod2
-  {sizeMask  : Nat}
-  {leftMask  : Nat}
-  {rightMask : Nat}
-  {0 sub     : OPE size n sizeMask}
-  {0 left    : OPE m1 size leftMask}
-  {0 right   : OPE m2 size rightMask}
-  0 leftComp  : Comp sub left  ope1
-  0 rightComp : Comp sub right ope2
-  {auto 0 isCover : Cover [left, right]}
-%name Coprod2 cop
+
+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
-coprod2 : {n, mask1, mask2 : Nat} ->
-          (0 ope1 : OPE m1 n mask1) -> (0 ope2 : OPE m2 n mask2) ->
-          Coprod2 ope1 ope2
-coprod2 ope1 ope2 with (view ope1) | (view ope2)
-  coprod2 Stop Stop | StopV | StopV = MkCoprod2 StopZ StopZ
-  coprod2 (Drop ope1 Refl) (Drop ope2 Refl) | DropV _ ope1 | DropV _ ope2 =
-    let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (DropZ l) (DropZ r)
-  coprod2 (Drop ope1 Refl) (Keep ope2 Refl) | DropV _ ope1 | KeepV _ ope2 =
-    let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (KDZ l) (KeepZ r)
-  coprod2 (Keep ope1 Refl) (Drop ope2 Refl) | KeepV _ ope1 | DropV _ ope2 =
-    let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (KeepZ l) (KDZ r)
-  coprod2 (Keep ope1 Refl) (Keep ope2 Refl) | KeepV _ ope1 | KeepV _ ope2 =
-    let MkCoprod2 l r = coprod2 ope1 ope2 in MkCoprod2 (KeepZ l) (KeepZ r)
+0 compsLength : Comps s ts us -> length ts = length us
+compsLength []           = Refl
+compsLength (_ :: comps) = cong S $ compsLength comps
 
--- [todo] n-ary coprod
+
+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

@@ -24,3 +24,4 @@ data Cover1 where
   Here  : Cover1 (Keep ope eq :: opes)
   There : Cover1 opes -> Cover1 (ope :: opes)
 %name Cover1 cov1
+%builtin Natural Cover1

lib/Quox/Thin/List.idr

@@ -16,17 +16,17 @@ data OPEList : Nat -> Type where
   (::) : {mask : Nat} -> (0 ope : OPE m n mask) -> OPEList n -> OPEList n
 %name OPEList opes
 
-export
+public export
 length : OPEList n -> Nat
 length []          = 0
 length (_ :: opes) = S $ length opes
 
-export
+public export
 toList : OPEList n -> List (SomeOPE n)
 toList []            = []
 toList (ope :: opes) = MkOPE ope :: toList opes
 
-export
+public export
 fromList : List (SomeOPE n) -> OPEList n
 fromList []                = []
 fromList (MkOPE ope :: xs) = ope :: fromList xs
@@ -56,6 +56,11 @@ namespace All2
            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
@@ -108,7 +113,6 @@ export
 tails : {n : Nat} -> (opes : OPEList (S n)) -> All Tail opes
 tails = all tail
 
--- [fixme] factor this out probably
 export
 tails_ : {n : Nat} -> (opes : OPEList (S n)) ->
          Subset (OPEList n) (All2 IsTail opes)

lib/Quox/Thin/View.idr

@@ -3,6 +3,7 @@ module Quox.Thin.View
 import public Quox.Thin.Base
 import Quox.NatExtra
 import Data.Singleton
+import Data.SnocVect
 
 %default total
 
@@ -74,3 +75,29 @@ 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 (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 (view (Keep ope eq))
+  viewKeep ope Refl | KeepV _ ope = Refl
+
+
+namespace SnocVect
+  export
+  select : {n, mask : Nat} -> (0 ope : OPE m n mask) ->
+           SnocVect n a -> SnocVect m a
+  select ope sx with (view ope)
+    select _ [<]       | StopV       = [<]
+    select _ (sx :< x) | DropV _ ope = select ope sx
+    select _ (sx :< x) | KeepV _ ope = select ope sx :< x

lib/Quox/Typechecker.idr

@@ -163,7 +163,7 @@ mutual
                 (subj : Term d n) -> (0 nc : NotClo subj) => Term d n ->
                 TC (CheckResult' n)
   toCheckType ctx sg t ty = do
-    u <- expectTYPE !defs ctx ty.loc ty
+    u <- expectTYPE !(askAt DEFS) ctx ty.loc ty
     expectEqualQ t.loc Zero sg.fst
     checkTypeNoWrap ctx t (Just u)
     pure $ zeroFor ctx
@@ -178,7 +178,7 @@ mutual
   check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Lam body loc) ty = do
-    (qty, arg, res) <- expectPi !defs ctx ty.loc ty
+    (qty, arg, res) <- expectPi !(askAt DEFS) ctx ty.loc ty
     -- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
     -- with ρ ≤ σπ
     let qty' = sg.fst * qty
@@ -189,7 +189,7 @@ mutual
   check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Pair fst snd loc) ty = do
-    (tfst, tsnd) <- expectSig !defs ctx ty.loc ty
+    (tfst, tsnd) <- expectSig !(askAt DEFS) ctx ty.loc ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
     qfst <- checkC ctx sg fst tfst
     let tsnd = sub1 tsnd (Ann fst tfst fst.loc)
@@ -201,7 +201,7 @@ mutual
   check' ctx sg t@(Enum {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Tag t loc) ty = do
-    tags <- expectEnum !defs ctx ty.loc ty
+    tags <- expectEnum !(askAt DEFS) ctx ty.loc ty
     -- if t ∈ ts
     unless (t `elem` tags) $ throw $ TagNotIn loc t tags
     -- then Ψ | Γ ⊢ σ · t ⇐ {ts} ⊳ 𝟎
@@ -210,7 +210,7 @@ mutual
   check' ctx sg t@(Eq {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (DLam body loc) ty = do
-    (ty, l, r) <- expectEq !defs ctx ty.loc ty
+    (ty, l, r) <- expectEq !(askAt DEFS) ctx ty.loc ty
     let ctx' = extendDim body.name ctx
         ty   = ty.term
         body = body.term
@@ -226,17 +226,17 @@ mutual
   check' ctx sg t@(Nat {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Zero {}) ty = do
-    expectNat !defs ctx ty.loc ty
+    expectNat !(askAt DEFS) ctx ty.loc ty
     pure $ zeroFor ctx
 
   check' ctx sg (Succ n {}) ty = do
-    expectNat !defs ctx ty.loc ty
+    expectNat !(askAt DEFS) ctx ty.loc ty
     checkC ctx sg n ty
 
   check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
 
   check' ctx sg (Box val loc) ty = do
-    (q, ty) <- expectBOX !defs ctx ty.loc ty
+    (q, ty) <- expectBOX !(askAt DEFS) ctx ty.loc ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
     valout <- checkC ctx sg val ty
     -- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
@@ -314,7 +314,7 @@ mutual
     -- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
     case u of
       Just u  => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
-      Nothing => ignore $ expectTYPE !defs ctx e.loc infres.type
+      Nothing => ignore $ expectTYPE !(askAt DEFS) ctx e.loc infres.type
     -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
 
 
@@ -333,7 +333,7 @@ mutual
 
   infer' ctx sg (F x u loc) = do
     -- if π·x : A {≔ s} in global context
-    g <- lookupFree x loc !defs
+    g <- lookupFree x loc !(askAt DEFS)
     -- if σ ≤ π
     expectCompatQ loc sg.fst g.qty.fst
     -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
@@ -355,7 +355,7 @@ mutual
   infer' ctx sg (App fun arg loc) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
     funres <- inferC ctx sg fun
-    (qty, argty, res) <- expectPi !defs ctx fun.loc funres.type
+    (qty, argty, res) <- expectPi !(askAt DEFS) ctx fun.loc funres.type
     -- if Ψ | Γ ⊢ σ ⨴ π · s ⇐ A ⊳ Σ₂
     argout <- checkC ctx (subjMult sg qty) arg argty
     -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + πΣ₂
@@ -372,7 +372,7 @@ mutual
     pairres <- inferC ctx sg pair
     -- if Ψ | Γ, p : (x : A) × B ⊢₀ ret ⇐ Type
     checkTypeC (extendTy Zero ret.name pairres.type ctx) ret.term Nothing
-    (tfst, tsnd) <- expectSig !defs ctx pair.loc pairres.type
+    (tfst, tsnd) <- expectSig !(askAt DEFS) ctx pair.loc pairres.type
     -- if Ψ | Γ, x : A, y : B ⊢ σ · body ⇐
     --    ret[(x, y) ∷ (x : A) × B/p] ⊳ Σ₂, ρ₁·x, ρ₂·y
     -- with ρ₁, ρ₂ ≤ πσ
@@ -391,7 +391,7 @@ mutual
   infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
     -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
     tres <- inferC ctx sg t
-    ttags <- expectEnum !defs ctx t.loc tres.type
+    ttags <- expectEnum !(askAt DEFS) ctx t.loc tres.type
     -- if 1 ≤ π, OR there is only zero or one option
     unless (length (SortedSet.toList ttags) <= 1) $ expectCompatQ loc One pi
     -- if Ψ | Γ, x : {ts} ⊢₀ A ⇐ Type
@@ -415,7 +415,7 @@ mutual
     -- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
     nres <- inferC ctx sg n
     let nat = nres.type
-    expectNat !defs ctx n.loc nat
+    expectNat !(askAt DEFS) ctx n.loc nat
     -- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
     checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
     -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
@@ -439,7 +439,7 @@ mutual
   infer' ctx sg (CaseBox pi box ret body loc) = do
     -- if Ψ | Γ ⊢ σ · b ⇒ [ρ.A] ⊳ Σ₁
     boxres <- inferC ctx sg box
-    (q, ty) <- expectBOX !defs ctx box.loc boxres.type
+    (q, ty) <- expectBOX !(askAt DEFS) ctx box.loc boxres.type
     -- if Ψ | Γ, x : [ρ.A] ⊢₀ R ⇐ Type
     checkTypeC (extendTy Zero ret.name boxres.type ctx) ret.term Nothing
     -- if Ψ | Γ, x : A ⊢ t ⇐ R[[x] ∷ [ρ.A/x]] ⊳ Σ₂, ς·x
@@ -457,7 +457,7 @@ mutual
   infer' ctx sg (DApp fun dim loc) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- inferC ctx sg fun
-    ty <- fst <$> expectEq !defs ctx fun.loc type
+    ty <- fst <$> expectEq !(askAt DEFS) ctx fun.loc type
     -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
@@ -485,7 +485,7 @@ mutual
     -- if σ = 0
     expectEqualQ loc Zero sg.fst
     -- if Ψ, Γ ⊢₀ e ⇒ Type u
-    u <- expectTYPE !defs ctx ty.loc . type =<< inferC ctx szero ty
+    u <- expectTYPE !(askAt DEFS) ctx ty.loc . type =<< inferC ctx szero ty
     -- if Ψ, Γ ⊢₀ C ⇐ Type (non-dependent return type)
     checkTypeC ctx ret Nothing
     -- if Ψ, Γ' ⊢₀ A ⇐ C for each rhs A

lib/Quox/Typing/Context.idr

@@ -69,7 +69,7 @@ namespace TContext
   zeroFor ctx = Zero <$ ctx
 
 private
-extendLen : Telescope a from to -> Singleton from -> Singleton to
+extendLen : Telescope a n1 n2 -> Singleton n1 -> Singleton n2
 extendLen [<]        x = x
 extendLen (tel :< _) x = [|S $ extendLen tel x|]
 
@@ -89,7 +89,7 @@ namespace TyContext
   null ctx = null ctx.dnames && null ctx.tnames
 
   export %inline
-  extendTyN : CtxExtension d from to -> TyContext d from -> TyContext d to
+  extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
   extendTyN xss (MkTyContext {termLen, dctx, dnames, tctx, tnames, qtys}) =
     let (qs, xs, ss) = unzip3 xss in
     MkTyContext {
@@ -172,7 +172,7 @@ namespace EqContext
   null ctx = null ctx.dnames && null ctx.tnames
 
   export %inline
-  extendTyN : CtxExtension 0 from to -> EqContext from -> EqContext to
+  extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
   extendTyN xss (MkEqContext {termLen, dassign, dnames, tctx, tnames, qtys}) =
     let (qs, xs, ss) = unzip3 xss in
     MkEqContext {

pack.toml

@@ -1,4 +1,4 @@
-collection = "nightly-230522"
+collection = "nightly-230622"
 
 [custom.all.tap]
 type = "git"

tests/Tests/Typechecker.idr

@@ -34,7 +34,7 @@ ToInfo Error' where
 M = Eff [Except Error', DefsReader]
 
 inj : TC a -> M a
-inj act = rethrow $ mapFst TCError $ runTC !defs act
+inj act = rethrow $ mapFst TCError $ runTC !(askAt DEFS) act
 
 
 reflTy : Term d n