allow multiple names in a binder

e.g. "(x y : ℕ) × plus x y ≡ 10 : ℕ"

fixes #2

examples/bool.quox

@@ -21,8 +21,8 @@ def true-not-false : Not ('true ≡ 'false : Bool) =
 
 
 -- [todo] infix
-def and : ω.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false;
+def and : 1.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false;
-def or : ω.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b;
+def or  : 1.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b;
 
 }
 

examples/either.quox

@@ -5,21 +5,20 @@ namespace either {
 
 def0 Tag : ★₀ = {left, right};
 
-def0 Payload : 0.(A : ★₀) → 0.(B : ★₀) → 1.Tag → ★₀ =
+def0 Payload : 0.★₀ → 0.★₀ → 1.Tag → ★₀ =
   λ A B tag ⇒ case1 tag return ★₀ of { 'left ⇒ A; 'right ⇒ B };
 
 def0 Either : 0.★₀ → 0.★₀ → ★₀ =
   λ A B ⇒ (tag : Tag) × Payload A B tag;
 
-def Left : 0.(A : ★₀) → 0.(B : ★₀) → 1.A → Either A B =
+def Left : 0.(A B : ★₀) → 1.A → Either A B =
   λ A B x ⇒ ('left, x);
 
-def Right : 0.(A : ★₀) → 0.(B : ★₀) → 1.B → Either A B =
+def Right : 0.(A B : ★₀) → 1.B → Either A B =
   λ A B x ⇒ ('right, x);
 
 def elim' :
-    0.(A : ★₀) → 0.(B : ★₀) →
+    0.(A B : ★₀) → 0.(P : 0.(Either A B) → ★₀) →
-    0.(P : 0.(Either A B) → ★₀) →
     ω.(1.(x : A) → P (Left  A B x)) →
     ω.(1.(x : B) → P (Right A B x)) →
     1.(t : Tag) → 1.(a : Payload A B t) → P (t, a) =
@@ -29,8 +28,7 @@ def elim' :
     of { 'left ⇒ f; 'right ⇒ g };
 
 def elim :
-    0.(A : ★₀) → 0.(B : ★₀) →
+    0.(A B : ★₀) → 0.(P : 0.(Either A B) → ★₀) →
-    0.(P : 0.(Either A B) → ★₀) →
     ω.(1.(x : A) → P (Left  A B x)) →
     ω.(1.(x : B) → P (Right A B x)) →
     1.(x : Either A B) → P x =

examples/list.quox

@@ -18,7 +18,7 @@ def nil : 0.(A : ★₀) → List A =
 def cons : 0.(A : ★₀) → 1.A → 1.(List A) → List A =
   λ A x xs ⇒ case1 xs return List A of { (len, elems) ⇒ (succ len, x, elems) };
 
-def foldr' : 0.(A : ★₀) → 0.(B : ★₀) →
+def foldr' : 0.(A B : ★₀) →
              1.B → ω.(1.A → 1.B → B) → 1.(n : ℕ) → 1.(Vec n A) → B =
   λ A B z c n ⇒
   case1 n return n' ⇒ 1.(Vec n' A) → B of {
@@ -28,8 +28,7 @@ def foldr' : 0.(A : ★₀) → 0.(B : ★₀) →
       λ cons ⇒ case1 cons return B of { (first, rest) ⇒ c first (ih rest) }
   };
 
-def foldr : 0.(A : ★₀) → 0.(B : ★₀) →
+def foldr : 0.(A B : ★₀) → 1.B → ω.(1.A → 1.B → B) → 1.(List A) → B =
-            1.B → ω.(1.A → 1.B → B) → 1.(List A) → B =
   λ A B z c xs ⇒
   case1 xs return B of { (len, elems) ⇒ foldr' A B z c len elems };
 

examples/misc.quox

@@ -12,10 +12,8 @@ def0 All : 0.(A : ★₀) → 0.(Pred A) → ★₁ =
   λ A P ⇒ 1.(x : A) → P x;
 
 def cong :
-    0.(A : ★₀) → 0.(P : Pred A) →
+    0.(A : ★₀) → 0.(P : Pred A) → 1.(p : All A P) →
-    1.(p : All A P) →
+    0.(x y : A) → 1.(xy : x ≡ y : A) → Eq [𝑖 ⇒ P (xy @𝑖)] (p x) (p y) =
-    0.(x : A) → 0.(y : A) → 1.(xy : x ≡ y : A) →
-    Eq [𝑖 ⇒ P (xy @𝑖)] (p x) (p y) =
   λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖);
 
 def0 eq-f :
@@ -25,17 +23,14 @@ def0 eq-f :
   λ A P p q x ⇒ p x ≡ q x : P x;
 
 def funext :
-    0.(A : ★₀) → 0.(P : Pred A) →
+    0.(A : ★₀) → 0.(P : Pred A) → 0.(p q : All A P) →
-    0.(p : All A P) → 0.(q : All A P) →
+    1.(All A (eq-f A P p q)) → p ≡ q : All A P =
-    1.(All A (eq-f A P p q)) →
-    p ≡ q : All A P =
   λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖;
 
-def sym : 0.(A : ★₀) → 0.(x : A) → 0.(y : A) →
+def sym : 0.(A : ★₀) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A =
-          1.(x ≡ y : A) → y ≡ x : A =
   λ A x y eq ⇒ δ 𝑖 ⇒ comp [A] @0 @1 (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 };
 
-def trans : 0.(A : ★₀) → 0.(x : A) → 0.(y : A) → 0.(z : A) →
+def trans : 0.(A : ★₀) → 0.(x y z : A) →
             ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A =
   λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒
     comp [A] @0 @1 (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 };

examples/nat.quox

@@ -33,8 +33,7 @@ def pred : 1.ℕ → ℕ = λ n ⇒ case1 n return ℕ of { zero ⇒ zero; succ
 def pred-succ : ω.(n : ℕ) → pred (succ n) ≡ n : ℕ =
   λ n ⇒ δ 𝑖 ⇒ n;
 
-def0 succ-inj : 0.(m : ℕ) → 0.(n : ℕ) →
+def0 succ-inj : 0.(m n : ℕ) → 0.(succ m ≡ succ n : ℕ) → m ≡ n : ℕ =
-                0.(succ m ≡ succ n : ℕ) → m ≡ n : ℕ =
   λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖);
 
 
@@ -94,14 +93,14 @@ def0 plus-zero : 0.(m : ℕ) → m ≡ plus m 0 : ℕ =
     succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
   };
 
-def0 plus-succ : 0.(m : ℕ) → 0.(n : ℕ) → succ (plus m n) ≡ plus m (succ n) : ℕ =
+def0 plus-succ : 0.(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 {
     zero         ⇒ δ _ ⇒ succ n;
     succ _, ω.ih ⇒ δ 𝑖 ⇒ succ (ih @𝑖)
   };
 
-def0 plus-comm : 0.(m : ℕ) → 0.(n : ℕ) → plus m n ≡ plus n m : ℕ =
+def0 plus-comm : 0.(m n : ℕ) → plus m n ≡ plus n m : ℕ =
   λ m n ⇒
   caseω m return m' ⇒ plus m' n ≡ plus n m' : ℕ of {
     zero ⇒ plus-zero n;

examples/pair.quox

@@ -2,12 +2,10 @@ namespace pair {
 
 def0 Σ : 0.(A : ★₀) → 0.(0.A → ★₀) → ★₀ = λ A B ⇒ (x : A) × B x;
 
-def fst : 0.(A : ★₀) → 0.(B : 0.A → ★₀) →
+def fst : 0.(A : ★₀) → 0.(B : 0.A → ★₀) → ω.(Σ A B) → A =
-          ω.(Σ A B) → A =
   λ A B p ⇒ caseω p return A of { (x, _) ⇒ x };
 
-def snd : 0.(A : ★₀) → 0.(B : 0.A → ★₀) →
+def snd : 0.(A : ★₀) → 0.(B : 0.A → ★₀) → ω.(p : Σ A B) → B (fst A B p) =
-          ω.(p : Σ A B) → B (fst A B p) =
   λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (_, y) ⇒ y };
 
 def uncurry :
@@ -17,11 +15,19 @@ def uncurry :
   λ A B C f p ⇒
     case1 p return p' ⇒ C (fst A B p') (snd A B p') of { (x, y) ⇒ f x y };
 
+def uncurry' :
+    0.(A B C : ★₀) → 1.(1.A → 1.B → C) → 1.(A × B) → C =
+  λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C);
+
 def curry :
     0.(A : ★₀) → 0.(B : 0.A → ★₀) → 0.(C : 0.(Σ A B) → ★₀) →
     1.(f : 1.(p : Σ A B) → C p) → 1.(x : A) → 1.(y : B x) → C (x, y) =
   λ A B C f x y ⇒ f (x, y);
 
+def curry' :
+    0.(A B C : ★₀) → 1.(1.(A × B) → C) → 1.A → 1.B → C =
+  λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C);
+
 def0 fst-snd :
     0.(A : ★₀) → 0.(B : 0.A → ★₀) →
     1.(p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B =
@@ -31,18 +37,15 @@ def0 fst-snd :
     of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) };
 
 def map :
