{-# 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
elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
elabValBind :: ElabInfo
-> ElabMode -> Bool -> PTerm -> Idris (Term, Term, [(Name, Term)])
elabValBind info :: ElabInfo
info aspat :: ElabMode
aspat norm :: Bool
norm tm_in :: PTerm
tm_in
= do Context
ctxt <- Idris Context
getContext
IState
i <- Idris IState
getIState
let tm :: PTerm
tm = [Name] -> IState -> PTerm -> PTerm
addImpl [] IState
i PTerm
tm_in
Int -> String -> Idris ()
logElab 10 (PTerm -> String
showTmImpls PTerm
tm)
(ElabResult tm' :: Term
tm' defer :: [(Name, (Int, Maybe Name, Term, [Name]))]
defer is :: [PDecl]
is ctxt' :: Context
ctxt' newDecls :: [RDeclInstructions]
newDecls highlights :: Set (FC', OutputAnnotation)
highlights newGName :: Int
newGName, _) <-
TC (ElabResult, String) -> Idris (ElabResult, String)
forall a. TC a -> Idris a
tclift (String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> EState
-> Elab' EState ElabResult
-> TC (ElabResult, String)
forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate (ElabInfo -> String
constraintNS ElabInfo
info) Context
ctxt (IState -> Ctxt TypeInfo
idris_datatypes IState
i) (IState -> Int
idris_name IState
i) (Int -> String -> Name
sMN 0 "val") Term
infP EState
initEState
(IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> Elab' EState ElabResult
build IState
i ElabInfo
info ElabMode
aspat [FnOpt
Reflection] (Int -> String -> Name
sMN 0 "val") (PTerm -> PTerm
infTerm PTerm
tm)))
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 ((IState -> IState) -> Idris ()) -> (IState -> IState) -> Idris ()
forall a b. (a -> b) -> a -> b
$ \i :: IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }
let vtm :: Term
vtm = Term -> Term
orderPats (Term -> Term
getInferTerm Term
tm')
[(Name, (Int, Maybe Name, Term, [Name]))]
def' <- ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Term, [Name]))]
checkDef ElabInfo
info (String -> FC
fileFC "(input)") Name -> Err -> Err
iderr Bool
True [(Name, (Int, Maybe Name, Term, [Name]))]
defer
let def'' :: [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
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 (\(n :: Name
n, (i :: Int
i, top :: Maybe Name
top, t :: Term
t, ns :: [Name]
ns)) -> (Name
n, (Int
i, Maybe Name
top, Term
t, [Name]
ns, Bool
True, Bool
True))) [(Name, (Int, Maybe Name, Term, [Name]))]
def'
[(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
def''
(PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabInfo -> FnOpts -> PDecl -> Idris ()
elabCaseBlock ElabInfo
info []) [PDecl]
is
Int -> String -> Idris ()
logElab 3 ("Value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
vtm)
(vtm_in :: Term
vtm_in, vty :: Term
vty) <- String
-> FC
-> (Err -> Err)
-> Env
-> Term
-> StateT IState (ExceptT Err IO) (Term, Term)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) (String -> FC
fileFC "(input)") Err -> Err
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Term
vtm
let vtm :: Term
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 :: [(Name, Term)]
bargs = Term -> [(Name, Term)]
forall a. TT a -> [(a, TT a)]
getPBtys Term
vtm
(Term, Term, [(Name, Term)]) -> Idris (Term, Term, [(Name, Term)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
vtm, Term
vty, [(Name, Term)]
bargs)
elabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)
elabVal :: ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal info :: ElabInfo
info aspat :: ElabMode
aspat tm_in :: PTerm
tm_in
= do (tm :: Term
tm, ty :: Term
ty, _) <- ElabInfo
-> ElabMode -> Bool -> PTerm -> Idris (Term, Term, [(Name, Term)])
elabValBind ElabInfo
info ElabMode
aspat Bool
False PTerm
tm_in
(Term, Term) -> StateT IState (ExceptT Err IO) (Term, Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
tm, Term
ty)
elabDocTerms :: ElabInfo -> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms :: ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms info :: ElabInfo
info str :: Docstring (Either Err PTerm)
str = do Docstring (Either Err Term)
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)
Traversable.mapM Either Err PTerm
-> StateT IState (ExceptT Err IO) (Either Err Term)
decorate Docstring (Either Err PTerm)
str
Docstring DocTerm -> Idris (Docstring DocTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring DocTerm -> Idris (Docstring DocTerm))
-> Docstring DocTerm -> Idris (Docstring DocTerm)
forall a b. (a -> b) -> a -> b
$ (String -> [String] -> String -> Either Err Term -> DocTerm)
-> Docstring (Either Err Term) -> Docstring DocTerm
forall a b.
(String -> [String] -> String -> a -> b)
-> Docstring a -> Docstring b
checkDocstring String -> [String] -> String -> Either Err Term -> DocTerm
mkDocTerm Docstring (Either Err Term)
typechecked
where decorate :: Either Err PTerm
-> StateT IState (ExceptT Err IO) (Either Err Term)
decorate (Left err :: Err
err) = Either Err Term -> StateT IState (ExceptT Err IO) (Either Err Term)
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 pt :: 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Term, Term) -> Term)
-> Either Err (Term, Term) -> Either Err Term
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 info :: ElabInfo
info aspat :: ElabMode
aspat tm_in :: 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 (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 (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 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 :: String -> [String] -> String -> Either Err Term -> DocTerm
mkDocTerm lang :: String
lang attrs :: [String]
attrs src :: String
src (Left err :: Err
err)
| (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
lang String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "idris" = Err -> DocTerm
Failing Err
err
| Bool
otherwise = DocTerm
Unchecked
mkDocTerm lang :: String
lang attrs :: [String]
attrs src :: String
src (Right tm :: Term
tm)
| (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
lang String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "idris" = if "example" String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower) [String]
attrs
then Term -> DocTerm
Example Term
tm
else Term -> DocTerm
Checked Term
tm
| Bool
otherwise = DocTerm
Unchecked
elabExec :: FC -> PTerm -> PTerm
elabExec :: FC -> PTerm -> PTerm
elabExec fc :: FC
fc tm :: 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 [] (String -> Name
sUN "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 [] (String -> Name
sUN ">>="))
[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 [] (String -> Name
sUN "printLn"))],
PTerm -> PTerm
printtm PTerm
tm
])
where
runtm :: PTerm -> PTerm
runtm t :: PTerm
t = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN "run__IO"))
[Name -> PTerm -> Bool -> PArg
forall t. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN "ffi") (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN "FFI_C")) Bool
False, PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
t]
printtm :: PTerm -> PTerm
printtm t :: PTerm
t = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN "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 info :: ElabInfo
info aspat :: ElabMode
aspat tm :: 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 _)
= ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
aspat ([[Text]] -> PTerm -> PTerm
PDisamb [[String -> Text
txt "List"]] PTerm
tm)
catchAmbig (NoValidAlts _)
= ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
aspat ([[Text]] -> PTerm -> PTerm
PDisamb [[String -> Text
txt "List"]] PTerm
tm)
catchAmbig e :: Err
e = Err -> StateT IState (ExceptT Err IO) (Term, Term)
forall a. Err -> Idris a
ierror Err
e