From 55626ba60de3bdbfc097ba231f0d81127b2cc2ea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 5 Jun 2019 15:20:02 -0700
Subject: [PATCH] chore(library/init/lean): disable new frontend for now

We are going to start making drastic changes in the parser,
elaborator, attributes, etc. Examples:
- No View objects. I am going to implement match_syntax.
- No RecT in the parser. I am going to implement parser extensions
using an approach similar to the one I used to implement environment
extensions.
- No Parsec. I will use an approach similar to the one used in the
experiment https://github.com/leanprover/lean4/tree/master/tests/playground/parser

It is easier to perform these changes with the new frontend disabled.
I will slowly re-active it as I apply the changes.

cc @kha
---
 library/init/lean/attributes.lean             |  5 ++--
 library/init/lean/default.lean                |  1 -
 library/init/lean/name_mangling.lean          |  4 +--
 library/init/lean/position.lean               | 25 +------------------
 src/shell/lean.cpp                            |  4 ++-
 .../lean => tmp/new-frontend}/elaborator.lean |  0
 .../lean => tmp/new-frontend}/expander.lean   |  0
 .../lean => tmp/new-frontend}/frontend.lean   |  0
 .../new-frontend}/parser/basic.lean           |  0
 .../new-frontend}/parser/combinators.lean     |  0
 .../new-frontend}/parser/command.lean         |  0
 .../new-frontend}/parser/declaration.lean     |  0
 .../new-frontend}/parser/identifier.lean      |  0
 .../new-frontend}/parser/level.lean           |  0
 .../new-frontend}/parser/module.lean          |  0
 .../new-frontend}/parser/notation.lean        |  0
 .../new-frontend}/parser/parsec.lean          |  0
 .../new-frontend}/parser/pratt.lean           |  0
 .../lean => tmp/new-frontend}/parser/rec.lean |  0
 .../new-frontend}/parser/stringliteral.lean   |  0
 .../new-frontend}/parser/syntax.lean          |  0
 .../new-frontend}/parser/term.lean            |  0
 .../new-frontend}/parser/token.lean           |  0
 .../new-frontend}/parser/trie.lean            |  0
 24 files changed, 8 insertions(+), 31 deletions(-)
 rename {library/init/lean => tmp/new-frontend}/elaborator.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/expander.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/frontend.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/basic.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/combinators.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/command.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/declaration.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/identifier.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/level.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/module.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/notation.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/parsec.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/pratt.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/rec.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/stringliteral.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/syntax.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/term.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/token.lean (100%)
 rename {library/init/lean => tmp/new-frontend}/parser/trie.lean (100%)

diff --git a/library/init/lean/attributes.lean b/library/init/lean/attributes.lean
index 86e85fb590..3308fac238 100644
--- a/library/init/lean/attributes.lean
+++ b/library/init/lean/attributes.lean
@@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.environment init.lean.parser.syntax
+import init.lean.environment
 
 namespace Lean
-open Lean.Parser
+def Syntax := Unit -- Temporary hack
+def Syntax.missing := () -- Temporary hack
 
 /- Scope management -/
 
diff --git a/library/init/lean/default.lean b/library/init/lean/default.lean
index c6409573fd..473f5acd1a 100644
--- a/library/init/lean/default.lean
+++ b/library/init/lean/default.lean
@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.lean.compiler
-import init.lean.frontend
 import init.lean.extern
 import init.lean.environment
 import init.lean.modifiers
diff --git a/library/init/lean/name_mangling.lean b/library/init/lean/name_mangling.lean
index d65ed26467..5d5900f57c 100644
--- a/library/init/lean/name_mangling.lean
+++ b/library/init/lean/name_mangling.lean
@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.lean.name init.lean.parser.stringliteral
+import init.lean.name
 namespace Lean
-open Lean.Parser
-open Lean.Parser.MonadParsec
 
 private def String.mangleAux : Nat → String.Iterator → String → String
 | 0     it r := r
diff --git a/library/init/lean/position.lean b/library/init/lean/position.lean
index 70678be580..e82cada81d 100644
--- a/library/init/lean/position.lean
+++ b/library/init/lean/position.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import init.data.nat init.data.rbmap init.lean.format init.lean.parser.parsec
+import init.data.nat init.data.rbmap init.lean.format
 
 namespace Lean
 
@@ -29,27 +29,4 @@ instance : HasFormat Position :=
 instance : Inhabited Position := ⟨⟨1, 0⟩⟩
 end Position
 
