@@ -23,9 +23,11 @@ import Control.Exception
2323import Control.Monad.Trans
2424import Control.Monad.Trans.State.Strict
2525import Control.Monad.Trans.Error
26−import Control.Monad
26+import Control.Monad hiding (forM)
2727import Data.Maybe
2828import Data.Bits
29+import Data.Traversable (forM)
30+import Data.Time.Clock.POSIX (getPOSIXTime)
2931import qualified Data.Map as M
3032
3133#ifdef IDRIS_FFI
@@ -163,7 +165,8 @@ doExec env ctxt p@(P Ref n ty) =
163165 doExec env ctxt tm
164166 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)
165167 [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."
166− thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined
168+ other | length other > 1 -> execFail . Msg $ "Multiple definitions found for " ++ show n
169+ | otherwise -> execFail . Msg . take 500 $ "got to " ++ show other ++ " lookup up " ++ show n
167170doExec env ctxt p@(P Bound n ty) =
168171 case lookup n env of
169172 Nothing -> execFail . Msg $ "not found"
@@ -175,9 +178,9 @@ doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))
175178doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v
176179 doExec ((n, v'):env) ctxt body
177180doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined
178−doExec env ctxt tm@(Bind n b body) = return $
179− EBind n (fmap (\_->EErased) b)
180− (\arg -> doExec ((n, arg):env) ctxt body)
181+doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)
182+ return $
183+ EBind n b' (\arg -> doExec ((n, arg):env) ctxt body)
181184doExec env ctxt a@(App _ _) =
182185 do let (f, args) = unApply a
183186 f' <- doExec env ctxt f
@@ -250,6 +253,10 @@ execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)
250253 "The argument to idris_readStr should be a handle, but it was " ++
251254 show handle ++
252255 ". Are all cases covered?"
256+execApp env ctxt (EP _ fp _) (_:fn:rest)
257+ | fp == mkfprim,
258+ Just (FFun "idris_time" _ _) <- foreignFromTT fn
259+ = do execIO $ fmap (ioWrap . EConstant . I . round) getPOSIXTime
253260execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
254261 | fp == mkfprim,
255262 Just (FFun "fileOpen" _ _) <- foreignFromTT fn
@@ -265,7 +272,9 @@ execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)
265272 "r+" -> Right ReadWriteMode
266273 _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)
267274 case fmap (openFile f) m of
268− Right h -> do h' <- h; return $ Right (ioWrap (EHandle h'), tail rest)
275+ Right h -> do h' <- h
276+ hSetBinaryMode h' True
277+ return $ Right (ioWrap (EHandle h'), tail rest)
269278 Left err -> return $ Left err)
270279 (\e -> let _ = ( e::SomeException)
271280 in return $ Right (ioWrap (EPtr nullPtr), tail rest))
@@ -442,7 +451,15 @@ execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =
442451 Nothing -> return Nothing
443452
444453chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
445−chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])
454+chooseAlt tm (DefaultCase sc : alts) | ok tm = Just (sc, [])
455+ | otherwise = Nothing
456+ where -- Default cases should only work on applications of constructors or on constants
457+ ok (EApp f x) = ok f
458+ ok (EP Bound _ _) = False
459+ ok (EP Ref _ _) = False
460+ ok _ = True
461+
462+
446463chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])
447464chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm
448465 , cn == n = Just (sc, zip ns args)