{-|
Module      : Idris.Elab.Type
Description : Code to elaborate types.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE PatternGuards #-}
module Idris.Elab.Type (
    buildType, elabType, elabType'
  , elabPostulate, elabExtern
  ) where

import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Docstrings (Docstring)
import Idris.Elab.Term
import Idris.Elab.Utils
import Idris.Elab.Value
import Idris.Error
import Idris.Options
import Idris.Output (sendHighlighting)

import Prelude hiding (id, (.))

import Control.Category
import Control.Monad
import qualified Data.Set as S

buildType :: ElabInfo
          -> SyntaxInfo
          -> FC
          -> FnOpts
          -> Name
          -> PTerm
          -> Idris (Type, Type, PTerm, [(Int, Name)])
buildType :: ElabInfo
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris (Term, Term, PTerm, [(Int, Name)])
buildType ElabInfo
info SyntaxInfo
syn FC
fc FnOpts
opts Name
n PTerm
ty' = do
         ctxt <- Idris Context
getContext
         i <- getIState

         logElab 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)
         ty' <- addUsingConstraints syn fc ty'
         ty' <- addUsingImpls syn n fc ty'
         let ty = [Name] -> IState -> PTerm -> PTerm
addImpl (SyntaxInfo -> [Name]
imp_methods SyntaxInfo
syn) IState
i PTerm
ty'

         logElab 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
         logElab 5 $ "with methods " ++ show (imp_methods syn)
         logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

         ((ElabResult tyT' defer is ctxt' newDecls highlights newGName, est), log) <-
            tclift $ elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState
                     (errAt "type of " n Nothing
                        (erunAux fc (build i info ETyDecl [] n ty)))

         displayWarnings est
         setContext ctxt'
         processTacticDecls info newDecls
         sendHighlighting highlights
         updateIState $ \IState
i -> IState
i { idris_name = newGName }

         let tyT = Term -> Term
forall {n}. TT n -> TT n
patToImp Term
tyT'

         logElab 3 $ show ty ++ "\nElaborated: " ++ show tyT'

         ds <- checkAddDef True False info fc iderr True defer
         -- if the type is not complete, note that we'll need to infer
         -- things later (for solving metavariables)
         when (length ds > length is) -- more deferred than case blocks
              $ addTyInferred n

         mapM_ (elabCaseBlock info opts) is
         ctxt <- getContext
         logElab 5 "Rechecking"
         logElab 6 (show tyT)
         logElab 10 $ "Elaborated to " ++ showEnvDbg [] tyT
         (cty, ckind)   <- recheckC (constraintNS info) fc id [] tyT

         -- record the implicit and inaccessible arguments
         i <- getIState
         let (inaccData, impls) = unzip $ getUnboundImplicits i cty ty
         let inacc = Int -> Term -> [Bool] -> [(Int, Name)]
inaccessibleImps Int
0 Term
cty [Bool]
inaccData
         logElab 3 $ show n ++ ": inaccessible arguments: " ++ show inacc ++
                     " from " ++ show cty ++ "\n" ++ showTmImpls ty

         putIState $ i { idris_implicits = addDef n impls (idris_implicits i) }
         logElab 3 ("Implicit " ++ show n ++ " " ++ show impls)
         addIBC (IBCImp n)

         -- Add the names referenced to the call graph, and check we're not
         -- referring to anything less visible
         -- In particular, a public/export type can not refer to anything
         -- private, but can refer to any public/export
         let refs = Term -> [Name]
forall n. Eq n => TT n -> [n]
freeNames Term
cty
         nvis <- getFromHideList n
         case nvis of
              Maybe Accessibility
Nothing -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just Accessibility
acc -> (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC -> Name -> Accessibility -> Accessibility -> Name -> Idris ()
checkVisibility FC
fc Name
n (Accessibility -> Accessibility -> Accessibility
forall a. Ord a => a -> a -> a
max Accessibility
Frozen Accessibility
acc) Accessibility
acc) [Name]
refs
         addCalls n refs
         addIBC (IBCCG n)

         when (Constructor `notElem` opts) $ do
             let pnames = IState -> [Name] -> [PArg] -> Term -> [Name]
getParamsInType IState
i [] [PArg]
impls Term
cty
             let fninfo = [Int] -> FnInfo
FnInfo (Int -> [Name] -> Term -> [Int]
forall {t :: * -> *} {a} {t}.
(Foldable t, Eq a, Num t) =>
t -> t a -> TT a -> [t]
param_pos Int
0 [Name]
pnames Term
cty)
             setFnInfo n fninfo
             addIBC (IBCFnInfo n fninfo)

         return (cty, ckind, ty, inacc)
  where
    patToImp :: TT n -> TT n
patToImp (Bind n
n (PVar RigCount
rig TT n
t) TT n
sc) = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> Maybe ImplicitInfo -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
forall a. Maybe a
Nothing TT n
t (UExp -> TT n
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] Int
0))) (TT n -> TT n
patToImp TT n
sc)
    patToImp (Bind n
n Binder (TT n)
b TT n
sc) = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n Binder (TT n)
b (TT n -> TT n
patToImp TT n
sc)
    patToImp TT n
t = TT n
t

    param_pos :: t -> t a -> TT a -> [t]
param_pos t
i t a
ns (Bind a
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT a
t TT a
_) TT a
sc)
        | a
n a -> t a -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ns = t
i t -> [t] -> [t]
forall a. a -> [a] -> [a]
: t -> t a -> TT a -> [t]
param_pos (t
i t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) t a
ns TT a
sc
        | Bool
otherwise = t -> t a -> TT a -> [t]
param_pos (t
i t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) t a
ns TT a
sc
    param_pos t
i t a
ns TT a
t = []

-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
elabType :: ElabInfo
         -> SyntaxInfo
         -> Docstring (Either Err PTerm)
         -> [(Name, Docstring (Either Err PTerm))]
         -> FC
         -> FnOpts
         -> Name
         -> FC -- ^ The precise location of the name
         -> PTerm
         -> Idris Type
elabType :: ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Term
elabType = Bool
-> ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Term
elabType' Bool
False

elabType' :: Bool  -- normalise it
          -> ElabInfo
          -> SyntaxInfo
          -> Docstring (Either Err PTerm)
          -> [(Name, Docstring (Either Err PTerm))]
          -> FC
          -> FnOpts
          -> Name
          -> FC
          -> PTerm
          -> Idris Type
elabType' :: Bool
-> ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Term
elabType' Bool
norm ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs FC
fc FnOpts
opts Name
n FC
nfc PTerm
ty' = {- let ty' = piBind (params info) ty_in
                                                       n  = liftname info n_in in    -}
      do FC -> Name -> Idris ()
checkUndefined FC
fc Name
n
         (cty, _, ty, inacc) <- ElabInfo
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris (Term, Term, PTerm, [(Int, Name)])
buildType ElabInfo
info SyntaxInfo
syn FC
fc FnOpts
opts Name
n PTerm
ty'

         addStatics n cty ty
         let nty = Term
cty -- normalise ctxt [] cty
         -- if the return type is something coinductive, freeze the definition
         ctxt <- getContext
         logElab 2 $ "Rechecked to " ++ show nty
         let nty' = Context -> [(Name, RigCount, Binder Term)] -> Term -> Term
normalise Context
ctxt [] Term
nty
         logElab 2 $ "Rechecked to " ++ show nty'

         -- Add function name to internals (used for making :addclause know
         -- the name unambiguously)
         i <- getIState
         rep <- useREPL
         when rep $ do
           addInternalApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty') -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
         addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))

         let (fam, _) = unApply (getRetTy nty')
         -- Productivity checking now via checking for guarded 'Delay'
         let opts' = FnOpts
opts -- if corec then (Coinductive : opts) else opts
         let usety = if Bool
norm then Term
nty' else Term
nty
         ds <- checkDef info fc iderr True [(n, (-1, Nothing, usety, []))]
         addIBC (IBCDef n)
         addDefinedName n
         let ds' = ((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
fam, [Name]
ns)) -> (Name
n, (Int
i, Maybe Name
top, Term
fam, [Name]
ns, Bool
True, Bool
True))) [(Name, (Int, Maybe Name, Term, [Name]))]
ds
         addDeferred ds'
         setFlags n opts'
         checkDocs fc argDocs ty
         doc' <- elabDocTerms info doc
         argDocs' <- mapM (\(Name
