make quantities optional and default to 1
This commit is contained in:
parent
349cf2f477
commit
932469a91e
10 changed files with 193 additions and 122 deletions
|
|
@ -4,24 +4,24 @@ namespace bool {
|
|||
|
||||
def0 Bool : ★ = {true, false};
|
||||
|
||||
def boolω : 1.Bool → [ω.Bool] =
|
||||
λ b ⇒ case1 b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] };
|
||||
def boolω : Bool → [ω.Bool] =
|
||||
λ b ⇒ case b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] };
|
||||
|
||||
def if : 0.(A : ★) → 1.Bool → ω.A → ω.A → A =
|
||||
λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f };
|
||||
def if : 0.(A : ★) → Bool → ω.A → ω.A → A =
|
||||
λ A b t f ⇒ case b return A of { 'true ⇒ t; 'false ⇒ f };
|
||||
|
||||
def0 If : 1.Bool → 0.★ → 0.★ → ★ =
|
||||
λ b T F ⇒ case1 b return ★ of { 'true ⇒ T; 'false ⇒ F };
|
||||
def0 If : Bool → ★ → ★ → ★ =
|
||||
λ b T F ⇒ case 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;
|
||||
|
||||
|
||||
-- [todo] infix
|
||||
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;
|
||||
def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false;
|
||||
def or : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b;
|
||||
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -5,35 +5,35 @@ namespace either {
|
|||
|
||||
def0 Tag : ★ = {left, right};
|
||||
|
||||
def0 Payload : 0.★ → 0.★ → 1.Tag → ★ =
|
||||
λ A B tag ⇒ case1 tag return ★ of { 'left ⇒ A; 'right ⇒ B };
|
||||
def0 Payload : ★ → ★ → Tag → ★ =
|
||||
λ A B tag ⇒ case tag return ★ of { 'left ⇒ A; 'right ⇒ B };
|
||||
|
||||
def0 Either : 0.★ → 0.★ → ★ =
|
||||
def0 Either : ★ → ★ → ★ =
|
||||
λ A B ⇒ (tag : Tag) × Payload A B tag;
|
||||
|
||||
def Left : 0.(A B : ★) → 1.A → Either A B =
|
||||
def Left : 0.(A B : ★) → A → Either A B =
|
||||
λ A B x ⇒ ('left, x);
|
||||
|
||||
def Right : 0.(A B : ★) → 1.B → Either A B =
|
||||
def Right : 0.(A B : ★) → B → Either A B =
|
||||
λ A B x ⇒ ('right, x);
|
||||
|
||||
def elim' :
|
||||
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) =
|
||||
ω.((x : A) → P (Left A B x)) →
|
||||
ω.((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
|
||||
return t' ⇒ 1.(a : Payload A B t') → P (t', a)
|
||||
case t
|
||||
return t' ⇒ (a : Payload A B t') → P (t', a)
|
||||
of { 'left ⇒ f; 'right ⇒ g };
|
||||
|
||||
def elim :
|
||||
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 =
|
||||
ω.((x : A) → P (Left A B x)) →
|
||||
ω.((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 };
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -45,25 +45,25 @@ def Right = either.Right;
|
|||
|
||||
namespace dec {
|
||||
|
||||
def0 Dec : 0.★ → ★ = λ A ⇒ Either [0.A] [0.Not A];
|
||||
def0 Dec : ★ → ★ = λ 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];
|
||||
|
||||
def0 DecEq : 0.★ → ★ =
|
||||
def0 DecEq : ★ → ★ =
|
||||
λ A ⇒ ω.(x : A) → ω.(y : A) → Dec (x ≡ y : A);
|
||||
|
||||
def elim :
|
||||
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 =
|
||||
(x : Dec A) → P x =
|
||||
λ A P f g ⇒
|
||||
either.elim [0.A] [0.Not A] P
|
||||
(λ 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 : ★) → Dec A → Bool =
|
||||
λ A ⇒ elim A (λ _ ⇒ Bool) (λ _ ⇒ 'true) (λ _ ⇒ 'false);
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -2,37 +2,37 @@ load "nat.quox";
|
|||
|
||||
namespace list {
|
||||
|
||||
def0 Vec : 0.ℕ → 0.★ → ★ =
|
||||
def0 Vec : ℕ → ★ → ★ =
|
||||
λ n A ⇒
|
||||
caseω n return ★ of {
|
||||
zero ⇒ {nil};
|
||||
succ _, 0.Tail ⇒ A × Tail
|
||||
};
|
||||
|
||||
def0 List : 0.★ → ★ =
|
||||
def0 List : ★ → ★ =
|
||||
λ A ⇒ (len : ℕ) × Vec len A;
|
||||
|
||||
def nil : 0.(A : ★) → List A =
|
||||
λ A ⇒ (0, 'nil);
|
||||
|
||||
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 cons : 0.(A : ★) → A → List A → List A =
|
||||
λ A x xs ⇒ case xs return List A of { (len, elems) ⇒ (succ len, x, elems) };
|
||||
|
||||
def foldr' : 0.(A B : ★) →
|
||||
1.B → ω.(1.A → 1.B → B) → 1.(n : ℕ) → 1.(Vec n A) → B =
|
||||
B → ω.(A → B → B) → (n : ℕ) → Vec n A → B =
|
||||
λ A B z c n ⇒
|
||||
case1 n return n' ⇒ 1.(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 : ★) → 1.B → ω.(1.A → 1.B → B) → 1.(List A) → B =
|
||||
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 : 1.(List ℕ) → ℕ = foldr ℕ ℕ 0 nat.plus;
|
||||
def sum : List ℕ → ℕ = foldr ℕ ℕ 0 nat.plus;
|
||||
|
||||
def numbers : List ℕ = (5, (0, 1, 2, 3, 4, 'nil));
|
||||
|
||||
|
|
|
|||
|
|
@ -5,10 +5,10 @@ namespace maybe {
|
|||
|
||||
def0 Tag : ★ = {nothing, just}
|
||||
|
||||
def0 Payload : ω.Tag → ω.★ → ★ =
|
||||
λ tag A ⇒ caseω tag return ★ of { 'nothing ⇒ True; 'just ⇒ A }
|
||||
def0 Payload : Tag → ★ → ★ =
|
||||
λ tag A ⇒ case tag return ★ of { 'nothing ⇒ True; 'just ⇒ A }
|
||||
|
||||
def0 Maybe : ω.★ → ★ =
|
||||
def0 Maybe : ★ → ★ =
|
||||
λ A ⇒ (t : Tag) × Payload t A
|
||||
|
||||
def tag : 0.(A : ★) → ω.(Maybe A) → Tag =
|
||||
|
|
@ -17,13 +17,13 @@ def tag : 0.(A : ★) → ω.(Maybe A) → Tag =
|
|||
def Nothing : 0.(A : ★) → Maybe A =
|
||||
λ _ ⇒ ('nothing, 'true)
|
||||
|
||||
def Just : 0.(A : ★) → 1.A → Maybe A =
|
||||
def Just : 0.(A : ★) → A → Maybe A =
|
||||
λ _ x ⇒ ('just, x)
|
||||
|
||||
def0 IsJustTag : ω.Tag → ★ =
|
||||
λ t ⇒ caseω t return ★ of { 'just ⇒ True; 'nothing ⇒ False }
|
||||
def0 IsJustTag : Tag → ★ =
|
||||
λ t ⇒ case t return ★ of { 'just ⇒ True; 'nothing ⇒ False }
|
||||
|
||||
def0 IsJust : 0.(A : ★) → ω.(Maybe A) → ★ =
|
||||
def0 IsJust : (A : ★) → Maybe A → ★ =
|
||||
λ A x ⇒ IsJustTag (tag A x)
|
||||
|
||||
def is-just? : 0.(A : ★) → ω.(x : Maybe A) → Dec (IsJust A x) =
|
||||
|
|
@ -34,9 +34,9 @@ def is-just? : 0.(A : ★) → ω.(x : Maybe A) → Dec (IsJust A x) =
|
|||
}
|
||||
|
||||
def0 nothing-unique :
|
||||
0.(A : ★) → ω.(x : True) → ('nothing, x) ≡ Nothing A : Maybe A =
|
||||
(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)
|
||||
}
|
||||
|
||||
|
|
@ -44,17 +44,17 @@ def elim :
|
|||
0.(A : ★) →
|
||||
0.(P : 0.(Maybe A) → ★) →
|
||||
ω.(P (Nothing A)) →
|
||||
ω.(1.(x : A) → P (Just A x)) →
|
||||
1.(x : Maybe A) → P x =
|
||||
ω.((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)
|
||||
|
|
|
|||
|
|
@ -1,33 +1,31 @@
|
|||
def0 True : ★ = {true}
|
||||
|
||||
def0 False : ★ = {}
|
||||
def0 Not : 0.★ → ★ = λ A ⇒ ω.A → False
|
||||
def0 Not : ★ → ★ = λ A ⇒ ω.A → False
|
||||
|
||||
def void : 0.(A : ★) → 0.False → A =
|
||||
λ A v ⇒ case0 v return A of { }
|
||||
|
||||
def0 Pred : 0.★ → ★¹ = λ A ⇒ 0.A → ★
|
||||
|
||||
def0 All : 0.(A : ★) → 0.(Pred A) → ★¹ =
|
||||
λ A P ⇒ 1.(x : A) → P x
|
||||
def0 All : (A : ★) → (0.A → ★) → ★¹ =
|
||||
λ A P ⇒ (x : A) → P x
|
||||
|
||||
def cong :
|
||||
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) =
|
||||
0.(A : ★) → 0.(P : 0.A → ★) → (p : All A P) →
|
||||
0.(x y : A) → (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 : 0.A → ★) →
|
||||
0.(p : All A P) → 0.(q : All A P) →
|
||||
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) →
|
||||
1.(All A (eq-f A P p q)) → p ≡ q : All A P =
|
||||
0.(A : ★) → 0.(P : 0.A → ★) → 0.(p q : All A P) →
|
||||
(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) → (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) →
|
||||
|
|
|
|||
|
|
@ -4,41 +4,41 @@ load "either.quox";
|
|||
|
||||
namespace nat {
|
||||
|
||||
def dup : 1.ℕ → [ω.ℕ] =
|
||||
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 : 1.ℕ → 1.ℕ → ℕ =
|
||||
def plus : ℕ → ℕ → ℕ =
|
||||
λ m n ⇒
|
||||
case1 m return ℕ of {
|
||||
case m return ℕ of {
|
||||
zero ⇒ n;
|
||||
succ _, 1.p ⇒ succ p
|
||||
};
|
||||
|
||||
def timesω : 1.ℕ → ω.ℕ → ℕ =
|
||||
def timesω : ℕ → ω.ℕ → ℕ =
|
||||
λ m n ⇒
|
||||
case1 m return ℕ of {
|
||||
case m return ℕ of {
|
||||
zero ⇒ zero;
|
||||
succ _, 1.t ⇒ plus n t
|
||||
};
|
||||
|
||||
def times : 1.ℕ → 1.ℕ → ℕ =
|
||||
λ m n ⇒ case1 dup n return ℕ of { [n] ⇒ timesω m n };
|
||||
def times : ℕ → ℕ → ℕ =
|
||||
λ m n ⇒ case dup n return ℕ of { [n] ⇒ timesω m n };
|
||||
|
||||
def pred : 1.ℕ → ℕ = λ 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;
|
||||
|
||||
def0 succ-inj : 0.(m n : ℕ) → 0.(succ m ≡ succ n : ℕ) → m ≡ n : ℕ =
|
||||
def0 succ-inj : (m n : ℕ) → 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 : ℕ → ★ =
|
||||
λ n ⇒ case n return ★ of { zero ⇒ False; succ _ ⇒ True };
|
||||
|
||||
def isSucc? : ω.(n : ℕ) → Dec (IsSucc n) =
|
||||
λ n ⇒
|
||||
|
|
@ -54,9 +54,9 @@ def succ-not-zero : 0.(m : ℕ) → Not (succ m ≡ zero : ℕ) =
|
|||
λ m eq ⇒ coe (𝑖 ⇒ IsSucc (eq @𝑖)) 'true;
|
||||
|
||||
|
||||
def0 not-succ-self : 0.(m : ℕ) → Not (m ≡ succ m : ℕ) =
|
||||
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)
|
||||
}
|
||||
|
|
@ -86,23 +86,23 @@ def eq? : DecEq ℕ =
|
|||
def eqb : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ dec.bool (m ≡ n : ℕ) (eq? m n);
|
||||
|
||||
|
||||
def0 plus-zero : 0.(m : ℕ) → m ≡ plus m 0 : ℕ =
|
||||
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 : 0.(m n : ℕ) → succ (plus m n) ≡ plus m (succ n) : ℕ =
|
||||
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 : 0.(m n : ℕ) → plus m n ≡ plus n m : ℕ =
|
||||
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'))
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
namespace pair {
|
||||
|
||||
def0 Σ : 0.(A : ★) → 0.(0.A → ★) → ★ = λ A B ⇒ (x : A) × B x;
|
||||
def0 Σ : (A : ★) → (0.A → ★) → ★ = λ A B ⇒ (x : A) × B x;
|
||||
|
||||
def fst : 0.(A : ★) → 0.(B : 0.A → ★) → ω.(Σ A B) → A =
|
||||
λ A B p ⇒ caseω p return A of { (x, _) ⇒ x };
|
||||
|
|
@ -10,42 +10,41 @@ def snd : 0.(A : ★) → 0.(B : 0.A → ★) → ω.(p : Σ A B) → B (fst A B
|
|||
|
||||
def uncurry :
|
||||
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) =
|
||||
(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 : ★) → 1.(1.A → 1.B → C) → 1.(A × B) → C =
|
||||
0.(A B C : ★) → (A → B → C) → (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) =
|
||||
(f : (p : Σ A B) → C p) → (x : A) → (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 : ★) → ((A × B) → C) → A → 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 =
|
||||
(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) };
|
||||
|
||||
def map :
|
||||
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' =
|
||||
(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' : ★) →
|
||||
1.(1.A → A') → 1.(1.B → B') → 1.(A × B) → A' × B' =
|
||||
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);
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -29,17 +29,20 @@ 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, ".".
|
||||
(* 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).
|
||||
|
|
|
|||
|
|
@ -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" :- [
|
||||
|
|
@ -335,6 +355,24 @@ tests = "parser" :- [
|
|||
(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" _)
|
||||
(App (V "r" {}) (V "l" {}) _) _) _),
|
||||
parseMatch term
|
||||
"case1 t return A of { 'x ⇒ p; 'y ⇒ q; 'z ⇒ r }"
|
||||
`(Case (PQ One _) (V "t" {})
|
||||
|
|
@ -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 }"
|
||||
],
|
||||
|
|
|
|||
Loading…
Reference in a new issue