{-|
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 ctxt <- Idris Context
getContext
       case converts ctxt [] ty 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
     (script, scriptTy) <- ElabInfo -> ElabMode -> PTerm -> Idris (Type, Type)
elabVal ElabInfo
info ElabMode
ERHS PTerm
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 = [] -- todo
                                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 $ \IState
i -> IState
i { idris_name = newGName }