5 changed files with 199 additions and 65 deletions
--- a/lib/Quox/Loc.idr
+++ b/lib/Quox/Loc.idr
@ -109,6 +109,8 @@ or (L l1) (L l2) = L $ l1 `or_` l2
 public export
 interface Located a where (.loc) : a -> Loc

+export %inline Located Loc where l.loc = l
+
 public export
 0 Located1 : (a -> Type) -> Type
 Located1 f = forall x. Located (f x)
--- a/lib/Quox/Parser/Lexer.idr
+++ b/lib/Quox/Parser/Lexer.idr
@ -197,6 +197,8 @@ reserved =
   Sym "×" `Or` Sym "**",
   Sym "≡" `Or` Sym "==",
   Sym "∷" `Or` Sym "::",
+   Sym "⊲" `Or` Sym "<|",
+   Sym "⋄" `Or` Sym "<>",
   Punc1 '.',
   Word1 "case",
   Word1 "case0", Word1 "case1",
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@ -212,7 +212,8 @@ export
 qtyPatVar : FileName -> Grammar True (PQty, PatVar)
 qtyPatVar fname =
      [|(,) (qty fname) (needRes "." *> patVar fname)|]
-  <|> [|(,) (defLoc fname $ PQ One) (patVar fname)|]
+  <|> do name <- patVar fname
+         pure (PQ (if isUnused name then Zero else One) name.loc, name)


 export
@ -226,15 +227,17 @@ data PCasePat =
  | PZero Loc
  | PSucc PatVar PQty PatVar Loc
  | PBox  PatVar Loc
+  | PSup  PatVar PatVar PQty PatVar Loc
 %runElab derive "PCasePat" [Eq, Ord, Show]

 export
 Located PCasePat where
-  (PPair _ _   loc).loc = loc
-  (PTag  _     loc).loc = loc
-  (PZero       loc).loc = loc
-  (PSucc _ _ _ loc).loc = loc
-  (PBox  _     loc).loc = loc
+  (PPair _ _     loc).loc = loc
+  (PTag  _       loc).loc = loc
+  (PZero         loc).loc = loc
+  (PSucc _ _ _   loc).loc = loc
+  (PBox  _       loc).loc = loc
+  (PSup  _ _ _ _ loc).loc = loc

 ||| either `zero` or `0`
 export
@ -251,6 +254,11 @@ casePat fname = withLoc fname $
         ih <- resC "," *> qtyPatVar fname
           <|> [|(,) (defLoc fname $ PQ Zero) (unused fname)|]
         pure $ PSucc p (fst ih) (snd ih)
+  <|> do x <- patVar fname
+         y <- resC "⋄" *> patVar fname
+         ih <- resC "," *> qtyPatVar fname
+           <|> [|(,) (defLoc fname $ PQ Zero) (unused fname)|]
+         pure $ PSup x y (fst ih) (snd ih)
  <|> delim "[" "]" [|PBox (patVar fname)|]
  <|> fatalError "invalid pattern"

@ -405,12 +413,19 @@ appTerm fname =
  <|> succTerm fname
  <|> normalAppTerm fname

+export
+supTerm : FileName -> Grammar True PTerm
+supTerm fname = withLoc fname $ do
+  l <- appTerm fname; commit
+  r <- optional $ res "⋄" *> assert_total supTerm fname
+  pure $ \loc => maybe l (\r => Sup l r loc) r
+
 export
 infixEqTerm : FileName -> Grammar True PTerm
 infixEqTerm fname = withLoc fname $ do
-  l <- appTerm fname; commit
+  l <- supTerm fname; commit
  rest <- optional $ res "≡" *>
-    [|(,) (assert_total term fname) (needRes ":" *> appTerm fname)|]
+    [|(,) (assert_total term fname) (needRes ":" *> supTerm fname)|]
  let u = Unused $ onlyStart l.loc
  pure $ \loc => maybe l (\rest => Eq (u, snd rest) l (fst rest) loc) rest

@ -430,8 +445,38 @@ lamTerm fname = withLoc fname $ do
    body <- assert_total term fname; commit
    pure $ \loc => foldr (\x, s => k x s loc) body xs

