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

feat(library/vm/vm_environment): expose 'environment.add_inductive'

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-07 17:24:43 -07:00
parent b28e724709
commit 8f10e18f53
2 changed files with 34 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
src/library/vm/vm_environment.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h"
#include "library/standard_kernel.h"
#include "library/hott_kernel.h"
#include "library/module.h"
#include "library/util.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_name.h"
@ -52,7 +53,7 @@ vm_obj environment_is_std(vm_obj const & env) {
vm_obj environment_add(vm_obj const & env, vm_obj const & decl) {
try {
return mk_vm_exceptional_success(to_obj(to_env(env).add(check(to_env(env), to_declaration(decl)))));
return mk_vm_exceptional_success(to_obj(module::add(to_env(env), check(to_env(env), to_declaration(decl)))));
} catch (throwable & ex) {
return mk_vm_exceptional_exception(ex);
}
@ -66,11 +67,32 @@ vm_obj environment_get(vm_obj const & env, vm_obj const & n) {
}
}
static list<inductive::intro_rule> to_list_intro_rule(vm_obj const & cnstrs) {
if (is_simple(cnstrs))
return list<inductive::intro_rule>();
else
return list<inductive::intro_rule>(mk_local(to_name(cfield(cfield(cnstrs, 0), 0)),
to_expr(cfield(cfield(cnstrs, 0), 1))),
to_list_intro_rule(cfield(cnstrs, 1)));
}
vm_obj environment_add_inductive(vm_obj const & env, vm_obj const & n, vm_obj const & ls, vm_obj const & num,
vm_obj const & type, vm_obj const & cnstrs) {
try {
environment new_env = module::add_inductive(to_env(env),
to_list_name(ls),
force_to_unsigned(num, 0),
list<inductive::inductive_decl>(
inductive::inductive_decl(to_name(n),
to_expr(type),
to_list_intro_rule(cnstrs))));
return mk_vm_exceptional_success(to_obj(new_env));
} catch (throwable & ex) {
return mk_vm_exceptional_exception(ex);
}
}
/*
/- Add a new inductive datatype to the environment
name, universe parameters, number of parameters, type, constructors (name and type) -/
meta_constant add_inductive : environment → name → list name → nat → expr → list (name × expr) → exceptional environment
/- Return tt iff the given name is an inductive datatype -/
meta_constant is_inductive : environment → name → bool
/- Return tt iff the given name is a constructor -/
meta_constant is_constructor : environment → name → bool
@ -97,6 +119,7 @@ void initialize_vm_environment() {
DECLARE_VM_BUILTIN(name({"environment", "is_std"}), environment_is_std);
DECLARE_VM_BUILTIN(name({"environment", "add"}), environment_add);
DECLARE_VM_BUILTIN(name({"environment", "get"}), environment_get);
DECLARE_VM_BUILTIN(name({"environment", "add_inductive"}), environment_add_inductive);
}
void finalize_vm_environment() {

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

@ -22,7 +22,11 @@ vm_eval do
(expr.sort (level.succ (level.zero)))
(expr.sort level.zero)
bool.tt),
d ← environment.get e₁ "foo",
e₂ ← environment.add_inductive e₁ "Two" [] 0 (expr.sort (level.succ level.zero))
[("Zero", expr.const "Two" []),
("One", expr.const "Two" [])],
d₁ ← environment.get e₂ "Zero",
d₂ ← environment.get e₂ "foo",
/- TODO(leo): use
return (declaration.type d)
@ -35,4 +39,4 @@ vm_eval do
The new elaborator should be able to handle it.
-/
exceptional.success (declaration.type d)
exceptional.success (declaration.type d₁, declaration.type d₂)