From 91d2ad592504e067be37db8222bef58eb34debb6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Jun 2018 10:54:43 -0700 Subject: [PATCH] chore(library/init/meta): remove `level` and `expr` unused functions --- library/init/meta/expr.lean | 199 ++++------------------------------- library/init/meta/level.lean | 16 --- src/library/vm/vm_expr.cpp | 11 -- src/library/vm/vm_level.cpp | 66 ------------ 4 files changed, 20 insertions(+), 272 deletions(-) diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 5a4bb2cd4c..e3b3fa4624 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -21,29 +21,11 @@ else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₁ h meta instance : has_to_format pos := ⟨λ ⟨l, c⟩, "⟨" ++ l ++ ", " ++ c ++ "⟩"⟩ -export lean (expr binder_info kvmap expr.bvar expr.fvar expr.sort expr.const expr.mvar expr.app expr.lam expr.pi expr.elet expr.lit expr.mdata expr.proj expr.quote - binder_info.default binder_info.implicit binder_info.strict_implicit binder_info.inst_implicit binder_info.aux_decl) +export lean (expr binder_info kvmap expr.bvar expr.fvar expr.sort expr.const expr.mvar expr.app expr.lam expr.pi expr.elet expr.lit expr.mdata expr.proj expr.quote) -instance : has_repr binder_info := -⟨λ bi, match bi with -| binder_info.default := "default" -| binder_info.implicit := "implicit" -| binder_info.strict_implicit := "strict_implicit" -| binder_info.inst_implicit := "inst_implicit" -| binder_info.aux_decl := "aux_decl"⟩ - -meta def expr.mk_bvar (n : nat) : expr := +def expr.mk_bvar (n : nat) : expr := expr.bvar n -/- Expressions can be annotated using the annotation macro. -/ -meta constant lean.expr.is_annotation : expr → option (name × expr) - -meta def lean.expr.erase_annotations : expr → expr -| e := - match e.is_annotation with - | some (_, a) := lean.expr.erase_annotations a - | none := e - /-- Compares expressions, including binder names. -/ meta constant lean.expr.has_decidable_eq : decidable_eq expr attribute [instance] lean.expr.has_decidable_eq @@ -110,212 +92,71 @@ meta instance {α} (a : α) : has_to_format (reflected a) := namespace lean.expr open decidable -meta def lean.expr.lt_prop (a b : expr) : Prop := -lean.expr.lt a b = tt - -meta instance : decidable_rel lean.expr.lt_prop := -λ a b, bool.decidable_eq _ _ - -/-- Compares expressions, ignoring binder names, and sorting by hash. -/ -meta instance : has_lt expr := -⟨ lean.expr.lt_prop ⟩ - -meta def mk_true : expr := -const `true [] - -meta def mk_false : expr := -const `false [] - -meta def is_bvar : expr → bool -| (bvar _) := tt -| _ := ff - -meta def app_of_list : expr → list expr → expr -| f [] := f -| f (p::ps) := app_of_list (f p) ps - -meta def is_app : expr → bool -| (app f a) := tt -| e := ff - -meta def app_fn : expr → expr +def app_fn : expr → expr | (app f a) := f | a := a -meta def app_arg : expr → expr +def app_arg : expr → expr | (app f a) := a | a := a -meta def get_app_fn : expr → expr +def get_app_fn : expr → expr | (app f a) := get_app_fn f | a := a -meta def get_app_num_args : expr → nat +def get_app_num_args : expr → nat | (app f a) := get_app_num_args f + 1 | e := 0 -meta def get_app_args_aux : list expr → expr → list expr +def get_app_args_aux : list expr → expr → list expr | r (app f a) := get_app_args_aux (a::r) f | r e := r -meta def get_app_args : expr → list expr := +def get_app_args : expr → list expr := get_app_args_aux [] -meta def mk_app : expr → list expr → expr +def mk_app : expr → list expr → expr | e [] := e -| e (x::xs) := mk_app (e x) xs +| e (x::xs) := mk_app (lean.expr.app e x) xs -meta def ith_arg_aux : expr → nat → expr -| (app f a) 0 := a -| (app f a) (n+1) := ith_arg_aux f n -| e _ := e - -meta def ith_arg (e : expr) (i : nat) : expr := -ith_arg_aux e (get_app_num_args e - i - 1) - -meta def const_name : expr → name +def const_name : expr → name | (const n ls) := n | e := name.anonymous -meta def is_constant : expr → bool +def is_constant : expr → bool | (const n ls) := tt | e := ff -meta def is_fvar : expr → bool +def is_fvar : expr → bool | (fvar n) := tt | e := ff -meta def fvar_id : expr → name +def fvar_id : expr → name | (fvar n) := n | e := name.anonymous -meta def is_constant_of : expr → name → bool +def is_constant_of : expr → name → bool | (const n₁ ls) n₂ := n₁ = n₂ | e n := ff -meta def is_app_of (e : expr) (n : name) : bool := +def is_app_of (e : expr) (n : name) : bool := is_constant_of (get_app_fn e) n -meta def is_napp_of (e : expr) (c : name) (n : nat) : bool := +def is_napp_of (e : expr) (c : name) (n : nat) : bool := is_app_of e c ∧ get_app_num_args e = n -meta def is_false : expr → bool -| `(false) := tt -| _ := ff - -meta def is_not : expr → option expr -| `(not %%a) := some a -| `(%%a → false) := some a -| e := none - -meta def is_and : expr → option (expr × expr) -| `(and %%α %%β) := some (α, β) -| _ := none - -meta def is_or : expr → option (expr × expr) -| `(or %%α %%β) := some (α, β) -| _ := none - -meta def is_iff : expr → option (expr × expr) -| `((%%a : Prop) ↔ %%b) := some (a, b) -| _ := none - -meta def is_eq : expr → option (expr × expr) +def is_eq : expr → option (expr × expr) | `((%%a : %%_) = %%b) := some (a, b) | _ := none -meta def is_ne : expr → option (expr × expr) -| `((%%a : %%_) ≠ %%b) := some (a, b) -| _ := none - -meta def is_bin_arith_app (e : expr) (op : name) : option (expr × expr) := -if is_napp_of e op 4 -then some (app_arg (app_fn e), app_arg e) -else none - -meta def is_lt (e : expr) : option (expr × expr) := -is_bin_arith_app e ``has_lt.lt - -meta def is_gt (e : expr) : option (expr × expr) := -is_bin_arith_app e ``gt - -meta def is_le (e : expr) : option (expr × expr) := -is_bin_arith_app e ``has_le.le - -meta def is_ge (e : expr) : option (expr × expr) := -is_bin_arith_app e ``ge - -meta def is_heq : expr → option (expr × expr × expr × expr) -| `(@heq %%α %%a %%β %%b) := some (α, a, β, b) -| _ := none - -meta def is_lambda : expr → bool -| (lam _ _ _ _) := tt -| e := ff - -meta def is_pi : expr → bool +def is_pi : expr → bool | (pi _ _ _ _) := tt | e := ff -meta def is_let : expr → bool +def is_let : expr → bool | (elet _ _ _ _) := tt | e := ff -meta def binding_name : expr → name -| (pi n _ _ _) := n -| (lam n _ _ _) := n -| e := name.anonymous - -meta def binding_info : expr → binder_info -| (pi _ bi _ _) := bi -| (lam _ bi _ _) := bi -| e := binder_info.default - -meta def binding_domain : expr → expr -| (pi _ _ d _) := d -| (lam _ _ d _) := d -| e := e - -meta def binding_body : expr → expr -| (pi _ _ _ b) := b -| (lam _ _ _ b) := b -| e := e - -meta def is_numeral : expr → bool -| `(@has_zero.zero %%α %%s) := tt -| `(@has_one.one %%α %%s) := tt -| `(@bit0 %%α %%s %%v) := is_numeral v -| `(@bit1 %%α %%s₁ %%s₂ %%v) := is_numeral v -| _ := ff - -meta def imp (a b : expr) : expr := -pi `_ binder_info.default a b - -meta def extract_opt_auto_param : expr → expr -| `(@opt_param %%t _) := extract_opt_auto_param t -| `(@auto_param %%t _) := extract_opt_auto_param t -| e := e - open format -private meta def p := λ xs, paren (format.join (list.intersperse " " xs)) - -meta def to_raw_fmt : expr → format -| (bvar n) := p ["bvar", to_fmt n] -| (lit l) := "lit" -| (fvar n) := p ["fvar", to_fmt n] -| (sort l) := p ["sort", to_fmt l] -| (const n ls) := p ["const", to_fmt n, to_fmt ls] -| (mvar n t) := p ["mvar", to_fmt n, to_raw_fmt t] -| (app e f) := p ["app", to_raw_fmt e, to_raw_fmt f] -| (lam n bi e t) := p ["lam", to_fmt n, repr bi, to_raw_fmt e, to_raw_fmt t] -| (pi n bi e t) := p ["pi", to_fmt n, repr bi, to_raw_fmt e, to_raw_fmt t] -| (elet n g e f) := p ["elet", to_fmt n, to_raw_fmt g, to_raw_fmt e, to_raw_fmt f] -| (mdata d e) := p ["mdata", to_raw_fmt e] -| (proj idx e) := p ["proj", to_fmt idx, to_raw_fmt e] -| (quote b v) := p ["quote", to_fmt b, to_raw_fmt v] - -meta def mfold {α : Type} {m : Type → Type} [monad m] (e : expr) (a : α) (fn : expr → nat → α → m α) : m α := -lean.expr.fold e (return a) (λ e n a, a >>= fn e n) - end lean.expr diff --git a/library/init/meta/level.lean b/library/init/meta/level.lean index 5bc08db444..1c6ff62801 100644 --- a/library/init/meta/level.lean +++ b/library/init/meta/level.lean @@ -7,19 +7,3 @@ prelude import init.meta.name init.lean.level export lean (level level.zero level.succ level.max level.imax level.param level.of_nat level.has_param) - -/- TODO(Leo): provide a definition in Lean. -/ -meta constant level.has_decidable_eq : decidable_eq level -attribute [instance] level.has_decidable_eq -meta constant level.lt : level → level → bool -meta constant level.lex_lt : level → level → bool -meta constant level.fold {α :Type} : level → α → (level → α → α) → α -/-- Return the given level expression normal form -/ -meta constant level.normalize : level → level -/-- Return tt iff lhs and rhs denote the same level. - The check is done by normalization. -/ -meta constant level.eqv : level → level → bool -/-- Return tt iff the first level occurs in the second -/ -meta constant level.occurs : level → level → bool -/-- Replace a parameter named n with l in the first level if the list contains the pair (n, l) -/ -meta constant level.instantiate : level → list (name × level) → list level diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index b9eefec14a..8e8b7e06a6 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -303,15 +303,6 @@ vm_obj expr_subst(vm_obj const & _e1, vm_obj const & _e2) { } } -vm_obj expr_is_annotation(vm_obj const & _e) { - expr const & e = to_expr(_e); - if (is_annotation(e)) { - return mk_vm_some(mk_vm_pair(to_obj(get_annotation_kind(e)), to_obj(get_annotation_arg(e)))); - } else { - return mk_vm_none(); - } -} - vm_obj reflect_expr(vm_obj const & e) { return to_obj(mk_elaborated_expr_quote(to_expr(e))); } @@ -352,8 +343,6 @@ void initialize_vm_expr() { DECLARE_VM_BUILTIN(name("mk_fin_val_ne_proof"), vm_mk_fin_val_ne_proof); DECLARE_VM_BUILTIN(name("mk_char_val_ne_proof"), vm_mk_char_val_ne_proof); DECLARE_VM_BUILTIN(name("mk_string_val_ne_proof"), vm_mk_string_val_ne_proof); - - DECLARE_VM_BUILTIN(name({"lean", "expr", "is_annotation"}), expr_is_annotation); } void finalize_vm_expr() { diff --git a/src/library/vm/vm_level.cpp b/src/library/vm/vm_level.cpp index 2ea437b61f..2e1778f244 100644 --- a/src/library/vm/vm_level.cpp +++ b/src/library/vm/vm_level.cpp @@ -86,64 +86,6 @@ unsigned level_cases_on(vm_obj const & o, buffer & data) { return static_cast(l.kind()); } -vm_obj level_has_decidable_eq(vm_obj const & o1, vm_obj const & o2) { - return mk_vm_bool(to_level(o1) == to_level(o2)); -} - -vm_obj level_lt(vm_obj const & o1, vm_obj const & o2) { - return mk_vm_bool(is_lt(to_level(o1), to_level(o2), true)); -} - -vm_obj level_lex_lt(vm_obj const & o1, vm_obj const & o2) { - return mk_vm_bool(is_lt(to_level(o1), to_level(o2), false)); -} - -vm_obj level_eqv(vm_obj const & o1, vm_obj const & o2) { - return mk_vm_bool(is_equivalent(to_level(o1), to_level(o2))); -} - -vm_obj level_normalize(vm_obj const & o) { - return to_obj(normalize(to_level(o))); -} - -vm_obj level_occurs(vm_obj const & o1, vm_obj const & o2) { - return mk_vm_bool(occurs(to_level(o1), to_level(o2))); -} - -vm_obj level_to_format(vm_obj const & l, vm_obj const & o) { - return to_obj(pp(to_level(l), to_options(o))); -} - -vm_obj level_to_string(vm_obj const & l) { - std::ostringstream out; - out << to_level(l); - return to_obj(out.str()); -} - -vm_obj level_fold(vm_obj const &, vm_obj const & l, vm_obj const & a, vm_obj const & fn) { - vm_obj r = a; - for_each(to_level(l), [&](level const & o) { - r = invoke(fn, to_obj(o), r); - return true; - }); - return r; -} - -// meta_constant level.instantiate : level → list (name × level) → list level -vm_obj level_instantiate(vm_obj const & o, vm_obj const & lst) { - level const & l = to_level(o); - buffer ns; - buffer ls; - vm_obj it = lst; - while (!is_simple(it)) { - vm_obj const & h = cfield(it, 0); - ns.push_back(to_name(cfield(h, 0))); - ls.push_back(to_level(cfield(h, 1))); - it = cfield(it, 1); - } - return to_obj(instantiate(l, names(ns), levels(ls))); -} - void initialize_vm_level() { DECLARE_VM_BUILTIN(name({"lean", "level", "zero"}), level_zero); DECLARE_VM_BUILTIN(name({"lean", "level", "succ"}), level_succ); @@ -151,15 +93,7 @@ void initialize_vm_level() { DECLARE_VM_BUILTIN(name({"lean", "level", "imax"}), level_imax); DECLARE_VM_BUILTIN(name({"lean", "level", "param"}), level_param); DECLARE_VM_BUILTIN(name({"lean", "level", "mvar"}), level_mvar); - DECLARE_VM_BUILTIN(name({"level", "has_decidable_eq"}), level_has_decidable_eq); DECLARE_VM_CASES_BUILTIN(name({"lean", "level", "cases_on"}), level_cases_on); - DECLARE_VM_BUILTIN(name({"level", "lt"}), level_lt); - DECLARE_VM_BUILTIN(name({"level", "lex_lt"}), level_lex_lt); - DECLARE_VM_BUILTIN(name({"level", "eqv"}), level_eqv); - DECLARE_VM_BUILTIN(name({"level", "normalize"}), level_normalize); - DECLARE_VM_BUILTIN(name({"level", "occurs"}), level_occurs); - DECLARE_VM_BUILTIN(name({"level", "fold"}), level_fold); - DECLARE_VM_BUILTIN(name({"level", "instantiate"}), level_instantiate); } void finalize_vm_level() {