feat(frontends/lean): Scopes in the default Lean frontend

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

examples/lean/ex5.lean

@@ -0,0 +1,57 @@
+Push
+   Theorem ReflIf (A : Type)
+                  (R : A -> A -> Bool)
+                  (Symmetry : Pi x y, R x y -> R y x)
+                  (Transitivity : Pi x y z, R x y -> R y z -> R x z)
+                  (Linked : Pi x, exists y, R x y)
+                  :
+                  Pi x, R x x :=
+       fun x, ExistsElim (Linked x)
+             (fun (w : A) (H : R x w),
+                 let L1 : R w x := Symmetry x w H
+                 in Transitivity x w x H L1)
+Pop
+
+Push
+  (*
+    Same example but using forall instead of Pi and => instead of ->
+  *)
+  Theorem ReflIf (A : Type)
+                 (R : A -> A -> Bool)
+                 (Symmetry : forall x y, R x y => R y x)
+                 (Transitivity : forall x y z, R x y => R y z => R x z)
+                 (Linked : forall x, exists y, R x y)
+                 :
+                 forall x, R x x :=
+    ForallIntro (fun x,
+         ExistsElim (ForallElim Linked x)
+            (fun (w : A) (H : R x w),
+                let L1 : R w x := (MP (ForallElim (ForallElim Symmetry x) w) H)
+                in (MP (MP (ForallElim (ForallElim (ForallElim Transitivity x) w) x) H) L1)))
+Pop
+
+Scope
+  (* Same example again. *)
+  Variable A : Type
+  Variable R : A -> A -> Bool
+  Axiom Symmetry  {x y : A} : R x y -> R y x
+  Axiom Transitivity {x y z : A} : R x y -> R y z -> R x z
+  Axiom Linked (x : A) : exists y, R x y
+
+  Theorem ReflIf (x : A) : R x x :=
+      ExistsElim (Linked x) (fun (w : A) (H : R x w),
+            let L1 : R w x := Symmetry H
+            in Transitivity H L1)
+
+  (* Even more compact proof of the same theorem *)
+  Theorem ReflIf2 (x : A) : R x x :=
+      ExistsElim (Linked x) (fun w H, Transitivity H (Symmetry H))
+
+(*
+  The command EndScope exports both theorem to the main scope
+  The variables and axioms in the scope become parameters to both theorems.
+*)
+EndScope
+
+(* Display the last two theorems *)
+Show Environment 2

src/frontends/lean/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_library(lean_frontend frontend.cpp operator_info.cpp scanner.cpp parser.cpp pp.cpp
-  notation.cpp frontend_elaborator.cpp register_module.cpp)
+  notation.cpp frontend_elaborator.cpp register_module.cpp environment_scope.cpp)
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/environment_scope.cpp

