{-# LANGUAGE PatternGuards #-}
module IRTS.Exports(findExports, getExpNames) where
import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Error
import IRTS.Lang
import Data.Maybe
findExports :: Idris [ExportIFace]
findExports :: Idris [ExportIFace]
findExports = do [Name]
exps <- Idris [Name]
getExports
[ExportIFace]
es <- (Name -> StateT IState (ExceptT Err IO) ExportIFace)
-> [Name] -> Idris [ExportIFace]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> StateT IState (ExceptT Err IO) ExportIFace
toIFace [Name]
exps
Int -> String -> Idris ()
logCodeGen 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Exporting " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ExportIFace] -> String
forall a. Show a => a -> String
show [ExportIFace]
es
[ExportIFace] -> Idris [ExportIFace]
forall (m :: * -> *) a. Monad m => a -> m a
return [ExportIFace]
es
getExpNames :: [ExportIFace] -> [Name]
getExpNames :: [ExportIFace] -> [Name]
getExpNames = (ExportIFace -> [Name]) -> [ExportIFace] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExportIFace -> [Name]
expNames
expNames :: ExportIFace -> [Name]
expNames :: ExportIFace -> [Name]
expNames (Export _ _ es :: [Export]
es) = (Export -> Maybe Name) -> [Export] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Export -> Maybe Name
fnames [Export]
es
where fnames :: Export -> Maybe Name
fnames (ExportData _) = Maybe Name
forall a. Maybe a
Nothing
fnames (ExportFun n :: Name
n _ _ _) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
toIFace :: Name -> Idris ExportIFace
toIFace :: Name -> StateT IState (ExceptT Err IO) ExportIFace
toIFace n :: Name
n = do IState
i <- Idris IState
getIState
let ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
i
Term
def <- case Name -> Context -> Maybe Def
lookupDefExact Name
n Context
ctxt of
Just (CaseOp _ _ _ _ _ cs :: CaseDefs
cs)
-> SC' Term -> StateT IState (ExceptT Err IO) Term
forall a. SC' a -> StateT IState (ExceptT Err IO) a
getExpList (([Name], SC' Term) -> SC' Term
forall a b. (a, b) -> b
snd (CaseDefs -> ([Name], SC' Term)
cases_compiletime CaseDefs
cs))
Nothing -> String -> StateT IState (ExceptT Err IO) Term
forall a. String -> Idris a
ifail "Can't happen [toIFace]"
case Name -> Context -> Maybe Term
lookupTyExact Name
n Context
ctxt of
Just ty :: Term
ty -> Term -> Term -> StateT IState (ExceptT Err IO) ExportIFace
toIFaceTyVal Term
ty Term
def
Nothing -> String -> StateT IState (ExceptT Err IO) ExportIFace
forall a. String -> Idris a
ifail "Can't happen [toIFace]"
where
getExpList :: SC' a -> StateT IState (ExceptT Err IO) a
getExpList (STerm t :: a
t) = a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
t
getExpList _ = String -> StateT IState (ExceptT Err IO) a
forall a. String -> Idris a
ifail "Badly formed export list"
toIFaceTyVal :: Type -> Term -> Idris ExportIFace
toIFaceTyVal :: Term -> Term -> StateT IState (ExceptT Err IO) ExportIFace
toIFaceTyVal ty :: Term
ty tm :: Term
tm
| (P _ exp :: Name
exp _, [P _ ffi :: Name
ffi _, Constant (Str hdr :: String
hdr), _]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
ty
= do [Export]
tm' <- Term -> Idris [Export]
toIFaceVal Term
tm
ExportIFace -> StateT IState (ExceptT Err IO) ExportIFace
forall (m :: * -> *) a. Monad m => a -> m a
return (ExportIFace -> StateT IState (ExceptT Err IO) ExportIFace)
-> ExportIFace -> StateT IState (ExceptT Err IO) ExportIFace
forall a b. (a -> b) -> a -> b
$ Name -> String -> [Export] -> ExportIFace
Export Name
ffi String
hdr [Export]
tm'
toIFaceVal :: Term -> Idris [Export]
toIFaceVal :: Term -> Idris [Export]
toIFaceVal tm :: Term
tm
| (P _ end :: Name
end _, _) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name
end Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN "End") ["FFI_Export"] = [Export] -> Idris [Export]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| (P _ fun :: Name
fun _, [_,_,_,_,(P _ fn :: Name
fn _),extnm :: Term
extnm,prf :: Term
prf,rest :: Term
rest]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name
fun Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN "Fun") ["FFI_Export"]
= do [Export]
rest' <- Term -> Idris [Export]
toIFaceVal Term
rest
[Export] -> Idris [Export]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Export] -> Idris [Export]) -> [Export] -> Idris [Export]
forall a b. (a -> b) -> a -> b
$
Name -> FDesc -> FDesc -> [FDesc] -> Export
ExportFun Name
fn (Term -> FDesc
toFDesc Term
extnm) (Term -> FDesc
toFDescRet Term
prf) (Term -> [FDesc]
toFDescArgs Term
prf)
Export -> [Export] -> [Export]
forall a. a -> [a] -> [a]
: [Export]
rest'
| (P _ dat :: Name
dat _, [_,_,_,_,d :: Term
d,rest :: Term
rest]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name
dat Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN "Data") ["FFI_Export"]
= do [Export]
rest' <- Term -> Idris [Export]
toIFaceVal Term
rest
[Export] -> Idris [Export]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Export] -> Idris [Export]) -> [Export] -> Idris [Export]
forall a b. (a -> b) -> a -> b
$ FDesc -> Export
ExportData (Term -> FDesc
toFDesc Term
d) Export -> [Export] -> [Export]
forall a. a -> [a] -> [a]
: [Export]
rest'
| Bool
otherwise = String -> Idris [Export]
forall a. String -> Idris a
ifail (String -> Idris [Export]) -> String -> Idris [Export]
forall a b. (a -> b) -> a -> b
$ "Badly formed export list " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm
toFDesc :: Term -> FDesc
toFDesc :: Term -> FDesc
toFDesc (Constant (Str str :: String
str)) = String -> FDesc
FStr String
str
toFDesc tm :: Term
tm
| (P _ n :: Name
n _, []) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> FDesc
FCon (Name -> Name
deNS Name
n)
| (P _ n :: Name
n _, as :: [Term]
as) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> [FDesc] -> FDesc
FApp (Name -> Name
deNS Name
n) ((Term -> FDesc) -> [Term] -> [FDesc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> FDesc
toFDesc [Term]
as)
toFDesc _ = FDesc
FUnknown
toFDescRet :: Term -> FDesc
toFDescRet :: Term -> FDesc
toFDescRet tm :: Term
tm
| (P _ ret :: Name
ret _, [_,_,_,b :: Term
b]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name
ret Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN "FFI_Ret") ["FFI_Export"]
= Term -> FDesc
toFDescBase Term
b
| (P _ io :: Name
io _, [_,_,_,b :: Term
b]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name
io Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN "FFI_IO") ["FFI_Export"]
= FDesc -> FDesc
FIO (FDesc -> FDesc) -> FDesc -> FDesc
forall a b. (a -> b) -> a -> b
$ Term -> FDesc
toFDescBase Term
b
| (P _ fun :: Name
fun _, [_,_,_,_,_,t :: Term
t]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name
fun Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN "FFI_Fun") ["FFI_Export"]
= Term -> FDesc
toFDescRet Term
t
| Bool
otherwise = String -> FDesc
forall a. HasCallStack => String -> a
error "Badly formed export proof"
toFDescBase :: Term -> FDesc
toFDescBase :: Term -> FDesc
toFDescBase tm :: Term
tm
| (P _ prim :: Name
prim _, [_, _, _, pdesc :: Term
pdesc]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name
prim Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN "FFI_Prim") ["FFI_Export"]
= Term -> FDesc
toFDescPrim Term
pdesc
| (P _ prim :: Name
prim _, [_, _, _, ddesc :: Term
ddesc, _]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name
prim Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN "FFI_ExpType") ["FFI_Export"]
= Term -> FDesc
toFDescPrim Term
ddesc
| Bool
otherwise = String -> FDesc
forall a. HasCallStack => String -> a
error "Badly formed export type"
toFDescArgs :: Term -> [FDesc]
toFDescArgs :: Term -> [FDesc]
toFDescArgs tm :: Term
tm
| (P _ fun :: Name
fun _, [_,_,_,_,b :: Term
b,t :: Term
t]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm,
Name
fun Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> [String] -> Name
sNS (String -> Name
sUN "FFI_Fun") ["FFI_Export"]
= Term -> FDesc
toFDescBase Term
b FDesc -> [FDesc] -> [FDesc]
forall a. a -> [a] -> [a]
: Term -> [FDesc]
toFDescArgs Term
t
| Bool
otherwise = []
toFDescPrim :: Term -> FDesc
toFDescPrim (Constant (Str str :: String
str)) = String -> FDesc
FStr String
str
toFDescPrim tm :: Term
tm
| (P _ n :: Name
n _, []) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> FDesc
FCon (Name -> Name
deNS Name
n)
| (P _ n :: Name
n _, as :: [Term]
as) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> [FDesc] -> FDesc
FApp (Name -> Name
deNS Name
n) ((Term -> FDesc) -> [Term] -> [FDesc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> FDesc
toFDescPrim [Term]
as)
toFDescPrim _ = FDesc
FUnknown
deNS :: Name -> Name
deNS (NS n :: Name
n _) = Name
n
deNS n :: Name
n = Name
n