refactor: cleanup

src/Init/Lean/Elab.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Init.Lean.Elab.Basic
+import Init.Lean.Elab.Import
+import Init.Lean.Elab.Exception
 import Init.Lean.Elab.ElabStrategyAttrs
 import Init.Lean.Elab.Command
 import Init.Lean.Elab.Term

src/Init/Lean/Elab/Command.lean

@@ -5,12 +5,14 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Elab.Alias
-import Init.Lean.Elab.Basic
 import Init.Lean.Elab.ResolveName
 import Init.Lean.Elab.Term
 
 namespace Lean
 namespace Elab
+
+
+
 /-
 private def addScopes (cmd : String) (updateNamespace : Bool) : Name → List ElabScope → List ElabScope
 | Name.anonymous, scopes => scopes

src/Init/Lean/Elab/Exception.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Meta
+
+namespace Lean
+namespace Elab
+
+inductive Exception
+| io     : IO.Error → Exception
+| msg    : Message → Exception
+| kernel : KernelException → Exception
+| meta   : Meta.Exception → Exception
+| other  : String → Exception
+/- Elab.Exception.silent is used when we log an error in `messages`, and then
+   want to interrupt the elaborator execution. We use it to make sure the
+   top-level handler does not record it again in `messages`. See `logErrorAndThrow` -/
+| silent : Exception
+
+instance Exception.inhabited : Inhabited Exception := ⟨Exception.silent⟩
+
+end Elab
+end Lean

src/Init/Lean/Elab/Import.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import Init.Lean.Parser.Module
+
+namespace Lean
+namespace Elab
+
+def headerToImports (header : Syntax) : List Import :=
+let header  := header.asNode;
+let imports := if (header.getArg 0).isNone then [{Import . module := `Init.Default}] else [];
+imports ++ (header.getArg 1).getArgs.toList.map (fun stx =>
+  -- `stx` is of the form `(Module.import "import" "runtime"? id)
+  let runtime := !(stx.getArg 1).isNone;
+  let id      := stx.getIdAt 2;
+  { module := normalizeModuleName id, runtimeOnly := runtime })
+
+def processHeader (header : Syntax) (messages : MessageLog) (ctx : Parser.ParserContextCore) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) :=
+catch
+  (do env ← importModules (headerToImports header) trustLevel;
+      pure (env, messages))
+  (fun e => do
+     env ← mkEmptyEnvironment;
+     let spos := header.getPos.getD 0;
+     let pos  := ctx.fileMap.toPosition spos;
+     pure (env, messages.add { fileName := ctx.fileName, data := toString e, pos := pos }))
+
+@[export lean_parse_imports]
+def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) :=
+do env ← mkEmptyEnvironment;
+   let fileName := fileName.getD "<input>";
+   let ctx := Parser.mkParserContextCore env input fileName;
+   match Parser.parseHeader env ctx with
+   | (header, parserState, messages) => do
+     pure (headerToImports header, ctx.fileMap.toPosition parserState.pos, messages)
+
+@[export lean_print_deps]
+def printDeps (deps : List Import) : IO Unit :=
+deps.forM $ fun dep => do
+  fname ← findOLean dep.module;
+  IO.println fname
+
+end Elab
+end Lean

src/Init/Lean/Elab/ResolveName.lean

@@ -6,11 +6,29 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 prelude
 import Init.Lean.Modifiers
 import Init.Lean.Elab.Alias
-import Init.Lean.Elab.Basic
 
 namespace Lean
 namespace Elab
 