@@ -0,0 +1,121 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <vector>
+#include <algorithm>
+#include "util/list.h"
+#include "util/name_set.h"
+#include "util/name_map.h"
+#include "kernel/environment.h"
+#include "kernel/replace_fn.h"
+#include "kernel/abstract.h"
+#include "frontends/lean/frontend.h"
+
+namespace lean {
+typedef std::vector<name> dependencies;
+
+struct object_info {
+    object       m_object;
+    unsigned     m_pos;
+    dependencies m_deps;
+    expr         m_ref; // a reference to this object, it can be a constant or an application containing the dependencies
+    object_info(object const & obj, unsigned pos, dependencies const & deps, expr const & ref):m_object(obj), m_pos(pos), m_deps(deps), m_ref(ref) {}
+};
+
+static expr convert(expr const & e, name_map<object_info> & info_map, name_set & dep_set) {
+    return replace(e, [&](expr const & e, unsigned) -> expr {
+            if (is_constant(e)) {
+                auto it = info_map.find(const_name(e));
+                if (it != info_map.end()) {
+                    auto const & info = it->second;
+                    if (info.m_object.is_axiom() || info.m_object.is_var_decl())
+                        dep_set.insert(const_name(e));
+                    for (auto const & d : info.m_deps)
+                        dep_set.insert(d);
+                    return info.m_ref;
+                }
+            }
+            return e;
+        });
+}
+
+static dependencies mk_dependencies(name_map<object_info> & info_map, name_set & dep_set) {
+    dependencies r;
+    for (auto d : dep_set) r.push_back(d);
+    std::sort(r.begin(), r.end(), [&](name const & n1, name const & n2) {
+            return info_map.find(n1)->second.m_pos < info_map.find(n2)->second.m_pos;
+        });
+    return r;
+}
+
+static expr mk_ref(object const & obj, dependencies const & deps) {
+    if (obj.is_axiom() || obj.is_var_decl()) {
+        return mk_constant(obj.get_name());
+    } else {
+        buffer<expr> args;
+        args.push_back(mk_constant(obj.get_name()));
+        for (auto d : deps) args.push_back(mk_constant(d));
+        return mk_app(args);
+    }
+}
+
+static expr abstract(bool is_lambda, expr e, name_map<object_info> & info_map, dependencies const & deps) {
+    auto it = deps.end();
+    auto begin = deps.begin();
+    while (it != begin) {
+        --it;
+        expr const & type = info_map.find(*it)->second.m_object.get_type();
+        if (is_lambda)
+            e = Fun(*it, type, e);
+        else
+            e = Pi(*it, type, e);
+    }
+    return e;
+}
+
+static expr Pi(expr e, name_map<object_info> & info_map, dependencies const & deps) {
+    return abstract(false, e, info_map, deps);
+}
+
+static expr Fun(expr e, name_map<object_info> & info_map, dependencies const & deps) {
+    return abstract(true, e, info_map, deps);
+}
+
+std::vector<object> export_local_objects(environment const & env) {
+    if (!env->has_parent())
+        return std::vector<object>();
+    name_map<object_info> info_map;
+    name_set dep_set;
+    unsigned pos = 0;
+    std::vector<object> new_objects;
+    auto it  = env->begin_local_objects();
+    auto end = env->end_local_objects();
+    for (; it != end; ++it) {
+        object const & obj = *it;
+        if (!obj.is_axiom() && !obj.is_var_decl() && !obj.is_theorem() && !obj.is_definition())
+            continue;
+        if (is_explicit(env, obj.get_name()))
+            continue;
+        dep_set.clear();
+        if (obj.is_axiom() || obj.is_var_decl()) {
+            expr new_type = convert(obj.get_type(), info_map, dep_set);
+            auto new_deps = mk_dependencies(info_map, dep_set);
+            info_map.insert(mk_pair(obj.get_name(), object_info(obj, pos, new_deps, mk_ref(obj, new_deps))));
+        } else {
+            expr new_type = convert(obj.get_type(), info_map, dep_set);
+            expr new_val  = convert(obj.get_value(), info_map, dep_set);
+            auto new_deps = mk_dependencies(info_map, dep_set);
+            new_type = Pi(new_type, info_map, new_deps);
+            new_val  = Fun(new_val, info_map, new_deps);
+            auto new_obj  = obj.is_theorem() ? mk_theorem(obj.get_name(), new_type, new_val) : mk_definition(obj.get_name(), new_type, new_val, obj.is_opaque(), obj.get_weight());
+            new_objects.push_back(new_obj);
+            info_map.insert(mk_pair(obj.get_name(), object_info(new_obj, pos, new_deps, mk_ref(new_obj, new_deps))));
+        }
+        pos++;
+    }
+    return new_objects;
+}
+}

src/frontends/lean/environment_scope.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <vector>
+#include "kernel/environment.h"
+namespace lean {
+std::vector<object> export_local_objects(environment const & env);
+}

src/frontends/lean/frontend_elaborator.cpp

@@ -125,7 +125,7 @@ inline justification mk_overload_justification(context const & ctx, expr const &
     \brief Actual implementation of the frontend_elaborator.
 */
 class frontend_elaborator::imp {
-    environment const &                 m_env;
+    environment                         m_env;
     type_checker                        m_type_checker;
     type_inferer                        m_type_inferer;
     normalizer                          m_normalizer;
@@ -511,5 +511,6 @@ std::tuple<expr, expr, metavar_env> frontend_elaborator::operator()(name const &
 }
 expr const & frontend_elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); }
 void frontend_elaborator::clear() { m_ptr->clear(); }
+void frontend_elaborator::reset(environment const & env) { m_ptr.reset(new imp(env)); }
 environment const & frontend_elaborator::get_environment() const { return m_ptr->get_environment(); }
 }

src/frontends/lean/frontend_elaborator.h

