4887599 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2018 from david-christiansen/issue/2010

4887599David Christiansen12 years ago

src/Idris/Core/Execute.hs+10−13

compare with master

unifiedsplit

@@ -1,4 +1,5 @@

1{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

2module Idris.Core.Execute (execute) where

3module Idris.Core.Execute (execute) where

4import Idris.AbsSyntax

5import Idris.AbsSyntax

@@ -111,7 +112,8 @@ toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env

111 return $ normalise ctxt env' tm

112 return $ normalise ctxt env' tm

112 where toBinder (n, v) = do v' <- toTT v

113 where toBinder (n, v) = do v' <- toTT v

113 return (n, Let Erased v')

114 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."

115

117

116unApplyV :: ExecVal -> (ExecVal, [ExecVal])

118unApplyV :: ExecVal -> (ExecVal, [ExecVal])

117unApplyV tm = ua [] tm

119unApplyV tm = ua [] tm

@@ -387,8 +389,8 @@ execForeign env ctxt arity ty fn xs onfail

387 Nothing -> fail $ "Could not call foreign function \"" ++ f ++

389 Nothing -> fail $ "Could not call foreign function \"" ++ f ++

388 "\" with args " ++ show (map snd argTs)

390 "\" with args " ++ show (map snd argTs)

389 Just r -> return (mkEApp r xs')

391 Just r -> return (mkEApp r xs')

390− Nothing -> return onfail

392+ _ -> return onfail

391−

393+

392

394

393splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits

395splitArg tm | (_, [_,_,l,r]) <- unApplyV tm -- pair, two implicits

394 = Just (toFDesc l, r)

396 = Just (toFDesc l, r)

@@ -443,6 +445,9 @@ getOp fn [_, EHandle h]

443 | fn == prf =

445 | fn == prf =

444 Just $ do contents <- execIO $ hGetLine h

446 Just $ do contents <- execIO $ hGetLine h

445 return (EConstant (Str (contents ++ "\n")))

447 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.")

446getOp n args = getPrim n primitives >>= flip applyPrim args

451getOp n args = getPrim n primitives >>= flip applyPrim args

447 where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)

452 where getPrim :: Name -> [Prim] -> Maybe ([ExecVal] -> Maybe ExecVal)

448 getPrim n [] = Nothing

453 getPrim n [] = Nothing

@@ -486,6 +491,7 @@ execCase' env ctxt amap (Case sh n alts) | Just tm <- lookup n amap =

486 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

491 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

487 execCase' env ctxt amap' newCase

492 execCase' env ctxt amap' newCase

488 Nothing -> return Nothing

493 Nothing -> return Nothing

494+execCase' _ _ _ cse = fail $ "The impossible happened: tried to exec " ++ show cse

489

495

490chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])

496chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])

491chooseAlt tm (DefaultCase sc : alts) | ok tm = Just (sc, [])

497chooseAlt tm (DefaultCase sc : alts) | ok tm = Just (sc, [])

@@ -505,15 +511,6 @@ chooseAlt tm (_:alts) = chooseAlt tm alts

505chooseAlt _ [] = Nothing

511chooseAlt _ [] = Nothing

506

512

507

513

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−

517data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show

514data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Show

518

515

519toFType :: FDesc -> FType

516toFType :: FDesc -> FType

@@ -574,7 +571,7 @@ call (FFun name argTypes retType) args =

574 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))

571 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))

575 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)

572 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)

576 return $ EP Ref unitCon EErased

573 return $ EP Ref unitCon EErased

577−

574+ call' _ _ _ = fail "the impossible happened in call' in Execute.hs"

578

575

579 prepArgs = map prepArg

576 prepArgs = map prepArg

580 prepArg (EConstant (I i)) = argCInt (fromIntegral i)

577 prepArg (EConstant (I i)) = argCInt (fromIntegral i)