@@ -1,4 +1,5 @@
11{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}
2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
23module Idris.Core.Execute (execute) where
34
45import Idris.AbsSyntax
@@ -111,7 +112,8 @@ toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env
111112 return $ normalise ctxt env' tm
112113 where toBinder (n, v) = do v' <- toTT v
113114 return (n, Let Erased v')
114−toTT (EHandle _) = return Erased
115+toTT (EHandle _) = execFail $ Msg "Can't convert handles back to TT after execution."
116+toTT (EPtr ptr) = execFail $ Msg "Can't convert pointers back to TT after execution."
115117
116118unApplyV :: ExecVal -> (ExecVal, [ExecVal])
117119unApplyV tm = ua [] tm
@@ -387,8 +389,8 @@ execForeign env ctxt arity ty fn xs onfail
387389 Nothing -> fail $ "Could not call foreign function \"" ++ f ++
388390 "\" with args " ++ show (map snd argTs)
389391 Just r -> return (mkEApp r xs')
390− Nothing -> return onfail
391−
392+ _ -> return onfail
393+
392394
393395splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits
394396 = Just (toFDesc l, r)
@@ -443,6 +445,9 @@ getOp fn [_, EHandle h]
443445 | fn == prf =
444446 Just $ do contents <- execIO $ hGetLine h
445447 return (EConstant (Str (contents ++ "\n")))
448+getOp fn [_, arg]
449+ | fn == prf =
450+ Just $ execFail (Msg "Can't use prim__readFile on a raw pointer in the executor.")
446451getOp n args = getPrim n primitives >>= flip applyPrim args
447452 where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)
448453 getPrim n [] = Nothing
@@ -486,6 +491,7 @@ execCase' env ctxt amap (Case sh n alts) | Just tm <- lookup n amap =
486491 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in
487492 execCase' env ctxt amap' newCase
488493 Nothing -> return Nothing
494+execCase' _ _ _ cse = fail $ "The impossible happened: tried to exec " ++ show cse
489495
490496chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
491497chooseAlt tm (DefaultCase sc : alts) | ok tm = Just (sc, [])
@@ -505,15 +511,6 @@ chooseAlt tm (_:alts) = chooseAlt tm alts
505511chooseAlt _ [] = Nothing
506512
507513
508−
509−
510−idrisType :: FType -> ExecVal
511−idrisType FUnit = EP Ref unitTy EErased
512−idrisType ft = EConstant (idr ft)
513− where idr (FArith ty) = AType ty
514− idr FString = StrType
515− idr FPtr = PtrType
516−
517514data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show
518515
519516toFType :: FDesc -> FType
@@ -574,7 +571,7 @@ call (FFun name argTypes retType) args =
574571 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))
575572 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)
576573 return $ EP Ref unitCon EErased
577−
574+ call' _ _ _ = fail "the impossible happened in call' in Execute.hs"
578575
579576 prepArgs = map prepArg
580577 prepArg (EConstant (I i)) = argCInt (fromIntegral i)