{-|
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 :: ElabInfo
-> ElabMode -> Bool -> PTerm -> Idris (Term, Term, [(Name, Term)])
elabValBind ElabInfo
info ElabMode
aspat Bool
norm PTerm
tm_in
   = do ctxt <- Idris Context
getContext
        i <- getIState
        let tm = [Name] -> IState -> PTerm -> PTerm
addImpl [] IState
i PTerm
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 $ \IState
i -> IState
i { idris_name = newGName }

        let vtm = Term -> Term
orderPats (Term -> Term
getInferTerm Term
tm')

        def' <- checkDef info (fileFC "(input)") iderr True defer
        let def'' = ((Name, (Int, Maybe Name, Term, [Name]))
 -> (Name, (Int, Maybe Name, Term, [Name], Bool, Bool)))
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, (Int
i, Maybe Name
top, Term
t, [Name]
ns)) -> (Name
n, (Int
i, Maybe Name
top, Term
t, [Name]
ns, Bool
True, Bool
True))) [(Name, (Int, Maybe Name, Term, [Name]))]
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 Bool
norm then Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
i) [] Term
vtm_in
                          else Term
vtm_in
        let bargs = Term -> [(Name, Term)]
forall {a}. TT a -> [(a, TT a)]
getPBtys Term
vtm

        return (vtm, vty, bargs)

elabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)
elabVal :: ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
aspat PTerm
tm_in
   = do (tm, ty, _) <- ElabInfo
-> ElabMode -> Bool -> PTerm -> Idris (Term, Term, [(Name, Term)])
elabValBind ElabInfo
info ElabMode
aspat Bool
False PTerm
tm_in
        return (tm, ty)



elabDocTerms :: ElabInfo -> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms :: ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
str = do typechecked <- (Either Err PTerm
 -> StateT IState (ExceptT Err IO) (Either Err Term))
-> Docstring (Either Err PTerm)
-> StateT IState (ExceptT Err IO) (Docstring (Either Err Term))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Docstring a -> m (Docstring b)
Traversable.mapM Either Err PTerm
-> StateT IState (ExceptT Err IO) (Either Err Term)
decorate Docstring (Either Err PTerm)
str
                           return $ checkDocstring mkDocTerm typechecked
  where decorate :: Either Err PTerm
-> StateT IState (ExceptT Err IO) (Either Err Term)
decorate (Left Err
err) = Either Err Term -> StateT IState (ExceptT Err IO) (Either Err Term)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err -> Either Err Term
forall a b. a -> Either a b
Left Err
err)
        decorate (Right PTerm
pt) = (Either Err (Term, Term) -> Either Err Term)
-> StateT IState (ExceptT Err IO) (Either Err (Term, Term))
-> StateT IState (ExceptT Err IO) (Either Err Term)
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Term, Term) -> Term)
-> Either Err (Term, Term) -> Either Err Term
forall a b. (a -> b) -> Either Err a -> Either Err b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Term
forall a b. (a, b) -> a
fst) (ElabInfo
-> ElabMode
-> PTerm
-> StateT IState (ExceptT Err IO) (Either Err (Term, Term))
tryElabVal ElabInfo
info ElabMode
ERHS PTerm
pt)

        tryElabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Either Err (Term, Type))
        tryElabVal :: ElabInfo
-> ElabMode
-> PTerm
-> StateT IState (ExceptT Err IO) (Either Err (Term, Term))
tryElabVal ElabInfo
info ElabMode
aspat PTerm
tm_in
           = StateT IState (ExceptT Err IO) (Either Err (Term, Term))
-> (Err
    -> StateT IState (ExceptT Err IO) (Either Err (Term, Term)))
-> StateT IState (ExceptT Err IO) (Either Err (Term, Term))
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (((Term, Term) -> Either Err (Term, Term))
-> StateT IState (ExceptT Err IO) (Term, Term)
-> StateT IState (ExceptT Err IO) (Either Err (Term, Term))
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Term, Term) -> Either Err (Term, Term)
forall a b. b -> Either a b
Right (StateT IState (ExceptT Err IO) (Term, Term)
 -> StateT IState (ExceptT Err IO) (Either Err (Term, Term)))
