From e88933bac9994db96a09209b41cf0889cae8ff94 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= <johannes.hoelzl@gmx.de>
Date: Fri, 2 Jun 2017 15:56:48 -0400
Subject: [PATCH] feat(library/init/meta/tactic): add tactic.set_env to set
 environment

---
 library/init/meta/tactic.lean       | 13 +++++++++++++
 src/library/tactic/tactic_state.cpp | 12 +++++++++++-
 2 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index d689fb709a..ab803122d4 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -409,6 +409,8 @@ meta constant generalize (e : expr) (n : name := `_x) (md := semireducible) : ta
 meta constant instantiate_mvars : expr → tactic expr
 /-- Add the given declaration to the environment -/
 meta constant add_decl : declaration → tactic unit
+/-- Changes the environment to the `new_env`. `new_env` needs to be a descendant from the current environment. -/
+meta constant set_env : environment → tactic unit
 /-- (doc_string env d k) return the doc string for d (if available) -/
 meta constant doc_string : name → tactic string
 meta constant add_doc_string : name → string → tactic unit
@@ -1008,6 +1010,17 @@ match _root_.try_for max (tac s) with
 | none   := mk_exception "try_for tactic failed, timeout" none s
 end
 
+meta def updateex_env (f : environment → exceptional environment) : tactic unit :=
+do env ← get_env,
+   env ← returnex $ f env,
+   set_env env
+
+/- Add a new inductive datatype to the environment
+   name, universe parameters, number of parameters, type, constructors (name and type), is_meta -/
+meta def add_inductive (n : name) (ls : list name) (p : nat) (ty : expr) (is : list (name × expr))
+  (is_meta : bool := ff) : tactic unit :=
+updateex_env $ λe, e.add_inductive n ls p ty is is_meta
+
 meta def add_meta_definition (n : name) (lvls : list name) (type value : expr) : tactic unit :=
 add_decl (declaration.defn n lvls type value reducibility_hints.abbrev ff)
 
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index b9f6b694e5..4f8dae2919 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -631,12 +631,21 @@ vm_obj tactic_add_decl(vm_obj const & _d, vm_obj const & _s) {
         declaration d       = to_declaration(_d);
         environment new_env = module::add(s.env(), check(s.env(), d));
         new_env = vm_compile(new_env, d);
-        return tactic::mk_success(set_env(s, new_env));
+         return tactic::mk_success(set_env(s, new_env));
     } catch (throwable & ex) {
         return tactic::mk_exception(ex, s);
     }
 }
 
+vm_obj tactic_set_env(vm_obj const & _env, vm_obj const & _s) {
+    tactic_state const & s      = tactic::to_state(_s);
+    environment const & new_env = to_env(_env);
+    if (new_env.is_descendant(s.env()))
+        return tactic::mk_success(set_env(s, new_env));
+    else
+        return tactic::mk_exception(sstream() << "new environment is not a descendent from old environment.", s);
+}
+
 vm_obj tactic_open_namespaces(vm_obj const & s) {
     environment env = tactic::to_state(s).env();
     buffer<name> b;
@@ -880,6 +889,7 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "is_trace_enabled_for"}), tactic_is_trace_enabled_for);
     DECLARE_VM_BUILTIN(name({"tactic", "instantiate_mvars"}),    tactic_instantiate_mvars);
     DECLARE_VM_BUILTIN(name({"tactic", "add_decl"}),             tactic_add_decl);
+    DECLARE_VM_BUILTIN(name({"tactic", "set_env"}),              tactic_set_env);
     DECLARE_VM_BUILTIN(name({"tactic", "doc_string"}),           tactic_doc_string);
     DECLARE_VM_BUILTIN(name({"tactic", "add_doc_string"}),       tactic_add_doc_string);
     DECLARE_VM_BUILTIN(name({"tactic", "module_doc_strings"}),   tactic_module_doc_strings);