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

refactor(library/init/meta): free_var ==> local_const

Browse source 
Use the same names used in the C++ version
This commit is contained in:
Leonardo de Moura 2016-06-22 14:46:42 -07:00
parent 1e005e185a
commit f0ec88c1d3
4 changed files with 34 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
library/init/meta/expr.lean
View file

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

2
library/init/meta/tactic.lean
View file

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

16
src/library/vm/vm_expr.cpp
View file

@ -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<expr> & 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<expr> 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);

16
tests/lean/run/meta_expr1.lean
View file

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