{-|
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
         Context
ctxt <- Idris Context
getContext
         IState
i <- Idris IState
getIState

         Int -> String -> Idris ()
logElab Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" pre-type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
ty' String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (SyntaxInfo -> [Name]
no_imp SyntaxInfo
syn)
         PTerm
ty' <- SyntaxInfo -> FC -> PTerm -> Idris PTerm
addUsingConstraints SyntaxInfo
syn FC
fc PTerm
ty'
         PTerm
ty' <- SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
addUsingImpls SyntaxInfo
syn Name
n FC
fc PTerm
ty'
         let ty :: PTerm
ty = [Name] -> IState -> PTerm -> PTerm
addImpl (SyntaxInfo -> [Name]
imp_methods SyntaxInfo
syn) IState
i PTerm
ty'

         Int -> String -> Idris ()
logElab Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" type pre-addimpl " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
ty'
         Int -> String -> Idris ()
logElab Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"with methods " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show (SyntaxInfo -> [Name]
imp_methods SyntaxInfo
syn)
         Int -> String -> Idris ()
logElab Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Using] -> String
forall a. Show a => a -> String
show (SyntaxInfo -> [Using]
using SyntaxInfo
syn) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
ty

         ((ElabResult Term
tyT' [(Name, (Int, Maybe Name, Term, [Name]))]
defer [PDecl]
is Context
ctxt' [RDeclInstructions]
newDecls Set (FC', OutputAnnotation)
highlights Int
newGName, EState
est), String
log) <-
            TC ((ElabResult, EState), String)
-> Idris ((ElabResult, EState), String)
forall a. TC a -> Idris a
tclift (TC ((ElabResult, EState), String)
 -> Idris ((ElabResult, EState), String))
-> TC ((ElabResult, EState), String)
-> Idris ((ElabResult, EState), String)
forall a b. (a -> b) -> a -> b
$ String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> Term
-> EState
-> Elab' EState (ElabResult, EState)
-> TC ((ElabResult, EState), 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) Name
n (UExp -> Term
forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0)) EState
initEState
                     (String
-> Name
-> Maybe Term
-> Elab' EState (ElabResult, EState)
-> Elab' EState (ElabResult, EState)
forall aux a.
String -> Name -> Maybe Term -> Elab' aux a -> Elab' aux a
errAt String
"type of " Name
n Maybe Term
forall a. Maybe a
Nothing
                        (FC -> Elab' EState ElabResult -> Elab' EState (ElabResult, EState)
forall aux a. FC -> Elab' aux a -> Elab' aux (a, aux)
erunAux FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> Elab' EState ElabResult
build IState
i ElabInfo
info ElabMode
ETyDecl [] Name
n PTerm
ty)))

         EState -> Idris ()
displayWarnings EState
est
         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
$ \IState
i -> IState
i { idris_name = newGName }

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

         Int -> String -> Idris ()
logElab Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ PTerm -> String
forall a. Show a => a -> String
show PTerm
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nElaborated: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tyT'

         [(Name, (Int, Maybe Name, Term, [Name]))]
ds <- Bool
-> Bool
-> ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Term, [Name]))]
checkAddDef Bool
True Bool
False ElabInfo
info FC
fc Name -> Err -> Err
iderr Bool
True [(Name, (Int, Maybe Name, Term, [Name]))]
defer
         -- if the type is not complete, note that we'll need to infer
         -- things later (for solving metavariables)
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(Name, (Int, Maybe Name, Term, [Name]))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, (Int, Maybe Name, Term, [Name]))]
ds Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [PDecl] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PDecl]
is) -- more deferred than case blocks
              (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Name -> Idris ()
addTyInferred Name
n

         (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 FnOpts
opts) [PDecl]
is
         Context
ctxt <- Idris Context
getContext
         Int -> String -> Idris ()
logElab Int
5 String
"Rechecking"
         Int -> String -> Idris ()
logElab Int
6 (Term -> String
forall a. Show a => a -> String
show Term
tyT)
         Int -> String -> Idris ()
logElab Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborated to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, RigCount, Binder Term)] -> Term -> String
forall {a}.
(Show a, Eq a) =>
[(a, RigCount, Binder (TT a))] -> TT a -> String
showEnvDbg [] Term
tyT
         (Term
cty, Term
ckind)   <- String
-> FC
-> (Err -> Err)
-> [(Name, RigCount, Binder Term)]
-> Term
-> StateT IState (ExceptT Err IO) (Term, Term)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc Err -> Err
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Term
tyT

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

         IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_implicits = addDef n impls (idris_implicits i) }
         Int -> String -> Idris ()
logElab Int
3 (String
"Implicit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [PArg] -> String
forall a. Show a => a -> String
show [PArg]
impls)
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCImp Name
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 :: [Name]
refs = Term -> [Name]
forall n. Eq n => TT n -> [n]
freeNames Term
cty
         Maybe Accessibility
nvis <- Name -> Idris (Maybe Accessibility)
getFromHideList Name
n
         case Maybe Accessibility
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
         Name -> [Name] -> Idris ()
addCalls Name
n [Name]
refs
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCCG Name
n)

         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
Constructor FnOpt -> FnOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
             let pnames :: [Name]
pnames = IState -> [Name] -> [PArg] -> Term -> [Name]
getParamsInType IState
i [] [PArg]
impls Term
cty
             let fninfo :: FnInfo
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)
             Name -> FnInfo -> Idris ()
setFnInfo Name
n FnInfo
fninfo
             IBCWrite -> Idris ()
addIBC (Name -> FnInfo -> IBCWrite
IBCFnInfo Name
n FnInfo
fninfo)

         (Term, Term, PTerm, [(Int, Name)])
-> Idris (Term, Term, PTerm, [(Int, Name)])
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
cty, Term
ckind, PTerm
ty, [(Int, Name)]
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
         (Term
cty, Term
_, PTerm
ty, [(Int, Name)]
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'

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

         -- Add function name to internals (used for making :addclause know
         -- the name unambiguously)
         IState
i <- Idris IState
getIState
         Bool
rep <- Idris Bool
useREPL
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
rep (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
           String -> Int -> PTerm -> Idris ()
addInternalApp (FC -> String
fc_fname FC
fc) ((Int, Int) -> Int
forall a b. (a, b) -> a
fst ((Int, Int) -> Int) -> (FC -> (Int, Int)) -> FC -> Int
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
. FC -> (Int, Int)
fc_start (FC -> Int) -> FC -> Int
forall a b. (a -> b) -> a -> b
$ FC
fc) (PTerm -> PTerm -> PTerm
PTyped (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) PTerm
ty') -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?
         IBCWrite -> Idris ()
addIBC (String -> Int -> PTerm -> IBCWrite
IBCLineApp (FC -> String
fc_fname FC
fc) ((Int, Int) -> Int
forall a b. (a, b) -> a
fst ((Int, Int) -> Int) -> (FC -> (Int, Int)) -> FC -> Int
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
. FC -> (Int, Int)
fc_start (FC -> Int) -> FC -> Int
forall a b. (a -> b) -> a -> b
$ FC
fc) (PTerm -> PTerm -> PTerm
PTyped (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) PTerm
ty')) -- (mergeTy ty' (delab i nty')))

         let (Term
fam, [Term]
_) = Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply (Term -> Term
forall {n}. TT n -> TT n
getRetTy Term
nty')
         -- Productivity checking now via checking for guarded 'Delay'
         let opts' :: FnOpts
opts' = FnOpts
opts -- if corec then (Coinductive : opts) else opts
         let usety :: Term
usety = if Bool
norm then Term
nty' else Term
nty
         [(Name, (Int, Maybe Name, Term, [Name]))]
ds <- ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Term, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Term, [Name]))]
checkDef ElabInfo
info FC
fc Name -> Err -> Err
iderr Bool
True [(Name
n, (-Int
1, Maybe Name
forall a. Maybe a
Nothing, Term
usety, []))]
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
         Name -> Idris ()
addDefinedName Name
n
         let ds' :: [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
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
         [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name, (Int, Maybe Name, Term, [Name], Bool, Bool))]
ds'
         Name -> FnOpts -> Idris ()
setFlags Name
n FnOpts
opts'
         FC -> [(Name, Docstring (Either Err PTerm))] -> PTerm -> Idris ()
forall a. FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
checkDocs FC
fc [(Name, Docstring (Either Err PTerm))]
argDocs PTerm
ty
         Docstring DocTerm
doc' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
doc
         [(Name, Docstring DocTerm)]
argDocs' <- ((Name, Docstring (Either Err PTerm))
 -> StateT IState (ExceptT Err IO) (Name, Docstring DocTerm))
-> [(Name, Docstring (Either Err PTerm))]
-> StateT IState (ExceptT Err IO) [(Name, Docstring DocTerm)]
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) -> [a] -> m [b]
mapM (\(Name
n, Docstring (Either Err PTerm)
d) -> do Docstring DocTerm
d' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
d
                                         (Name, Docstring DocTerm)
-> StateT IState (ExceptT Err IO) (Name, Docstring DocTerm)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, Docstring DocTerm
d')) [(Name, Docstring (Either Err PTerm))]
argDocs
         Name
-> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
addDocStr Name
n Docstring DocTerm
doc' [(Name, Docstring DocTerm)]
argDocs'
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDoc Name
n)
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCFlags Name
n)
         Field IState [(Int, Name)] -> [(Int, Name)] -> Idris ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field OptInfo [(Int, Name)]
opt_inaccessible Field OptInfo [(Int, Name)]
-> Field IState OptInfo -> Field IState [(Int, Name)]
forall b c a. Field b c -> Field a b -> Field a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
n) [(Int, Name)]
inacc
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
n)
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
Implicit FnOpt -> FnOpts -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts') (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do Name -> Idris ()
addCoercion Name
n
                                           IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCCoercion Name
n)
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
AutoHint FnOpt -> FnOpts -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts') (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
             case Term
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.
         Bool
errorReflection <- (IState -> Bool) -> Idris IState -> Idris Bool
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 (LanguageExt -> [LanguageExt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem LanguageExt
ErrorReflection ([LanguageExt] -> Bool)
-> (IState -> [LanguageExt]) -> IState -> Bool
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 -> [LanguageExt]
idris_language_extensions) Idris IState
getIState
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
ErrorHandler FnOpt -> FnOpts -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ do
           if Bool
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 Term -> Bool
tyIsHandler Term
nty'
                 then do IState
i <- Idris IState
getIState
                         IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_errorhandlers = idris_errorhandlers i ++ [n] }
                         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCErrorHandler Name
n)
                 else String -> Idris ()
forall a. String -> Idris a
ifail (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"The type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
nty' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is invalid for an error handler"
             else String -> Idris ()
forall a. String -> Idris a
ifail String
"Error handlers can only be defined when the ErrorReflection language extension is enabled."
         -- Send highlighting information about the name being declared
         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 Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)]
         -- if it's an export list type, make a note of it
         case (Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
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 ()
         Term -> Idris Term
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
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
    Term
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
    IState
ist <- Idris IState
getIState
    let arity :: Int
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))

    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_externs = S.insert (n, arity) (idris_externs 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, Int) -> IBCWrite
IBCExtern (Name
n, Int
arity))

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