diff --git a/examples/bool.quox b/examples/bool.quox index c05e4c1..1d142b5 100644 --- a/examples/bool.quox +++ b/examples/bool.quox @@ -2,19 +2,19 @@ load "misc.quox"; namespace bool { -def0 Bool : ★₀ = {true, false}; +def0 Bool : ★⁰ = {true, false}; def boolω : 1.Bool → [ω.Bool] = λ b ⇒ case1 b return [ω.Bool] of { 'true ⇒ ['true]; 'false ⇒ ['false] }; -def if : 0.(A : ★₀) → 1.Bool → ω.A → ω.A → A = +def if : 0.(A : ★⁰) → 1.Bool → ω.A → ω.A → A = λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f }; -- [todo]: universe lifting -def0 If : 1.Bool → 0.★₀ → 0.★₀ → ★₀ = - λ b T F ⇒ case1 b return ★₀ of { 'true ⇒ T; 'false ⇒ F }; +def0 If : 1.Bool → 0.★⁰ → 0.★⁰ → ★⁰ = + λ b T F ⇒ case1 b return ★⁰ of { 'true ⇒ T; 'false ⇒ F }; -def0 T : ω.Bool → ★₀ = λ b ⇒ If b True False; +def0 T : ω.Bool → ★⁰ = λ b ⇒ If b True False; def true-not-false : Not ('true ≡ 'false : Bool) = λ eq ⇒ coe (i ⇒ T (eq @i)) 'true; diff --git a/examples/either.quox b/examples/either.quox index f2d748e..4abe355 100644 --- a/examples/either.quox +++ b/examples/either.quox @@ -3,22 +3,22 @@ load "bool.quox"; namespace either { -def0 Tag : ★₀ = {left, right}; +def0 Tag : ★⁰ = {left, right}; -def0 Payload : 0.★₀ → 0.★₀ → 1.Tag → ★₀ = - λ A B tag ⇒ case1 tag return ★₀ of { 'left ⇒ A; 'right ⇒ B }; +def0 Payload : 0.★⁰ → 0.★⁰ → 1.Tag → ★⁰ = + λ A B tag ⇒ case1 tag return ★⁰ of { 'left ⇒ A; 'right ⇒ B }; -def0 Either : 0.★₀ → 0.★₀ → ★₀ = +def0 Either : 0.★⁰ → 0.★⁰ → ★⁰ = λ A B ⇒ (tag : Tag) × Payload A B tag; -def Left : 0.(A B : ★₀) → 1.A → Either A B = +def Left : 0.(A B : ★⁰) → 1.A → Either A B = λ A B x ⇒ ('left, x); -def Right : 0.(A B : ★₀) → 1.B → Either A B = +def Right : 0.(A B : ★⁰) → 1.B → Either A B = λ A B x ⇒ ('right, x); def elim' : - 0.(A B : ★₀) → 0.(P : 0.(Either A B) → ★₀) → + 0.(A B : ★⁰) → 0.(P : 0.(Either A B) → ★⁰) → ω.(1.(x : A) → P (Left A B x)) → ω.(1.(x : B) → P (Right A B x)) → 1.(t : Tag) → 1.(a : Payload A B t) → P (t, a) = @@ -28,7 +28,7 @@ def elim' : of { 'left ⇒ f; 'right ⇒ g }; def elim : - 0.(A B : ★₀) → 0.(P : 0.(Either A B) → ★₀) → + 0.(A B : ★⁰) → 0.(P : 0.(Either A B) → ★⁰) → ω.(1.(x : A) → P (Left A B x)) → ω.(1.(x : B) → P (Right A B x)) → 1.(x : Either A B) → P x = @@ -45,16 +45,16 @@ def Right = either.Right; namespace dec { -def0 Dec : 0.★₀ → ★₀ = λ A ⇒ Either [0.A] [0.Not A]; +def0 Dec : 0.★⁰ → ★⁰ = λ A ⇒ Either [0.A] [0.Not A]; -def Yes : 0.(A : ★₀) → 0.A → Dec A = λ A y ⇒ Left [0.A] [0.Not A] [y]; -def No : 0.(A : ★₀) → 0.(Not A) → Dec A = λ A n ⇒ Right [0.A] [0.Not A] [n]; +def Yes : 0.(A : ★⁰) → 0.A → Dec A = λ A y ⇒ Left [0.A] [0.Not A] [y]; +def No : 0.(A : ★⁰) → 0.(Not A) → Dec A = λ A n ⇒ Right [0.A] [0.Not A] [n]; -def0 DecEq : 0.★₀ → ★₀ = +def0 DecEq : 0.★⁰ → ★⁰ = λ A ⇒ ω.(x : A) → ω.(y : A) → Dec (x ≡ y : A); def elim : - 0.(A : ★₀) → 0.(P : 0.(Dec A) → ★₀) → + 0.(A : ★⁰) → 0.(P : 0.(Dec A) → ★⁰) → ω.(0.(y : A) → P (Yes A y)) → ω.(0.(n : Not A) → P (No A n)) → 1.(x : Dec A) → P x = @@ -63,7 +63,7 @@ def elim : (λ y ⇒ case0 y return y' ⇒ P (Left [0.A] [0.Not A] y') of {[y'] ⇒ f y'}) (λ n ⇒ case0 n return n' ⇒ P (Right [0.A] [0.Not A] n') of {[n'] ⇒ g n'}); -def bool : 0.(A : ★₀) → 1.(Dec A) → Bool = +def bool : 0.(A : ★⁰) → 1.(Dec A) → Bool = λ A ⇒ elim A (λ _ ⇒ Bool) (λ _ ⇒ 'true) (λ _ ⇒ 'false); } diff --git a/examples/list.quox b/examples/list.quox index 9a0173b..659d98e 100644 --- a/examples/list.quox +++ b/examples/list.quox @@ -2,23 +2,23 @@ load "nat.quox"; namespace list { -def0 Vec : 0.ℕ → 0.★₀ → ★₀ = +def0 Vec : 0.ℕ → 0.★⁰ → ★⁰ = λ n A ⇒ - caseω n return ★₀ of { + caseω n return ★⁰ of { zero ⇒ {nil}; succ _, 0.Tail ⇒ A × Tail }; -def0 List : 0.★₀ → ★₀ = +def0 List : 0.★⁰ → ★⁰ = λ A ⇒ (len : ℕ) × Vec len A; -def nil : 0.(A : ★₀) → List A = +def nil : 0.(A : ★⁰) → List A = λ A ⇒ (0, 'nil); -def cons : 0.(A : ★₀) → 1.A → 1.(List A) → List A = +def cons : 0.(A : ★⁰) → 1.A → 1.(List A) → List A = λ A x xs ⇒ case1 xs return List A of { (len, elems) ⇒ (succ len, x, elems) }; -def foldr' : 0.(A B : ★₀) → +def foldr' : 0.(A B : ★⁰) → 1.B → ω.(1.A → 1.B → B) → 1.(n : ℕ) → 1.(Vec n A) → B = λ A B z c n ⇒ case1 n return n' ⇒ 1.(Vec n' A) → B of { @@ -28,7 +28,7 @@ def foldr' : 0.(A B : ★₀) → λ cons ⇒ case1 cons return B of { (first, rest) ⇒ c first (ih rest) } }; -def foldr : 0.(A B : ★₀) → 1.B → ω.(1.A → 1.B → B) → 1.(List A) → B = +def foldr : 0.(A B : ★⁰) → 1.B → ω.(1.A → 1.B → B) → 1.(List A) → B = λ A B z c xs ⇒ case1 xs return B of { (len, elems) ⇒ foldr' A B z c len elems }; diff --git a/examples/misc.quox b/examples/misc.quox index 47ba323..80c0ac9 100644 --- a/examples/misc.quox +++ b/examples/misc.quox @@ -1,36 +1,36 @@ -def0 True : ★₀ = {true}; +def0 True : ★⁰ = {true}; -def0 False : ★₀ = {}; -def0 Not : 0.★₀ → ★₀ = λ A ⇒ ω.A → False; +def0 False : ★⁰ = {}; +def0 Not : 0.★⁰ → ★⁰ = λ A ⇒ ω.A → False; -def void : 0.(A : ★₀) → 0.False → A = +def void : 0.(A : ★⁰) → 0.False → A = λ A v ⇒ case0 v return A of { }; -def0 Pred : 0.★₀ → ★₁ = λ A ⇒ 0.A → ★₀; +def0 Pred : 0.★⁰ → ★¹ = λ A ⇒ 0.A → ★⁰; -def0 All : 0.(A : ★₀) → 0.(Pred A) → ★₁ = +def0 All : 0.(A : ★⁰) → 0.(Pred A) → ★¹ = λ A P ⇒ 1.(x : A) → P x; def cong : - 0.(A : ★₀) → 0.(P : Pred A) → 1.(p : All A P) → + 0.(A : ★⁰) → 0.(P : Pred A) → 1.(p : All A P) → 0.(x y : A) → 1.(xy : x ≡ y : A) → Eq (𝑖 ⇒ P (xy @𝑖)) (p x) (p y) = λ A P p x y xy ⇒ δ 𝑖 ⇒ p (xy @𝑖); def0 eq-f : - 0.(A : ★₀) → 0.(P : Pred A) → + 0.(A : ★⁰) → 0.(P : Pred A) → 0.(p : All A P) → 0.(q : All A P) → - 0.A → ★₀ = + 0.A → ★⁰ = λ A P p q x ⇒ p x ≡ q x : P x; def funext : - 0.(A : ★₀) → 0.(P : Pred A) → 0.(p q : All A P) → + 0.(A : ★⁰) → 0.(P : Pred A) → 0.(p q : All A P) → 1.(All A (eq-f A P p q)) → p ≡ q : All A P = λ A P p q eq ⇒ δ 𝑖 ⇒ λ x ⇒ eq x @𝑖; -def sym : 0.(A : ★₀) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A = +def sym : 0.(A : ★⁰) → 0.(x y : A) → 1.(x ≡ y : A) → y ≡ x : A = λ A x y eq ⇒ δ 𝑖 ⇒ comp A (eq @0) @𝑖 { 0 𝑗 ⇒ eq @𝑗; 1 _ ⇒ eq @0 }; -def trans : 0.(A : ★₀) → 0.(x y z : A) → +def trans : 0.(A : ★⁰) → 0.(x y z : A) → ω.(x ≡ y : A) → ω.(y ≡ z : A) → x ≡ z : A = λ A x y z eq1 eq2 ⇒ δ 𝑖 ⇒ comp A (eq1 @𝑖) @𝑖 { 0 _ ⇒ eq1 @0; 1 𝑗 ⇒ eq2 @𝑗 }; diff --git a/examples/nat.quox b/examples/nat.quox index ef0784e..1177334 100644 --- a/examples/nat.quox +++ b/examples/nat.quox @@ -37,8 +37,8 @@ def0 succ-inj : 0.(m n : ℕ) → 0.(succ m ≡ succ n : ℕ) → m ≡ n : ℕ λ m n eq ⇒ δ 𝑖 ⇒ pred (eq @𝑖); -def0 IsSucc : 0.ℕ → ★₀ = - λ n ⇒ caseω n return ★₀ of { zero ⇒ False; succ _ ⇒ True }; +def0 IsSucc : 0.ℕ → ★⁰ = + λ n ⇒ caseω n return ★⁰ of { zero ⇒ False; succ _ ⇒ True }; def isSucc? : ω.(n : ℕ) → Dec (IsSucc n) = λ n ⇒ diff --git a/examples/pair.quox b/examples/pair.quox index 016bae4..925f7fa 100644 --- a/examples/pair.quox +++ b/examples/pair.quox @@ -1,35 +1,35 @@ namespace pair { -def0 Σ : 0.(A : ★₀) → 0.(0.A → ★₀) → ★₀ = λ A B ⇒ (x : A) × B x; +def0 Σ : 0.(A : ★⁰) → 0.(0.A → ★⁰) → ★⁰ = λ A B ⇒ (x : A) × B x; -def fst : 0.(A : ★₀) → 0.(B : 0.A → ★₀) → ω.(Σ A B) → A = +def fst : 0.(A : ★⁰) → 0.(B : 0.A → ★⁰) → ω.(Σ A B) → A = λ A B p ⇒ caseω p return A of { (x, _) ⇒ x }; -def snd : 0.(A : ★₀) → 0.(B : 0.A → ★₀) → ω.(p : Σ A B) → B (fst A B p) = +def snd : 0.(A : ★⁰) → 0.(B : 0.A → ★⁰) → ω.(p : Σ A B) → B (fst A B p) = λ A B p ⇒ caseω p return p' ⇒ B (fst A B p') of { (_, y) ⇒ y }; def uncurry : - 0.(A : ★₀) → 0.(B : 0.A → ★₀) → 0.(C : 0.(x : A) → 0.(B x) → ★₀) → + 0.(A : ★⁰) → 0.(B : 0.A → ★⁰) → 0.(C : 0.(x : A) → 0.(B x) → ★⁰) → 1.(f : 1.(x : A) → 1.(y : B x) → C x y) → 1.(p : Σ A B) → C (fst A B p) (snd A B p) = λ A B C f p ⇒ case1 p return p' ⇒ C (fst A B p') (snd A B p') of { (x, y) ⇒ f x y }; def uncurry' : - 0.(A B C : ★₀) → 1.(1.A → 1.B → C) → 1.(A × B) → C = + 0.(A B C : ★⁰) → 1.(1.A → 1.B → C) → 1.(A × B) → C = λ A B C ⇒ uncurry A (λ _ ⇒ B) (λ _ _ ⇒ C); def curry : - 0.(A : ★₀) → 0.(B : 0.A → ★₀) → 0.(C : 0.(Σ A B) → ★₀) → + 0.(A : ★⁰) → 0.(B : 0.A → ★⁰) → 0.(C : 0.(Σ A B) → ★⁰) → 1.(f : 1.(p : Σ A B) → C p) → 1.(x : A) → 1.(y : B x) → C (x, y) = λ A B C f x y ⇒ f (x, y); def curry' : - 0.(A B C : ★₀) → 1.(1.(A × B) → C) → 1.A → 1.B → C = + 0.(A B C : ★⁰) → 1.(1.(A × B) → C) → 1.A → 1.B → C = λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C); def0 fst-snd : - 0.(A : ★₀) → 0.(B : 0.A → ★₀) → + 0.(A : ★⁰) → 0.(B : 0.A → ★⁰) → 1.(p : Σ A B) → p ≡ (fst A B p, snd A B p) : Σ A B = λ A B p ⇒ case1 p @@ -37,14 +37,14 @@ def0 fst-snd : of { (x, y) ⇒ δ 𝑖 ⇒ (x, y) }; def map : - 0.(A A' : ★₀) → - 0.(B : 0.A → ★₀) → 0.(B' : 0.A' → ★₀) → + 0.(A A' : ★⁰) → + 0.(B : 0.A → ★⁰) → 0.(B' : 0.A' → ★⁰) → 1.(f : 1.A → A') → 1.(g : 0.(x : A) → 1.(B x) → B' (f x)) → 1.(Σ A B) → Σ A' B' = λ A A' B B' f g p ⇒ case1 p return Σ A' B' of { (x, y) ⇒ (f x, g x y) }; -def map' : 0.(A A' B B' : ★₀) → +def map' : 0.(A A' B B' : ★⁰) → 1.(1.A → A') → 1.(1.B → B') → 1.(A × B) → A' × B' = λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g); diff --git a/lib/Quox/CharExtra.idr b/lib/Quox/CharExtra.idr index 8e7af2f..a2a05a3 100644 --- a/lib/Quox/CharExtra.idr +++ b/lib/Quox/CharExtra.idr @@ -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 diff --git a/lib/Quox/Displace.idr b/lib/Quox/Displace.idr new file mode 100644 index 0000000..c7d5e02 --- /dev/null +++ b/lib/Quox/Displace.idr @@ -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 diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index abd4d66..d4f9890 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -398,11 +398,11 @@ parameters (defs : Definitions) (0 ne : NotRedex defs e) -> (0 nf : NotRedex defs f) -> Equal_ () - 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 @@ -538,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 @@ -551,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 diff --git a/lib/Quox/Name.idr b/lib/Quox/Name.idr index f4637e7..fe0eb46 100644 --- a/lib/Quox/Name.idr +++ b/lib/Quox/Name.idr @@ -124,7 +124,7 @@ fromList = fromPName . fromListP export syntaxChars : List Char -syntaxChars = ['(', ')', '[', ']', '{', '}', '"', '\'', ',', '.', ';'] +syntaxChars = ['(', ')', '[', ']', '{', '}', '"', '\'', ',', '.', ';', '^'] export isSymStart, isSymCont : Char -> Bool diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index 312585b..637be56 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -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 diff --git a/lib/Quox/Parser/FromParser/Error.idr b/lib/Quox/Parser/FromParser/Error.idr index 49c6df7..98313ce 100644 --- a/lib/Quox/Parser/FromParser/Error.idr +++ b/lib/Quox/Parser/FromParser/Error.idr @@ -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 diff --git a/lib/Quox/Parser/Lexer.idr b/lib/Quox/Parser/Lexer.idr index 2760f53..a6b1fee 100644 --- a/lib/Quox/Parser/Lexer.idr +++ b/lib/Quox/Parser/Lexer.idr @@ -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)) diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr index a54fb89..c5d5764 100644 --- a/lib/Quox/Parser/Parser.idr +++ b/lib/Quox/Parser/Parser.idr @@ -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 "★" *> 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 "★" *> mustWork [|TYPE $ nat <|> super|] + -- having super here looks redundant, but when parsing a non-atomic term + -- this branch will be taken first export eqTerm : FileName -> Grammar True PTerm diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr index 59feadd..335eb49 100644 --- a/lib/Quox/Parser/Syntax.idr +++ b/lib/Quox/Parser/Syntax.idr @@ -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 diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index cc427a3..f90e5ec 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -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 diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr index 46d346d..67151c0 100644 --- a/lib/Quox/Reduce.idr +++ b/lib/Quox/Reduce.idr @@ -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 @@ -237,9 +238,9 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) export covering computeElimType : (e : Elim d n) -> (0 ne : No (isRedexE defs e)) => WhnfM (Term d n) - computeElimType (F {x, loc}) = do + 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); @@ -477,7 +478,7 @@ 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 -> @@ -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 -- @@ -569,9 +569,9 @@ where 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 + 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 diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr index 7b5e089..5682c73 100644 --- a/lib/Quox/Syntax/Term/Base.idr +++ b/lib/Quox/Syntax/Term/Base.idr @@ -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 _) = diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index 4d8e81d..d9c20fb 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -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 @@ -368,11 +376,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 +471,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 diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr index 191d3ac..2054976 100644 --- a/lib/Quox/Syntax/Term/Subst.idr +++ b/lib/Quox/Syntax/Term/Subst.idr @@ -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 diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr index 1062342..dee04ff 100644 --- a/lib/Quox/Syntax/Term/Tighten.idr +++ b/lib/Quox/Syntax/Term/Tighten.idr @@ -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) = diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index 0cc2e19..3a019e9 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -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 ∈ Γ diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 53c93f6..77285c5 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -31,6 +31,7 @@ modules = Quox.Syntax.Term.Pretty, Quox.Syntax.Term.Subst, Quox.Syntax.Var, + Quox.Displace, Quox.Definition, Quox.Reduce, Quox.Context, diff --git a/syntax.ebnf b/syntax.ebnf index 426416c..3325b28 100644 --- a/syntax.ebnf +++ b/syntax.ebnf @@ -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 / ","}+, [","], ")". diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index ccd690e..7756528 100644 --- a/tests/Tests/Equal.idr +++ b/tests/Tests/Equal.idr @@ -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" :- [ diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr index a8b1ca6..c4202eb 100644 --- a/tests/Tests/FromPTerm.idr +++ b/tests/Tests/FromPTerm.idr @@ -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" diff --git a/tests/Tests/Lexer.idr b/tests/Tests/Lexer.idr index 118ba5e..7823d5d 100644 --- a/tests/Tests/Lexer.idr +++ b/tests/Tests/Lexer.idr @@ -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 "★"] diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr index ffb7378..6c1a3bb 100644 --- a/tests/Tests/Parser.idr +++ b/tests/Tests/Parser.idr @@ -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,14 +105,14 @@ 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 _), @@ -122,137 +122,139 @@ tests = "parser" :- [ "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") {}) _]) ] ] diff --git a/tests/Tests/PrettyTerm.idr b/tests/Tests/PrettyTerm.idr index bdca2f6..71e183f 100644 --- a/tests/Tests/PrettyTerm.idr +++ b/tests/Tests/PrettyTerm.idr @@ -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" ] ] diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr index b81d564..53404e4 100644 --- a/tests/Tests/Reduce.idr +++ b/tests/Tests/Reduce.idr @@ -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))) ] ] diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index 59b23f0..d9e91bc 100644 --- a/tests/Tests/Typechecker.idr +++ b/tests/Tests/Typechecker.idr @@ -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" :- [