From f0ec88c1d38405f6af320b08f34e6cce0342faae Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Jun 2016 14:46:42 -0700 Subject: [PATCH] refactor(library/init/meta): free_var ==> local_const Use the same names used in the C++ version --- library/init/meta/expr.lean | 34 +++++++++++++++++----------------- library/init/meta/tactic.lean | 2 +- src/library/vm/vm_expr.cpp | 16 ++++++++-------- tests/lean/run/meta_expr1.lean | 16 ++++++++-------- 4 files changed, 34 insertions(+), 34 deletions(-) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 3675382fce..579204f7ed 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -13,16 +13,16 @@ meta_constant macro_def : Type₁ /- Reflect a C++ expr object. The VM replaces it with the C++ implementation. -/ inductive expr := -| var : unsigned → expr -| sort : level → expr -| const : name → list level → expr -| meta : name → expr → expr -| free_var : name → name → binder_info → expr → expr -| app : expr → expr → expr -| lam : name → binder_info → expr → expr → expr -| pi : name → binder_info → expr → expr → expr -| elet : name → expr → expr → expr → expr -| macro : macro_def → ∀ n : unsigned, (fin (unsigned.to_nat n) → expr) → expr +| var : unsigned → expr +| sort : level → expr +| const : name → list level → expr +| meta : name → expr → expr +| local_const : name → name → binder_info → expr → expr +| app : expr → expr → expr +| lam : name → binder_info → expr → expr → expr +| pi : name → binder_info → expr → expr → expr +| elet : name → expr → expr → expr → expr +| macro : macro_def → ∀ n : unsigned, (fin (unsigned.to_nat n) → expr) → expr definition expr.is_inhabited [instance] : inhabited expr := inhabited.mk (expr.sort level.zero) @@ -49,18 +49,18 @@ else ordering.gt meta_constant expr.fold {A :Type} : expr → A → (expr → unsigned → A → A) → A -meta_constant expr.abstract_fv : expr → name → expr -meta_constant expr.abstract_fvs : expr → list name → expr +meta_constant expr.abstract_local : expr → name → expr +meta_constant expr.abstract_locals : expr → list name → expr meta_constant expr.instantiate_var : expr → expr → expr meta_constant expr.instantiate_vars : expr → list expr → expr -meta_constant expr.has_var : expr → bool -meta_constant expr.has_var_idx : expr → nat → bool -meta_constant expr.has_free_var : expr → bool +meta_constant expr.has_var : expr → bool +meta_constant expr.has_var_idx : expr → nat → bool +meta_constant expr.has_local : expr → bool meta_constant expr.has_meta_var : expr → bool -meta_constant expr.lift_vars : expr → nat → nat → expr -meta_constant expr.lower_vars : expr → nat → nat → expr +meta_constant expr.lift_vars : expr → nat → nat → expr +meta_constant expr.lower_vars : expr → nat → nat → expr namespace expr open bool decidable option diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 0e80a70ca7..51a8773cbe 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -320,7 +320,7 @@ do u ← mk_meta_univ, private meta_definition get_arity_aux : expr → tactic nat | (expr.pi n bi d b) := do m ← mk_fresh_name, - l ← return (expr.free_var m n bi d), + l ← return (expr.local_const m n bi d), new_b ← whnf (expr.instantiate_var b l), r ← get_arity_aux new_b, return (r + 1) diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index e886d3f627..60b7bc87a2 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -100,7 +100,7 @@ vm_obj expr_meta(vm_obj const & n, vm_obj const & t) { return to_obj(mk_metavar(to_name(n), to_expr(t))); } -vm_obj expr_free_var(vm_obj const & n, vm_obj const & ppn, vm_obj const & bi, vm_obj const & t) { +vm_obj expr_local_const(vm_obj const & n, vm_obj const & ppn, vm_obj const & bi, vm_obj const & t) { return to_obj(mk_local(to_name(n), to_name(ppn), to_expr(t), to_binder_info(bi))); } @@ -231,7 +231,7 @@ vm_obj expr_instantiate_vars(vm_obj const & e, vm_obj const & vs) { return to_obj(instantiate(to_expr(e), vs_buf.size(), vs_buf.data())); } -vm_obj expr_abstract_fv(vm_obj const & e, vm_obj const & n) { +vm_obj expr_abstract_local(vm_obj const & e, vm_obj const & n) { return to_obj(abstract_local(to_expr(e), to_name(n))); } @@ -245,7 +245,7 @@ static void list_name_to_buffer_local(vm_obj const & o, buffer & r) { } } -vm_obj expr_abstract_fvs(vm_obj const & e, vm_obj const & ns) { +vm_obj expr_abstract_locals(vm_obj const & e, vm_obj const & ns) { buffer locals; list_name_to_buffer_local(ns, locals); return to_obj(abstract_locals(to_expr(e), locals.size(), locals.data())); @@ -263,7 +263,7 @@ vm_obj expr_has_var_idx(vm_obj const & e, vm_obj const & u) { } } -vm_obj expr_has_free_var(vm_obj const & e) { +vm_obj expr_has_local(vm_obj const & e) { return mk_vm_bool(has_local(to_expr(e))); } @@ -294,7 +294,7 @@ void initialize_vm_expr() { DECLARE_VM_BUILTIN(name({"expr", "sort"}), expr_sort); DECLARE_VM_BUILTIN(name({"expr", "const"}), expr_const); DECLARE_VM_BUILTIN(name({"expr", "meta"}), expr_meta); - DECLARE_VM_BUILTIN(name({"expr", "free_var"}), expr_free_var); + DECLARE_VM_BUILTIN(name({"expr", "local_const"}), expr_local_const); DECLARE_VM_BUILTIN(name({"expr", "app"}), expr_app); DECLARE_VM_BUILTIN(name({"expr", "lam"}), expr_lam); DECLARE_VM_BUILTIN(name({"expr", "pi"}), expr_pi); @@ -310,11 +310,11 @@ void initialize_vm_expr() { DECLARE_VM_BUILTIN(name({"expr", "fold"}), expr_fold); DECLARE_VM_BUILTIN(name({"expr", "instantiate_var"}), expr_instantiate_var); DECLARE_VM_BUILTIN(name({"expr", "instantiate_vars"}), expr_instantiate_vars); - DECLARE_VM_BUILTIN(name({"expr", "abstract_fv"}), expr_abstract_fv); - DECLARE_VM_BUILTIN(name({"expr", "abstract_fvs"}), expr_abstract_fvs); + DECLARE_VM_BUILTIN(name({"expr", "abstract_local"}), expr_abstract_local); + DECLARE_VM_BUILTIN(name({"expr", "abstract_locals"}), expr_abstract_locals); DECLARE_VM_BUILTIN(name({"expr", "has_var"}), expr_has_var); DECLARE_VM_BUILTIN(name({"expr", "has_var_idx"}), expr_has_var_idx); - DECLARE_VM_BUILTIN(name({"expr", "has_free_var"}), expr_has_free_var); + DECLARE_VM_BUILTIN(name({"expr", "has_local"}), expr_has_local); DECLARE_VM_BUILTIN(name({"expr", "has_meta_var"}), expr_has_meta_var); DECLARE_VM_BUILTIN(name({"expr", "lift_vars"}), expr_lift_vars); DECLARE_VM_BUILTIN(name({"expr", "lower_vars"}), expr_lower_vars); diff --git a/tests/lean/run/meta_expr1.lean b/tests/lean/run/meta_expr1.lean index 578169a7bf..54a0f106e0 100644 --- a/tests/lean/run/meta_expr1.lean +++ b/tests/lean/run/meta_expr1.lean @@ -33,18 +33,18 @@ vm_eval expr.instantiate_var v1 (expr.const "a" []) vm_eval expr.instantiate_vars v1 [expr.const "a" [], expr.const "b" []] meta_definition fv1 := (expr.const "f" []) - (expr.free_var "a" "a" binder_info.default (expr.sort level.zero)) - (expr.free_var "b" "b" binder_info.default (expr.sort level.zero)) + (expr.local_const "a" "a" binder_info.default (expr.sort level.zero)) + (expr.local_const "b" "b" binder_info.default (expr.sort level.zero)) vm_eval fv1 -vm_eval expr.abstract_fv (expr.abstract_fv fv1 "a") "b" -vm_eval expr.abstract_fvs fv1 ["a", "b"] -vm_eval expr.abstract_fvs fv1 ["b", "a"] -vm_eval expr.lift_vars (expr.abstract_fvs fv1 ["b", "a"]) 1 1 -vm_eval expr.has_free_var fv1 +vm_eval expr.abstract_local (expr.abstract_local fv1 "a") "b" +vm_eval expr.abstract_locals fv1 ["a", "b"] +vm_eval expr.abstract_locals fv1 ["b", "a"] +vm_eval expr.lift_vars (expr.abstract_locals fv1 ["b", "a"]) 1 1 +vm_eval expr.has_local fv1 vm_eval expr.has_var fv1 -vm_eval expr.has_var (expr.abstract_fvs fv1 ["b", "a"]) +vm_eval expr.has_var (expr.abstract_locals fv1 ["b", "a"]) meta_definition foo : nat → expr | 0 := expr.const "aa" [level.zero, level.succ level.zero]