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

git.iko.soy/Idris-dev

Fixed accessibility bug; added some library functions

commit201ade97f9cc691e400741520a225a1fd65e9207 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 8 Jan 2012, 13:36 (15 years ago) parent0b9cab2

7 files changed+29−4

compare with master

unifiedsplit

lib/Makefile+1−1 lib/prelude.idr+14−1 lib/prelude/list.idr+8 src/Core/Evaluate.hs+1−1 src/Core/Typecheck.hs+1−1 src/Idris/IBC.hs+1 src/Idris/Parser.hs+3

lib/Makefile+1−1

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

55recheck: clean check

7−install: recheck

7+install: check

88 mkdir -p $(TARGET)/prelude

99 mkdir -p $(TARGET)/network

1010 install *.ibc $(TARGET)

lib/prelude.idr+14−1

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

1313import prelude.strings

1414import prelude.char

1515

16+%access public

17+

1618-- Show and instances

1719

1820class Show a where

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

164166ceiling : Float -> Float

165167ceiling x = prim__floatCeil x

166168

167−-- Ranges

169+---- Ranges

168170

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

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

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

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

176178 = count start (next - start) end

177179

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+

178191---- some basic io

179192

180193putStr : String -> IO ()

lib/prelude/list.idr+8

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

4747 Nothing => mapMaybe f xs

4848 Just v => v :: mapMaybe f xs

4949

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+

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

5159filter pred [] = []

5260filter 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

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

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

447447 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" ++

449449 show ns ++ " " ++ show sc

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

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

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

5353 chk env (Var n)

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

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

5757 chk env (RApp f a)

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

src/Idris/IBC.hs+1

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

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

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

184184 do i <- getIState

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

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

186187 ds

187188

src/Idris/Parser.hs+3

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

8181 file_in <- liftIO $ readFile f

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

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

84+ i <- getIState

85+ putIState (i { default_access = Hidden })

8486 mapM_ loadModule modules

8587 clearIBC -- start a new .ibc file

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

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

104106 when ok $

105107 idrisCatch (do writeIBC f ibc; clearIBC)

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

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

107110 return ()

108111 where

109112 namespaces [] ds = ds