michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/parser): parse_type method

Browse source 
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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-19 15:15:32 -08:00
parent 46627289b8
commit ae01d3818d
12 changed files with 57 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/frontends/lean/parser.cpp
View file

@ -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 <tt>'Type'</tt> and <tt>'Type' level</tt> 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 <universe>)' 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;
}
}

2
src/tests/frontends/lean/parser.cpp
View file

@ -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");

6
tests/lean/conv.lean
View file

@ -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

2
tests/lean/elab6.lean
View file

@ -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))

4
tests/lean/elab7.lean
View file

@ -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

2
tests/lean/exists3.lean
View file

@ -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,

2
tests/lean/norm1.lean
View file

@ -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)

4
tests/lean/revapp.lean
View file

@ -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

38
tests/lean/tactic7.lean
View file

@ -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)
*)

32
tests/lean/tst15.lean
View file

@ -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)

2
tests/lean/tst7.lean
View file

@ -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)

4
tests/lean/ty2.lean
View file

@ -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