From 1fd81dd3a1cfbad9d2e9319c691e1bfda7bf2844 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 28 Dec 2013 12:24:13 -0800
Subject: [PATCH] feat(frontends/lean/parser): disable verbose messages when
 importing files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/parser.cpp              | 28 +++++++++++++++-------
 src/util/script_state.cpp                  | 19 ++++++++-------
 src/util/script_state.h                    |  8 +++----
 tests/lean/cast1.lean.expected.out         |  6 +----
 tests/lean/cast2.lean.expected.out         |  6 +----
 tests/lean/cast3.lean.expected.out         |  6 +----
 tests/lean/cast4.lean.expected.out         |  6 +----
 tests/lean/discharge.lean.expected.out     |  1 +
 tests/lean/disj1.lean.expected.out         |  1 +
 tests/lean/mod1.lean.expected.out          |  8 +++----
 tests/lean/norm_bug1.lean.expected.out     |  6 +----
 tests/lean/norm_tac.lean.expected.out      |  1 +
 tests/lean/type_inf_bug1.lean.expected.out |  6 +----
 13 files changed, 47 insertions(+), 55 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 29802868b2..c9a459697c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2373,23 +2373,26 @@ class parser::imp {
             regular(m_io_state) << "  Set: " << id << endl;
     }
 
-    void import_lean_file(std::string const & fname) {
+    bool import_lean_file(std::string const & fname) {
         std::ifstream in(fname);
         if (!in.is_open())
             throw parser_error(sstream() << "invalid import command, failed to open file '" << fname << "'", m_last_cmd_pos);
         if (!m_env->mark_imported(fname.c_str())) {
             // module already imported
-            return;
+            return false;
         }
         try {
             script_state state; // Empty state object for the imported module
-            parser import_parser(m_env, m_io_state, in, &state, true /* use exceptions */, false /* not interactive */);
+            io_state ios = m_io_state;
+            ios.set_option(g_parser_verbose, false);
+            parser import_parser(m_env, ios, in, &state, true /* use exceptions */, false /* not interactive */);
             import_parser();
         } catch (interrupted &) {
             throw;
         } catch (exception &) {
             throw parser_error(sstream() << "failed to import file '" << fname << "'", m_last_cmd_pos);
         }
+        return true;
     }
 
     void parse_import() {
@@ -2401,16 +2404,23 @@ class parser::imp {
         } else {
             fname  = check_string_next("invalid import command, string (i.e., file name) or identifier expected");
         }
-        fname = find_file(fname);
-        if (is_lean_file(fname)) {
-            import_lean_file(fname);
-        } else if (is_lua_file(fname)) {
+        std::string ffname = find_file(fname);
+        bool r = false;
+        if (is_lean_file(ffname)) {
+            r = import_lean_file(ffname);
+        } else if (is_lua_file(ffname)) {
             if (!m_script_state)
                 throw parser_error(sstream() << "failed to import Lua file '" << fname << "', parser does not have an intepreter", m_last_cmd_pos);
-            m_script_state->import_explicit(fname.c_str());
+            r = m_script_state->import_explicit(ffname.c_str());
         } else {
             // assume is a Lean file
-            import_lean_file(fname);
+            r = import_lean_file(ffname);
+        }
+        if (m_verbose) {
+            if (r)
+                regular(m_io_state) << "  Imported '" << fname << "'" << endl;
+            else
+                regular(m_io_state) << "  Skipped '" << fname << "'" << endl;
         }
     }
 
diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp
index 3d9c86fc88..ca01b978bf 100644
--- a/src/util/script_state.cpp
+++ b/src/util/script_state.cpp
@@ -119,18 +119,21 @@ struct script_state::imp {
         ::lean::dostring(m_state, str);
     }
 
-    void import_explicit(std::string const & fname) {
+    bool import_explicit(std::string const & fname) {
         if (m_imported_modules.find(fname) == m_imported_modules.end()) {
             dofile(fname.c_str());
             m_imported_modules.insert(fname);
+            return true;
+        } else {
+            return false;
         }
     }
 
-    void import_explicit(char const * fname) {
-        import_explicit(std::string(fname));
+    bool import_explicit(char const * fname) {
+        return import_explicit(std::string(fname));
     }
 
-    void import(char const * fname) {
+    bool import(char const * fname) {
         return import_explicit(find_file(fname));
     }
 };
@@ -161,12 +164,12 @@ void script_state::dostring(char const * str) {
     m_ptr->dostring(str);
 }
 
-void script_state::import(char const * str) {
-    m_ptr->import(str);
+bool script_state::import(char const * str) {
+    return m_ptr->import(str);
 }
 
-void script_state::import_explicit(char const * str) {
-    m_ptr->import_explicit(str);
+bool script_state::import_explicit(char const * str) {
+    return m_ptr->import_explicit(str);
 }
 
 mutex & script_state::get_mutex() {
diff --git a/src/util/script_state.h b/src/util/script_state.h
index 9e31fbb4eb..cfa03fbe7f 100644
--- a/src/util/script_state.h
+++ b/src/util/script_state.h
@@ -46,14 +46,14 @@ public:
     void dostring(char const * str);
     /**
        \brief Import file \c fname from the LEAN_PATH.
-       If the file was already included, then nothing happens.
+       If the file was already included, then nothing happens, and method returns false.
     */
-    void import(char const * fname);
+    bool import(char const * fname);
     /**
        \brief Import file \c fname. \c fname is the explicit path to the file.
-       If the file was already included, then nothing happens.
+       If the file was already included, then nothing happens, and method returns false.
     */
-    void import_explicit(char const * fname);
+    bool import_explicit(char const * fname);
 
     /**
        \brief Execute \c f in the using the internal Lua State.
diff --git a/tests/lean/cast1.lean.expected.out b/tests/lean/cast1.lean.expected.out
index 0702123ea9..6135bcb45f 100644
--- a/tests/lean/cast1.lean.expected.out
+++ b/tests/lean/cast1.lean.expected.out
@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast.lean'
   Assumed: vector
   Assumed: N0
   Proved: V0
diff --git a/tests/lean/cast2.lean.expected.out b/tests/lean/cast2.lean.expected.out
index 73bc1a18f1..52761ae163 100644
--- a/tests/lean/cast2.lean.expected.out
+++ b/tests/lean/cast2.lean.expected.out
@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast.lean'
   Assumed: A
   Assumed: B
   Assumed: A'
diff --git a/tests/lean/cast3.lean.expected.out b/tests/lean/cast3.lean.expected.out
index 0b2c56e9c3..9b52b76162 100644
--- a/tests/lean/cast3.lean.expected.out
+++ b/tests/lean/cast3.lean.expected.out
@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast.lean'
   Assumed: A
   Assumed: A'
   Assumed: B
diff --git a/tests/lean/cast4.lean.expected.out b/tests/lean/cast4.lean.expected.out
index 59f4e9d905..bff990e8d7 100644
--- a/tests/lean/cast4.lean.expected.out
+++ b/tests/lean/cast4.lean.expected.out
@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast'
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU
diff --git a/tests/lean/discharge.lean.expected.out b/tests/lean/discharge.lean.expected.out
index c9da3cd332..f628955447 100644
--- a/tests/lean/discharge.lean.expected.out
+++ b/tests/lean/discharge.lean.expected.out
@@ -1,4 +1,5 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'tactic'
 @Discharge : Π (a b : Bool), (a → b) → (a ⇒ b)
   Proved: T
diff --git a/tests/lean/disj1.lean.expected.out b/tests/lean/disj1.lean.expected.out
index 03e073b159..e45fcf2db6 100644
--- a/tests/lean/disj1.lean.expected.out
+++ b/tests/lean/disj1.lean.expected.out
@@ -1,5 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'tactic'
   Proved: T1
   Proved: T2
 Theorem T2 (a b : Bool) : a ∨ b ⇒ b ∨ a :=
diff --git a/tests/lean/mod1.lean.expected.out b/tests/lean/mod1.lean.expected.out
index f5a3e3192d..adf445a01d 100644
--- a/tests/lean/mod1.lean.expected.out
+++ b/tests/lean/mod1.lean.expected.out
@@ -1,9 +1,9 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: x
-  Assumed: y
-  Assumed: x
-  Assumed: y
+  Imported 'simple'
+  Skipped 'simple'
+  Imported 'simple.lean'
+  Skipped 'simple.lean'
 x + y : ℤ
   Assumed: z
 z : ℤ
diff --git a/tests/lean/norm_bug1.lean.expected.out b/tests/lean/norm_bug1.lean.expected.out
index b0d3c6bddc..2db1d9aff0 100644
--- a/tests/lean/norm_bug1.lean.expected.out
+++ b/tests/lean/norm_bug1.lean.expected.out
@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast.lean'
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU
diff --git a/tests/lean/norm_tac.lean.expected.out b/tests/lean/norm_tac.lean.expected.out
index c8d9283d40..bf964344d7 100644
--- a/tests/lean/norm_tac.lean.expected.out
+++ b/tests/lean/norm_tac.lean.expected.out
@@ -1,5 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'tactic'
   Set: lean::pp::implicit
   Set: lean::pp::coercion
   Set: lean::pp::notation
diff --git a/tests/lean/type_inf_bug1.lean.expected.out b/tests/lean/type_inf_bug1.lean.expected.out
index 4cdca5f3d3..e52bc4c939 100644
--- a/tests/lean/type_inf_bug1.lean.expected.out
+++ b/tests/lean/type_inf_bug1.lean.expected.out
@@ -1,10 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-  Assumed: cast
-  Assumed: CastEq
-  Assumed: CastApp
-  Assumed: DomInj
-  Assumed: RanInj
+  Imported 'cast.lean'
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU