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

git.iko.soy/Idris-dev

Merge remote-tracking branch 'upstream/master'

commit3541c70e306bd527830b893079f2dd226611565e authorDominic Mulligan <dominic.p.mulligan@googlemail.com> dateThu 1 Mar 2012, 14:25 (15 years ago) parent637f3bf dca8f9f

10 files changed+32−19

compare with master

unifiedsplit

CHANGELOG+2 idris.cabal+2−2 lib/builtins.idr+7−1 samples/interp.idr+3−7 src/Core/Evaluate.hs+1 src/Idris/Compiler.hs+7 src/Idris/ElabDecls.hs+6−5 src/Idris/Parser.hs+2−2 src/Idris/REPL.hs+1−1 tutorial/examples/interp.idr+1−1

CHANGELOG+2

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

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

77* case expressions allowed in type signatures

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

9+* malloc/trace_malloc added to builtins.idr

910

1011Internal changes:

1112

1213* Some type class resolution fixes

1314* Several minor bug fixes

15+* Performance improvements in resolving overloading and type classes

1416

1517New in 0.9.1:

1618-------------

idris.cabal+2−2

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

11Name: idris

2−Version: 0.9.2

2+Version: 0.9.3

33License: BSD3

44License-file: LICENSE

55Author: Edwin Brady

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

6767

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

6969 containers, process, transformers, filepath, directory,

70− binary, bytestring, epic>=0.9.2.1

70+ binary, bytestring, epic>=0.9.3

7171

7272 Extensions: MultiParamTypeClasses, FunctionalDependencies,

7373 FlexibleInstances, TemplateHaskell

lib/builtins.idr+7−1

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

2121lazy : a -> a

2222lazy x = x -- compiled specially

2323

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+

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

2531believe_me x = prim__believe_me _ _ x

2632

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

186192 else compare xr yr

187193

188194

189−class Eq a => Num a where

195+class Num a where

190196 (+) : a -> a -> a

191197 (-) : a -> a -> a

192198 (*) : a -> a -> a

samples/interp.idr+3−7

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

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

4949 (==) = Op (==)

5050

51− -- Some dummy instances for Num overloading

52− instance Eq (Expr G TyInt) where

53− (==) x y = False

54−

55− instance Ord (Expr G TyInt) where

56− compare x y = EQ

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

52+ (<) = Op (<)

5753

5854 instance Num (Expr G TyInt) where

5955 (+) x y = Op (+) x y

6056 (-) x y = Op (-) x y

6157 (*) x y = Op (*) x y

6258

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

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

6460

6561 fromInteger = Val . fromInteger

6662

src/Core/Evaluate.hs+1

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

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

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

8282

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

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

8485normaliseC ctxt env t

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

src/Idris/Compiler.hs+7

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

102102 = do v' <- epic' env v

103103 k' <- epic' env k

104104 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'

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

106113 = epicCon env t a n args

107114 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)

207207 mapM_ (elabCaseBlock info) is

208208 ctxt <- getContext

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

210− tyIs cty

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

210+ let cty' = normaliseC ctxt [] cty

211+ tyIs cty'

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

212213 addIBC (IBCDef n)

213− forceArgs n cty

214− return (n, cty)

214+ forceArgs n cty'

215+ return (n, cty')

215216 where

216217 tyIs (Bind n b sc) = tyIs sc

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

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

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

802803 dappname t = t

803804

805+

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

805807 pbinds sc

806808pbinds tm = return ()

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

862864 = do i <- get

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

864866 addIBC (IBCDSL n)

865−

866867elabDecl' info (PDirective i) = i

867868

868869elabCaseBlock 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;

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

12621262 return [PDirective (do i <- getIState

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

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

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

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

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

12661266

12671267pTactic :: SyntaxInfo -> IParser PTactic

12681268pTactic 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

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

189189 _ -> return ()

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

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

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

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

193193 let si = lookupCtxt Nothing n (idris_statics i)

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

tutorial/examples/interp.idr+1−1

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

5858testFac : Int

5959testFac = interp [] fact 4

6060

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

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

6262unitTestFac = oh

6363

6464main : IO ()