3541c70 · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -6,11 +6,13 @@ User visible changes:

6* backtick notation added: x `foo` y ==> foo x y

7* case expressions allowed in type signatures

8* Library extensions in prelude.vect and prelude.algebra

9+* malloc/trace_malloc added to builtins.idr

9

10

10Internal changes:

11Internal changes:

11

12

12* Some type class resolution fixes

13* Some type class resolution fixes

13* Several minor bug fixes

14* Several minor bug fixes

15+* Performance improvements in resolving overloading and type classes

14

16

15New in 0.9.1:

17New in 0.9.1:

16-------------

18-------------

idris.cabal+2−2

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

1Name: idris

2−Version: 0.9.2

2+Version: 0.9.3

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -67,7 +67,7 @@ Executable idris

67

68 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,

69 containers, process, transformers, filepath, directory,

70− binary, bytestring, epic>=0.9.2.1

70+ binary, bytestring, epic>=0.9.3

71

72 Extensions: MultiParamTypeClasses, FunctionalDependencies,

73 FlexibleInstances, TemplateHaskell

lib/builtins.idr+7−1

@@ -21,6 +21,12 @@ sym refl = refl

21lazy : a -> a

22lazy x = x -- compiled specially

23

24+malloc : Int -> a -> a

25+malloc size x = x -- compiled specially

26+

27+trace_malloc : a -> a

28+trace_malloc x = x -- compiled specially

29+

24believe_me : a -> b -- compiled specially as id, use with care!

30believe_me : a -> b -- compiled specially as id, use with care!

25believe_me x = prim__believe_me _ _ x

31believe_me x = prim__believe_me _ _ x

26

32

@@ -186,7 +192,7 @@ instance (Ord a, Ord b) => Ord (a, b) where

186 else compare xr yr

192 else compare xr yr

187

193

188

194

189−class Eq a => Num a where

195+class Num a where

190 (+) : a -> a -> a

196 (+) : a -> a -> a

191 (-) : a -> a -> a

197 (-) : a -> a -> a

192 (*) : a -> a -> a

198 (*) : a -> a -> a

samples/interp.idr+3−7

@@ -48,19 +48,15 @@ using (G : Vect Ty n)

48 (==) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool

49 (==) = Op (==)

50

51− -- Some dummy instances for Num overloading

51+ (<) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool

52− instance Eq (Expr G TyInt) where

52+ (<) = Op (<)

53− (==) x y = False

54−

55− instance Ord (Expr G TyInt) where

56− compare x y = EQ

57

53

58 instance Num (Expr G TyInt) where

54 instance Num (Expr G TyInt) where

59 (+) x y = Op (+) x y

55 (+) x y = Op (+) x y

60 (-) x y = Op (-) x y

56 (-) x y = Op (-) x y

61 (*) x y = Op (*) x y

57 (*) x y = Op (*) x y

62

58

63− abs x = If (Op (<) x (Val 0)) (Op (-) 0 x) x

59+ abs x = IF (x < 0) THEN (-x) ELSE x

64

60

65 fromInteger = Val . fromInteger

61 fromInteger = Val . fromInteger

66

62

src/Core/Evaluate.hs+1

@@ -80,6 +80,7 @@ instance Show (a -> b) where

80threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking

81 -- in fact it's a maximum recursion depth

82

83+-- Normalise fully type checked terms (so, assume all names/let bindings resolved)

83normaliseC :: Context -> Env -> TT Name -> TT Name

84normaliseC :: Context -> Env -> TT Name -> TT Name

84normaliseC ctxt env t

85normaliseC ctxt env t