n, Docstring (Either Err PTerm)
d) -> do d' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
d
                                         return (n, d')) argDocs
         addDocStr n doc' argDocs'
         addIBC (IBCDoc n)
         addIBC (IBCFlags n)
         fputState (opt_inaccessible . ist_optimisation n) inacc
         addIBC (IBCOpt n)
         when (Implicit `elem` opts') $ do addCoercion n
                                           addIBC (IBCCoercion n)
         when (AutoHint `elem` opts') $
             case fam of
                P NameType
_ Name
tyn Term
_ -> do Name -> Name -> Idris ()
addAutoHint Name
tyn Name
n
                                IBCWrite -> Idris ()
addIBC (Name -> Name -> IBCWrite
IBCAutoHint Name
tyn Name
n)
                Term
t -> String -> Idris ()
forall a. String -> Idris a
ifail String
"Hints must return a data or record type"

         -- If the function is declared as an error handler and the language
         -- extension is enabled, then add it to the list of error handlers.
         errorReflection <- fmap (elem ErrorReflection . idris_language_extensions) getIState
         when (ErrorHandler `elem` opts) $ do
           if errorReflection
             then
               -- Check that the declared type is the correct type for an error handler:
               -- handler : List (TTName, TT) -> Err -> ErrorReport - for now no ctxt
               if tyIsHandler nty'
                 then do i <- getIState
                         putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ [n] }
                         addIBC (IBCErrorHandler n)
                 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"
             else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."
         -- Send highlighting information about the name being declared
         sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)]
         -- if it's an export list type, make a note of it
         case (unApply usety) of
              (P NameType
_ Name
ut Term
_, [Term]
_)
                 | Name
ut Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
ffiexport -> do IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCExport Name
n)
                                         Name -> Idris ()
addExport Name
n
              (Term, [Term])
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         return usety
  where
    ffiexport :: Name
ffiexport = Name -> [String] -> Name
sNS (String -> Name
sUN String
"FFI_Export") [String
"FFI_Export"]

    err :: Text
err = String -> Text
txt String
"Err"
    maybe :: Text
maybe = String -> Text
txt String
"Maybe"
    lst :: Text
lst = String -> Text
txt String
"List"
    errrep :: Text
errrep = String -> Text
txt String
"ErrorReportPart"

    tyIsHandler :: Term -> Bool
tyIsHandler (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ (P NameType
_ (NS (UN Text
e) [Text]
ns1) Term
_) Term
_)
                        (App AppStatus Name
_ (P NameType
_ (NS (UN Text
m) [Text]
ns2) Term
_)
                             (App AppStatus Name
_ (P NameType
_ (NS (UN Text
l) [Text]
ns3) Term
_)
                                  (P NameType
_ (NS (UN Text
r) [Text]
ns4) Term
_))))
        | Text
e Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
err Bool -> Bool -> Bool
&& Text
m Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
maybe Bool -> Bool -> Bool
&& Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
lst Bool -> Bool -> Bool
&& Text
r Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
errrep
        , [Text]
ns1 [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== (String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
txt [String
"Errors",String
"Reflection",String
"Language"]
        , [Text]
ns2 [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== (String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
txt [String
"Maybe", String
"Prelude"]
        , [Text]
ns3 [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== (String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
txt [String
"List", String
"Prelude"]
        , [Text]
ns4 [Text] -> [Text] -> Bool
forall a. Eq a => a -> a -> Bool
== (String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
txt [String
"Reflection",String
"Language"] = Bool
True
    tyIsHandler Term
_                                           = Bool
False

elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->
                 FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()
elabPostulate :: ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> FC
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris ()
elabPostulate ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc FC
fc FC
nfc FnOpts
opts Name
n PTerm
ty = do
    ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Term
elabType ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc [] FC
fc FnOpts
opts Name
n FC
NoFC PTerm
ty
    IState -> Idris ()
putIState (IState -> Idris ()) -> (IState -> IState) -> IState -> Idris ()
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
. (\IState
ist -> IState
ist{ idris_postulates = S.insert n (idris_postulates ist) }) (IState -> Idris ()) -> Idris IState -> Idris ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Idris IState
getIState
    IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCPostulate Name
n)
    Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting (Set (FC', OutputAnnotation) -> Idris ())
-> Set (FC', OutputAnnotation) -> Idris ()
forall a b. (a -> b) -> a -> b
$ [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a. Ord a => [a] -> Set a
S.fromList [(FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n (NameOutput -> Maybe NameOutput
forall a. a -> Maybe a
Just NameOutput
PostulateOutput) Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)]

    -- remove it from the deferred definitions list
    FC -> Name -> Idris ()
solveDeferred FC
fc Name
n

elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->
                 FC -> FC -> FnOpts -> Name -> PTerm -> Idris ()
elabExtern :: ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> FC
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris ()
elabExtern ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc FC
fc FC
nfc FnOpts
opts Name
n PTerm
ty = do
    cty <- ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Term
elabType ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc [] FC
fc FnOpts
opts Name
n FC
NoFC PTerm
ty
    ist <- getIState
    let arity = [(Name, Term)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getArgTys (Context -> [(Name, RigCount, Binder Term)] -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
ist) [] Term
cty))

    putIState . (\IState
ist -> IState
ist{ idris_externs = S.insert (n, arity) (idris_externs ist) }) =<< getIState
    addIBC (IBCExtern (n, arity))

    -- remove it from the deferred definitions list
    solveDeferred fc n