0 | module TTImp.ProcessRunElab
 1 |
 2 | import Core.Env
 3 | import Core.Metadata
 4 | import Core.Reflect
 5 | import Core.UnifyState
 6 | import Core.Value
 7 |
 8 | import Idris.REPL.Opts
 9 | import Idris.Syntax
10 |
11 | import TTImp.Elab
12 | import TTImp.Elab.Check
13 | import TTImp.Elab.RunElab
14 | import TTImp.TTImp
15 |
16 | %default covering
17 |
18 | export
19 | processRunElab : {vars : _} ->
20 |                  {auto c : Ref Ctxt Defs} ->
21 |                  {auto m : Ref MD Metadata} ->
22 |                  {auto u : Ref UST UState} ->
23 |                  {auto s : Ref Syn SyntaxInfo} ->
24 |                  {auto o : Ref ROpts REPLOpts} ->
25 |                  List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
26 |                  RawImp -> Core ()
27 | processRunElab eopts nest env fc tm
28 |     = do defs <- get Ctxt
29 |          unless (isExtension ElabReflection defs) $
30 |              throw (GenericMsg fc "%language ElabReflection not enabled")
31 |          tidx <- resolveName (UN $ Basic "[elaborator script]")
32 |          let n = NS reflectionNS (UN $ Basic "Elab")
33 |          unit <- getCon fc defs (builtin "Unit")
34 |          exp <- appCon fc defs n [unit]
35 |
36 |          stm <- checkTerm tidx InExpr eopts nest env tm (gnf env exp)
37 |          nfstm <- nfOpts withAll defs env stm
38 |          ignore $ logTime 2 "Elaboration script" $
39 |            elabScript top fc nest env nfstm Nothing
40 |