{-# 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 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" pre-type " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
ty' forall a. [a] -> [a] -> [a]
++ 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 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" type pre-addimpl " forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
ty'
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"with methods " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (SyntaxInfo -> [Name]
imp_methods SyntaxInfo
syn)
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (SyntaxInfo -> [Using]
using SyntaxInfo
syn) forall a. [a] -> [a] -> [a]
++ String
"\n" 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) <-
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ 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 (forall n. UExp -> TT n
TType (Int -> UExp
UVal Int
0)) EState
initEState
(forall aux a.
String -> Name -> Maybe Term -> Elab' aux a -> Elab' aux a
errAt String
"type of " Name
n forall a. Maybe a
Nothing
(forall aux a. FC -> Elab' aux a -> Elab' aux (a, aux)
erunAux FC
fc (IState
-> ElabInfo
-> ElabMode
-> FnOpts
-> Name
-> PTerm
-> ElabD 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 forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i { idris_name :: Int
idris_name = Int
newGName }
let tyT :: Term
tyT = forall {n}. TT n -> TT n
patToImp Term
tyT'
Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show PTerm
ty forall a. [a] -> [a] -> [a]
++ String
"\nElaborated: " forall a. [a] -> [a] -> [a]
++ 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
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, (Int, Maybe Name, Term, [Name]))]
ds forall a. Ord a => a -> a -> Bool
> forall (t :: * -> *) a. Foldable t => t a -> Int
length [PDecl]
is)
forall a b. (a -> b) -> a -> b
$ Name -> Idris ()
addTyInferred Name
n
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 (forall a. Show a => a -> String
show Term
tyT)
Int -> String -> Idris ()
logElab Int
10 forall a b. (a -> b) -> a -> b
$ String
"Elaborated to " forall a. [a] -> [a] -> [a]
++ 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)
-> Env
-> Term
-> StateT IState (ExceptT Err IO) (Term, Term)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] Term
tyT
IState
i <- Idris IState
getIState
let ([Bool]
inaccData, [PArg]
impls) = forall a b. [(a, b)] -> ([a], [b])
unzip 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 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
": inaccessible arguments: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Int, Name)]
inacc forall a. [a] -> [a] -> [a]
++
String
" from " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
cty forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
ty
IState -> Idris ()
putIState forall a b. (a -> b) -> a -> b
$ IState
i { idris_implicits :: Ctxt [PArg]
idris_implicits = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n [PArg]
impls (IState -> Ctxt [PArg]
idris_implicits IState
i) }
Int -> String -> Idris ()
logElab Int
3 (String
"Implicit " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [PArg]
impls)
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCImp Name
n)
let refs :: [Name]
refs = 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Accessibility
acc -> 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 (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)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
Constructor forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts) 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 (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)
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) = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig forall a. Maybe a
Nothing TT n
t (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) = 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ns = t
i forall a. a -> [a] -> [a]
: t -> t a -> TT a -> [t]
param_pos (t
i 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 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 = []
elabType :: ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> 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
-> 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' =
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
Context
ctxt <- Idris Context
getContext
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ String
"Rechecked to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
nty
let nty' :: Term
nty' = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
nty
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ String
"Rechecked to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
nty'
IState
i <- Idris IState
getIState
Bool
rep <- Idris Bool
useREPL
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
rep forall a b. (a -> b) -> a -> b
$ do
String -> Int -> PTerm -> Idris ()
addInternalApp (FC -> String
fc_fname FC
fc) (forall a b. (a, b) -> a
fst 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 forall a b. (a -> b) -> a -> b
$ FC
fc) (PTerm -> PTerm -> PTerm
PTyped (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) PTerm
ty')
IBCWrite -> Idris ()
addIBC (String -> Int -> PTerm -> IBCWrite
IBCLineApp (FC -> String
fc_fname FC
fc) (forall a b. (a, b) -> a
fst 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 forall a b. (a -> b) -> a -> b
$ FC
fc) (PTerm -> PTerm -> PTerm
PTyped (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) PTerm
ty'))
let (Term
fam, [Term]
_) = forall n. TT n -> (TT n, [TT n])
unApply (forall {n}. TT n -> TT n
getRetTy Term
nty')
let opts' :: FnOpts
opts' = FnOpts
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, 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' = 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'
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' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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
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)
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field OptInfo [(Int, Name)]
opt_inaccessible 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)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
Implicit forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts') forall a b. (a -> b) -> a -> b
$ do Name -> Idris ()
addCoercion Name
n
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCCoercion Name
n)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
AutoHint forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts') 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 -> forall a. String -> Idris a
ifail String
"Hints must return a data or record type"
Bool
errorReflection <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem LanguageExt
ErrorReflection 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
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
ErrorHandler forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FnOpts
opts) forall a b. (a -> b) -> a -> b
$ do
if Bool
errorReflection
then
if Term -> Bool
tyIsHandler Term
nty'
then do IState
i <- Idris IState
getIState
IState -> Idris ()
putIState forall a b. (a -> b) -> a -> b
$ IState
i { idris_errorhandlers :: [Name]
idris_errorhandlers = IState -> [Name]
idris_errorhandlers IState
i forall a. [a] -> [a] -> [a]
++ [Name
n] }
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCErrorHandler Name
n)
else forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ String
"The type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
nty' forall a. [a] -> [a] -> [a]
++ String
" is invalid for an error handler"
else forall a. String -> Idris a
ifail String
"Error handlers can only be defined when the ErrorReflection language extension is enabled."
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting forall a b. (a -> b) -> a -> b
$ 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 forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Maybe a
Nothing)]
case (forall n. TT n -> (TT n, [TT n])
unApply Term
usety) of
(P NameType
_ Name
ut Term
_, [Term]
_)
| Name
ut 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])
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
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 forall a. Eq a => a -> a -> Bool
== Text
err Bool -> Bool -> Bool
&& Text
m forall a. Eq a => a -> a -> Bool
== Text
maybe Bool -> Bool -> Bool
&& Text
l forall a. Eq a => a -> a -> Bool
== Text
lst Bool -> Bool -> Bool
&& Text
r forall a. Eq a => a -> a -> Bool
== Text
errrep
, [Text]
ns1 forall a. Eq a => a -> a -> Bool
== forall a b. (a -> b) -> [a] -> [b]
map String -> Text
txt [String
"Errors",String
"Reflection",String
"Language"]
, [Text]
ns2 forall a. Eq a => a -> a -> Bool
== forall a b. (a -> b) -> [a] -> [b]
map String -> Text
txt [String
"Maybe", String
"Prelude"]
, [Text]
ns3 forall a. Eq a => a -> a -> Bool
== forall a b. (a -> b) -> [a] -> [b]
map String -> Text
txt [String
"List", String
"Prelude"]
, [Text]
ns4 forall a. Eq a => a -> a -> Bool
== 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 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 :: Set Name
idris_postulates = forall a. Ord a => a -> Set a -> Set a
S.insert Name
n (IState -> Set Name
idris_postulates IState
ist) }) 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 forall a b. (a -> b) -> a -> b
$ 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 (forall a. a -> Maybe a
Just NameOutput
PostulateOutput) forall a. Maybe a
Nothing forall a. Maybe a
Nothing)]
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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall n. TT n -> [(n, TT n)]
getArgTys (Context -> Env -> Term -> Term
normalise (IState -> Context
tt_ctxt IState
ist) [] Term
cty))
IState -> Idris ()
putIState 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 :: Set (Name, Int)
idris_externs = forall a. Ord a => a -> Set a -> Set a
S.insert (Name
n, Int
arity) (IState -> Set (Name, Int)
idris_externs IState
ist) }) 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))
FC -> Name -> Idris ()
solveDeferred FC
fc Name
n