8a108b4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1475 from david-christiansen/testing-postulates-work

8a108b4David Christiansen12 years ago

idris.cabal+2

compare with master

unifiedsplit

@@ -690,6 +690,8 @@ Library

690 , zlib

691 , optparse-applicative >= 0.8

692 Extensions: MultiParamTypeClasses

693+ , DeriveFoldable

694+ , DeriveTraversable

693 , FunctionalDependencies

695 , FunctionalDependencies

694 , FlexibleContexts

696 , FlexibleContexts

695 , FlexibleInstances

697 , FlexibleInstances

src/Idris/Core/Execute.hs+24−7

@@ -23,9 +23,11 @@ import Control.Exception

23import Control.Monad.Trans

24import Control.Monad.Trans.State.Strict

25import Control.Monad.Trans.Error

26−import Control.Monad

26+import Control.Monad hiding (forM)

27import Data.Maybe

28import Data.Bits

29+import Data.Traversable (forM)

30+import Data.Time.Clock.POSIX (getPOSIXTime)

29import qualified Data.Map as M

31import qualified Data.Map as M

31#ifdef IDRIS_FFI

33#ifdef IDRIS_FFI

@@ -163,7 +165,8 @@ doExec env ctxt p@(P Ref n ty) =

163 doExec env ctxt tm

165 doExec env ctxt tm

164 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)

166 [CaseOp _ _ _ _ _ (CaseDefs _ (ns, sc) _ _)] -> return (EP Ref n EErased)

165 [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."

167 [] -> execFail . Msg $ "Could not find " ++ show n ++ " in definitions."

168+ other | length other > 1 -> execFail . Msg $ "Multiple definitions found for " ++ show n

166− thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

169+ | otherwise -> execFail . Msg . take 500 $ "got to " ++ show other ++ " lookup up " ++ show n

167doExec env ctxt p@(P Bound n ty) =

170doExec env ctxt p@(P Bound n ty) =

168 case lookup n env of

171 case lookup n env of

169 Nothing -> execFail . Msg $ "not found"

172 Nothing -> execFail . Msg $ "not found"

@@ -175,9 +178,9 @@ doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

175doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

178doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

176 doExec ((n, v'):env) ctxt body

179 doExec ((n, v'):env) ctxt body

177doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

180doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

178−doExec env ctxt tm@(Bind n b body) = return $

181+doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)

179− EBind n (fmap (\_->EErased) b)

182+ return $

180− (\arg -> doExec ((n, arg):env) ctxt body)

183+ EBind n b' (\arg -> doExec ((n, arg):env) ctxt body)

181doExec env ctxt a@(App _ _) =

184doExec env ctxt a@(App _ _) =

182 do let (f, args) = unApply a

185 do let (f, args) = unApply a

183 f' <- doExec env ctxt f

186 f' <- doExec env ctxt f

@@ -250,6 +253,10 @@ execApp env ctxt (EP _ fp _) (_:fn:_:handle:_:rest)

250 "The argument to idris_readStr should be a handle, but it was " ++

253 "The argument to idris_readStr should be a handle, but it was " ++

251 show handle ++

254 show handle ++

252 ". Are all cases covered?"

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

253execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)

260execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)

254 | fp == mkfprim,

261 | fp == mkfprim,

255 Just (FFun "fileOpen" _ _) <- foreignFromTT fn

262 Just (FFun "fileOpen" _ _) <- foreignFromTT fn

@@ -265,7 +272,9 @@ execApp env ctxt (EP _ fp _) (_:fn:fileStr:modeStr:rest)

265 "r+" -> Right ReadWriteMode

272 "r+" -> Right ReadWriteMode

266 _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)

273 _ -> Left ("Invalid mode for " ++ f ++ ": " ++ mode)

267 case fmap (openFile f) m of

274 case fmap (openFile f) m of

275+ Right h -> do h' <- h

276+ hSetBinaryMode h' True

268− Right h -> do h' <- h; return $ Right (ioWrap (EHandle h'), tail rest)

277+ return $ Right (ioWrap (EHandle h'), tail rest)

269 Left err -> return $ Left err)

278 Left err -> return $ Left err)

270 (\e -> let _ = ( e::SomeException)

279 (\e -> let _ = ( e::SomeException)

271 in return $ Right (ioWrap (EPtr nullPtr), tail rest))

280 in return $ Right (ioWrap (EPtr nullPtr), tail rest))

@@ -442,7 +451,15 @@ execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

442 Nothing -> return Nothing

451 Nothing -> return Nothing

443

452

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

453chooseAlt :: 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+

446chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])

463chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])

447chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm

464chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm

448 , cn == n = Just (sc, zip ns args)

465 , cn == n = Just (sc, zip ns args)

src/Idris/Core/TT.hs+3−1

@@ -31,6 +31,8 @@ import Numeric (showIntAtBase)

31import qualified Data.Text as T

32import Data.List

33import Data.Maybe (listToMaybe)

34+import Data.Foldable (Foldable)

35+import Data.Traversable (Traversable)

34import Data.Vector.Unboxed (Vector)

36import Data.Vector.Unboxed (Vector)

35import qualified Data.Vector.Unboxed as V

37import qualified Data.Vector.Unboxed as V

36import qualified Data.Binary as B

38import qualified Data.Binary as B

@@ -638,7 +640,7 @@ data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}

638 | PVar { binderTy :: !b }

640 | PVar { binderTy :: !b }

639 -- ^ A pattern variable

641 -- ^ A pattern variable

640 | PVTy { binderTy :: !b }

642 | PVTy { binderTy :: !b }

641− deriving (Show, Eq, Ord, Functor)

643+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)

642{-!

644{-!

643deriving instance Binary Binder

645deriving instance Binary Binder

644deriving instance NFData Binder

646deriving instance NFData Binder

src/Idris/Providers.hs+2−1

@@ -34,5 +34,6 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm

34 , pioret == ioret && nm == prmod

35 = return . Provide $ res

36 | otherwise = ifail $ "Internal type provider error: result was not " ++

37− "IO (Provider a), or perhaps missing normalisation."

37+ "IO (Provider a), or perhaps missing normalisation." ++

38+ "Term: " ++ take 1000 (show tm)