Compare commits
6 Commits
64de93a13c
...
3bbf0366c8
| Author | SHA1 | Date |
|---|---|---|
 rhiannon morris
|
3bbf0366c8 | |
|
rhiannon morris
|
7c68cd9098 | |
|
rhiannon morris
|
282565c7a3 | |
|
rhiannon morris
|
2af8ee20ea | |
|
rhiannon morris
|
42aa07c9c8 | |
|
rhiannon morris
|
e4a20cc632 |
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 };
|
||||
|
||||
|
|
|
|||
|
|
@ -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 @𝑗 };
|
||||
|
|
|
|||
|
|
@ -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 ⇒
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
||||
|
|
|
|||
|
|
@ -121,15 +121,29 @@ namespace Char
|
|||
isOther = isOther . genCat
|
||||
|
||||
|
||||
export
|
||||
isSupDigit : Char -> Bool
|
||||
isSupDigit ch = ch `elem` unpack "⁰¹²³⁴⁵⁶⁷⁸⁹"
|
||||
|
||||
export
|
||||
isSubDigit : Char -> Bool
|
||||
isSubDigit ch = ch `elem` unpack "₀₁₂₃₄₅₆₇₈₉"
|
||||
|
||||
export
|
||||
isAsciiDigit : Char -> Bool
|
||||
isAsciiDigit ch = '0' <= ch && ch <= '9'
|
||||
|
||||
export
|
||||
isIdStart : Char -> Bool
|
||||
isIdStart ch =
|
||||
ch == '_' || isLetter ch || isNumber ch && not ('0' <= ch && ch <= '9')
|
||||
(ch == '_' || isLetter ch || isNumber ch) &&
|
||||
not (isSupDigit ch || isAsciiDigit ch)
|
||||
|
||||
export
|
||||
isIdCont : Char -> Bool
|
||||
isIdCont ch =
|
||||
isIdStart ch || ch == '\'' || ch == '-' || isMark ch || isNumber ch
|
||||
(isIdStart ch || ch == '\'' || ch == '-' || isMark ch || isNumber ch) &&
|
||||
not (isSupDigit ch)
|
||||
|
||||
export
|
||||
isIdConnector : Char -> Bool
|
||||
|
|
|
|||
|
|
@ -0,0 +1,85 @@
|
|||
module Quox.Displace
|
||||
|
||||
import Quox.Syntax
|
||||
|
||||
|
||||
parameters (k : Universe)
|
||||
namespace Term
|
||||
export doDisplace : Term d n -> Term d n
|
||||
export doDisplaceS : ScopeTermN s d n -> ScopeTermN s d n
|
||||
export doDisplaceDS : DScopeTermN s d n -> DScopeTermN s d n
|
||||
|
||||
namespace Elim
|
||||
export doDisplace : Elim d n -> Elim d n
|
||||
|
||||
namespace Term
|
||||
doDisplace (TYPE l loc) = TYPE (k + l) loc
|
||||
doDisplace (Pi qty arg res loc) =
|
||||
Pi qty (doDisplace arg) (doDisplaceS res) loc
|
||||
doDisplace (Lam body loc) = Lam (doDisplaceS body) loc
|
||||
doDisplace (Sig fst snd loc) = Sig (doDisplace fst) (doDisplaceS snd) loc
|
||||
doDisplace (Pair fst snd loc) = Pair (doDisplace fst) (doDisplace snd) loc
|
||||
doDisplace (Enum cases loc) = Enum cases loc
|
||||
doDisplace (Tag tag loc) = Tag tag loc
|
||||
doDisplace (Eq ty l r loc) =
|
||||
Eq (doDisplaceDS ty) (doDisplace l) (doDisplace r) loc
|
||||
doDisplace (DLam body loc) = DLam (doDisplaceDS body) loc
|
||||
doDisplace (Nat loc) = Nat loc
|
||||
doDisplace (Zero loc) = Zero loc
|
||||
doDisplace (Succ p loc) = Succ (doDisplace p) loc
|
||||
doDisplace (BOX qty ty loc) = BOX qty (doDisplace ty) loc
|
||||
doDisplace (Box val loc) = Box (doDisplace val) loc
|
||||
doDisplace (E e) = E (doDisplace e)
|
||||
doDisplace (CloT (Sub t th)) =
|
||||
CloT (Sub (doDisplace t) (map doDisplace th))
|
||||
doDisplace (DCloT (Sub t th)) =
|
||||
DCloT (Sub (doDisplace t) th)
|
||||
|
||||
doDisplaceS (S names (Y body)) = S names $ Y $ doDisplace body
|
||||
doDisplaceS (S names (N body)) = S names $ N $ doDisplace body
|
||||
|
||||
doDisplaceDS (S names (Y body)) = S names $ Y $ doDisplace body
|
||||
doDisplaceDS (S names (N body)) = S names $ N $ doDisplace body
|
||||
|
||||
namespace Elim
|
||||
doDisplace (F x u loc) = F x (k + u) loc
|
||||
doDisplace (B i loc) = B i loc
|
||||
doDisplace (App fun arg loc) = App (doDisplace fun) (doDisplace arg) loc
|
||||
doDisplace (CasePair qty pair ret body loc) =
|
||||
CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc
|
||||
doDisplace (CaseEnum qty tag ret arms loc) =
|
||||
CaseEnum qty (doDisplace tag) (doDisplaceS ret) (map doDisplace arms) loc
|
||||
doDisplace (CaseNat qty qtyIH nat ret zero succ loc) =
|
||||
CaseNat qty qtyIH (doDisplace nat) (doDisplaceS ret)
|
||||
(doDisplace zero) (doDisplaceS succ) loc
|
||||
doDisplace (CaseBox qty box ret body loc) =
|
||||
CaseBox qty (doDisplace box) (doDisplaceS ret) (doDisplaceS body) loc
|
||||
doDisplace (DApp fun arg loc) =
|
||||
DApp (doDisplace fun) arg loc
|
||||
doDisplace (Ann tm ty loc) =
|
||||
Ann (doDisplace tm) (doDisplace ty) loc
|
||||
doDisplace (Coe ty p q val loc) =
|
||||
Coe (doDisplaceDS ty) p q (doDisplace val) loc
|
||||
doDisplace (Comp ty p q val r zero one loc) =
|
||||
Comp (doDisplace ty) p q (doDisplace val) r
|
||||
(doDisplaceDS zero) (doDisplaceDS one) loc
|
||||
doDisplace (TypeCase ty ret arms def loc) =
|
||||
TypeCase (doDisplace ty) (doDisplace ret)
|
||||
(map doDisplaceS arms) (doDisplace def) loc
|
||||
doDisplace (CloE (Sub e th)) =
|
||||
CloE (Sub (doDisplace e) (map doDisplace th))
|
||||
doDisplace (DCloE (Sub e th)) =
|
||||
DCloE (Sub (doDisplace e) th)
|
||||
|
||||
|
||||
namespace Term
|
||||
export
|
||||
displace : Universe -> Term d n -> Term d n
|
||||
displace 0 t = t
|
||||
displace u t = doDisplace u t
|
||||
|
||||
namespace Elim
|
||||
export
|
||||
displace : Universe -> Elim d n -> Elim d n
|
||||
displace 0 t = t
|
||||
displace u t = doDisplace u t
|
||||
|
|
@ -373,17 +373,6 @@ parameters (defs : Definitions)
|
|||
-- has been inlined by whnf
|
||||
Elim.compare0 ctx e f
|
||||
|
||||
-- Ψ | Γ ⊢₀ e ⇒ Eq [𝑖 ⇒ A] s t
|
||||
-- -----------------------------
|
||||
-- Ψ | Γ ⊢ e @0 = s ⇒ A[0/𝑖]
|
||||
-- Ψ | Γ ⊢ e @1 = s ⇒ A[1/𝑖]
|
||||
private covering
|
||||
replaceEnd : EqContext n ->
|
||||
(e : Elim 0 n) -> Loc -> DimConst -> Loc ->
|
||||
(0 ne : NotRedex defs e) -> Equal_ (Elim 0 n)
|
||||
replaceEnd ctx e eloc p ploc ne = do
|
||||
(ty, l, r) <- expectEq defs ctx eloc !(computeElimTypeE defs ctx e)
|
||||
pure $ Ann (ends l r p) (dsub1 ty (K p ploc)) eloc
|
||||
|
||||
namespace Elim
|
||||
-- [fixme] the following code ends up repeating a lot of work in the
|
||||
|
|
@ -408,18 +397,12 @@ parameters (defs : Definitions)
|
|||
(e, f : Elim 0 n) ->
|
||||
(0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) ->
|
||||
Equal_ ()
|
||||
-- replace applied equalities with the appropriate end first
|
||||
-- (see `replaceEnd`)
|
||||
compare0' ctx (DApp e (K p ploc) loc) f ne nf =
|
||||
compare0 ctx !(replaceEnd ctx e loc p ploc $ noOr1 ne) f
|
||||
compare0' ctx e (DApp f (K q qloc) loc) ne nf =
|
||||
compare0 ctx e !(replaceEnd ctx f loc q qloc $ noOr1 nf)
|
||||
|
||||
compare0' ctx e@(F x {}) f@(F y {}) _ _ =
|
||||
unless (x == y) $ clashE e.loc ctx e f
|
||||
compare0' ctx e@(F x u _) f@(F y v _) _ _ =
|
||||
unless (x == y && u == v) $ clashE e.loc ctx e f
|
||||
compare0' ctx e@(F {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
compare0' ctx e@(B i {}) f@(B j {}) _ _ =
|
||||
compare0' ctx e@(B i _) f@(B j _) _ _ =
|
||||
unless (i == j) $ clashE e.loc ctx e f
|
||||
compare0' ctx e@(B {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
|
|
@ -523,6 +506,10 @@ parameters (defs : Definitions)
|
|||
expectEqualQ eloc epi fpi
|
||||
compare0' ctx e@(CaseBox {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
-- all dim apps replaced with ends by whnf
|
||||
compare0' _ (DApp _ (K {}) _) _ ne _ = void $ absurd $ noOr2 $ noOr2 ne
|
||||
compare0' _ _ (DApp _ (K {}) _) _ nf = void $ absurd $ noOr2 $ noOr2 nf
|
||||
|
||||
-- Ψ | Γ ⊢ s <: t : B
|
||||
-- --------------------------------
|
||||
-- Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
|
||||
|
|
@ -551,6 +538,7 @@ parameters (defs : Definitions)
|
|||
compare0' _ (Comp {r = B i _, _}) _ _ _ = absurd i
|
||||
compare0' _ _ (Comp {r = K _ _, _}) _ nf = void $ absurd $ noOr2 nf
|
||||
|
||||
-- (type case equality purely structural)
|
||||
compare0' ctx (TypeCase ty1 ret1 arms1 def1 eloc)
|
||||
(TypeCase ty2 ret2 arms2 def2 floc) ne _ =
|
||||
local_ Equal $ do
|
||||
|
|
@ -564,6 +552,11 @@ parameters (defs : Definitions)
|
|||
(lookupPrecise k arms1) (lookupPrecise k arms2) def1
|
||||
compare0' ctx e@(TypeCase {}) f _ _ = clashE e.loc ctx e f
|
||||
|
||||
-- Ψ | Γ ⊢ s <: f ⇐ A
|
||||
-- --------------------------
|
||||
-- Ψ | Γ ⊢ (s ∷ A) <: f ⇒ A
|
||||
--
|
||||
-- and vice versa
|
||||
compare0' ctx (Ann s a _) f _ _ = Term.compare0 ctx a s (E f)
|
||||
compare0' ctx e (Ann t b _) _ _ = Term.compare0 ctx b (E e) t
|
||||
compare0' ctx e@(Ann {}) f _ _ = clashE e.loc ctx e f
|
||||
|
|
|
|||
|
|
@ -124,7 +124,7 @@ fromList = fromPName . fromListP
|
|||
|
||||
export
|
||||
syntaxChars : List Char
|
||||
syntaxChars = ['(', ')', '[', ']', '{', '}', '"', '\'', ',', '.', ';']
|
||||
syntaxChars = ['(', ')', '[', ']', '{', '}', '"', '\'', ',', '.', ';', '^']
|
||||
|
||||
export
|
||||
isSymStart, isSymCont : Char -> Bool
|
||||
|
|
|
|||
|
|
@ -83,15 +83,16 @@ avoidDim ds loc x =
|
|||
fromName (const $ throw $ DimNameInTerm loc x.base) (pure . fromPName) ds x
|
||||
|
||||
private
|
||||
resolveName : Mods -> Loc -> Name -> Eff FromParserPure (Term d n)
|
||||
resolveName ns loc x =
|
||||
resolveName : Mods -> Loc -> Name -> Maybe Universe ->
|
||||
Eff FromParserPure (Term d n)
|
||||
resolveName ns loc x u =
|
||||
let here = addMods ns x in
|
||||
if isJust $ lookup here !(getAt DEFS) then
|
||||
pure $ FT here loc
|
||||
pure $ FT here (fromMaybe 0 u) loc
|
||||
else do
|
||||
let ns :< _ = ns
|
||||
| _ => throw $ TermNotInScope loc x
|
||||
resolveName ns loc x
|
||||
resolveName ns loc x u
|
||||
|
||||
export
|
||||
fromPatVar : PatVar -> BindName
|
||||
|
|
@ -107,6 +108,17 @@ fromPTagVal : PTagVal -> TagVal
|
|||
fromPTagVal (PT t _) = t
|
||||
|
||||
|
||||
private
|
||||
fromV : Context' PatVar d -> Context' PatVar n ->
|
||||
PName -> Maybe Universe -> Loc -> Eff FromParserPure (Term d n)
|
||||
fromV ds ns x u loc = fromName bound free ns x where
|
||||
bound : Var n -> Eff FromParserPure (Term d n)
|
||||
bound i = do whenJust u $ \u => throw $ DisplacedBoundVar loc x
|
||||
pure $ E $ B i loc
|
||||
free : PName -> Eff FromParserPure (Term d n)
|
||||
free x = do x <- avoidDim ds loc x
|
||||
resolveName !(getAt NS) loc x u
|
||||
|
||||
mutual
|
||||
export
|
||||
fromPTermWith : Context' PatVar d -> Context' PatVar n ->
|
||||
|
|
@ -199,9 +211,7 @@ mutual
|
|||
<*> fromPTermTScope ds ns [< b] body
|
||||
<*> pure loc
|
||||
|
||||
V x loc =>
|
||||
fromName (\i => pure $ E $ B i loc)
|
||||
(resolveName !(getAt NS) loc <=< avoidDim ds loc) ns x
|
||||
V x u loc => fromV ds ns x u loc
|
||||
|
||||
Ann s a loc =>
|
||||
map E $ Ann
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@ data Error =
|
|||
| DimNotInScope Loc PBaseName
|
||||
| QtyNotGlobal Loc Qty
|
||||
| DimNameInTerm Loc PBaseName
|
||||
| DisplacedBoundVar Loc PName
|
||||
| WrapTypeError TypeError
|
||||
| LoadError Loc String FileError
|
||||
| WrapParseError String ParseError
|
||||
|
|
@ -89,6 +90,11 @@ parameters (showContext : Bool)
|
|||
(sep ["dimension" <++> !(hl DVar $ text i),
|
||||
"used in a term context"])
|
||||
|
||||
prettyError (DisplacedBoundVar loc x) = pure $
|
||||
vappend !(prettyLoc loc)
|
||||
(sep ["local variable" <++> !(hl TVar $ text $ toDotsP x),
|
||||
"cannot be displaced"])
|
||||
|
||||
prettyError (WrapTypeError err) =
|
||||
Typing.prettyError showContext $ trimContext 2 err
|
||||
|
||||
|
|
|
|||
|
|
@ -21,7 +21,8 @@ import Derive.Prelude
|
|||
||| @ Nat nat literal
|
||||
||| @ String string literal
|
||||
||| @ Tag tag literal
|
||||
||| @ TYPE "Type" or "★" with subscript
|
||||
||| @ TYPE "Type" or "★" with ascii nat directly after
|
||||
||| @ Sup superscript or ^ number (displacement, or universe for ★)
|
||||
public export
|
||||
data Token =
|
||||
Reserved String
|
||||
|
|
@ -30,6 +31,7 @@ data Token =
|
|||
| Str String
|
||||
| Tag String
|
||||
| TYPE Nat
|
||||
| Sup Nat
|
||||
%runElab derive "Token" [Eq, Ord, Show]
|
||||
|
||||
-- token or whitespace
|
||||
|
|
@ -94,21 +96,33 @@ fromSub c = case c of
|
|||
'₀' => '0'; '₁' => '1'; '₂' => '2'; '₃' => '3'; '₄' => '4'
|
||||
'₅' => '5'; '₆' => '6'; '₇' => '7'; '₈' => '8'; '₉' => '9'; _ => c
|
||||
|
||||
private %inline
|
||||
fromSup : Char -> Char
|
||||
fromSup c = case c of
|
||||
'⁰' => '0'; '¹' => '1'; '²' => '2'; '³' => '3'; '⁴' => '4'
|
||||
'⁵' => '5'; '⁶' => '6'; '⁷' => '7'; '⁸' => '8'; '⁹' => '9'; _ => c
|
||||
|
||||
private %inline
|
||||
subToNat : String -> Nat
|
||||
subToNat = cast . pack . map fromSub . unpack
|
||||
|
||||
private %inline
|
||||
supToNat : String -> Nat
|
||||
supToNat = cast . pack . map fromSup . unpack
|
||||
|
||||
-- ★0, Type0. base ★/Type is a Reserved
|
||||
private
|
||||
universe : Tokenizer TokenW
|
||||
universe = universeWith "★" <|> universeWith "Type" where
|
||||
universeWith : String -> Tokenizer TokenW
|
||||
universeWith pfx =
|
||||
let len = length pfx in
|
||||
match (exact pfx <+> some (range '0' '9'))
|
||||
(TYPE . cast . drop len) <|>
|
||||
match (exact pfx <+> some (range '₀' '₉'))
|
||||
(TYPE . subToNat . drop len)
|
||||
match (exact pfx <+> digits) (TYPE . cast . drop len)
|
||||
|
||||
private
|
||||
sup : Tokenizer TokenW
|
||||
sup = match (some $ pred isSupDigit) (Sup . supToNat)
|
||||
<|> match (is '^' <+> digits) (Sup . cast . drop 1)
|
||||
|
||||
|
||||
private %inline
|
||||
|
|
@ -219,7 +233,7 @@ tokens = choice $
|
|||
blockComment (exact "{-") (exact "-}")] <+>
|
||||
[universe] <+> -- ★ᵢ takes precedence over bare ★
|
||||
map resTokenizer reserved <+>
|
||||
[nat, string, tag, name]
|
||||
[sup, nat, string, tag, name]
|
||||
|
||||
export
|
||||
lex : String -> Either Error (List (WithBounds Token))
|
||||
|
|
|
|||
|
|
@ -106,10 +106,14 @@ export
|
|||
strLit : Grammar True String
|
||||
strLit = terminalMatch "string literal" `(Str s) `(s)
|
||||
|
||||
||| single-token universe, like ★₀ or Type1
|
||||
||| single-token universe, like ★0 or Type1
|
||||
export
|
||||
universe1 : Grammar True Universe
|
||||
universe1 = terminalMatch "universe" `(TYPE u) `(u)
|
||||
universeTok : Grammar True Universe
|
||||
universeTok = terminalMatch "universe" `(TYPE u) `(u)
|
||||
|
||||
export
|
||||
super : Grammar True Nat
|
||||
super = terminalMatch "superscript number or '^'" `(Sup n) `(n)
|
||||
|
||||
||| possibly-qualified name
|
||||
export
|
||||
|
|
@ -134,6 +138,11 @@ qtyVal = terminalMatchN "quantity"
|
|||
[(`(Nat 0), `(Zero)), (`(Nat 1), `(One)), (`(Reserved "ω"), `(Any))]
|
||||
|
||||
|
||||
||| optional superscript number
|
||||
export
|
||||
displacement : Grammar False (Maybe Universe)
|
||||
displacement = optional super
|
||||
|
||||
||| quantity (0, 1, or ω)
|
||||
export
|
||||
qty : FileName -> Grammar True PQty
|
||||
|
|
@ -263,6 +272,10 @@ tupleTerm fname = withLoc fname $ do
|
|||
terms <- delimSep1 "(" ")" "," $ assert_total term fname
|
||||
pure $ \loc => foldr1 (\s, t => Pair s t loc) terms
|
||||
|
||||
export
|
||||
universe1 : Grammar True Universe
|
||||
universe1 = universeTok <|> res "★" *> option 0 super
|
||||
|
||||
||| argument/atomic term: single-token terms, or those with delimiters e.g.
|
||||
||| `[t]`
|
||||
export
|
||||
|
|
@ -275,7 +288,7 @@ termArg fname = withLoc fname $
|
|||
<|> Nat <$ res "ℕ"
|
||||
<|> Zero <$ res "zero"
|
||||
<|> [|fromNat nat|]
|
||||
<|> [|V qname|]
|
||||
<|> [|V qname displacement|]
|
||||
<|> const <$> tupleTerm fname
|
||||
|
||||
export
|
||||
|
|
@ -345,7 +358,10 @@ compTerm fname = withLoc fname $ do
|
|||
|
||||
export
|
||||
splitUniverseTerm : FileName -> Grammar True PTerm
|
||||
splitUniverseTerm fname = withLoc fname $ resC "★" *> mustWork [|TYPE nat|]
|
||||
splitUniverseTerm fname =
|
||||
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
|
||||
eqTerm : FileName -> Grammar True PTerm
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ namespace PTerm
|
|||
| BOX PQty PTerm Loc
|
||||
| Box PTerm Loc
|
||||
|
||||
| V PName Loc
|
||||
| V PName (Maybe Universe) Loc
|
||||
| Ann PTerm PTerm Loc
|
||||
|
||||
| Coe (PatVar, PTerm) PDim PDim PTerm Loc
|
||||
|
|
@ -124,7 +124,7 @@ Located PTerm where
|
|||
(Succ _ loc).loc = loc
|
||||
(BOX _ _ loc).loc = loc
|
||||
(Box _ loc).loc = loc
|
||||
(V _ loc).loc = loc
|
||||
(V _ _ loc).loc = loc
|
||||
(Ann _ _ loc).loc = loc
|
||||
(Coe _ _ _ _ loc).loc = loc
|
||||
(Comp _ _ _ _ _ _ _ loc).loc = loc
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ data HL
|
|||
= Delim
|
||||
| Free | TVar | TVarErr
|
||||
| Dim | DVar | DVarErr
|
||||
| Qty
|
||||
| Qty | Universe
|
||||
| Syntax
|
||||
| Tag
|
||||
%runElab derive "HL" [Eq, Ord, Show]
|
||||
|
|
@ -74,16 +74,17 @@ runPrettyWith prec flavor highlight indent act =
|
|||
|
||||
export %inline
|
||||
toSGR : HL -> List SGR
|
||||
toSGR Delim = []
|
||||
toSGR TVar = [SetForeground BrightYellow]
|
||||
toSGR TVarErr = [SetForeground BrightYellow, SetStyle SingleUnderline]
|
||||
toSGR Dim = [SetForeground BrightGreen]
|
||||
toSGR DVar = [SetForeground BrightGreen]
|
||||
toSGR DVarErr = [SetForeground BrightGreen, SetStyle SingleUnderline]
|
||||
toSGR Qty = [SetForeground BrightMagenta]
|
||||
toSGR Free = [SetForeground BrightBlue]
|
||||
toSGR Syntax = [SetForeground BrightCyan]
|
||||
toSGR Tag = [SetForeground BrightRed]
|
||||
toSGR Delim = []
|
||||
toSGR Free = [SetForeground BrightBlue]
|
||||
toSGR TVar = [SetForeground BrightYellow]
|
||||
toSGR TVarErr = [SetForeground BrightYellow, SetStyle SingleUnderline]
|
||||
toSGR Dim = [SetForeground BrightGreen]
|
||||
toSGR DVar = [SetForeground BrightGreen]
|
||||
toSGR DVarErr = [SetForeground BrightGreen, SetStyle SingleUnderline]
|
||||
toSGR Qty = [SetForeground BrightMagenta]
|
||||
toSGR Universe = [SetForeground BrightRed]
|
||||
toSGR Syntax = [SetForeground BrightCyan]
|
||||
toSGR Tag = [SetForeground BrightRed]
|
||||
|
||||
export %inline
|
||||
highlightSGR : HL -> Highlight
|
||||
|
|
@ -205,9 +206,13 @@ withPrec : PPrec -> Eff Pretty a -> Eff Pretty a
|
|||
withPrec = localAt_ PREC
|
||||
|
||||
|
||||
export
|
||||
prettyName : Name -> Doc opts
|
||||
prettyName = text . toDots
|
||||
|
||||
export
|
||||
prettyFree : {opts : _} -> Name -> Eff Pretty (Doc opts)
|
||||
prettyFree = hl Free . text . toDots
|
||||
prettyFree = hl Free . prettyName
|
||||
|
||||
export
|
||||
prettyBind' : BindName -> Doc opts
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@ module Quox.Reduce
|
|||
import Quox.No
|
||||
import Quox.Syntax
|
||||
import Quox.Definition
|
||||
import Quox.Displace
|
||||
import Quox.Typing.Context
|
||||
import Quox.Typing.Error
|
||||
import Data.SnocVect
|
||||
|
|
@ -15,15 +16,15 @@ import Control.Eff
|
|||
|
||||
-- [fixme] rename this to Whnf and the interface to CanWhnf
|
||||
public export
|
||||
WhnfM : Type -> Type
|
||||
WhnfM = Eff [NameGen, Except Error]
|
||||
Whnf : List (Type -> Type)
|
||||
Whnf = [NameGen, Except Error]
|
||||
|
||||
export
|
||||
runWhnfWith : NameSuf -> WhnfM a -> (Either Error a, NameSuf)
|
||||
runWhnfWith : NameSuf -> Eff Whnf a -> (Either Error a, NameSuf)
|
||||
runWhnfWith suf act = extract $ runStateAt GEN suf $ runExcept act
|
||||
|
||||
export
|
||||
runWhnf : WhnfM a -> Either Error a
|
||||
runWhnf : Eff Whnf a -> Either Error a
|
||||
runWhnf = fst . runWhnfWith 0
|
||||
|
||||
|
||||
|
|
@ -32,30 +33,30 @@ public export
|
|||
RedexTest tm = {d, n : Nat} -> Definitions -> tm d n -> Bool
|
||||
|
||||
public export
|
||||
interface Whnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
|
||||
interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
|
||||
where
|
||||
whnf : {d, n : Nat} -> (defs : Definitions) ->
|
||||
(ctx : WhnfContext d n) ->
|
||||
tm d n -> WhnfM (Subset (tm d n) (No . isRedex defs))
|
||||
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs))
|
||||
|
||||
public export %inline
|
||||
whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
|
||||
(defs : Definitions) -> WhnfContext d n -> tm d n -> WhnfM (tm d n)
|
||||
whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
|
||||
(defs : Definitions) -> WhnfContext d n -> tm d n -> Eff Whnf (tm d n)
|
||||
whnf0 defs ctx t = fst <$> whnf defs ctx t
|
||||
|
||||
public export
|
||||
0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> Whnf tm isRedex =>
|
||||
0 IsRedex, NotRedex : {isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
|
||||
Definitions -> Pred (tm d n)
|
||||
IsRedex defs = So . isRedex defs
|
||||
NotRedex defs = No . isRedex defs
|
||||
|
||||
public export
|
||||
0 NonRedex : (tm : TermLike) -> {isRedex : RedexTest tm} ->
|
||||
Whnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type
|
||||
CanWhnf tm isRedex => (d, n : Nat) -> (defs : Definitions) -> Type
|
||||
NonRedex tm d n defs = Subset (tm d n) (NotRedex defs)
|
||||
|
||||
public export %inline
|
||||
nred : {0 isRedex : RedexTest tm} -> (0 _ : Whnf tm isRedex) =>
|
||||
nred : {0 isRedex : RedexTest tm} -> (0 _ : CanWhnf tm isRedex) =>
|
||||
(t : tm d n) -> (0 nr : NotRedex defs t) => NonRedex tm d n defs
|
||||
nred t = Element t nr
|
||||
|
||||
|
|
@ -225,10 +226,10 @@ coeScoped ty p q loc (S names (N body)) =
|
|||
|
||||
|
||||
export covering
|
||||
Whnf Term Reduce.isRedexT
|
||||
CanWhnf Term Reduce.isRedexT
|
||||
|
||||
export covering
|
||||
Whnf Elim Reduce.isRedexE
|
||||
CanWhnf Elim Reduce.isRedexE
|
||||
|
||||
parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
|
||||
||| performs the minimum work required to recompute the type of an elim.
|
||||
|
|
@ -236,10 +237,10 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
|
|||
||| ⚠ **assumes the elim is already typechecked.** ⚠
|
||||
export covering
|
||||
computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE defs e)) =>
|
||||
WhnfM (Term d n)
|
||||
computeElimType (F {x, loc}) = do
|
||||
Eff Whnf (Term d n)
|
||||
computeElimType (F {x, u, loc}) = do
|
||||
let Just def = lookup x defs | Nothing => throw $ NotInScope loc x
|
||||
pure $ def.type
|
||||
pure $ displace u def.type
|
||||
computeElimType (B {i, _}) = pure $ ctx.tctx !! i
|
||||
computeElimType (App {fun = f, arg = s, loc}) {ne} = do
|
||||
Pi {arg, res, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne}
|
||||
|
|
@ -253,10 +254,10 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
|
|||
Eq {ty, _} <- whnf0 defs ctx =<< computeElimType f {ne = noOr1 ne}
|
||||
| t => throw $ ExpectedEq loc ctx.names t
|
||||
pure $ dsub1 ty p
|
||||
computeElimType (Ann {ty, _}) = pure ty
|
||||
computeElimType (Coe {ty, q, _}) = pure $ dsub1 ty q
|
||||
computeElimType (Comp {ty, _}) = pure ty
|
||||
computeElimType (TypeCase {ret, _}) = pure ret
|
||||
computeElimType (Ann {ty, _}) = pure ty
|
||||
|
||||
parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
|
||||
||| for π.(x : A) → B, returns (A, B);
|
||||
|
|
@ -264,7 +265,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
|
|||
||| for other intro forms error
|
||||
private covering
|
||||
tycasePi : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
|
||||
WhnfM (Term (S d) n, ScopeTerm (S d) n)
|
||||
Eff Whnf (Term (S d) n, ScopeTerm (S d) n)
|
||||
tycasePi (Pi {arg, res, _}) = pure (arg, res)
|
||||
tycasePi (E e) {tnf} = do
|
||||
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
||||
|
|
@ -282,7 +283,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
|
|||
||| for other intro forms error
|
||||
private covering
|
||||
tycaseSig : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
|
||||
WhnfM (Term (S d) n, ScopeTerm (S d) n)
|
||||
Eff Whnf (Term (S d) n, ScopeTerm (S d) n)
|
||||
tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
|
||||
tycaseSig (E e) {tnf} = do
|
||||
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
||||
|
|
@ -300,7 +301,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
|
|||
||| for other intro forms error
|
||||
private covering
|
||||
tycaseBOX : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
|
||||
WhnfM (Term (S d) n)
|
||||
Eff Whnf (Term (S d) n)
|
||||
tycaseBOX (BOX {ty, _}) = pure ty
|
||||
tycaseBOX (E e) {tnf} = do
|
||||
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
||||
|
|
@ -312,8 +313,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
|
|||
||| for other intro forms error
|
||||
private covering
|
||||
tycaseEq : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
|
||||
WhnfM (Term (S d) n, Term (S d) n, DScopeTerm (S d) n,
|
||||
Term (S d) n, Term (S d) n)
|
||||
Eff Whnf (Term (S d) n, Term (S d) n, DScopeTerm (S d) n,
|
||||
Term (S d) n, Term (S d) n)
|
||||
tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r)
|
||||
tycaseEq (E e) {tnf} = do
|
||||
ty <- computeElimType defs ctx e @{noOr2 tnf}
|
||||
|
|
@ -335,7 +336,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
|
|||
private covering
|
||||
piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
|
||||
(val, s : Term d n) -> Loc ->
|
||||
WhnfM (Subset (Elim d n) (No . isRedexE defs))
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||
piCoe sty@(S [< i] ty) p q val s loc = do
|
||||
-- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
|
||||
-- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
|
||||
|
|
@ -356,7 +357,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
|
|||
sigCoe : (qty : Qty) ->
|
||||
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
||||
(ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
|
||||
WhnfM (Subset (Elim d n) (No . isRedexE defs))
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||
sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
|
||||
-- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
|
||||
-- ⇝
|
||||
|
|
@ -382,7 +383,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
|
|||
private covering
|
||||
eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
||||
(r : Dim d) -> Loc ->
|
||||
WhnfM (Subset (Elim d n) (No . isRedexE defs))
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||
eqCoe sty@(S [< j] ty) p q val r loc = do
|
||||
-- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
|
||||
-- ⇝
|
||||
|
|
@ -400,7 +401,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
|
|||
boxCoe : (qty : Qty) ->
|
||||
(ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
|
||||
(ret : ScopeTerm d n) -> (body : ScopeTerm d n) -> Loc ->
|
||||
WhnfM (Subset (Elim d n) (No . isRedexE defs))
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||
boxCoe qty sty@(S [< i] ty) p q val ret body loc = do
|
||||
-- caseπ (coe [i ⇒ [ρ. A]] @p @q s) return z ⇒ C of { [a] ⇒ e }
|
||||
-- ⇝
|
||||
|
|
@ -420,7 +421,7 @@ reduceTypeCase : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
|
|||
(ty : Term d n) -> (u : Universe) -> (ret : Term d n) ->
|
||||
(arms : TypeCaseArms d n) -> (def : Term d n) ->
|
||||
(0 _ : So (isTyCon ty)) => Loc ->
|
||||
WhnfM (Subset (Elim d n) (No . isRedexE defs))
|
||||
Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
|
||||
reduceTypeCase defs ctx ty u ret arms def loc = case ty of
|
||||
-- (type-case ★ᵢ ∷ _ return Q of { ★ ⇒ s; ⋯ }) ⇝ s ∷ Q
|
||||
TYPE {} =>
|
||||
|
|
@ -477,12 +478,12 @@ reduceTypeCase defs ctx ty u ret arms def loc = case ty of
|
|||
|
||||
||| pushes a coercion inside a whnf-ed term
|
||||
private covering
|
||||
pushCoe : {n, d : Nat} -> (defs : Definitions) -> WhnfContext d n ->
|
||||
pushCoe : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
|
||||
BindName ->
|
||||
(ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) =>
|
||||
Dim d -> Dim d ->
|
||||
(s : Term d n) -> (0 snf : No (isRedexT defs s)) => Loc ->
|
||||
WhnfM (NonRedex Elim d n defs)
|
||||
Eff Whnf (NonRedex Elim d n defs)
|
||||
pushCoe defs ctx i ty p q s loc =
|
||||
if p == q then whnf defs ctx $ Ann s (ty // one q) loc else
|
||||
case s of
|
||||
|
|
@ -524,8 +525,7 @@ pushCoe defs ctx i ty p q s loc =
|
|||
snd' = E $ CoeT i tsnd' p q snd snd.loc
|
||||
pure $
|
||||
Element (Ann (Pair fst' snd' pairLoc)
|
||||
(Sig (tfst // one q) (tsnd // one q) sigLoc) loc)
|
||||
Ah
|
||||
(Sig (tfst // one q) (tsnd // one q) sigLoc) loc) Ah
|
||||
|
||||
-- η expand, like for Lam
|
||||
--
|
||||
|
|
@ -562,16 +562,16 @@ pushCoe defs ctx i ty p q s loc =
|
|||
|
||||
E e => pure $ Element (CoeT i ty p q (E e) e.loc) (snf `orNo` Ah)
|
||||
where
|
||||
unwrapTYPE : Term (S d) n -> WhnfM Universe
|
||||
unwrapTYPE : Term (S d) n -> Eff Whnf Universe
|
||||
unwrapTYPE (TYPE {l, _}) = pure l
|
||||
unwrapTYPE ty = throw $ ExpectedTYPE ty.loc (extendDim i ctx.names) ty
|
||||
|
||||
|
||||
export covering
|
||||
Whnf Elim Reduce.isRedexE where
|
||||
whnf defs ctx (F x loc) with (lookupElim x defs) proof eq
|
||||
_ | Just y = whnf defs ctx $ setLoc loc y
|
||||
_ | Nothing = pure $ Element (F x loc) $ rewrite eq in Ah
|
||||
CanWhnf Elim Reduce.isRedexE where
|
||||
whnf defs ctx (F x u loc) with (lookupElim x defs) proof eq
|
||||
_ | Just y = whnf defs ctx $ setLoc loc $ displace u y
|
||||
_ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
|
||||
|
||||
whnf _ _ (B i loc) = pure $ nred $ B i loc
|
||||
|
||||
|
|
@ -659,10 +659,10 @@ Whnf Elim Reduce.isRedexE where
|
|||
Right nb =>
|
||||
pure $ Element (CaseBox pi box ret body caseLoc) $ boxnf `orNo` nb
|
||||
|
||||
-- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @0 ⇝ t ∷ A‹0/𝑗›
|
||||
-- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @1 ⇝ u ∷ A‹1/𝑗›
|
||||
-- ((δ 𝑖 ⇒ s) ∷ Eq [𝑗 ⇒ A] t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
|
||||
-- (if 𝑘 is a variable)
|
||||
-- e : Eq (𝑗 ⇒ A) t u ⊢ e @0 ⇝ t ∷ A‹0/𝑗›
|
||||
-- e : Eq (𝑗 ⇒ A) t u ⊢ e @1 ⇝ u ∷ A‹1/𝑗›
|
||||
--
|
||||
-- ((δ 𝑖 ⇒ s) ∷ Eq (𝑗 ⇒ A) t u) @𝑘 ⇝ s‹𝑘/𝑖› ∷ A‹𝑘/𝑗›
|
||||
whnf defs ctx (DApp f p appLoc) = do
|
||||
Element f fnf <- whnf defs ctx f
|
||||
case nchoose $ isDLamHead f of
|
||||
|
|
@ -725,7 +725,7 @@ Whnf Elim Reduce.isRedexE where
|
|||
whnf defs ctx (DCloE (Sub el th)) = whnf defs ctx $ pushSubstsWith' th id el
|
||||
|
||||
export covering
|
||||
Whnf Term Reduce.isRedexT where
|
||||
CanWhnf Term Reduce.isRedexT where
|
||||
whnf _ _ t@(TYPE {}) = pure $ nred t
|
||||
whnf _ _ t@(Pi {}) = pure $ nred t
|
||||
whnf _ _ t@(Lam {}) = pure $ nred t
|
||||
|
|
|
|||
|
|
@ -134,8 +134,11 @@ mutual
|
|||
||| first argument `d` is dimension scope size, second `n` is term scope size
|
||||
public export
|
||||
data Elim : (d, n : Nat) -> Type where
|
||||
||| free variable
|
||||
F : (x : Name) -> (loc : Loc) -> Elim d n
|
||||
||| free variable, possibly with a displacement (see @crude, or @mugen for a
|
||||
||| more abstract and formalised take)
|
||||
|||
|
||||
||| e.g. if f : ★₀ → ★₁, then f¹ : ★₁ → ★₂
|
||||
F : (x : Name) -> (u : Universe) -> (loc : Loc) -> Elim d n
|
||||
||| bound variable
|
||||
B : (i : Var n) -> (loc : Loc) -> Elim d n
|
||||
|
||||
|
|
@ -318,8 +321,8 @@ Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
|
|||
|
||||
||| same as `F` but as a term
|
||||
public export %inline
|
||||
FT : Name -> (loc : Loc) -> Term d n
|
||||
FT x loc = E $ F x loc
|
||||
FT : Name -> Universe -> Loc -> Term d n
|
||||
FT x u loc = E $ F x u loc
|
||||
|
||||
||| abbreviation for a bound variable like `BV 4` instead of
|
||||
||| `B (VS (VS (VS (VS VZ))))`
|
||||
|
|
@ -357,7 +360,7 @@ typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
|
|||
|
||||
export
|
||||
Located (Elim d n) where
|
||||
(F _ loc).loc = loc
|
||||
(F _ _ loc).loc = loc
|
||||
(B _ loc).loc = loc
|
||||
(App _ _ loc).loc = loc
|
||||
(CasePair _ _ _ _ loc).loc = loc
|
||||
|
|
@ -404,7 +407,7 @@ Located1 f => Located (Scoped s f n) where
|
|||
|
||||
export
|
||||
Relocatable (Elim d n) where
|
||||
setLoc loc (F x _) = F x loc
|
||||
setLoc loc (F x u _) = F x u loc
|
||||
setLoc loc (B i _) = B i loc
|
||||
setLoc loc (App fun arg _) = App fun arg loc
|
||||
setLoc loc (CasePair qty pair ret body _) =
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@ import Derive.Prelude
|
|||
|
||||
export
|
||||
prettyUniverse : {opts : _} -> Universe -> Eff Pretty (Doc opts)
|
||||
prettyUniverse = hl Syntax . text . show
|
||||
prettyUniverse = hl Universe . text . show
|
||||
|
||||
|
||||
export
|
||||
|
|
@ -38,6 +38,14 @@ subscript = pack . map sub . unpack where
|
|||
'0' => '₀'; '1' => '₁'; '2' => '₂'; '3' => '₃'; '4' => '₄'
|
||||
'5' => '₅'; '6' => '₆'; '7' => '₇'; '8' => '₈'; '9' => '₉'; _ => c
|
||||
|
||||
private
|
||||
superscript : String -> String
|
||||
superscript = pack . map sup . unpack where
|
||||
sup : Char -> Char
|
||||
sup c = case c of
|
||||
'0' => '⁰'; '1' => '¹'; '2' => '²'; '3' => '³'; '4' => '⁴'
|
||||
'5' => '⁵'; '6' => '⁶'; '7' => '⁷'; '8' => '⁸'; '9' => '⁹'; _ => c
|
||||
|
||||
|
||||
private
|
||||
PiBind : Nat -> Nat -> Type
|
||||
|
|
@ -213,9 +221,6 @@ where
|
|||
go (Left p :: xs) $ assert_smaller e $ pushSubsts' f
|
||||
go xs s = (s, xs)
|
||||
|
||||
export FromString (Elim d n) where fromString s = F (fromString s) noLoc
|
||||
export FromString (Term d n) where fromString s = FT (fromString s) noLoc
|
||||
|
||||
private
|
||||
prettyDTApps : {opts : _} ->
|
||||
BContext d -> BContext n ->
|
||||
|
|
@ -368,11 +373,19 @@ where
|
|||
header cs = sep <$> traverse (\(s, xs) => header1 s (toList xs)) (toList cs)
|
||||
|
||||
|
||||
prettyDisp : {opts : _} -> Universe -> Eff Pretty (Maybe (Doc opts))
|
||||
prettyDisp 0 = pure Nothing
|
||||
prettyDisp u = map Just $ hl Universe =<<
|
||||
ifUnicode (text $ superscript $ show u) (text $ "^" ++ show u)
|
||||
|
||||
|
||||
prettyTerm dnames tnames (TYPE l _) =
|
||||
hl Syntax =<<
|
||||
case !(askAt FLAVOR) of
|
||||
Unicode => pure $ text $ "★" ++ subscript (show l)
|
||||
Ascii => prettyAppD (text "Type") [text $ show l]
|
||||
case !(askAt FLAVOR) of
|
||||
Unicode => do
|
||||
star <- hl Syntax "★"
|
||||
level <- hl Universe $ text $ superscript $ show l
|
||||
pure $ hcat [star, level]
|
||||
Ascii => [|hl Syntax "Type" <++> hl Universe (text $ show l)|]
|
||||
|
||||
prettyTerm dnames tnames (Pi qty arg res _) =
|
||||
parensIfM Outer =<< do
|
||||
|
|
@ -455,8 +468,10 @@ prettyTerm dnames tnames t0@(CloT (Sub t ph)) =
|
|||
prettyTerm dnames tnames t0@(DCloT (Sub t ph)) =
|
||||
prettyTerm dnames tnames $ assert_smaller t0 $ pushSubstsWith' ph id t
|
||||
|
||||
prettyElim dnames tnames (F x _) =
|
||||
prettyFree x
|
||||
prettyElim dnames tnames (F x u _) = do
|
||||
x <- prettyFree x
|
||||
u <- prettyDisp u
|
||||
pure $ maybe x (x <+>) u
|
||||
|
||||
prettyElim dnames tnames (B i _) =
|
||||
prettyTBind $ tnames !!! i
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ subDArgs e th = DCloE $ Sub e th
|
|||
export
|
||||
CanDSubst Elim where
|
||||
e // Shift SZ = e
|
||||
F x loc // _ = F x loc
|
||||
F x u loc // _ = F x u loc
|
||||
B i loc // _ = B i loc
|
||||
e@(DApp {}) // th = subDArgs e th
|
||||
DCloE (Sub e ph) // th = DCloE $ Sub e $ ph . th
|
||||
|
|
@ -73,7 +73,7 @@ export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
|
|||
||| - otherwise, wraps in a new closure
|
||||
export
|
||||
CanSubstSelf (Elim d) where
|
||||
F x loc // _ = F x loc
|
||||
F x u loc // _ = F x u loc
|
||||
B i loc // th = getLoc th i loc
|
||||
CloE (Sub e ph) // th = assert_total CloE $ Sub e $ ph . th
|
||||
e // th = case force th of
|
||||
|
|
@ -292,8 +292,8 @@ mutual
|
|||
|
||||
export
|
||||
PushSubsts Elim Subst.isCloE where
|
||||
pushSubstsWith th ph (F x loc) =
|
||||
nclo $ F x loc
|
||||
pushSubstsWith th ph (F x u loc) =
|
||||
nclo $ F x u loc
|
||||
pushSubstsWith th ph (B i loc) =
|
||||
let res = getLoc ph i loc in
|
||||
case nchoose $ isCloE res of
|
||||
|
|
|
|||
|
|
@ -90,8 +90,8 @@ mutual
|
|||
|
||||
private
|
||||
tightenE : OPE n1 n2 -> Elim d n2 -> Maybe (Elim d n1)
|
||||
tightenE p (F x loc) =
|
||||
pure $ F x loc
|
||||
tightenE p (F x u loc) =
|
||||
pure $ F x u loc
|
||||
tightenE p (B i loc) =
|
||||
B <$> tighten p i <*> pure loc
|
||||
tightenE p (App fun arg loc) =
|
||||
|
|
@ -204,8 +204,8 @@ mutual
|
|||
|
||||
export
|
||||
dtightenE : OPE d1 d2 -> Elim d2 n -> Maybe (Elim d1 n)
|
||||
dtightenE p (F x loc) =
|
||||
pure $ F x loc
|
||||
dtightenE p (F x u loc) =
|
||||
pure $ F x u loc
|
||||
dtightenE p (B i loc) =
|
||||
pure $ B i loc
|
||||
dtightenE p (App fun arg loc) =
|
||||
|
|
|
|||
|
|
@ -2,6 +2,7 @@ module Quox.Typechecker
|
|||
|
||||
import public Quox.Typing
|
||||
import public Quox.Equal
|
||||
import Quox.Displace
|
||||
|
||||
import Data.List
|
||||
import Data.SnocVect
|
||||
|
|
@ -107,8 +108,14 @@ mutual
|
|||
TC (CheckResult' n)
|
||||
checkC ctx sg subj ty =
|
||||
wrapErr (WhileChecking ctx sg.fst subj ty) $
|
||||
let Element subj nc = pushSubsts subj in
|
||||
check' ctx sg subj ty
|
||||
checkCNoWrap ctx sg subj ty
|
||||
|
||||
export covering %inline
|
||||
checkCNoWrap : (ctx : TyContext d n) -> SQty -> Term d n -> Term d n ->
|
||||
TC (CheckResult' n)
|
||||
checkCNoWrap ctx sg subj ty =
|
||||
let Element subj nc = pushSubsts subj in
|
||||
check' ctx sg subj ty
|
||||
|
||||
||| "Ψ | Γ ⊢₀ s ⇐ ★ᵢ"
|
||||
|||
|
||||
|
|
@ -324,14 +331,14 @@ mutual
|
|||
(subj : Elim d n) -> (0 nc : NotClo subj) =>
|
||||
TC (InferResult' d n)
|
||||
|
||||
infer' ctx sg (F x loc) = do
|
||||
infer' ctx sg (F x u loc) = do
|
||||
-- if π·x : A {≔ s} in global context
|
||||
g <- lookupFree x loc !defs
|
||||
-- if σ ≤ π
|
||||
expectCompatQ loc sg.fst g.qty.fst
|
||||
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
|
||||
let Val d = ctx.dimLen; Val n = ctx.termLen
|
||||
pure $ InfRes {type = g.type, qout = zeroFor ctx}
|
||||
pure $ InfRes {type = displace u g.type, qout = zeroFor ctx}
|
||||
|
||||
infer' ctx sg (B i _) =
|
||||
-- if x : A ∈ Γ
|
||||
|
|
|
|||
|
|
@ -69,7 +69,7 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
|
|||
namespace TyContext
|
||||
parameters (ctx : TyContext d n) (loc : Loc)
|
||||
export covering
|
||||
whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
|
||||
whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
|
||||
tm d n -> Eff fs (NonRedex tm d n defs)
|
||||
whnf tm = do
|
||||
let Val n = ctx.termLen; Val d = ctx.dimLen
|
||||
|
|
@ -115,7 +115,7 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
|
|||
namespace EqContext
|
||||
parameters (ctx : EqContext n) (loc : Loc)
|
||||
export covering
|
||||
whnf : {0 isRedex : RedexTest tm} -> Whnf tm isRedex =>
|
||||
whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
|
||||
tm 0 n -> Eff fs (NonRedex tm 0 n defs)
|
||||
whnf tm = do
|
||||
let Val n = ctx.termLen
|
||||
|
|
|
|||
|
|
@ -31,6 +31,7 @@ modules =
|
|||
Quox.Syntax.Term.Pretty,
|
||||
Quox.Syntax.Term.Subst,
|
||||
Quox.Syntax.Var,
|
||||
Quox.Displace,
|
||||
Quox.Definition,
|
||||
Quox.Reduce,
|
||||
Quox.Context,
|
||||
|
|
|
|||
19
quox.bib
19
quox.bib
|
|
@ -253,6 +253,25 @@
|
|||
date = {2023},
|
||||
}
|
||||
|
||||
@inproceedings{multimodal,
|
||||
author = {Daniel Gratzer and
|
||||
G. A. Kavvos and
|
||||
Andreas Nuyts and
|
||||
Lars Birkedal},
|
||||
editor = {Holger Hermanns and
|
||||
Lijun Zhang and
|
||||
Naoki Kobayashi and
|
||||
Dale Miller},
|
||||
title = {Multimodal Dependent Type Theory},
|
||||
booktitle = {{LICS} '20: 35th Annual {ACM/IEEE} Symposium on Logic in Computer
|
||||
Science, Saarbr{\"{u}}cken, Germany, July 8-11, 2020},
|
||||
pages = {492--506},
|
||||
publisher = {{ACM}},
|
||||
year = {2020},
|
||||
url = {https://doi.org/10.1145/3373718.3394736},
|
||||
doi = {10.1145/3373718.3394736},
|
||||
}
|
||||
|
||||
|
||||
% Misc implementation
|
||||
|
||||
|
|
|
|||
|
|
@ -63,12 +63,14 @@ comp = "comp", type line, [dim arg, dim arg],
|
|||
comp body = "{", comp branch, ";", comp branch, [";"], "}".
|
||||
comp branch = dim const, name, "⇒", term.
|
||||
|
||||
term arg = UNIVERSE
|
||||
displacement = SUPER.
|
||||
|
||||
term arg = UNIVERSE | "★", SUPER
|
||||
| "{", {BARE TAG / ","}, [","], "}"
|
||||
| TAG
|
||||
| "[", [qty, "."], term, "]"
|
||||
| "ℕ"
|
||||
| "zero"
|
||||
| NAT
|
||||
| QNAME
|
||||
| QNAME, displacement
|
||||
| "(", {term / ","}+, [","], ")".
|
||||
|
|
|
|||
|
|
@ -12,12 +12,12 @@ defGlobals : Definitions
|
|||
defGlobals = fromList
|
||||
[("A", ^mkPostulate gzero (^TYPE 0)),
|
||||
("B", ^mkPostulate gzero (^TYPE 0)),
|
||||
("a", ^mkPostulate gany (^FT "A")),
|
||||
("a'", ^mkPostulate gany (^FT "A")),
|
||||
("b", ^mkPostulate gany (^FT "B")),
|
||||
("f", ^mkPostulate gany (^Arr One (^FT "A") (^FT "A"))),
|
||||
("id", ^mkDef gany (^Arr One (^FT "A") (^FT "A")) (^LamY "x" (^BVT 0))),
|
||||
("eq-AB", ^mkPostulate gzero (^Eq0 (^TYPE 0) (^FT "A") (^FT "B"))),
|
||||
("a", ^mkPostulate gany (^FT "A" 0)),
|
||||
("a'", ^mkPostulate gany (^FT "A" 0)),
|
||||
("b", ^mkPostulate gany (^FT "B" 0)),
|
||||
("f", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "A" 0))),
|
||||
("id", ^mkDef gany (^Arr One (^FT "A" 0) (^FT "A" 0)) (^LamY "x" (^BVT 0))),
|
||||
("eq-AB", ^mkPostulate gzero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))),
|
||||
("two", ^mkDef gany (^Nat) (^Succ (^Succ (^Zero))))]
|
||||
|
||||
parameters (label : String) (act : Equal ())
|
||||
|
|
@ -87,10 +87,10 @@ tests = "equality & subtyping" :- [
|
|||
tm2 = ^Arr One (^TYPE 0) (^TYPE 1) in
|
||||
subT empty (^TYPE 2) tm1 tm2,
|
||||
testEq "1.A → B = 1.A → B" $
|
||||
let tm = ^Arr One (^FT "A") (^FT "B") in
|
||||
let tm = ^Arr One (^FT "A" 0) (^FT "B" 0) in
|
||||
equalT empty (^TYPE 0) tm tm,
|
||||
testEq "1.A → B <: 1.A → B" $
|
||||
let tm = ^Arr One (^FT "A") (^FT "B") in
|
||||
let tm = ^Arr One (^FT "A" 0) (^FT "B" 0) in
|
||||
subT empty (^TYPE 0) tm tm,
|
||||
note "incompatible quantities",
|
||||
testNeq "1.★₀ → ★₀ ≠ 0.★₀ → ★₁" $
|
||||
|
|
@ -98,52 +98,52 @@ tests = "equality & subtyping" :- [
|
|||
tm2 = ^Arr Zero (^TYPE 0) (^TYPE 1) in
|
||||
equalT empty (^TYPE 2) tm1 tm2,
|
||||
testNeq "0.A → B ≠ 1.A → B" $
|
||||
let tm1 = ^Arr Zero (^FT "A") (^FT "B")
|
||||
tm2 = ^Arr One (^FT "A") (^FT "B") in
|
||||
let tm1 = ^Arr Zero (^FT "A" 0) (^FT "B" 0)
|
||||
tm2 = ^Arr One (^FT "A" 0) (^FT "B" 0) in
|
||||
equalT empty (^TYPE 0) tm1 tm2,
|
||||
testNeq "0.A → B ≮: 1.A → B" $
|
||||
let tm1 = ^Arr Zero (^FT "A") (^FT "B")
|
||||
tm2 = ^Arr One (^FT "A") (^FT "B") in
|
||||
let tm1 = ^Arr Zero (^FT "A" 0) (^FT "B" 0)
|
||||
tm2 = ^Arr One (^FT "A" 0) (^FT "B" 0) in
|
||||
subT empty (^TYPE 0) tm1 tm2,
|
||||
testEq "0=1 ⊢ 0.A → B = 1.A → B" $
|
||||
let tm1 = ^Arr Zero (^FT "A") (^FT "B")
|
||||
tm2 = ^Arr One (^FT "A") (^FT "B") in
|
||||
let tm1 = ^Arr Zero (^FT "A" 0) (^FT "B" 0)
|
||||
tm2 = ^Arr One (^FT "A" 0) (^FT "B" 0) in
|
||||
equalT empty01 (^TYPE 0) tm1 tm2,
|
||||
todo "dependent function types"
|
||||
],
|
||||
|
||||
"lambda" :- [
|
||||
testEq "λ x ⇒ x = λ x ⇒ x" $
|
||||
equalT empty (^Arr One (^FT "A") (^FT "A"))
|
||||
equalT empty (^Arr One (^FT "A" 0) (^FT "A" 0))
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^LamY "x" (^BVT 0)),
|
||||
testEq "λ x ⇒ x <: λ x ⇒ x" $
|
||||
subT empty (^Arr One (^FT "A") (^FT "A"))
|
||||
subT empty (^Arr One (^FT "A" 0) (^FT "A" 0))
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^LamY "x" (^BVT 0)),
|
||||
testEq "λ x ⇒ x = λ y ⇒ y" $
|
||||
equalT empty (^Arr One (^FT "A") (^FT "A"))
|
||||
equalT empty (^Arr One (^FT "A" 0) (^FT "A" 0))
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^LamY "y" (^BVT 0)),
|
||||
testEq "λ x ⇒ x <: λ y ⇒ y" $
|
||||
subT empty (^Arr One (^FT "A") (^FT "A"))
|
||||
subT empty (^Arr One (^FT "A" 0) (^FT "A" 0))
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^LamY "y" (^BVT 0)),
|
||||
testNeq "λ x y ⇒ x ≠ λ x y ⇒ y" $
|
||||
equalT empty
|
||||
(^Arr One (^FT "A") (^Arr One (^FT "A") (^FT "A")))
|
||||
(^Arr One (^FT "A" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^LamY "x" (^LamY "y" (^BVT 1)))
|
||||
(^LamY "x" (^LamY "y" (^BVT 0))),
|
||||
testEq "λ x ⇒ a = λ x ⇒ a (Y vs N)" $
|
||||
equalT empty
|
||||
(^Arr Zero (^FT "B") (^FT "A"))
|
||||
(^LamY "x" (^FT "a"))
|
||||
(^LamN (^FT "a")),
|
||||
(^Arr Zero (^FT "B" 0) (^FT "A" 0))
|
||||
(^LamY "x" (^FT "a" 0))
|
||||
(^LamN (^FT "a" 0)),
|
||||
testEq "λ x ⇒ f x = f (η)" $
|
||||
equalT empty
|
||||
(^Arr One (^FT "A") (^FT "A"))
|
||||
(^LamY "x" (E $ ^App (^F "f") (^BVT 0)))
|
||||
(^FT "f")
|
||||
(^Arr One (^FT "A" 0) (^FT "A" 0))
|
||||
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
|
||||
(^FT "f" 0)
|
||||
],
|
||||
|
||||
"eq type" :- [
|
||||
|
|
@ -154,7 +154,7 @@ tests = "equality & subtyping" :- [
|
|||
{globals = fromList [("A", ^mkDef gzero (^TYPE 2) (^TYPE 1))]} $
|
||||
equalT empty (^TYPE 2)
|
||||
(^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0))
|
||||
(^Eq0 (^FT "A") (^TYPE 0) (^TYPE 0)),
|
||||
(^Eq0 (^FT "A" 0) (^TYPE 0) (^TYPE 0)),
|
||||
todo "dependent equality types"
|
||||
],
|
||||
|
||||
|
|
@ -166,94 +166,100 @@ tests = "equality & subtyping" :- [
|
|||
note "binds before ∥ are globals, after it are BVs",
|
||||
note #"refl A x is an abbreviation for "(δ i ⇒ x) ∷ (x ≡ x : A)""#,
|
||||
testEq "refl A a = refl A a" $
|
||||
equalE empty (refl (^FT "A") (^FT "a")) (refl (^FT "A") (^FT "a")),
|
||||
equalE empty
|
||||
(refl (^FT "A" 0) (^FT "a" 0))
|
||||
(refl (^FT "A" 0) (^FT "a" 0)),
|
||||
|
||||
testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q (free)"
|
||||
{globals =
|
||||
let def = ^mkPostulate gzero (^Eq0 (^FT "A") (^FT "a") (^FT "a'"))
|
||||
let def = ^mkPostulate gzero
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))
|
||||
in defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
|
||||
equalE empty (^F "p") (^F "q"),
|
||||
equalE empty (^F "p" 0) (^F "q" 0),
|
||||
|
||||
testEq "∥ x : (a ≡ a' : A), y : (a ≡ a' : A) ⊢ x = y (bound)" $
|
||||
let ty : forall n. Term 0 n := ^Eq0 (^FT "A") (^FT "a") (^FT "a'") in
|
||||
let ty : forall n. Term 0 n :=
|
||||
^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0) in
|
||||
equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
|
||||
(^BV 0) (^BV 1),
|
||||
|
||||
testEq "∥ x : (a ≡ a' : A) ∷ Type 0, y : [ditto] ⊢ x = y" $
|
||||
let ty : forall n. Term 0 n :=
|
||||
E $ ^Ann (^Eq0 (^FT "A") (^FT "a") (^FT "a'")) (^TYPE 0) in
|
||||
E $ ^Ann (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)) (^TYPE 0) in
|
||||
equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
|
||||
(^BV 0) (^BV 1),
|
||||
|
||||
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y"
|
||||
{globals = defGlobals `mergeLeft` fromList
|
||||
[("E", ^mkDef gzero (^TYPE 0)
|
||||
(^Eq0 (^FT "A") (^FT "a") (^FT "a'"))),
|
||||
("EE", ^mkDef gzero (^TYPE 0) (^FT "E"))]} $
|
||||
equalE (extendTyN [< (Any, "x", ^FT "EE"), (Any, "y", ^FT "EE")] empty)
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
|
||||
("EE", ^mkDef gzero (^TYPE 0) (^FT "E" 0))]} $
|
||||
equalE
|
||||
(extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "EE" 0)] empty)
|
||||
(^BV 0) (^BV 1),
|
||||
|
||||
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
|
||||
{globals = defGlobals `mergeLeft` fromList
|
||||
[("E", ^mkDef gzero (^TYPE 0)
|
||||
(^Eq0 (^FT "A") (^FT "a") (^FT "a'"))),
|
||||
("EE", ^mkDef gzero (^TYPE 0) (^FT "E"))]} $
|
||||
equalE (extendTyN [< (Any, "x", ^FT "EE"), (Any, "y", ^FT "E")] empty)
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
|
||||
("EE", ^mkDef gzero (^TYPE 0) (^FT "E" 0))]} $
|
||||
equalE
|
||||
(extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "E" 0)] empty)
|
||||
(^BV 0) (^BV 1),
|
||||
|
||||
testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
|
||||
{globals = defGlobals `mergeLeft` fromList
|
||||
[("E", ^mkDef gzero (^TYPE 0)
|
||||
(^Eq0 (^FT "A") (^FT "a") (^FT "a'")))]} $
|
||||
equalE (extendTyN [< (Any, "x", ^FT "E"), (Any, "y", ^FT "E")] empty)
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
|
||||
equalE (extendTyN [< (Any, "x", ^FT "E" 0), (Any, "y", ^FT "E" 0)] empty)
|
||||
(^BV 0) (^BV 1),
|
||||
|
||||
testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
|
||||
{globals = defGlobals `mergeLeft` fromList
|
||||
[("E", ^mkDef gzero (^TYPE 0)
|
||||
(^Eq0 (^FT "A") (^FT "a") (^FT "a'")))]} $
|
||||
let ty : forall n. Term 0 n := ^Sig (^FT "E") (SN $ ^FT "E") in
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
|
||||
let ty : forall n. Term 0 n := ^Sig (^FT "E" 0) (SN $ ^FT "E" 0) in
|
||||
equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
|
||||
(^BV 0) (^BV 1),
|
||||
|
||||
testEq "E ≔ a ≡ a' : A, W ≔ E × E ∥ x : W, y : E×E ⊢ x = y"
|
||||
{globals = defGlobals `mergeLeft` fromList
|
||||
[("E", ^mkDef gzero (^TYPE 0)
|
||||
(^Eq0 (^FT "A") (^FT "a") (^FT "a'"))),
|
||||
("W", ^mkDef gzero (^TYPE 0) (^And (^FT "E") (^FT "E")))]} $
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
|
||||
("W", ^mkDef gzero (^TYPE 0) (^And (^FT "E" 0) (^FT "E" 0)))]} $
|
||||
equalE
|
||||
(extendTyN [< (Any, "x", ^FT "W"),
|
||||
(Any, "y", ^And (^FT "E") (^FT "E"))] empty)
|
||||
(extendTyN [< (Any, "x", ^FT "W" 0),
|
||||
(Any, "y", ^And (^FT "E" 0) (^FT "E" 0))] empty)
|
||||
(^BV 0) (^BV 1)
|
||||
],
|
||||
|
||||
"term closure" :- [
|
||||
note "bold numbers for de bruijn indices",
|
||||
testEq "𝟎{} = 𝟎 : A" $
|
||||
equalT (extendTy Any "x" (^FT "A") empty)
|
||||
(^FT "A")
|
||||
equalT (extendTy Any "x" (^FT "A" 0) empty)
|
||||
(^FT "A" 0)
|
||||
(CloT (Sub (^BVT 0) id))
|
||||
(^BVT 0),
|
||||
testEq "𝟎{a} = a : A" $
|
||||
equalT empty (^FT "A")
|
||||
(CloT (Sub (^BVT 0) (^F "a" ::: id)))
|
||||
(^FT "a"),
|
||||
equalT empty (^FT "A" 0)
|
||||
(CloT (Sub (^BVT 0) (^F "a" 0 ::: id)))
|
||||
(^FT "a" 0),
|
||||
testEq "𝟎{a,b} = a : A" $
|
||||
equalT empty (^FT "A")
|
||||
(CloT (Sub (^BVT 0) (^F "a" ::: ^F "b" ::: id)))
|
||||
(^FT "a"),
|
||||
equalT empty (^FT "A" 0)
|
||||
(CloT (Sub (^BVT 0) (^F "a" 0 ::: ^F "b" 0 ::: id)))
|
||||
(^FT "a" 0),
|
||||
testEq "𝟏{a,b} = b : A" $
|
||||
equalT empty (^FT "A")
|
||||
(CloT (Sub (^BVT 1) (^F "a" ::: ^F "b" ::: id)))
|
||||
(^FT "b"),
|
||||
equalT empty (^FT "A" 0)
|
||||
(CloT (Sub (^BVT 1) (^F "a" 0 ::: ^F "b" 0 ::: id)))
|
||||
(^FT "b" 0),
|
||||
testEq "(λy ⇒ 𝟏){a} = λy ⇒ a : 0.B → A (N)" $
|
||||
equalT empty (^Arr Zero (^FT "B") (^FT "A"))
|
||||
(CloT (Sub (^LamN (^BVT 0)) (^F "a" ::: id)))
|
||||
(^LamN (^FT "a")),
|
||||
equalT empty (^Arr Zero (^FT "B" 0) (^FT "A" 0))
|
||||
(CloT (Sub (^LamN (^BVT 0)) (^F "a" 0 ::: id)))
|
||||
(^LamN (^FT "a" 0)),
|
||||
testEq "(λy ⇒ 𝟏){a} = λy ⇒ a : 0.B → A (Y)" $
|
||||
equalT empty (^Arr Zero (^FT "B") (^FT "A"))
|
||||
(CloT (Sub (^LamY "y" (^BVT 1)) (^F "a" ::: id)))
|
||||
(^LamY "y" (^FT "a"))
|
||||
equalT empty (^Arr Zero (^FT "B" 0) (^FT "A" 0))
|
||||
(CloT (Sub (^LamY "y" (^BVT 1)) (^F "a" 0 ::: id)))
|
||||
(^LamY "y" (^FT "a" 0))
|
||||
],
|
||||
|
||||
"term d-closure" :- [
|
||||
|
|
@ -262,9 +268,9 @@ tests = "equality & subtyping" :- [
|
|||
(^TYPE 1) (DCloT (Sub (^TYPE 0) (^K Zero ::: id))) (^TYPE 0),
|
||||
testEq "(δ i ⇒ a)‹0› = (δ i ⇒ a) : (a ≡ a : A)" $
|
||||
equalT (extendDim "𝑗" empty)
|
||||
(^Eq0 (^FT "A") (^FT "a") (^FT "a"))
|
||||
(DCloT (Sub (^DLamN (^FT "a")) (^K Zero ::: id)))
|
||||
(^DLamN (^FT "a")),
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(DCloT (Sub (^DLamN (^FT "a" 0)) (^K Zero ::: id)))
|
||||
(^DLamN (^FT "a" 0)),
|
||||
note "it is hard to think of well-typed terms with big dctxs"
|
||||
],
|
||||
|
||||
|
|
@ -274,37 +280,37 @@ tests = "equality & subtyping" :- [
|
|||
("B", ^mkDef gany (^TYPE 1) (^TYPE 0))]
|
||||
au_ba = fromList
|
||||
[("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
|
||||
("B", ^mkDef gany (^TYPE 1) (^FT "A"))]
|
||||
("B", ^mkDef gany (^TYPE 1) (^FT "A" 0))]
|
||||
in [
|
||||
testEq "A = A" $
|
||||
equalE empty (^F "A") (^F "A"),
|
||||
equalE empty (^F "A" 0) (^F "A" 0),
|
||||
testNeq "A ≠ B" $
|
||||
equalE empty (^F "A") (^F "B"),
|
||||
equalE empty (^F "A" 0) (^F "B" 0),
|
||||
testEq "0=1 ⊢ A = B" $
|
||||
equalE empty01 (^F "A") (^F "B"),
|
||||
equalE empty01 (^F "A" 0) (^F "B" 0),
|
||||
testEq "A : ★₁ ≔ ★₀ ⊢ A = (★₀ ∷ ★₁)" {globals = au_bu} $
|
||||
equalE empty (^F "A") (^Ann (^TYPE 0) (^TYPE 1)),
|
||||
equalE empty (^F "A" 0) (^Ann (^TYPE 0) (^TYPE 1)),
|
||||
testEq "A : ★₁ ≔ ★₀ ⊢ A = ★₀" {globals = au_bu} $
|
||||
equalT empty (^TYPE 1) (^FT "A") (^TYPE 0),
|
||||
equalT empty (^TYPE 1) (^FT "A" 0) (^TYPE 0),
|
||||
testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A = B" {globals = au_bu} $
|
||||
equalE empty (^F "A") (^F "B"),
|
||||
equalE empty (^F "A" 0) (^F "B" 0),
|
||||
testEq "A ≔ ★₀, B ≔ A ⊢ A = B" {globals = au_ba} $
|
||||
equalE empty (^F "A") (^F "B"),
|
||||
equalE empty (^F "A" 0) (^F "B" 0),
|
||||
testEq "A <: A" $
|
||||
subE empty (^F "A") (^F "A"),
|
||||
subE empty (^F "A" 0) (^F "A" 0),
|
||||
testNeq "A ≮: B" $
|
||||
subE empty (^F "A") (^F "B"),
|
||||
subE empty (^F "A" 0) (^F "B" 0),
|
||||
testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
|
||||
{globals = fromList [("A", ^mkDef gany (^TYPE 3) (^TYPE 0)),
|
||||
("B", ^mkDef gany (^TYPE 3) (^TYPE 2))]} $
|
||||
subE empty (^F "A") (^F "B"),
|
||||
subE empty (^F "A" 0) (^F "B" 0),
|
||||
note "(A and B in different universes)",
|
||||
testEq "A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
|
||||
{globals = fromList [("A", ^mkDef gany (^TYPE 1) (^TYPE 0)),
|
||||
("B", ^mkDef gany (^TYPE 3) (^TYPE 2))]} $
|
||||
subE empty (^F "A") (^F "B"),
|
||||
subE empty (^F "A" 0) (^F "B" 0),
|
||||
testEq "0=1 ⊢ A <: B" $
|
||||
subE empty01 (^F "A") (^F "B")
|
||||
subE empty01 (^F "A" 0) (^F "B" 0)
|
||||
],
|
||||
|
||||
"bound var" :- [
|
||||
|
|
@ -326,110 +332,115 @@ tests = "equality & subtyping" :- [
|
|||
|
||||
"application" :- [
|
||||
testEq "f a = f a" $
|
||||
equalE empty (^App (^F "f") (^FT "a")) (^App (^F "f") (^FT "a")),
|
||||
equalE empty (^App (^F "f" 0) (^FT "a" 0)) (^App (^F "f" 0) (^FT "a" 0)),
|
||||
testEq "f a <: f a" $
|
||||
subE empty (^App (^F "f") (^FT "a")) (^App (^F "f") (^FT "a")),
|
||||
subE empty (^App (^F "f" 0) (^FT "a" 0)) (^App (^F "f" 0) (^FT "a" 0)),
|
||||
testEq "(λ x ⇒ x ∷ 1.A → A) a = ((a ∷ A) ∷ A) (β)" $
|
||||
equalE empty
|
||||
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A") (^FT "A")))
|
||||
(^FT "a"))
|
||||
(^Ann (E $ ^Ann (^FT "a") (^FT "A")) (^FT "A")),
|
||||
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^FT "a" 0))
|
||||
(^Ann (E $ ^Ann (^FT "a" 0) (^FT "A" 0)) (^FT "A" 0)),
|
||||
testEq "(λ x ⇒ x ∷ A ⊸ A) a = a (βυ)" $
|
||||
equalE empty
|
||||
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A") (^FT "A")))
|
||||
(^FT "a"))
|
||||
(^F "a"),
|
||||
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^FT "a" 0))
|
||||
(^F "a" 0),
|
||||
testEq "((λ g ⇒ g a) ∷ 1.(1.A → A) → A) f = ((λ y ⇒ f y) ∷ 1.A → A) a # β↘↙" $
|
||||
let a = ^FT "A"; a2a = ^Arr One a a; aa2a = ^Arr One a2a a in
|
||||
let a = ^FT "A" 0; a2a = ^Arr One a a; aa2a = ^Arr One a2a a in
|
||||
equalE empty
|
||||
(^App (^Ann (^LamY "g" (E $ ^App (^BV 0) (^FT "a"))) aa2a) (^FT "f"))
|
||||
(^App (^Ann (^LamY "y" (E $ ^App (^F "f") (^BVT 0))) a2a) (^FT "a")),
|
||||
(^App (^Ann (^LamY "g" (E $ ^App (^BV 0) (^FT "a" 0))) aa2a)
|
||||
(^FT "f" 0))
|
||||
(^App (^Ann (^LamY "y" (E $ ^App (^F "f" 0) (^BVT 0))) a2a)
|
||||
(^FT "a" 0)),
|
||||
testEq "((λ x ⇒ x) ∷ 1.A → A) a <: a" $
|
||||
subE empty
|
||||
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A") (^FT "A")))
|
||||
(^FT "a"))
|
||||
(^F "a"),
|
||||
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^FT "a" 0))
|
||||
(^F "a" 0),
|
||||
note "id : A ⊸ A ≔ λ x ⇒ x",
|
||||
testEq "id a = a" $ equalE empty (^App (^F "id") (^FT "a")) (^F "a"),
|
||||
testEq "id a <: a" $ subE empty (^App (^F "id") (^FT "a")) (^F "a")
|
||||
testEq "id a = a" $ equalE empty (^App (^F "id" 0) (^FT "a" 0)) (^F "a" 0),
|
||||
testEq "id a <: a" $ subE empty (^App (^F "id" 0) (^FT "a" 0)) (^F "a" 0)
|
||||
],
|
||||
|
||||
"dim application" :- [
|
||||
testEq "eq-AB @0 = eq-AB @0" $
|
||||
equalE empty
|
||||
(^DApp (^F "eq-AB") (^K Zero))
|
||||
(^DApp (^F "eq-AB") (^K Zero)),
|
||||
(^DApp (^F "eq-AB" 0) (^K Zero))
|
||||
(^DApp (^F "eq-AB" 0) (^K Zero)),
|
||||
testNeq "eq-AB @0 ≠ eq-AB @1" $
|
||||
equalE empty
|
||||
(^DApp (^F "eq-AB") (^K Zero))
|
||||
(^DApp (^F "eq-AB") (^K One)),
|
||||
(^DApp (^F "eq-AB" 0) (^K Zero))
|
||||
(^DApp (^F "eq-AB" 0) (^K One)),
|
||||
testEq "𝑖 | ⊢ eq-AB @𝑖 = eq-AB @𝑖" $
|
||||
equalE
|
||||
(extendDim "𝑖" empty)
|
||||
(^DApp (^F "eq-AB") (^BV 0))
|
||||
(^DApp (^F "eq-AB") (^BV 0)),
|
||||
(^DApp (^F "eq-AB" 0) (^BV 0))
|
||||
(^DApp (^F "eq-AB" 0) (^BV 0)),
|
||||
testNeq "𝑖 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
|
||||
equalE (extendDim "𝑖" empty)
|
||||
(^DApp (^F "eq-AB") (^BV 0))
|
||||
(^DApp (^F "eq-AB") (^K Zero)),
|
||||
(^DApp (^F "eq-AB" 0) (^BV 0))
|
||||
(^DApp (^F "eq-AB" 0) (^K Zero)),
|
||||
testEq "𝑖, 𝑖=0 | ⊢ eq-AB @𝑖 = eq-AB @0" $
|
||||
equalE (eqDim (^BV 0) (^K Zero) $ extendDim "𝑖" empty)
|
||||
(^DApp (^F "eq-AB") (^BV 0))
|
||||
(^DApp (^F "eq-AB") (^K Zero)),
|
||||
(^DApp (^F "eq-AB" 0) (^BV 0))
|
||||
(^DApp (^F "eq-AB" 0) (^K Zero)),
|
||||
testNeq "𝑖, 𝑖=1 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
|
||||
equalE (eqDim (^BV 0) (^K One) $ extendDim "𝑖" empty)
|
||||
(^DApp (^F "eq-AB") (^BV 0))
|
||||
(^DApp (^F "eq-AB") (^K Zero)),
|
||||
(^DApp (^F "eq-AB" 0) (^BV 0))
|
||||
(^DApp (^F "eq-AB" 0) (^K Zero)),
|
||||
testNeq "𝑖, 𝑗 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $
|
||||
equalE (extendDim "𝑗" $ extendDim "𝑖" empty)
|
||||
(^DApp (^F "eq-AB") (^BV 1))
|
||||
(^DApp (^F "eq-AB") (^BV 0)),
|
||||
(^DApp (^F "eq-AB" 0) (^BV 1))
|
||||
(^DApp (^F "eq-AB" 0) (^BV 0)),
|
||||
testEq "𝑖, 𝑗, 𝑖=𝑗 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
|
||||
equalE (eqDim (^BV 0) (^BV 1) $ extendDim "𝑗" $ extendDim "𝑖" empty)
|
||||
(^DApp (^F "eq-AB") (^BV 1))
|
||||
(^DApp (^F "eq-AB") (^BV 0)),
|
||||
(^DApp (^F "eq-AB" 0) (^BV 1))
|
||||
(^DApp (^F "eq-AB" 0) (^BV 0)),
|
||||
testEq "𝑖, 𝑗, 𝑖=0, 𝑗=0 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
|
||||
equalE
|
||||
(eqDim (^BV 0) (^K Zero) $ eqDim (^BV 1) (^K Zero) $
|
||||
extendDim "𝑗" $ extendDim "𝑖" empty)
|
||||
(^DApp (^F "eq-AB") (^BV 1))
|
||||
(^DApp (^F "eq-AB") (^BV 0)),
|
||||
(^DApp (^F "eq-AB" 0) (^BV 1))
|
||||
(^DApp (^F "eq-AB" 0) (^BV 0)),
|
||||
testEq "0=1 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
|
||||
equalE (extendDim "𝑗" $ extendDim "𝑖" empty01)
|
||||
(^DApp (^F "eq-AB") (^BV 1))
|
||||
(^DApp (^F "eq-AB") (^BV 0)),
|
||||
(^DApp (^F "eq-AB" 0) (^BV 1))
|
||||
(^DApp (^F "eq-AB" 0) (^BV 0)),
|
||||
testEq "eq-AB @0 = A" $
|
||||
equalE empty (^DApp (^F "eq-AB") (^K Zero)) (^F "A"),
|
||||
equalE empty (^DApp (^F "eq-AB" 0) (^K Zero)) (^F "A" 0),
|
||||
testEq "eq-AB @1 = B" $
|
||||
equalE empty (^DApp (^F "eq-AB") (^K One)) (^F "B"),
|
||||
equalE empty (^DApp (^F "eq-AB" 0) (^K One)) (^F "B" 0),
|
||||
testEq "((δ i ⇒ a) ∷ a ≡ a : A) @0 = a" $
|
||||
equalE empty
|
||||
(^DApp (^Ann (^DLamN (^FT "a")) (^Eq0 (^FT "A") (^FT "a") (^FT "a")))
|
||||
(^DApp (^Ann (^DLamN (^FT "a" 0))
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0)))
|
||||
(^K Zero))
|
||||
(^F "a"),
|
||||
(^F "a" 0),
|
||||
testEq "((δ i ⇒ a) ∷ a ≡ a : A) @0 = ((δ i ⇒ a) ∷ a ≡ a : A) @1" $
|
||||
equalE empty
|
||||
(^DApp (^Ann (^DLamN (^FT "a")) (^Eq0 (^FT "A") (^FT "a") (^FT "a")))
|
||||
(^DApp (^Ann (^DLamN (^FT "a" 0))
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0)))
|
||||
(^K Zero))
|
||||
(^DApp (^Ann (^DLamN (^FT "a")) (^Eq0 (^FT "A") (^FT "a") (^FT "a")))
|
||||
(^DApp (^Ann (^DLamN (^FT "a" 0))
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0)))
|
||||
(^K One))
|
||||
],
|
||||
|
||||
"annotation" :- [
|
||||
testEq "(λ x ⇒ f x) ∷ 1.A → A = f ∷ 1.A → A" $
|
||||
equalE empty
|
||||
(^Ann (^LamY "x" (E $ ^App (^F "f") (^BVT 0)))
|
||||
(^Arr One (^FT "A") (^FT "A")))
|
||||
(^Ann (^FT "f") (^Arr One (^FT "A") (^FT "A"))),
|
||||
(^Ann (^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
|
||||
(^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^Ann (^FT "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0))),
|
||||
testEq "f ∷ 1.A → A = f" $
|
||||
equalE empty
|
||||
(^Ann (^FT "f") (^Arr One (^FT "A") (^FT "A")))
|
||||
(^F "f"),
|
||||
(^Ann (^FT "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^F "f" 0),
|
||||
testEq "(λ x ⇒ f x) ∷ 1.A → A = f" $
|
||||
equalE empty
|
||||
(^Ann (^LamY "x" (E $ ^App (^F "f") (^BVT 0)))
|
||||
(^Arr One (^FT "A") (^FT "A")))
|
||||
(^F "f")
|
||||
(^Ann (^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
|
||||
(^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^F "f" 0)
|
||||
],
|
||||
|
||||
"natural type" :- [
|
||||
|
|
@ -443,9 +454,9 @@ tests = "equality & subtyping" :- [
|
|||
"natural numbers" :- [
|
||||
testEq "0 = 0" $ equalT empty (^Nat) (^Zero) (^Zero),
|
||||
testEq "succ two = succ two" $
|
||||
equalT empty (^Nat) (^Succ (^FT "two")) (^Succ (^FT "two")),
|
||||
equalT empty (^Nat) (^Succ (^FT "two" 0)) (^Succ (^FT "two" 0)),
|
||||
testNeq "succ two ≠ two" $
|
||||
equalT empty (^Nat) (^Succ (^FT "two")) (^FT "two"),
|
||||
equalT empty (^Nat) (^Succ (^FT "two" 0)) (^FT "two" 0),
|
||||
testNeq "0 ≠ 1" $
|
||||
equalT empty (^Nat) (^Zero) (^Succ (^Zero)),
|
||||
testEq "0=1 ⊢ 0 = 1" $
|
||||
|
|
@ -517,10 +528,10 @@ tests = "equality & subtyping" :- [
|
|||
"elim closure" :- [
|
||||
note "bold numbers for de bruijn indices",
|
||||
testEq "𝟎{a} = a" $
|
||||
equalE empty (CloE (Sub (^BV 0) (^F "a" ::: id))) (^F "a"),
|
||||
equalE empty (CloE (Sub (^BV 0) (^F "a" 0 ::: id))) (^F "a" 0),
|
||||
testEq "𝟏{a} = 𝟎" $
|
||||
equalE (extendTy Any "x" (^FT "A") empty)
|
||||
(CloE (Sub (^BV 1) (^F "a" ::: id))) (^BV 0)
|
||||
equalE (extendTy Any "x" (^FT "A" 0) empty)
|
||||
(CloE (Sub (^BV 1) (^F "a" 0 ::: id))) (^BV 0)
|
||||
],
|
||||
|
||||
"elim d-closure" :- [
|
||||
|
|
@ -528,40 +539,40 @@ tests = "equality & subtyping" :- [
|
|||
note "0·eq-AB : (A ≡ B : ★₀)",
|
||||
testEq "(eq-AB @𝟎)‹0› = eq-AB @0" $
|
||||
equalE empty
|
||||
(DCloE (Sub (^DApp (^F "eq-AB") (^BV 0)) (^K Zero ::: id)))
|
||||
(^DApp (^F "eq-AB") (^K Zero)),
|
||||
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^K Zero ::: id)))
|
||||
(^DApp (^F "eq-AB" 0) (^K Zero)),
|
||||
testEq "(eq-AB @𝟎)‹0› = A" $
|
||||
equalE empty
|
||||
(DCloE (Sub (^DApp (^F "eq-AB") (^BV 0)) (^K Zero ::: id)))
|
||||
(^F "A"),
|
||||
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^K Zero ::: id)))
|
||||
(^F "A" 0),
|
||||
testEq "(eq-AB @𝟎)‹1› = B" $
|
||||
equalE empty
|
||||
(DCloE (Sub (^DApp (^F "eq-AB") (^BV 0)) (^K One ::: id)))
|
||||
(^F "B"),
|
||||
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^K One ::: id)))
|
||||
(^F "B" 0),
|
||||
testNeq "(eq-AB @𝟎)‹1› ≠ A" $
|
||||
equalE empty
|
||||
(DCloE (Sub (^DApp (^F "eq-AB") (^BV 0)) (^K One ::: id)))
|
||||
(^F "A"),
|
||||
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^K One ::: id)))
|
||||
(^F "A" 0),
|
||||
testEq "(eq-AB @𝟎)‹𝟎,0› = (eq-AB 𝟎)" $
|
||||
equalE (extendDim "𝑖" empty)
|
||||
(DCloE (Sub (^DApp (^F "eq-AB") (^BV 0)) (^BV 0 ::: ^K Zero ::: id)))
|
||||
(^DApp (^F "eq-AB") (^BV 0)),
|
||||
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^BV 0 ::: ^K Zero ::: id)))
|
||||
(^DApp (^F "eq-AB" 0) (^BV 0)),
|
||||
testNeq "(eq-AB 𝟎)‹0› ≠ (eq-AB 0)" $
|
||||
equalE (extendDim "𝑖" empty)
|
||||
(DCloE (Sub (^DApp (^F "eq-AB") (^BV 0)) (^BV 0 ::: ^K Zero ::: id)))
|
||||
(^DApp (^F "eq-AB") (^K Zero)),
|
||||
(DCloE (Sub (^DApp (^F "eq-AB" 0) (^BV 0)) (^BV 0 ::: ^K Zero ::: id)))
|
||||
(^DApp (^F "eq-AB" 0) (^K Zero)),
|
||||
testEq "𝟎‹0› = 𝟎 # term and dim vars distinct" $
|
||||
equalE
|
||||
(extendTy Any "x" (^FT "A") empty)
|
||||
(extendTy Any "x" (^FT "A" 0) empty)
|
||||
(DCloE (Sub (^BV 0) (^K Zero ::: id))) (^BV 0),
|
||||
testEq "a‹0› = a" $
|
||||
equalE empty
|
||||
(DCloE (Sub (^F "a") (^K Zero ::: id))) (^F "a"),
|
||||
(DCloE (Sub (^F "a" 0) (^K Zero ::: id))) (^F "a" 0),
|
||||
testEq "(f a)‹0› = f‹0› a‹0›" $
|
||||
let th = ^K Zero ::: id in
|
||||
equalE empty
|
||||
(DCloE (Sub (^App (^F "f") (^FT "a")) th))
|
||||
(^App (DCloE (Sub (^F "f") th)) (DCloT (Sub (^FT "a") th)))
|
||||
(DCloE (Sub (^App (^F "f" 0) (^FT "a" 0)) th))
|
||||
(^App (DCloE (Sub (^F "f" 0) th)) (DCloT (Sub (^FT "a" 0) th)))
|
||||
],
|
||||
|
||||
"clashes" :- [
|
||||
|
|
|
|||
|
|
@ -93,7 +93,7 @@ tests = "PTerm → Term" :- [
|
|||
note "dim ctx: [𝑖, 𝑗]; term ctx: [A, x, y, z]",
|
||||
parseMatch term fromPTerm "x" `(E $ B (VS $ VS VZ) _),
|
||||
parseFails term fromPTerm "𝑖",
|
||||
parseMatch term fromPTerm "f" `(E $ F "f" _),
|
||||
parseMatch term fromPTerm "f" `(E $ F "f" {}),
|
||||
parseMatch term fromPTerm "λ w ⇒ w"
|
||||
`(Lam (S _ $ Y $ E $ B VZ _) _),
|
||||
parseMatch term fromPTerm "λ w ⇒ x"
|
||||
|
|
@ -103,9 +103,10 @@ tests = "PTerm → Term" :- [
|
|||
parseMatch term fromPTerm "λ a b ⇒ f a b"
|
||||
`(Lam (S _ $ Y $
|
||||
Lam (S _ $ Y $
|
||||
E $ App (App (F "f" _) (E $ B (VS VZ) _) _) (E $ B VZ _) _) _) _),
|
||||
E $ App (App (F "f" {}) (E $ B (VS VZ) _) _) (E $ B VZ _) _) _) _),
|
||||
parseMatch term fromPTerm "f @𝑖" $
|
||||
`(E $ DApp (F "f" _) (B (VS VZ) _) _)
|
||||
`(E $ DApp (F "f" {}) (B (VS VZ) _) _),
|
||||
parseFails term fromPTerm "λ x ⇒ x¹"
|
||||
],
|
||||
|
||||
todo "everything else"
|
||||
|
|
|
|||
|
|
@ -74,10 +74,9 @@ tests = "lexer" :- [
|
|||
lexes "uhh??!?!?!?" [Name "uhh??!?!?!?"],
|
||||
|
||||
todo "check for reserved words in a qname",
|
||||
{-
|
||||
skip $
|
||||
lexes "abc.fun.def"
|
||||
[Name "abc", Reserved ".", Reserved "λ", Reserved ".", Name "def"],
|
||||
-}
|
||||
|
||||
lexes "+" [Name "+"],
|
||||
lexes "*" [Name "*"],
|
||||
|
|
@ -110,6 +109,10 @@ tests = "lexer" :- [
|
|||
lexes "a'" [Name "a'"],
|
||||
lexes "+'" [Name "+'"],
|
||||
|
||||
lexes "a₁" [Name "a₁"],
|
||||
lexes "a⁰" [Name "a", Sup 0],
|
||||
lexes "a^0" [Name "a", Sup 0],
|
||||
|
||||
lexes "0.x" [Nat 0, Reserved ".", Name "x"],
|
||||
lexes "1.x" [Nat 1, Reserved ".", Name "x"],
|
||||
lexes "ω.x" [Reserved "ω", Reserved ".", Name "x"],
|
||||
|
|
@ -119,7 +122,7 @@ tests = "lexer" :- [
|
|||
"syntax characters" :- [
|
||||
lexes "()" [Reserved "(", Reserved ")"],
|
||||
lexes "(a)" [Reserved "(", Name "a", Reserved ")"],
|
||||
lexes "(^)" [Reserved "(", Name "^", Reserved ")"],
|
||||
lexFail "(^)",
|
||||
lexes "{a,b}"
|
||||
[Reserved "{", Name "a", Reserved ",", Name "b", Reserved "}"],
|
||||
lexes "{+,-}"
|
||||
|
|
@ -151,10 +154,10 @@ tests = "lexer" :- [
|
|||
|
||||
"universes" :- [
|
||||
lexes "Type0" [TYPE 0],
|
||||
lexes "Type₀" [TYPE 0],
|
||||
lexes "Type⁰" [Reserved "★", Sup 0],
|
||||
lexes "Type9999999" [TYPE 9999999],
|
||||
lexes "★₀" [TYPE 0],
|
||||
lexes "★₆₉" [TYPE 69],
|
||||
lexes "★⁰" [Reserved "★", Sup 0],
|
||||
lexes "★⁶⁹" [Reserved "★", Sup 69],
|
||||
lexes "★4" [TYPE 4],
|
||||
lexes "Type" [Reserved "★"],
|
||||
lexes "★" [Reserved "★"]
|
||||
|
|
|
|||
|
|
@ -72,7 +72,7 @@ tests = "parser" :- [
|
|||
"dimensions" :- [
|
||||
parseMatch dim "0" `(K Zero _),
|
||||
parseMatch dim "1" `(K One _),
|
||||
parseMatch dim "𝑖" `(V "𝑖" _),
|
||||
parseMatch dim "𝑖" `(V "𝑖" {}),
|
||||
parseFails dim "M.x",
|
||||
parseFails dim "_"
|
||||
],
|
||||
|
|
@ -105,154 +105,156 @@ tests = "parser" :- [
|
|||
parseMatch term #" '"a b c" "# `(Tag "a b c" _),
|
||||
note "application to two arguments",
|
||||
parseMatch term #" 'a b c "#
|
||||
`(App (App (Tag "a" _) (V "b" _) _) (V "c" _) _)
|
||||
`(App (App (Tag "a" _) (V "b" {}) _) (V "c" {}) _)
|
||||
],
|
||||
|
||||
"universes" :- [
|
||||
parseMatch term "★₀" `(TYPE 0 _),
|
||||
parseMatch term "★⁰" `(TYPE 0 _),
|
||||
parseMatch term "★1" `(TYPE 1 _),
|
||||
parseMatch term "★ 2" `(TYPE 2 _),
|
||||
parseMatch term "Type₃" `(TYPE 3 _),
|
||||
parseMatch term "Type³" `(TYPE 3 _),
|
||||
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" :- [
|
||||
parseMatch term "f"
|
||||
`(V "f" _),
|
||||
`(V "f" {}),
|
||||
parseMatch term "f.x.y"
|
||||
`(V (MakePName [< "f", "x"] "y") _),
|
||||
`(V (MakePName [< "f", "x"] "y") {}),
|
||||
parseMatch term "f x"
|
||||
`(App (V "f" _) (V "x" _) _),
|
||||
`(App (V "f" {}) (V "x" {}) _),
|
||||
parseMatch term "f x y"
|
||||
`(App (App (V "f" _) (V "x" _) _) (V "y" _) _),
|
||||
`(App (App (V "f" {}) (V "x" {}) _) (V "y" {}) _),
|
||||
parseMatch term "(f x) y"
|
||||
`(App (App (V "f" _) (V "x" _) _) (V "y" _) _),
|
||||
`(App (App (V "f" {}) (V "x" {}) _) (V "y" {}) _),
|
||||
parseMatch term "f (g x)"
|
||||
`(App (V "f" _) (App (V "g" _) (V "x" _) _) _),
|
||||
`(App (V "f" {}) (App (V "g" {}) (V "x" {}) _) _),
|
||||
parseMatch term "f (g x) y"
|
||||
`(App (App (V "f" _) (App (V "g" _) (V "x" _) _) _) (V "y" _) _),
|
||||
`(App (App (V "f" {}) (App (V "g" {}) (V "x" {}) _) _) (V "y" {}) _),
|
||||
parseMatch term "f @p"
|
||||
`(DApp (V "f" _) (V "p" _) _),
|
||||
`(DApp (V "f" {}) (V "p" {}) _),
|
||||
parseMatch term "f x @p y"
|
||||
`(App (DApp (App (V "f" _) (V "x" _) _) (V "p" _) _) (V "y" _) _)
|
||||
`(App (DApp (App (V "f" {}) (V "x" {}) _) (V "p" {}) _) (V "y" {}) _)
|
||||
],
|
||||
|
||||
"annotations" :- [
|
||||
parseMatch term "f :: A"
|
||||
`(Ann (V "f" _) (V "A" _) _),
|
||||
`(Ann (V "f" {}) (V "A" {}) _),
|
||||
parseMatch term "f ∷ A"
|
||||
`(Ann (V "f" _) (V "A" _) _),
|
||||
`(Ann (V "f" {}) (V "A" {}) _),
|
||||
parseMatch term "f x y ∷ A B C"
|
||||
`(Ann (App (App (V "f" _) (V "x" _) _) (V "y" _) _)
|
||||
(App (App (V "A" _) (V "B" _) _) (V "C" _) _) _),
|
||||
`(Ann (App (App (V "f" {}) (V "x" {}) _) (V "y" {}) _)
|
||||
(App (App (V "A" {}) (V "B" {}) _) (V "C" {}) _) _),
|
||||
parseMatch term "Type 0 ∷ Type 1 ∷ Type 2"
|
||||
`(Ann (TYPE 0 _) (Ann (TYPE 1 _) (TYPE 2 _) _) _)
|
||||
],
|
||||
|
||||
"binders" :- [
|
||||
parseMatch term "1.(x : A) → B x"
|
||||
`(Pi (PQ One _) (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _),
|
||||
`(Pi (PQ One _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
|
||||
parseMatch term "1.(x : A) -> B x"
|
||||
`(Pi (PQ One _) (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _),
|
||||
`(Pi (PQ One _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
|
||||
parseMatch term "ω.(x : A) → B x"
|
||||
`(Pi (PQ Any _) (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _),
|
||||
`(Pi (PQ Any _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
|
||||
parseMatch term "#.(x : A) -> B x"
|
||||
`(Pi (PQ Any _) (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _),
|
||||
`(Pi (PQ Any _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
|
||||
parseMatch term "1.(x y : A) -> B x"
|
||||
`(Pi (PQ One _) (PV "x" _) (V "A" _)
|
||||
(Pi (PQ One _) (PV "y" _) (V "A" _)
|
||||
(App (V "B" _) (V "x" _) _) _) _),
|
||||
`(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 "1.A → B"
|
||||
`(Pi (PQ One _) (Unused _) (V "A" _) (V "B" _) _),
|
||||
`(Pi (PQ One _) (Unused _) (V "A" {}) (V "B" {}) _),
|
||||
parseMatch term "1.(List A) → List B"
|
||||
`(Pi (PQ One _) (Unused _)
|
||||
(App (V "List" _) (V "A" _) _)
|
||||
(App (V "List" _) (V "B" _) _) _),
|
||||
(App (V "List" {}) (V "A" {}) _)
|
||||
(App (V "List" {}) (V "B" {}) _) _),
|
||||
parseMatch term "0.★⁰ → ★⁰"
|
||||
`(Pi (PQ Zero _) (Unused _) (TYPE 0 _) (TYPE 0 _) _),
|
||||
parseFails term "1.List A → List B",
|
||||
parseMatch term "(x : A) × B x"
|
||||
`(Sig (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _),
|
||||
`(Sig (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
|
||||
parseMatch term "(x : A) ** B x"
|
||||
`(Sig (PV "x" _) (V "A" _) (App (V "B" _) (V "x" _) _) _),
|
||||
`(Sig (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
|
||||
parseMatch term "(x y : A) × B" $
|
||||
`(Sig (PV "x" _) (V "A" _) (Sig (PV "y" _) (V "A" _) (V "B" _) _) _),
|
||||
`(Sig (PV "x" _) (V "A" {}) (Sig (PV "y" _) (V "A" {}) (V "B" {}) _) _),
|
||||
parseFails term "1.(x : A) × B x",
|
||||
parseMatch term "A × B"
|
||||
`(Sig (Unused _) (V "A" _) (V "B" _) _),
|
||||
`(Sig (Unused _) (V "A" {}) (V "B" {}) _),
|
||||
parseMatch term "A ** B"
|
||||
`(Sig (Unused _) (V "A" _) (V "B" _) _),
|
||||
`(Sig (Unused _) (V "A" {}) (V "B" {}) _),
|
||||
parseMatch term "A × B × C" $
|
||||
`(Sig (Unused _) (V "A" _) (Sig (Unused _) (V "B" _) (V "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" {}) _)
|
||||
],
|
||||
|
||||
"lambdas" :- [
|
||||
parseMatch term "λ x ⇒ x"
|
||||
`(Lam (PV "x" _) (V "x" _) _),
|
||||
`(Lam (PV "x" _) (V "x" {}) _),
|
||||
parseMatch term "fun x => x"
|
||||
`(Lam (PV "x" _) (V "x" _) _),
|
||||
`(Lam (PV "x" _) (V "x" {}) _),
|
||||
parseMatch term "δ i ⇒ x @i"
|
||||
`(DLam (PV "i" _) (DApp (V "x" _) (V "i" _) _) _),
|
||||
`(DLam (PV "i" _) (DApp (V "x" {}) (V "i" {}) _) _),
|
||||
parseMatch term "dfun i => x @i"
|
||||
`(DLam (PV "i" _) (DApp (V "x" _) (V "i" _) _) _),
|
||||
`(DLam (PV "i" _) (DApp (V "x" {}) (V "i" {}) _) _),
|
||||
parseMatch term "λ x y z ⇒ x z y"
|
||||
`(Lam (PV "x" _)
|
||||
(Lam (PV "y" _)
|
||||
(Lam (PV "z" _)
|
||||
(App (App (V "x" _) (V "z" _) _) (V "y" _) _) _) _) _)
|
||||
(App (App (V "x" {}) (V "z" {}) _) (V "y" {}) _) _) _) _)
|
||||
],
|
||||
|
||||
"pairs" :- [
|
||||
parseMatch term "(x, y)"
|
||||
`(Pair (V "x" _) (V "y" _) _),
|
||||
`(Pair (V "x" {}) (V "y" {}) _),
|
||||
parseMatch term "(x, y, z)"
|
||||
`(Pair (V "x" _) (Pair (V "y" _) (V "z" _) _) _),
|
||||
`(Pair (V "x" {}) (Pair (V "y" {}) (V "z" {}) _) _),
|
||||
parseMatch term "((x, y), z)"
|
||||
`(Pair (Pair (V "x" _) (V "y" _) _) (V "z" _) _),
|
||||
`(Pair (Pair (V "x" {}) (V "y" {}) _) (V "z" {}) _),
|
||||
parseMatch term "(f x, g @y)"
|
||||
`(Pair (App (V "f" _) (V "x" _) _) (DApp (V "g" _) (V "y" _) _) _),
|
||||
`(Pair (App (V "f" {}) (V "x" {}) _) (DApp (V "g" {}) (V "y" {}) _) _),
|
||||
parseMatch term "((x : A) × B, 0.(x : C) → D)"
|
||||
`(Pair (Sig (PV "x" _) (V "A" _) (V "B" _) _)
|
||||
(Pi (PQ Zero _) (PV "x" _) (V "C" _) (V "D" _) _) _),
|
||||
`(Pair (Sig (PV "x" _) (V "A" {}) (V "B" {}) _)
|
||||
(Pi (PQ Zero _) (PV "x" _) (V "C" {}) (V "D" {}) _) _),
|
||||
parseMatch term "(λ x ⇒ x, δ i ⇒ e @i)"
|
||||
`(Pair (Lam (PV "x" _) (V "x" _) _)
|
||||
(DLam (PV "i" _) (DApp (V "e" _) (V "i" _) _) _) _),
|
||||
parseMatch term "(x,)" `(V "x" _), -- i GUESS
|
||||
`(Pair (Lam (PV "x" _) (V "x" {}) _)
|
||||
(DLam (PV "i" _) (DApp (V "e" {}) (V "i" {}) _) _) _),
|
||||
parseMatch term "(x,)" `(V "x" {}), -- i GUESS
|
||||
parseFails term "(,y)",
|
||||
parseFails term "(x,,y)"
|
||||
],
|
||||
|
||||
"equality type" :- [
|
||||
parseMatch term "Eq (i ⇒ A) s t"
|
||||
`(Eq (PV "i" _, V "A" _) (V "s" _) (V "t" _) _),
|
||||
`(Eq (PV "i" _, V "A" {}) (V "s" {}) (V "t" {}) _),
|
||||
parseMatch term "Eq (i ⇒ A (B @i)) (f x) (g y)"
|
||||
`(Eq (PV "i" _, App (V "A" _) (DApp (V "B" _) (V "i" _) _) _)
|
||||
(App (V "f" _) (V "x" _) _)
|
||||
(App (V "g" _) (V "y" _) _) _),
|
||||
`(Eq (PV "i" _, App (V "A" {}) (DApp (V "B" {}) (V "i" {}) _) _)
|
||||
(App (V "f" {}) (V "x" {}) _)
|
||||
(App (V "g" {}) (V "y" {}) _) _),
|
||||
parseMatch term "Eq A s t"
|
||||
`(Eq (Unused _, V "A" _) (V "s" _) (V "t" _) _),
|
||||
`(Eq (Unused _, V "A" {}) (V "s" {}) (V "t" {}) _),
|
||||
parseMatch term "s ≡ t : A"
|
||||
`(Eq (Unused _, V "A" _) (V "s" _) (V "t" _) _),
|
||||
`(Eq (Unused _, V "A" {}) (V "s" {}) (V "t" {}) _),
|
||||
parseMatch term "s == t : A"
|
||||
`(Eq (Unused _, V "A" _) (V "s" _) (V "t" _) _),
|
||||
`(Eq (Unused _, V "A" {}) (V "s" {}) (V "t" {}) _),
|
||||
parseMatch term "f x ≡ g y : A B"
|
||||
`(Eq (Unused _, App (V "A" _) (V "B" _) _)
|
||||
(App (V "f" _) (V "x" _) _)
|
||||
(App (V "g" _) (V "y" _) _) _),
|
||||
parseMatch term "(A × B) ≡ (A' × B') : ★₁"
|
||||
`(Eq (Unused _, App (V "A" {}) (V "B" {}) _)
|
||||
(App (V "f" {}) (V "x" {}) _)
|
||||
(App (V "g" {}) (V "y" {}) _) _),
|
||||
parseMatch term "(A × B) ≡ (A' × B') : ★¹"
|
||||
`(Eq (Unused _, TYPE 1 _)
|
||||
(Sig (Unused _) (V "A" _) (V "B" _) _)
|
||||
(Sig (Unused _) (V "A'" _) (V "B'" _) _) _),
|
||||
note "A × (B ≡ A' × B' : ★₁)",
|
||||
parseMatch term "A × B ≡ A' × B' : ★₁"
|
||||
`(Sig (Unused _) (V "A" _)
|
||||
(Sig (Unused _) (V "A" {}) (V "B" {}) _)
|
||||
(Sig (Unused _) (V "A'" {}) (V "B'" {}) _) _),
|
||||
note "A × (B ≡ A' × B' : ★¹)",
|
||||
parseMatch term "A × B ≡ A' × B' : ★¹"
|
||||
`(Sig (Unused _) (V "A" {})
|
||||
(Eq (Unused _, TYPE 1 _)
|
||||
(V "B" _) (Sig (Unused _) (V "A'" _) (V "B'" _) _) _) _),
|
||||
(V "B" {}) (Sig (Unused _) (V "A'" {}) (V "B'" {}) _) _) _),
|
||||
parseFails term "Eq",
|
||||
parseFails term "Eq s t",
|
||||
parseFails term "s ≡ t",
|
||||
|
|
@ -263,7 +265,7 @@ tests = "parser" :- [
|
|||
parseMatch term "ℕ" `(Nat _),
|
||||
parseMatch term "Nat" `(Nat _),
|
||||
parseMatch term "zero" `(Zero _),
|
||||
parseMatch term "succ n" `(Succ (V "n" _) _),
|
||||
parseMatch term "succ n" `(Succ (V "n" {}) _),
|
||||
parseMatch term "3"
|
||||
`(Succ (Succ (Succ (Zero _) _) _) _),
|
||||
parseMatch term "succ (succ 1)"
|
||||
|
|
@ -278,7 +280,7 @@ tests = "parser" :- [
|
|||
parseMatch term "[ω. ℕ × ℕ]"
|
||||
`(BOX (PQ Any _) (Sig (Unused _) (Nat _) (Nat _) _) _),
|
||||
parseMatch term "[a]"
|
||||
`(Box (V "a" _) _),
|
||||
`(Box (V "a" {}) _),
|
||||
parseMatch term "[0]"
|
||||
`(Box (Zero _) _),
|
||||
parseMatch term "[1]"
|
||||
|
|
@ -287,28 +289,28 @@ tests = "parser" :- [
|
|||
|
||||
"coe" :- [
|
||||
parseMatch term "coe A @p @q x"
|
||||
`(Coe (Unused _, V "A" _) (V "p" _) (V "q" _) (V "x" _) _),
|
||||
`(Coe (Unused _, V "A" {}) (V "p" {}) (V "q" {}) (V "x" {}) _),
|
||||
parseMatch term "coe (i ⇒ A) @p @q x"
|
||||
`(Coe (PV "i" _, V "A" _) (V "p" _) (V "q" _) (V "x" _) _),
|
||||
`(Coe (PV "i" _, V "A" {}) (V "p" {}) (V "q" {}) (V "x" {}) _),
|
||||
parseMatch term "coe A x"
|
||||
`(Coe (Unused _, V "A" _) (K Zero _) (K One _) (V "x" _) _),
|
||||
`(Coe (Unused _, V "A" {}) (K Zero _) (K One _) (V "x" {}) _),
|
||||
parseFails term "coe A @p @q",
|
||||
parseFails term "coe (i ⇒ A) @p q x"
|
||||
],
|
||||
|
||||
"comp" :- [
|
||||
parseMatch term "comp A @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }"
|
||||
`(Comp (Unused _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _)
|
||||
(PV "𝑗" _, V "s₀" _) (PV "𝑘" _, V "s₁" _) _),
|
||||
`(Comp (Unused _, V "A" {}) (V "p" {}) (V "q" {}) (V "s" {}) (V "r" {})
|
||||
(PV "𝑗" _, V "s₀" {}) (PV "𝑘" _, V "s₁" {}) _),
|
||||
parseMatch term "comp (𝑖 ⇒ A) @p @q s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }"
|
||||
`(Comp (PV "𝑖" _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _)
|
||||
(PV "𝑗" _, V "s₀" _) (PV "𝑘" _, V "s₁" _) _),
|
||||
`(Comp (PV "𝑖" _, V "A" {}) (V "p" {}) (V "q" {}) (V "s" {}) (V "r" {})
|
||||
(PV "𝑗" _, V "s₀" {}) (PV "𝑘" _, V "s₁" {}) _),
|
||||
parseMatch term "comp A @p @q s @r { 1 𝑗 ⇒ s₀; 0 𝑘 ⇒ s₁; }"
|
||||
`(Comp (Unused _, V "A" _) (V "p" _) (V "q" _) (V "s" _) (V "r" _)
|
||||
(PV "𝑘" _, V "s₁" _) (PV "𝑗" _, V "s₀" _) _),
|
||||
`(Comp (Unused _, V "A" {}) (V "p" {}) (V "q" {}) (V "s" {}) (V "r" {})
|
||||
(PV "𝑘" _, V "s₁" {}) (PV "𝑗" _, V "s₀" {}) _),
|
||||
parseMatch term "comp A s @r { 0 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁ }"
|
||||
`(Comp (Unused _, V "A" _) (K Zero _) (K One _) (V "s" _) (V "r" _)
|
||||
(PV "𝑗" _, V "s₀" _) (PV "𝑘" _, V "s₁" _) _),
|
||||
`(Comp (Unused _, V "A" {}) (K Zero _) (K One _) (V "s" {}) (V "r" {})
|
||||
(PV "𝑗" _, V "s₀" {}) (PV "𝑘" _, V "s₁" {}) _),
|
||||
parseFails term "comp A @p @q s @r { 1 𝑗 ⇒ s₀; 1 𝑘 ⇒ s₁; }",
|
||||
parseFails term "comp A @p @q s @r { 0 𝑗 ⇒ s₀ }",
|
||||
parseFails term "comp A @p @q s @r { }"
|
||||
|
|
@ -317,39 +319,39 @@ tests = "parser" :- [
|
|||
"case" :- [
|
||||
parseMatch term
|
||||
"case1 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" _) _)
|
||||
`(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" _) _) _) _),
|
||||
(App (V "r" {}) (V "l" {}) _) _) _),
|
||||
parseMatch term
|
||||
"case1 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" _) _)
|
||||
`(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" _) _) _) _),
|
||||
(App (V "r" {}) (V "l" {}) _) _) _),
|
||||
parseMatch term
|
||||
"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" _) _)
|
||||
`(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" _) _) _) _),
|
||||
(App (V "r" {}) (V "l" {}) _) _) _),
|
||||
parseMatch term
|
||||
"case1 t return A of { 'x ⇒ p; 'y ⇒ q; 'z ⇒ r }"
|
||||
`(Case (PQ One _) (V "t" _)
|
||||
(Unused _, V "A" _)
|
||||
(CaseEnum [(PT "x" _, V "p" _),
|
||||
(PT "y" _, V "q" _),
|
||||
(PT "z" _, V "r" _)] _) _),
|
||||
`(Case (PQ One _) (V "t" {})
|
||||
(Unused _, V "A" {})
|
||||
(CaseEnum [(PT "x" _, V "p" {}),
|
||||
(PT "y" _, V "q" {}),
|
||||
(PT "z" _, V "r" {})] _) _),
|
||||
parseMatch term "caseω t return A of {}"
|
||||
`(Case (PQ Any _) (V "t" _) (Unused _, V "A" _) (CaseEnum [] _) _),
|
||||
`(Case (PQ Any _) (V "t" {}) (Unused _, V "A" {}) (CaseEnum [] _) _),
|
||||
parseMatch term "case# t return A of {}"
|
||||
`(Case (PQ Any _) (V "t" _) (Unused _, V "A" _) (CaseEnum [] _) _),
|
||||
`(Case (PQ Any _) (V "t" {}) (Unused _, V "A" {}) (CaseEnum [] _) _),
|
||||
parseMatch term "caseω n return A of { 0 ⇒ a; succ n' ⇒ b }"
|
||||
`(Case (PQ Any _) (V "n" _) (Unused _, V "A" _)
|
||||
(CaseNat (V "a" _) (PV "n'" _, PQ Zero _, Unused _, V "b" _) _) _),
|
||||
`(Case (PQ Any _) (V "n" {}) (Unused _, V "A" {})
|
||||
(CaseNat (V "a" {}) (PV "n'" _, PQ Zero _, Unused _, V "b" {}) _) _),
|
||||
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" _) _) _),
|
||||
`(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 }"
|
||||
],
|
||||
|
|
@ -371,18 +373,18 @@ tests = "parser" :- [
|
|||
`(MkPDef (PQ Any _) "x"
|
||||
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
|
||||
(Pair (Tag "a" _) (Tag "b" _) _) _),
|
||||
parseMatch definition "def0 A : ★₀ = {a, b, c}"
|
||||
parseMatch definition "def0 A : ★⁰ = {a, b, c}"
|
||||
`(MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _)
|
||||
(Enum ["a", "b", "c"] _) _)
|
||||
],
|
||||
|
||||
"top level" :- [
|
||||
parseMatch input "def0 A : ★₀ = {}; def0 B : ★₁ = A;"
|
||||
parseMatch input "def0 A : ★⁰ = {}; def0 B : ★¹ = A;"
|
||||
`([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _,
|
||||
PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" _) _]),
|
||||
parseMatch input "def0 A : ★₀ = {} def0 B : ★₁ = A" $
|
||||
PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _]),
|
||||
parseMatch input "def0 A : ★⁰ = {} def0 B : ★¹ = A" $
|
||||
`([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _,
|
||||
PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" _) _]),
|
||||
PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _]),
|
||||
note "empty input",
|
||||
parsesAs input "" [],
|
||||
parseFails input ";;;;;;;;;;;;;;;;;;;;;;;;;;",
|
||||
|
|
@ -401,10 +403,10 @@ tests = "parser" :- [
|
|||
[PDef $ MkPDef (PQ Any _) "x" Nothing
|
||||
(Ann (Tag "t" _) (Enum ["t"] _) _) _] _,
|
||||
PD $ PDef $ MkPDef (PQ Any _) "y" Nothing
|
||||
(V (MakePName [< "a"] "x") _) _]),
|
||||
(V (MakePName [< "a"] "x") {}) _]),
|
||||
parseMatch input #" load "a.quox"; def b = a.b "#
|
||||
`([PLoad "a.quox" _,
|
||||
PD $ PDef $ MkPDef (PQ Any _) "b" Nothing
|
||||
(V (MakePName [< "a"] "b") _) _])
|
||||
(V (MakePName [< "a"] "b") {}) _])
|
||||
]
|
||||
]
|
||||
|
|
|
|||
|
|
@ -35,36 +35,40 @@ export
|
|||
tests : Test
|
||||
tests = "pretty printing terms" :- [
|
||||
"free vars" :- [
|
||||
testPrettyE1 [<] [<] (^F "x") "x",
|
||||
testPrettyE1 [<] [<] (^F (MakeName [< "A", "B", "C"] "x")) "A.B.C.x"
|
||||
testPrettyE1 [<] [<] (^F "x" 0) "x",
|
||||
testPrettyE [<] [<] (^F "x" 1) "x¹" "x^1",
|
||||
testPrettyE1 [<] [<] (^F (MakeName [< "A", "B", "C"] "x") 0) "A.B.C.x",
|
||||
testPrettyE [<] [<] (^F (MakeName [< "A", "B", "C"] "x") 2)
|
||||
"A.B.C.x²"
|
||||
"A.B.C.x^2"
|
||||
],
|
||||
|
||||
"bound vars" :- [
|
||||
testPrettyE1 [< "𝑖", "𝑗"] [< "x", "y"] (^BV 0) "y",
|
||||
testPrettyE1 [< "𝑖", "𝑗"] [< "x", "y"] (^BV 1) "x",
|
||||
testPrettyE1 [< "𝑖", "𝑗"] [< "x", "y"]
|
||||
(^DApp (^F "eq") (^BV 1))
|
||||
(^DApp (^F "eq" 0) (^BV 1))
|
||||
"eq @𝑖",
|
||||
testPrettyE1 [< "𝑖", "𝑗"] [< "x", "y"]
|
||||
(^DApp (^DApp (^F "eq") (^BV 1)) (^BV 0))
|
||||
(^DApp (^DApp (^F "eq" 0) (^BV 1)) (^BV 0))
|
||||
"eq @𝑖 @𝑗"
|
||||
],
|
||||
|
||||
"applications" :- [
|
||||
testPrettyE1 [<] [<]
|
||||
(^App (^F "f") (^FT "x"))
|
||||
(^App (^F "f" 0) (^FT "x" 0))
|
||||
"f x",
|
||||
testPrettyE1 [<] [<]
|
||||
(^App (^App (^F "f") (^FT "x")) (^FT "y"))
|
||||
(^App (^App (^F "f" 0) (^FT "x" 0)) (^FT "y" 0))
|
||||
"f x y",
|
||||
testPrettyE1 [<] [<]
|
||||
(^DApp (^F "f") (^K Zero))
|
||||
(^DApp (^F "f" 0) (^K Zero))
|
||||
"f @0",
|
||||
testPrettyE1 [<] [<]
|
||||
(^DApp (^App (^F "f") (^FT "x")) (^K Zero))
|
||||
(^DApp (^App (^F "f" 0) (^FT "x" 0)) (^K Zero))
|
||||
"f x @0",
|
||||
testPrettyE1 [<] [<]
|
||||
(^App (^DApp (^F "g") (^K One)) (^FT "y"))
|
||||
(^App (^DApp (^F "g" 0) (^K One)) (^FT "y" 0))
|
||||
"g @1 y"
|
||||
],
|
||||
|
||||
|
|
@ -74,7 +78,7 @@ tests = "pretty printing terms" :- [
|
|||
"λ x ⇒ x"
|
||||
"fun x => x",
|
||||
testPrettyT [<] [<]
|
||||
(^LamN (^FT "a"))
|
||||
(^LamN (^FT "a" 0))
|
||||
"λ _ ⇒ a"
|
||||
"fun _ => a",
|
||||
testPrettyT [<] [< "y"]
|
||||
|
|
@ -87,11 +91,11 @@ tests = "pretty printing terms" :- [
|
|||
"λ x y f ⇒ f x y"
|
||||
"fun x y f => f x y",
|
||||
testPrettyT [<] [<]
|
||||
(^DLam (SN (^FT "a")))
|
||||
(^DLam (SN (^FT "a" 0)))
|
||||
"δ _ ⇒ a"
|
||||
"dfun _ => a",
|
||||
testPrettyT [<] [<]
|
||||
(^DLamY "i" (^FT "x"))
|
||||
(^DLamY "i" (^FT "x" 0))
|
||||
"δ i ⇒ x"
|
||||
"dfun i => x",
|
||||
testPrettyT [<] [<]
|
||||
|
|
@ -101,51 +105,51 @@ tests = "pretty printing terms" :- [
|
|||
],
|
||||
|
||||
"type universes" :- [
|
||||
testPrettyT [<] [<] (^TYPE 0) "★₀" "Type 0",
|
||||
testPrettyT [<] [<] (^TYPE 100) "★₁₀₀" "Type 100"
|
||||
testPrettyT [<] [<] (^TYPE 0) "★⁰" "Type 0",
|
||||
testPrettyT [<] [<] (^TYPE 100) "★¹⁰⁰" "Type 100"
|
||||
],
|
||||
|
||||
"function types" :- [
|
||||
testPrettyT [<] [<]
|
||||
(^Arr One (^FT "A") (^FT "B"))
|
||||
(^Arr One (^FT "A" 0) (^FT "B" 0))
|
||||
"1.A → B"
|
||||
"1.A -> B",
|
||||
testPrettyT [<] [<]
|
||||
(^PiY One "x" (^FT "A") (E $ ^App (^F "B") (^BVT 0)))
|
||||
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "B" 0) (^BVT 0)))
|
||||
"1.(x : A) → B x"
|
||||
"1.(x : A) -> B x",
|
||||
testPrettyT [<] [<]
|
||||
(^PiY Zero "A" (^TYPE 0) (^Arr Any (^BVT 0) (^BVT 0)))
|
||||
"0.(A : ★₀) → ω.A → A"
|
||||
"0.(A : ★⁰) → ω.A → A"
|
||||
"0.(A : Type 0) -> #.A -> A",
|
||||
testPrettyT [<] [<]
|
||||
(^Arr Any (^Arr Any (^FT "A") (^FT "A")) (^FT "A"))
|
||||
(^Arr Any (^Arr Any (^FT "A" 0) (^FT "A" 0)) (^FT "A" 0))
|
||||
"ω.(ω.A → A) → A"
|
||||
"#.(#.A -> A) -> A",
|
||||
testPrettyT [<] [<]
|
||||
(^Arr Any (^FT "A") (^Arr Any (^FT "A") (^FT "A")))
|
||||
(^Arr Any (^FT "A" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)))
|
||||
"ω.A → ω.A → A"
|
||||
"#.A -> #.A -> A",
|
||||
testPrettyT [<] [<]
|
||||
(^PiY Zero "P" (^Arr Zero (^FT "A") (^TYPE 0))
|
||||
(E $ ^App (^BV 0) (^FT "a")))
|
||||
"0.(P : 0.A → ★₀) → P a"
|
||||
(^PiY Zero "P" (^Arr Zero (^FT "A" 0) (^TYPE 0))
|
||||
(E $ ^App (^BV 0) (^FT "a" 0)))
|
||||
"0.(P : 0.A → ★⁰) → P a"
|
||||
"0.(P : 0.A -> Type 0) -> P a"
|
||||
],
|
||||
|
||||
"pair types" :- [
|
||||
testPrettyT [<] [<]
|
||||
(^And (^FT "A") (^FT "B"))
|
||||
(^And (^FT "A" 0) (^FT "B" 0))
|
||||
"A × B"
|
||||
"A ** B",
|
||||
testPrettyT [<] [<]
|
||||
(^SigY "x" (^FT "A") (E $ ^App (^F "B") (^BVT 0)))
|
||||
(^SigY "x" (^FT "A" 0) (E $ ^App (^F "B" 0) (^BVT 0)))
|
||||
"(x : A) × B x"
|
||||
"(x : A) ** B x",
|
||||
testPrettyT [<] [<]
|
||||
(^SigY "x" (^FT "A")
|
||||
(^SigY "y" (E $ ^App (^F "B") (^BVT 0))
|
||||
(E $ ^App (^App (^F "C") (^BVT 1)) (^BVT 0))))
|
||||
(^SigY "x" (^FT "A" 0)
|
||||
(^SigY "y" (E $ ^App (^F "B" 0) (^BVT 0))
|
||||
(E $ ^App (^App (^F "C" 0) (^BVT 1)) (^BVT 0))))
|
||||
"(x : A) × (y : B x) × C x y"
|
||||
"(x : A) ** (y : B x) ** C x y",
|
||||
todo "non-dependent, left and right nested"
|
||||
|
|
@ -153,16 +157,16 @@ tests = "pretty printing terms" :- [
|
|||
|
||||
"pairs" :- [
|
||||
testPrettyT1 [<] [<]
|
||||
(^Pair (^FT "A") (^FT "B"))
|
||||
(^Pair (^FT "A" 0) (^FT "B" 0))
|
||||
"(A, B)",
|
||||
testPrettyT1 [<] [<]
|
||||
(^Pair (^FT "A") (^Pair (^FT "B") (^FT "C")))
|
||||
(^Pair (^FT "A" 0) (^Pair (^FT "B" 0) (^FT "C" 0)))
|
||||
"(A, B, C)",
|
||||
testPrettyT1 [<] [<]
|
||||
(^Pair (^Pair (^FT "A") (^FT "B")) (^FT "C"))
|
||||
(^Pair (^Pair (^FT "A" 0) (^FT "B" 0)) (^FT "C" 0))
|
||||
"((A, B), C)",
|
||||
testPrettyT [<] [<]
|
||||
(^Pair (^LamY "x" (^BVT 0)) (^Arr One (^FT "B₁") (^FT "B₂")))
|
||||
(^Pair (^LamY "x" (^BVT 0)) (^Arr One (^FT "B₁" 0) (^FT "B₂" 0)))
|
||||
"(λ x ⇒ x, 1.B₁ → B₂)"
|
||||
"(fun x => x, 1.B₁ -> B₂)"
|
||||
],
|
||||
|
|
@ -188,12 +192,12 @@ tests = "pretty printing terms" :- [
|
|||
|
||||
"case" :- [
|
||||
testPrettyE [<] [<]
|
||||
(^CasePair One (^F "a") (SN $ ^TYPE 1) (SN $ ^TYPE 0))
|
||||
"case1 a return ★₁ of { (_, _) ⇒ ★₀ }"
|
||||
(^CasePair One (^F "a" 0) (SN $ ^TYPE 1) (SN $ ^TYPE 0))
|
||||
"case1 a return ★¹ of { (_, _) ⇒ ★⁰ }"
|
||||
"case1 a return Type 1 of { (_, _) => Type 0 }",
|
||||
testPrettyT [<] [<]
|
||||
(^LamY "u" (E $
|
||||
^CaseEnum One (^F "u")
|
||||
^CaseEnum One (^F "u" 0)
|
||||
(SY [< "x"] $ ^Eq0 (^enum ["tt"]) (^BVT 0) (^Tag "tt"))
|
||||
(fromList [("tt", ^DLamN (^Tag "tt"))])))
|
||||
"λ u ⇒ case1 u return x ⇒ x ≡ 'tt : {tt} of { 'tt ⇒ δ _ ⇒ 'tt }"
|
||||
|
|
@ -205,32 +209,32 @@ tests = "pretty printing terms" :- [
|
|||
|
||||
"type-case" :- [
|
||||
testPrettyE [<] [<]
|
||||
{label = "type-case ℕ ∷ ★₀ return ★₀ of { ⋯ }"}
|
||||
{label = "type-case ℕ ∷ ★⁰ return ★⁰ of { ⋯ }"}
|
||||
(^TypeCase (^Ann (^Nat) (^TYPE 0)) (^TYPE 0) empty (^Nat))
|
||||
"type-case ℕ ∷ ★₀ return ★₀ of { _ ⇒ ℕ }"
|
||||
"type-case ℕ ∷ ★⁰ return ★⁰ of { _ ⇒ ℕ }"
|
||||
"type-case Nat :: Type 0 return Type 0 of { _ => Nat }"
|
||||
],
|
||||
|
||||
"annotations" :- [
|
||||
testPrettyE [<] [<]
|
||||
(^Ann (^FT "a") (^FT "A"))
|
||||
(^Ann (^FT "a" 0) (^FT "A" 0))
|
||||
"a ∷ A"
|
||||
"a :: A",
|
||||
testPrettyE [<] [<]
|
||||
(^Ann (^FT "a") (E $ ^Ann (^FT "A") (^FT "𝐀")))
|
||||
(^Ann (^FT "a" 0) (E $ ^Ann (^FT "A" 0) (^FT "𝐀" 0)))
|
||||
"a ∷ A ∷ 𝐀"
|
||||
"a :: A :: 𝐀",
|
||||
testPrettyE [<] [<]
|
||||
(^Ann (E $ ^Ann (^FT "α") (^FT "a")) (^FT "A"))
|
||||
(^Ann (E $ ^Ann (^FT "α" 0) (^FT "a" 0)) (^FT "A" 0))
|
||||
"(α ∷ a) ∷ A"
|
||||
"(α :: a) :: A",
|
||||
testPrettyE [<] [<]
|
||||
(^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A") (^FT "A")))
|
||||
(^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
"(λ x ⇒ x) ∷ 1.A → A"
|
||||
"(fun x => x) :: 1.A -> A",
|
||||
testPrettyE [<] [<]
|
||||
(^Ann (^Arr One (^FT "A") (^FT "A")) (^TYPE 7))
|
||||
"(1.A → A) ∷ ★₇"
|
||||
(^Ann (^Arr One (^FT "A" 0) (^FT "A" 0)) (^TYPE 7))
|
||||
"(1.A → A) ∷ ★⁷"
|
||||
"(1.A -> A) :: Type 7"
|
||||
]
|
||||
]
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ import Control.Eff
|
|||
%hide Pretty.App
|
||||
|
||||
|
||||
parameters {0 isRedex : RedexTest tm} {auto _ : Whnf tm isRedex} {d, n : Nat}
|
||||
parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
|
||||
{auto _ : (Eq (tm d n), Show (tm d n))}
|
||||
{default empty defs : Definitions}
|
||||
private
|
||||
|
|
@ -35,42 +35,42 @@ tests = "whnf" :- [
|
|||
"head constructors" :- [
|
||||
testNoStep "★₀" empty $ ^TYPE 0,
|
||||
testNoStep "1.A → B" empty $
|
||||
^Arr One (^FT "A") (^FT "B"),
|
||||
^Arr One (^FT "A" 0) (^FT "B" 0),
|
||||
testNoStep "(x: A) ⊸ B x" empty $
|
||||
^PiY One "x" (^FT "A") (E $ ^App (^F "B") (^BVT 0)),
|
||||
^PiY One "x" (^FT "A" 0) (E $ ^App (^F "B" 0) (^BVT 0)),
|
||||
testNoStep "λ x ⇒ x" empty $
|
||||
^LamY "x" (^BVT 0),
|
||||
testNoStep "f a" empty $
|
||||
E $ ^App (^F "f") (^FT "a")
|
||||
E $ ^App (^F "f" 0) (^FT "a" 0)
|
||||
],
|
||||
|
||||
"neutrals" :- [
|
||||
testNoStep "x" (ctx [< ("A", ^Nat)]) $ ^BV 0,
|
||||
testNoStep "a" empty $ ^F "a",
|
||||
testNoStep "f a" empty $ ^App (^F "f") (^FT "a"),
|
||||
testNoStep "a" empty $ ^F "a" 0,
|
||||
testNoStep "f a" empty $ ^App (^F "f" 0) (^FT "a" 0),
|
||||
testNoStep "★₀ ∷ ★₁" empty $ ^Ann (^TYPE 0) (^TYPE 1)
|
||||
],
|
||||
|
||||
"redexes" :- [
|
||||
testWhnf "a ∷ A" empty
|
||||
(^Ann (^FT "a") (^FT "A"))
|
||||
(^F "a"),
|
||||
(^Ann (^FT "a" 0) (^FT "A" 0))
|
||||
(^F "a" 0),
|
||||
testWhnf "★₁ ∷ ★₃" empty
|
||||
(E $ ^Ann (^TYPE 1) (^TYPE 3))
|
||||
(^TYPE 1),
|
||||
testWhnf "(λ x ⇒ x ∷ 1.A → A) a" empty
|
||||
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A") (^FT "A")))
|
||||
(^FT "a"))
|
||||
(^F "a")
|
||||
(^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^FT "a" 0))
|
||||
(^F "a" 0)
|
||||
],
|
||||
|
||||
"definitions" :- [
|
||||
testWhnf "a (transparent)" empty
|
||||
{defs = fromList [("a", ^mkDef gzero (^TYPE 1) (^TYPE 0))]}
|
||||
(^F "a") (^Ann (^TYPE 0) (^TYPE 1)),
|
||||
(^F "a" 0) (^Ann (^TYPE 0) (^TYPE 1)),
|
||||
testNoStep "a (opaque)" empty
|
||||
{defs = fromList [("a", ^mkPostulate gzero (^TYPE 1))]}
|
||||
(^F "a")
|
||||
(^F "a" 0)
|
||||
],
|
||||
|
||||
"elim closure" :- [
|
||||
|
|
@ -78,56 +78,56 @@ tests = "whnf" :- [
|
|||
(CloE (Sub (^BV 0) id))
|
||||
(^BV 0),
|
||||
testWhnf "x{a/x}" empty
|
||||
(CloE (Sub (^BV 0) (^F "a" ::: id)))
|
||||
(^F "a"),
|
||||
(CloE (Sub (^BV 0) (^F "a" 0 ::: id)))
|
||||
(^F "a" 0),
|
||||
testWhnf "x{a/y}" (ctx [< ("x", ^Nat)])
|
||||
(CloE (Sub (^BV 0) (^BV 0 ::: ^F "a" ::: id)))
|
||||
(CloE (Sub (^BV 0) (^BV 0 ::: ^F "a" 0 ::: id)))
|
||||
(^BV 0),
|
||||
testWhnf "x{(y{a/y})/x}" empty
|
||||
(CloE (Sub (^BV 0) ((CloE (Sub (^BV 0) (^F "a" ::: id))) ::: id)))
|
||||
(^F "a"),
|
||||
(CloE (Sub (^BV 0) ((CloE (Sub (^BV 0) (^F "a" 0 ::: id))) ::: id)))
|
||||
(^F "a" 0),
|
||||
testWhnf "(x y){f/x,a/y}" empty
|
||||
(CloE (Sub (^App (^BV 0) (^BVT 1)) (^F "f" ::: ^F "a" ::: id)))
|
||||
(^App (^F "f") (^FT "a")),
|
||||
(CloE (Sub (^App (^BV 0) (^BVT 1)) (^F "f" 0 ::: ^F "a" 0 ::: id)))
|
||||
(^App (^F "f" 0) (^FT "a" 0)),
|
||||
testWhnf "(y ∷ x){A/x}" (ctx [< ("x", ^Nat)])
|
||||
(CloE (Sub (^Ann (^BVT 1) (^BVT 0)) (^F "A" ::: id)))
|
||||
(CloE (Sub (^Ann (^BVT 1) (^BVT 0)) (^F "A" 0 ::: id)))
|
||||
(^BV 0),
|
||||
testWhnf "(y ∷ x){A/x,a/y}" empty
|
||||
(CloE (Sub (^Ann (^BVT 1) (^BVT 0)) (^F "A" ::: ^F "a" ::: id)))
|
||||
(^F "a")
|
||||
(CloE (Sub (^Ann (^BVT 1) (^BVT 0)) (^F "A" 0 ::: ^F "a" 0 ::: id)))
|
||||
(^F "a" 0)
|
||||
],
|
||||
|
||||
"term closure" :- [
|
||||
testWhnf "(λ y ⇒ x){a/x}" empty
|
||||
(CloT (Sub (^LamN (^BVT 0)) (^F "a" ::: id)))
|
||||
(^LamN (^FT "a")),
|
||||
(CloT (Sub (^LamN (^BVT 0)) (^F "a" 0 ::: id)))
|
||||
(^LamN (^FT "a" 0)),
|
||||
testWhnf "(λy. y){a/x}" empty
|
||||
(CloT (Sub (^LamY "y" (^BVT 0)) (^F "a" ::: id)))
|
||||
(CloT (Sub (^LamY "y" (^BVT 0)) (^F "a" 0 ::: id)))
|
||||
(^LamY "y" (^BVT 0))
|
||||
],
|
||||
|
||||
"looking inside `E`" :- [
|
||||
testWhnf "(λx. x ∷ A ⊸ A) a" empty
|
||||
(E $ ^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A") (^FT "A")))
|
||||
(^FT "a"))
|
||||
(^FT "a")
|
||||
(E $ ^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^FT "a" 0))
|
||||
(^FT "a" 0)
|
||||
],
|
||||
|
||||
"nested redex" :- [
|
||||
testNoStep "λ y ⇒ ((λ x ⇒ x) ∷ 1.A → A) y" empty $
|
||||
^LamY "y" (E $
|
||||
^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A") (^FT "A")))
|
||||
^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^BVT 0)),
|
||||
testNoStep "f (((λ x ⇒ x) ∷ 1.A → A) a)" empty $
|
||||
^App (^F "f")
|
||||
(E $ ^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A") (^FT "A")))
|
||||
(^FT "a")),
|
||||
^App (^F "f" 0)
|
||||
(E $ ^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
|
||||
(^FT "a" 0)),
|
||||
testNoStep "λx. (y x){x/x,a/y}" (ctx [< ("y", ^Nat)]) $
|
||||
^LamY "x" (CloT $ Sub (E $ ^App (^BV 1) (^BVT 0))
|
||||
(^BV 0 ::: ^F "a" ::: id)),
|
||||
(^BV 0 ::: ^F "a" 0 ::: id)),
|
||||
testNoStep "f (y x){x/x,a/y}" (ctx [< ("y", ^Nat)]) $
|
||||
^App (^F "f")
|
||||
^App (^F "f" 0)
|
||||
(CloT (Sub (E $ ^App (^BV 1) (^BVT 0))
|
||||
(^BV 0 ::: ^F "a" ::: id)))
|
||||
(^BV 0 ::: ^F "a" 0 ::: id)))
|
||||
]
|
||||
]
|
||||
|
|
|
|||
|
|
@ -49,8 +49,8 @@ reflDef = ^LamY "A" (^LamY "x" (^DLamY "i" (^BVT 0)))
|
|||
|
||||
fstTy : Term d n
|
||||
fstTy =
|
||||
^PiY Zero "A" (^TYPE 1)
|
||||
(^PiY Zero "B" (^Arr Any (^BVT 0) (^TYPE 1))
|
||||
^PiY Zero "A" (^TYPE 0)
|
||||
(^PiY Zero "B" (^Arr Any (^BVT 0) (^TYPE 0))
|
||||
(^Arr Any (^SigY "x" (^BVT 1) (E $ ^App (^BV 1) (^BVT 0))) (^BVT 1)))
|
||||
|
||||
fstDef : Term d n
|
||||
|
|
@ -61,11 +61,11 @@ fstDef =
|
|||
|
||||
sndTy : Term d n
|
||||
sndTy =
|
||||
^PiY Zero "A" (^TYPE 1)
|
||||
(^PiY Zero "B" (^Arr Any (^BVT 0) (^TYPE 1))
|
||||
^PiY Zero "A" (^TYPE 0)
|
||||
(^PiY Zero "B" (^Arr Any (^BVT 0) (^TYPE 0))
|
||||
(^PiY Any "p" (^SigY "x" (^BVT 1) (E $ ^App (^BV 1) (^BVT 0)))
|
||||
(E $ ^App (^BV 1)
|
||||
(E $ ^App (^App (^App (^F "fst") (^BVT 2)) (^BVT 1)) (^BVT 0)))))
|
||||
(E $ ^App (^App (^App (^F "fst" 0) (^BVT 2)) (^BVT 1)) (^BVT 0)))))
|
||||
|
||||
sndDef : Term d n
|
||||
sndDef =
|
||||
|
|
@ -74,12 +74,15 @@ sndDef =
|
|||
(E $ ^CasePair Any (^BV 0)
|
||||
(SY [< "p"] $ E $
|
||||
^App (^BV 2)
|
||||
(E $ ^App (^App (^App (^F "fst") (^BVT 3)) (^BVT 2)) (^BVT 0)))
|
||||
(E $ ^App (^App (^App (^F "fst" 0) (^BVT 3)) (^BVT 2)) (^BVT 0)))
|
||||
(SY [< "x", "y"] $ ^BVT 0))))
|
||||
|
||||
nat : Term d n
|
||||
nat = ^Nat
|
||||
|
||||
apps : Elim d n -> List (Term d n) -> Elim d n
|
||||
apps = foldl (\f, s => ^App f s)
|
||||
|
||||
|
||||
defGlobals : Definitions
|
||||
defGlobals = fromList
|
||||
|
|
@ -87,19 +90,21 @@ defGlobals = fromList
|
|||
("B", ^mkPostulate gzero (^TYPE 0)),
|
||||
("C", ^mkPostulate gzero (^TYPE 1)),
|
||||
("D", ^mkPostulate gzero (^TYPE 1)),
|
||||
("P", ^mkPostulate gzero (^Arr Any (^FT "A") (^TYPE 0))),
|
||||
("a", ^mkPostulate gany (^FT "A")),
|
||||
("a'", ^mkPostulate gany (^FT "A")),
|
||||
("b", ^mkPostulate gany (^FT "B")),
|
||||
("f", ^mkPostulate gany (^Arr One (^FT "A") (^FT "A"))),
|
||||
("fω", ^mkPostulate gany (^Arr Any (^FT "A") (^FT "A"))),
|
||||
("g", ^mkPostulate gany (^Arr One (^FT "A") (^FT "B"))),
|
||||
("P", ^mkPostulate gzero (^Arr Any (^FT "A" 0) (^TYPE 0))),
|
||||
("a", ^mkPostulate gany (^FT "A" 0)),
|
||||
("a'", ^mkPostulate gany (^FT "A" 0)),
|
||||
("b", ^mkPostulate gany (^FT "B" 0)),
|
||||
("c", ^mkPostulate gany (^FT "C" 0)),
|
||||
("d", ^mkPostulate gany (^FT "D" 0)),
|
||||
("f", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "A" 0))),
|
||||
("fω", ^mkPostulate gany (^Arr Any (^FT "A" 0) (^FT "A" 0))),
|
||||
("g", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "B" 0))),
|
||||
("f2", ^mkPostulate gany
|
||||
(^Arr One (^FT "A") (^Arr One (^FT "A") (^FT "B")))),
|
||||
(^Arr One (^FT "A" 0) (^Arr One (^FT "A" 0) (^FT "B" 0)))),
|
||||
("p", ^mkPostulate gany
|
||||
(^PiY One "x" (^FT "A") (E $ ^App (^F "P") (^BVT 0)))),
|
||||
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
|
||||
("q", ^mkPostulate gany
|
||||
(^PiY One "x" (^FT "A") (E $ ^App (^F "P") (^BVT 0)))),
|
||||
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
|
||||
("refl", ^mkDef gany reflTy reflDef),
|
||||
("fst", ^mkDef gany fstTy fstDef),
|
||||
("snd", ^mkDef gany sndTy sndDef)]
|
||||
|
|
@ -180,36 +185,36 @@ tests = "typechecker" :- [
|
|||
"function types" :- [
|
||||
note "A, B : ★₀; C, D : ★₁; P : 0.A → ★₀",
|
||||
testTC "0 · 1.A → B ⇐ ★₀" $
|
||||
check_ empty szero (^Arr One (^FT "A") (^FT "B")) (^TYPE 0),
|
||||
check_ empty szero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 0),
|
||||
note "subtyping",
|
||||
testTC "0 · 1.A → B ⇐ ★₁" $
|
||||
check_ empty szero (^Arr One (^FT "A") (^FT "B")) (^TYPE 1),
|
||||
check_ empty szero (^Arr One (^FT "A" 0) (^FT "B" 0)) (^TYPE 1),
|
||||
testTC "0 · 1.C → D ⇐ ★₁" $
|
||||
check_ empty szero (^Arr One (^FT "C") (^FT "D")) (^TYPE 1),
|
||||
check_ empty szero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 1),
|
||||
testTCFail "0 · 1.C → D ⇍ ★₀" $
|
||||
check_ empty szero (^Arr One (^FT "C") (^FT "D")) (^TYPE 0),
|
||||
check_ empty szero (^Arr One (^FT "C" 0) (^FT "D" 0)) (^TYPE 0),
|
||||
testTC "0 · 1.(x : A) → P x ⇐ ★₀" $
|
||||
check_ empty szero
|
||||
(^PiY One "x" (^FT "A") (E $ ^App (^F "P") (^BVT 0)))
|
||||
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
|
||||
(^TYPE 0),
|
||||
testTCFail "0 · 1.A → P ⇍ ★₀" $
|
||||
check_ empty szero (^Arr One (^FT "A") (^FT "P")) (^TYPE 0),
|
||||
check_ empty szero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
|
||||
testTC "0=1 ⊢ 0 · 1.A → P ⇐ ★₀" $
|
||||
check_ empty01 szero (^Arr One (^FT "A") (^FT "P")) (^TYPE 0)
|
||||
check_ empty01 szero (^Arr One (^FT "A" 0) (^FT "P" 0)) (^TYPE 0)
|
||||
],
|
||||
|
||||
"pair types" :- [
|
||||
testTC "0 · A × A ⇐ ★₀" $
|
||||
check_ empty szero (^And (^FT "A") (^FT "A")) (^TYPE 0),
|
||||
check_ empty szero (^And (^FT "A" 0) (^FT "A" 0)) (^TYPE 0),
|
||||
testTCFail "0 · A × P ⇍ ★₀" $
|
||||
check_ empty szero (^And (^FT "A") (^FT "P")) (^TYPE 0),
|
||||
check_ empty szero (^And (^FT "A" 0) (^FT "P" 0)) (^TYPE 0),
|
||||
testTC "0 · (x : A) × P x ⇐ ★₀" $
|
||||
check_ empty szero
|
||||
(^SigY "x" (^FT "A") (E $ ^App (^F "P") (^BVT 0)))
|
||||
(^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
|
||||
(^TYPE 0),
|
||||
testTC "0 · (x : A) × P x ⇐ ★₁" $
|
||||
check_ empty szero
|
||||
(^SigY "x" (^FT "A") (E $ ^App (^F "P") (^BVT 0)))
|
||||
(^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
|
||||
(^TYPE 1),
|
||||
testTC "0 · (A : ★₀) × A ⇐ ★₁" $
|
||||
check_ empty szero
|
||||
|
|
@ -221,7 +226,7 @@ tests = "typechecker" :- [
|
|||
(^TYPE 0),
|
||||
testTCFail "1 · A × A ⇍ ★₀" $
|
||||
check_ empty sone
|
||||
(^And (^FT "A") (^FT "A"))
|
||||
(^And (^FT "A" 0) (^FT "A" 0))
|
||||
(^TYPE 0)
|
||||
],
|
||||
|
||||
|
|
@ -239,64 +244,64 @@ tests = "typechecker" :- [
|
|||
"free vars" :- [
|
||||
note "A : ★₀",
|
||||
testTC "0 · A ⇒ ★₀" $
|
||||
inferAs empty szero (^F "A") (^TYPE 0),
|
||||
inferAs empty szero (^F "A" 0) (^TYPE 0),
|
||||
testTC "0 · [A] ⇐ ★₀" $
|
||||
check_ empty szero (^FT "A") (^TYPE 0),
|
||||
check_ empty szero (^FT "A" 0) (^TYPE 0),
|
||||
note "subtyping",
|
||||
testTC "0 · [A] ⇐ ★₁" $
|
||||
check_ empty szero (^FT "A") (^TYPE 1),
|
||||
check_ empty szero (^FT "A" 0) (^TYPE 1),
|
||||
note "(fail) runtime-relevant type",
|
||||
testTCFail "1 · A ⇏ ★₀" $
|
||||
infer_ empty sone (^F "A"),
|
||||
infer_ empty sone (^F "A" 0),
|
||||
testTC "1 . f ⇒ 1.A → A" $
|
||||
inferAs empty sone (^F "f") (^Arr One (^FT "A") (^FT "A")),
|
||||
inferAs empty sone (^F "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 . f ⇐ 1.A → A" $
|
||||
check_ empty sone (^FT "f") (^Arr One (^FT "A") (^FT "A")),
|
||||
check_ empty sone (^FT "f" 0) (^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
testTCFail "1 . f ⇍ 0.A → A" $
|
||||
check_ empty sone (^FT "f") (^Arr Zero (^FT "A") (^FT "A")),
|
||||
check_ empty sone (^FT "f" 0) (^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
testTCFail "1 . f ⇍ ω.A → A" $
|
||||
check_ empty sone (^FT "f") (^Arr Any (^FT "A") (^FT "A")),
|
||||
check_ empty sone (^FT "f" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 . (λ x ⇒ f x) ⇐ 1.A → A" $
|
||||
check_ empty sone
|
||||
(^LamY "x" (E $ ^App (^F "f") (^BVT 0)))
|
||||
(^Arr One (^FT "A") (^FT "A")),
|
||||
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
|
||||
(^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 . (λ x ⇒ f x) ⇐ ω.A → A" $
|
||||
check_ empty sone
|
||||
(^LamY "x" (E $ ^App (^F "f") (^BVT 0)))
|
||||
(^Arr Any (^FT "A") (^FT "A")),
|
||||
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
|
||||
(^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
testTCFail "1 . (λ x ⇒ f x) ⇍ 0.A → A" $
|
||||
check_ empty sone
|
||||
(^LamY "x" (E $ ^App (^F "f") (^BVT 0)))
|
||||
(^Arr Zero (^FT "A") (^FT "A")),
|
||||
(^LamY "x" (E $ ^App (^F "f" 0) (^BVT 0)))
|
||||
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 . fω ⇒ ω.A → A" $
|
||||
inferAs empty sone (^F "fω") (^Arr Any (^FT "A") (^FT "A")),
|
||||
inferAs empty sone (^F "fω" 0) (^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 . (λ x ⇒ fω x) ⇐ ω.A → A" $
|
||||
check_ empty sone
|
||||
(^LamY "x" (E $ ^App (^F "fω") (^BVT 0)))
|
||||
(^Arr Any (^FT "A") (^FT "A")),
|
||||
(^LamY "x" (E $ ^App (^F "fω" 0) (^BVT 0)))
|
||||
(^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
testTCFail "1 . (λ x ⇒ fω x) ⇍ 0.A → A" $
|
||||
check_ empty sone
|
||||
(^LamY "x" (E $ ^App (^F "fω") (^BVT 0)))
|
||||
(^Arr Zero (^FT "A") (^FT "A")),
|
||||
(^LamY "x" (E $ ^App (^F "fω" 0) (^BVT 0)))
|
||||
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
testTCFail "1 . (λ x ⇒ fω x) ⇍ 1.A → A" $
|
||||
check_ empty sone
|
||||
(^LamY "x" (E $ ^App (^F "fω") (^BVT 0)))
|
||||
(^Arr One (^FT "A") (^FT "A")),
|
||||
(^LamY "x" (E $ ^App (^F "fω" 0) (^BVT 0)))
|
||||
(^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
note "refl : (0·A : ★₀) → (1·x : A) → (x ≡ x : A) ≔ (λ A x ⇒ δ _ ⇒ x)",
|
||||
testTC "1 · refl ⇒ ⋯" $ inferAs empty sone (^F "refl") reflTy,
|
||||
testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (^FT "refl") reflTy
|
||||
testTC "1 · refl ⇒ ⋯" $ inferAs empty sone (^F "refl" 0) reflTy,
|
||||
testTC "1 · [refl] ⇐ ⋯" $ check_ empty sone (^FT "refl" 0) reflTy
|
||||
],
|
||||
|
||||
"bound vars" :- [
|
||||
testTC "x : A ⊢ 1 · x ⇒ A ⊳ 1·x" $
|
||||
inferAsQ (ctx [< ("x", ^FT "A")]) sone
|
||||
(^BV 0) (^FT "A") [< One],
|
||||
inferAsQ (ctx [< ("x", ^FT "A" 0)]) sone
|
||||
(^BV 0) (^FT "A" 0) [< One],
|
||||
testTC "x : A ⊢ 1 · x ⇐ A ⊳ 1·x" $
|
||||
checkQ (ctx [< ("x", ^FT "A")]) sone (^BVT 0) (^FT "A") [< One],
|
||||
checkQ (ctx [< ("x", ^FT "A" 0)]) sone (^BVT 0) (^FT "A" 0) [< One],
|
||||
note "f2 : 1.A → 1.A → B",
|
||||
testTC "x : A ⊢ 1 · f2 x x ⇒ B ⊳ ω·x" $
|
||||
inferAsQ (ctx [< ("x", ^FT "A")]) sone
|
||||
(^App (^App (^F "f2") (^BVT 0)) (^BVT 0)) (^FT "B") [< Any]
|
||||
inferAsQ (ctx [< ("x", ^FT "A" 0)]) sone
|
||||
(^App (^App (^F "f2" 0) (^BVT 0)) (^BVT 0)) (^FT "B" 0) [< Any]
|
||||
],
|
||||
|
||||
"lambda" :- [
|
||||
|
|
@ -304,24 +309,25 @@ tests = "typechecker" :- [
|
|||
testTC "1 · (λ x ⇒ x) ⇐ A → A" $
|
||||
check_ empty sone
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^Arr One (^FT "A") (^FT "A")),
|
||||
(^Arr One (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 · (λ x ⇒ x) ⇐ ω.A → A" $
|
||||
check_ empty sone
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^Arr Any (^FT "A") (^FT "A")),
|
||||
(^Arr Any (^FT "A" 0) (^FT "A" 0)),
|
||||
note "(fail) zero binding used relevantly",
|
||||
testTCFail "1 · (λ x ⇒ x) ⇍ 0.A → A" $
|
||||
check_ empty sone
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^Arr Zero (^FT "A") (^FT "A")),
|
||||
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
note "(but ok in overall erased context)",
|
||||
testTC "0 · (λ x ⇒ x) ⇐ A ⇾ A" $
|
||||
check_ empty szero
|
||||
(^LamY "x" (^BVT 0))
|
||||
(^Arr Zero (^FT "A") (^FT "A")),
|
||||
(^Arr Zero (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "1 · (λ A x ⇒ refl A x) ⇐ ⋯ # (type of refl)" $
|
||||
check_ empty sone
|
||||
(^LamY "A" (^LamY "x" (E $ ^App (^App (^F "refl") (^BVT 1)) (^BVT 0))))
|
||||
(^LamY "A" (^LamY "x"
|
||||
(E $ ^App (^App (^F "refl" 0) (^BVT 1)) (^BVT 0))))
|
||||
reflTy,
|
||||
testTC "1 · (λ A x ⇒ δ i ⇒ x) ⇐ ⋯ # (def. and type of refl)" $
|
||||
check_ empty sone reflDef reflTy
|
||||
|
|
@ -330,68 +336,87 @@ tests = "typechecker" :- [
|
|||
"pairs" :- [
|
||||
testTC "1 · (a, a) ⇐ A × A" $
|
||||
check_ empty sone
|
||||
(^Pair (^FT "a") (^FT "a")) (^And (^FT "A") (^FT "A")),
|
||||
(^Pair (^FT "a" 0) (^FT "a" 0)) (^And (^FT "A" 0) (^FT "A" 0)),
|
||||
testTC "x : A ⊢ 1 · (x, x) ⇐ A × A ⊳ ω·x" $
|
||||
checkQ (ctx [< ("x", ^FT "A")]) sone
|
||||
(^Pair (^BVT 0) (^BVT 0)) (^And (^FT "A") (^FT "A")) [< Any],
|
||||
checkQ (ctx [< ("x", ^FT "A" 0)]) sone
|
||||
(^Pair (^BVT 0) (^BVT 0)) (^And (^FT "A" 0) (^FT "A" 0)) [< Any],
|
||||
testTC "1 · (a, δ i ⇒ a) ⇐ (x : A) × (x ≡ a)" $
|
||||
check_ empty sone
|
||||
(^Pair (^FT "a") (^DLamN (^FT "a")))
|
||||
(^SigY "x" (^FT "A") (^Eq0 (^FT "A") (^BVT 0) (^FT "a")))
|
||||
(^Pair (^FT "a" 0) (^DLamN (^FT "a" 0)))
|
||||
(^SigY "x" (^FT "A" 0) (^Eq0 (^FT "A" 0) (^BVT 0) (^FT "a" 0)))
|
||||
],
|
||||
|
||||
"unpairing" :- [
|
||||
testTC "x : A × A ⊢ 1 · (case1 x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 1·x" $
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A") (^FT "A"))]) sone
|
||||
(^CasePair One (^BV 0) (SN $ ^FT "B")
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2") (^BVT 1)) (^BVT 0)))
|
||||
(^FT "B") [< One],
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) sone
|
||||
(^CasePair One (^BV 0) (SN $ ^FT "B" 0)
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
|
||||
(^FT "B" 0) [< One],
|
||||
testTC "x : A × A ⊢ 1 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ ω·x" $
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A") (^FT "A"))]) sone
|
||||
(^CasePair Any (^BV 0) (SN $ ^FT "B")
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2") (^BVT 1)) (^BVT 0)))
|
||||
(^FT "B") [< Any],
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) sone
|
||||
(^CasePair Any (^BV 0) (SN $ ^FT "B" 0)
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
|
||||
(^FT "B" 0) [< Any],
|
||||
testTC "x : A × A ⊢ 0 · (caseω x return B of (l,r) ⇒ f2 l r) ⇒ B ⊳ 0·x" $
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A") (^FT "A"))]) szero
|
||||
(^CasePair Any (^BV 0) (SN $ ^FT "B")
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2") (^BVT 1)) (^BVT 0)))
|
||||
(^FT "B") [< Zero],
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) szero
|
||||
(^CasePair Any (^BV 0) (SN $ ^FT "B" 0)
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0)))
|
||||
(^FT "B" 0) [< Zero],
|
||||
testTCFail "x : A × A ⊢ 1 · (case0 x return B of (l,r) ⇒ f2 l r) ⇏" $
|
||||
infer_ (ctx [< ("x", ^And (^FT "A") (^FT "A"))]) sone
|
||||
(^CasePair Zero (^BV 0) (SN $ ^FT "B")
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2") (^BVT 1)) (^BVT 0))),
|
||||
infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "A" 0))]) sone
|
||||
(^CasePair Zero (^BV 0) (SN $ ^FT "B" 0)
|
||||
(SY [< "l", "r"] $ E $ ^App (^App (^F "f2" 0) (^BVT 1)) (^BVT 0))),
|
||||
testTC "x : A × B ⊢ 1 · (caseω x return A of (l,r) ⇒ l) ⇒ A ⊳ ω·x" $
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A") (^FT "B"))]) sone
|
||||
(^CasePair Any (^BV 0) (SN $ ^FT "A")
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) sone
|
||||
(^CasePair Any (^BV 0) (SN $ ^FT "A" 0)
|
||||
(SY [< "l", "r"] $ ^BVT 1))
|
||||
(^FT "A") [< Any],
|
||||
(^FT "A" 0) [< Any],
|
||||
testTC "x : A × B ⊢ 0 · (case1 x return A of (l,r) ⇒ l) ⇒ A ⊳ 0·x" $
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A") (^FT "B"))]) szero
|
||||
(^CasePair One (^BV 0) (SN $ ^FT "A")
|
||||
inferAsQ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) szero
|
||||
(^CasePair One (^BV 0) (SN $ ^FT "A" 0)
|
||||
(SY [< "l", "r"] $ ^BVT 1))
|
||||
(^FT "A") [< Zero],
|
||||
(^FT "A" 0) [< Zero],
|
||||
testTCFail "x : A × B ⊢ 1 · (case1 x return A of (l,r) ⇒ l) ⇏" $
|
||||
infer_ (ctx [< ("x", ^And (^FT "A") (^FT "B"))]) sone
|
||||
(^CasePair One (^BV 0) (SN $ ^FT "A")
|
||||
infer_ (ctx [< ("x", ^And (^FT "A" 0) (^FT "B" 0))]) sone
|
||||
(^CasePair One (^BV 0) (SN $ ^FT "A" 0)
|
||||
(SY [< "l", "r"] $ ^BVT 1)),
|
||||
note "fst : (0·A : ★₁) → (0·B : A ↠ ★₁) → ((x : A) × B x) ↠ A",
|
||||
note "fst : 0.(A : ★₀) → 0.(B : ω.A → ★₀) → ω.((x : A) × B x) → A",
|
||||
note " ≔ (λ A B p ⇒ caseω p return A of (x, y) ⇒ x)",
|
||||
testTC "0 · ‹type of fst› ⇐ ★₂" $
|
||||
check_ empty szero fstTy (^TYPE 2),
|
||||
testTC "0 · ‹type of fst› ⇐ ★₁" $
|
||||
check_ empty szero fstTy (^TYPE 1),
|
||||
testTC "1 · ‹def of fst› ⇐ ‹type of fst›" $
|
||||
check_ empty sone fstDef fstTy,
|
||||
note "snd : (0·A : ★₁) → (0·B : A ↠ ★₁) → (ω·p : (x : A) × B x) → B (fst A B p)",
|
||||
note "snd : 0.(A : ★₀) → 0.(B : A ↠ ★₀) → ω.(p : (x : A) × B x) → B (fst A B p)",
|
||||
note " ≔ (λ A B p ⇒ caseω p return p ⇒ B (fst A B p) of (x, y) ⇒ y)",
|
||||
testTC "0 · ‹type of snd› ⇐ ★₂" $
|
||||
check_ empty szero sndTy (^TYPE 2),
|
||||
testTC "0 · ‹type of snd› ⇐ ★₁" $
|
||||
check_ empty szero sndTy (^TYPE 1),
|
||||
testTC "1 · ‹def of snd› ⇐ ‹type of snd›" $
|
||||
check_ empty sone sndDef sndTy,
|
||||
testTC "0 · snd ★₀ (λ x ⇒ x) ⇒ (ω·p : (A : ★₀) × A) → fst ★₀ (λ x ⇒ x) p" $
|
||||
testTC "0 · snd A P ⇒ ω.(p : (x : A) × P x) → P (fst A P p)" $
|
||||
inferAs empty szero
|
||||
(^App (^App (^F "snd") (^TYPE 0)) (^LamY "x" (^BVT 0)))
|
||||
(^PiY Any "p" (^SigY "A" (^TYPE 0) (^BVT 0))
|
||||
(E $ ^App (^App (^App (^F "fst") (^TYPE 0)) (^LamY "x" (^BVT 0)))
|
||||
(^BVT 0)))
|
||||
(^App (^App (^F "snd" 0) (^FT "A" 0)) (^FT "P" 0))
|
||||
(^PiY Any "p" (^SigY "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))
|
||||
(E $ ^App (^F "P" 0)
|
||||
(E $ apps (^F "fst" 0) [^FT "A" 0, ^FT "P" 0, ^BVT 0]))),
|
||||
testTC "1 · fst A (λ _ ⇒ B) (a, b) ⇒ A" $
|
||||
inferAs empty sone
|
||||
(apps (^F "fst" 0)
|
||||
[^FT "A" 0, ^LamN (^FT "B" 0), ^Pair (^FT "a" 0) (^FT "b" 0)])
|
||||
(^FT "A" 0),
|
||||
testTC "1 · fst¹ A (λ _ ⇒ B) (a, b) ⇒ A" $
|
||||
inferAs empty sone
|
||||
(apps (^F "fst" 1)
|
||||
[^FT "A" 0, ^LamN (^FT "B" 0), ^Pair (^FT "a" 0) (^FT "b" 0)])
|
||||
(^FT "A" 0),
|
||||
testTCFail "1 · fst ★⁰ (λ _ ⇒ ★⁰) (A, B) ⇏" $
|
||||
infer_ empty sone
|
||||
(apps (^F "fst" 0)
|
||||
[^TYPE 0, ^LamN (^TYPE 0), ^Pair (^FT "A" 0) (^FT "B" 0)]),
|
||||
testTC "0 · fst¹ ★⁰ (λ _ ⇒ ★⁰) (A, B) ⇒ ★⁰" $
|
||||
inferAs empty szero
|
||||
(apps (^F "fst" 1)
|
||||
[^TYPE 0, ^LamN (^TYPE 0), ^Pair (^FT "A" 0) (^FT "B" 0)])
|
||||
(^TYPE 0)
|
||||
],
|
||||
|
||||
"enums" :- [
|
||||
|
|
@ -435,33 +460,35 @@ tests = "typechecker" :- [
|
|||
(^Eq0 (^enum ["beep"]) (^Zero) (^Tag "beep"))
|
||||
Nothing,
|
||||
testTC "ab : A ≡ B : ★₀, x : A, y : B ⊢ 0 · Eq [i ⇒ ab i] x y ⇐ ★₀" $
|
||||
check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A") (^FT "B")),
|
||||
("x", ^FT "A"), ("y", ^FT "B")]) szero
|
||||
check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0)),
|
||||
("x", ^FT "A" 0), ("y", ^FT "B" 0)]) szero
|
||||
(^EqY "i" (E $ ^DApp (^BV 2) (^BV 0)) (^BVT 1) (^BVT 0))
|
||||
(^TYPE 0),
|
||||
testTCFail "ab : A ≡ B : ★₀, x : A, y : B ⊢ Eq [i ⇒ ab i] y x ⇍ Type" $
|
||||
check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A") (^FT "B")),
|
||||
("x", ^FT "A"), ("y", ^FT "B")]) szero
|
||||
check_ (ctx [< ("ab", ^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0)),
|
||||
("x", ^FT "A" 0), ("y", ^FT "B" 0)]) szero
|
||||
(^EqY "i" (E $ ^DApp (^BV 2) (^BV 0)) (^BVT 0) (^BVT 1))
|
||||
(^TYPE 0)
|
||||
],
|
||||
|
||||
"equalities" :- [
|
||||
testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
|
||||
check_ empty sone (^DLamN (^FT "a"))
|
||||
(^Eq0 (^FT "A") (^FT "a") (^FT "a")),
|
||||
check_ empty sone (^DLamN (^FT "a" 0))
|
||||
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0)),
|
||||
testTC "0 · (λ p q ⇒ δ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q # uip" $
|
||||
check_ empty szero
|
||||
(^LamY "p" (^LamY "q" (^DLamN (^BVT 1))))
|
||||
(^PiY Any "p" (^Eq0 (^FT "A") (^FT "a") (^FT "a"))
|
||||
(^PiY Any "q" (^Eq0 (^FT "A") (^FT "a") (^FT "a"))
|
||||
(^Eq0 (^Eq0 (^FT "A") (^FT "a") (^FT "a")) (^BVT 1) (^BVT 0)))),
|
||||
(^PiY Any "p" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(^PiY Any "q" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(^Eq0 (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(^BVT 1) (^BVT 0)))),
|
||||
testTC "0 · (λ p q ⇒ δ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q # uip(2)" $
|
||||
check_ empty szero
|
||||
(^LamY "p" (^LamY "q" (^DLamN (^BVT 0))))
|
||||
(^PiY Any "p" (^Eq0 (^FT "A") (^FT "a") (^FT "a"))
|
||||
(^PiY Any "q" (^Eq0 (^FT "A") (^FT "a") (^FT "a"))
|
||||
(^Eq0 (^Eq0 (^FT "A") (^FT "a") (^FT "a")) (^BVT 1) (^BVT 0))))
|
||||
(^PiY Any "p" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(^PiY Any "q" (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(^Eq0 (^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a" 0))
|
||||
(^BVT 1) (^BVT 0))))
|
||||
],
|
||||
|
||||
"natural numbers" :- [
|
||||
|
|
|
|||
Loading…
Reference in New Issue