+
+private
+data BindType = BPi | BW | BSig
+%runElab derive "BindType" [Eq, Ord]
+
+private
+data BindSequence' b a = BLast a | BMore a b (BindSequence' b a)
+
+private
+data BindTypeL = BTL BindType Loc
+%runElab derive "BindTypeL" [Eq, Ord]
+
+private
+data BindPart = BT (Maybe PQty) (List1 PatVar) PTerm
+Located BindPart where
+  (BT q xs t).loc = maybe (head xs).loc (.loc) q `extendL` t.loc
+
+
+private
+BindSequence : Type
+BindSequence = BindSequence' BindTypeL BindPart
+
+private
+bindType : FileName -> Grammar True BindTypeL
+bindType fname = bt BPi "→" <|> bt BW "⊲" <|> bt BSig "×"
+where
+  bt : BindType -> (s : String) -> (0 _ : IsReserved s) =>
+       Grammar True BindTypeL
+  bt t str = withLoc fname $ resC str $> BTL t
+
 -- [todo] fix the backtracking in e.g. (F x y z × B)
-export
+private
 properBinders : FileName -> Grammar True (List1 PatVar, PTerm)
 properBinders fname = assert_total $ do
  -- putting assert_total directly on `term`, in this one function,
@ -441,61 +486,85 @@ properBinders fname = assert_total $ do
  t  <- term fname;          needRes ")"
  pure (xs, t)

-export
-sigmaTerm : FileName -> Grammar True PTerm
-sigmaTerm fname =
-      (properBinders fname >>= continueDep)
-  <|> (annTerm fname       >>= continueNondep)
-where
-  continueDep : (List1 PatVar, PTerm) -> Grammar True PTerm
-  continueDep (names, fst) = withLoc fname $ do
-    snd <- needRes "×" *> sigmaTerm fname
-    pure $ \loc => foldr (\x, snd => Sig x fst snd loc) snd names
+private
+bindPart : FileName -> Grammar True BindPart
+bindPart fname = do
+  qty <- optional $ qty fname <* resC "."
+  bnd <- properBinders fname
+     <|> do n <- unused fname
+            t <- if isJust qty then termArg fname else annTerm fname
+            pure (singleton n, t)
+  pure $ uncurry (BT qty) bnd

-  cross : PTerm -> PTerm -> PTerm
-  cross l r = let loc = extend' l.loc r.loc.bounds in
-              Sig (Unused $ onlyStart l.loc) l r loc
+private
+bindSequence : FileName -> Grammar True BindSequence
+bindSequence fname = do
+  x  <- bindPart fname
+  by <- optional $ do
+    b <- bindType fname
+    y <- mustWork $ assert_total bindSequence fname
+    pure (b, y)
+  pure $ maybe (BLast x) (\by => BMore x (fst by) (snd by)) by

