{-|
Module      : IRTS.Exports
Description : Deal with external things.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name -> StateT IState (ExceptT Err IO) ExportIFace
toIFace [Name]
exps
                 Int -> String -> Idris ()
logCodeGen Int
2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Exporting " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ExportIFace] -> String
forall a. Show a => a -> String
show [ExportIFace]
es
                 [ExportIFace] -> Idris [ExportIFace]
forall a. a -> StateT IState (ExceptT Err IO) a
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 Name
_ String
_ [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 FDesc
_) = Maybe Name
forall a. Maybe a
Nothing
        fnames (ExportFun Name
n FDesc
_ FDesc
_ [FDesc]
_) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n

toIFace :: Name -> Idris ExportIFace
toIFace :: Name -> StateT IState (ExceptT Err IO) ExportIFace
toIFace 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 CaseInfo
_ Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
_ 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))
                           Maybe Def
Nothing -> String -> StateT IState (ExceptT Err IO) Term
forall a. String -> Idris a
ifail String
"Can't happen [toIFace]"
               case Name -> Context -> Maybe Term
lookupTyExact Name
n Context
ctxt of
                    Just Term
ty -> Term -> Term -> StateT IState (ExceptT Err IO) ExportIFace
toIFaceTyVal Term
ty Term
def
                    Maybe Term
Nothing -> String -> StateT IState (ExceptT Err IO) ExportIFace
forall a. String -> Idris a
ifail String
"Can't happen [toIFace]"
  where
    getExpList :: SC' a -> StateT IState (ExceptT Err IO) a
getExpList (STerm a
t) = a -> StateT IState (ExceptT Err IO) a
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
t
    getExpList SC' a
_ = String -> StateT IState (ExceptT Err IO) a
forall a. String -> Idris a
ifail String
"Badly formed export list"

toIFaceTyVal :: Type -> Term -> Idris ExportIFace
toIFaceTyVal :: Term -> Term -> StateT IState (ExceptT Err IO) ExportIFace
toIFaceTyVal Term
ty Term
tm
   | (P NameType
_ Name
exp Term
_, [P NameType
_ Name
ffi Term
_, Constant (Str String
hdr), Term
_]) <- 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 a. a -> StateT IState (ExceptT Err IO) a
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 Term
tm
   | (P NameType
_ Name
end Term
_, [Term]
_) <- 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 String
"End") [String
"FFI_Export"] = [Export] -> Idris [Export]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
   | (P NameType
_ Name
fun Term
_, [Term
_,Term
_,Term
_,Term
_,(P NameType
_ Name
fn Term
_),Term
extnm,Term
prf,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 String
"Fun") [String
"FFI_Export"]
       = do [Export]
rest' <- Term -> Idris [Export]
toIFaceVal Term
rest
            [Export] -> Idris [Export]
forall a. a -> StateT IState (ExceptT Err IO) a
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 NameType
_ Name
dat Term
_, [Term
_,Term
_,Term
_,Term
_,Term
d,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 String
"Data") [String
"FFI_Export"]
       = do [Export]
rest' <- Term -> Idris [Export]
toIFaceVal Term
rest
            [Export] -> Idris [Export]
forall a. a -> StateT IState (ExceptT Err IO) a
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
$ String
"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 String
str)) = String -> FDesc
FStr String
str
toFDesc Term
tm
   | (P NameType
_ Name
n Term
_, []) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> FDesc
FCon (Name -> Name
deNS Name
n)
   | (P NameType
_ Name
n Term
_, [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 Term
_ = FDesc
FUnknown

toFDescRet :: Term -> FDesc
toFDescRet :: Term -> FDesc
toFDescRet Term
tm
   | (P NameType
_ Name
ret Term
_, [Term
_,Term
_,Term
_,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 String
"FFI_Ret") [String
"FFI_Export"]
       = Term -> FDesc
toFDescBase Term
b
   | (P NameType
_ Name
io Term
_, [Term
_,Term
_,Term
_,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 String
"FFI_IO") [String
"FFI_Export"]
       = FDesc -> FDesc
FIO (FDesc -> FDesc) -> FDesc -> FDesc
forall a b. (a -> b) -> a -> b
$ Term -> FDesc
toFDescBase Term
b
   | (P NameType
_ Name
fun Term
_, [Term
_,Term
_,Term
_,Term
_,Term
_,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 String
"FFI_Fun") [String
"FFI_Export"]
       = Term -> FDesc
toFDescRet Term
t
   | Bool
otherwise = String -> FDesc
forall a. HasCallStack => String -> a
error String
"Badly formed export proof"

toFDescBase :: Term -> FDesc
toFDescBase :: Term -> FDesc
toFDescBase Term
tm
   | (P NameType
_ Name
prim Term
_, [Term
_, Term
_, Term
_, 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 String
"FFI_Prim") [String
"FFI_Export"]
       = Term -> FDesc
toFDescPrim Term
pdesc
   | (P NameType
_ Name
prim Term
_, [Term
_, Term
_, Term
_, Term
ddesc, Term
_]) <- 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 String
"FFI_ExpType") [String
"FFI_Export"]
       = Term -> FDesc
toFDescPrim Term
ddesc
   | Bool
otherwise = String -> FDesc
forall a. HasCallStack => String -> a
error String
"Badly formed export type"

toFDescArgs :: Term -> [FDesc]
toFDescArgs :: Term -> [FDesc]
toFDescArgs Term
tm
   | (P NameType
_ Name
fun Term
_, [Term
_,Term
_,Term
_,Term
_,Term
b,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 String
"FFI_Fun") [String
"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 String
str)) = String -> FDesc
FStr String
str
toFDescPrim Term
tm
   | (P NameType
_ Name
n Term
_, []) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> FDesc
FCon (Name -> Name
deNS Name
n)
   | (P NameType
_ Name
n Term
_, [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 Term
_ = FDesc
FUnknown

deNS :: Name -> Name
deNS (NS Name
n [Text]
_) = Name
n
deNS Name
n = Name
n