From c05559a99d82a563ae44eb7ec289c43c30da4fa8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Dec 2019 14:41:39 -0800 Subject: [PATCH] refactor: cleanup --- src/Init/Lean/Elab.lean | 3 +- src/Init/Lean/Elab/Command.lean | 4 +- src/Init/Lean/Elab/Exception.lean | 26 +++++++++++ src/Init/Lean/Elab/Import.lean | 47 ++++++++++++++++++++ src/Init/Lean/Elab/ResolveName.lean | 20 ++++++++- src/Init/Lean/Elab/Term.lean | 1 - {src/Init/Lean/Elab => tmp}/Basic.lean | 60 ++------------------------ 7 files changed, 100 insertions(+), 61 deletions(-) create mode 100644 src/Init/Lean/Elab/Exception.lean create mode 100644 src/Init/Lean/Elab/Import.lean rename {src/Init/Lean/Elab => tmp}/Basic.lean (89%) diff --git a/src/Init/Lean/Elab.lean b/src/Init/Lean/Elab.lean index 10a874bc7e..910f72da46 100644 --- a/src/Init/Lean/Elab.lean +++ b/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 diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean index d2c5181376..42919b858b 100644 --- a/src/Init/Lean/Elab/Command.lean +++ b/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 diff --git a/src/Init/Lean/Elab/Exception.lean b/src/Init/Lean/Elab/Exception.lean new file mode 100644 index 0000000000..9b0d1feaad --- /dev/null +++ b/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 diff --git a/src/Init/Lean/Elab/Import.lean b/src/Init/Lean/Elab/Import.lean new file mode 100644 index 0000000000..0e413e24fc --- /dev/null +++ b/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 ""; + 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 diff --git a/src/Init/Lean/Elab/ResolveName.lean b/src/Init/Lean/Elab/ResolveName.lean index 0240256d95..f215b60fdb 100644 --- a/src/Init/Lean/Elab/ResolveName.lean +++ b/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; diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index d689244798..69794ec92f 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Init/Lean/Elab/Basic.lean b/tmp/Basic.lean similarity index 89% rename from src/Init/Lean/Elab/Basic.lean rename to tmp/Basic.lean index 4a09c985e8..bf4521d756 100644 --- a/src/Init/Lean/Elab/Basic.lean +++ b/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 ""; - 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 ""; @@ -520,4 +465,5 @@ constant runIO {α : Type} (x : IO α) : Elab α := arbitrary _ end Elab -/ +end Elab end Lean