201ade9 · Idris-dev · git.iko.soy

lib/Makefile+1−1

compare with master

unifiedsplit

@@ -4,7 +4,7 @@ check: .PHONY

4

5recheck: clean check

6

7−install: recheck

7+install: check

8 mkdir -p $(TARGET)/prelude

9 mkdir -p $(TARGET)/network

10 install *.ibc $(TARGET)

lib/prelude.idr+14−1

@@ -13,6 +13,8 @@ import prelude.vect

13import prelude.strings

14import prelude.char

15

16+%access public

17+

16-- Show and instances

18-- Show and instances

17

19

18class Show a where

20class Show a where

@@ -164,7 +166,7 @@ floor x = prim__floatFloor x

164ceiling : Float -> Float

166ceiling : Float -> Float

165ceiling x = prim__floatCeil x

167ceiling x = prim__floatCeil x

166

168

167−-- Ranges

169+---- Ranges

168

170

169count : Num a => a -> a -> a -> List a

171count : Num a => a -> a -> a -> List a

170count a inc b = if (a <= b) then (a :: count (a + inc) inc b)

172count a inc b = if (a <= b) then (a :: count (a + inc) inc b)

@@ -175,6 +177,17 @@ syntax "[" [start] ".." [end] "]"

175syntax "[" [start] "," [next] ".." [end] "]"

177syntax "[" [start] "," [next] ".." [end] "]"

176 = count start (next - start) end

178 = count start (next - start) end

177

179

180+---- More utilities

181+

182+flip : (a -> b -> c) -> b -> a -> c

183+flip f x y = f y x

184+

185+sum : Num a => List a -> a

186+sum = foldl (+) 0

187+

188+prod : Num a => List a -> a

189+prod = foldl (*) 1

190+

178---- some basic io

191---- some basic io

179

192

180putStr : String -> IO ()

193putStr : String -> IO ()

lib/prelude/list.idr+8

@@ -47,6 +47,14 @@ mapMaybe f (x :: xs) = case f x of

47 Nothing => mapMaybe f xs

48 Just v => v :: mapMaybe f xs

49

50+foldl : (a -> b -> a) -> a -> List b -> a

51+foldl f a [] = a

52+foldl f a (x :: xs) = foldl f (f a x) xs

53+

54+foldr : (a -> b -> b) -> b -> List a -> b

55+foldr f b [] = b

56+foldr f b (x :: xs) = f x (foldr f b xs)

57+

50filter : (y -> Bool) -> List y -> List y

58filter : (y -> Bool) -> List y -> List y

51filter pred [] = []

59filter pred [] = []

52filter pred (x :: xs) = if (pred x) then (x :: filter pred xs)

60filter pred (x :: xs) = if (pred x) then (x :: filter pred xs)

src/Core/Evaluate.hs+1−1

@@ -445,7 +445,7 @@ instance Show Def where

445 show (Function ty tm) = "Function: " ++ show (ty, tm)

446 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

447 show (Operator ty _ _) = "Operator: " ++ show ty

448− show (CaseOp _ ty ps ns sc) = "Case: " ++ show ps ++ "\n" ++

448+ show (CaseOp _ ty ps ns sc) = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

449 show ns ++ " " ++ show sc

450-- We need this for serialising Def. Fortunately, it never gets used because

451-- we'll never serialise a primitive operator

src/Core/Typecheck.hs+1−1

@@ -52,7 +52,7 @@ check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

52check' holes ctxt env top = chk env top where

53 chk env (Var n)

54 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

55− | [P nt n' ty] <- lookupP Nothing n ctxt = return (P nt n' ty, ty)

55+ | (P nt n' ty : _) <- lookupP Nothing n ctxt = return (P nt n' ty, ty)

56 | otherwise = do fail $ "No such variable " ++ show n ++ " in " ++ show (map fst env)

57 chk env (RApp f a)

58 = do (fv, fty) <- chk env f

src/Idris/IBC.hs+1

@@ -182,6 +182,7 @@ pHdrs hs = mapM_ addHdr hs

182pDefs :: [(Name, Def)] -> Idris ()

183pDefs ds = mapM_ (\ (n, d) ->

184 do i <- getIState

185+ logLvl 5 $ "Added " ++ show (n, d)

185 putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))

186 putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))

186 ds

187 ds

187

188

src/Idris/Parser.hs+3

@@ -81,6 +81,8 @@ loadSource lidr f

81 file_in <- liftIO $ readFile f

82 file <- if lidr then tclift $ unlit f file_in else return file_in

83 (mname, modules, rest, pos) <- parseImports f file

84+ i <- getIState

85+ putIState (i { default_access = Hidden })

84 mapM_ loadModule modules

86 mapM_ loadModule modules

85 clearIBC -- start a new .ibc file

87 clearIBC -- start a new .ibc file

86 mapM_ (\m -> addIBC (IBCImport m)) modules

88 mapM_ (\m -> addIBC (IBCImport m)) modules

@@ -104,6 +106,7 @@ loadSource lidr f

104 when ok $

106 when ok $

105 idrisCatch (do writeIBC f ibc; clearIBC)

107 idrisCatch (do writeIBC f ibc; clearIBC)

106 (\c -> return ()) -- failure is harmless

108 (\c -> return ()) -- failure is harmless

109+ putIState (i { hide_list = [] })

107 return ()

110 return ()

108 where

111 where

109 namespaces [] ds = ds

112 namespaces [] ds = ds