e30ff97 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:idris-lang/Idris-dev

e30ff97Edwin Brady12 years ago

idris.cabal+2

compare with master

unifiedsplit

@@ -691,6 +691,8 @@ Library

691 , zlib

692 , optparse-applicative >= 0.8

693 Extensions: MultiParamTypeClasses

694+ , DeriveFoldable

695+ , DeriveTraversable

694 , FunctionalDependencies

696 , FunctionalDependencies

695 , FlexibleContexts

697 , FlexibleContexts

696 , FlexibleInstances

698 , FlexibleInstances

libs/prelude/IO.idr+6−2

@@ -5,7 +5,9 @@ import Prelude.List

5%access public

7||| Idris's primitive IO, for building abstractions on top of

8−abstract data PrimIO a = prim__IO a

8+abstract

9+data PrimIO : Type -> Type where

10+ prim__IO : a -> PrimIO a

10||| A token representing the world, for use in `IO`

12||| A token representing the world, for use in `IO`

11abstract data World = TheWorld

13abstract data World = TheWorld

@@ -15,7 +17,9 @@ WorldRes x = x

16-- abstract data WorldRes a = MkWR a World

18-- abstract data WorldRes a = MkWR a World

20+abstract

21+data IO : Type -> Type where

18−abstract data IO a = MkIO (World -> PrimIO (WorldRes a))

22+ MkIO : (World -> PrimIO (WorldRes a)) -> IO a

20abstract

24abstract

21prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b

25prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b

src/IRTS/Bytecode.hs+82−24

@@ -25,30 +25,88 @@ returns) are stored.

25data Reg = RVal | L Int | T Int | Tmp

26 deriving (Show, Eq)

28+data BC =

29+ -- reg1 = reg2

28−data BC = ASSIGN Reg Reg

30+ ASSIGN Reg Reg

31+

32+ -- reg = const

29− | ASSIGNCONST Reg Const

33+ | ASSIGNCONST Reg Const

34+

35+ -- reg1 = reg2 (same as assign, it seems)

30− | UPDATE Reg Reg

36+ | UPDATE Reg Reg

37+

38+ -- reg = constructor, where constructor consists of a tag and

39+ -- values from registers, e.g. (cons tag args)

40+ -- the 'Maybe Reg', if set, is a register which can be overwritten

41+ -- (i.e. safe for mutable update), though this can be ignored

31− | MKCON Reg (Maybe Reg) Int [Reg]

42+ | MKCON Reg (Maybe Reg) Int [Reg]

32− | CASE Bool -- definitely a constructor, no need to check, if true

43+

44+ -- Matching on value of reg: usually (but not always) there are

45+ -- constructors, hence "Int" for patterns (that's a tag on which

46+ -- we should match), and the following [BC] is just a list of

47+ -- instructions for the corresponding case. The last argument is

48+ -- for default case. When it's not necessary a constructor in the

49+ -- reg, the Bool should be False, indicating that it's not safe to

50+ -- work with that as with a constructor, so a check should be

51+ -- added. If it's not a constructor, default case should be used.

52+ | CASE Bool

33− Reg [(Int, [BC])] (Maybe [BC])

53+ Reg [(Int, [BC])] (Maybe [BC])

34− | PROJECT Reg Int Int -- get all args from reg, put them from Int onwards

54+

55+ -- get a value from register, which should be a constructor, and

56+ -- put its arguments into the stack, starting from (base + int1)

57+ -- and onwards; second Int provides arity

58+ | PROJECT Reg Int Int

59+

60+ -- probably not used

35− | PROJECTINTO Reg Reg Int -- project argument from one reg into another

61+ | PROJECTINTO Reg Reg Int -- project argument from one reg into another

62+

63+ -- same as CASE, but there's an exact value (not constructor) in reg

36− | CONSTCASE Reg [(Const, [BC])] (Maybe [BC])

64+ | CONSTCASE Reg [(Const, [BC])] (Maybe [BC])

65+

66+ -- just call a function, passing MYOLDBASE (see below) to it

37− | CALL Name

67+ | CALL Name

68+

69+ -- same, perhaps exists just for TCO

38− | TAILCALL Name

70+ | TAILCALL Name

71+

72+ -- set reg to (apply string args), FLang argument is the language to

73+ -- be called. FType is the foreign language type, which may be used to

74+ -- control marshaling.

39− | FOREIGNCALL Reg FLang FType String [(FType, Reg)]

75+ | FOREIGNCALL Reg FLang FType String [(FType, Reg)]

40− | SLIDE Int -- move this number from TOP to BASE

76+

77+ -- move this number of elements from TOP to BASE

78+ | SLIDE Int

79+

80+ -- set BASE = OLDBASE

41− | REBASE -- set BASE = OLDBASE

81+ | REBASE

42− | RESERVE Int -- reserve n more stack items

82+

43− -- (i.e. check there's space, grow if necessary)

83+ -- reserve n more stack items (i.e. check there's space, grow if

84+ -- necessary)

85+ | RESERVE Int

86+

44− | ADDTOP Int -- move the top of stack up

87+ -- move the top of stack up

88+ | ADDTOP Int

89+

90+ -- set TOP = BASE + n

45− | TOPBASE Int -- set TOP = BASE + n

91+ | TOPBASE Int

92+

93+ -- set BASE = TOP + n

46− | BASETOP Int -- set BASE = TOP + n

94+ | BASETOP Int

95+

96+ -- set MYOLDBASE = BASE, where MYOLDBASE is a function-local

97+ -- variable, set to OLDBASE by default, and passed on function

98+ -- call to called functions as their OLDBASE

47− | STOREOLD -- set OLDBASE = BASE

99+ | STOREOLD

100+

101+ -- reg = apply primitive_function args

48− | OP Reg PrimFn [Reg]

102+ | OP Reg PrimFn [Reg]

103+

104+ -- clear reg

49− | NULL Reg -- clear reg

105+ | NULL Reg

106+

107+ -- throw an error

50− | ERROR String

108+ | ERROR String

51− deriving Show

109+ deriving Show

110

53toBC :: (Name, SDecl) -> (Name, [BC])

111toBC :: (Name, SDecl) -> (Name, [BC])

54toBC (n, SFun n' args locs exp)

112toBC (n, SFun n' args locs exp)

src/Idris/Completion.hs+4

@@ -168,6 +168,10 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo

168 completeArg ColourArg = completeColour (prev, next)

169 completeArg NoArg = noCompletion (prev, next)

170 completeArg ConsoleWidthArg = completeConsoleWidth (prev, next)

171+ completeArg DeclArg = completeExpr [] (prev, next)

172+ completeArg (ManyArgs a) = completeArg a

173+ completeArg (OptionalArg a) = completeArg a

174+ completeArg (SeqArgs a b) = completeArg a

171 completeCmdName = return $ ("", completeWith commands cmd)

175 completeCmdName = return $ ("", completeWith commands cmd)

172

176

173-- | Complete REPL commands and defined identifiers

177-- | Complete REPL commands and defined identifiers

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 sh 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

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

652 | PVar { binderTy :: !b }

654 | PVar { binderTy :: !b }

653 -- ^ A pattern variable

655 -- ^ A pattern variable

654 | PVTy { binderTy :: !b }

656 | PVTy { binderTy :: !b }

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

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

656{-!

658{-!

657deriving instance Binary Binder

659deriving instance Binary Binder

658deriving instance NFData Binder

660deriving 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)