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 :: Type
elabScriptTy = AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Elab") [String
"Elab", String
"Reflection", String
"Language"]) Type
forall n. TT n
Erased)
(NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
unitTy Type
forall n. TT n
Erased)
mustBeElabScript :: Type -> Idris ()
mustBeElabScript :: Type -> Idris ()
mustBeElabScript Type
ty =
do Context
ctxt <- Idris Context
getContext
case Context -> Env -> Type -> Type -> TC ()
converts Context
ctxt [] Type
ty Type
elabScriptTy of
OK ()
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Error Err
e -> Err -> Idris ()
forall a. Err -> Idris a
ierror Err
e
elabRunElab :: ElabInfo -> FC -> PTerm -> [String] -> Idris ()
elabRunElab :: ElabInfo -> FC -> PTerm -> [String] -> Idris ()
elabRunElab ElabInfo
info FC
fc PTerm
script' [String]
ns =
do
(Type
script, Type
scriptTy) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal ElabInfo
info ElabMode
ERHS PTerm
script'
Type -> Idris ()
mustBeElabScript Type
scriptTy
IState
ist <- Idris IState
getIState
Context
ctxt <- Idris Context
getContext
(ElabResult Type
tyT' [(Name, (Int, Maybe Name, Type, [Name]))]
defer [PDecl]
is Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName, String
log) <-
TC (ElabResult, String) -> Idris (ElabResult, String)
forall a. TC a -> Idris a
tclift (TC (ElabResult, String) -> Idris (ElabResult, String))
-> TC (ElabResult, String) -> Idris (ElabResult, String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> EState
-> Elab' EState ElabResult
-> TC (ElabResult, String)
forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Type
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) (IState -> Int
idris_name IState
ist) (Int -> String -> Name
sMN Int
0 String
"toplLevelElab") Type
elabScriptTy EState
initEState
((Err -> Err) -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. (Err -> Err) -> Elab' aux a -> Elab' aux a
transformErr Err -> Err
forall t. Err' t -> Err' t
RunningElabScript
(FC -> Elab' EState ElabResult -> Elab' EState ElabResult
forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
fc (do Type
tm <- ElabInfo -> IState -> FC -> Env -> Type -> [String] -> ElabD Type
runElabAction ElabInfo
info IState
ist FC
fc [] Type
script [String]
ns
EState [(Name, PDecl)]
is [(Int, Elab' EState ())]
_ [RDeclInstructions]
impls Set (FC', OutputAnnotation)
highlights [Name]
_ [(FC, Name)]
_ <- Elab' EState EState
forall aux. Elab' aux aux
getAux
Context
ctxt <- Elab' EState Context
forall aux. Elab' aux Context
get_context
let ds :: [a]
ds = []
String
log <- Elab' EState String
forall aux. Elab' aux String
getLog
Int
newGName <- Elab' EState Int
forall aux. Elab' aux Int
get_global_nextname
ElabResult -> Elab' EState ElabResult
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> [PDecl]
-> Context
-> [RDeclInstructions]
-> Set (FC', OutputAnnotation)
-> Int
-> ElabResult
ElabResult Type
tm [(Name, (Int, Maybe Name, Type, [Name]))]
forall a. [a]
ds (((Name, PDecl) -> PDecl) -> [(Name, PDecl)] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Name, PDecl) -> PDecl
forall a b. (a, b) -> b
snd [(Name, PDecl)]
is) Context
ctxt [RDeclInstructions]
impls Set (FC', OutputAnnotation)
highlights Int
newGName))))
Context -> Idris ()
setContext Context
ctxt'
ElabInfo -> [RDeclInstructions] -> Idris ()
processTacticDecls ElabInfo
info [RDeclInstructions]
newDecls
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting Set (FC', OutputAnnotation)
highlights
(IState -> IState) -> Idris ()
updateIState ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name = newGName }