@@ -44,9 +44,10 @@ public:
     */
     expr const & get_original(expr const & e) const;
 
-    void clear();
-
     environment const & get_environment() const;
+
+    void clear();
+    void reset(environment const & env);
 };
 
 /**

src/frontends/lean/parser.cpp

@@ -51,6 +51,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/notation.h"
 #include "frontends/lean/pp.h"
+#include "frontends/lean/environment_scope.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
@@ -96,6 +97,10 @@ static name g_import_kwd("Import");
 static name g_help_kwd("Help");
 static name g_coercion_kwd("Coercion");
 static name g_exit_kwd("Exit");
+static name g_push_kwd("Push");
+static name g_pop_kwd("Pop");
+static name g_scope_kwd("Scope");
+static name g_end_scope_kwd("EndScope");
 static name g_apply("apply");
 static name g_done("done");
 static name g_back("back");
@@ -105,7 +110,8 @@ static list<name> g_tactic_cmds = { g_apply, g_done, g_back, g_abort, g_assumpti
 /** \brief Table/List with all builtin command keywords */
 static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
                                         g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd,
-                                        g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd, g_exit_kwd};
+                                        g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd, g_exit_kwd, g_push_kwd, g_pop_kwd,
+                                        g_scope_kwd, g_end_scope_kwd};
 // ==========================================
 
 // ==========================================
@@ -2043,12 +2049,16 @@ class parser::imp {
                                 << "  Definition [id] : [type] := [expr]   define a new element" << endl
                                 << "  Theorem [id] : [type] := [expr]      define a new theorem" << endl
                                 << "  Echo [string]          display the given string" << endl
+                                << "  EndScope               end the current scope and import its objects into the parent scope" << endl
                                 << "  Eval [expr]            evaluate the given expression" << endl
                                 << "  Exit                   exit" << endl
                                 << "  Help                   display this message" << endl
                                 << "  Help Options           display available options" << endl
                                 << "  Help Notation          describe commands for defining infix, mixfix, postfix operators" << endl
                                 << "  Import [string]        load the given file" << endl
+                                << "  Push                   create a scope (it is just an alias for the command Scope)" << endl
+                                << "  Pop                    discard the current scope" << endl
+                                << "  Scope                  create a scope" << endl
                                 << "  Set [id] [value]       set option [id] with value [value]" << endl
                                 << "  Show [expr]            pretty print the given expression" << endl
                                 << "  Show Options           show current the set of assigned options" << endl
@@ -2071,6 +2081,38 @@ class parser::imp {
             regular(m_io_state) << "  Coercion " << coercion << endl;
     }
 
+    void reset_env(environment env) {
+        m_env = env;
+        m_elaborator.reset(env);
+        m_type_inferer.reset(env);
+    }
+
+    void parse_scope() {
+        next();
+        reset_env(m_env->mk_child());
+    }
+
+    void parse_pop() {
+        next();
+        if (!m_env->has_parent())
+            throw parser_error("main scope cannot be removed", m_last_cmd_pos);
+        reset_env(m_env->parent());
+    }
+
+    void parse_end_scope() {
+        next();
+        if (!m_env->has_parent())
+            throw parser_error("main scope cannot be removed", m_last_cmd_pos);
+        auto new_objects = export_local_objects(m_env);
+        reset_env(m_env->parent());
+        for (auto const & obj : new_objects) {
+            if (obj.is_theorem())
+                m_env->add_theorem(obj.get_name(), obj.get_type(), obj.get_value());
+            else
+                m_env->add_definition(obj.get_name(), obj.get_type(), obj.get_value(), obj.is_opaque());
+        }
+    }
+
     /** \brief Parse a Lean command. */
     bool parse_command() {
         m_elaborator.clear();
@@ -2115,6 +2157,12 @@ class parser::imp {
         } else if (cmd_id == g_exit_kwd) {
             next();
             return false;
+        } else if (cmd_id == g_push_kwd || cmd_id == g_scope_kwd) {
+            parse_scope();
+        } else if (cmd_id == g_pop_kwd) {
+            parse_pop();
+        } else if (cmd_id == g_end_scope_kwd) {
+            parse_end_scope();
         } else {
             next();
             throw parser_error(sstream() << "invalid command '" << cmd_id << "'", m_last_cmd_pos);

src/library/type_inferer.cpp

@@ -254,6 +254,7 @@ public:
 };
 type_inferer::type_inferer(ro_environment const & env):m_ptr(new imp(env)) {}
 type_inferer::~type_inferer() {}
+void type_inferer::reset(ro_environment const & env) { m_ptr.reset(new imp(env)); }
 expr type_inferer::operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * uc) {
     return m_ptr->operator()(e, ctx, menv, uc);
 }

src/library/type_inferer.h

@@ -39,6 +39,7 @@ public:
     bool is_proposition(expr const & e, context const & ctx, metavar_env const & menv);
     bool is_proposition(expr const & e, context const & ctx = context());
     void clear();
+    void reset(ro_environment const & env);
 };
 
 void open_type_inferer(lua_State * L);

