content: {-|
  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 = do exps <- getExports
                   es <- mapM toIFace exps
                   logCodeGen 2 $ "Exporting " ++ show es
                   return es
  
  getExpNames :: [ExportIFace] -> [Name]
  getExpNames = concatMap expNames
  
  expNames :: ExportIFace -> [Name]
  expNames (Export _ _ es) = mapMaybe fnames es
    where fnames (ExportData _) = Nothing
          fnames (ExportFun n _ _ _) = Just n
  
  toIFace :: Name -> Idris ExportIFace
  toIFace n = do i <- getIState
                 let ctxt = tt_ctxt i
                 def <- case lookupDefExact n ctxt of
                             Just (CaseOp _ _ _ _ _ cs)
                                -> getExpList (snd (cases_compiletime cs))
                             Nothing -> ifail "Can't happen [toIFace]"
                 case lookupTyExact n ctxt of
                      Just ty -> toIFaceTyVal ty def
                      Nothing -> ifail "Can't happen [toIFace]"
    where
      getExpList (STerm t) = return t
      getExpList _ = ifail "Badly formed export list"
  
  toIFaceTyVal :: Type -> Term -> Idris ExportIFace
  toIFaceTyVal ty tm
     | (P _ exp _, [P _ ffi _, Constant (Str hdr), _]) <- unApply ty
           = do tm' <- toIFaceVal tm
                return $ Export ffi hdr tm'
  
  toIFaceVal :: Term -> Idris [Export]
  toIFaceVal tm
     | (P _ end _, _) <- unApply tm,
       end == sNS (sUN "End") ["FFI_Export"] = return []
     | (P _ fun _, [_,_,_,_,(P _ fn _),extnm,prf,rest]) <- unApply tm,
       fun == sNS (sUN "Fun") ["FFI_Export"]
         = do rest' <- toIFaceVal rest
              return $
                ExportFun fn (toFDesc extnm) (toFDescRet prf) (toFDescArgs prf)
                    : rest'
     | (P _ dat _, [_,_,_,_,d,rest]) <- unApply tm,
       dat == sNS (sUN "Data") ["FFI_Export"]
         = do rest' <- toIFaceVal rest
              return $ ExportData (toFDesc d) : rest'
     | otherwise = ifail $ "Badly formed export list " ++ show tm
  
  toFDesc :: Term -> FDesc
  toFDesc (Constant (Str str)) = FStr str
  toFDesc tm
     | (P _ n _, []) <- unApply tm = FCon (deNS n)
     | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDesc as)
  toFDesc _ = FUnknown
  
  toFDescRet :: Term -> FDesc
  toFDescRet tm
     | (P _ ret _, [_,_,_,b]) <- unApply tm,
       ret == sNS (sUN "FFI_Ret") ["FFI_Export"]
         = toFDescBase b
     | (P _ io _, [_,_,_,b]) <- unApply tm,
       io == sNS (sUN "FFI_IO") ["FFI_Export"]
         = FIO $ toFDescBase b
     | (P _ fun _, [_,_,_,_,_,t]) <- unApply tm,
       fun == sNS (sUN "FFI_Fun") ["FFI_Export"]
         = toFDescRet t
     | otherwise = error "Badly formed export proof"
  
  toFDescBase :: Term -> FDesc
  toFDescBase tm
     | (P _ prim _, [_, _, _, pdesc]) <- unApply tm,
       prim == sNS (sUN "FFI_Prim") ["FFI_Export"]
         = toFDescPrim pdesc
     | (P _ prim _, [_, _, _, ddesc, _]) <- unApply tm,
       prim == sNS (sUN "FFI_ExpType") ["FFI_Export"]
         = toFDescPrim ddesc
     | otherwise = error "Badly formed export type"
  
  toFDescArgs :: Term -> [FDesc]
  toFDescArgs tm
     | (P _ fun _, [_,_,_,_,b,t]) <- unApply tm,
       fun == sNS (sUN "FFI_Fun") ["FFI_Export"]
         = toFDescBase b : toFDescArgs t
     | otherwise = []
  
  toFDescPrim (Constant (Str str)) = FStr str
  toFDescPrim tm
     | (P _ n _, []) <- unApply tm = FCon (deNS n)
     | (P _ n _, as) <- unApply tm = FApp (deNS n) (map toFDescPrim as)
  toFDescPrim _ = FUnknown
  
  deNS (NS n _) = n
  deNS n = n
  