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

feat(library/vm): expose reducibility_hints

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-04 18:09:10 -07:00
parent e8397681a5
commit d6d68cd70a
4 changed files with 44 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
library/init/meta/declaration.lean
View file

@ -6,10 +6,15 @@ Authors: Leonardo de Moura
prelude
import init.meta.expr init.meta.name
inductive reducibility_hints
| opaque : reducibility_hints
| abbrev : reducibility_hints
| regular : nat → bool → reducibility_hints
/- Reflect a C++ declaration object. The VM replaces it with the C++ implementation. -/
inductive declaration
/- definition: name, list universe parameters, type, value, is_trusted -/
| defn : name → list name → expr → expr → bool → declaration
| defn : name → list name → expr → expr → reducibility_hints → bool → declaration
/- theorem: name, list universe parameters, type, value (remark: theorems are always trusted) -/
| thm : name → list name → expr → expr → declaration
/- constant assumption: name, list universe parameters, type, is_trusted -/
@ -18,19 +23,19 @@ inductive declaration
| ax : name → list name → expr → declaration
definition declaration.to_name : declaration → name
| (declaration.defn n ls t v tr) := n
| (declaration.defn n ls t v h tr) := n
| (declaration.thm n ls t v) := n
| (declaration.cnst n ls t tr) := n
| (declaration.ax n ls t) := n
definition declaration.univ_params : declaration → list name
| (declaration.defn n ls t v tr) := ls
| (declaration.defn n ls t v h tr) := ls
| (declaration.thm n ls t v) := ls
| (declaration.cnst n ls t tr) := ls
| (declaration.ax n ls t) := ls
definition declaration.type : declaration → expr
| (declaration.defn n ls t v tr) := t
| (declaration.defn n ls t v h tr) := t
| (declaration.thm n ls t v) := t
| (declaration.cnst n ls t tr) := t
| (declaration.ax n ls t) := t

30
src/library/vm/vm_declaration.cpp
View file

@ -9,9 +9,34 @@ Author: Leonardo de Moura
#include "library/vm/vm_level.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_option.h"
namespace lean {
/*
inductive reducibility_hint
| opaque : reducibility_hint
| abbrev : reducibility_hint
| regular : nat → bool → reducibility_hint
*/
vm_obj to_obj(reducibility_hints const & h) {
switch (h.get_kind()) {
case reducibility_hints::Opaque: return mk_vm_simple(0);
case reducibility_hints::Abbreviation: return mk_vm_simple(1);
case reducibility_hints::Regular: return mk_vm_constructor(2, mk_vm_nat(h.get_height()), mk_vm_bool(h.use_self_opt()));
}
lean_unreachable();
}
reducibility_hints to_reducibility_hints(vm_obj const & o) {
switch (cidx(o)) {
case 0: return reducibility_hints::mk_opaque();
case 1: return reducibility_hints::mk_abbreviation();
case 2: return reducibility_hints::mk_regular(force_to_unsigned(cfield(o, 0), 0), to_bool(cfield(o, 1)));
}
lean_unreachable();
}
struct vm_declaration : public vm_external {
declaration m_val;
vm_declaration(declaration const & v):m_val(v) {}
@ -29,8 +54,8 @@ vm_obj to_obj(declaration const & n) {
}
vm_obj declaration_defn(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & value,
vm_obj const & trusted) {
return to_obj(mk_definition(to_name(n), to_list_name(ls), to_expr(type), to_expr(value), reducibility_hints::mk_regular(0, true), to_bool(trusted)));
vm_obj const & hints, vm_obj const & trusted) {
return to_obj(mk_definition(to_name(n), to_list_name(ls), to_expr(type), to_expr(value), to_reducibility_hints(hints), to_bool(trusted)));
}
vm_obj declaration_thm(vm_obj const & n, vm_obj const & ls, vm_obj const & type, vm_obj const & value) {
@ -52,6 +77,7 @@ unsigned declaration_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
data.push_back(to_obj(d.get_type()));
if (d.is_definition()) {
data.push_back(to_obj(d.get_value()));
data.push_back(to_obj(d.get_hints()));
data.push_back(mk_vm_bool(d.is_trusted()));
return 0;
} else if (d.is_theorem()) {

8
tests/lean/run/meta_env1.lean
View file

@ -2,18 +2,20 @@ open list
meta_definition e := environment.mk_std 0
definition hints := reducibility_hints.regular 10 tt
vm_eval environment.trust_lvl e
vm_eval environment.is_std e
vm_eval (environment.add e (declaration.defn `foo []
(expr.sort (level.succ (level.zero)))
(expr.sort (level.succ (level.zero)))
bool.tt) : exceptional environment)
hints tt) : exceptional environment)
meta_definition e1 := (environment.add e (declaration.defn `foo []
(expr.sort (level.succ (level.zero)))
(expr.sort level.zero)
bool.tt) : exceptional environment)
hints tt) : exceptional environment)
print "-----------"
open name
@ -22,7 +24,7 @@ vm_eval do
e₁ ← environment.add e (declaration.defn `foo []
(expr.sort (level.succ (level.zero)))
(expr.sort level.zero)
bool.tt),
hints tt),
e₂ ← environment.add_inductive e₁ `Two [] 0 (expr.sort (level.succ level.zero))
[(`Zero, expr.const `Two []),
(`One, expr.const `Two [])],

4
tests/lean/run/run_tactic1.lean
View file

@ -5,7 +5,7 @@ run_command tactic.trace "hello world"
run_command do
N ← to_expr `(nat),
v ← to_expr `(10),
add_decl (declaration.defn `val10 [] N v tt)
add_decl (declaration.defn `val10 [] N v reducibility_hints.opaque tt)
vm_eval val10
@ -16,7 +16,7 @@ meta_definition mk_defs : nat → command
| (n+1) := do
N ← to_expr `(nat),
v ← expr_of_nat n,
add_decl (declaration.defn (name.append_after `val n) [] N v tt),
add_decl (declaration.defn (name.append_after `val n) [] N v reducibility_hints.opaque tt),
mk_defs n
run_command mk_defs 10