content: {-|
  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 = 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 -- First elaborate the script itself
       (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 = [] -- 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 $ \i -> i { idris_name = newGName }
  