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

feat(kernel): add unexpected_metavar_occurrence exception

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-24 19:56:44 -07:00
parent 83907d7c73
commit a5c3829d1b
4 changed files with 520 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/kernel/kernel_exception.h
View file

@ -198,6 +198,7 @@ public:
invalid_builtin_value_declaration(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {} invalid_builtin_value_declaration(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
virtual ~invalid_builtin_value_declaration() {} virtual ~invalid_builtin_value_declaration() {}
virtual char const * what() const noexcept { return "invalid builtin value declaration, expression is not a builtin value"; } virtual char const * what() const noexcept { return "invalid builtin value declaration, expression is not a builtin value"; }
virtual expr const & get_main_expr() const { return m_expr; }
}; };
/** /**
@ -210,5 +211,18 @@ public:
invalid_builtin_value_reference(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {} invalid_builtin_value_reference(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
virtual ~invalid_builtin_value_reference() {} virtual ~invalid_builtin_value_reference() {}
virtual char const * what() const noexcept { return "invalid builtin value reference, this kind of builtin value was not declared in the environment"; } virtual char const * what() const noexcept { return "invalid builtin value reference, this kind of builtin value was not declared in the environment"; }
virtual expr const & get_main_expr() const { return m_expr; }
};
/**
\brief Unexpected metavariable occurrence
*/
class unexpected_metavar_occurrence : public kernel_exception {
expr m_expr;
public:
unexpected_metavar_occurrence(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
virtual ~unexpected_metavar_occurrence() {}
virtual char const * what() const noexcept { return "unexpected metavariable occurrence"; }
virtual expr const & get_main_expr() const { return m_expr; }
}; };
} }

2
src/kernel/type_checker.cpp
View file

@ -99,7 +99,7 @@ class type_checker::imp {
else else
return m_menv->get_type(e); return m_menv->get_type(e);
} else { } else {
throw kernel_exception(m_env, "unexpected metavariable occurrence"); throw unexpected_metavar_occurrence(m_env, e);
} }
break; break;
case expr_kind::Constant: case expr_kind::Constant:

2
src/library/type_inferer.cpp
View file

@ -107,7 +107,7 @@ class type_inferer::imp {
else else
return m_menv->get_type(e); return m_menv->get_type(e);
} else { } else {
throw kernel_exception(m_env, "unexpected metavariable occurrence"); throw unexpected_metavar_occurrence(m_env, e);
} }
case expr_kind::Constant: { case expr_kind::Constant: {
object const & obj = m_env.get_object(const_name(e)); object const & obj = m_env.get_object(const_name(e));

548
tests/lean/elab1.lean.expected.out
View file

@ -114,8 +114,7 @@ Failed to solve
⊢ ?M3::1 ≈ nat_to_real ⊢ ?M3::1 ≈ nat_to_real
assumption 2 assumption 2
Assumed: g Assumed: g
Error (line: 7, pos: 6) unsolved placeholder at term Error (line: 7, pos: 8) unexpected metavariable occurrence
g 10
Assumed: h Assumed: h
Failed to solve Failed to solve
x : ?M3::0, A : Type ⊢ ?M3::0[lift:0:2] ≺ A x : ?M3::0, A : Type ⊢ ?M3::0[lift:0:2] ≺ A
@ -136,45 +135,506 @@ A : Type, B : Type, a : ?M3::0, b : ?M3::1, C : Type ⊢ ?M3::0[lift:0:3] ≺ C
Assumed: a Assumed: a
Assumed: b Assumed: b
Assumed: H Assumed: H
Error (line: 20, pos: 18) type mismatch during term elaboration Error (line: 20, pos: 28) unexpected metavariable occurrence
Discharge (λ H1 : _, Conj H1 (Conjunct1 H)) Failed to solve
Term after elaboration: ⊢ b ≈ a
Discharge (λ H1 : ?M4, Conj H1 (Conjunct1 H)) Destruct/Decompose
Expected type: ⊢ b = b ≺ a = ?M3::3
b Normalize
Got: ⊢ b = b ≺ ?M3::2 = ?M3::3
?M4 ⇒ ?M2 (line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of
Elaborator state Trans::explicit
?M2[lift:0:1] ≈ (?M4[lift:0:1]) ∧ a with arguments:
b ≈ if Bool ?M4 ?M2 ⊤ ?M3::0
b ≈ if Bool ?M4 ?M2 ⊤ ?M3::1
Error (line: 22, pos: 22) type mismatch at application ?M3::2
Trans (Refl a) (Refl b) ?M3::3
Function type: Refl a
Π (A : Type U) (a b c : A), (a = b) → (b = c) → (a = c) Refl b
Arguments types: Failed to solve
Bool : Type ⊢ (?M3::0 ≈ Type) ⊕ (?M3::0 ≈ Type 1) ⊕ (?M3::0 ≈ Type 2) ⊕ (?M3::0 ≈ Type M) ⊕ (?M3::0 ≈ Type U)
a : Bool Destruct/Decompose
a : Bool ⊢ Type ≺ ?M3::0
b : Bool (line: 24: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
Refl a : a = a f::explicit
Refl b : b = b with arguments:
Error (line: 24, pos: 6) type mismatch at application ?M3::0
f Bool Bool Bool
Function type: Bool
Π (A : Type), A → A → A Failed to solve
Arguments types: ⊢
Type : Type 1 (?M3::1 ≈ Type 1) ⊕ (?M3::1 ≈ Type 2) ⊕ (?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U)
Bool : Type Destruct/Decompose
Bool : Type ⊢ Type 1 ≺ ?M3::1
Error (line: 27, pos: 21) type mismatch at application Propagate type, ?M3::0 : ?M3::1
DisjCases (EM a) (λ H_a : a, H) (λ H_na : ¬ a, NotImp1 (MT H H_na)) Assignment
Function type: ⊢ ?M3::0 ≈ Type
Π (a b c : Bool), (a ∨ b) → (a → c) → (b → c) → c assumption 0
Arguments types: Failed to solve
a : Bool ⊢ Type 1 ≺ Type
¬ a : Bool Substitution
a : Bool ⊢ ?M3::1 ≺ Type
EM a : a ∨ ¬ a (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
(λ H_a : a, H) : a → ((a ⇒ b) ⇒ a) f::explicit
(λ H_na : ¬ a, NotImp1 (MT H H_na)) : (¬ a) → a with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type 1
assumption 1
Failed to solve
⊢ Type 2 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type 2
assumption 2
Failed to solve
⊢ Type 3 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type 3
assumption 3
Failed to solve
⊢ Type M ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type M
assumption 4
Failed to solve
⊢ Type U ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type U
assumption 5
Failed to solve
⊢
(?M3::1 ≈ Type 2) ⊕ (?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type 4) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U)
Destruct/Decompose
⊢ Type 2 ≺ ?M3::1
Propagate type, ?M3::0 : ?M3::1
Assignment
⊢ ?M3::0 ≈ Type 1
assumption 6
Failed to solve
⊢ Type 2 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type 2
assumption 7
Failed to solve
⊢ Type 3 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type 3
assumption 8
Failed to solve
⊢ Type 4 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type 4
assumption 9
Failed to solve
⊢ Type M ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type M
assumption 10
Failed to solve
⊢ Type U ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type U
assumption 11
Failed to solve
⊢
(?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type 4) ⊕ (?M3::1 ≈ Type 5) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U)
Destruct/Decompose
⊢ Type 3 ≺ ?M3::1
Propagate type, ?M3::0 : ?M3::1
Assignment
⊢ ?M3::0 ≈ Type 2
assumption 12
Failed to solve
⊢ Type 3 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type 3
assumption 13
Failed to solve
⊢ Type 4 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type 4
assumption 14
Failed to solve
⊢ Type 5 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type 5
assumption 15
Failed to solve
⊢ Type M ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type M
assumption 16
Failed to solve
⊢ Type U ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type U
assumption 17
Failed to solve
⊢
(?M3::1 ≈ Type M+1) ⊕
(?M3::1 ≈ Type M+2) ⊕
(?M3::1 ≈ Type M+3) ⊕
(?M3::1 ≈ Type M) ⊕
(?M3::1 ≈ Type U)
Destruct/Decompose
⊢ Type M+1 ≺ ?M3::1
Propagate type, ?M3::0 : ?M3::1
Assignment
⊢ ?M3::0 ≈ Type M
assumption 18
Failed to solve
⊢ Type M+1 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type M+1
assumption 19
Failed to solve
⊢ Type M+2 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type M+2
assumption 20
Failed to solve
⊢ Type M+3 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type M+3
assumption 21
Failed to solve
⊢ Type M ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type M
assumption 22
Failed to solve
⊢ Type U ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type U
assumption 23
Failed to solve
⊢
(?M3::1 ≈ Type U+1) ⊕
(?M3::1 ≈ Type U+2) ⊕
(?M3::1 ≈ Type U+3) ⊕
(?M3::1 ≈ Type M) ⊕
(?M3::1 ≈ Type U)
Destruct/Decompose
⊢ Type U+1 ≺ ?M3::1
Propagate type, ?M3::0 : ?M3::1
Assignment
⊢ ?M3::0 ≈ Type U
assumption 24
Failed to solve
⊢ Type U+1 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type U+1
assumption 25
Failed to solve
⊢ Type U+2 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type U+2
assumption 26
Failed to solve
⊢ Type U+3 ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type U+3
assumption 27
Failed to solve
⊢ Type M ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type M
assumption 28
Failed to solve
⊢ Type U ≺ Type
Substitution
⊢ ?M3::1 ≺ Type
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
?M3::0
Bool
Bool
Assignment
⊢ ?M3::1 ≈ Type U
assumption 29
Failed to solve
a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≺ if Bool (if Bool a b ⊤) a ⊤
Substitution
a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≺ ?M3::5[lift:0:1]
Substitution
a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ ?M3::8 ≺ ?M3::5[lift:0:1]
Destruct/Decompose
a : Bool, b : Bool, H : ?M3::2 ⊢ Π H_na : ?M3::7, ?M3::8 ≺ Π _ : ?M3::4, ?M3::5[lift:0:1]
(line: 27: pos: 21) Type of argument 6 must be convertible to the expected type in the application of
DisjCases::explicit
with arguments:
?M3::3
?M3::4
?M3::5
EM a
λ H_a : ?M3::6, H
λ H_na : ?M3::7, NotImp1 (MT H H_na)
Assignment
a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≈ ?M3::8
Destruct/Decompose
a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ if Bool a b ⊤ ≈ if Bool ?M3::8 ?M3::9 ⊤
Destruct/Decompose
a : Bool,
b : Bool,
H : ?M3::2,
H_na : ?M3::7 ⊢
if Bool (if Bool a b ⊤) a ⊤ ≺ if Bool (if Bool ?M3::8 ?M3::9 ⊤) ?M3::11 ⊤
Normalize
a : Bool,
b : Bool,
H : ?M3::2,
H_na : ?M3::7 ⊢
(a ⇒ b) ⇒ a ≺ if Bool ?M3::10 ?M3::11 ⊤
Substitution
a : Bool,
b : Bool,
H : ?M3::2,
H_na : ?M3::7 ⊢
?M3::2[lift:0:2] ≺ if Bool ?M3::10 ?M3::11 ⊤
Normalize
a : Bool,
b : Bool,
H : ?M3::2,
H_na : ?M3::7 ⊢
?M3::2[lift:0:2] ≺ ?M3::10 ⇒ ?M3::11
(line: 29: pos: 48) Type of argument 3 must be convertible to the expected type in the application of
MT::explicit
with arguments:
?M3::10
?M3::11
H
H_na
Assignment
a : Bool, b : Bool ⊢ ?M3::2 ≈ ?M3::0
Destruct/Decompose
a : Bool, b : Bool ⊢ Π H : ?M3::2, ?M3::5 ≺ Π _ : ?M3::0, ?M3::1[lift:0:1]
(line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
Discharge::explicit
with arguments:
?M3::0
?M3::1
λ H : ?M3::2,
DisjCases
(EM a)
(λ H_a : ?M3::6, H)
(λ H_na : ?M3::7, NotImp1 (MT H H_na))
Assignment
a : Bool, b : Bool, H : ?M3::2 ⊢ if Bool (if Bool a b ⊤) a ⊤ ≺ ?M3::5
Normalize
a : Bool, b : Bool, H : ?M3::2 ⊢ (a ⇒ b) ⇒ a ≺ ?M3::5
Normalize
a : Bool, b : Bool, H : ?M3::2, H_a : ?M3::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M3::5[lift:0:1]
Substitution
a : Bool, b : Bool, H : ?M3::2, H_a : ?M3::6 ⊢ ?M3::2[lift:0:2] ≺ ?M3::5[lift:0:1]
Destruct/Decompose
a : Bool,
b : Bool,
H : ?M3::2 ⊢
Π H_a : ?M3::6, ?M3::2[lift:0:2] ≺ Π _ : ?M3::3, ?M3::5[lift:0:1]
(line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of
DisjCases::explicit
with arguments:
?M3::3
?M3::4
?M3::5
EM a
λ H_a : ?M3::6, H
λ H_na : ?M3::7, NotImp1 (MT H H_na)
Assignment
a : Bool, b : Bool ⊢ ?M3::2 ≈ ?M3::0
Destruct/Decompose
a : Bool, b : Bool ⊢ Π H : ?M3::2, ?M3::5 ≺ Π _ : ?M3::0, ?M3::1[lift:0:1]
(line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
Discharge::explicit
with arguments:
?M3::0
?M3::1
λ H : ?M3::2,
DisjCases (EM a) (λ H_a : ?M3::6, H) (λ H_na : ?M3::7, NotImp1 (MT H H_na))