-    0.(A : ★₀) → 0.(A' : ★₀) →
+    0.(A A' : ★₀) →
     0.(B : 0.A → ★₀) → 0.(B' : 0.A' → ★₀) →
     1.(f : 1.A → A') → 1.(g : 0.(x : A) → 1.(B x) → B' (f x)) →
     1.(Σ A B) → Σ A' B' =
   λ A A' B B' f g p ⇒
     case1 p return Σ A' B' of { (x, y) ⇒ (f x, g x y) };
 
-def map' :
+def map' : 0.(A A' B B' : ★₀) →
-    0.(A : ★₀) → 0.(A' : ★₀) →
+           1.(1.A → A') → 1.(1.B → B') → 1.(A × B) → A' × B' =
-    0.(B : ★₀) → 0.(B' : ★₀) →
-    1.(f : 1.A → A') → 1.(g : 1.B → B') →
-    1.(A × B) → A' × B' =
   λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g);
 
 }

lib/Quox/Parser/Parser.idr

@@ -242,19 +242,20 @@ mutual
   bindTerm : Grammar True PTerm
   bindTerm = pi <|> sigma
   where
-    binderHead = parens {commit = False} [|MkPair bname (resC ":" *> term)|]
+    binderHead =
+      parens {commit = False} [|MkPair (some bname) (resC ":" *> term)|]
 
     pi, sigma : Grammar True PTerm
     pi = [|makePi (qty <* res ".") domain (resC "→" *> term)|]
     where
-      makePi : Qty -> (BName, PTerm) -> PTerm -> PTerm
+      makePi : Qty -> (List1 BName, PTerm) -> PTerm -> PTerm
-      makePi q (x, s) t = Pi q x s t
+      makePi q (xs, s) t = foldr (\x => Pi q x s) t xs
-      domain = binderHead <|> [|(Nothing,) aTerm|]
+      domain = binderHead <|> [|(Nothing ::: [],) aTerm|]
 
     sigma = [|makeSigma binderHead (resC "×" *> annTerm)|]
     where
-      makeSigma : (BName, PTerm) -> PTerm -> PTerm
+      makeSigma : (List1 BName, PTerm) -> PTerm -> PTerm
-      makeSigma (x, s) t = Sig x s t
+      makeSigma (xs, s) t = foldr (\x => Sig x s) t xs
 
   private covering
   annTerm : Grammar True PTerm

tests/Tests/Parser.idr

@@ -148,6 +148,8 @@ tests = "parser" :- [
       Pi Any (Just "x") (V "A") (V "B" :@ V "x"),
     parsesAs term "#.(x : A) -> B x" $
       Pi Any (Just "x") (V "A") (V "B" :@ V "x"),
+    parsesAs term "1.(x y : A) -> B x" $
+      Pi One (Just "x") (V "A") $ Pi One (Just "y") (V "A") (V "B" :@ V "x"),
     parseFails term "(x : A) → B x",
     parsesAs term "1.A → B"
       (Pi One Nothing (V "A") (V "B")),
@@ -158,6 +160,8 @@ tests = "parser" :- [
       Sig (Just "x") (V "A") (V "B" :@ V "x"),
     parsesAs term "(x : A) ** B x" $
       Sig (Just "x") (V "A") (V "B" :@ V "x"),
+    parsesAs term "(x y : A) × B x" $
+      Sig (Just "x") (V "A") $ Sig (Just "y") (V "A") (V "B" :@ V "x"),
     parseFails term "1.(x : A) × B x",
     parsesAs term "A × B" $
       Sig Nothing (V "A") (V "B"),