max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add Lean.Elab.process

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-09 16:04:49 -08:00
parent 86c1e97523
commit d586dc6c68
2 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Init/Lean/Elab/Frontend.lean
View file

@ -62,6 +62,14 @@ end Frontend
open Frontend
def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : Environment × MessageLog :=
let fileName := fileName.getD "<input>";
let ctx := Parser.mkParserContextCore env input fileName;
let cmdState := Command.mkState env {} opts;
match (processCommands ctx).run { commandState := cmdState, parserState := {} } with
| EStateM.Result.ok _ s => (s.commandState.env, s.commandState.messages)
| EStateM.Result.error _ s => (s.commandState.env, s.commandState.messages)
def testFrontend (input : String) (opts : Options := {}) (fileName : Option String := none) : IO (Environment × MessageLog) :=
do env ← mkEmptyEnvironment;
let fileName := fileName.getD "<input>";

9
tests/lean/run/frontend1.lean
View file

@ -3,16 +3,16 @@ open Lean
open Lean.Elab
def run (input : String) : MetaIO Unit :=
do opts ← MetaIO.getOptions;
(env, messages) ← liftM $ testFrontend input opts;
do env ← MetaIO.getEnv;
opts ← MetaIO.getOptions;
let (env, messages) := process input env opts;
messages.toList.forM $ fun msg => IO.println msg;
pure ()
set_option trace.Elab true
#eval run
"import Init.Core
universe u universe v
"universe u universe v
section namespace foo.bla end bla end foo
variable (p q : Prop)
variable (_ b : _)
@ -24,4 +24,5 @@ set_option trace.Elab true
#check α
#check Nat.succ
#check Nat.add
#check run
end"