make quantities optional and default to 1

examples/bool.quox

@@ -5,13 +5,13 @@ namespace bool {
 def0 Bool : ★ = {true, false};
 
 def boolω : Bool → [ω.Bool] =
-  λ b ⇒ case1 b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] };
+  λ b ⇒ case b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] };
 
 def if : 0.(A : ★) → Bool → ω.A → ω.A → A =
-  λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f };
+  λ A b t f ⇒ case b return A of { 'true ⇒ t; 'false ⇒ f };
 
 def0 If : Bool → ★ → ★ → ★ =
-  λ b T F ⇒ case1 b return ★ of { 'true ⇒ T; 'false ⇒ F };
+  λ b T F ⇒ case b return ★ of { 'true ⇒ T; 'false ⇒ F };
 
 def0 T : Bool → ★ = λ b ⇒ If b True False;
 

examples/either.quox

@@ -6,7 +6,7 @@ namespace either {
 def0 Tag : ★ = {left, right};
 
 def0 Payload : ★ → ★ → Tag → ★ =
-  λ A B tag ⇒ case1 tag return ★ of { 'left ⇒ A; 'right ⇒ B };
+  λ A B tag ⇒ case tag return ★ of { 'left ⇒ A; 'right ⇒ B };
 
 def0 Either : ★ → ★ → ★ =
   λ A B ⇒ (tag : Tag) × Payload A B tag;
@@ -23,7 +23,7 @@ def elim' :
     ω.((x : B) → P (Right A B x)) →
     (t : Tag) → (a : Payload A B t) → P (t, a) =
   λ A B P f g t ⇒
-    case1 t
+    case t
     return t' ⇒ (a : Payload A B t') → P (t', a)
     of { 'left ⇒ f; 'right ⇒ g };
 
@@ -33,7 +33,7 @@ def elim :
     ω.((x : B) → P (Right A B x)) →
     (x : Either A B) → P x =
   λ A B P f g e ⇒
-    case1 e return e' ⇒ P e' of { (t, a) ⇒ elim' A B P f g t a };
+    case e return e' ⇒ P e' of { (t, a) ⇒ elim' A B P f g t a };
 
 
 }

examples/list.quox

@@ -16,21 +16,21 @@ def nil : 0.(A : ★) → List A =
   λ A ⇒ (0, 'nil);
 
 def cons : 0.(A : ★) → A → List A → List A =
-  λ A x xs ⇒ case1 xs return List A of { (len, elems) ⇒ (succ len, x, elems) };
+  λ A x xs ⇒ case xs return List A of { (len, elems) ⇒ (succ len, x, elems) };
 
 def foldr' : 0.(A B : ★) →
              B → ω.(A → B → B) → (n : ℕ) → Vec n A → B =
   λ A B z c n ⇒
-  case1 n return n' ⇒ Vec n' A → B of {
+  case n return n' ⇒ Vec n' A → B of {
     zero ⇒
-      λ nil ⇒ case1 nil return B of { 'nil ⇒ z };
+      λ nil ⇒ case nil return B of { 'nil ⇒ z };
     succ n, 1.ih ⇒
-      λ cons ⇒ case1 cons return B of { (first, rest) ⇒ c first (ih rest) }
+      λ cons ⇒ case cons return B of { (first, rest) ⇒ c first (ih rest) }
   };
 
 def foldr : 0.(A B : ★) → B → ω.(A → B → B) → List A → B =
   λ A B z c xs ⇒
-  case1 xs return B of { (len, elems) ⇒ foldr' A B z c len elems };
+  case xs return B of { (len, elems) ⇒ foldr' A B z c len elems };
 
 def sum : List ℕ → ℕ = foldr ℕ ℕ 0 nat.plus;
 

examples/maybe.quox

@@ -6,7 +6,7 @@ namespace maybe {
 def0 Tag : ★ = {nothing, just}
 
 def0 Payload : Tag → ★ → ★ =
-  λ tag A ⇒ caseω tag return ★ of { 'nothing ⇒ True; 'just ⇒ A }
+  λ tag A ⇒ case tag return ★ of { 'nothing ⇒ True; 'just ⇒ A }
 
 def0 Maybe : ★ → ★ =
   λ A ⇒ (t : Tag) × Payload t A
@@ -21,7 +21,7 @@ def Just : 0.(A : ★) → A → Maybe A =
   λ _ x ⇒ ('just, x)
 
 def0 IsJustTag : Tag → ★ =
-  λ t ⇒ caseω t return ★ of { 'just ⇒ True; 'nothing ⇒ False }
+  λ t ⇒ case t return ★ of { 'just ⇒ True; 'nothing ⇒ False }
 
 def0 IsJust : (A : ★) → Maybe A → ★ =
   λ A x ⇒ IsJustTag (tag A x)
@@ -36,7 +36,7 @@ def is-just? : 0.(A : ★) → ω.(x : Maybe A) → Dec (IsJust A x) =
 def0 nothing-unique :
     (A : ★) → (x : True) → ('nothing, x) ≡ Nothing A : Maybe A =
   λ A x ⇒
-  caseω x return x' ⇒ ('nothing, x') ≡ Nothing A : Maybe A of {
+  case x return x' ⇒ ('nothing, x') ≡ Nothing A : Maybe A of {
     'true ⇒ δ _ ⇒ ('nothing, 'true)
   }
 
@@ -47,14 +47,14 @@ def elim :
     ω.((x : A) → P (Just A x)) →
     (x : Maybe A) → P x =
   λ A P n j x ⇒
-  case1 x return x' ⇒ P x' of { (tag, payload) ⇒
-    (case1 tag
+  case x return x' ⇒ P x' of { (tag, payload) ⇒
+    (case tag
      return t ⇒
        0.(eq : tag ≡ t : Tag) → P (t, coe (i ⇒ Payload (eq @i) A) payload)
      of {
        'nothing ⇒
           λ eq ⇒
-          case1 coe (i ⇒ Payload (eq @i) A) payload
+          case coe (i ⇒ Payload (eq @i) A) payload
           return p ⇒ P ('nothing, p)
           of { 'true ⇒ n };
        'just ⇒ λ eq ⇒ j (coe (i ⇒ Payload (eq @i) A) payload)

examples/nat.quox

@@ -6,29 +6,29 @@ namespace nat {
 
 def dup : ℕ → [ω.ℕ] =
   λ n ⇒
-  case1 n return [ω.ℕ] of {
+  case n return [ω.ℕ] of {
     zero        ⇒ [zero];
-    succ _, 1.d ⇒ case1 d return [ω.ℕ] of { [d] ⇒ [succ d] }
+    succ _, 1.d ⇒ case d return [ω.ℕ] of { [d] ⇒ [succ d] }
   };
 
 def plus : ℕ → ℕ → ℕ =
   λ m n ⇒
-  case1 m return ℕ of {
+  case m return ℕ of {
     zero        ⇒ n;
     succ _, 1.p ⇒ succ p
   };
 
 def timesω : ℕ → ω.ℕ → ℕ =
   λ m n ⇒
-  case1 m return ℕ of {
+  case m return ℕ of {
     zero        ⇒ zero;
     succ _, 1.t ⇒ plus n t
   };
 
 def times : ℕ → ℕ → ℕ =
-  λ m n ⇒ case1 dup n return ℕ of { [n] ⇒ timesω m n };
+  λ m n ⇒ case dup n return ℕ of { [n] ⇒ timesω m n };
 
-def pred : ℕ → ℕ = λ n ⇒ case1 n return ℕ of { zero ⇒ zero; succ n ⇒ n };
+def pred : ℕ → ℕ = λ n ⇒ case n return ℕ of { zero ⇒ zero; succ n ⇒ n };
 
 def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
   λ n ⇒ δ 𝑖 ⇒ n;
@@ -38,7 +38,7 @@ def0 succ-inj : (m n : ℕ) → succ m ≡ succ n : ℕ → m ≡ n : ℕ =
 
 
 def0 IsSucc : ℕ → ★ =
-  λ n ⇒ caseω n return ★ of { zero ⇒ False; succ _ ⇒ True };
+  λ n ⇒ case n return ★ of { zero ⇒ False; succ _ ⇒ True };
 
 def isSucc? : ω.(n : ℕ) → Dec (IsSucc n) =
   λ n ⇒
@@ -56,7 +56,7 @@ def succ-not-zero : 0.(m : ℕ) → Not (succ m ≡ zero : ℕ) =
 
 def0 not-succ-self : (m : ℕ) → Not (m ≡ succ m : ℕ) =
   λ m ⇒
-  caseω m return m' ⇒ Not (m' ≡ succ m' : ℕ) of {
+  case m return m' ⇒ Not (m' ≡ succ m' : ℕ) of {
     zero         ⇒ zero-not-succ 0;
     succ n, ω.ih ⇒ λ eq ⇒ ih (succ-inj n (succ n) eq)
   }
@@ -88,21 +88,21 @@ def eqb : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ dec.bool (m ≡ n : ℕ) (eq?
 
 def0 plus-zero : (m : ℕ) → m ≡ plus m 0 : ℕ =
   λ m ⇒
-  caseω m return m' ⇒ m' ≡ plus m' 0 : ℕ of {
+  case m return m' ⇒ m' ≡ plus m' 0 : ℕ of {
     zero         ⇒ δ _ ⇒ zero;
     succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
   };
 
 def0 plus-succ : (m n : ℕ) → succ (plus m n) ≡ plus m (succ n) : ℕ =
   λ m n ⇒
-  caseω m return m' ⇒ succ (plus m' n) ≡ plus m' (succ n) : ℕ of {
+  case m return m' ⇒ succ (plus m' n) ≡ plus m' (succ n) : ℕ of {
     zero         ⇒ δ _ ⇒ succ n;
     succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
   };
 
 def0 plus-comm : (m n : ℕ) → plus m n ≡ plus n m : ℕ =
   λ m n ⇒
-  caseω m return m' ⇒ plus m' n ≡ plus n m' : ℕ of {
+  case m return m' ⇒ plus m' n ≡ plus n m' : ℕ of {
     zero ⇒ plus-zero n;
     succ m', ω.ih ⇒
       trans ℕ (succ (plus m' n)) (succ (plus n m')) (plus n (succ m'))

examples/pair.quox

@@ -13,7 +13,7 @@ def uncurry :
     (f : (x : A) → (y : B x) → C x y) →
     (p : Σ A B) → C (fst A B p) (snd A B p) =
   λ A B C f p ⇒
-    case1 p return p' ⇒ C (fst A B p') (snd A B p') of { (x, y) ⇒ f x y };
+    case p return p' ⇒ C (fst A B p') (snd A B p') of { (x, y) ⇒ f x y };
 
 def uncurry' :
     0.(A B C : ★) → (A → B → C) → (A × B) → C =
@@ -32,7 +32,7 @@ def0 fst-snd :
     (A : ★) → (B : 0.A → ★) →
     (p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B =
   λ A B p ⇒
-    case1 p
+    case p
     return p' ⇒ p' ≡ (fst A B p', snd A B p') : Σ A B
     of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) };
 
@@ -42,7 +42,7 @@ def map :
     (f : A → A') → (g : 0.(x : A) → (B x) → B' (f x)) →
     (Σ A B) → Σ A' B' =
   λ A A' B B' f g p ⇒
-    case1 p return Σ A' B' of { (x, y) ⇒ (f x, g x y) };
+    case p return Σ A' B' of { (x, y) ⇒ (f x, g x y) };
 
 def map' : 0.(A A' B B' : ★) → (A → A') → (B → B') → (A × B) → A' × B' =
   λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g);

lib/Quox/Parser/Parser.idr

@@ -198,18 +198,21 @@ export
 enumType : Grammar True (List TagVal)
 enumType = delimSep "{" "}" "," bareTag
 
-||| e.g. `case` or `case 1.`
+||| e.g. `case1` or `case 1.`
 export
 caseIntro : FileName -> Grammar True PQty
 caseIntro fname =
       withLoc fname (PQ Zero <$ res "case0")
   <|> withLoc fname (PQ One  <$ res "case1")
   <|> withLoc fname (PQ Any  <$ res "caseω")
-  <|> delim "case" "." (qty fname)
+  <|> do resC "case"
+         qty fname <* needRes "." <|> defLoc fname (PQ One)
 
 export
 qtyPatVar : FileName -> Grammar True (PQty, PatVar)
-qtyPatVar fname = [|(,) (qty fname) (needRes "." *> patVar fname)|]
+qtyPatVar fname =
+      [|(,) (qty fname) (needRes "." *> patVar fname)|]
+  <|> [|(,) (defLoc fname $ PQ One) (patVar fname)|]
 
 
 export
@@ -438,18 +441,6 @@ properBinders fname = assert_total $ do
   t  <- term fname;          needRes ")"
   pure (xs, t)
 
-export
-piTerm : FileName -> Grammar True PTerm
-piTerm fname = withLoc fname $ do
-  q   <- qty fname;               resC "."
-  dom <- piBinder;                needRes "→"
-  cod <- assert_total term fname; commit
-  pure $ \loc => foldr (\x, t => Pi q x (snd dom) t loc) cod (fst dom)
-where
-  piBinder : Grammar True (List1 PatVar, PTerm)
-  piBinder = properBinders fname
-         <|> [|(,) [|singleton $ unused fname|] (termArg fname)|]
-
 export
 sigmaTerm : FileName -> Grammar True PTerm
 sigmaTerm fname =
@@ -470,6 +461,42 @@ where
     rest <- optional $ resC "×" *> sepBy1 (res "×") (annTerm fname)
     pure $ foldr1 cross $ fst ::: maybe [] toList rest
 
+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
+
+  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
 PCaseArm = (PCasePat, PTerm)

syntax.ebnf

@@ -28,18 +28,21 @@ term = lambda | case | pi | sigma | ann.
 
 lambda = ("λ" | "δ"), {pat var}+, "⇒", term.
 
-case        = case intro, term, "return", case return, "of", case body.
-case intro  = "case0" | "case1" | "caseω" | "case", qty, ".".
+case = case intro, term, "return", case return, "of", case body.
+(* default qty is 1 *)
+case intro  = "case0" | "case1" | "caseω" | "case", [qty, "."].
 case return = [pat var, "⇒"], term.
 case body   = "{", {pattern, "⇒", term / ";"}, [";"], "}".
 
 pattern = "zero" | "0"
-        | "succ", pat var, [",", qty, ".", pat var]
+        | "succ", pat var, [",", [qty, "."], pat var]
+            (* default qty for IH is 1 *)
         | TAG
         | "[", pat var, "]"
         | "(", pat var, ",", pat var, ")".
 
-pi = qty, ".", (binder | term arg), "→", term.
+(* default qty is 1 *)
+pi = [qty, "."], (binder | term arg), "→", term.
 binder = "(", {NAME}+, ":", term, ")".
 
 sigma = (binder | ann), "×", (sigma | ann).

tests/Tests/Parser.idr

@@ -35,7 +35,7 @@ ToInfo Failure where
 parameters {auto _ : (Show a, Eq a)} {c : Bool} (grm : FileName -> Grammar c a)
   parsesWith : String -> (a -> Bool) -> Test
   parsesWith inp p = test (ltrim inp) $ do
-    res <- mapFst ParseError $ lexParseWith (grm "‹test›") inp
+    res <- mapFst ParseError $ lexParseWith (grm "<test>") inp
     unless (p res) $ Left $ WrongResult $ show res
 
   parsesAs : String -> a -> Test
@@ -166,9 +166,15 @@ tests = "parser" :- [
       `(Pi (PQ One _) (PV "x" _) (V "A" {})
         (Pi (PQ One _) (PV "y" _) (V "A" {})
           (App (V "B" {}) (V "x" {}) _) _) _),
-    parseFails term "(x : A) → B x",
+    parseMatch term "(x : A) → B x"
+      `(Pi (PQ One _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
     parseMatch term "1.A → B"
       `(Pi (PQ One _) (Unused _) (V "A" {}) (V "B" {}) _),
+    parseMatch term "A → B"
+      `(Pi (PQ One _) (Unused _) (V "A" {}) (V "B" {}) _),
+    parseMatch term "A → B → C"
+      `(Pi (PQ One _) (Unused _) (V "A" {})
+          (Pi (PQ One _) (Unused _) (V "B" {}) (V "C" {}) _) _),
     parseMatch term "1.(List A) → List B"
       `(Pi (PQ One _) (Unused _)
           (App (V "List" {}) (V "A" {}) _)
@@ -190,7 +196,21 @@ tests = "parser" :- [
     parseMatch term "A × B × C" $
       `(Sig (Unused _) (V "A" {}) (Sig (Unused _) (V "B" {}) (V "C" {}) _) _),
     parseMatch term "(A × B) × C" $
-      `(Sig (Unused _) (Sig (Unused _) (V "A" {}) (V "B" {}) _) (V "C" {}) _)
+      `(Sig (Unused _) (Sig (Unused _) (V "A" {}) (V "B" {}) _) (V "C" {}) _),
+    parseMatch term "A × B → C" $
+      `(Pi (PQ One _) (Unused _)
+          (Sig (Unused _) (V "A" {}) (V "B" {}) _)
+          (V "C" {}) _),
+    parseMatch term "A → B × C" $
+      `(Pi (PQ One _) (Unused _)
+          (V "A" {})
+          (Sig (Unused _) (V "B" {}) (V "C" {}) _) _),
+    parseMatch term "A → B × C → D" $
+      `(Pi (PQ One _) (Unused _)
+          (V "A" {})
+          (Pi (PQ One _) (Unused _)
+            (Sig (Unused _) (V "B" {}) (V "C" {}) _)
+              (V "D" {}) _) _)
   ],
 
   "lambdas" :- [
@@ -330,7 +350,25 @@ tests = "parser" :- [
         (CasePair (PV "l" _, PV "r" _)
                   (App (V "r" {}) (V "l" {}) _) _) _),
     parseMatch term
-      "case 1 . f s return x ⇒ A x of { (l, r) ⇒ r l }"
+      "case 1. f s return x ⇒ A x of { (l, r) ⇒ r l }"
+      `(Case (PQ One _) (App (V "f" {}) (V "s" {}) _)
+        (PV "x" _, App (V "A" {}) (V "x" {}) _)
+        (CasePair (PV "l" _, PV "r" _)
+                  (App (V "r" {}) (V "l" {}) _) _) _),
+    parseMatch term
+      "caseω f s return x ⇒ A x of { (l, r) ⇒ r l }"
+      `(Case (PQ Any _) (App (V "f" {}) (V "s" {}) _)
+        (PV "x" _, App (V "A" {}) (V "x" {}) _)
+        (CasePair (PV "l" _, PV "r" _)
+                  (App (V "r" {}) (V "l" {}) _) _) _),
+    parseMatch term
+      "case0 f s return x ⇒ A x of { (l, r) ⇒ r l }"
+      `(Case (PQ Zero _) (App (V "f" {}) (V "s" {}) _)
+        (PV "x" _, App (V "A" {}) (V "x" {}) _)
+        (CasePair (PV "l" _, PV "r" _)
+                  (App (V "r" {}) (V "l" {}) _) _) _),
+    parseMatch term
+      "case f s return x ⇒ A x of { (l, r) ⇒ r l }"
       `(Case (PQ One _) (App (V "f" {}) (V "s" {}) _)
         (PV "x" _, App (V "A" {}) (V "x" {}) _)
         (CasePair (PV "l" _, PV "r" _)
@@ -352,6 +390,12 @@ tests = "parser" :- [
     parseMatch term "caseω n return ℕ of { succ _, 1.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 ⇒ ih; zero ⇒ 0; }"
+      `(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
+        (CaseNat (Zero _) (Unused _, PQ Any _, PV "ih" _, V "ih" {}) _) _),
+    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" {}) _) _),
     parseFails term "caseω n return A of { zero ⇒ a }",
     parseFails term "caseω n return ℕ of { succ ⇒ 5 }"
   ],