From 8f10e18f53bca73d812bef87f64c6a7e16fbfdb7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 Jun 2016 17:24:43 -0700
Subject: [PATCH] feat(library/vm/vm_environment): expose
 'environment.add_inductive'

---
 src/library/vm/vm_environment.cpp | 33 ++++++++++++++++++++++++++-----
 tests/lean/run/meta_env1.lean     |  8 ++++++--
 2 files changed, 34 insertions(+), 7 deletions(-)

diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp
index 7d38ac8487..4b3b6c1111 100644
--- a/src/library/vm/vm_environment.cpp
+++ b/src/library/vm/vm_environment.cpp
@@ -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() {
diff --git a/tests/lean/run/meta_env1.lean b/tests/lean/run/meta_env1.lean
index b5cc7f76c1..1b8cb8a28e 100644
--- a/tests/lean/run/meta_env1.lean
+++ b/tests/lean/run/meta_env1.lean
@@ -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₂)