content: {-|
  Module      : Idris.Core.Execute
  Description : Execute Idris code and deal with FFI.
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  
  {-# LANGUAGE CPP, ExistentialQuantification, PatternGuards #-}
  {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
  module Idris.Core.Execute (execute) where
  
  import Idris.AbsSyntax
  import Idris.Core.CaseTree
  import Idris.Core.Evaluate
  import Idris.Core.TT
  import Idris.Error
  import Idris.Primitives (Prim(..), primitives)
  import IRTS.Lang (FDesc(..), FType(..))
  
  import Util.DynamicLinker
  import Util.System
  
  import Control.Exception
  import Control.Monad.Trans
  import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
  import Control.Monad.Trans.State.Strict
  import Data.IORef
  import Data.Maybe
  import Data.Time.Clock.POSIX (getPOSIXTime)
  import Data.Traversable (forM)
  import Debug.Trace
  import System.Directory
  import System.IO
  import System.IO.Error
  import System.IO.Unsafe
  
  #ifdef IDRIS_FFI
  import Foreign.C.String
  import Foreign.LibFFI
  import Foreign.Ptr
  #endif
  
  #ifndef IDRIS_FFI
  execute :: Term -> Idris Term
  execute tm = fail "libffi not supported, rebuild Idris with -f FFI"
  #else
  -- else is rest of file
  
  data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
  
  data ExecState = ExecState { exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
                             , binderNames :: [Name] -- ^ Used to uniquify binders when converting to TT
                             }
  
  data ExecVal = EP NameType Name ExecVal
               | EV Int
               | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
               | EApp ExecVal ExecVal
               | EType UExp
               | EUType Universe
               | EErased
               | EConstant Const
               | forall a. EPtr (Ptr a)
               | EThunk Context ExecEnv Term
               | EHandle Handle
               | EStringBuf (IORef String)
  
  fileError :: IORef ExecVal
  {-# NOINLINE fileError #-}
  fileError = unsafePerformIO $ newIORef $ operationNotPermitted
  
  operationNotPermitted =
    ioWrap $ mkRaw $ EApp (EP (DCon 0 1 False)
                              (sNS (sUN "GenericFileError") ["File", "Prelude"])
                              EErased)
                          (EConstant (I 1))
  
  namedFileError name =
    ioWrap $ mkRaw $ (EP (DCon 0 0 False)
                         (sNS (sUN name) ["File", "Prelude"])
                         EErased)
  
  mapError :: IOError -> ExecVal
  mapError e
    | (isDoesNotExistError e) = namedFileError "FileNotFound"
    | (isPermissionError e)   = namedFileError "PermissionDenied"
    | otherwise               = operationNotPermitted
  
  mkRaw :: ExecVal -> ExecVal
  mkRaw arg = EApp (EApp (EP (DCon 0 1 False) (sNS (sUN "MkRaw") ["FFI_C"]) EErased)
                         EErased) arg
  
  instance Show ExecVal where
    show (EP _ n _)        = show n
    show (EV i)            = "!!V" ++ show i ++ "!!"
    show (EBind n b body)  = "EBind " ++ show b ++ " <<fn>>"
    show (EApp e1 e2)      = show e1 ++ " (" ++ show e2 ++ ")"
    show (EType _)         = "Type"
    show (EUType _)        = "UType"
    show EErased           = "[__]"
    show (EConstant c)     = show c
    show (EPtr p)          = "<<ptr " ++ show p ++ ">>"
    show (EThunk _ env tm) = "<<thunk " ++ show env ++ "||||" ++ show tm ++ ">>"
    show (EHandle h)       = "<<handle " ++ show h ++ ">>"
    show (EStringBuf h)    = "<<string buffer>>"
  
  toTT :: ExecVal -> Exec Term
  toTT (EP nt n ty) = (P nt n) <$> (toTT ty)
  toTT (EV i) = return $ V i
  toTT (EBind n b body) = do n' <- newN n
                             body' <- body $ EP Bound n' EErased
                             b' <- fixBinder b
                             Bind n' b' <$> toTT body'
      where fixBinder (Lam rig t)    = Lam rig  <$> toTT t
            fixBinder (Pi rig i t k) = Pi rig i <$> toTT t <*> toTT k
            fixBinder (Let rig t1 t2)   = Let rig <$> toTT t1 <*> toTT t2
            fixBinder (NLet t1 t2)  = NLet    <$> toTT t1 <*> toTT t2
            fixBinder (Hole t)      = Hole    <$> toTT t
            fixBinder (GHole i ns t) = GHole i ns <$> toTT t
            fixBinder (Guess t1 t2) = Guess   <$> toTT t1 <*> toTT t2
            fixBinder (PVar rig t)  = PVar rig <$> toTT t
            fixBinder (PVTy t)      = PVTy    <$> toTT t
            newN n = do (ExecState hs ns) <- lift get
                        let n' = uniqueName n ns
                        lift (put (ExecState hs (n':ns)))
                        return n'
  toTT (EApp e1 e2) = do e1' <- toTT e1
                         e2' <- toTT e2
                         return $ App Complete e1' e2'
  toTT (EType u) = return $ TType u
  toTT (EUType u) = return $ UType u
  toTT EErased = return Erased
  toTT (EConstant c) = return (Constant c)
  toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env
                                 return $ normalise ctxt env' tm
    where toBinder (n, v) = do v' <- toTT v
                               return (n, RigW, Let RigW Erased v')
  toTT (EHandle _) = execFail $ Msg "Can't convert handles back to TT after execution."
  toTT (EPtr ptr) = execFail $ Msg "Can't convert pointers back to TT after execution."
  toTT (EStringBuf ptr) = execFail $ Msg "Can't convert string buffers back to TT after execution."
  
  unApplyV :: ExecVal -> (ExecVal, [ExecVal])
  unApplyV tm = ua [] tm
      where ua args (EApp f a) = ua (a:args) f
            ua args t = (t, args)
  
  mkEApp :: ExecVal -> [ExecVal] -> ExecVal
  mkEApp f [] = f
  mkEApp f (a:args) = mkEApp (EApp f a) args
  
  initState :: Idris ExecState
  initState = do ist <- getIState
                 return $ ExecState (idris_dynamic_libs ist) []
  
  type Exec = ExceptT Err (StateT ExecState IO)
  
  runExec :: Exec a -> ExecState -> IO (Either Err a)
  runExec ex st = fst <$> runStateT (runExceptT ex) st
  
  getExecState :: Exec ExecState
  getExecState = lift get
  
  execFail :: Err -> Exec a
  execFail = throwE
  
  execIO :: IO a -> Exec a
  execIO = lift . lift
  
  
  execute :: Term -> Idris Term
  execute tm = do est <- initState
                  ctxt <- getContext
                  res <- lift . lift . flip runExec est $
                           do res <- doExec [] ctxt tm
                              toTT res
                  case res of
                    Left err -> ierror err
                    Right tm' -> return tm'
  
  ioWrap :: ExecVal -> ExecVal
  ioWrap tm = mkEApp (EP (DCon 0 2 False) (sUN "prim__IO") EErased) [EErased, tm]
  
  ioUnit :: ExecVal
  ioUnit = ioWrap (EP Ref unitCon EErased)
  
  type ExecEnv = [(Name, ExecVal)]
  
  doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
  doExec env ctxt p@(P Ref n ty) | Just v <- lookup n env = return v
  doExec env ctxt p@(P Ref n ty) =
      do let val = lookupDef n ctxt
         case val of
           [Function _ tm] -> doExec env ctxt tm
           [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def
           [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later
           [CaseOp _ _ _ _ _ (CaseDefs ([], STerm tm) _)] -> -- nullary fun
               doExec env ctxt tm
           [CaseOp _ _ _ _ _ (CaseDefs (ns, sc) _)] -> return (EP Ref n EErased)
           [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."
           other | length other > 1 -> execFail . Msg $ "Multiple definitions found for " ++ show n
                 | otherwise        -> execFail . Msg . take 500 $ "got to " ++ show other ++ " lookup up " ++ show n
  doExec env ctxt p@(P Bound n ty) =
    case lookup n env of
      Nothing -> execFail . Msg $ "not found"
      Just tm -> return tm
  doExec env ctxt (P (DCon a b u) n _) = return (EP (DCon a b u) n EErased)
  doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)
  doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
                          | otherwise      = execFail . Msg $ "env too small"
  doExec env ctxt (Bind n (Let rig t v) body)
       = do v' <- doExec env ctxt v
            doExec ((n, v'):env) ctxt body
  doExec env ctxt (Bind n (NLet t v) body) = undefined
  doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)
                                          return $
                                            EBind n b' (\arg -> doExec ((n, arg):env) ctxt body)
  doExec env ctxt a@(App _ _ _) =
    do let (f, args) = unApply a
       f' <- doExec env ctxt f
       args' <- case f' of
                  (EP _ d _) | d == delay ->
                    case args of
                      [t,a,tm] -> do t' <- doExec env ctxt t
                                     a' <- doExec env ctxt a
                                     return [t', a', EThunk ctxt env tm]
                      _ -> mapM (doExec env ctxt) args -- partial applications are fine to evaluate
                  fun' -> do mapM (doExec env ctxt) args
       execApp env ctxt f' args'
  doExec env ctxt (Constant c) = return (EConstant c)
  doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in
                                doExec env ctxt ((x:xs) !! i)
  doExec env ctxt Erased = return EErased
  doExec env ctxt Impossible = fail "Tried to execute an impossible case"
  doExec env ctxt (Inferred t) = doExec env ctxt t
  doExec env ctxt (TType u) = return (EType u)
  doExec env ctxt (UType u) = return (EUType u)
  
  execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
  execApp env ctxt v [] = return v -- no args is just a constant! can result from function calls
  execApp env ctxt (EP _ f _) (t:a:delayed:rest)
    | f == force
    , (_, [_, _, EThunk tmCtxt tmEnv tm]) <- unApplyV delayed =
      do tm' <- doExec tmEnv tmCtxt tm
         execApp env ctxt tm' rest
  execApp env ctxt (EP _ fp _) (ty:action:rest)
    | fp == upio,
      (prim__IO, [_, v]) <- unApplyV action
         = execApp env ctxt v rest
  
  execApp env ctxt (EP _ fp _) args@(_:_:v:k:rest)
    | fp == piobind,
      (prim__IO, [_, v']) <- unApplyV v =
      do res <- execApp env ctxt k [v']
         execApp env ctxt res rest
  execApp env ctxt con@(EP _ fp _) args@(tp:v:rest)
    | fp == pioret = execApp env ctxt (mkEApp con [tp, v]) rest
  
  -- Special cases arising from not having access to the C RTS in the interpreter
  execApp env ctxt f@(EP _ fp _) args@(xs:_:_:_:args')
      | fp == mkfprim,
        (ty : fn : w : rest) <- reverse args' =
            execForeign env ctxt getArity ty fn rest (mkEApp f args)
    where getArity = case unEList xs of
                          Just as -> length as
                          _ -> 0
  
  execApp env ctxt c@(EP (DCon _ arity _) n _) args =
      do let args' = take arity args
         let restArgs = drop arity args
         execApp env ctxt (mkEApp c args') restArgs
  
  execApp env ctxt c@(EP (TCon _ arity) n _) args =
      do let args' = take arity args
         let restArgs = drop arity args
         execApp env ctxt (mkEApp c args') restArgs
  
  execApp env ctxt f@(EP _ n _) args
      | Just (res, rest) <- getOp n args = do r <- res
                                              execApp env ctxt r rest
  execApp env ctxt f@(EP _ n _) args =
      do let val = lookupDef n ctxt
         case val of
           [Function _ tm] -> fail "should already have been eval'd"
           [TyDecl nt ty] -> return $ mkEApp f args
           [Operator tp arity op] ->
               if length args >= arity
                 then let args' = take arity args in
                      case getOp n args' of
                        Just (res, []) -> do r <- res
                                             execApp env ctxt r (drop arity args)
                        _ -> return (mkEApp f args)
                 else return (mkEApp f args)
           [CaseOp _ _ _ _ _ (CaseDefs ([], STerm tm) _)] -> -- nullary fun
               do rhs <- doExec env ctxt tm
                  execApp env ctxt rhs args
           [CaseOp _ _ _ _ _ (CaseDefs (ns, sc) _)] ->
               do res <- execCase env ctxt ns sc args
                  return $ fromMaybe (mkEApp f args) res
           thing -> return $ mkEApp f args
  execApp env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg
                                                        let (f', as) = unApplyV ret
                                                        execApp env ctxt f' (as ++ args)
  execApp env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp env ctxt f (args1 ++ args2)
  execApp env ctxt f args = return (mkEApp f args)
  
  execForeign env ctxt arity ty fn xs onfail
      | Just (FFun "putStr" [(_, str)] _) <- foreignFromTT arity ty fn xs
         = case str of
             EConstant (Str arg) -> do execIO (putStr arg)
                                       execApp env ctxt ioUnit (drop arity xs)
             _ -> execFail . Msg $
                    "The argument to putStr should be a constant string, but it was " ++
                    show str ++
                    ". Are all cases covered?"
      | Just (FFun "putchar" [(_, ch)] _) <- foreignFromTT arity ty fn xs
             = case ch of
                 EConstant (Ch c) -> do execIO (putChar c)
                                        execApp env ctxt ioUnit (drop arity xs)
                 EConstant (I i)  -> do execIO (putChar (toEnum i))
                                        execApp env ctxt ioUnit (drop arity xs)
                 _ -> execFail . Msg $
                        "The argument to putchar should be a constant character, but it was " ++
                        show str ++
                        ". Are all cases covered?"
      | Just (FFun "idris_readStr" [_, (_, handle)] _) <- foreignFromTT arity ty fn xs
             = case handle of
                 EHandle h -> do contents <- execIO $ hGetLine h
                                 execApp env ctxt (EConstant (Str (contents ++ "\n"))) (drop arity xs)
                 _ -> execFail . Msg $
                        "The argument to idris_readStr should be a handle, but it was " ++
                        show handle ++
                        ". Are all cases covered?"
      | Just (FFun "getchar" _ _) <- foreignFromTT arity ty fn xs
             = do -- The C API returns an Int which Idris library code
                  -- converts; thus, we must make an int here.
                  ch <- execIO $ fmap (ioWrap . EConstant . I . fromEnum) getChar
                  execApp env ctxt ch xs
      | Just (FFun "idris_time" _ _) <- foreignFromTT arity ty fn xs
             = do execIO $ fmap (ioWrap . mkRaw . EConstant . I . round) getPOSIXTime
      | Just (FFun "idris_showerror" _ _) <- foreignFromTT arity ty fn xs
             = do execIO $ return $ ioWrap $ EConstant $ Str "Operation not permitted"
      | Just (FFun "idris_mkFileError" _ _) <- foreignFromTT arity ty fn xs
             = do execIO $ readIORef fileError
      | Just (FFun "fileOpen" [(_,fileStr), (_,modeStr)] _) <- foreignFromTT arity ty fn xs
             = case (fileStr, modeStr) of
                 (EConstant (Str f), EConstant (Str mode)) ->
                   do f <- execIO $
                           catch (do let m = case filter (/= 'b') mode of
                                               "r"  -> Right ReadMode
                                               "w"  -> Right WriteMode
                                               "a"  -> Right AppendMode
                                               "rw" -> Right ReadWriteMode
                                               "wr" -> Right ReadWriteMode
                                               "r+" -> Right ReadWriteMode
                                               _    -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)
                                     case fmap (openFile f) m of
                                       Right h -> do h' <- h
                                                     hSetBinaryMode h' True
                                                     return $ Right (ioWrap (EHandle h'), drop arity xs)
                                       Left err -> return $ Left err)
                                 (\e -> do writeIORef fileError $ mapError e
                                           return $ Right (ioWrap (EPtr nullPtr), drop arity xs))
                      case f of
                        Left err -> execFail . Msg $ err
                        Right (res, rest) -> execApp env ctxt res rest
                 _ -> execFail . Msg $
                        "The arguments to fileOpen should be constant strings, but they were " ++
                        show fileStr ++ " and " ++ show modeStr ++
                        ". Are all cases covered?"
      | Just (FFun "fileEOF" [(_,handle)] _) <- foreignFromTT arity ty fn xs
             = case handle of
                 EHandle h -> do eofp <- execIO $ hIsEOF h
                                 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))
                                 execApp env ctxt res (drop arity xs)
                 _ -> execFail . Msg $
                        "The argument to fileEOF should be a file handle, but it was " ++
                        show handle ++
                        ". Are all cases covered?"
      | Just (FFun "fileError" [(_,handle)] _) <- foreignFromTT arity ty fn xs
             = case handle of
               -- errors handled differently in Haskell than in C, so if
               -- there's been an error we'll have had an exception already.
               -- Therefore, assume we're okay.
                 EHandle h -> do let res = ioWrap (EConstant (I 0))
                                 execApp env ctxt res (drop arity xs)
                 _ -> execFail . Msg $
                        "The argument to fileError should be a file handle, but it was " ++
                        show handle ++
                        ". Are all cases covered?"
      | Just (FFun "fileRemove" [(_,fileStr)] _) <- foreignFromTT arity ty fn xs
             = case fileStr of
                 EConstant (Str f) -> do res <- execIO $ catch (do removeFile f
                                                                   return $ ioWrap $ EConstant $ I 0)
                                                               (\e -> do writeIORef fileError $ mapError e
                                                                         return $ ioWrap $ EConstant $ I (-1))
                                         execApp env ctxt res (drop arity xs)
                 _ -> execFail . Msg $
                        "The argument to fileRemove should be a constant string, but it was " ++
                        show fileStr ++
                        ". Are all cases covered?"
      | Just (FFun "fileClose" [(_,handle)] _) <- foreignFromTT arity ty fn xs
             = case handle of
                 EHandle h -> do execIO $ hClose h
                                 execApp env ctxt ioUnit (drop arity xs)
                 _ -> execFail . Msg $
                        "The argument to fileClose should be a file handle, but it was " ++
                        show handle ++
                        ". Are all cases covered?"
      | Just (FFun "fileSize" [(_,handle)] _) <- foreignFromTT arity ty fn xs
             = case handle of
                 EHandle h -> do size <- execIO $ hFileSize h
                                 let res = ioWrap (EConstant (I (fromInteger size)))
                                 execApp env ctxt res (drop arity xs)
                 _ -> execFail . Msg $
                        "The argument to fileSize should be a file handle, but it was " ++
                        show handle ++
                        ". Are all cases covered?"
  
      | Just (FFun "isNull" [(_, ptr)] _) <- foreignFromTT arity ty fn xs
             = case ptr of
                 EPtr p -> let res = ioWrap . EConstant . I $
                                     if p == nullPtr then 1 else 0
                           in execApp env ctxt res (drop arity xs)
                 -- Handles will be checked as null pointers sometimes - but if we got a
                 -- real Handle, then it's valid, so just return 1.
                 EHandle h -> let res = ioWrap . EConstant . I $ 0
                              in execApp env ctxt res (drop arity xs)
                 -- A foreign-returned char* has to be tested for NULL sometimes
                 EConstant (Str s) -> let res = ioWrap . EConstant . I $ 0
                                      in execApp env ctxt res (drop arity xs)
                 _ -> execFail . Msg $
                        "The argument to isNull should be a pointer or file handle or string, but it was " ++
                        show ptr ++
                        ". Are all cases covered?"
  
      | Just (FFun "idris_disableBuffering" _ _) <- foreignFromTT arity ty fn xs
         = do execIO $ hSetBuffering stdin NoBuffering
              execIO $ hSetBuffering stdout NoBuffering
              execApp env ctxt ioUnit (drop arity xs)
  
      -- Just use a Haskell String in an IORef for a string buffer
      | Just (FFun "idris_makeStringBuffer" [(_, len)] _) <- foreignFromTT arity ty fn xs
         = case len of
                EConstant (I _) -> do buf <- execIO $ newIORef ""
                                      let res = ioWrap (EStringBuf buf)
                                      execApp env ctxt res (drop arity xs)
  
                _ -> execFail . Msg $
                        "The argument to idris_makeStringBuffer should be an Int, but it was " ++
                        show len ++
                        ". Are all cases covered?"
      | Just (FFun "idris_addToString" [(_, strBuf), (_, str)] _) <- foreignFromTT arity ty fn xs
         = case (strBuf, str) of
                (EStringBuf ref, EConstant (Str add)) ->
                    do execIO $ modifyIORef ref (++add)
                       execApp env ctxt ioUnit (drop arity xs)
                _ -> execFail . Msg $
                        "The arguments to idris_addToString should be a StringBuffer and a String, but were " ++
                        show strBuf ++ " and " ++ show str ++
                        ". Are all cases covered?"
      | Just (FFun "idris_getString" [_, (_, str)] _) <- foreignFromTT arity ty fn xs
         = case str of
                EStringBuf ref -> do str <- execIO $ readIORef ref
                                     let res = ioWrap (mkRaw (EConstant (Str str)))
                                     execApp env ctxt res (drop arity xs)
                _ -> execFail . Msg $
                        "The argument to idris_getString should be a StringBuffer, but it was " ++
                        show str ++
                        ". Are all cases covered?"
  
  
  
  -- Right now, there's no way to send command-line arguments to the executor,
  -- so just return 0.
  execForeign env ctxt arity ty fn xs onfail
      | Just (FFun "idris_numArgs" _ _) <- foreignFromTT arity ty fn xs
             = let res = ioWrap . EConstant . I $ 0
               in execApp env ctxt res (drop arity xs)
  
  execForeign env ctxt arity ty fn xs onfail
     = case foreignFromTT arity ty fn xs of
          Just ffun@(FFun f argTs retT) | length xs >= arity ->
             do let (_, xs') = (take arity xs, -- foreign args
                                drop arity xs) -- rest
                res <- call ffun (map snd argTs)
                case res of
                     Nothing -> fail $ "Could not call foreign function \"" ++ f ++
                                       "\" with args " ++ show (map snd argTs)
                     Just r -> return (mkEApp r xs')
          _ -> return onfail
  
  
  splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits
      = Just (toFDesc l, r)
  splitArg _ = Nothing
  
  toFDesc tm
     | (EP _ n _, []) <- unApplyV tm = FCon (deNS n)
     | (EP _ n _, as) <- unApplyV tm = FApp (deNS n) (map toFDesc as)
  toFDesc _ = FUnknown
  
  deNS (NS n _) = n
  deNS n = n
  
  prf = sUN "prim__readFile"
  prc = sUN "prim__readChars"
  pwf = sUN "prim__writeFile"
  prs = sUN "prim__readString"
  pws = sUN "prim__writeString"
  pbm = sUN "prim__believe_me"
  pstdin = sUN "prim__stdin"
  pstdout = sUN "prim__stdout"
  mkfprim = sUN "mkForeignPrim"
  pioret = sUN "prim_io_pure"
  piobind = sUN "prim_io_bind"
  upio = sUN "unsafePerformPrimIO"
  delay = sUN "Delay"
  force = sUN "Force"
  
  -- | Look up primitive operations in the global table and transform
  -- them into ExecVal functions
  getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
  getOp fn (_ : _ : x : xs) | fn == pbm = Just (return x, xs)
  getOp fn (_ : EConstant (Str n) : xs)
      | fn == pws =
                Just (do execIO $ putStr n >> hFlush stdout
                         return (EConstant (I 0)), xs)
  getOp fn (_:xs)
      | fn == prs =
                Just (do line <- execIO getLine
                         return (EConstant (Str line)), xs)
  getOp fn (_ : EP _ fn' _ : EConstant (Str n) : xs)
      | fn == pwf && fn' == pstdout =
                Just (do execIO $ putStr n >> hFlush stdout
                         return (EConstant (I 0)), xs)
  getOp fn (_ : EP _ fn' _ : xs)
      | fn == prf && fn' == pstdin =
                Just (do line <- execIO getLine
                         return (EConstant (Str line)), xs)
  getOp fn (_ : EHandle h : EConstant (Str n) : xs)
      | fn == pwf =
                Just (do execIO $ hPutStr h n >> hFlush h
                         return (EConstant (I 0)), xs)
  getOp fn (_ : EHandle h : xs)
      | fn == prf =
                Just (do contents <- execIO $ hGetLine h
                         return (EConstant (Str (contents ++ "\n"))), xs)
  getOp fn (_ : EConstant (I len) : EHandle h : xs)
      | fn == prc =
                Just (do contents <- execIO $ hGetChars h len
                         return (EConstant (Str contents)), xs)
    where hGetChars h 0 = return ""
          hGetChars h i = do eof <- hIsEOF h
                             if eof then return "" else do
                               c <- hGetChar h
                               rest <- hGetChars h (i - 1)
                               return (c : rest)
  getOp fn (_ : arg : xs)
      | fn == prf =
                Just $ (execFail (Msg "Can't use prim__readFile on a raw pointer in the executor."), xs)
  getOp n args = do (arity, prim) <- getPrim n primitives
                    if (length args >= arity)
                       then do res <- applyPrim prim (take arity args)
                               Just (res, drop arity args)
                       else Nothing
      where getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
            getPrim n [] = Nothing
            getPrim n ((Prim pn _ arity def _ _) : prims)
               | n == pn   = Just (arity, execPrim def)
               | otherwise = getPrim n prims
  
            execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
            execPrim f args = EConstant <$> (mapM getConst args >>= f)
  
            getConst (EConstant c) = Just c
            getConst _             = Nothing
  
            applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
            applyPrim fn args = return <$> fn args
  
  
  
  
  -- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
  -- evaluates them, then begins the checks for matching cases.
  execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
  execCase env ctxt ns sc args =
      let arity = length ns in
      if arity <= length args
      then do let amap = zip ns args
  --            trace ("Case " ++ show sc ++ "\n   in " ++ show amap ++"\n   in env " ++ show env ++ "\n\n" ) $ return ()
              caseRes <- execCase' env ctxt amap sc
              case caseRes of
                Just res -> Just <$> execApp (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)
                Nothing -> return Nothing
      else return Nothing
  
  -- | Take bindings and a case tree and examines them, executing the matching case if possible.
  execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
  execCase' env ctxt amap (UnmatchedCase _) = return Nothing
  execCase' env ctxt amap (STerm tm) =
      Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm
  execCase' env ctxt amap (Case sh n alts) | Just tm <- lookup n amap =
         case chooseAlt tm alts of
           Just (newCase, newBindings) ->
               let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
               execCase' env ctxt amap' newCase
           Nothing -> return Nothing
  execCase' _ _ _ cse = fail $ "The impossible happened: tried to exec  " ++ show cse
  
  chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
  chooseAlt tm (DefaultCase sc : alts) | ok tm = Just (sc, [])
                                       | otherwise = Nothing
    where -- Default cases should only work on applications of constructors or on constants
          ok (EApp f x) = ok f
          ok (EP Bound _ _) = False
          ok (EP Ref _ _) = False
          ok _ = True
  
  
  chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
  chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
                                          , cn == n = Just (sc, zip ns args)
                                          | otherwise = chooseAlt tm alts
  chooseAlt tm (_:alts) = chooseAlt tm alts
  chooseAlt _ [] = Nothing
  
  
  data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show
  
  toFType :: FDesc -> FType
  toFType (FCon c)
      | c == sUN "C_Str" = FString
      | c == sUN "C_Float" = FArith ATFloat
      | c == sUN "C_Ptr" = FPtr
      | c == sUN "C_MPtr" = FManagedPtr
      | c == sUN "C_Unit" = FUnit
  toFType (FApp c [_,ity])
      | c == sUN "C_IntT" = FArith (toAType ity)
    where toAType (FCon i)
            | i == sUN "C_IntChar" = ATInt ITChar
            | i == sUN "C_IntNative" = ATInt ITNative
            | i == sUN "C_IntBits8" = ATInt (ITFixed IT8)
            | i == sUN "C_IntBits16" = ATInt (ITFixed IT16)
            | i == sUN "C_IntBits32" = ATInt (ITFixed IT32)
            | i == sUN "C_IntBits64" = ATInt (ITFixed IT64)
          toAType t = error (show t ++ " not defined in toAType")
  
  toFType (FApp c [_])
      | c == sUN "C_Any" = FAny
  toFType t = error (show t ++ " not defined in toFType")
  
  call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
  call (FFun name argTypes retType) args =
      do fn <- findForeign name
         maybe (return Nothing)
               (\f -> Just . ioWrap <$> call' f args (toFType retType)) fn
      where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
            call' (Fun _ h) args (FArith (ATInt ITNative)) = do
              res <- execIO $ callFFI h retCInt (prepArgs args)
              return (EConstant (I (fromIntegral res)))
            call' (Fun _ h) args (FArith (ATInt (ITFixed IT8))) = do
              res <- execIO $ callFFI h retCChar (prepArgs args)
              return (EConstant (B8 (fromIntegral res)))
            call' (Fun _ h) args (FArith (ATInt (ITFixed IT16))) = do
              res <- execIO $ callFFI h retCWchar (prepArgs args)
              return (EConstant (B16 (fromIntegral res)))
            call' (Fun _ h) args (FArith (ATInt (ITFixed IT32))) = do
              res <- execIO $ callFFI h retCInt (prepArgs args)
              return (EConstant (B32 (fromIntegral res)))
            call' (Fun _ h) args (FArith (ATInt (ITFixed IT64))) = do
              res <- execIO $ callFFI h retCLong (prepArgs args)
              return (EConstant (B64 (fromIntegral res)))
            call' (Fun _ h) args (FArith ATFloat) = do
              res <- execIO $ callFFI h retCDouble (prepArgs args)
              return (EConstant (Fl (realToFrac res)))
            call' (Fun _ h) args (FArith (ATInt ITChar)) = do
              res <- execIO $ callFFI h retCChar (prepArgs args)
              return (EConstant (Ch (castCCharToChar res)))
            call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)
                                              if res == nullPtr
                                                 then return (EPtr res)
                                                 else do hStr <- execIO $ peekCString res
                                                         return (EConstant (Str hStr))
  
            call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))
            call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)
                                            return $ EP Ref unitCon EErased
            call' _ _ _ = fail "the impossible happened in call' in Execute.hs"
  
            prepArgs = map prepArg
            prepArg (EConstant (I i)) = argCInt (fromIntegral i)
            prepArg (EConstant (B8 i)) = argCChar (fromIntegral i)
            prepArg (EConstant (B16 i)) = argCWchar (fromIntegral i)
            prepArg (EConstant (B32 i)) = argCInt (fromIntegral i)
            prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)
            prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)
            prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars
                                                                      -- Issue #1720 on the issue tracker.
                                                                      -- https://github.com/idris-lang/Idris-dev/issues/1720
            prepArg (EConstant (Str s)) = argString s
            prepArg (EPtr p) = argPtr p
            prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined
  
  
  foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
  foreignFromTT arity ty (EConstant (Str name)) args
      = do argFTyVals <- mapM splitArg (take arity args)
           return $ FFun name argFTyVals (toFDesc ty)
  foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing
  
  unEList :: ExecVal -> Maybe [ExecVal]
  unEList tm = case unApplyV tm of
                 (nil, [_]) -> Just []
                 (cons, ([_, x, xs])) ->
                     do rest <- unEList xs
                        return $ x:rest
                 (f, args) -> Nothing
  
  
  mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
  mapMaybeM f [] = return []
  mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
                          maybe rest (:rest) <$> f x
  findForeign :: String -> Exec (Maybe ForeignFun)
  findForeign fn = do est <- getExecState
                      let libs = exec_dynamic_libs est
                      fns <- mapMaybeM getFn libs
                      case fns of
                        [f] -> return (Just f)
                        [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"
                                 return Nothing
                        fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++
                                                     show (length fs) ++ " occurrences."
                                 return Nothing
      where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)
  
  #endif
  