chore(library/init/meta): remove level and expr unused functions
This commit is contained in:
Leonardo de Moura
parent
318530cf07
commit
91d2ad5925
4 changed files with 20 additions and 272 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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() {
|
||||
|
|
|
|||
|
|
@ -86,64 +86,6 @@ unsigned level_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
|
|||
return static_cast<unsigned>(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<name> ns;
|
||||
buffer<level> 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() {
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue