module Idris.Elab.RunElab (elabRunElab) where
import Idris.AbsSyntax
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Elab.Term
import Idris.Elab.Value (elabVal)
import Idris.Error
import Idris.Output (sendHighlighting)
elabScriptTy :: Type
elabScriptTy = App Complete (P Ref (sNS (sUN "Elab") ["Elab", "Reflection", "Language"]) Erased)
(P Ref unitTy Erased)
mustBeElabScript :: Type -> Idris ()
mustBeElabScript ty =
do ctxt <- getContext
case converts ctxt [] ty elabScriptTy of
OK _ -> return ()
Error e -> ierror e
elabRunElab :: ElabInfo -> FC -> PTerm -> [String] -> Idris ()
elabRunElab info fc script' ns =
do
(script, scriptTy) <- elabVal info ERHS script'
mustBeElabScript scriptTy
ist <- getIState
ctxt <- getContext
(ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-
tclift $ elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState
(transformErr RunningElabScript
(erun fc (do tm <- runElabAction info ist fc [] script ns
EState is _ impls highlights _ _ <- getAux
ctxt <- get_context
let ds = []
log <- getLog
newGName <- get_global_nextname
return (ElabResult tm ds (map snd is) ctxt impls highlights newGName))))
setContext ctxt'
processTacticDecls info newDecls
sendHighlighting highlights
updateIState $ \i -> i { idris_name = newGName }