From d6d68cd70a25e957dd67c03baa4dfbd560b03ef9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 4 Sep 2016 18:09:10 -0700 Subject: [PATCH] feat(library/vm): expose reducibility_hints --- library/init/meta/declaration.lean | 13 +++++++++---- src/library/vm/vm_declaration.cpp | 30 ++++++++++++++++++++++++++++-- tests/lean/run/meta_env1.lean | 8 +++++--- tests/lean/run/run_tactic1.lean | 4 ++-- 4 files changed, 44 insertions(+), 11 deletions(-) diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean index 0c45bdaefd..573ad1dc58 100644 --- a/library/init/meta/declaration.lean +++ b/library/init/meta/declaration.lean @@ -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 diff --git a/src/library/vm/vm_declaration.cpp b/src/library/vm/vm_declaration.cpp index 45a144242a..14e75b0f93 100644 --- a/src/library/vm/vm_declaration.cpp +++ b/src/library/vm/vm_declaration.cpp @@ -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 & 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()) { diff --git a/tests/lean/run/meta_env1.lean b/tests/lean/run/meta_env1.lean index cf59517eee..4c0699f08a 100644 --- a/tests/lean/run/meta_env1.lean +++ b/tests/lean/run/meta_env1.lean @@ -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 [])], diff --git a/tests/lean/run/run_tactic1.lean b/tests/lean/run/run_tactic1.lean index 911eb68e98..08d1820e7c 100644 --- a/tests/lean/run/run_tactic1.lean +++ b/tests/lean/run/run_tactic1.lean @@ -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