From 3f06e8d68b6a6b058f8cf0f4fa46be1af6aa7a5f Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 19 Apr 2023 21:36:57 +0200 Subject: [PATCH] allow multiple names in a binder MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit e.g. "(x y : ℕ) × plus x y ≡ 10 : ℕ" fixes #2 --- examples/bool.quox | 4 ++-- examples/either.quox | 12 +++++------- examples/list.quox | 19 +++++++++---------- examples/misc.quox | 17 ++++++----------- examples/nat.quox | 7 +++---- examples/pair.quox | 23 +++++++++++++---------- lib/Quox/Parser/Parser.idr | 13 +++++++------ tests/Tests/Parser.idr | 4 ++++ 8 files changed, 49 insertions(+), 50 deletions(-) diff --git a/examples/bool.quox b/examples/bool.quox index d4c5de3..5de0f0a 100644 --- a/examples/bool.quox +++ b/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 or : ω.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b; +def and : 1.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false; +def or : 1.Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b; } diff --git a/examples/either.quox b/examples/either.quox index 45f5c23..f2d748e 100644 --- a/examples/either.quox +++ 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.(P : 0.(Either A B) → ★₀) → + 0.(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.(P : 0.(Either A B) → ★₀) → + 0.(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 = diff --git a/examples/list.quox b/examples/list.quox index 5fe605e..9a0173b 100644 --- a/examples/list.quox +++ b/examples/list.quox @@ -18,20 +18,19 @@ 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 { - zero ⇒ - λ nil ⇒ case1 nil return B of { 'nil ⇒ z }; - succ n, 1.ih ⇒ - λ cons ⇒ case1 cons return B of { (first, rest) ⇒ c first (ih rest) } - }; + case1 n return n' ⇒ 1.(Vec n' A) → B of { + zero ⇒ + λ nil ⇒ case1 nil return B of { 'nil ⇒ z }; + succ n, 1.ih ⇒ + λ cons ⇒ case1 cons return B of { (first, rest) ⇒ c first (ih rest) } + }; -def foldr : 0.(A : ★₀) → 0.(B : ★₀) → - 1.B → ω.(1.A → 1.B → B) → 1.(List A) → B = +def foldr : 0.(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 }; + case1 xs return B of { (len, elems) ⇒ foldr' A B z c len elems }; def sum : 1.(List ℕ) → ℕ = foldr ℕ ℕ 0 nat.plus; diff --git a/examples/misc.quox b/examples/misc.quox index 2c87e2a..f6ba7d9 100644 --- a/examples/misc.quox +++ b/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) → - 1.(p : All A P) → - 0.(x : A) → 0.(y : A) → 1.(xy : x ≡ y : A) → - Eq [𝑖 ⇒ P (xy @𝑖)] (p x) (p y) = + 0.(A : ★₀) → 0.(P : Pred A) → 1.(p : All A P) → + 0.(x 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.(p : All A P) → 0.(q : All A P) → - 1.(All A (eq-f A P p q)) → - p ≡ q : All A P = + 0.(A : ★₀) → 0.(P : Pred A) → 0.(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) → - 1.(x ≡ y : A) → y ≡ x : A = +def sym : 0.(A : ★₀) → 0.(x y : 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 @𝑗 }; diff --git a/examples/nat.quox b/examples/nat.quox index 6fbe4f0..36ce76c 100644 --- a/examples/nat.quox +++ b/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 : ℕ) → - 0.(succ m ≡ succ n : ℕ) → m ≡ n : ℕ = +def0 succ-inj : 0.(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; diff --git a/examples/pair.quox b/examples/pair.quox index 8eee382..016bae4 100644 --- a/examples/pair.quox +++ b/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 → ★₀) → - ω.(Σ A B) → A = +def fst : 0.(A : ★₀) → 0.(B : 0.A → ★₀) → ω.(Σ A B) → A = λ A B p ⇒ caseω p return A of { (x, _) ⇒ x }; -def snd : 0.(A : ★₀) → 0.(B : 0.A → ★₀) → - ω.(p : Σ A B) → B (fst A B p) = +def snd : 0.(A : ★₀) → 0.(B : 0.A → ★₀) → ω.(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' : - 0.(A : ★₀) → 0.(A' : ★₀) → - 0.(B : ★₀) → 0.(B' : ★₀) → - 1.(f : 1.A → A') → 1.(g : 1.B → B') → - 1.(A × B) → A' × B' = +def map' : 0.(A A' B B' : ★₀) → + 1.(1.A → A') → 1.(1.B → B') → 1.(A × B) → A' × B' = λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g); } diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index 3e3a71f..cc33b4b 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/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 q (x, s) t = Pi q x s t - domain = binderHead <|> [|(Nothing,) aTerm|] + makePi : Qty -> (List1 BName, PTerm) -> PTerm -> PTerm + makePi q (xs, s) t = foldr (\x => Pi q x s) t xs + domain = binderHead <|> [|(Nothing ::: [],) aTerm|] sigma = [|makeSigma binderHead (resC "×" *> annTerm)|] where - makeSigma : (BName, PTerm) -> PTerm -> PTerm - makeSigma (x, s) t = Sig x s t + makeSigma : (List1 BName, PTerm) -> PTerm -> PTerm + makeSigma (xs, s) t = foldr (\x => Sig x s) t xs private covering annTerm : Grammar True PTerm diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index 6ca28fd..316b8d0 100644 --- a/tests/Tests/Parser.idr +++ b/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"),