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

feat(library/init/meta/level): use lean.level

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-22 09:15:49 -07:00
parent ede1a51d60
commit c30f40e4ac
3 changed files with 12 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.level init.control.monad init.lean.expr
import init.meta.level init.control.monad init.lean.expr init.meta.format
universes u v
structure pos :=

33
library/init/meta/level.lean
View file

@ -4,19 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.name init.meta.format
import init.meta.name init.lean.level
/-- Reflect a C++ level object. The VM replaces it with the C++ implementation. -/
meta inductive level
| zero : level
| succ : level → level
| max : level → level → level
| imax : level → level → level
| param : name → level
| mvar : name → level
meta instance : inhabited level :=
⟨level.zero⟩
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
@ -33,22 +23,3 @@ meta constant level.eqv : level → level → bool
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
meta constant level.to_format : level → options → format
meta constant level.to_string : level → string
meta instance : has_to_string level :=
⟨level.to_string⟩
meta instance : has_to_format level :=
⟨λ l, level.to_format l options.mk⟩
meta def level.of_nat : nat → level
| 0 := level.zero
| (nat.succ n) := level.succ (level.of_nat n)
meta def level.has_param : level → name → bool
| (level.succ l) n := level.has_param l n
| (level.max l₁ l₂) n := level.has_param l₁ n || level.has_param l₂ n
| (level.imax l₁ l₂) n := level.has_param l₁ n || level.has_param l₂ n
| (level.param n₁) n := n₁ = n
| l n := ff

20
src/library/vm/vm_level.cpp
View file

@ -45,11 +45,11 @@ vm_obj level_succ(vm_obj const & o) {
}
vm_obj level_max(vm_obj const & o1, vm_obj const & o2) {
return to_obj(mk_max(to_level(o1), to_level(o2)));
return to_obj(mk_max_core(to_level(o1), to_level(o2)));
}
vm_obj level_imax(vm_obj const & o1, vm_obj const & o2) {
return to_obj(mk_imax(to_level(o1), to_level(o2)));
return to_obj(mk_imax_core(to_level(o1), to_level(o2)));
}
vm_obj level_param(vm_obj const & n) {
@ -145,23 +145,21 @@ vm_obj level_instantiate(vm_obj const & o, vm_obj const & lst) {
}
void initialize_vm_level() {
DECLARE_VM_BUILTIN(name({"level", "zero"}), level_zero);
DECLARE_VM_BUILTIN(name({"level", "succ"}), level_succ);
DECLARE_VM_BUILTIN(name({"level", "max"}), level_max);
DECLARE_VM_BUILTIN(name({"level", "imax"}), level_imax);
DECLARE_VM_BUILTIN(name({"level", "param"}), level_param);
DECLARE_VM_BUILTIN(name({"level", "mvar"}), level_mvar);
DECLARE_VM_BUILTIN(name({"lean", "level", "zero"}), level_zero);
DECLARE_VM_BUILTIN(name({"lean", "level", "succ"}), level_succ);
DECLARE_VM_BUILTIN(name({"lean", "level", "max"}), level_max);
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", "to_format"}), level_to_format);
DECLARE_VM_BUILTIN(name({"level", "to_string"}), level_to_string);
DECLARE_VM_BUILTIN(name({"level", "fold"}), level_fold);
DECLARE_VM_BUILTIN(name({"level", "instantiate"}), level_instantiate);
DECLARE_VM_CASES_BUILTIN(name({"level", "cases_on"}), level_cases_on);
}
void finalize_vm_level() {