-/-- A precomputed cache for quickly mapping Char offsets to positionitions. -/
-structure FileMap :=
--- A mapping from Char offset of line start to line index
-(lines : RBMap Nat Nat (λ a b, a < b))
-
-namespace FileMap
-private def fromStringAux : Nat → String.OldIterator → Nat → List (Nat × Nat)
-| 0     it line := []
-| (k+1) it line :=
-  if it.hasNext = false then []
-  else match it.curr with
-       | '\n'  := (it.next.offset, line+1) :: fromStringAux k it.next (line+1)
-       | other := fromStringAux k it.next line
-
-def fromString (s : String) : FileMap :=
-{lines := RBMap.ofList $ fromStringAux s.length s.mkOldIterator 1}
-
-def toPosition (m : FileMap) (off : Nat) : Position :=
-match m.lines.lowerBound off with
-| some ⟨start, l⟩ := ⟨l, off - start⟩
-| none            := ⟨1, off⟩
-end FileMap
-
 end Lean
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index c00c7f7ad0..6bc6163916 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -154,7 +154,7 @@ int getopt_long(int argc, char *in_argv[], const char *optstring, const option *
 
 using namespace lean; // NOLINT
 
-object * lean_process_file(object * filename, object * contents, uint8 json, object * env, object * world);
+// object * lean_process_file(object * filename, object * contents, uint8 json, object * env, object * world);
 
 #ifndef LEAN_SERVER_DEFAULT_MAX_MEMORY
 #define LEAN_SERVER_DEFAULT_MAX_MEMORY 1024
@@ -505,6 +505,7 @@ int main(int argc, char ** argv) {
 
         bool ok;
         if (new_frontend) {
+#if 0
             env.set_main_module(main_module_name);
             // Some C++ parts like profiling need a global message log. We may want to refactor them into a
             // message_log-passing state monad in the future.
@@ -521,6 +522,7 @@ int main(int argc, char ** argv) {
                 ok = true;
                 env = environment(cnstr_get(io_result_get_value(res.raw()), 1), true);
             }
+#endif
         } else {
             message_log l;
             scope_message_log scope_log(l);
diff --git a/library/init/lean/elaborator.lean b/tmp/new-frontend/elaborator.lean
similarity index 100%
rename from library/init/lean/elaborator.lean
rename to tmp/new-frontend/elaborator.lean
diff --git a/library/init/lean/expander.lean b/tmp/new-frontend/expander.lean
similarity index 100%
rename from library/init/lean/expander.lean
rename to tmp/new-frontend/expander.lean
diff --git a/library/init/lean/frontend.lean b/tmp/new-frontend/frontend.lean
similarity index 100%
rename from library/init/lean/frontend.lean
rename to tmp/new-frontend/frontend.lean
diff --git a/library/init/lean/parser/basic.lean b/tmp/new-frontend/parser/basic.lean
similarity index 100%
rename from library/init/lean/parser/basic.lean
rename to tmp/new-frontend/parser/basic.lean
diff --git a/library/init/lean/parser/combinators.lean b/tmp/new-frontend/parser/combinators.lean
similarity index 100%
rename from library/init/lean/parser/combinators.lean
rename to tmp/new-frontend/parser/combinators.lean
diff --git a/library/init/lean/parser/command.lean b/tmp/new-frontend/parser/command.lean
similarity index 100%
rename from library/init/lean/parser/command.lean
rename to tmp/new-frontend/parser/command.lean
diff --git a/library/init/lean/parser/declaration.lean b/tmp/new-frontend/parser/declaration.lean
similarity index 100%
rename from library/init/lean/parser/declaration.lean
rename to tmp/new-frontend/parser/declaration.lean
diff --git a/library/init/lean/parser/identifier.lean b/tmp/new-frontend/parser/identifier.lean
similarity index 100%
rename from library/init/lean/parser/identifier.lean
rename to tmp/new-frontend/parser/identifier.lean
diff --git a/library/init/lean/parser/level.lean b/tmp/new-frontend/parser/level.lean
similarity index 100%
rename from library/init/lean/parser/level.lean
rename to tmp/new-frontend/parser/level.lean
diff --git a/library/init/lean/parser/module.lean b/tmp/new-frontend/parser/module.lean
similarity index 100%
rename from library/init/lean/parser/module.lean
rename to tmp/new-frontend/parser/module.lean
diff --git a/library/init/lean/parser/notation.lean b/tmp/new-frontend/parser/notation.lean
similarity index 100%
rename from library/init/lean/parser/notation.lean
rename to tmp/new-frontend/parser/notation.lean
diff --git a/library/init/lean/parser/parsec.lean b/tmp/new-frontend/parser/parsec.lean
similarity index 100%
rename from library/init/lean/parser/parsec.lean
rename to tmp/new-frontend/parser/parsec.lean
diff --git a/library/init/lean/parser/pratt.lean b/tmp/new-frontend/parser/pratt.lean
similarity index 100%
rename from library/init/lean/parser/pratt.lean
rename to tmp/new-frontend/parser/pratt.lean
diff --git a/library/init/lean/parser/rec.lean b/tmp/new-frontend/parser/rec.lean
similarity index 100%
rename from library/init/lean/parser/rec.lean
rename to tmp/new-frontend/parser/rec.lean
diff --git a/library/init/lean/parser/stringliteral.lean b/tmp/new-frontend/parser/stringliteral.lean
similarity index 100%
rename from library/init/lean/parser/stringliteral.lean
rename to tmp/new-frontend/parser/stringliteral.lean
diff --git a/library/init/lean/parser/syntax.lean b/tmp/new-frontend/parser/syntax.lean
similarity index 100%
rename from library/init/lean/parser/syntax.lean
rename to tmp/new-frontend/parser/syntax.lean
diff --git a/library/init/lean/parser/term.lean b/tmp/new-frontend/parser/term.lean
similarity index 100%
rename from library/init/lean/parser/term.lean
rename to tmp/new-frontend/parser/term.lean
diff --git a/library/init/lean/parser/token.lean b/tmp/new-frontend/parser/token.lean
similarity index 100%
rename from library/init/lean/parser/token.lean
rename to tmp/new-frontend/parser/token.lean
diff --git a/library/init/lean/parser/trie.lean b/tmp/new-frontend/parser/trie.lean
similarity index 100%
rename from library/init/lean/parser/trie.lean
rename to tmp/new-frontend/parser/trie.lean