max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/init/meta/declaration): def will be a keyword

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-03 14:58:53 -07:00
parent 029766495b
commit a862c6e89f
5 changed files with 18 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/meta/declaration.lean
View file

@ -9,7 +9,7 @@ import init.meta.expr init.meta.name
/- Reflect a C++ declaration object. The VM replaces it with the C++ implementation. -/
inductive declaration
/- definition: name, list universe parameters, type, value, is_trusted -/
| def : name → list name → expr → expr → bool → declaration
| defn : name → list name → expr → expr → bool → declaration
/- theorem: name, list universe parameters, type, value (remark: theorems are always trusted) -/
| thm : name → list name → expr → expr → declaration
/- constant assumption: name, list universe parameters, type, is_trusted -/
@ -18,19 +18,19 @@ inductive declaration
| ax : name → list name → expr → declaration
definition declaration.to_name : declaration → name
| (declaration.def n ls t v tr) := n
| (declaration.defn n ls t v tr) := n
| (declaration.thm n ls t v) := n
| (declaration.cnst n ls t tr) := n
| (declaration.ax n ls t) := n
definition declaration.univ_params : declaration → list name
| (declaration.def n ls t v tr) := ls
| (declaration.defn n ls t v tr) := ls
| (declaration.thm n ls t v) := ls
| (declaration.cnst n ls t tr) := ls
| (declaration.ax n ls t) := ls
definition declaration.type : declaration → expr
| (declaration.def n ls t v tr) := t
| (declaration.defn n ls t v tr) := t
| (declaration.thm n ls t v) := t
| (declaration.cnst n ls t tr) := t
| (declaration.ax n ls t) := t

4
src/library/vm/vm_declaration.cpp
View file

@ -28,7 +28,7 @@ vm_obj to_obj(declaration const & n) {
return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_declaration))) vm_declaration(n));
}
vm_obj declaration_def(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & value,
vm_obj declaration_defn(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & value,
vm_obj const & trusted) {
return to_obj(mk_definition(to_name(n), to_list_name(ls), to_expr(type), to_expr(value), 0, true, to_bool(trusted)));
}
@ -93,7 +93,7 @@ vm_obj declaration_instantiate_value_univ_params(vm_obj const & _d, vm_obj const
}
void initialize_vm_declaration() {
DECLARE_VM_BUILTIN(name({"declaration", "def"}), declaration_def);
DECLARE_VM_BUILTIN(name({"declaration", "defn"}), declaration_defn);
DECLARE_VM_BUILTIN(name({"declaration", "thm"}), declaration_thm);
DECLARE_VM_BUILTIN(name({"declaration", "cnst"}), declaration_cnst);
DECLARE_VM_BUILTIN(name({"declaration", "ax"}), declaration_ax);

2
tests/lean/eqn_sanitizer1.lean.expected.out
View file

@ -1,2 +1,2 @@
definition fib._main.equations.eqn_3 : ∀ (n : ℕ), fib._main (n + 2) = fib._main (n + 1) + fib._main n :=
λ n, eq.refl (fib._main (n + 2))
λ n, eq.refl (fib._main (nat.succ n) + fib._main n)

18
tests/lean/run/meta_env1.lean
View file

@ -5,12 +5,12 @@ meta_definition e := environment.mk_std 0
vm_eval environment.trust_lvl e
vm_eval environment.is_std e
vm_eval (environment.add e (declaration.def `foo []
(expr.sort (level.succ (level.zero)))
(expr.sort (level.succ (level.zero)))
bool.tt) : exceptional environment)
vm_eval (environment.add e (declaration.defn `foo []
(expr.sort (level.succ (level.zero)))
(expr.sort (level.succ (level.zero)))
bool.tt) : exceptional environment)
meta_definition e1 := (environment.add e (declaration.def `foo []
meta_definition e1 := (environment.add e (declaration.defn `foo []
(expr.sort (level.succ (level.zero)))
(expr.sort level.zero)
bool.tt) : exceptional environment)
@ -19,10 +19,10 @@ print "-----------"
open name
vm_eval do
e₁ ← environment.add e (declaration.def `foo []
(expr.sort (level.succ (level.zero)))
(expr.sort level.zero)
bool.tt),
e₁ ← environment.add e (declaration.defn `foo []
(expr.sort (level.succ (level.zero)))
(expr.sort level.zero)
bool.tt),
e₂ ← environment.add_inductive e₁ `Two [] 0 (expr.sort (level.succ level.zero))
[(`Zero, expr.const `Two []),
(`One, expr.const `Two [])],

4
tests/lean/run/run_tactic1.lean
View file

@ -5,7 +5,7 @@ run_command tactic.trace "hello world"
run_command do
N ← to_expr `(nat),
v ← to_expr `(10),
add_decl (declaration.def `val10 [] N v tt)
add_decl (declaration.defn `val10 [] N v tt)
vm_eval val10
@ -16,7 +16,7 @@ meta_definition mk_defs : nat → command
| (n+1) := do
N ← to_expr `(nat),
v ← expr_of_nat n,
add_decl (declaration.def (name.append_after `val n) [] N v tt),
add_decl (declaration.defn (name.append_after `val n) [] N v tt),
mk_defs n
run_command mk_defs 10