From a862c6e89fc8ddf216ccc9039b3201d33c39100a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 3 Sep 2016 14:58:53 -0700 Subject: [PATCH] refactor(library/init/meta/declaration): `def` will be a keyword --- library/init/meta/declaration.lean | 8 ++++---- src/library/vm/vm_declaration.cpp | 4 ++-- tests/lean/eqn_sanitizer1.lean.expected.out | 2 +- tests/lean/run/meta_env1.lean | 18 +++++++++--------- tests/lean/run/run_tactic1.lean | 4 ++-- 5 files changed, 18 insertions(+), 18 deletions(-) diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean index 0bef49c8ba..0c45bdaefd 100644 --- a/library/init/meta/declaration.lean +++ b/library/init/meta/declaration.lean @@ -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 diff --git a/src/library/vm/vm_declaration.cpp b/src/library/vm/vm_declaration.cpp index f30e6d3d17..bf15e2d1aa 100644 --- a/src/library/vm/vm_declaration.cpp +++ b/src/library/vm/vm_declaration.cpp @@ -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); diff --git a/tests/lean/eqn_sanitizer1.lean.expected.out b/tests/lean/eqn_sanitizer1.lean.expected.out index 5b7df6f4a8..6e8b5b0779 100644 --- a/tests/lean/eqn_sanitizer1.lean.expected.out +++ b/tests/lean/eqn_sanitizer1.lean.expected.out @@ -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) diff --git a/tests/lean/run/meta_env1.lean b/tests/lean/run/meta_env1.lean index 78b9ab187c..cf59517eee 100644 --- a/tests/lean/run/meta_env1.lean +++ b/tests/lean/run/meta_env1.lean @@ -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 [])], diff --git a/tests/lean/run/run_tactic1.lean b/tests/lean/run/run_tactic1.lean index 452bff25ec..911eb68e98 100644 --- a/tests/lean/run/run_tactic1.lean +++ b/tests/lean/run/run_tactic1.lean @@ -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