-> StateT IState (ExceptT Err IO) (Term, Term)
-> StateT IState (ExceptT Err IO) (Either Err (Term, Term))
forall a b. (a -> b) -> a -> b
$ ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
aspat PTerm
tm_in)
                        (Either Err (Term, Term)
-> StateT IState (ExceptT Err IO) (Either Err (Term, Term))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Err (Term, Term)
 -> StateT IState (ExceptT Err IO) (Either Err (Term, Term)))
-> (Err -> Either Err (Term, Term))
-> Err
-> StateT IState (ExceptT Err IO) (Either Err (Term, Term))
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Err -> Either Err (Term, Term)
forall a b. a -> Either a b
Left)

        mkDocTerm :: String -> [String] -> String -> Either Err Term -> DocTerm
        mkDocTerm :: [Char] -> [[Char]] -> [Char] -> Either Err Term -> DocTerm
mkDocTerm [Char]
lang [[Char]]
attrs [Char]
src (Left Err
err)
          | (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower [Char]
lang [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"idris" = Err -> DocTerm
Failing Err
err
          | Bool
otherwise                   = DocTerm
Unchecked
        mkDocTerm [Char]
lang [[Char]]
attrs [Char]
src (Right Term
tm)
          | (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower [Char]
lang [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"idris" = if [Char]
"example" [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char] -> [Char]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower) [[Char]]
attrs
                                            then Term -> DocTerm
Example Term
tm
                                            else Term -> DocTerm
Checked Term
tm
          | Bool
otherwise                   = DocTerm
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 -> PTerm -> PTerm
elabExec FC
fc PTerm
tm = PTerm -> PTerm
runtm ([(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [] PAltType
FirstSuccess
                   [PTerm -> PTerm
printtm (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Char] -> Name
sUN [Char]
"the"))
                     [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> Const -> PTerm
PConstant FC
NoFC (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITBig))), PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
tm]),
                    PTerm
tm,
                    FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Char] -> Name
sUN [Char]
">>="))
                     [PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
tm, PTerm -> PArg
forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Char] -> Name
sUN [Char]
"printLn"))],
                    PTerm -> PTerm
printtm PTerm
tm
                    ])
  where
    runtm :: PTerm -> PTerm
runtm PTerm
t = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Char] -> Name
sUN [Char]
"run__IO"))
                  [Name -> PTerm -> Bool -> PArg
forall {t}. Name -> t -> Bool -> PArg' t
pimp ([Char] -> Name
sUN [Char]
"ffi") (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Char] -> Name
sUN [Char]
"FFI_C")) Bool
False, PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
t]
    printtm :: PTerm -> PTerm
printtm PTerm
t = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] ([Char] -> Name
sUN [Char]
"printLn")) [PTerm -> PArg
forall {t}. t -> PArg' t
pexp PTerm
t]

elabREPL :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)
elabREPL :: ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabREPL ElabInfo
info ElabMode
aspat PTerm
tm
    = StateT IState (ExceptT Err IO) (Term, Term)
-> (Err -> StateT IState (ExceptT Err IO) (Term, Term))
-> StateT IState (ExceptT Err IO) (Term, Term)
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
aspat PTerm
tm) Err -> StateT IState (ExceptT Err IO) (Term, Term)
catchAmbig
  where
    catchAmbig :: Err -> StateT IState (ExceptT Err IO) (Term, Term)
catchAmbig (CantResolveAlts [Name]
_)
       = ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
aspat ([[Text]] -> PTerm -> PTerm
PDisamb [[[Char] -> Text
txt [Char]
"List"]] PTerm
tm)
    catchAmbig (NoValidAlts [Name]
_)
       = ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
aspat ([[Text]] -> PTerm -> PTerm
PDisamb [[[Char] -> Text
txt [Char]
"List"]] PTerm
tm)
    catchAmbig Err
e = Err -> StateT IState (ExceptT Err IO) (Term, Term)
forall a. Err -> Idris a
ierror Err
e