tests/lean/push.lean

@@ -0,0 +1,21 @@
+
+Variable first : Bool
+
+Push
+  Variables a b c : Int
+  Variable f : Int -> Int
+  Eval f a
+Pop
+
+Eval f a (* should produce an error *)
+
+Show Environment 1
+
+Push
+  Infixl 100 ++ : Int::add
+  Check 10 ++ 20
+Pop
+
+Check 10 ++ 20 (* should produce an error *)
+
+Pop (* should produce an error *)

tests/lean/push.lean.expected.out

@@ -0,0 +1,13 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: first
+  Assumed: a
+  Assumed: b
+  Assumed: c
+  Assumed: f
+f a
+Error (line: 10, pos: 5) unknown identifier 'f'
+Variable first : Bool
+10 + 20 : ℤ
+Error (line: 19, pos: 9) unknown identifier '++'
+Error (line: 21, pos: 0) main scope cannot be removed

tests/lean/scope.lean

@@ -0,0 +1,26 @@
+
+Scope
+  Variable A : Type
+  Variable B : Type
+  Variable f : A -> A -> A
+  Definition g (x y : A) : A := f y x
+  Variable h : A -> B
+  Variable hinv : B -> A
+  Axiom Inv (x : A) : hinv (h x) = x
+  Axiom H1 (x y : A) : f x y = f y x
+  Theorem f_eq_g : f = g := Abst (fun x, (Abst (fun y,
+                                      let L1 : f x y = f y x := H1 x y,
+                                          L2 : f y x = g x y := Refl (g x y)
+                                      in Trans L1 L2)))
+
+  Theorem Inj (x y : A) (H : h x = h y) : x = y :=
+         let L1 : hinv (h x) = hinv (h y) := Congr2 hinv H,
+             L2 : hinv (h x) = x          := Inv x,
+             L3 : hinv (h y) = y          := Inv y,
+             L4 : x = hinv (h x)          := Symm L2,
+             L5 : x = hinv (h y)          := Trans L4 L1
+         in Trans L5 L3.
+EndScope
+
+Show Environment 3.
+Eval g Int Int::sub 10 20

tests/lean/scope.lean.expected.out

@@ -0,0 +1,32 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: A
+  Assumed: B
+  Assumed: f
+  Defined: g
+  Assumed: h
+  Assumed: hinv
+  Assumed: Inv
+  Assumed: H1
+  Proved: f_eq_g
+  Proved: Inj
+Definition g (A : Type) (f : A → A → A) (x y : A) : A := f y x
+Theorem f_eq_g (A : Type) (f : A → A → A) (H1 : Π x y : A, (f x y) = (f y x)) : f = (g A f) :=
+    Abst (λ x : A,
+            Abst (λ y : A,
+                    let L1 : (f x y) = (f y x) := H1 x y,
+                        L2 : (f y x) = (g A f x y) := Refl (g A f x y)
+                    in Trans L1 L2))
+Theorem Inj (A B : Type)
+    (h : A → B)
+    (hinv : B → A)
+    (Inv : Π x : A, (hinv (h x)) = x)
+    (x y : A)
+    (H : (h x) = (h y)) : x = y :=
+    let L1 : (hinv (h x)) = (hinv (h y)) := Congr2 hinv H,
+        L2 : (hinv (h x)) = x := Inv x,
+        L3 : (hinv (h y)) = y := Inv y,
+        L4 : x = (hinv (h x)) := Symm L2,
+        L5 : x = (hinv (h y)) := Trans L4 L1
+    in Trans L5 L3
+10