-  continueNondep : PTerm -> Grammar False PTerm
-  continueNondep fst = do
-    rest <- optional $ resC "×" *> sepBy1 (res "×") (annTerm fname)
-    pure $ foldr1 cross $ fst ::: maybe [] toList rest
+private
+fromBindSequence : BindSequence -> Grammar False PTerm
+fromBindSequence as = go [<] as where
+  -- the ol’ shunty
+  data Elem = E BindPart BindTypeL
+
+  fatalLoc' : Located z => z -> String -> Grammar False a
+  fatalLoc' z = maybe fatalError fatalLoc z.loc.bounds
+
+  toTerm : BindPart -> Grammar False PTerm
+  toTerm (BT Nothing (Unused _ ::: []) s) = pure s
+  toTerm s = fatalLoc' s $
+    "binder with no following body\n" ++
+    "(maybe some missing parens)"
+
+  fromTerm : PTerm -> BindPart
+  fromTerm t = BT Nothing (singleton $ Unused t.loc) t
+
+  checkNoQty : String -> Maybe PQty -> Grammar False ()
+  checkNoQty s (Just q) = fatalLoc' q "no quantity allowed with \{s}"
+  checkNoQty _ _ = pure ()
+
+  apply : Elem -> PTerm -> Grammar False PTerm
+  apply (E s'@(BT mqty xs s) (BTL b _)) t = case b of
+    BPi => do
+      let q   = fromMaybe (PQ One s.loc) mqty
+          loc = s'.loc `extendL` t.loc
+      pure $ foldr (\x, t => Pi q x s t loc) t xs
+    BW => do
+      checkNoQty "⊲" mqty
+      when (length xs /= 1) $ do
+        let loc = foldr1 extendL $ map (.loc) xs
+        fatalLoc' loc "only one binding allowed with ⊲"
+      pure $ W (head xs) s t (s.loc `extendL` t.loc)
+    BSig => do
+      checkNoQty "×" mqty
+      let loc = s'.loc `extendL` t.loc
+      pure $ foldr (\x, t => Sig x s t loc) t xs
+
+  end : SnocList Elem -> PTerm -> Grammar False PTerm
+  end [<]       t = pure t
+  end (es :< e) t = end es !(apply e t)
+
+  go : SnocList Elem -> BindSequence -> Grammar False PTerm
+  go es (BLast a) = do
+    end es !(toTerm a)
+  go [<] (BMore a b as) =
+    go [< E a b] as
+  go (es :< e@(E a' b')) (BMore a b as) =
+    if b' > b then do
+      t <- apply e !(toTerm a)
+      go (es :< E (fromTerm t) b) as
+    else
+      go (es :< e :< E a b) as

 export
-piTerm : FileName -> Grammar True PTerm
-piTerm fname = withLoc fname $ do
-  q   <- [|GivenQ $ qty fname <* resC "."|] <|> defLoc fname DefaultQ
-  dom <- [|Dep $ properBinders fname|] <|> [|Nondep $ ndDom q fname|]
-  cod <- optional $ do resC "→"; assert_total term fname <* commit
-  when (needCod q dom && isNothing cod) $ fail "missing function type result"
-  pure $ maybe (const $ toTerm dom) (makePi q dom) cod
-where
-  data PiQty = GivenQ PQty | DefaultQ Loc
-  data PiDom = Dep (List1 PatVar, PTerm) | Nondep PTerm
+bindTerm : FileName -> Grammar True PTerm
+bindTerm fname = fromBindSequence !(bindSequence fname)

-  ndDom : PiQty -> FileName -> Grammar True PTerm
-  ndDom (GivenQ   _) = termArg   -- ｢1.(List A)｣, not ｢1.List A｣
-  ndDom (DefaultQ _) = sigmaTerm
-
-  needCod : PiQty -> PiDom -> Bool
-  needCod (DefaultQ _) (Nondep _) = False
-  needCod _            _          = True
-
-  toTerm : PiDom -> PTerm
-  toTerm (Dep (_, s)) = s
-  toTerm (Nondep s)   = s
-
-  toQty : PiQty -> PQty
-  toQty (GivenQ   qty) = qty
-  toQty (DefaultQ loc) = PQ One loc
-
-  toDoms : PQty -> PiDom -> List1 (PQty, PatVar, PTerm)
-  toDoms qty (Dep (xs, s)) = [(qty, x, s) | x <- xs]
-  toDoms qty (Nondep s)    = singleton (qty, Unused s.loc, s)
-
-  makePi : PiQty -> PiDom -> PTerm -> Loc -> PTerm
-  makePi q doms cod loc =
-    foldr (\(q, x, s), t => Pi q x s t loc) cod $ toDoms (toQty q) doms

 public export
 PCaseArm : Type
@ -529,6 +598,9 @@ checkCaseArms loc ((PSucc p q ih _, rhs1) :: rest) = do
 checkCaseArms loc ((PBox x _, rhs) :: rest) =
  if null rest then pure $ CaseBox x rhs loc
  else fatalError "unexpected pattern after box"
+checkCaseArms loc ((PSup x y rh ih _, rhs) :: rest) =
+  if null rest then pure $ CaseW x y (rh, ih) rhs loc
+  else fatalError "unexpected pattern after sup"

 export
 caseBody : FileName -> Grammar True PCaseBody
@ -557,8 +629,7 @@ caseTerm fname = withLoc fname $ do
 -- term : FileName -> Grammar True PTerm
 term fname = lamTerm fname
         <|> caseTerm fname
-         <|> piTerm fname
-         <|> sigmaTerm fname
+         <|> bindTerm fname


 export
--- a/syntax.ebnf
+++ b/syntax.ebnf
@ -24,7 +24,7 @@ dim arg = "@", dim.

 pat var = NAME | "_".

-term = lambda | case | pi | sigma | ann.
+term = lambda | case | pi | w | sigma | ann.

 lambda = ("λ" | "δ"), {pat var}+, "⇒", term.

@ -39,17 +39,22 @@ pattern = "zero" | "0"
            (* default qty for IH is 1 *)
        | TAG
        | "[", pat var, "]"
-        | "(", pat var, ",", pat var, ")".
+        | "(", pat var, ",", pat var, ")"
+        | pat var, "⋄", pat var, [",", [qty, "."], pat var].

 (* default qty is 1 *)
 pi = [qty, "."], (binder | term arg), "→", term.
 binder = "(", {NAME}+, ":", term, ")".

+w = binder, "⊲", ann.
+
 sigma = (binder | ann), "×", (sigma | ann).

 ann = infix eq, ["∷", term].

-infix eq = app term, ["≡", term, ":", app term]. (* dependent is below *)
+infix eq = sup term, ["≡", term, ":", sup term]. (* dependent is below *)
+
+sup term = app term, ["⋄", app term].

 app term       = coe | comp | split universe | dep eq | succ | normal app.
 split universe = "★", NAT.
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@ -168,6 +168,8 @@ tests = "parser" :- [
          (App (V "B" {}) (V "x" {}) _) _) _),
    parseMatch term "(x : A) → B x"
      `(Pi (PQ One _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
+    parseFails term "(x : A) → (y : B x)",
+    parseFails term "(x : A) → 1.(B x)",
    parseMatch term "1.A → B"
      `(Pi (PQ One _) (Unused _) (V "A" {}) (V "B" {}) _),
    parseMatch term "A → B"
