{-|
Module      : Idris.Elab.RunElab
Description : Code to run the elaborator process.

License     : BSD3
Maintainer  : The Idris Community.
-}
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 -- First elaborate the script itself
     (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 = [] -- todo
                                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 }