+inductive OpenDecl
+| simple   (ns : Name) (except : List Name)
+| explicit (id : Name) (declName : Name)
+
+namespace OpenDecl
+instance : Inhabited OpenDecl := ⟨simple Name.anonymous []⟩
+
+instance : HasToString OpenDecl :=
+⟨fun decl => match decl with
+ | explicit id decl => toString id ++ " → " ++ toString decl
+ | simple ns ex     => toString ns ++ (if ex == [] then "" else " hiding " ++ toString ex)⟩
+
+end OpenDecl
+
+def rootNamespace := `_root_
+
+def removeRoot (n : Name) : Name :=
+n.replacePrefix rootNamespace Name.anonymous
+
 /- Check whether `ns ++ id` is a valid namepace name and/or there are aliases names `ns ++ id`. -/
 private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name :=
 let resolvedId  := ns ++ id;

src/Init/Lean/Elab/Term.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Elab.Alias
-import Init.Lean.Elab.Basic
 
 namespace Lean
 namespace Elab

tmp/Basic.lean

@@ -5,30 +5,11 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Init.Control.Reader
-import Init.Lean.MetavarContext
-import Init.Lean.Scopes
+import Init.Lean.Meta
 import Init.Lean.Parser.Module
 
 namespace Lean
-
-inductive OpenDecl
-| simple   (ns : Name) (except : List Name)
-| explicit (id : Name) (declName : Name)
-
-namespace OpenDecl
-instance : Inhabited OpenDecl := ⟨simple Name.anonymous []⟩
-
-instance : HasToString OpenDecl :=
-⟨fun decl => match decl with
- | explicit id decl => toString id ++ " → " ++ toString decl
- | simple ns ex     => toString ns ++ (if ex == [] then "" else " hiding " ++ toString ex)⟩
-
-end OpenDecl
-
-def rootNamespace := `_root_
-
-def removeRoot (n : Name) : Name :=
-n.replacePrefix rootNamespace Name.anonymous
+namespace Elab
 
 /-
 structure ElabContext :=
@@ -354,43 +335,7 @@ partial def processCommandsAux : Unit → Frontend Unit
 
 def processCommands : Frontend Unit :=
 processCommandsAux ()
--/
 
-def headerToImports (header : Syntax) : List Import :=
-let header  := header.asNode;
-let imports := if (header.getArg 0).isNone then [{Import . module := `Init.Default}] else [];
-imports ++ (header.getArg 1).getArgs.toList.map (fun stx =>
-  -- `stx` is of the form `(Module.import "import" "runtime"? id)
-  let runtime := !(stx.getArg 1).isNone;
-  let id      := stx.getIdAt 2;
-  { module := normalizeModuleName id, runtimeOnly := runtime })
-
-def processHeader (header : Syntax) (messages : MessageLog) (ctx : Parser.ParserContextCore) (trustLevel : UInt32 := 0) : IO (Environment × MessageLog) :=
-catch
-  (do env ← importModules (headerToImports header) trustLevel;
-      pure (env, messages))
-  (fun e => do
-     env ← mkEmptyEnvironment;
-     let spos := header.getPos.getD 0;
-     let pos  := ctx.fileMap.toPosition spos;
-     pure (env, messages.add { fileName := ctx.fileName, data := toString e, pos := pos }))
-
-@[export lean_parse_imports]
-def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) :=
-do env ← mkEmptyEnvironment;
-   let fileName := fileName.getD "<input>";
-   let ctx := Parser.mkParserContextCore env input fileName;
-   match Parser.parseHeader env ctx with
-   | (header, parserState, messages) => do
-     pure (headerToImports header, ctx.fileMap.toPosition parserState.pos, messages)
-
-@[export lean_print_deps]
-def printDeps (deps : List Import) : IO Unit :=
-deps.forM $ fun dep => do
-  fname ← findOLean dep.module;
-  IO.println fname
-
-/-
 def testFrontend (input : String) (fileName : Option String := none) : IO (Environment × MessageLog) :=
 do env ← mkEmptyEnvironment;
    let fileName := fileName.getD "<input>";
@@ -520,4 +465,5 @@ constant runIO {α : Type} (x : IO α) : Elab α := arbitrary _
 
 end Elab
 -/
+end Elab
 end Lean