@ -249,6 +251,43 @@ tests = "parser" :- [
    parseFails term "(x,,y)"
  ],

+  "w" :- [
+    parseMatch term "(x : A) ⊲ B"
+      `(W (PV "x" _) (V "A" {}) (V "B" {}) _),
+    parseFails term "(x y : A) ⊲ B",
+    parseFails term "1.(x : A) ⊲ B",
+    parseMatch term "(x : A) ⊲ (y : B) ⊲ C"
+      `(W (PV "x" _) (V "A" {})
+        (W (PV "y" _) (V "B" {})  (V "C" {}) _) _),
+    parseMatch term "A ⊲ B"
+      `(W _ (V "A" {}) (V "B" {}) _),
+    parseMatch term "A <| B"
+      `(W _ (V "A" {}) (V "B" {}) _),
+    parseFails term "A ⊲ (y : B)",
+    parseMatch term "(x : A) ⊲ B x × C"
+      `(W (PV "x" _) (V "A" {})
+         (Sig _ (App (V "B" {}) (V "x" {}) _) (V "C" {}) _) _),
+    parseMatch term "A ⊲ B → C"
+      `(Pi _ _ (W _ (V "A" {}) (V "B" {}) _) (V "C" {}) _),
+    parseMatch term "A → B ⊲ C"
+      `(Pi _ _ (V "A" {}) (W _ (V "B" {}) (V "C" {}) _) _)
+  ],
+
+  "sup" :- [
+    parseMatch term "s ⋄ t"
+      `(Sup (V "s" {}) (V "t" {}) _),
+    parseMatch term "s ⋄ t ⋄ u"
+      `(Sup (V "s" {}) (Sup (V "t" {}) (V "u" {}) _) _),
+    parseMatch term "s <> t"
+      `(Sup (V "s" {}) (V "t" {}) _),
+    parseMatch term "a b ⋄ c d"
+      `(Sup (App (V "a" {}) (V "b" {}) _) (App (V "c" {}) (V "d" {}) _) _),
+    parseMatch term "a ⋄ b ≡ a' ⋄ b' : (A ⊲ B)"
+      `(Eq (_, W _ (V "A" {}) (V "B" {}) _)
+           (Sup (V "a"  {}) (V "b"  {}) _)
+           (Sup (V "a'" {}) (V "b'" {}) _) _)
+  ],
+
  "equality type" :- [
    parseMatch term "Eq (i ⇒ A) s t"
      `(Eq (PV "i" _, V "A" {}) (V "s" {}) (V "t" {}) _),
@ -396,8 +435,23 @@ tests = "parser" :- [
    parseMatch term "caseω n return ℕ of { succ _, ih ⇒ ih; zero ⇒ 0; }"
      `(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
        (CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
+    parseMatch term "caseω n return ℕ of { succ _, _ ⇒ ih; zero ⇒ 0; }"
+      `(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
+        (CaseNat (Zero _) (Unused _, PQ Zero _, Unused _, V "ih" {}) _) _),
    parseFails term "caseω n return A of { zero ⇒ a }",
-    parseFails term "caseω n return ℕ of { succ ⇒ 5 }"
+    parseFails term "caseω n return ℕ of { succ ⇒ 5 }",
+    parseMatch term "case e return z ⇒ C of { a ⋄ b, ω.ih ⇒ u }"
+      `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
+        (CaseW (PV "a" _) (PV "b" _) (PQ Any _, PV "ih" _) (V "u" {}) _) _),
+    parseMatch term "case e return z ⇒ C of { a ⋄ b, ih ⇒ u }"
+      `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
+        (CaseW (PV "a" _) (PV "b" _) (PQ One _, PV "ih" _) (V "u" {}) _) _),
+    parseMatch term "case e return z ⇒ C of { a ⋄ b ⇒ u }"
+      `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
+        (CaseW (PV "a" _) (PV "b" _) (PQ Zero _, Unused _) (V "u" {}) _) _),
+    parseMatch term "case e return z ⇒ C of { a ⋄ b, _ ⇒ u }"
+      `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
+        (CaseW (PV "a" _) (PV "b" _) (PQ Zero _, Unused _) (V "u" {}) _) _)
  ],

  "definitions" :- [