85 = evalState (do val <- eval ctxt threshold [] env t []

86 = evalState (do val <- eval ctxt threshold [] env t []

src/Idris/Compiler.hs+7

@@ -102,6 +102,13 @@ instance ToEpic (TT Name) where

102 = do v' <- epic' env v

103 k' <- epic' env k

104 return (k' @@ (effect_ v'))

105+ | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm

106+ = do size' <- epic' env size

107+ t' <- epic' env t

108+ return $ malloc_ size' t'

109+ | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm

110+ = do t' <- epic' env t

111+ return $ mallocTrace_ t'

105 | (P (DCon t a) n _, args) <- unApply tm

112 | (P (DCon t a) n _, args) <- unApply tm

106 = epicCon env t a n args

113 = epicCon env t a n args

107 epic' env (P (DCon t a) n _) = return $ con_ t

114 epic' env (P (DCon t a) n _) = return $ con_ t

src/Idris/ElabDecls.hs+6−5

@@ -207,11 +207,12 @@ elabCon info syn tn (n, t_in, fc)

207 mapM_ (elabCaseBlock info) is

208 ctxt <- getContext

209 (cty, _) <- recheckC fc [] t'

210+ let cty' = normaliseC ctxt [] cty

210− tyIs cty

211+ tyIs cty'

211− logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

212+ logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

212 addIBC (IBCDef n)

213 addIBC (IBCDef n)

213− forceArgs n cty

214+ forceArgs n cty'

214− return (n, cty)

215+ return (n, cty')

215 where

216 where

216 tyIs (Bind n b sc) = tyIs sc

217 tyIs (Bind n b sc) = tyIs sc

217 tyIs t | (P _ n' _, _) <- unApply t

218 tyIs t | (P _ n' _, _) <- unApply t

@@ -801,6 +802,7 @@ decorateid decorate (PClauses f o n cs)

801 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

802 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

802 dappname t = t

803 dappname t = t

803

804

805+

804pbinds (Bind n (PVar t) sc) = do attack; patbind n

806pbinds (Bind n (PVar t) sc) = do attack; patbind n

805 pbinds sc

807 pbinds sc

806pbinds tm = return ()

808pbinds tm = return ()

@@ -862,7 +864,6 @@ elabDecl' info (PDSL n dsl)

862 = do i <- get

864 = do i <- get

863 put (i { idris_dsls = addDef n dsl (idris_dsls i) })

865 put (i { idris_dsls = addDef n dsl (idris_dsls i) })

864 addIBC (IBCDSL n)

866 addIBC (IBCDSL n)

865−

866elabDecl' info (PDirective i) = i

867elabDecl' info (PDirective i) = i

867

868

868elabCaseBlock info d@(PClauses f o n ps)

869elabCaseBlock info d@(PClauses f o n ps)

src/Idris/Parser.hs+2−2

@@ -1261,8 +1261,8 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

1261 <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'

1262 return [PDirective (do i <- getIState

1263 putIState (i { default_access = acc }))])

1264− <|> do lchar '%'; reserved "logging"; i <- natural;

1264+ <|> try (do lchar '%'; reserved "logging"; i <- natural;

1265− return [PDirective (setLogLevel (fromInteger i))]

1265+ return [PDirective (setLogLevel (fromInteger i))])

1266

1267pTactic :: SyntaxInfo -> IParser PTactic

1268pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

src/Idris/REPL.hs+1−1

@@ -188,7 +188,7 @@ process fn (TotCheck n) = do i <- get

188 [t] -> iputStrLn (showTotal t i)

189 _ -> return ()

190process fn (Info n) = do i <- get

191− let oi = lookupCtxt Nothing n (idris_optimisation i)

191+ let oi = lookupCtxtName Nothing n (idris_optimisation i)

192 when (not (null oi)) $ iputStrLn (show oi)

193 let si = lookupCtxt Nothing n (idris_statics i)

194 when (not (null si)) $ iputStrLn (show si)

tutorial/examples/interp.idr+1−1

@@ -58,7 +58,7 @@ using (G : Vect Ty n)

58testFac : Int

59testFac = interp [] fact 4

60

61−unitTestFac : so (interp [] fact 4 == 25)

61+unitTestFac : so (interp [] fact 4 == 24)

62unitTestFac = oh

63

64main : IO ()