From ae01d3818d0b3813afe3f7add6d89936ab43af4e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Dec 2013 15:15:32 -0800 Subject: [PATCH] fix(frontends/lean/parser): parse_type method The parser had a nasty ambiguity. For example, f Type 1 had two possible interpretations (f (Type) (1)) or (f (Type 1)) To fix this issue, whenever we want to specify a particular universe, we have to precede 'Type' with a parenthesis. Examples: (Type 1) (Type U) (Type M + 1) Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 16 ++++++------ src/tests/frontends/lean/parser.cpp | 2 +- tests/lean/conv.lean | 6 ++--- tests/lean/elab6.lean | 2 +- tests/lean/elab7.lean | 4 +-- tests/lean/exists3.lean | 2 +- tests/lean/norm1.lean | 2 +- tests/lean/revapp.lean | 4 +-- tests/lean/tactic7.lean | 38 ++++++++++++++--------------- tests/lean/tst15.lean | 32 ++++++++++++------------ tests/lean/tst7.lean | 2 +- tests/lean/ty2.lean | 4 +-- 12 files changed, 57 insertions(+), 57 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index f9c94b5f2..9f3d2e788 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -927,9 +927,9 @@ class parser::imp { expr parse_lparen() { auto p = pos(); next(); - expr r = save(parse_expr(), p); + expr r = curr() == scanner::token::Type ? parse_type(true) : parse_expr(); check_rparen_next("invalid expression, ')' expected"); - return r; + return save(r, p); } /** @@ -1168,13 +1168,13 @@ class parser::imp { } /** \brief Parse 'Type' and 'Type' level expressions. */ - expr parse_type() { + expr parse_type(bool level_expected) { auto p = pos(); next(); - if (curr_is_identifier() || curr_is_nat()) { + if (level_expected) { return save(mk_type(parse_level()), p); } else { - return Type(); + return save(Type(), p); } } @@ -1267,7 +1267,7 @@ class parser::imp { case scanner::token::DecimalVal: return parse_decimal(); case scanner::token::StringVal: return parse_string(); case scanner::token::Placeholder: return parse_placeholder(); - case scanner::token::Type: return parse_type(); + case scanner::token::Type: return parse_type(false); case scanner::token::Show: return parse_show_expr(); case scanner::token::By: return parse_by_expr(); default: @@ -1279,6 +1279,8 @@ class parser::imp { \brief Create a new application and associate position of left with the resultant expression. */ expr mk_app_left(expr const & left, expr const & arg) { + if (is_type(left)) + throw parser_error("Type is not a function, use '(Type )' for specifying a particular type universe", pos()); auto it = m_expr_pos_info.find(left); lean_assert(it != m_expr_pos_info.end()); return save(mk_app(left, arg), it->second); @@ -1297,7 +1299,7 @@ class parser::imp { case scanner::token::DecimalVal: return mk_app_left(left, parse_decimal()); case scanner::token::StringVal: return mk_app_left(left, parse_string()); case scanner::token::Placeholder: return mk_app_left(left, parse_placeholder()); - case scanner::token::Type: return mk_app_left(left, parse_type()); + case scanner::token::Type: return mk_app_left(left, parse_type(false)); default: return left; } } diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index 1756b793f..adb6dd827 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/src/tests/frontends/lean/parser.cpp @@ -86,7 +86,7 @@ static void tst3() { parse_error(env, ios, "Help Echo"); check(env, ios, "10.3", mk_real_value(mpq(103, 10))); parse(env, ios, "Variable f : Real -> Real. Check f 10.3."); - parse(env, ios, "Variable g : Type 1 -> Type. Check g Type"); + parse(env, ios, "Variable g : (Type 1) -> Type. Check g Type"); parse_error(env, ios, "Check fun ."); parse_error(env, ios, "Definition foo ."); parse_error(env, ios, "Check a"); diff --git a/tests/lean/conv.lean b/tests/lean/conv.lean index f96da3a38..9d1f0be6f 100644 --- a/tests/lean/conv.lean +++ b/tests/lean/conv.lean @@ -1,18 +1,18 @@ -Definition id (A : Type) : Type U := A. +Definition id (A : Type) : (Type U) := A. Variable p : (Int -> Int) -> Bool. Check fun (x : id Int), x. Variable f : (id Int) -> (id Int). Check p f. -Definition c (A : Type 3) : Type 3 := Type 1. +Definition c (A : (Type 3)) : (Type 3) := (Type 1). Variable g : (c (Type 2)) -> Bool. Variable a : (c (Type 1)). Check g a. -Definition c2 {T : Type} (A : Type 3) (a : T) : Type 3 := Type 1 +Definition c2 {T : Type} (A : (Type 3)) (a : T) : (Type 3) := (Type 1) Variable b : Int Check c2::explicit Variable g2 : (c2 (Type 2) b) -> Bool diff --git a/tests/lean/elab6.lean b/tests/lean/elab6.lean index 7f913193e..be1ea8590 100644 --- a/tests/lean/elab6.lean +++ b/tests/lean/elab6.lean @@ -1,2 +1,2 @@ -Theorem ForallIntro2 (A : Type U) (P : A -> Bool) (H : Pi x, P x) : forall x, P x := +Theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x := Abst (fun x, EqTIntro (H x)) diff --git a/tests/lean/elab7.lean b/tests/lean/elab7.lean index fe2f8f070..7708b9417 100644 --- a/tests/lean/elab7.lean +++ b/tests/lean/elab7.lean @@ -1,6 +1,4 @@ -Variable A : Type U -Variable B : Type U -Variable C : Type U +Variables A B C : (Type U) Variable P : A -> Bool Variable F1 : A -> B -> C Variable F2 : A -> B -> C diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean index eedecb73a..8db4891c2 100644 --- a/tests/lean/exists3.lean +++ b/tests/lean/exists3.lean @@ -16,7 +16,7 @@ Theorem T2 : exists x y, P x y := in ExistsElim L2 (fun (w : Int) (H : P 0 w), Absurd H (ForallElim (ForallElim L1 0) w))). -Theorem T3 (A : Type U) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y := +Theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y := Refute (fun R : not (exists x y, P x y), let L1 : forall x y, not (P x y) := ForallIntro (fun a, ForallIntro (fun b, diff --git a/tests/lean/norm1.lean b/tests/lean/norm1.lean index 28a17f05d..7a434f154 100644 --- a/tests/lean/norm1.lean +++ b/tests/lean/norm1.lean @@ -8,7 +8,7 @@ Eval fun f : N -> N, (fun x y : N, g x) (f a) Eval fun (a : N) (f : N -> N) (g : (N -> N) -> N -> N) (h : N -> N -> N), (fun (x : N) (y : N) (z : N), h x y) (g (fun x : N, f (f x)) (f a)) (f a) Eval fun (a b : N) (g : Bool -> N), (fun x y : Bool, g x) (a == b) -Eval fun (a : Type) (b : a -> Type) (g : Type U -> Bool), (fun x y : Type U, g x) (Pi x : a, b x) +Eval fun (a : Type) (b : a -> Type) (g : (Type U) -> Bool), (fun x y : (Type U), g x) (Pi x : a, b x) Eval fun f : N -> N, (fun x y z : N, g x) (f a) Eval fun f g : N -> N, (fun x y z : N, g x) (f a) Eval fun f : N -> N, (fun x : N, fun y : N, fun z : N, P x y z) (f a) diff --git a/tests/lean/revapp.lean b/tests/lean/revapp.lean index bb127385d..805736798 100644 --- a/tests/lean/revapp.lean +++ b/tests/lean/revapp.lean @@ -1,4 +1,4 @@ -Definition revapp {A : Type U} {B : A -> Type U} (a : A) (f : Pi (x : A), B x) : (B a) := f a. +Definition revapp {A : (Type U)} {B : A -> (Type U)} (a : A) (f : Pi (x : A), B x) : (B a) := f a. Infixl 100 |> : revapp Eval 10 |> (fun x, x + 1) @@ -7,7 +7,7 @@ Eval 10 |> (fun x, x + 1) |> (fun x, 3 - x) |> (fun x, x + 2) -Definition revcomp {A B C: Type U} (f : A -> B) (g : B -> C) : A -> C := +Definition revcomp {A B C: (Type U)} (f : A -> B) (g : B -> C) : A -> C := fun x, g (f x) Infixl 100 #> : revcomp diff --git a/tests/lean/tactic7.lean b/tests/lean/tactic7.lean index 6bcfe2228..50334e64f 100644 --- a/tests/lean/tactic7.lean +++ b/tests/lean/tactic7.lean @@ -1,25 +1,25 @@ -Variable Eq {A : Type U+1} (a b : A) : Bool +Variable Eq {A : (Type U+1)} (a b : A) : Bool Infix 50 === : Eq -Axiom EqSubst {A : Type U+1} {a b : A} (P : A -> Bool) (H1 : P a) (H2 : a === b) : P b -Axiom EqRefl {A : Type U+1} (a : A) : a === a -Theorem EqSymm {A : Type U+1} {a b : A} (H : a === b) : b === a := +Axiom EqSubst {A : (Type U+1)} {a b : A} (P : A -> Bool) (H1 : P a) (H2 : a === b) : P b +Axiom EqRefl {A : (Type U+1)} (a : A) : a === a +Theorem EqSymm {A : (Type U+1)} {a b : A} (H : a === b) : b === a := EqSubst (fun x, x === a) (EqRefl a) H -Theorem EqTrans {A : Type U+1} {a b c : A} (H1 : a === b) (H2 : b === c) : a === c := +Theorem EqTrans {A : (Type U+1)} {a b c : A} (H1 : a === b) (H2 : b === c) : a === c := EqSubst (fun x, a === x) H1 H2 -Theorem EqCongr {A B : Type U+1} (f : A -> B) {a b : A} (H : a === b) : (f a) === (f b) := +Theorem EqCongr {A B : (Type U+1)} (f : A -> B) {a b : A} (H : a === b) : (f a) === (f b) := EqSubst (fun x, (f a) === (f x)) (EqRefl (f a)) H -Theorem EqCongr1 {A : Type U+1} {B : A -> Type U+1} {f g : Pi x : A, B x} (a : A) (H : f === g) : (f a) === (g a) := +Theorem EqCongr1 {A : (Type U+1)} {B : A -> (Type U+1)} {f g : Pi x : A, B x} (a : A) (H : f === g) : (f a) === (g a) := EqSubst (fun h : (Pi x : A, B x), (f a) === (h a)) (EqRefl (f a)) H Axiom ProofIrrelevance (P : Bool) (pr1 pr2 : P) : pr1 === pr2 -Axiom EqCast {A B : Type U} (H : A === B) (a : A) : B -Axiom EqCastHom {A B : Type U} {a1 a2 : A} (HAB : A === B) (H : a1 === a2) : (EqCast HAB a1) === (EqCast HAB a2) -Axiom EqCastRefl {A : Type U} (a : A) : (EqCast (EqRefl A) a) === a +Axiom EqCast {A B : (Type U)} (H : A === B) (a : A) : B +Axiom EqCastHom {A B : (Type U)} {a1 a2 : A} (HAB : A === B) (H : a1 === a2) : (EqCast HAB a1) === (EqCast HAB a2) +Axiom EqCastRefl {A : (Type U)} (a : A) : (EqCast (EqRefl A) a) === a Variable Vector : (Type U) -> Nat -> (Type U) -Variable empty {A : Type U} : Vector A 0 -Variable append {A : Type U} {m n : Nat} (v1 : Vector A m) (v2 : Vector A n) : Vector A (m + n) +Variable empty {A : (Type U)} : Vector A 0 +Variable append {A : (Type U)} {m n : Nat} (v1 : Vector A m) (v2 : Vector A n) : Vector A (m + n) Axiom Plus0 (n : Nat) : (n + 0) === n -Theorem VectorPlus0 (A : Type U) (n : Nat) : (Vector A (n + 0)) === (Vector A n) := +Theorem VectorPlus0 (A : (Type U)) (n : Nat) : (Vector A (n + 0)) === (Vector A n) := EqSubst (fun x : Nat, (Vector A x) === (Vector A n)) (EqRefl (Vector A n)) (EqSymm (Plus0 n)) @@ -27,8 +27,8 @@ SetOption pp::implicit true (* Check fun (A : Type) (n : Nat), VectorPlus0 A n *) Axiom AppendNil {A : Type} {n : Nat} (v : Vector A n) : (EqCast (VectorPlus0 A n) (append v empty)) === v -Variable List : Type U -> Type U. -Variables A B : Type U +Variable List : (Type U) -> (Type U). +Variables A B : (Type U) Axiom H1 : A === B. Theorem LAB : (List A) === (List B) := EqCongr List H1 @@ -38,13 +38,13 @@ Variable H2 : (EqCast LAB l1) == l2 (* -Theorem EqCastInv {A B : Type U} (H : A === B) (a : A) : (EqCast (EqSymm H) (EqCast H a)) === a := +Theorem EqCastInv {A B : (Type U)} (H : A === B) (a : A) : (EqCast (EqSymm H) (EqCast H a)) === a := *) (* -Variable ReflCast : Pi (A : Type U) (a : A) (H : Eq (Type U) A A), Eq A (Casting A A H a) a -Theorem AppEq (A : Type U) (B : A -> Type U) (a b : A) (H : Eq A a b) : (Eq (Type U) (B b) (B a)) := +Variable ReflCast : Pi (A : (Type U)) (a : A) (H : Eq (Type U) A A), Eq A (Casting A A H a) a +Theorem AppEq (A : (Type U)) (B : A -> (Type U)) (a b : A) (H : Eq A a b) : (Eq (Type U) (B b) (B a)) := EqCongr A (Type U) B b a (EqSymm A a b H) -Theorem EqCongr2 (A : Type U) (B : A -> Type U) (f : Pi x : A, B x) (a b : A) (H : Eq A a b) : Eq (B a) (f a) (Casting (B b) (B a) (AppEq A B a b H) (f a)) (f b) := +Theorem EqCongr2 (A : (Type U)) (B : A -> (Type U)) (f : Pi x : A, B x) (a b : A) (H : Eq A a b) : Eq (B a) (f a) (Casting (B b) (B a) (AppEq A B a b H) (f a)) (f b) := EqSubst (B a) a b (fun x : A, Eq (B a) (f a) (Casting (B x) (B a) (AppEq A B a b H) (f a)) (f x) *) \ No newline at end of file diff --git a/tests/lean/tst15.lean b/tests/lean/tst15.lean index 1b2fedc44..5c1256f24 100644 --- a/tests/lean/tst15.lean +++ b/tests/lean/tst15.lean @@ -1,20 +1,20 @@ -Variable x : Type max U+1+2 M+1 M+2 3 +Variable x : (Type max U+1+2 M+1 M+2 3) Check x -Variable f : Type U+10 -> Type +Variable f : (Type U+10) -> Type Check f Check f x -Check Type 4 +Check (Type 4) Check x -Check Type max U M -Show Type U+3 -Check Type U+3 -Check Type U ⊔ M -Check Type U ⊔ M ⊔ 3 -Show Type U+1 ⊔ M ⊔ 3 -Check Type U+1 ⊔ M ⊔ 3 -Show Type U -> Type 5 -Check Type U -> Type 5 -Check Type M ⊔ 3 -> Type U+5 -Show Type M ⊔ 3 -> Type U -> Type 5 -Check Type M ⊔ 3 -> Type U -> Type 5 -Show Type U +Check (Type max U M) +Show (Type U+3) +Check (Type U+3) +Check (Type U ⊔ M) +Check (Type U ⊔ M ⊔ 3) +Show (Type U+1 ⊔ M ⊔ 3) +Check (Type U+1 ⊔ M ⊔ 3) +Show (Type U) -> (Type 5) +Check (Type U) -> (Type 5) +Check (Type M ⊔ 3) -> (Type U+5) +Show (Type M ⊔ 3) -> (Type U) -> (Type 5) +Check (Type M ⊔ 3) -> (Type U) -> (Type 5) +Show (Type U) diff --git a/tests/lean/tst7.lean b/tests/lean/tst7.lean index ca3cd1d30..b72d2bfab 100644 --- a/tests/lean/tst7.lean +++ b/tests/lean/tst7.lean @@ -3,7 +3,7 @@ Show fun (A B : Type) (a : _), f B a (* The following one should produce an error *) Show fun (A : Type) (a : _) (B : Type), f B a -Variable myeq : Pi (A : Type U), A -> A -> Bool +Variable myeq : Pi A : (Type U), A -> A -> Bool Show myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b) Check myeq _ (fun (A : Type) (a : _), a) (fun (B : Type) (b : B), b) diff --git a/tests/lean/ty2.lean b/tests/lean/ty2.lean index f07cbfc64..31d897482 100644 --- a/tests/lean/ty2.lean +++ b/tests/lean/ty2.lean @@ -1,5 +1,5 @@ -Definition B : Type := Bool -Definition T : Type 1 := Type +Definition B : Type := Bool +Definition T : (Type 1) := Type Variable N : T Variable x : N Variable a : B