{-|
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 = forall n. AppStatus n -> TT n -> TT n -> TT n
App forall n. AppStatus n
Complete (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"]) forall n. TT n
Erased)
                   (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref Name
unitTy 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 ()
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Error Err
e -> 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) <-
        forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ 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
                 (forall aux a. (Err -> Err) -> Elab' aux a -> Elab' aux a
transformErr forall t. Err' t -> Err' t
RunningElabScript
                   (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)]
_ <- forall aux. Elab' aux aux
getAux
                                Context
ctxt <- forall aux. Elab' aux Context
get_context
                                let ds :: [a]
ds = [] -- todo
                                String
log <- forall aux. Elab' aux String
getLog
                                Int
newGName <- forall aux. Elab' aux Int
get_global_nextname
                                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 forall a. [a]
ds (forall a b. (a -> b) -> [a] -> [b]
map 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 forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }