From 3bbf0366c8171af51c16420a8439e7d5ca798c11 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 21 May 2023 20:33:42 +0200 Subject: [PATCH] =?UTF-8?q?make=200=20in=20=E2=98=85=E2=82=80=20optional?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- examples/bool.quox | 10 +++++----- examples/either.quox | 28 ++++++++++++++-------------- examples/list.quox | 14 +++++++------- examples/misc.quox | 24 ++++++++++++------------ examples/nat.quox | 4 ++-- examples/pair.quox | 22 +++++++++++----------- lib/Quox/Parser/Parser.idr | 6 +++--- tests/Tests/Parser.idr | 4 ++-- 8 files changed, 56 insertions(+), 56 deletions(-) diff --git a/examples/bool.quox b/examples/bool.quox index 1d142b5..79ad6f9 100644 --- a/examples/bool.quox +++ b/examples/bool.quox @@ -2,19 +2,19 @@ load "misc.quox"; namespace bool { -def0 Bool : ★⁰ = {true, false}; +def0 Bool : ★ = {true, false}; def boolω : 1.Bool → [ω.Bool] = λ b ⇒ case1 b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] }; -def if : 0.(A : ★⁰) → 1.Bool → ω.A → ω.A → A = +def if : 0.(A : ★) → 1.Bool → ω.A → ω.A → A = λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f }; -- [todo]: universe lifting -def0 If : 1.Bool → 0.★⁰ → 0.★⁰ → ★⁰ = - λ b T F ⇒ case1 b return ★⁰ of { 'true ⇒ T; 'false ⇒ F }; +def0 If : 1.Bool → 0.★ → 0.★ → ★ = + λ b T F ⇒ case1 b return ★ of { 'true ⇒ T; 'false ⇒ F }; -def0 T : ω.Bool → ★⁰ = λ b ⇒ If b True False; +def0 T : ω.Bool → ★ = λ b ⇒ If b True False; def true-not-false : Not ('true ≡ 'false : Bool) = λ eq ⇒ coe (i ⇒ T (eq @i)) 'true; diff --git a/examples/either.quox b/examples/either.quox index 4abe355..df93527 100644 --- a/examples/either.quox +++ b/examples/either.quox @@ -3,22 +3,22 @@ load "bool.quox"; namespace either { -def0 Tag : ★⁰ = {left, right}; +def0 Tag : ★ = {left, right}; -def0 Payload : 0.★⁰ → 0.★⁰ → 1.Tag → ★⁰ = - λ A B tag ⇒ case1 tag return ★⁰ of { 'left ⇒ A; 'right ⇒ B }; +def0 Payload : 0.★ → 0.★ → 1.Tag → ★ = + λ A B tag ⇒ case1 tag return ★ of { 'left ⇒ A; 'right ⇒ B }; -def0 Either : 0.★⁰ → 0.★⁰ → ★⁰ = +def0 Either : 0.★ → 0.★ → ★ = λ A B ⇒ (tag : Tag) × Payload A B tag; -def Left : 0.(A 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 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 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) = @@ -28,7 +28,7 @@ def elim' : of { 'left ⇒ f; 'right ⇒ g }; def elim : - 0.(A 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 = @@ -45,16 +45,16 @@ def Right = either.Right; namespace dec { -def0 Dec : 0.★⁰ → ★⁰ = λ A ⇒ Either [0.A] [0.Not A]; +def0 Dec : 0.★ → ★ = λ A ⇒ Either [0.A] [0.Not A]; -def Yes : 0.(A : ★⁰) → 0.A → Dec A = λ A y ⇒ Left [0.A] [0.Not A] [y]; -def No : 0.(A : ★⁰) → 0.(Not A) → Dec A = λ A n ⇒ Right [0.A] [0.Not A] [n]; +def Yes : 0.(A : ★) → 0.A → Dec A = λ A y ⇒ Left [0.A] [0.Not A] [y]; +def No : 0.(A : ★) → 0.(Not A) → Dec A = λ A n ⇒ Right [0.A] [0.Not A] [n]; -def0 DecEq : 0.★⁰ → ★⁰ = +def0 DecEq : 0.★ → ★ = λ A ⇒ ω.(x : A) → ω.(y : A) → Dec (x ≡ y : A); def elim : - 0.(A : ★⁰) → 0.(P : 0.(Dec A) → ★⁰) → + 0.(A : ★) → 0.(P : 0.(Dec A) → ★) → ω.(0.(y : A) → P (Yes A y)) → ω.(0.(n : Not A) → P (No A n)) → 1.(x : Dec A) → P x = @@ -63,7 +63,7 @@ def elim : (λ y ⇒ case0 y return y' ⇒ P (Left [0.A] [0.Not A] y') of {[y'] ⇒ f y'}) (λ n ⇒ case0 n return n' ⇒ P (Right [0.A] [0.Not A] n') of {[n'] ⇒ g n'}); -def bool : 0.(A : ★⁰) → 1.(Dec A) → Bool = +def bool : 0.(A : ★) → 1.(Dec A) → Bool = λ A ⇒ elim A (λ _ ⇒ Bool) (λ _ ⇒ 'true) (λ _ ⇒ 'false); } diff --git a/examples/list.quox b/examples/list.quox index 659d98e..870ae6b 100644 --- a/examples/list.quox +++ b/examples/list.quox @@ -2,23 +2,23 @@ load "nat.quox"; namespace list { -def0 Vec : 0.ℕ → 0.★⁰ → ★⁰ = +def0 Vec : 0.ℕ → 0.★ → ★ = λ n A ⇒ - caseω n return ★⁰ of { + caseω n return ★ of { zero ⇒ {nil}; succ _, 0.Tail ⇒ A × Tail }; -def0 List : 0.★⁰ → ★⁰ = +def0 List : 0.★ → ★ = λ A ⇒ (len : ℕ) × Vec len A; -def nil : 0.(A : ★⁰) → List A = +def nil : 0.(A : ★) → List A = λ A ⇒ (0, 'nil); -def cons : 0.(A : ★⁰) → 1.A → 1.(List 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 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,7 +28,7 @@ def foldr' : 0.(A B : ★⁰) → λ cons ⇒ case1 cons return B of { (first, rest) ⇒ c first (ih rest) } }; -def foldr : 0.(A 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 }; diff --git a/examples/misc.quox b/examples/misc.quox index 80c0ac9..8c6a8c1 100644 --- a/examples/misc.quox +++ b/examples/misc.quox @@ -1,36 +1,36 @@ -def0 True : ★⁰ = {true}; +def0 True : ★ = {true}; -def0 False : ★⁰ = {}; -def0 Not : 0.★⁰ → ★⁰ = λ A ⇒ ω.A → False; +def0 False : ★ = {}; +def0 Not : 0.★ → ★ = λ A ⇒ ω.A → False; -def void : 0.(A : ★⁰) → 0.False → A = +def void : 0.(A : ★) → 0.False → A = λ A v ⇒ case0 v return A of { }; -def0 Pred : 0.★⁰ → ★¹ = λ A ⇒ 0.A → ★⁰; +def0 Pred : 0.★ → ★¹ = λ A ⇒ 0.A → ★; -def0 All : 0.(A : ★⁰) → 0.(Pred A) → ★¹ = +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.(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 : - 0.(A : ★⁰) → 0.(P : Pred A) → + 0.(A : ★) → 0.(P : Pred A) → 0.(p : All A P) → 0.(q : All A P) → - 0.A → ★⁰ = + 0.A → ★ = λ A P p q x ⇒ p x ≡ q x : P x; def funext : - 0.(A : ★⁰) → 0.(P : Pred A) → 0.(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 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 (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }; -def trans : 0.(A : ★⁰) → 0.(x y 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 (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 }; diff --git a/examples/nat.quox b/examples/nat.quox index 1177334..9ac818b 100644 --- a/examples/nat.quox +++ b/examples/nat.quox @@ -37,8 +37,8 @@ def0 succ-inj : 0.(m n : ℕ) → 0.(succ m ≡ succ n : ℕ) → m ≡ n : ℕ λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖); -def0 IsSucc : 0.ℕ → ★⁰ = - λ n ⇒ caseω n return ★⁰ of { zero ⇒ False; succ _ ⇒ True }; +def0 IsSucc : 0.ℕ → ★ = + λ n ⇒ caseω n return ★ of { zero ⇒ False; succ _ ⇒ True }; def isSucc? : ω.(n : ℕ) → Dec (IsSucc n) = λ n ⇒ diff --git a/examples/pair.quox b/examples/pair.quox index 925f7fa..790df56 100644 --- a/examples/pair.quox +++ b/examples/pair.quox @@ -1,35 +1,35 @@ namespace pair { -def0 Σ : 0.(A : ★⁰) → 0.(0.A → ★⁰) → ★⁰ = λ A B ⇒ (x : A) × B x; +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 : - 0.(A : ★⁰) → 0.(B : 0.A → ★⁰) → 0.(C : 0.(x : A) → 0.(B x) → ★⁰) → + 0.(A : ★) → 0.(B : 0.A → ★) → 0.(C : 0.(x : A) → 0.(B x) → ★) → 1.(f : 1.(x : A) → 1.(y : B x) → C x y) → 1.(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 }; def uncurry' : - 0.(A B C : ★⁰) → 1.(1.A → 1.B → C) → 1.(A × B) → C = + 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) → ★⁰) → + 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 = + 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 → ★⁰) → + 0.(A : ★) → 0.(B : 0.A → ★) → 1.(p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B = λ A B p ⇒ case1 p @@ -37,14 +37,14 @@ def0 fst-snd : of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) }; def map : - 0.(A A' : ★⁰) → - 0.(B : 0.A → ★⁰) → 0.(B' : 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 A' B 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 c5d5764..1fe34d4 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -274,7 +274,7 @@ tupleTerm fname = withLoc fname $ do export universe1 : Grammar True Universe -universe1 = universeTok <|> res "★" *> super +universe1 = universeTok <|> res "★" *> option 0 super ||| argument/atomic term: single-token terms, or those with delimiters e.g. ||| `[t]` @@ -359,8 +359,8 @@ compTerm fname = withLoc fname $ do export splitUniverseTerm : FileName -> Grammar True PTerm splitUniverseTerm fname = - withLoc fname $ resC "★" *> mustWork [|TYPE $ nat <|> super|] - -- having super here looks redundant, but when parsing a non-atomic term + withLoc fname $ resC "★" *> [|TYPE $ option 0 $ nat <|> super|] + -- some of this looks redundant, but when parsing a non-atomic term -- this branch will be taken first export diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index 6c1a3bb..fcda2fc 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -116,8 +116,8 @@ tests = "parser" :- [ parseMatch term "Type4" `(TYPE 4 _), parseMatch term "Type 100" `(TYPE 100 _), parseMatch term "(Type 1000)" `(TYPE 1000 _), - parseFails term "Type", - parseFails term "★" + parseMatch term "Type" `(TYPE 0 _), + parseMatch term "★" `(TYPE 0 _) ], "applications" :- [