add W to internal language

lib/Quox/Displace.idr

@@ -19,6 +19,9 @@ parameters (k : Universe)
     doDisplace (Lam body loc) = Lam (doDisplaceS body) loc
     doDisplace (Sig fst snd loc) = Sig (doDisplace fst) (doDisplaceS snd) loc
     doDisplace (Pair fst snd loc) = Pair (doDisplace fst) (doDisplace snd) loc
+    doDisplace (W shape body loc) =
+      W (doDisplace shape) (doDisplaceS body) loc
+    doDisplace (Sup root sub loc) = Sup (doDisplace root) (doDisplace sub) loc
     doDisplace (Enum cases loc) = Enum cases loc
     doDisplace (Tag tag loc) = Tag tag loc
     doDisplace (Eq ty l r loc) =
@@ -47,6 +50,8 @@ parameters (k : Universe)
     doDisplace (App fun arg loc) = App (doDisplace fun) (doDisplace arg) loc
     doDisplace (CasePair qty pair ret body loc) =
       CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc
+    doDisplace (CaseW qty qtyIH tree ret body loc) =
+      CaseW qty qtyIH (doDisplace tree) (doDisplaceS ret) (doDisplaceS body) loc
     doDisplace (CaseEnum qty tag ret arms loc) =
       CaseEnum qty (doDisplace tag) (doDisplaceS ret) (map doDisplace arms) loc
     doDisplace (CaseNat qty qtyIH nat ret zero succ loc) =

lib/Quox/EffExtra.idr

@@ -26,6 +26,26 @@ local_ : Has (State s) fs => s -> Eff fs a -> Eff fs a
 local_ = localAt_ ()
 
 
+public export
+record StateRes s a where
+  constructor SR
+  state  : s
+  result : a
+
+export
+stateAt : (0 lbl : tag) -> Has (StateL lbl s) fs =>
+          (s -> StateRes s a) -> Eff fs a
+stateAt lbl f = do
+  s <- getAt lbl
+  let out = f s
+  putAt lbl out.state
+  pure out.result
+
+export %inline
+state : Has (State s) fs => (s -> StateRes s a) -> Eff fs a
+state = stateAt ()
+
+
 export
 hasDrop : (0 neq : Not (a = b)) ->
           (ha : Has a fs) => (hb : Has b fs) =>

lib/Quox/Equal.idr

@@ -79,6 +79,8 @@ sameTyCon (Pi   {}) (Pi   {}) = True
 sameTyCon (Pi   {}) _         = False
 sameTyCon (Sig  {}) (Sig  {}) = True
 sameTyCon (Sig  {}) _         = False
+sameTyCon (W    {}) (W    {}) = True
+sameTyCon (W    {}) _         = False
 sameTyCon (Enum {}) (Enum {}) = True
 sameTyCon (Enum {}) _         = False
 sameTyCon (Eq   {}) (Eq   {}) = True
@@ -111,6 +113,7 @@ isSubSing defs ctx ty0 = do
     Sig {fst, snd, _} =>
       isSubSing defs ctx fst `andM`
       isSubSing defs (extendTy Zero snd.name fst ctx) snd.term
+    W {} => pure False
     Enum {cases, _} =>
       pure $ length (SortedSet.toList cases) <= 1
     Eq {} => pure True
@@ -120,6 +123,7 @@ isSubSing defs ctx ty0 = do
     E _ => pure False
     Lam  {} => pure False
     Pair {} => pure False
+    Sup  {} => pure False
     Tag  {} => pure False
     DLam {} => pure False
     Zero {} => pure False
@@ -209,9 +213,9 @@ parameters (defs : Definitions)
         case (s, t) of
           --  Γ ⊢ s₁ = t₁ : A     Γ ⊢ s₂ = t₂ : B{s₁/x}
           -- --------------------------------------------
-          --     Γ ⊢ (s₁, t₁) = (s₂,t₂) : (x : A) × B
+          --    Γ ⊢ (s₁, t₁) = (s₂, t₂) : (x : A) × B
           --
-          -- [todo] η for π ≥ 0 maybe
+          -- [todo] η for π ≰ 1 maybe
           (Pair sFst sSnd {}, Pair tFst tSnd {}) => do
             compare0 ctx fst sFst tFst
             compare0 ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
@@ -225,6 +229,27 @@ parameters (defs : Definitions)
           (E _,     t) => wrongType t.loc ctx ty t
           (s,       _) => wrongType s.loc ctx ty s
 
+      compare0' ctx ty@(W {shape, body, _}) s t =
+        case (s, t) of
+          --           Γ ⊢ s₁ = t₁ : A
+          --  Γ ⊢ s₂ = t₂ : 1.B[s₁∷A/x] → (x : A) ⊲ B
+          -- -----------------------------------------
+          --     Γ ⊢ s₁⋄s₂ = t₁⋄t₂ : (x : A) ⊲ B
+          (Sup sRoot sSub {}, Sup tRoot tSub {}) => do
+            compare0 ctx shape sRoot tRoot
+            let arg   = sub1 body (Ann sRoot shape sRoot.loc)
+                subTy = Arr One arg ty ty.loc
+            compare0 ctx subTy sSub tSub
+
+          (E e, E f) => Elim.compare0 ctx e f
+
+          (Sup {}, E   {}) => clashT s.loc ctx ty s t
+          (E   {}, Sup {}) => clashT s.loc ctx ty s t
+
+          (Sup {}, t) => wrongType t.loc ctx ty t
+          (E   {}, t) => wrongType t.loc ctx ty t
+          (s,      _) => wrongType s.loc ctx ty s
+
       compare0' ctx ty@(Enum {}) s t = local_ Equal $
         case (s, t) of
           -- --------------------
@@ -322,12 +347,16 @@ parameters (defs : Definitions)
       --  Γ ⊢ Type 𝓀 <: Type ℓ
       expectModeU a.loc !mode k l
 
