content: {-|
  Module      : Idris.Elab.Value
  Description : Code to elaborate values.
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  {-# LANGUAGE PatternGuards #-}
  {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
  module Idris.Elab.Value(
      elabVal, elabValBind, elabDocTerms
    , elabExec, elabREPL
    ) where
  
  import Idris.AbsSyntax
  import Idris.Core.Elaborate hiding (Tactic(..))
  import Idris.Core.Evaluate hiding (Unchecked)
  import Idris.Core.TT
  import Idris.Docstrings
  import Idris.Elab.Term
  import Idris.Elab.Utils
  import Idris.Error
  import Idris.Output (sendHighlighting)
  
  import Prelude hiding (id, (.))
  
  import Control.Category
  import Data.Char (toLower)
  import qualified Data.Set as S ()
  import qualified Data.Traversable as Traversable
  
  -- | Elaborate a value, returning any new bindings created (this will only
  -- happen if elaborating as a pattern clause)
  elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
  elabValBind info aspat norm tm_in
     = do ctxt <- getContext
          i <- getIState
          let tm = addImpl [] i tm_in
          logElab 10 (showTmImpls tm)
          -- try:
          --    * ordinary elaboration
          --    * elaboration as a Type
          --    * elaboration as a function a -> b
  
          (ElabResult tm' defer is ctxt' newDecls highlights newGName, _) <-
               tclift (elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "val") infP initEState
                       (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))
  
          -- Extend the context with new definitions created
          setContext ctxt'
          processTacticDecls info newDecls
          sendHighlighting highlights
          updateIState $ \i -> i { idris_name = newGName }
  
          let vtm = orderPats (getInferTerm tm')
  
          def' <- checkDef info (fileFC "(input)") iderr True defer
          let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) def'
          addDeferred def''
          mapM_ (elabCaseBlock info []) is
  
          logElab 3 ("Value: " ++ show vtm)
          (vtm_in, vty) <- recheckC (constraintNS info) (fileFC "(input)") id [] vtm
  
          let vtm = if norm then normalise (tt_ctxt i) [] vtm_in
                            else vtm_in
          let bargs = getPBtys vtm
  
          return (vtm, vty, bargs)
  
  elabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)
  elabVal info aspat tm_in
     = do (tm, ty, _) <- elabValBind info aspat False tm_in
          return (tm, ty)
  
  
  
  elabDocTerms :: ElabInfo -> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
  elabDocTerms info str = do typechecked <- Traversable.mapM decorate str
                             return $ checkDocstring mkDocTerm typechecked
    where decorate (Left err) = return (Left err)
          decorate (Right pt) = fmap (fmap fst) (tryElabVal info ERHS pt)
  
          tryElabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Either Err (Term, Type))
          tryElabVal info aspat tm_in
             = idrisCatch (fmap Right $ elabVal info aspat tm_in)
                          (return . Left)
  
          mkDocTerm :: String -> [String] -> String -> Either Err Term -> DocTerm
          mkDocTerm lang attrs src (Left err)
            | map toLower lang == "idris" = Failing err
            | otherwise                   = Unchecked
          mkDocTerm lang attrs src (Right tm)
            | map toLower lang == "idris" = if "example" `elem` map (map toLower) attrs
                                              then Example tm
                                              else Checked tm
            | otherwise                   = Unchecked
  
  -- | Try running the term directly (as IO ()) or with >>= printLn appended
  -- (for other IO _), then printing it as an Integer (as a default numeric
  -- type), then printing it as any Showable thing
  elabExec :: FC -> PTerm -> PTerm
  elabExec fc tm = runtm (PAlternative [] FirstSuccess
                     [printtm (PApp fc (PRef fc [] (sUN "the"))
                       [pexp (PConstant NoFC (AType (ATInt ITBig))), pexp tm]),
                      tm,
                      PApp fc (PRef fc [] (sUN ">>="))
                       [pexp tm, pexp (PRef fc [] (sUN "printLn"))],
                      printtm tm
                      ])
    where
      runtm t = PApp fc (PRef fc [] (sUN "run__IO"))
                    [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]
      printtm t = PApp fc (PRef fc [] (sUN "printLn")) [pexp t]
  
  elabREPL :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)
  elabREPL info aspat tm
      = idrisCatch (elabVal info aspat tm) catchAmbig
    where
      catchAmbig (CantResolveAlts _)
         = elabVal info aspat (PDisamb [[txt "List"]] tm)
      catchAmbig (NoValidAlts _)
         = elabVal info aspat (PDisamb [[txt "List"]] tm)
      catchAmbig e = ierror e
  