-    compareType' ctx a@(Pi {qty = sQty, arg = sArg, res = sRes, _})
+    compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc})
                      (Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
       --   Γ ⊢ A₁ :> A₂    Γ, x : A₁ ⊢ B₁ <: B₂
       -- ----------------------------------------
-      --  Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
+      --  Γ ⊢ π.(x : A₁) → B₁ <: π.(x : A₂) → B₂
-      expectEqualQ a.loc sQty tQty
+      --
+      -- no quantity subtyping since that would need a runtime coercion
+      -- e.g. if ⌊0.A → B⌋ ⇝ ⌊B⌋, then the promotion to ω.A → B would need
+      -- to re-add the abstraction
+      expectEqualQ loc sQty tQty
       local flip $ compareType ctx sArg tArg -- contra
       compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term
 
@@ -339,12 +368,20 @@ parameters (defs : Definitions)
       compareType ctx sFst tFst
       compareType (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term
 
+    compareType' ctx (W {shape = sShape, body = sBody, loc})
+                     (W {shape = tShape, body = tBody, _}) = do
+      --  Γ ⊢ A₁ <: A₂    Γ, x : A₁ ⊢ B₁ <: B₂
+      -- --------------------------------------
+      --   Γ ⊢ (x : A₁) ⊲ B₁ <: (x : A₂) ⊲ B₂
+      compareType ctx sShape tShape
+      compareType (extendTy Zero sBody.name sShape ctx) sBody.term tBody.term
+
     compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
                      (Eq {ty = tTy, l = tl, r = tr, _}) = do
       --            Γ ⊢ A₁‹ε/i› <: A₂‹ε/i›
-      --  Γ ⊢ l₁ = l₂ : A₁‹𝟎/i›    Γ ⊢ r₁ = r₂ : A₁‹𝟏/i›
+      --  Γ ⊢ l₁ = l₂ : A₁‹0/i›    Γ ⊢ r₁ = r₂ : A₁‹1/i›
       -- ------------------------------------------------
-      --    Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
+      --    Γ ⊢ 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
@@ -366,6 +403,9 @@ parameters (defs : Definitions)
       pure ()
 
     compareType' ctx (BOX pi a loc) (BOX rh b {}) = do
+      --     Γ ⊢ A <: B
+      -- --------------------
+      --  Γ ⊢ [π.A] <: [π.B]
       expectEqualQ loc pi rh
       compareType ctx a b
 
@@ -439,6 +479,36 @@ parameters (defs : Definitions)
           expectEqualQ e.loc epi fpi
       compare0' ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f
 
+      --  Ψ | Γ ⊢ e = f ⇒ (x : A) ⊲ B
+      --  Ψ | Γ, p : (x : A) ⊲ B ⊢ Q = R ⇐ Type
+      --  Ψ | Γ, x : A, y : 1.B → (x : A) ⊲ B, ih : 1.(z : B) → Q[y z/p]
+      --    ⊢ s = t ⇐ Q[(x⋄y ∷ (x : A) ⊲ B)/p]
+      -- ----------------------------------------------------------------
+      --  Ψ | Γ ⊢ caseπ e return Q of { x ⋄ y, ς.ih ⇒ s }
+      --        = caseπ f return R of { x ⋄ y, ς.ih ⇒ t } ⇒ Q[e/p]
+      compare0' ctx (CaseW epi epi' e eret ebody eloc)
+                    (CaseW fpi fpi' f fret fbody floc) ne nf =
+        local_ Equal $ do
+          compare0 ctx e f
+          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
+          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
+          (shape, tbody) <- expectW defs ctx eloc ety
+          let [< x, y, ih] = ebody.names
+          z <- mnb "z" ih.loc
+          let xbind = (epi, x, shape)
+              ybind = (epi, y, Arr One tbody.term (weakT 1 ety) y.loc)
+              ihbind = (epi', ih,
+                PiY One z
+                  (sub1 (weakS 2 tbody) (BV 1 x.loc))
+                  (sub1 (weakS 3 eret) (App (BV 1 y.loc) (BVT 0 z.loc) ih.loc))
+                  ih.loc)
+              ctx' = extendTyN [< xbind, ybind, ihbind] ctx
+          Term.compare0 ctx' (substCaseWRet ebody.names ety eret)
+            ebody.term fbody.term
+          expectEqualQ e.loc epi  fpi
+          expectEqualQ e.loc epi' fpi'
+      compare0' ctx e@(CaseW {}) f _ _ = clashE e.loc ctx e f
+
       --  Ψ | Γ ⊢ e = f ⇒ {𝐚s}
       --  Ψ | Γ, x : {𝐚s} ⊢ Q = R
       --  Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}]
@@ -598,6 +668,13 @@ parameters (defs : Definitions)
                  (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
         compare0 ctx (weakT 2 ret) b1.term b2.term
 
+      compareArm_ ctx KW ret u b1 b2 = do
+        let [< a, b] = b1.names
+            ctx = extendTyN
+              [< (Zero, a, TYPE u a.loc),
+                 (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
+        compare0 ctx (weakT 2 ret) b1.term b2.term
+
       compareArm_ ctx KEnum ret u b1 b2 =
         compare0 ctx ret b1.term b2.term
 

lib/Quox/Name.idr

@@ -4,7 +4,7 @@ import Quox.Loc
 import Quox.CharExtra
 import public Data.SnocList
 import Data.List
-import Control.Eff
+import Quox.EffExtra
 import Text.Lexer
 import Derive.Prelude
 
@@ -178,23 +178,22 @@ export
 runNameGen : Has NameGen fs => Eff fs a -> Eff (fs - NameGen) a
 runNameGen = map fst . runNameGenWith 0
 
+export
+gen : Has NameGen fs => Eff fs Nat
+gen = stateAt GEN $ \i => SR {result = i, state = S i}
+
 ||| generate a fresh name with the given base
 export
 mn : Has NameGen fs => PBaseName -> Eff fs BaseName
-mn base = do
+mn base = MN base <$> gen
-  i <- getAt GEN
-  modifyAt GEN S
-  pure $ MN base i
 
-||| generate a fresh binding name with the given base and
+||| generate a fresh binding name with the given base and location `loc`
-||| (optionally) location `loc`
 export
-mnb : Has NameGen fs =>
+mnb : Has NameGen fs => PBaseName -> Loc -> Eff fs BindName
-      PBaseName -> {default noLoc loc : Loc} -> Eff fs BindName
+mnb base loc = pure $ BN !(mn base) loc
-mnb base = pure $ BN !(mn base) loc
 
 export
 fresh : Has NameGen fs => BindName -> Eff fs BindName
-fresh (BN (UN str)   loc) = mnb str {loc}
+fresh (BN (UN str)   loc) = mnb str loc
-fresh (BN (MN str k) loc) = mnb str {loc}
+fresh (BN (MN str k) loc) = mnb str loc
-fresh (BN Unused     loc) = mnb "x" {loc}
+fresh (BN Unused     loc) = mnb "x" loc

lib/Quox/Pretty.idr

@@ -24,9 +24,13 @@ data PPrec
 = Outer
 | Times   -- "_ × _"
 | InTimes -- arguments of ×
+| W       -- "_ ⊲ _"
+| InW     -- arguments of ⊲
 | AnnL    -- left of "∷"
 | Eq      -- "_ ≡ _ : _"
 | InEq    -- arguments of ≡
+| Sup     -- "_ ⋄ _"
+| InSup   -- arguments of ⋄
   -- ...
 | App  -- term/dimension application
 | Arg  -- argument to nonfix function
@@ -229,10 +233,10 @@ prettyDBind = hl DVar . prettyBind'
 
 
 export %inline
-typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
+typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD, triD, diamondD,
-eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
+eqD, colonD, commaD, semiD, caseD, typecaseD, returnD, ofD, dotD, zeroD, succD,
-ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD :
+coeD, compD, undD, cstD, pipeD :
-  {opts : _} -> Eff Pretty (Doc opts)
+  {opts : LayoutOpts} -> Eff Pretty (Doc opts)
 typeD     = hl Syntax . text =<< ifUnicode "★" "Type"
 arrowD    = hl Delim  . text =<< ifUnicode "→" "->"
 darrowD   = hl Delim  . text =<< ifUnicode "⇒" "=>"
@@ -242,6 +246,8 @@ eqndD     = hl Delim  . text =<< ifUnicode "≡" "=="
 dlamD     = hl Syntax . text =<< ifUnicode "δ" "dfun"
 annD      = hl Delim  . text =<< ifUnicode "∷" "::"
 natD      = hl Syntax . text =<< ifUnicode "ℕ" "Nat"
+triD      = hl Syntax . text =<< ifUnicode "⊲" "<|"
+diamondD  = hl Syntax . text =<< ifUnicode "⋄" "<>"
 eqD       = hl Syntax $ text "Eq"
 colonD    = hl Delim  $ text ":"
 commaD    = hl Delim  $ text ","

lib/Quox/Reduce.idr

@@ -78,6 +78,12 @@ isPairHead (Ann (Pair {}) (Sig {}) _) = True
 isPairHead (Coe {})                   = True
 isPairHead _                          = False
 
+public export %inline
+isWHead : Elim {} -> Bool
+isWHead (Ann (Sup {}) (W {}) _) = True
+isWHead (Coe {})                = True
+isWHead _                       = False
+
 public export %inline
 isTagHead : Elim {} -> Bool
 isTagHead (Ann (Tag {}) (Enum {}) _) = True
@@ -113,6 +119,8 @@ isTyCon : Term {} -> Bool
 isTyCon (TYPE  {}) = True
 isTyCon (Pi    {}) = True
 isTyCon (Lam   {}) = False
+isTyCon (W     {}) = True
+isTyCon (Sup   {}) = False
 isTyCon (Sig   {}) = True
 isTyCon (Pair  {}) = False
 isTyCon (Enum  {}) = True
@@ -155,6 +163,8 @@ mutual
     isRedexE defs fun || isLamHead fun
   isRedexE defs (CasePair {pair, _}) =
     isRedexE defs pair || isPairHead pair
+  isRedexE defs (CaseW {tree, _}) =
+    isRedexE defs tree || isWHead tree
   isRedexE defs (CaseEnum {tag, _}) =
     isRedexE defs tag || isTagHead tag
   isRedexE defs (CaseNat {nat, _}) =
@@ -204,16 +214,36 @@ tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
 tycaseRhsDef0 def k arms = fromMaybe def $ tycaseRhs0 k arms
 
 
+export
+weakAtT : CanTSubst f => (by, at : Nat) ->
+          f d (at + n) -> f d (at + (by + n))
+weakAtT by at t = t `CanTSubst.(//)` pushN at (shift by)
 
-private
+export
-weakDS : (by : Nat) -> DScopeTerm d n -> DScopeTerm d (by + n)
+weakAtD : CanDSubst f => (by, at : Nat) ->
-weakDS by (S names (Y body)) = S names $ Y $ weakT by body
+          f (at + d) n -> f (at + (by + d)) n
-weakDS by (S names (N body)) = S names $ N $ weakT by body
+weakAtD by at t = t `CanDSubst.(//)` pushN at (shift by)
 
-private
+parameters {s : Nat}
-dweakS : (by : Nat) -> ScopeTerm d n -> ScopeTerm (by + d) n
+  export
-dweakS by (S names (Y body)) = S names $ Y $ dweakT by body
+  weakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s d (by + n)
-dweakS by (S names (N body)) = S names $ N $ dweakT by body
+  weakS by (S names (Y body)) = S names $ Y $ weakAtT by s body
+  weakS by (S names (N body)) = S names $ N $ weakT by body
+
+  export
+  weakDS : (by : Nat) -> DScopeTermN s d n -> DScopeTermN s d (by + n)
+  weakDS by (S names (Y body)) = S names $ Y $ weakT by body
+  weakDS by (S names (N body)) = S names $ N $ weakT by body
+
+  export
+  dweakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s (by + d) n
+  dweakS by (S names (Y body)) = S names $ Y $ dweakT by body
+  dweakS by (S names (N body)) = S names $ N $ dweakT by body
+
+  export
+  dweakDS : (by : Nat) -> DScopeTermN s d n -> DScopeTermN s (by + d) n
+  dweakDS by (S names (Y body)) = S names $ Y $ weakAtD by s body
+  dweakDS by (S names (N body)) = S names $ N $ dweakT by body
 
 private
 coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d -> Loc ->
@@ -246,6 +276,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
       | t => throw $ ExpectedPi loc ctx.names t
     pure $ sub1 res $ Ann s arg loc
   computeElimType (CasePair {pair, ret, _}) = pure $ sub1 ret pair
+  computeElimType (CaseW {tree, ret, _}) = pure $ sub1 ret tree
   computeElimType (CaseEnum {tag, ret, _}) = pure $ sub1 ret tag
   computeElimType (CaseNat {nat, ret, _}) = pure $ sub1 ret nat
   computeElimType (CaseBox {box, ret, _}) = pure $ sub1 ret box
@@ -269,7 +300,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   tycasePi (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
     let loc  = e.loc
-        narg = mnb "Arg"; nret = mnb "Ret"
+        narg = mnb "Arg" loc; nret = mnb "Ret" loc
         arg  = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc
         res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret]
                  (BVT 0 loc) loc
@@ -287,7 +318,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   tycaseSig (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
     let loc  = e.loc
-        nfst = mnb "Fst"; nsnd = mnb "Snd"
+        nfst = mnb "Fst" loc; nsnd = mnb "Snd" loc
         fst  = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc
         snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd]
                  (BVT 0 loc) loc
@@ -295,6 +326,24 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
     pure (fst, snd)
   tycaseSig t = throw $ ExpectedSig t.loc ctx.names t
 
+  ||| for (x : A) ⊲ B, returns (A, B);
+  ||| for an elim returns a pair of type-cases that will reduce to that;
+  ||| for other intro forms error
+  private covering
+  tycaseW : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
+            Eff Whnf (Term (S d) n, ScopeTerm (S d) n)
+  tycaseW (W {shape, body, _}) = pure (shape, body)
+  tycaseW (E e) {tnf} = do
+    ty <- computeElimType defs ctx e @{noOr2 tnf}
+    let loc    = e.loc
+        nshape = mnb "Shape" loc; nbody = mnb "Body" loc
+        shape  = E $ typeCase1Y e ty KW [< !nshape, !nbody] (BVT 1 loc) loc
+        body'  = typeCase1Y e (Arr Zero shape ty loc) KW [< !nshape, !nbody]
+                   (BVT 0 loc) loc
+        body   = ST [< !nshape] $ E $ App (weakE 1 body') (BVT 0 loc) loc
+    pure (shape, body)
+  tycaseW t = throw $ ExpectedW t.loc ctx.names t
+
   ||| for [π. A], returns A;
   ||| for an elim returns a type-case that will reduce to that;
   ||| for other intro forms error
@@ -303,8 +352,9 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
               Eff Whnf (Term (S d) n)
   tycaseBOX (BOX {ty, _}) = pure ty
   tycaseBOX (E e) {tnf} = do
+    let loc = e.loc
     ty <- computeElimType defs ctx e @{noOr2 tnf}
-    pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty")] (BVT 0 e.loc) e.loc
+    pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty" loc)] (BVT 0 loc) loc
   tycaseBOX t = throw $ ExpectedBOX t.loc ctx.names t
 
   ||| for Eq [i ⇒ A] l r, returns (A‹0/i›, A‹1/i›, A, l, r);
@@ -318,11 +368,11 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   tycaseEq (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
     let loc   = e.loc
-        names = traverse' (\x => mnb x) [< "A0", "A1", "A", "L", "R"]
+        names = traverse' (\x => mnb x loc) [< "A0", "A1", "A", "l", "r"]
         a0    = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc
         a1    = E $ typeCase1Y e ty KEq !names (BVT 3 loc) loc
         a'    = typeCase1Y e (Eq0 ty a0 a1 loc) KEq !names (BVT 2 loc) loc
-        a     = DST [< !(mnb "i")] $ E $ DApp (dweakE 1 a') (B VZ loc) loc
+        a     = DST [< !(mnb "i" loc)] $ E $ DApp (dweakE 1 a') (B VZ loc) loc
         l     = E $ typeCase1Y e a0 KEq !names (BVT 1 loc) loc
         r     = E $ typeCase1Y e a1 KEq !names (BVT 0 loc) loc
     pure (a0, a1, a, l, r)
@@ -337,9 +387,12 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
           (val, s : Term d n) -> Loc ->
           Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
   piCoe sty@(S [< i] ty) p q val s loc = do
-    -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
+    --  𝒮‹𝑘› ≔ π.(x : A‹𝑘/𝑖›) → B‹𝑘/𝑖›
-    -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
+    --  𝓈‹𝑘› ≔ coe [𝑖 ⇒ A] @q @𝑘 s
-    --   where 𝒔‹j› ≔ coe [i ⇒ A] @q @j s
+    -- -------------------------------------------------------
+    --  (coe [𝑖 ⇒ 𝒮‹𝑖›] @p @q t) s
+    --    ⇝
+    --  coe [i ⇒ B[𝓈‹i›/x] @p @q ((t ∷ 𝒮‹p›) 𝓈‹p›)
     --
     -- type-case is used to expose A,B if the type is neutral
     let ctx1 = extendDim i ctx
@@ -358,11 +411,11 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
            (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
            Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
   sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
-    -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
+    -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ u }
     -- ⇝
     -- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C
     -- of { (a, b) ⇒
-    --   e[(coe [i ⇒ A] @p @q a)/a,
+    --   u[(coe [i ⇒ A] @p @q a)/a,
     --     (coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i a)/x]] @p @q b)/b] }
     --
     -- type-case is used to expose A,B if the type is neutral
@@ -370,14 +423,58 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
     Element ty tynf <- whnf defs ctx1 ty.term
     (tfst, tsnd) <- tycaseSig defs ctx1 ty
     let [< x, y] = body.names
-        a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc
+        a' = CoeT i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc
         tsnd' = tsnd.term //
-          (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
+          (CoeT !(fresh i) (weakT 2 $ tfst // (B VZ i.loc ::: shift 2))
-            (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2)
+            (weakD 1 p) (B VZ i.loc) (BVT 1 x.loc) y.loc ::: shift 2)
-        b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc
+        b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc
-    whnf defs ctx $ CasePair qty (Ann val (ty // one p) val.loc) ret
+    whnf defs ctx $ CasePair qty (Ann val (dsub1 sty p) val.loc) ret
       (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
 
+  ||| reduce a w elimination `CaseW pi piIH (Coe ty p q val) ret body loc`
+  private covering
+  wCoe : (qty, qtyIH : Qty) ->
+         (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
+         (ret : ScopeTerm d n) -> (body : ScopeTermN 3 d n) -> Loc ->
+         Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
+  wCoe qty qtyIH sty@(S [< i] ty) p q val ret body loc = do
+    --  𝒮‹𝑘› ≔ ((x : A) ⊲ B)‹𝑘/𝑖›
+    --  𝒶‹𝑘› ≔ coe [𝑖 ⇒ A] @p @𝑘 a
+    --       : A‹𝑘/𝑖›
+    --  𝒷‹𝑘› ≔ coe [𝑖 ⇒ 1.B[𝒶‹𝑖›/x] → 𝒮‹𝑖›] @p @𝑘 b
+    --       : 1.B‹𝑘/𝑖›[𝒶‹𝑘›/x] → 𝒮‹𝑘›
+    --  𝒾𝒽   ≔ coe [𝑖 ⇒ π.(z : B[𝒶‹𝑖›/x]) → C[𝒷‹𝑖› z/p]] @p @q ih
+    --       : π.(z : B‹q/𝑖›[𝒶‹q›/x]) → C[𝒷‹q› z/p]
+    -- --------------------------------------------------------------------
+    --  caseπ (coe [𝑖 ⇒ 𝒮‹𝑖›] @p @q s) return z ⇒ C of { a ⋄ b, ς.ih ⇒ u }
+    --    ⇝
+    --  caseπ s ∷ 𝒮‹p› return z ⇒ C
+    --  of { a ⋄ b, ς.ih ⇒ u[𝒶‹q›/a, 𝒷‹q›/b, 𝒾𝒽/ih] }
+    let ctx1 = extendDim i ctx
+    Element ty tynf <- whnf defs ctx1 ty.term
+    (shape, tbody) <- tycaseW defs ctx1 ty
+    let [< a, b, ih] = body.names
+    ai <- fresh i; bi <- fresh i; ihi <- fresh i; z <- mnb "z" ih.loc
+    let a', b' : forall d'. (by : Shift d d') => Dim d' -> Elim d' (3 + n)
+        a' k =
+          let shape' = shape // Shift (weak 1 by) // shift 3 in
+          CoeT ai shape' (p // by) k (BVT 2 a.loc) a.loc
+        b' k =
+          let tbody' = tbody.term // Shift (weak 1 by)
+                                  // (a' (BV 0 bi.loc) ::: shift 3)
+              ty' = ty // Shift (weak 1 by) // shift 3
+          in
+          CoeT bi (Arr One tbody' ty' b.loc) (p // by) k (BVT 1 b.loc) b.loc
+        ih' : Elim d (3 + n) :=
+          let tbody' = tbody.term // (a' (BV 0 ihi.loc) ::: shift 3)
+              ret' = sub1 (weakS 4 $ dweakS 1 ret) $
+                     App (weakE 1 $ b' (BV 0 ihi.loc)) (BVT 0 z.loc) ih.loc
+              ty = PiY qty z tbody' ret' ih.loc
+          in
+          CoeT ihi ty p q (BVT 0 ih.loc) ih.loc
+    whnf defs ctx $ CaseW qty qtyIH (Ann val (dsub1 sty p) val.loc) ret
+      (ST body.names $ body.term // (a' q ::: b' q ::: ih' ::: shift 3)) loc
+
   ||| reduce a dimension application `DApp (Coe ty p q val) r loc`
   private covering
   eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
@@ -392,7 +489,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
     Element ty tynf <- whnf defs ctx1 ty.term
     (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
     let a'   = dsub1 a (weakD 1 r)
-        val' = E $ DApp (Ann val (ty // one p) val.loc) r loc
+        val' = E $ DApp (Ann val (dsub1 sty p) val.loc) r loc
     whnf defs ctx $ CompH j a' p q val' r j s j t loc
 
   ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
@@ -409,8 +506,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
     let ctx1 = extendDim i ctx
     Element ty tynf <- whnf defs ctx1 ty.term
     ta <- tycaseBOX defs ctx1 ty
-    let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
+    let a' = CoeT i (weakT 1 ta) p q (BVT 0 body.name.loc) body.name.loc
-    whnf defs ctx $ CaseBox qty (Ann val (ty // one p) val.loc) ret
+    whnf defs ctx $ CaseBox qty (Ann val (dsub1 sty p) val.loc) ret
       (ST body.names $ body.term // (a' ::: shift 1)) loc
 
 
@@ -429,19 +526,29 @@ reduceTypeCase defs ctx ty u ret arms def loc = case ty of
   -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
   -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
   Pi {arg, res, loc = piLoc, _} =>
-    let arg' = Ann arg (TYPE u noLoc) arg.loc
+    let arg' = Ann arg (TYPE u arg.loc) arg.loc
         res' = Ann (Lam res res.loc)
-                   (Arr Zero arg (TYPE u noLoc) arg.loc) res.loc
+                   (Arr Zero arg (TYPE u arg.loc) arg.loc) res.loc
     in
     whnf defs ctx $
       Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc
 
+  -- (type-case (x : A) ⊲ π.B ∷ ★ᵢ return Q of { (a ⊲ b) ⇒ s; ⋯ }) ⇝
+  -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
+  W {shape, body, loc = wLoc, _} =>
+    let shape' = Ann shape (TYPE u shape.loc) shape.loc
+        body'  = Ann (Lam body body.loc)
+                     (Arr Zero shape (TYPE u shape.loc) shape.loc) body.loc
+    in
+    whnf defs ctx $
+      Ann (subN (tycaseRhsDef def KW arms) [< shape', body']) ret loc
+
   -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
   -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
   Sig {fst, snd, loc = sigLoc, _} =>
-    let fst' = Ann fst (TYPE u noLoc) fst.loc
+    let fst' = Ann fst (TYPE u fst.loc) fst.loc
         snd' = Ann (Lam snd snd.loc)
-                   (Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc
+                   (Arr Zero fst (TYPE u fst.loc) fst.loc) snd.loc
     in
     whnf defs ctx $
       Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc
@@ -459,8 +566,8 @@ reduceTypeCase defs ctx ty u ret arms def loc = case ty of
     let a0 = a.zero; a1 = a.one in
     whnf defs ctx $ Ann
       (subN (tycaseRhsDef def KEq arms)
-         [< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc,
+         [< Ann a0 (TYPE u a.loc) a.loc, Ann a1 (TYPE u a.loc) a.loc,
-            Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc,
+            Ann (DLam a a.loc) (Eq0 (TYPE u a.loc) a0 a1 a.loc) a.loc,
             Ann l a0 l.loc, Ann r a1 r.loc])
       ret loc
 
@@ -471,7 +578,7 @@ reduceTypeCase defs ctx ty u ret arms def loc = case ty of
   -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
   BOX {ty = a, loc = boxLoc, _} =>
     whnf defs ctx $ Ann
-      (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc))
+      (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u a.loc) a.loc))
       ret loc
 
 
@@ -489,6 +596,7 @@ pushCoe defs ctx i ty p q s loc =
     -- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ)
     TYPE {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
     Pi   {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
+    W    {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
     Sig  {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
     Enum {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
     Eq   {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
@@ -503,7 +611,7 @@ pushCoe defs ctx i ty p q s loc =
     lam@(Lam {body, _}) => do
       let lam'  = CoeT i ty p q lam loc
           term' = LamY !(fresh body.name)
-                    (E $ App (weakE 1 lam') (BVT 0 noLoc) loc) loc
+                    (E $ App (weakE 1 lam') (BVT 0 loc) loc) loc
           type' = ty // one q
       whnf defs ctx $ Ann term' type' loc
 
@@ -517,23 +625,40 @@ pushCoe defs ctx i ty p q s loc =
       let Sig {fst = tfst, snd = tsnd, loc = sigLoc} = ty
         | _ => throw $ ExpectedSig ty.loc (extendDim i ctx.names) ty
       let fst'  = E $ CoeT i tfst p q fst fst.loc
-          tfst' = tfst // (B VZ noLoc ::: shift 2)
+          tfst' = tfst // (B VZ i.loc ::: shift 2)
           tsnd' = sub1 tsnd $
-                  CoeT !(fresh i) tfst' (weakD 1 p) (B VZ noLoc)
+                  CoeT !(fresh i) tfst' (weakD 1 p) (B VZ snd.loc)
-                    (dweakT 1 fst) fst.loc
+                    (dweakT 1 fst) snd.loc
           snd'  = E $ CoeT i tsnd' p q snd snd.loc
       pure $
         Element (Ann (Pair fst' snd' pairLoc)
                      (Sig (tfst // one q) (tsnd // one q) sigLoc) loc) Ah
 
+    -- (coe [i ⇒ (x : A) ⊲ π.B] @p @q (s ⋄ t) ⇝
+    -- (coe [i ⇒ A] @p @q s ⋄
+    --  coe [i ⇒ 1.B[coe [j ⇒ A‹j/i›] @p @i s/x] → (x : A) ⊲ B] t)
+    --   ∷ ((x : A) ⊲ B)‹q/i›
+    Sup {root, sub, loc = supLoc} => do
+      let W {shape, body, loc = wLoc} = ty
+        | _ => throw $ ExpectedW ty.loc (extendDim i ctx.names) ty
+      let root' = E $ CoeT i shape p q root root.loc
+          tsub' = sub1 body $
+                  CoeT !(fresh i) (shape // (B VZ root.loc ::: shift 2))
+                    (weakD 1 p) (BV 0 sub.loc)
+                    (dweakT 1 sub) sub.loc
+          sub' = E $ CoeT i tsub' p q sub sub.loc
+      pure $
+        Element (Ann (Sup root' sub' supLoc)
+                     (W (shape // one q) (body // one q) wLoc) loc) Ah
+
     -- η expand, like for Lam
     --
     -- (coe [i ⇒ A] @p @q (δ j ⇒ s)) ⇝
     -- (δ k ⇒ (coe [i ⇒ A] @p @q (δ j ⇒ s)) @k) ∷ A‹q/i› ⇝ ⋯
     dlam@(DLam {body, _}) => do
       let dlam' = CoeT i ty p q dlam loc
-          term' = DLamY !(mnb "j")
+          term' = DLamY !(mnb "j" loc)
-                    (E $ DApp (dweakE 1 dlam') (B VZ noLoc) loc) loc
+                    (E $ DApp (dweakE 1 dlam') (B VZ loc) loc) loc
           type' = ty // one q
       whnf defs ctx $ Ann term' type' loc
 
@@ -585,8 +710,12 @@ CanWhnf Elim Reduce.isRedexE where
         Coe ty p q val _ => piCoe defs ctx ty p q val s appLoc
       Right nlh => pure $ Element (App f s appLoc) $ fnf `orNo` nlh
 
-  -- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
+  --  s'  ≔ s ∷ A
-  -- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
+  --  t'  ≔ t ∷ B[s'/x]
+  --  st' ≔ (s, t) ∷ (x : A) × B
+  --  C'  ≔ C[st'/p]
+  -- ---------------------------------------------------------------
+  --  case st' return p ⇒ C of { (a, b) ⇒ u } ⇝ u[s'/a, t'/x]] ∷ C'
   whnf defs ctx (CasePair pi pair ret body caseLoc) = do
     Element pair pairnf <- whnf defs ctx pair
     case nchoose $ isPairHead pair of
@@ -601,6 +730,43 @@ CanWhnf Elim Reduce.isRedexE where
       Right np =>
         pure $ Element (CasePair pi pair ret body caseLoc) $ pairnf `orNo` np
 
+  --  s'  ≔ s ∷ A
+  --  t'  ≔ t ∷ 1.B[s'/x] → (x : A) ⊲ B
+  --  ih' ≔ (λ x ⇒ caseπ t x return p ⇒ C of { (a ⋄ b), ς.ih ⇒ u }) ∷
+  --          π.(y : B[s'/x]) → C[t' y/p]
+  --  st' ≔ s ⋄ t ∷ (x : A) ⊲ B
+  --  C'  ≔ C[st'/p]
+  -- --------------------------------------------------------------------
+  --  caseπ st' return p ⇒ C of { a ⋄ b, ς.ih ⇒ u }
+  --   ⇝
+  --  u[s'/a, t'/b, ih'/ih] ∷ C'
+  whnf defs ctx (CaseW qty qtyIH tree ret body caseLoc) = do
+    Element tree treenf <- whnf defs ctx tree
+    case nchoose $ isWHead tree of
+      Left _ => case tree of
+        Ann (Sup {root, sub, _})
+            w@(W {shape, body = wbody, _}) treeLoc =>
+          let root = Ann root shape root.loc
+              wbody' = sub1 wbody root
+              tsub = Arr One wbody' w sub.loc
+              sub = Ann sub tsub sub.loc
+              ih' = LamY !(mnb "y" caseLoc) -- [todo] better name
+                    (E $ CaseW qty qtyIH
+                           (App (weakE 1 sub) (BVT 0 sub.loc) sub.loc)
+                           (weakS 1 ret) (weakS 1 body) caseLoc) sub.loc
+              ihret = sub1 (weakS 1 ret)
+                           (App (weakE 1 sub) (BVT 0 sub.loc) caseLoc)
+              tih = PiY qty !(mnb "y" caseLoc)
+                      wbody' ihret caseLoc
+              ih = Ann ih' tih caseLoc
+          in
+          whnf defs ctx $
+          Ann (subN body [< root, sub, ih]) (sub1 ret tree) tree.loc
+        Coe ty p q val _ => do
+          wCoe defs ctx qty qtyIH ty p q val ret body caseLoc
+      Right nw => pure $
+        Element (CaseW qty qtyIH tree ret body caseLoc) $ treenf `orNo` nw
+
   -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
   -- u ∷ C['a∷{a,…}/p]
   whnf defs ctx (CaseEnum pi tag ret arms caseLoc) = do
@@ -730,6 +896,8 @@ CanWhnf Term Reduce.isRedexT where
   whnf _ _ t@(Lam  {}) = pure $ nred t
   whnf _ _ t@(Sig  {}) = pure $ nred t
   whnf _ _ t@(Pair {}) = pure $ nred t
+  whnf _ _ t@(W    {}) = pure $ nred t
+  whnf _ _ t@(Sup  {}) = pure $ nred t
   whnf _ _ t@(Enum {}) = pure $ nred t
   whnf _ _ t@(Tag  {}) = pure $ nred t
   whnf _ _ t@(Eq   {}) = pure $ nred t

lib/Quox/Syntax/Term/Base.idr

@@ -102,6 +102,16 @@ mutual
     ||| pair value
     Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
 
+    ||| inductive (w) type `(x : A) ⊲ B`
+    W : (shape : Term d n) ->
+        (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
+    ||| subterms for `(x : A) ⊲ B` are:
+    |||   1. `x : A`
+    |||      (the "constructor" and non-recursive fields)
+    |||   2. `f : 1.(B x) → (x : A) ⊲ B`
+    |||      (the recursive fields, one for each element of B x)
+    Sup : (root, sub : Term d n) -> (loc : Loc) -> Term d n
+
     ||| enumeration type
     Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n
     ||| enumeration value
@@ -155,6 +165,13 @@ mutual
                (loc : Loc) ->
                Elim d n
 
+    ||| recursion
+    CaseW : (qty, qtyIH : Qty) -> (tree : Elim d n) ->
+            (ret : ScopeTerm d n) ->
+            (body : ScopeTermN 3 d n) ->
+            (loc : Loc) ->
+            Elim d n
+
     ||| enum matching
     CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
                (ret : ScopeTerm d n) ->
@@ -364,6 +381,7 @@ Located (Elim d n) where
   (B _ loc).loc                 = loc
   (App _ _ loc).loc             = loc
   (CasePair _ _ _ _ loc).loc    = loc
+  (CaseW _ _ _ _ _ loc).loc     = loc
   (CaseEnum _ _ _ _ loc).loc    = loc
   (CaseNat _ _ _ _ _ _ loc).loc = loc
   (CaseBox _ _ _ _ loc).loc     = loc
@@ -382,6 +400,8 @@ Located (Term d n) where
   (Lam _ loc).loc       = loc
   (Sig _ _ loc).loc     = loc
   (Pair _ _ loc).loc    = loc
+  (W _ _ loc).loc       = loc
+  (Sup _ _ loc).loc     = loc
   (Enum _ loc).loc      = loc
   (Tag _ loc).loc       = loc
   (Eq _ _ _ loc).loc    = loc
@@ -412,6 +432,8 @@ Relocatable (Elim d n) where
   setLoc loc (App fun arg _) = App fun arg loc
   setLoc loc (CasePair qty pair ret body _) =
     CasePair qty pair ret body loc
+  setLoc loc (CaseW qty qtyIH tree ret body _) =
+    CaseW qty qtyIH tree 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 _) =
@@ -440,6 +462,8 @@ Relocatable (Term d n) where
   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 (W shape body _) = W shape body loc
+  setLoc loc (Sup root sub _) = Sup root sub 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

lib/Quox/Syntax/Term/Pretty.idr

@@ -346,6 +346,8 @@ prettyTyCasePat KPi [< a, b] =
   parens . hsep =<< sequence [prettyTBind a, arrowD, prettyTBind b]
 prettyTyCasePat KSig [< a, b] =
   parens . hsep =<< sequence [prettyTBind a, timesD, prettyTBind b]
+prettyTyCasePat KW [< a, b] =
+  parens . hsep =<< sequence [prettyTBind a, triD, prettyTBind b]
 prettyTyCasePat KEnum [<] = hl Syntax $ text "{}"
 prettyTyCasePat KEq [< a0, a1, a, l, r] =
   hsep <$> sequence (eqD :: map prettyTBind [a0, a1, a, l, r])
@@ -420,6 +422,21 @@ prettyTerm dnames tnames p@(Pair fst snd _) =
       withPrec Outer $ prettyTerm dnames tnames $ assert_smaller p t
     pure $ separateTight !commaD lines
 
+prettyTerm dnames tnames (W a b _) = do
+  parensIfM W =<< do
+    left <- prettySigBind1 b.name dnames tnames a
+    right <- withPrec InW $
+             prettyTerm dnames (tnames :< b.name) (assert_smaller b b.term)
+    pure $ sep [hsep [left, !triD], right]
+
+prettyTerm dnames tnames (Sup root sub _) = do
+  parensIfM Sup =<< do
+    left  <- withPrec InSup $ prettyTerm dnames tnames root
+    right <- withPrec InSup $ prettyTerm dnames tnames sub
+    pure $
+      hsep [left, !diamondD, right] <|>
+      vsep [hsep [left, !diamondD], !(indentD right)]
+
 prettyTerm dnames tnames (Enum cases _) =
   prettyEnum $ SortedSet.toList cases
 
@@ -446,17 +463,22 @@ prettyTerm dnames tnames s@(DLam {}) =
 prettyTerm dnames tnames (Nat _) = natD
 prettyTerm dnames tnames (Zero _) = hl Syntax "0"
 prettyTerm dnames tnames (Succ p _) = do
-  succD <- succD
+  s <- succD
-  let succ : Doc opts -> Eff Pretty (Doc opts)
+  either (succ s) prettyNat =<< tryToNat s p
-      succ t = prettyAppD succD [t]
+where
-      toNat : Term d n -> Eff Pretty (Either (Doc opts) Nat)
+  succ : Doc opts -> Doc opts -> Eff Pretty (Doc opts)
-      toNat s with (pushSubsts' s)
+  succ s t = prettyAppD s [t]
+
+  tryToNat : Doc opts -> Term d n -> Eff Pretty (Either (Doc opts) Nat)
+  tryToNat s t with (pushSubsts' t)
     _ | Zero _   = pure $ Right 0
-        _ | Succ d _ = bitraverse succ (pure . S) =<<
+    _ | Succ d _ = bitraverse (succ s) (pure . S) =<<
-                       toNat (assert_smaller s d)
+                   tryToNat s (assert_smaller t d)
-        _ | s'       = map Left . withPrec Arg $
+    _ | t'       = map Left . withPrec Arg $
-                       prettyTerm dnames tnames $ assert_smaller s s'
+                   prettyTerm dnames tnames $ assert_smaller t t'
-  either succ (hl Syntax . text . show . S) =<< toNat p
+
+  prettyNat : Nat -> Eff Pretty (Doc opts)
+  prettyNat = hl Syntax . text . show . S
 
 prettyTerm dnames tnames (BOX qty ty _) =
   bracks . hcat =<<
@@ -493,6 +515,16 @@ prettyElim dnames tnames (CasePair qty pair ret body _) = do
   prettyCase dnames tnames qty pair ret
     [MkCaseArm pat [<] [< x, y] body.term]
 
+prettyElim dnames tnames (CaseW qty qtyIH tree ret body _) = do
+  let [< t, r, ih] = body.names
+  pat0 <- hsep <$> sequence [prettyTBind t, diamondD, prettyTBind r]
+  ihpat <- map hcat $ sequence [prettyQty qtyIH, dotD, prettyTBind ih]
+  pat <- if ih.name == Unused
+         then pure pat0
+         else pure $ hsep [pat0 <+> !commaD, ihpat]
+  let arm = MkCaseArm pat [<] [< t, r, ih] body.term
+  prettyCase dnames tnames qty tree ret [arm]
+
 prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do
   arms <- for (SortedMap.toList arms) $ \(tag, body) =>
     pure $ MkCaseArm !(prettyTag tag) [<] [<] body

lib/Quox/Syntax/Term/Subst.idr

@@ -261,6 +261,10 @@ mutual
       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 (W a b loc) =
+      nclo $ W (a // th // ph) (b // th // ph) loc
+    pushSubstsWith th ph (Sup s t loc) =
+      nclo $ Sup (s // th // ph) (t // th // ph) loc
     pushSubstsWith th ph (Enum tags loc) =
       nclo $ Enum tags loc
     pushSubstsWith th ph (Tag tag loc) =
@@ -299,6 +303,8 @@ mutual
       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 (CaseW pi pi' e r b loc) =
+      nclo $ CaseW pi pi' (e // 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

lib/Quox/Syntax/Term/Tighten.idr

@@ -52,6 +52,10 @@ mutual
     Sig <$> tightenT p fst <*> tightenS p snd <*> pure loc
   tightenT' p (Pair fst snd loc) =
     Pair <$> tightenT p fst <*> tightenT p snd <*> pure loc
+  tightenT' p (W shape body loc) =
+    W <$> tightenT p shape <*> tightenS p body <*> pure loc
+  tightenT' p (Sup root sub loc) =
+    Sup <$> tightenT p root <*> tightenT p sub <*> pure loc
   tightenT' p (Enum cases loc) =
     pure $ Enum cases loc
   tightenT' p (Tag tag loc) =
@@ -87,6 +91,12 @@ mutual
                  <*> tightenS p ret
                  <*> tightenS p body
                  <*> pure loc
+  tightenE' p (CaseW qty qtyIH tree ret body loc) =
+    CaseW qty qtyIH
+      <$> tightenE p tree
+      <*> tightenS p ret
+      <*> tightenS p body
+      <*> pure loc
   tightenE' p (CaseEnum qty tag ret arms loc) =
     CaseEnum qty <$> tightenE p tag
                  <*> tightenS p ret
@@ -167,6 +177,10 @@ mutual
     Sig <$> dtightenT p fst <*> dtightenS p snd <*> pure loc
   dtightenT' p (Pair fst snd loc) =
     Pair <$> dtightenT p fst <*> dtightenT p snd <*> pure loc
+  dtightenT' p (W shape body loc) =
+    W <$> dtightenT p shape <*> dtightenS p body <*> pure loc
+  dtightenT' p (Sup root sub loc) =
+    Sup <$> dtightenT p root <*> dtightenT p sub <*> pure loc
   dtightenT' p (Enum cases loc) =
     pure $ Enum cases loc
   dtightenT' p (Tag tag loc) =
@@ -202,6 +216,12 @@ mutual
                  <*> dtightenS p ret
                  <*> dtightenS p body
                  <*> pure loc
+  dtightenE' p (CaseW qty qtyIH tree ret body loc) =
+    CaseW qty qtyIH
+      <$> dtightenE p tree
+      <*> dtightenS p ret
+      <*> dtightenS p body
+      <*> pure loc
   dtightenE' p (CaseEnum qty tag ret arms loc) =
     CaseEnum qty <$> dtightenE p tag
                  <*> dtightenS p ret

lib/Quox/Syntax/Term/TyConKind.idr

@@ -9,7 +9,7 @@ import Generics.Derive
 
 
 public export
-data TyConKind = KTYPE | KPi | KSig | KEnum | KEq | KNat | KBOX
+data TyConKind = KTYPE | KPi | KSig | KW | KEnum | KEq | KNat | KBOX
 %name TyConKind k
 %runElab derive "TyConKind" [Eq.Eq, Ord.Ord, Show.Show, Generic, Meta, DecEq]
 
@@ -28,6 +28,7 @@ arity : TyConKind -> Nat
 arity KTYPE = 0
 arity KPi   = 2
 arity KSig  = 2
+arity KW    = 2
 arity KEnum = 0
 arity KEq   = 5
 arity KNat  = 0

lib/Quox/Typechecker.idr

@@ -57,27 +57,40 @@ typecaseTel : (k : TyConKind) -> BContext (arity k) -> Universe ->
               CtxExtension d n (arity k + n)
 typecaseTel k xs u = case k of
   KTYPE => [<]
-  -- A : ★ᵤ, B : 0.A → ★ᵤ
+  KPi   => binaryTyCon xs
-  KPi =>
+  KSig  => binaryTyCon xs
-    let [< a, b] = xs in
+  KW    => binaryTyCon xs
-    [< (Zero, a, TYPE u a.loc),
-       (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
-  KSig =>
-    let [< a, b] = xs in
-    [< (Zero, a, TYPE u a.loc),
-       (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
   KEnum => [<]
-  -- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
+  KEq   => eqCon xs
-  KEq =>
+  KNat  => [<]
-    let [< a0, a1, a, l, r] = xs in
+  KBOX  => unaryTyCon xs
+where
+  -- 0.A : ★ᵤ
+  unaryTyCon : BContext 1 -> CtxExtension d n (S n)
+  unaryTyCon [< a] = [< (Zero, a, TYPE u a.loc)]
+
+  -- 0.A : ★ᵤ, 0.B : 0.A → ★ᵤ
+  binaryTyCon : BContext 2 -> CtxExtension d n (2 + n)
+  binaryTyCon [< a, b] =
+    [< (Zero, a, TYPE u a.loc),
+       (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
+
+  -- 0.A₀ : ★ᵤ, 0.A₁ : ★ᵤ, 0.A : (A₀ ≡ A₁ : ★ᵤ), 0.L : A₀, 0.R : A₁
+  eqCon : BContext 5 -> CtxExtension d n (5 + n)
+  eqCon [< a0, a1, a, l, r] =
     [< (Zero, a0, TYPE u a0.loc),
        (Zero, a1, TYPE u a1.loc),
        (Zero, a,  Eq0 (TYPE u a.loc) (BVT 1 a.loc) (BVT 0 a.loc) a.loc),
        (Zero, l,  BVT 2 l.loc),
        (Zero, r,  BVT 2 r.loc)]
-  KNat => [<]
+
-  -- A : ★ᵤ
+||| if a ⋄ b : (x : A) ⊲ B, then b : `supSubTy a A B _`
-  KBOX => let [< a] = xs in [< (Zero, a, TYPE u a.loc)]
+||| i.e. 1.B[a∷A/x] → ((x : A) ⊲ B)
+export
+supSubTy : (root, rootTy : Term d n) ->
+           (body : ScopeTerm d n) -> Loc -> Term d n
+supSubTy root rootTy body loc =
+  Arr One (sub1 body (Ann root rootTy root.loc)) (W rootTy body loc) loc
 
 
 mutual
@@ -188,6 +201,17 @@ mutual
 
   check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
 
+  check' ctx sg t@(W {}) ty = toCheckType ctx sg t ty
+
+  check' ctx sg (Sup root sub loc) ty = do
+    (shape, body) <- expectW !(askAt DEFS) ctx ty.loc ty
+    -- if Ψ | Γ ⊢ σ · a ⇐ A ⊳ Σ₁
+    qroot <- checkC ctx sg root shape
+    -- if Ψ | Γ ⊢ σ · b ⇐ 1.B[a∷A/x] → ((x : A) ⊲ B) ⊳ Σ₂
+    qsub <- checkC ctx sg sub (supSubTy root shape body sub.loc)
+    -- then Ψ | Γ ⊢ σ · (a ⋄ b) ⇐ ((x : A) ⊲ B) ⊳ Σ₁+Σ₂
+    pure $ qroot + qsub
+
   check' ctx sg (Pair fst snd loc) ty = do
     (tfst, tsnd) <- expectSig !(askAt DEFS) ctx ty.loc ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
@@ -281,6 +305,16 @@ mutual
   checkType' ctx t@(Pair {}) u =
     throw $ NotType t.loc ctx t
 
+  checkType' ctx (W shape body _) u = do
+    -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
+    checkTypeC ctx shape u
+    -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
+    checkTypeScope ctx shape body u
+    -- then Ψ | Γ ⊢₀ (x : A) ⊲ π.B ⇐ Type ℓ
+
+  checkType' ctx t@(Sup {}) u =
+    throw $ NotType t.loc ctx t
+
   checkType' ctx (Enum {}) u = pure ()
     -- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
 
@@ -388,6 +422,42 @@ mutual
       qout = pi * pairres.qout + bodyout
     }
 
+  infer' ctx sg (CaseW pi si tree ret body loc) = do
+    -- if 1 ≤ π
+    expectCompatQ loc One pi
+    -- if Ψ | Γ ⊢ σ · e ⇒ ((x : A) ⊲ B) ⊳ Σ₁
+    InfRes {type = w, qout = qtree} <- inferC ctx sg tree
+    -- if Ψ | Γ, p : (x : A) ⊲ B ⊢₀ C ⇐ Type
+    checkTypeC (extendTy Zero ret.name w ctx) ret.term Nothing
+    (shape, tbody) <- expectW !(askAt DEFS) ctx tree.loc w
+    -- if Ψ | Γ, x : A, y : 1.B → (x : A) ⊲ B,
+    --           ih : π.(z : B) → C[y z/p]
+    --  ⊢ σ · u ⇐ C[((x ⋄ y) ∷ (x : A) ⊲ B)/p]
+    --  ⊳ Σ₂, π'.x, ς₁.y, ς₂.ih
+    -- with π' ≤ σπ,  ς₂ ≤ σς,  ς₁+ς₂ ≤ σπ
+    let [< x, y, ih] = body.names
+        -- 1.B → (x : A) ⊲ B
+        tsub = Arr One tbody.term (weakT 1 w) y.loc
+        -- y z
+        ihret = App (BV 1 y.loc) (BVT 0 ih.loc) y.loc
+        -- π.(z : B) → C[y z/p]
+        tih  = PiY pi !(mnb "z" ih.loc)
+                   (tbody.term // (BV 1 x.loc ::: shift 2))
+                   (ret.term // (ihret ::: shift 3)) ih.loc
+        sp = sg.fst * pi; ss = sg.fst * si
+        ctx' = extendTyN [< (sp, x, shape), (sp, y, tsub), (ss, ih, tih)] ctx
+    qbody' <- checkC ctx' sg body.term $ substCaseWRet body.names w ret
+    let qbody :< qx :< qy :< qih = qbody'
+    expectCompatQ x.loc qx sp
+    expectCompatQ (ih.loc `or` loc) qih ss
+    expectCompatQ y.loc (qy + qih) sp -- [todo] better error message
+    -- then Ψ | Γ ⊢ σ · caseπ e return p ⇒ C of { x ⋄ y, ς.ih ⇒ u }
+    --            ⇒ C[e/p] ⊳ Σ₁+Σ₂
+    pure $ InfRes {
+      type = sub1 ret tree,
+      qout = qtree + qbody
+    }
+
   infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
     -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
     tres <- inferC ctx sg t

lib/Quox/Typing.idr

@@ -47,10 +47,18 @@ public export
 substCasePairRet : BContext 2 -> Term d n -> ScopeTerm d n -> Term d (2 + n)
 substCasePairRet [< x, y] dty retty =
   let tm = Pair (BVT 1 x.loc) (BVT 0 y.loc) $ x.loc `extendL` y.loc
-      arg = Ann tm (dty // fromNat 2) tm.loc
+      arg = Ann tm (dty // shift 2) tm.loc
   in
   retty.term // (arg ::: shift 2)
 
+public export
+substCaseWRet : BContext 3 -> Term d n -> ScopeTerm d n -> Term d (3 + n)
+substCaseWRet [< x, y, ih] dty retty =
+  let tm = Sup (BVT 2 x.loc) (BVT 1 y.loc) $ x.loc `extendL` y.loc
+      arg = Ann tm (dty // shift 3) tm.loc
+  in
+  sub1 (weakS 3 retty) arg
+
 public export
 substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n)
 substCaseSuccRet [< p, ih] retty =
@@ -95,6 +103,10 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
     expectSig : Term d n -> Eff fs (Term d n, ScopeTerm d n)
     expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
 
+    export covering %inline
+    expectW : Term d n -> Eff fs (Term d n, ScopeTerm d n)
+    expectW = expect ExpectedW `(W {shape, body, _}) `((shape, body))
+
     export covering %inline
     expectEnum : Term d n -> Eff fs (SortedSet TagVal)
     expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
@@ -143,6 +155,10 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
     expectSig : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n)
     expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
 
+    export covering %inline
+    expectW : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n)
+    expectW = expect ExpectedW `(W {shape, body, _}) `((shape, body))
+
     export covering %inline
     expectEnum : Term 0 n -> Eff fs (SortedSet TagVal)
     expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)

lib/Quox/Typing/Error.idr

@@ -58,6 +58,7 @@ data Error
 = ExpectedTYPE Loc (NameContexts d n) (Term d n)
 | ExpectedPi   Loc (NameContexts d n) (Term d n)
 | ExpectedSig  Loc (NameContexts d n) (Term d n)
+| ExpectedW    Loc (NameContexts d n) (Term d n)
 | ExpectedEnum Loc (NameContexts d n) (Term d n)
 | ExpectedEq   Loc (NameContexts d n) (Term d n)
 | ExpectedNat  Loc (NameContexts d n) (Term d n)
@@ -116,6 +117,7 @@ Located Error where
   (ExpectedTYPE    loc _ _).loc       = loc
   (ExpectedPi      loc _ _).loc       = loc
   (ExpectedSig     loc _ _).loc       = loc
+  (ExpectedW       loc _ _).loc       = loc
   (ExpectedEnum    loc _ _).loc       = loc
   (ExpectedEq      loc _ _).loc       = loc
   (ExpectedNat     loc _ _).loc       = loc
@@ -256,6 +258,10 @@ prettyErrorNoLoc showContext = \case
     hangDSingle "expected a pair type, but got"
       !(prettyTerm ctx.dnames ctx.tnames s)
 
+  ExpectedW _ ctx s =>
+    hangDSingle "expected an inductive (W) type, but got"
+      !(prettyTerm ctx.dnames ctx.tnames s)
+
   ExpectedEnum _ ctx s =>
     hangDSingle "expected an enumeration type, but got"
       !(prettyTerm ctx.dnames ctx.tnames s)