b1a9e75 · Idris-dev · git.iko.soy

.gitignore+4

@@ -3,6 +3,9 @@ cabal-dev/

33*.ibc

44*.o

55*.a

6+*.so

7+*.dll

8+*.dylib

69*.swp

710*~

811custom.mk

@@ -11,3 +14,4 @@ test/test???/output

1114test/reg???/output

1215test/test???/*.exe

1316test/reg???/*.exe

17+

CHANGELOG+2

@@ -9,10 +9,12 @@ User visible changes:

99* Tab completion in REPL

1010* Dynamic loading of C libraries in the interpreter

1111* Testing IO actions at the REPL with :x command

12+* Improve rendering of :t

1213* Fixed some INTERNAL ERROR messages

1314

1415Internal changes:

1516

17+* Fix non-linear pattern checking

1618* Improved name disambiguation

1719* More flexible unification and elaboration of lambdas

1820* Various unification and totality checking bug fixes

Makefile+2−2

@@ -17,8 +17,8 @@ test:

1717 make -C test

1818

1919relib:

20− make -C lib IDRIS=../dist/build/idris/idris clean

21− make -C effects IDRIS=../dist/build/idris/idris clean

20+ make -C lib IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts clean

21+ make -C effects IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts DIST=../dist/build clean

2222 $(CABAL) install $(CABALFLAGS)

2323

2424linecount:

Setup.hs+6−3

@@ -28,8 +28,11 @@ mvn verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "mv

2828(<//>) = (Px.</>)

2929idrisCmd local = Px.joinPath $ splitDirectories $

3030 ".." <//> buildDir local <//> "idris" <//> "idris"

31+rtsDir local = Px.joinPath $ splitDirectories $

32+ ".." <//> buildDir local <//> "rts" <//> "libidris_rts"

3133#else

3234idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"

35+rtsDir local = ".." </> buildDir local </> "rts" </> "libidris_rts"

3336#endif

3437

3538cleanStdLib verbosity

@@ -103,9 +106,9 @@ checkStdLib local withoutEffects verbosity

103106 ]

104107 unless withoutEffects $

105108 make verbosity

106− [ "-C", "effects", "check"

107− , "IDRIS=" ++ icmd

108− ]

109+ [ "-C", "effects", "check"

110+ , "IDRIS=" ++ icmd

111+ ]

109112 make verbosity

110113 [ "-C", "rts", "check"

111114 , "IDRIS=" ++ icmd

config.mk+26

@@ -7,3 +7,29 @@ CABAL :=cabal

77## Disable building of Effects

88#CABALFLAGS :=-f NoEffects

99

10+

11+MACHINE := $(shell $(CC) -dumpmachine)

12+ifneq (, $(findstring darwin, $(MACHINE)))

13+ OS :=darwin

14+else

15+ifneq (, $(findstring cygwin, $(MACHINE)))

16+ OS :=windows

17+else

18+ifneq (, $(findstring mingw, $(MACHINE)))

19+ OS :=windows

20+else

21+ OS :=unix

22+endif

23+endif

24+endif

25+

26+ifeq ($(OS),darwin)

27+ SHLIB_SUFFIX :=.dylib

28+else

29+ifeq ($(OS),windows)

30+ SHLIB_SUFFIX :=.DLL

31+else

32+ SHLIB_SUFFIX :=.so

33+endif

34+endif

35+

contribs/lib/SQLite3/Makefile+1−1

@@ -3,7 +3,7 @@

33

44.PHONY: all

55

6−sqltest : testunit.idr sqlite3.idr sqlite3api.o

6+sqltest : testunit.idr Sqlite3.idr sqlite3api.o

77 idris testunit.idr -o sqltest

88

99sqlite3api.o : sqlite3api.c

contribs/lib/SQLite3/Sqlexpr.idrnew file+278

@@ -0,0 +1,278 @@

1+module Sqlexpr

2+import Prelude.List

3+

4+-----------------------------------------------------------------------------

5+-- |

6+-- Module : sqlexpr

7+-- Copyright : (c) The University of St Andrews, 2012

8+--

9+-- Implementations for SQLite query data type.

10+--

11+-----------------------------------------------------------------------------

12+

13+

14+-----------------------------------------------------------

15+-- | SQL data type

16+-----------------------------------------------------------

17+

18+data Value = VInt Int

19+ | VStr String

20+ | VFloat Float

21+ | VCol String

22+ | VNULL

23+

24+--Perhaps could extend this by adding

25+-- a dot operator to allow mapping

26+-- between table and column and

27+-- comparing different table columns.

28+

29+data Cond = Equals Value Value

30+ | MkGT Value Value

31+ | MkGTE Value Value

32+ | MkLT Value Value

33+ | MkLTE Value Value

34+ | MkNULL Value

35+

36+data SelVar = Cols (List String)

37+ | ALL

38+

39+data ColType = CInt String -- parsed as string "int"

40+ | Varchar String

41+

42+

43+

44+mutual

45+ data Clause = MkCond Cond

46+ | AND Clause Clause

47+ | OR Clause Clause

48+ | Empty

49+ | MkSQL SQL

50+

51+ data condClause = SET Clause

52+ | WHERE condClause Clause

53+

54+ data Constr = NOTNULL

55+ | UNIQUE Constr

56+ | None

57+ | PRIMARYKEY

58+ | FOREIGNKEY

59+ | CHECK

60+ | DEFAULT

61+

62+

63+ data SQL = SELECT SelVar SQL Clause

64+ | TBL (List String)

65+ | INSERT SQL (List Value)

66+ | INSERTC SQL (List Value) (List Value)

67+ | UPDATE SQL condClause

68+ | CREATE SQL (List (Value, ColType , Constr))

69+

70+-- remember to remove these funcs later

71+-- foldr1 : (a -> a -> a) -> List a -> a

72+-- foldr1 f [x] = x

73+-- foldr1 f (x::xs) = f x (foldr1 f xs)

74+

75+

76+-- unwords' : List (List Char) -> List Char

77+-- unwords' [] = []

78+-- unwords' ws = (foldr1 addSpace ws)

79+-- where

80+-- addSpace : List Char -> List Char -> List Char

81+-- addSpace w s = w ++ (' ' :: s)

82+--

83+--

84+-- unwords : List String -> String

85+-- unwords = pack . unwords' . map unpack

86+

87+-----------------------------------------------------------

88+-- | This function replaces values with question mark

89+-- following by an index number. It then puts the value

90+-- replaced, in the list.

91+-----------------------------------------------------------

92+

93+valString : List (Maybe (Int, Value)) -> Value -> (String, List (Maybe (Int, Value)))

94+valString xs (VInt x) = ("?" ++ show (cast (length xs) + 1), xs ++ [Just (cast ((length xs) + 1), (VInt x))])

95+valString xs (VStr x) = ("?" ++ show (cast (length xs) + 1), xs ++ [Just (cast ((length xs) + 1), (VStr x))])

96+valString xs (VFloat x) = ("?" ++ show (cast (length xs) + 1), xs ++ [Just (cast ((length xs) + 1), (VFloat x))])

97+valString xs (VCol n) = (n, xs)

98+

99+-----------------------------------------------------------

100+-- | This function calls valString on a list of Values

101+-- and separates the values by commas.

102+-----------------------------------------------------------

103+

104+listVal : List (Maybe (Int, Value)) -> List Value -> (String, List (Maybe (Int, Value)))

105+listVal xs [] = ("", xs)

106+listVal xs (v::vs) = let (str, newxs) = (valString xs v) in

107+ let (str', newxs') = listVal newxs vs in

108+ (unwords (intersperse "," (words (str) ++ words (str'))), newxs')

109+

110+-----------------------------------------------------------

111+-- | Parses the type of column to be created.

112+-----------------------------------------------------------

113+

114+getColType : List (Maybe (Int, Value)) -> ColType -> (String, List (Maybe (Int, Value)))

115+getColType xs (CInt x) = ("int", xs)

116+getColType xs (Varchar str) = ("varchar(255)", xs)

117+

118+-----------------------------------------------------------

119+-- | CREATE Constraints

120+-----------------------------------------------------------

121+

122+getConstr : List (Maybe (Int, Value)) -> Constr -> (String, List (Maybe (Int, Value)))

123+getConstr xs (NOTNULL) = ("NOT NULL", xs)

124+getConstr xs (UNIQUE constr) = ("NOT NULL UNIQUE", xs)

125+getConstr xs (PRIMARYKEY) = ("PRIMARY KEY", xs)

126+getConstr xs (FOREIGNKEY) = ("FOREIGN KEY", xs)

127+getConstr xs (CHECK) = ("CHECK", xs)

128+getConstr xs (DEFAULT) = ("DEFAULT", xs)

129+getConstr xs (None) = ("", xs)

130+

131+putBrackets : String -> String

132+putBrackets str = "(" ++ str ++ ")"

133+

134+-----------------------------------------------------------

135+-- | Used to detect a complex type in a nested SQLite query

136+-- This function is used for bracketing the nested queries.

137+-----------------------------------------------------------

138+complexType : SQL -> Bool

139+complexType (TBL tbl) = False

140+complexType (SELECT vars sql c) = True

141+

142+-----------------------------------------------------------

143+-- | Used in CREATE

144+-----------------------------------------------------------

145+

146+listValType : List (Maybe (Int, Value)) -> List (Value, ColType , Constr) -> (String, List (Maybe (Int, Value)))

147+listValType xs [] = ("", xs)

148+listValType xs ((val, types, constr) :: vs) =

149+ let (str , newxs) = valString xs val in

150+ let (str' , newxs') = getColType newxs types in

151+ let (str'', newxs'') = getConstr newxs' constr in

152+ let (finalstr, finalxs) = listValType newxs'' vs in

153+ (unwords (intersperse " " (words str ++ words str' ++ words str'' ++ words finalstr)) , finalxs)

154+

155+

156+-----------------------------------------------------------

157+-- | Evaluates a conditional WHERE clause

158+-----------------------------------------------------------

159+

160+evalCond : List (Maybe (Int, Value)) -> Cond -> (String, List (Maybe (Int, Value)))

161+evalCond xs (Equals val1 val2) = let (restring , newxs ) = valString xs val1 in

162+ let (restring2, newxs') = valString newxs val2 in

163+ (restring ++ " = " ++ restring2, newxs')

164+

165+evalCond xs (MkGT val1 val2) = let (restring , newxs ) = valString xs val1 in

166+ let (restring2, newxs') = valString newxs val2 in

167+ (restring ++ " > " ++ restring2, newxs')

168+

169+evalCond xs (MkGTE val1 val2) = let (restring , newxs ) = valString xs val1 in

170+ let (restring2, newxs') = valString newxs val2 in

171+ (restring ++ " >= " ++ restring2, newxs')

172+

173+evalCond xs (MkLT val1 val2) = let (restring , newxs ) = valString xs val1 in

174+ let (restring2, newxs') = valString newxs val2 in

175+ (restring ++ " < " ++ restring2, newxs')

176+

177+evalCond xs (MkLTE val1 val2) = let (restring , newxs ) = valString xs val1 in

178+ let (restring2, newxs') = valString newxs val2 in

179+ (restring ++ " =< " ++ restring2, newxs')

180+

181+evalCond xs (MkNULL val) = let (restring , newxs ) = valString xs val in

182+ (restring ++ " IS NULL " , newxs)

183+

184+

185+-----------------------------------------------------------

186+-- | Evaluates clauses

187+-- Supports WHERE Clause

188+-- WHERE Clause And Another-Clause

189+-- WHERE Clause Or Another-Clause

190+-----------------------------------------------------------

191+clauseString : List (Maybe (Int, Value)) -> Clause -> (String, List (Maybe (Int, Value)))

192+

193+clauseString xs (Empty) = ("" , []) -- No condition

194+clauseString xs (MkCond cond') = let (condstr, newxs) = evalCond xs cond' in

195+ (condstr , newxs)

196+

197+clauseString xs (AND c1 c2) = let (clausestr, newxs) = clauseString xs c1 in

198+ let (clausestr2, newxs') = clauseString newxs c2 in

199+ (clausestr ++ " AND " ++ clausestr2 , newxs')

200+

201+clauseString xs (OR c1 c2) = let (clausestr, newxs) = clauseString xs c1 in

202+ let (clausestr2, newxs') = clauseString newxs c2 in

203+ (clausestr ++ " OR " ++ clausestr2 , newxs')

204+

205+

206+-----------------------------------------------------------

207+-- | Evaluates conditional clauses.

208+-----------------------------------------------------------

209+

210+condClauseStr : List (Maybe (Int, Value)) -> condClause -> (String, List (Maybe (Int, Value)))

211+condClauseStr xs (SET setcl) = let (condstr, newxs) = clauseString xs setcl in

212+ (" SET " ++ condstr, newxs)

213+

214+condClauseStr xs (WHERE setcl1 setcl2) = let (condstr, newxs) = condClauseStr xs setcl1 in

215+ let (condstr', newxs') = clauseString newxs setcl2 in

216+ ( condstr ++ " WHERE " ++ condstr', newxs')

217+

218+

219+-----------------------------------------------------------

220+-- | Evaluates queries by calling the other functions

221+-- on each part of the query

222+-----------------------------------------------------------

223+evalSQL : List (Maybe (Int, Value)) -> SQL -> (String, List (Maybe (Int, Value)))

224+-- SELECT data from tbl1 where num > (SELECT num from tbl1 where num = 24)

225+-- evalSQL [] ((SELECT ALL)(TBL "tbl")(MkSQL ((SELECT ALL) (TBL "tbl")(MkCond (VCol "))))

226+-- NTBF

227+--clauseString xs (MkSQL sql) = (evalSQL xs sql)

228+

229+-- Separate list of tables

230+-- For complex type, return list returned by evalSQL

231+-- And add brackets

232+evalSQL xs (TBL tbl) = (unwords (intersperse "," ( tbl)), xs)

233+evalSQL xs (SELECT vars sql' c) =

234+ let (sqlstring, newxs) = evalSQL xs sql' in

235+ let (csstring, newxs') = clauseString newxs c in

236+ case c of

237+ Empty => case vars of

238+ ALL => if complexType sql'

239+ then ("SELECT " ++ "*" ++ " FROM " ++

240+ putBrackets sqlstring ++ csstring, newxs)

241+ else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring ++

242+ csstring, newxs')

243+ Cols selvar => if complexType sql'

244+ then ("SELECT " ++ unwords selvar ++

245+ " FROM " ++ putBrackets sqlstring ++ csstring, newxs)

246+ else ("SELECT " ++ unwords selvar ++ " FROM " ++ sqlstring ++

247+ csstring, newxs')

248+ _ => case vars of

249+ ALL => if complexType sql'

250+ then ("SELECT " ++ "*" ++ " FROM " ++

251+ " WHERE " ++ csstring, newxs)

252+ else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring

253+ ++ " WHERE " ++ csstring, newxs')

254+ Cols selvar => if complexType sql'

255+ then ("SELECT " ++ (unwords selvar) ++ " FROM " ++

256+ putBrackets sqlstring ++ " WHERE " ++

257+ csstring , newxs)

258+ else ("SELECT " ++ (unwords selvar) ++ " FROM " ++ sqlstring ++

259+ " WHERE " ++ csstring, newxs')

260+

261+

262+evalSQL xs (INSERT sql vals) = let (tblname, newvals) = evalSQL xs sql in

263+ let (str, newxs ) = listVal newvals vals in

264+ ("INSERT INTO " ++ tblname ++ " VALUES (" ++ str ++ ")", newxs)

265+

266+evalSQL xs (INSERTC sql cols vals) = let (tblname, newvals) = evalSQL xs sql in

267+ let (strcol, newcol) = listVal newvals cols in

268+ let (strval, newcolval) = listVal newcol vals in

269+ ("INSERT INTO " ++ tblname ++ "(" ++ strcol ++ ")" ++ "VALUES (" ++ strval ++ ")", newcolval)

270+

271+

272+evalSQL xs (UPDATE sql cl) = let (tblname, newxs) = evalSQL xs sql in

273+ let (csstring, newxs') = condClauseStr newxs cl in

274+ ("UPDATE " ++ tblname ++ csstring, newxs')

275+

276+evalSQL xs (CREATE sql details) = let (sqlstring, newxs) = evalSQL xs sql in

277+ let (csstring, newxs') = listValType newxs details in

278+ ("CREATE TABLE " ++ sqlstring ++ "(" ++ csstring ++ ")", newxs')

contribs/lib/SQLite3/sqlite3.idr → contribs/lib/SQLite3/Sqlite3.idrrenamed+172−155

@@ -22,7 +22,7 @@ data DBVal = DBInt Int

2222 | DBText String

2323 | DBFloat Float

2424 | DBNull

25−

25+

2626-- Database pointer

2727data DBPointer = MkDBPointer Ptr

2828-- Table pointer

@@ -30,16 +30,29 @@ data TBPointer = MkTBPointer Ptr

3030-- Statement pointer

3131data StmtPtr = MkStmtPtr Ptr

3232

33−Table : Set

33+Table : Type

3434Table = List (List DBVal)

3535

3636-- ForMap used in to_list_v1

37−forM : Monad m => List a -> (a -> m b) -> m (List b)

38−forM f xs = mapM xs f

37+forM : Applicative f => List a -> (a -> f b) -> f (List b)

38+forM xs f = (sequence (map f xs))

3939

4040-- Neater error handling done using DB

4141data DB a = MkDB (IO (Either String a))

4242

43+instance Functor DB where

44+ fmap f (MkDB action) = MkDB (do res <- action

45+ return (fmap f res))

46+

47+

48+instance Applicative DB where

49+ pure = MkDB . return . Right

50+ (MkDB f) <$> (MkDB x) = MkDB (do f' <- f

51+ case f' of

52+ Left err => return (Left err)

53+ Right op => x >>= (return . fmap op))

54+

55+

4356instance Monad DB where

4457 (MkDB l) >>= k = MkDB (do c <- l

4558 case c of

@@ -63,14 +76,14 @@ runDB : DB a -> IO a

6376runDB (MkDB f) = do f' <- f

6477 case f' of

6578 Right v => return v

66− Left str => ioError str

67−

79+ Left str => ioError str

80+

6881-----------------------------------------------------------------------------

6982-- | Opens an SQLite database file as specified by the String name argument.

7083-----------------------------------------------------------------------------

71−

84+

7285open_db : String -> DB DBPointer

73−open_db name = do x <- liftIO(mkForeign (FFun "sqlite3_open_idr" [FString] FPtr) name)

86+open_db name = do x <- liftIO (mkForeign (FFun "sqlite3_open_idr" [FString] FPtr) name)

7487 return (MkDBPointer x)

7588

7689-----------------------------------------------------------------------------

@@ -78,38 +91,38 @@ open_db name = do x <- liftIO(mkForeign (FFun "sqlite3_open_idr" [FString] FPtr)

7891-----------------------------------------------------------------------------

7992

8093close_db : DBPointer -> DB Int

81−close_db (MkDBPointer pointer) = liftIO (mkForeign (FFun "sqlite3_close_idr" [FPtr] FInt)pointer)

94+close_db (MkDBPointer pointer) = liftIO (mkForeign (FFun "sqlite3_close_idr" [FPtr] FInt) pointer)

8295

8396-----------------------------------------------------------------------------

8497-- | Wrapper around prepare, step and finalize.

8598-----------------------------------------------------------------------------

86−

99+

87100exec_db : DBPointer -> String -> DB Int

88−exec_db (MkDBPointer pointer) stmt = do

89− x <- liftIO(mkForeign (FFun "sqlite3_exec_idr" [FPtr, FString] FInt)pointer stmt)

101+exec_db (MkDBPointer pointer) stmt = do

102+ x <- liftIO (mkForeign (FFun "sqlite3_exec_idr" [FPtr, FString] FInt) pointer stmt)

90103 if (x == 1)

91− then fail "Could not execute."

92− else return x

104+ then fail "Could not execute."

105+ else return x

93106

94107-----------------------------------------------------------------------------

95108-- | Executes a prepared query. Use of this version is recommended.

96109-----------------------------------------------------------------------------

97110

98111exec_db_v2 : StmtPtr -> DB Int

99−exec_db_v2 (MkStmtPtr pointer) = do

112+exec_db_v2 (MkStmtPtr pointer) = do

100113 x <- liftIO (mkForeign (FFun "exec_db" [FPtr] FInt) pointer)

101114 if (x == 21)

102− then fail "No data returned."

103− else return x

104−

115+ then fail "No data returned."

116+ else return x

117+

105118-----------------------------------------------------------------------------

106119-- | Returns the error stored in the buffer by exec_db function.

107120-- This function can only be used with exec_db and get_table.

108121-- Only these functions store any occured error in the buffer array.

109122-----------------------------------------------------------------------------

110−

123+

111124get_error : DBPointer -> IO String

112−get_error (MkDBPointer pointer) =mkForeign (FFun "sqlite3_get_error" [FPtr] FString)pointer

125+get_error (MkDBPointer pointer) = mkForeign (FFun "sqlite3_get_error" [FPtr] FString) pointer

113126

114127

115128-----------------------------------------------------------------------------

@@ -117,14 +130,14 @@ get_error (MkDBPointer pointer) =mkForeign (FFun "sqlite3_get_error" [FPtr] FStr

117130-- Returns a pointer to a Statement pointer on a successful call.

118131-- Returns a null pointer on a failure.

119132-----------------------------------------------------------------------------

120−

133+

121134prepare_db : DBPointer -> String -> DB StmtPtr

122135prepare_db (MkDBPointer pointer) cmd = do

123− result <- liftIO(mkForeign (FFun "sqlite3_prepare_idr" [FPtr, FString] FPtr)pointer cmd)

124− flag <- liftIO(nullPtr result)

136+ result <- liftIO (mkForeign (FFun "sqlite3_prepare_idr" [FPtr, FString] FPtr) pointer cmd)

137+ flag <- liftIO (nullPtr result)

125138 if flag

126− then fail "Error occured while preparing"

127− else return (MkStmtPtr result)

139+ then fail "Error occured while preparing"

140+ else return (MkStmtPtr result)

128141

129142-----------------------------------------------------------------------------

130143-- | Returns the error stored in the buffer by exec_db function.

@@ -136,81 +149,92 @@ step_db : StmtPtr -> DB Int

136149step_db (MkStmtPtr pointer)= do

137150 x <- liftIO (mkForeign (FFun "sqlite3_step_idr" [FPtr] FInt)pointer)

138151 if ( x == 101)

139− then fail "SQLITE_DONE"

140− else return x

152+ then fail "SQLITE_DONE"

153+ else return x

141154

142155-----------------------------------------------------------------------------

143−-- | Deletes a prepared statement. This function must be called after

156+-- | Deletes a prepared statement. This function must be called after

144157-- prepare function.

145158-----------------------------------------------------------------------------

146159

147160finalize_db : StmtPtr -> DB Int

148−finalize_db (MkStmtPtr pointer) = do

149− x <- liftIO (mkForeign (FFun "sqlite3_finalize_idr" [FPtr] FInt)pointer)

161+finalize_db (MkStmtPtr pointer) = do

162+ x <- liftIO (mkForeign (FFun "sqlite3_finalize_idr" [FPtr] FInt) pointer)

150163 if (x /= 0)

151− then fail "Could not finalize"

152− else return x

164+ then fail "Could not finalize"

165+ else return x

153166

154167-----------------------------------------------------------------------------

155168-- | Resets a prepared statement pointer back to its initial state.

156169-----------------------------------------------------------------------------

157170

158171reset_db : StmtPtr -> DB Int

159−reset_db (MkStmtPtr pointer) = do

160− x <- liftIO(mkForeign (FFun "sqlite3_reset_idr" [FPtr] FInt)pointer)

161− if (x /=0)

162− then fail "Could not reset"

163− else return x

172+reset_db (MkStmtPtr pointer) = do

173+ x <- liftIO (mkForeign (FFun "sqlite3_reset_idr" [FPtr] FInt) pointer)

174+ if (x /= 0)

175+ then fail "Could not reset"

176+ else return x

164177

165178-----------------------------------------------------------------------------

166179-- | These routines obtain column information.

167180-----------------------------------------------------------------------------

168181

169182column_count : DBPointer -> IO (Either String Int)

170−column_count (MkDBPointer pointer) = do

171− x <- mkForeign (FFun "sqlite3_column_count_idr" [FPtr] FInt)pointer

172− if (x == 0 )

173− then return (Left "No Data")

174− else return (Right x)

183+column_count (MkDBPointer pointer) = do

184+ x <- mkForeign (FFun "sqlite3_column_count_idr" [FPtr] FInt) pointer

185+ return $ if (x == 0 )

186+ then Left "No Data"

187+ else (Right x)

175188

176189column_name : DBPointer -> Int -> IO String

177−column_name (MkDBPointer pointer) iCol =mkForeign (FFun "sqlite3_column_name_idr" [FPtr, FInt] FString)pointer iCol

178−

190+column_name (MkDBPointer pointer) iCol =

191+ mkForeign (FFun "sqlite3_column_name_idr" [FPtr, FInt] FString) pointer iCol

192+

179193column_decltype : DBPointer -> Int -> IO String

180−column_decltype (MkDBPointer pointer) iCol =mkForeign (FFun "sqlite3_column_decltype_idr" [FPtr, FInt] FString)pointer iCol

194+column_decltype (MkDBPointer pointer) iCol =

195+ mkForeign (FFun "sqlite3_column_decltype_idr" [FPtr, FInt] FString) pointer iCol

181196

182197

183198column_bytes : DBPointer -> Int -> IO Int

184−column_bytes (MkDBPointer pointer) iCol =mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FInt)pointer iCol

199+column_bytes (MkDBPointer pointer) iCol =

200+ mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FInt) pointer iCol

185201

186202

187203column_blob : DBPointer -> Int -> IO String

188−column_blob (MkDBPointer pointer) iCol =mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FString)pointer iCol

204+column_blob (MkDBPointer pointer) iCol =

205+ mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FString) pointer iCol

189206

190207

191208column_text : DBPointer -> Int -> IO String

192−column_text (MkDBPointer pointer) iCol =mkForeign (FFun "sqlite3_column_text_idr" [FPtr, FInt] FString)pointer iCol

209+column_text (MkDBPointer pointer) iCol =

210+ mkForeign (FFun "sqlite3_column_text_idr" [FPtr, FInt] FString) pointer iCol

193211

194212

195213column_Int : DBPointer -> Int -> IO Int

196−column_Int (MkDBPointer pointer) iCol =mkForeign (FFun "sqlite3_column_int_idr" [FPtr, FInt] FInt)pointer iCol

214+column_Int (MkDBPointer pointer) iCol =

215+ mkForeign (FFun "sqlite3_column_int_idr" [FPtr, FInt] FInt) pointer iCol

197216

198217-----------------------------------------------------------------------------

199218-- | These routines support some of SQLite backup functions.

200219-----------------------------------------------------------------------------

201220

202−backup_init : DBPointer -> String -> DBPointer -> String -> IO DBPointer

203−backup_init (MkDBPointer des_pointer) destName (MkDBPointer src_pointer) srcName = do x <- mkForeign (FFun "sqlite3_backup_init_idr" [FPtr,FString, FPtr, FString] FPtr)des_pointer destName src_pointer srcName

204− return (MkDBPointer x)

221+backup_init : DBPointer -> String -> DBPointer -> String -> IO DBPointer

222+backup_init (MkDBPointer des_pointer) destName (MkDBPointer src_pointer) srcName =

223+ do x <- mkForeign (FFun "sqlite3_backup_init_idr" [FPtr,FString, FPtr, FString] FPtr)

224+ des_pointer destName src_pointer srcName

225+ return (MkDBPointer x)

205226

206227backup_step : DBPointer -> Int -> IO Int

207−backup_step (MkDBPointer pointer) nPage =mkForeign (FFun "sqlite3_backup_step_idr" [FPtr, FInt] FInt)pointer nPage

228+backup_step (MkDBPointer pointer) nPage =

229+ mkForeign (FFun "sqlite3_backup_step_idr" [FPtr, FInt] FInt) pointer nPage

208230

209231backup_finish : DBPointer -> IO Int

210−backup_finish (MkDBPointer pointer) =mkForeign (FFun "sqlite3_backup_finish_idr" [FPtr] FInt)pointer

232+backup_finish (MkDBPointer pointer) =

233+ mkForeign (FFun "sqlite3_backup_finish_idr" [FPtr] FInt) pointer

211234

212235backup_remaining : DBPointer -> IO Int

213−backup_remaining (MkDBPointer pointer) =mkForeign (FFun "sqlite3_backup_remaining_idr" [FPtr] FInt)pointer

236+backup_remaining (MkDBPointer pointer) =

237+ mkForeign (FFun "sqlite3_backup_remaining_idr" [FPtr] FInt) pointer

214238

215239

216240-----------------------------------------------------------------------------

@@ -221,104 +245,98 @@ backup_remaining (MkDBPointer pointer) =mkForeign (FFun "sqlite3_backup_remainin

221245-----------------------------------------------------------------------------

222246

223247get_table : DBPointer -> String -> DB TBPointer

224−get_table (MkDBPointer pointer) name = do

225− x <- liftIO(mkForeign (FFun "sqlite3_get_table_idr" [FPtr, FString] FPtr)pointer name)

226− flag <- liftIO(nullPtr x)

248+get_table (MkDBPointer pointer) name = do

249+ x <- liftIO(mkForeign (FFun "sqlite3_get_table_idr" [FPtr, FString] FPtr) pointer name)

250+ flag <- liftIO (nullPtr x)

227251 if flag

228− then do x <- liftIO(get_error_table pointer) ; fail x

229− else return (MkTBPointer x)

252+ then do x <- liftIO(get_error_table pointer) ; fail x

253+ else return (MkTBPointer x)

230254 where

231255 get_error_table : Ptr-> IO String

232− get_error_table pointer = do x <- mkForeign (FFun "sqlite3_get_error" [FPtr] FString)pointer

256+ get_error_table pointer = do x <- mkForeign (FFun "sqlite3_get_error" [FPtr] FString) pointer

233257 return x

234258

235259

236260free_table : TBPointer -> IO ()

237−free_table (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_free_table_idr" [FPtr] FUnit)pointer

261+free_table (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_free_table_idr" [FPtr] FUnit) pointer

238262 return ()

239−

263+

240264-----------------------------------------------------------------------------

241265-- | This version of these function obtain the row and column number

242266-- from the Table struct. These functions are only used with get_table.

243267-----------------------------------------------------------------------------

244268

245269num_row : TBPointer -> IO Int

246−num_row (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_row" [FPtr] FInt)pointer

247− return (x)

270+num_row (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_row" [FPtr] FInt) pointer

271+ return x

248272

249273num_col : TBPointer -> IO Int

250−num_col (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col" [FPtr] FInt)pointer

251− return (x)

252−

274+num_col (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col" [FPtr] FInt) pointer

275+ return x

276+

253277-----------------------------------------------------------------------------

254278-- | This version of these function obtain the row and column number

255279-- from the Database struct.

256280-----------------------------------------------------------------------------

257281

258282num_row_v2 : DBPointer -> IO Int

259−num_row_v2 (MkDBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_row_v2" [FPtr] FInt)pointer

260− return (x)

283+num_row_v2 (MkDBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_row_v2" [FPtr] FInt) pointer

284+ return x

261285

262286num_col_v2 : DBPointer -> IO Int

263−num_col_v2 (MkDBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col_v2" [FPtr] FInt)pointer

264− return (x)

265−

287+num_col_v2 (MkDBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col_v2" [FPtr] FInt) pointer

288+ return x

289+

266290-----------------------------------------------------------------------------

267291-- | This function prints the result of a query by checking the type

268292-- of each value returned, it then calls the appropriate function.

269293-- Ther result is one of the DBVal variants.

270294-----------------------------------------------------------------------------

271−

295+

272296get_data : DBPointer -> Int -> Int -> IO DBVal

273297get_data (MkDBPointer pointer) row col = do

274298 ty <- get_data_type pointer row col

275299 helper ty

276− where

277− get_data_type : Ptr ->Int -> Int -> IO Int

278− get_data_type pointer row col =mkForeign (FFun "sqlite3_get_data_type" [FPtr, FInt, FInt] FInt)pointer row col

279−

280− get_data_val_int : Ptr -> Int -> IO Int

281− get_data_val_int pointer col =mkForeign (FFun "sqlite3_get_val_int" [FPtr,FInt] FInt)pointer col

282−

283− get_data_val_text : Ptr -> Int -> IO String

284− get_data_val_text pointer col =mkForeign (FFun "sqlite3_get_val_text" [FPtr, FInt] FString)pointer col

285−

286−

287−

288− get_data_val_float : Ptr -> Int -> IO Float

289− get_data_val_float pointer col =mkForeign (FFun "sqlite3_get_float" [FPtr, FInt] FFloat)pointer col

290−

291− helper : Int -> IO DBVal

292− helper 1 = do i <- get_data_val_int pointer col ; return (DBInt i)

293− helper 2 = do i <- get_data_val_float pointer col ; return (DBFloat i)

294− helper 3 = do i <- get_data_val_text pointer col; return (DBText i)

295− helper _ =return (DBNull)

296−

300+ where get_data_type : Ptr ->Int -> Int -> IO Int

301+ get_data_type pointer row col =

302+ mkForeign (FFun "sqlite3_get_data_type" [FPtr, FInt, FInt] FInt) pointer row col

303+ get_data_val_int : Ptr -> Int -> IO Int

304+ get_data_val_int pointer col =

305+ mkForeign (FFun "sqlite3_get_val_int" [FPtr,FInt] FInt) pointer col

306+

307+ get_data_val_text : Ptr -> Int -> IO String

308+ get_data_val_text pointer col =

309+ mkForeign (FFun "sqlite3_get_val_text" [FPtr, FInt] FString) pointer col

310+

311+ get_data_val_float : Ptr -> Int -> IO Float

312+ get_data_val_float pointer col =

313+ mkForeign (FFun "sqlite3_get_float" [FPtr, FInt] FFloat) pointer col

314+

315+ helper : Int -> IO DBVal

316+ helper 1 = do i <- get_data_val_int pointer col ; return (DBInt i)

317+ helper 2 = do i <- get_data_val_float pointer col ; return (DBFloat i)

318+ helper 3 = do i <- get_data_val_text pointer col; return (DBText i)

319+ helper _ = return DBNull

320+

297321-----------------------------------------------------------------------------

298322-- | This function makes use of get_data to get all the result.

299323-----------------------------------------------------------------------------

300324

301−toList_v1 : DBPointer -> DB Table

302−toList_v1 db = do

303− nbR <- liftIO (num_row_v2 db)

304− nmC <- liftIO (num_col_v2 db)

305− res <- forM [0..(nbR-1)] (\ i =>

306− forM [0..(nmC-1)] (\ j =>

307− liftIO(get_data db i j)

308−

309− )

310− )

311− return res

312−

313−

325+toList_v1 : DBPointer -> DB Table

326+toList_v1 db = do nbR <- liftIO (num_row_v2 db)

327+ nmC <- liftIO (num_col_v2 db)

328+ res <- liftIO $ forM [0..(nbR-1)] $ \ i =>

329+ forM [0..(nmC-1)] $ \ j => get_data db i j

330+ return (the (List (List DBVal)) res)

331+

314332strcat : String -> String-> String

315−strcat str1 str2 = (str1 ++ str2)

333+strcat str1 str2 = str1 ++ str2

316334

317335-----------------------------------------------------------------------------

318336-- | This version of toList retunrs result from get_table

319337-- This could be removed if not needed in the future.

320338-----------------------------------------------------------------------------

321−

339+

322340--toList_v2 : String -> String -> DBPointer -> DB Table

323341--toList_v2 name stmt x = do

324342-- ptr <- (get_table x (stmt))

@@ -327,12 +345,12 @@ strcat str1 str2 = (str1 ++ str2)

327345-- res <- forM [0..(nbR-1)] (\ i =>

328346-- forM [0..(nmC-1)] (\ j =>

329347-- liftIO(get_data x name i j)

330−--

348+--

331349-- )

332350-- )

333351-- liftIO (free_table ptr)

334−-- return res

335−

352+-- return res

353+

336354

337355-----------------------------------------------------------------------------

338356-- | These routines support binding the types supported by Idris.

@@ -341,68 +359,67 @@ strcat str1 str2 = (str1 ++ str2)

341359-----------------------------------------------------------------------------

342360

343361bind_int : StmtPtr -> Int -> Int -> DB StmtPtr

344−bind_int (MkStmtPtr pointer) indexval val = do

345− x <- liftIO(mkForeign (FFun "sqlite3_bind_int_idr" [FPtr, FInt, FInt] FPtr)pointer indexval val)

346− flag <- liftIO(nullPtr x)

362+bind_int (MkStmtPtr pointer) indexval val = do

363+ x <- liftIO (mkForeign (FFun "sqlite3_bind_int_idr" [FPtr, FInt, FInt] FPtr) pointer indexval val)

364+ flag <- liftIO (nullPtr x)

347365 if flag

348− then fail "Could not bind int."

349− else return (MkStmtPtr x)

350−

351−

366+ then fail "Could not bind int."

367+ else return (MkStmtPtr x)

368+

369+

352370bind_float : StmtPtr -> Int -> Float -> DB StmtPtr

353−bind_float (MkStmtPtr pointer) indexval val = do

354− x <- liftIO(mkForeign (FFun "sqlite3_bind_float_idr" [FPtr, FInt, FFloat] FPtr)pointer indexval val)

355− flag <- liftIO(nullPtr x)

371+bind_float (MkStmtPtr pointer) indexval val = do

372+ x <- liftIO (mkForeign (FFun "sqlite3_bind_float_idr" [FPtr, FInt, FFloat] FPtr) pointer indexval val)

373+ flag <- liftIO (nullPtr x)

356374 if flag

357− then fail "Could not bind float."

358− else return (MkStmtPtr x)

375+ then fail "Could not bind float."

376+ else return (MkStmtPtr x)

359377

360378bind_text : StmtPtr -> String -> Int -> Int -> DB StmtPtr

361379bind_text (MkStmtPtr pointer) text indexval lengthval = do

362− x <- liftIO(mkForeign (FFun "sqlite3_bind_text_idr" [FPtr, FString, FInt, FInt] FPtr)pointer text indexval lengthval)

363− flag <- liftIO(nullPtr x)

380+ x <- liftIO (mkForeign (FFun "sqlite3_bind_text_idr" [FPtr, FString, FInt, FInt] FPtr)

381+ pointer text indexval lengthval)

382+ flag <- liftIO(nullPtr x)

364383 if flag

365− then fail "Could not bind text."

366− else return (MkStmtPtr x)

384+ then fail "Could not bind text."

385+ else return (MkStmtPtr x)

367386

368387bind_null : StmtPtr -> Int -> DB StmtPtr

369−bind_null (MkStmtPtr pointer) indexval = do

370− x <- liftIO(mkForeign (FFun "sqlite3_bind_null_idr" [FPtr, FInt] FPtr)pointer indexval)

371− flag <- liftIO(nullPtr x)

388+bind_null (MkStmtPtr pointer) indexval = do

389+ x <- liftIO (mkForeign (FFun "sqlite3_bind_null_idr" [FPtr, FInt] FPtr) pointer indexval)

390+ flag <- liftIO (nullPtr x)

372391 if flag

373− then fail "Could not bind null."

374− else return (MkStmtPtr x)

392+ then fail "Could not bind null."

393+ else return (MkStmtPtr x)

375394

376395-----------------------------------------------------------------------------

377396-- | String Length

378397-----------------------------------------------------------------------------

379−

398+

380399strlen : String -> DB Int

381−strlen str = liftIO(mkForeign (FFun "strLength" [FString] FInt) str)

382−

400+strlen str = liftIO (mkForeign (FFun "strLength" [FString] FInt) str)

401+

383402instance Show DBVal where

384− show (DBInt i) = "Int val: " ++ show i ++ "\n"

385− show (DBText i) = "Text val: " ++ show i ++ "\n"

386− show (DBFloat i) = "Float val: " ++ show i ++ "\n"

387− show (DBNull ) = "NULL"

403+ show (DBInt i) = "Int val: " ++ show i ++ "\n"

404+ show (DBText i) = "Text val: " ++ show i ++ "\n"

405+ show (DBFloat i) = "Float val: " ++ show i ++ "\n"

406+ show (DBNull ) = "NULL"

388407

389408-----------------------------------------------------------------------------

390409-- | Multi bind a list of values.

391410-----------------------------------------------------------------------------

392411

393412bindMulti : StmtPtr-> List (Maybe (Int, Value)) -> DB StmtPtr

394−bindMulti pointer [] = return pointer

395−bindMulti pointer (Nothing :: vs) = bindMulti pointer vs

396−bindMulti pointer ((Just (indexs, val))::vs) = case val of

397− (VInt intval) => do x <- bind_int pointer indexs intval

398− bindMulti(x) vs

399−

400− (VStr strval) => do len <- strlen strval

401− x <- bind_text pointer strval indexs len

402− bindMulti(x) vs

403−

404−

405− (VFloat floatval) => do x <- bind_float pointer indexs floatval

406−

407− bindMulti(x) vs

413+bindMulti pointer [] = return pointer

414+bindMulti pointer (Nothing :: vs) = bindMulti pointer vs

415+bindMulti pointer ((Just (indexs, (VInt i)))::vs) =

416+ do x <- bind_int pointer indexs i

417+ bindMulti x vs

418+bindMulti pointer ((Just (indexs, (VStr s)))::vs) =

419+ do len <- strlen s

420+ x <- bind_text pointer s indexs len

421+ bindMulti x vs

422+bindMulti pointer ((Just (indexs, (VFloat f)))::vs) =

423+ do x <- bind_float pointer indexs f

424+ bindMulti x vs

408425

contribs/lib/SQLite3/sqlexpr.idrdeleted−274

@@ -1,274 +0,0 @@

1−module Sqlexpr

2−import Prelude.List

3−

4−-----------------------------------------------------------------------------

5−-- |

6−-- Module : sqlexpr

7−-- Copyright : (c) The University of St Andrews, 2012

8−--

9−-- Implementations for SQLite query data type.

10−--

11−-----------------------------------------------------------------------------

12−

13−

14−-----------------------------------------------------------

15−-- | SQL data type

16−-----------------------------------------------------------

17−

18−data Value = VInt Int

19− |VStr String

20− |VFloat Float

21− |VCol String

22− |VNULL

23−

24−--Perhaps could extend this by adding

25−-- a dot operator to allow mapping

26−-- between table and column and

27−-- comparing different table columns.

28−

29−data Cond = Equals Value Value

30− |MkGT Value Value

31− |MkGTE Value Value

32− |MkLT Value Value

33− |MkLTE Value Value

34− |MkNULL Value

35−

36−

37−data Clause = MkCond Cond

38− | AND Clause Clause

39− | OR Clause Clause

40− | Empty

41− | MkSQL SQL

42−

43−data condClause = SET Clause

44− |WHERE condClause Clause

45−

46−data SelVar = Cols (List String)

47− |ALL

48−

49−data ColType = CInt String -- parsed as string "int"

50− |Varchar String

51−

52−data Constr = NOTNULL

53− | UNIQUE Constr

54− | None

55− | PRIMARYKEY

56− | FOREIGNKEY

57− | CHECK

58− | DEFAULT

59−

60−

61−data SQL = SELECT SelVar SQL Clause

62− | TBL (List String)

63− | INSERT SQL (List Value)

64− | INSERTC SQL (List Value) (List Value)

65− | UPDATE SQL condClause

66− | CREATE SQL (List (Value, ColType , Constr))

67−

68−-- remember to remove these funcs later

69−-- foldr1 : (a -> a -> a) -> List a -> a

70−-- foldr1 f [x] = x

71−-- foldr1 f (x::xs) = f x (foldr1 f xs)

72−

73−

74−-- unwords' : List (List Char) -> List Char

75−-- unwords' [] = []

76−-- unwords' ws = (foldr1 addSpace ws)

77−-- where

78−-- addSpace : List Char -> List Char -> List Char

79−-- addSpace w s = w ++ (' ' :: s)

80−--

81−--

82−-- unwords : List String -> String

83−-- unwords = pack . unwords' . map unpack

84−

85−-----------------------------------------------------------

86−-- | This function replaces values with question mark

87−-- following by an index number. It then puts the value

88−-- replaced, in the list.

89−-----------------------------------------------------------

90−

91−valString : List (Maybe(Int, Value)) -> Value -> (String, List (Maybe(Int, Value)))

92−valString xs (VInt x) = ("?" ++ show (cast(length xs)+1), xs ++ [Just (cast((length xs)+1),(VInt x))])

93−valString xs (VStr x) = ("?" ++ show (cast(length xs)+1), xs ++ [Just (cast((length xs)+1),(VStr x))])

94−valString xs (VFloat x) = ("?" ++ show (cast(length xs)+1), xs ++ [Just (cast((length xs)+1),(VFloat x))])

95−valString xs (VCol n) = (n, xs)

96−

97−-----------------------------------------------------------

98−-- | This function calls valString on a list of Values

99−-- and separates the values by commas.

100−-----------------------------------------------------------

101−

102−listVal : List (Maybe(Int, Value)) -> List Value -> (String, List (Maybe(Int, Value)))

103−listVal xs [] = ("", xs)

104−listVal xs (v::vs) = let (str, newxs) = (valString xs v) in

105− let (str', newxs') = listVal newxs vs in

106− ((unwords(intersperse "," (words(str) ++ words (str')))), newxs')

107−

108−-----------------------------------------------------------

109−-- | Parses the type of column to be created.

110−-----------------------------------------------------------

111−

112−getColType : List (Maybe(Int, Value)) -> ColType -> (String, List (Maybe(Int, Value)))

113−getColType xs (CInt x) = ("int", xs)

114−getColType xs (Varchar str) = ("varchar(255)", xs)

115−

116−-----------------------------------------------------------

117−-- | CREATE Constraints

118−-----------------------------------------------------------

119−

120−getConstr : List (Maybe(Int, Value)) -> Constr -> (String, List (Maybe(Int, Value)))

121−getConstr xs (NOTNULL) = ("NOT NULL", xs)

122−getConstr xs (UNIQUE constr) = ("NOT NULL UNIQUE", xs)

123−getConstr xs (PRIMARYKEY) = ("PRIMARY KEY", xs)

124−getConstr xs (FOREIGNKEY) = ("FOREIGN KEY", xs)

125−getConstr xs (CHECK) = ("CHECK", xs)

126−getConstr xs (DEFAULT) = ("DEFAULT", xs)

127−getConstr xs (None) = ("", xs)

128−

129−putBrackets : String -> String

130−putBrackets str = "(" ++ str ++ ")"

131−

132−-----------------------------------------------------------

133−-- | Used to detect a complex type in a nested SQLite query

134−-- This function is used for bracketing the nested queries.

135−-----------------------------------------------------------

136−complexType : SQL -> Bool

137−complexType (TBL tbl) = False

138−complexType (SELECT vars sql c) = True

139−

140−-----------------------------------------------------------

141−-- | Used in CREATE

142−-----------------------------------------------------------

143−

144−listValType : List (Maybe(Int, Value)) -> List (Value, ColType , Constr) -> (String, List (Maybe(Int, Value)))

145−listValType xs [] = ("", xs)

146−listValType xs ((val, types, constr) :: vs) = let (str , newxs) = valString xs val in

147− let (str' , newxs') = getColType newxs types in

148− let (str'', newxs'') = getConstr newxs' constr in

149− let (finalstr, finalxs) = listValType newxs'' vs in

150− ((unwords(intersperse " " (words(str) ++ words(str') ++ words(str'') ++ words(finalstr)))) , finalxs)

151−

152−

153−-----------------------------------------------------------

154−-- | Evaluates a conditional WHERE clause

155−-----------------------------------------------------------

156−

157−evalCond : List (Maybe(Int, Value)) -> Cond -> (String, List (Maybe(Int, Value)))

158−evalCond xs (Equals val1 val2) = let (restring , newxs ) = valString xs val1 in

159− let (restring2, newxs') = valString newxs val2 in

160− (restring ++ " = " ++ restring2, newxs')

161−

162−evalCond xs (MkGT val1 val2) = let (restring , newxs ) = valString xs val1 in

163− let (restring2, newxs') = valString newxs val2 in

164− (restring ++ " > " ++ restring2, newxs')

165−

166−evalCond xs (MkGTE val1 val2) = let (restring , newxs ) = valString xs val1 in

167− let (restring2, newxs') = valString newxs val2 in

168− (restring ++ " >= " ++ restring2, newxs')

169−

170−evalCond xs (MkLT val1 val2) = let (restring , newxs ) = valString xs val1 in

171− let (restring2, newxs') = valString newxs val2 in

172− (restring ++ " < " ++ restring2, newxs')

173−

174−evalCond xs (MkLTE val1 val2) = let (restring , newxs ) = valString xs val1 in

175− let (restring2, newxs') = valString newxs val2 in

176− (restring ++ " =< " ++ restring2, newxs')

177−

178−evalCond xs (MkNULL val) = let (restring , newxs ) = valString xs val in

179− (restring ++ " IS NULL " , newxs)

180−

181−-----------------------------------------------------------

182−-- | Evaluates queries by calling the other functions

183−-- on each part of the query

184−-----------------------------------------------------------

185−evalSQL : List (Maybe(Int, Value)) -> SQL -> ( String, List (Maybe(Int, Value)))

186−-----------------------------------------------------------

187−-- | Evaluates clauses

188−-- Supports WHERE Clause

189−-- WHERE Clause And Another-Clause

190−-- WHERE Clause Or Another-Clause

191−-----------------------------------------------------------

192−clauseString : List (Maybe(Int, Value)) -> Clause -> (String, List (Maybe(Int, Value)))

193−

194−clauseString xs (Empty) = ("" , []) -- No condition

195−clauseString xs (MkCond cond') = let (condstr, newxs) = evalCond xs cond' in

196− (condstr , newxs)

197−

198−clauseString xs (AND c1 c2) = let (clausestr, newxs) = clauseString xs c1 in

199− let (clausestr2, newxs') = clauseString newxs c2 in

200− (clausestr ++ " AND " ++clausestr2 , newxs')

201−

202−clauseString xs (OR c1 c2) = let (clausestr, newxs) = clauseString xs c1 in

203− let (clausestr2, newxs') = clauseString newxs c2 in

204− (clausestr ++ " OR " ++clausestr2 , newxs')

205−

206−

207−-----------------------------------------------------------

208−-- | Evaluates conditional clauses.

209−-----------------------------------------------------------

210−

211−condClauseStr : List (Maybe(Int, Value)) -> condClause -> (String, List (Maybe(Int, Value)))

212−condClauseStr xs (SET setcl) = let (condstr, newxs) = clauseString xs setcl in

213− (" SET " ++ condstr, newxs)

214−

215−condClauseStr xs (WHERE setcl1 setcl2) = let (condstr, newxs) = condClauseStr xs setcl1 in

216− let (condstr', newxs') = clauseString newxs setcl2 in

217− ( condstr ++ " WHERE " ++ condstr', newxs')

218−

219−-- SELECT data from tbl1 where num > (SELECT num from tbl1 where num = 24)

220−-- evalSQL [] ((SELECT ALL)(TBL "tbl")(MkSQL ((SELECT ALL) (TBL "tbl")(MkCond (VCol "))))

221−-- NTBF

222−--clauseString xs (MkSQL sql) = (evalSQL xs sql)

223−

224−-- Separate list of tables

225−-- For complex type, return list returned by evalSQL

226−-- And add brackets

227−evalSQL xs (TBL tbl) = ((unwords (intersperse "," ( tbl))), xs)

228−evalSQL xs (SELECT vars sql' c) = let (sqlstring, newxs) = evalSQL xs sql' in

229− let (csstring, newxs') = clauseString newxs c in

230− case c of

231− Empty => case vars of

232− (ALL ) => if complexType sql' then ("SELECT " ++ "*" ++ " FROM "

233− ++ (putBrackets sqlstring) ++ csstring, newxs)

234−

235− else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring

236− ++ csstring, newxs')

237−

238− (Cols selvar) => if complexType sql' then ("SELECT " ++ (unwords selvar) ++

239− " FROM " ++ (putBrackets sqlstring) ++ csstring, newxs)

240−

241− else ("SELECT " ++ (unwords selvar )++ " FROM " ++ sqlstring

242− ++ csstring, newxs')

243−

244− _ => case vars of

245− (ALL ) => if complexType sql' then ("SELECT " ++ "*" ++ " FROM "

246− ++ " WHERE " ++ csstring , newxs)

247− else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring

248− ++ " WHERE " ++ csstring , newxs')

249−

250− (Cols selvar) => if complexType sql' then ("SELECT " ++ (unwords selvar) ++ " FROM " ++

251− (putBrackets sqlstring) ++ " WHERE "

252− ++ csstring , newxs)

253−

254− else ("SELECT " ++ (unwords selvar) ++ " FROM " ++ sqlstring

255− ++ " WHERE " ++ csstring , newxs')

256−

257−

258−evalSQL xs (INSERT sql vals) = let (tblname, newvals) = evalSQL xs sql in

259− let (str, newxs ) = listVal newvals vals in

260− ("INSERT INTO " ++ tblname ++ " VALUES (" ++ str ++ ")" , newxs)

261−

262−evalSQL xs (INSERTC sql cols vals) = let (tblname, newvals) = evalSQL xs sql in

263− let (strcol, newcol) = listVal newvals cols in

264− let (strval, newcolval) = listVal newcol vals in

265− ("INSERT INTO " ++ tblname ++ "(" ++ strcol ++ ")" ++ "VALUES (" ++ strval ++ ")", newcolval)

266−

267−

268−evalSQL xs (UPDATE sql cl) = let (tblname, newxs) = evalSQL xs sql in

269− let (csstring, newxs') = condClauseStr newxs cl in

270− ("UPDATE " ++ tblname ++ csstring, newxs')

271−

272−evalSQL xs (CREATE sql details) = let (sqlstring, newxs) = evalSQL xs sql in

273− let (csstring, newxs') = listValType newxs details in

274− ("CREATE TABLE " ++ sqlstring ++ "(" ++ csstring ++ ")", newxs')

contribs/tool-support/vim/ftplugin/idris.vim+3−3

@@ -1,3 +1,3 @@

1−set shiftwidth=2

2−set tabstop=2

3−set expandtab

1+setlocal shiftwidth=2

2+setlocal tabstop=2

3+setlocal expandtab

effects/Effect/Memory.idrnew file+168

@@ -0,0 +1,168 @@

1+module Effect.Memory

2+

3+import Effects

4+import Control.IOExcept

5+

6+%access public

7+

8+abstract

9+data MemoryChunk : Nat -> Nat -> Type where

10+ CH : Ptr -> MemoryChunk size initialized

11+

12+abstract

13+data RawMemory : Effect where

14+ Allocate : (n : Nat) ->

15+ RawMemory () (MemoryChunk n 0) ()

16+ Free : RawMemory (MemoryChunk n i) () ()

17+ Initialize : Bits8 ->

18+ (size : Nat) ->

19+ so (i + size <= n) ->

20+ RawMemory (MemoryChunk n i) (MemoryChunk n (i + size)) ()

21+ Peek : (offset : Nat) ->

22+ (size : Nat) ->

23+ so (offset + size <= i) ->

24+ RawMemory (MemoryChunk n i) (MemoryChunk n i) (Vect Bits8 size)

25+ Poke : (offset : Nat) ->

26+ (Vect Bits8 size) ->

27+ so (offset <= i && offset + size <= n) ->

28+ RawMemory (MemoryChunk n i) (MemoryChunk n (max i (offset + size))) ()

29+ Move : (src : MemoryChunk src_size src_init) ->

30+ (dst_offset : Nat) ->

31+ (src_offset : Nat) ->

32+ (size : Nat) ->

33+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

34+ so (src_offset + size <= src_init) ->

35+ RawMemory (MemoryChunk dst_size dst_init)

36+ (MemoryChunk dst_size (max dst_init (dst_offset + size))) ()

37+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (MemoryChunk n i)

38+

39+private

40+do_malloc : Nat -> IOExcept String Ptr

41+do_malloc size with (fromInteger (cast size) == size)

42+ | True = do ptr <- ioe_lift $ mkForeign (FFun "malloc" [FInt ITNative] FPtr) (cast size)

43+ fail <- ioe_lift $ nullPtr ptr

44+ if fail then ioe_fail "Cannot allocate memory"

45+ else return ptr

46+ | False = ioe_fail "The target architecture does not support adressing enough memory"

47+

48+private

49+do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()

50+do_memset ptr offset c size

51+ = mkForeign (FFun "idris_memset" [FPtr, FInt ITNative, FAny Bits8, FInt ITNative] FUnit)

52+ ptr (cast offset) c (cast size)

53+

54+private

55+do_free : Ptr -> IO ()

56+do_free ptr = mkForeign (FFun "free" [FPtr] FUnit) ptr

57+

58+private

59+do_memmove : Ptr -> Ptr -> Nat -> Nat -> Nat -> IO ()

60+do_memmove dest src dest_offset src_offset size

61+ = mkForeign (FFun "idris_memmove" [FPtr, FPtr, FInt ITNative, FInt ITNative, FInt ITNative] FUnit)

62+ dest src (cast dest_offset) (cast src_offset) (cast size)

63+

64+private

65+do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size)

66+do_peek _ _ O = return (Prelude.Vect.Nil)

67+do_peek ptr offset (S n)

68+ = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt ITNative] (FInt ITNative)) ptr (cast offset)

69+ bs <- do_peek ptr (S offset) n

70+ Prelude.Monad.return (Prelude.Vect.(::) (prim__intToB8 b) bs)

71+

72+private

73+do_poke : Ptr -> Nat -> Vect Bits8 size -> IO ()

74+do_poke _ _ [] = return ()

75+do_poke ptr offset (b::bs)

76+ = do mkForeign (FFun "idris_poke" [FPtr, FInt ITNative, FAny Bits8] FUnit) ptr (cast offset) b

77+ do_poke ptr (S offset) bs

78+

79+instance Handler RawMemory (IOExcept String) where

80+ handle () (Allocate n) k

81+ = do ptr <- do_malloc n

82+ k (CH ptr) ()

83+ handle {res = MemoryChunk _ offset} (CH ptr) (Initialize c size _) k

84+ = ioe_lift (do_memset ptr offset c size) $> k (CH ptr) ()

85+ handle (CH ptr) (Free) k

86+ = ioe_lift (do_free ptr) $> k () ()

87+ handle (CH ptr) (Peek offset size _) k

88+ = do res <- ioe_lift (do_peek ptr offset size)

89+ k (CH ptr) res

90+ handle (CH ptr) (Poke offset content _) k

91+ = do ioe_lift (do_poke ptr offset content)

92+ k (CH ptr) ()

93+ handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k

94+ = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)

95+ k (CH dest_ptr) ()

96+ handle chunk (GetRawPtr) k

97+ = k chunk chunk

98+

99+RAW_MEMORY : Type -> EFFECT

100+RAW_MEMORY t = MkEff t RawMemory

101+

102+allocate : (n : Nat) -> EffM m [RAW_MEMORY ()] [RAW_MEMORY (MemoryChunk n 0)] ()

103+allocate size = Allocate size

104+

105+initialize : {i : Nat} ->

106+ {n : Nat} ->

107+ Bits8 ->

108+ (size : Nat) ->

109+ so (i + size <= n) ->

110+ EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (i + size))] ()

111+initialize c size prf = Initialize c size prf

112+

113+free : EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY ()] ()

114+free = Free

115+

116+peek : {i : Nat} ->

117+ (offset : Nat) ->

118+ (size : Nat) ->

119+ so (offset + size <= i) ->

120+ Eff m [RAW_MEMORY (MemoryChunk n i)] (Vect Bits8 size)

121+peek offset size prf = Peek offset size prf

122+

123+poke : {n : Nat} ->

124+ {i : Nat} ->

125+ (offset : Nat) ->

126+ Vect Bits8 size ->

127+ so (offset <= i && offset + size <= n) ->

128+ EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (max i (offset + size)))] ()

129+poke offset content prf = Poke offset content prf

130+

131+private

132+getRawPtr : Eff m [RAW_MEMORY (MemoryChunk n i)] (MemoryChunk n i)

133+getRawPtr = GetRawPtr

134+

135+private

136+move' : {dst_size : Nat} ->

137+ {dst_init : Nat} ->

138+ {src_init : Nat} ->

139+ (src_ptr : MemoryChunk src_size src_init) ->

140+ (dst_offset : Nat) ->

141+ (src_offset : Nat) ->

142+ (size : Nat) ->

143+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

144+ so (src_offset + size <= src_init) ->

145+ EffM m [RAW_MEMORY (MemoryChunk dst_size dst_init)]

146+ [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))] ()

147+move' src_ptr dst_offset src_offset size dst_bounds src_bounds

148+ = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

149+

150+data MoveDescriptor = Dst | Src

151+

152+move : {dst_size : Nat} ->

153+ {dst_init : Nat} ->

154+ {src_size : Nat} ->

155+ {src_init : Nat} ->

156+ (dst_offset : Nat) ->

157+ (src_offset : Nat) ->

158+ (size : Nat) ->

159+ so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

160+ so (src_offset + size <= src_init) ->

161+ EffM m [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)

162+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]

163+ [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))

164+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)] ()

165+move dst_offset src_offset size dst_bounds src_bounds

166+ = do src_ptr <- Src :- getRawPtr

167+ Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

168+ return ()

effects/Makefile+1−1

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

44

55recheck: clean check

66

7−install:

7+install:

88 $(IDRIS) --install effects.ipkg

99

1010clean: .PHONY

effects/effects.ipkg+3−1

@@ -3,4 +3,6 @@ package effects

33opts = "-i ../lib"

44modules = Effects,

55 Effect.Exception, Effect.File, Effect.State,

6− Effect.Random, Effect.StdIO, Effect.Select

6+ Effect.Random, Effect.StdIO, Effect.Select,

7+ Effect.Memory

8+

idris.cabal+6−2

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

11Name: idris

2−Version: 0.9.7

2+Version: 0.9.8

33License: BSD3

44License-file: LICENSE

55Author: Edwin Brady

@@ -58,6 +58,7 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr

5858 lib/Control/Monad/*.idr lib/Language/*.idr

5959 lib/System/Concurrency/*.idr

6060 lib/Data/*.idr lib/Debug/*.idr

61+ lib/Data/Vect/*.idr

6162 lib/Decidable/*.idr

6263 tutorial/examples/*.idr lib/base.ipkg

6364 effects/Makefile effects/*.idr effects/Effect/*.idr

@@ -111,7 +112,7 @@ Executable idris

111112 haskeline>=0.7, split, directory,

112113 containers, process, transformers, filepath,

113114 directory, binary, bytestring, text, pretty,

114− language-java>=0.2.2, libffi, unix

115+ language-java>=0.2.2, libffi

115116

116117 Extensions: MultiParamTypeClasses, FunctionalDependencies,

117118 FlexibleInstances, TemplateHaskell

@@ -119,7 +120,10 @@ Executable idris

119120 ghc-options: -rtsopts

120121 if os(linux)

121122 cpp-options: -DLINUX

123+ build-depends: unix

122124 if os(darwin)

123125 cpp-options: -DMACOSX

126+ build-depends: unix

124127 if os(windows)

125128 cpp-options: -DWINDOWS

129+ build-depends: Win32

java/src/main/java/org/idris/rts/ForeignPrimitives.java+42

@@ -191,6 +191,48 @@ public class ForeignPrimitives {

191191 return (o == null ? 1 : 0);

192192 }

193193

194+ public static Object malloc(int size) {

195+ return ByteBuffer.allocate(size);

196+ }

197+

198+ public static void idris_memset(Object buf, int offset, Object c, int size) {

199+ ByteBuffer buffer = (ByteBuffer)buf;

200+ buffer.rewind();

201+ buffer.position(offset);

202+ byte init[] = new byte[size];

203+ Arrays.fill(init, (Byte)c);

204+ buffer.put(init, offset, size);

205+ buffer.rewind();

206+ }

207+

208+ public static void free(Object buf) {

209+ buf = null;

210+ }

211+

212+ public static Integer idris_peek(Object buf, int offset) {

213+ ByteBuffer buffer = (ByteBuffer)buf;

214+ return Integer.valueOf(buffer.get(offset));

215+ }

216+

217+ public static void idris_poke(Object buf, int offset, Object data) {

218+ ByteBuffer buffer = (ByteBuffer)buf;

219+ buffer.put(offset, (Byte)data);

220+ }

221+

222+ public static void idris_memmove(Object dstBuf, Object srcBuf, int dstOffset, int srcOffset, int size) {

223+ ByteBuffer dst = (ByteBuffer)dstBuf;

224+ ByteBuffer src = (ByteBuffer)srcBuf;

225+ byte [] srcData = new byte[size];

226+ src.rewind();

227+ src.position(srcOffset);

228+ src.get(srcData, 0, size);

229+ src.rewind();

230+ dst.rewind();

231+ dst.position(dstOffset);

232+ dst.put(srcData, 0, size);

233+ dst.rewind();

234+ }

235+

194236 public final static Object idris_K(final Object result, final Object drop) {

195237 return result;

196238 }

js/Runtime-common.js+2

@@ -10,8 +10,10 @@ __IDRRT__.Char = new __IDRRT__.Type('Char');

1010__IDRRT__.String = new __IDRRT__.Type('String');

1111__IDRRT__.Integer = new __IDRRT__.Type('Integer');

1212__IDRRT__.Float = new __IDRRT__.Type('Float');

13+__IDRRT__.Ptr = new __IDRRT__.Type('Pointer')

1314__IDRRT__.Forgot = new __IDRRT__.Type('Forgot');

1415

16+

1517/** @constructor */

1618__IDRRT__.Tailcall = function(f) { this.f = f };

1719

lib/Builtins.idr+3

@@ -44,6 +44,9 @@ really_believe_me x = prim__believe_me _ _ x

4444

4545namespace Builtins {

4646

47+Not : Type -> Type

48+Not a = a -> _|_

49+

4750id : a -> a

4851id x = x

4952

lib/Data/BoundedList.idrnew file+93

@@ -0,0 +1,93 @@

1+module Data.BoundedList

2+

3+%access public

4+%default total

5+

6+data BoundedList : Type -> Nat -> Type where

7+ Nil : BoundedList a n

8+ (::) : a -> BoundedList a n -> BoundedList a (S n)

9+

10+length : BoundedList a n -> Fin (S n)

11+length [] = fO

12+length (x :: xs) = fS (length xs)

13+

14+--------------------------------------------------------------------------------

15+-- Indexing into bounded lists

16+--------------------------------------------------------------------------------

17+

18+index : Fin (S n) -> BoundedList a n -> Maybe a

19+index _ [] = Nothing

20+index fO (x :: _) = Just x

21+index (fS f) (_ :: xs) = index f xs

22+

23+--------------------------------------------------------------------------------

24+-- Adjusting bounds

25+--------------------------------------------------------------------------------

26+

27+weaken : BoundedList a n -> BoundedList a (n + m)

28+weaken [] = []

29+weaken (x :: xs) = x :: weaken xs

30+

31+--------------------------------------------------------------------------------

32+-- Conversions to and from list

33+--------------------------------------------------------------------------------

34+

35+take : (n : Nat) -> List a -> BoundedList a n

36+take _ [] = []

37+take O _ = []

38+take (S n') (x :: xs) = x :: take n' xs

39+

40+toList : BoundedList a n -> List a

41+toList [] = []

42+toList (x :: xs) = x :: toList xs

43+

44+fromList : (xs : List a) -> BoundedList a (length xs)

45+fromList [] = []

46+fromList (x :: xs) = x :: fromList xs

47+

48+--------------------------------------------------------------------------------

49+-- Building (bigger) bounded lists

50+--------------------------------------------------------------------------------

51+

52+replicate : (n : Nat) -> a -> BoundedList a n

53+replicate O _ = []

54+replicate (S n) x = x :: replicate n x

55+

56+--------------------------------------------------------------------------------

57+-- Folds

58+--------------------------------------------------------------------------------

59+

60+foldl : (a -> b -> a) -> a -> BoundedList b n -> a

61+foldl f e [] = e

62+foldl f e (x::xs) = foldl f (f e x) xs

63+

64+foldr : (a -> b -> b) -> b -> BoundedList a n -> b

65+foldr f e [] = e

66+foldr f e (x::xs) = f x (foldr f e xs)

67+

68+--------------------------------------------------------------------------------

69+-- Maps

70+--------------------------------------------------------------------------------

71+

72+map : (a -> b) -> BoundedList a n -> BoundedList b n

73+map f [] = []

74+map f (x :: xs) = f x :: map f xs

75+

76+--------------------------------------------------------------------------------

77+-- Misc

78+--------------------------------------------------------------------------------

79+

80+%assert_total -- not sure why this isn't accepted - clearly decreasing on n

81+pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n

82+pad {n=O} [] _ = []

83+pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)

84+pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding

85+

86+

87+--------------------------------------------------------------------------------

88+-- Simple properties

89+--------------------------------------------------------------------------------

90+

91+zeroBoundIsEmpty : (xs : BoundedList a 0) -> xs = the (BoundedList a 0) []

92+zeroBoundIsEmpty [] = refl

93+zeroBoundIsEmpty (_ :: _) impossible

lib/Data/SortedMap.idrnew file+235

@@ -0,0 +1,235 @@

1+module Data.SortedMap

2+

3+-- TODO: write merge and split

4+

5+data Tree : Nat -> Type -> Type -> Type where

6+ Leaf : k -> v -> Tree O k v

7+ Branch2 : Tree n k v -> k -> Tree n k v -> Tree (S n) k v

8+ Branch3 : Tree n k v -> k -> Tree n k v -> k -> Tree n k v -> Tree (S n) k v

9+

10+branch4 :

11+ Tree n k v -> k ->

12+ Tree n k v -> k ->

13+ Tree n k v -> k ->

14+ Tree n k v ->

15+ Tree (S (S n)) k v

16+branch4 a b c d e f g =

17+ Branch2 (Branch2 a b c) d (Branch2 e f g)

18+

19+branch5 :

20+ Tree n k v -> k ->

21+ Tree n k v -> k ->

22+ Tree n k v -> k ->

23+ Tree n k v -> k ->

24+ Tree n k v ->

25+ Tree (S (S n)) k v

26+branch5 a b c d e f g h i =

27+ Branch2 (Branch2 a b c) d (Branch3 e f g h i)

28+

29+branch6 :

30+ Tree n k v -> k ->

31+ Tree n k v -> k ->

32+ Tree n k v -> k ->

33+ Tree n k v -> k ->

34+ Tree n k v -> k ->

35+ Tree n k v ->

36+ Tree (S (S n)) k v

37+branch6 a b c d e f g h i j k =

38+ Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)

39+

40+branch7 :

41+ Tree n k v -> k ->

42+ Tree n k v -> k ->

43+ Tree n k v -> k ->

44+ Tree n k v -> k ->

45+ Tree n k v -> k ->

46+ Tree n k v -> k ->

47+ Tree n k v ->

48+ Tree (S (S n)) k v

49+branch7 a b c d e f g h i j k l m =

50+ Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)

51+

52+merge1 : Tree n k v -> k -> Tree (S n) k v -> k -> Tree (S n) k v -> Tree (S (S n)) k v

53+merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i

54+merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k

55+merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k

56+merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

57+

58+merge2 : Tree (S n) k v -> k -> Tree n k v -> k -> Tree (S n) k v -> Tree (S (S n)) k v

59+merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i

60+merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k

61+merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k

62+merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

63+

64+merge3 : Tree (S n) k v -> k -> Tree (S n) k v -> k -> Tree n k v -> Tree (S (S n)) k v

65+merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i

66+merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k

67+merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k

68+merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m

69+

70+treeLookup : Ord k => k -> Tree n k v -> Maybe v

71+treeLookup k (Leaf k' v) =

72+ if k == k' then

73+ Just v

74+ else

75+ Nothing

76+treeLookup k (Branch2 t1 k' t2) =

77+ if k <= k' then

78+ treeLookup k t1

79+ else

80+ treeLookup k t2

81+treeLookup k (Branch3 t1 k1 t2 k2 t3) =

82+ if k <= k1 then

83+ treeLookup k t1

84+ else if k <= k2 then

85+ treeLookup k t2

86+ else

87+ treeLookup k t3

88+

89+treeInsert' : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree n k v, k, Tree n k v)

90+treeInsert' k v (Leaf k' v') =

91+ case compare k k' of

92+ LT => Right (Leaf k v, k, Leaf k' v')

93+ EQ => Left (Leaf k v)

94+ GT => Right (Leaf k' v', k', Leaf k v)

95+treeInsert' k v (Branch2 t1 k' t2) =

96+ if k <= k' then

97+ case treeInsert' k v t1 of

98+ Left t1' => Left (Branch2 t1' k' t2)

99+ Right (a, b, c) => Left (Branch3 a b c k' t2)

100+ else

101+ case treeInsert' k v t2 of

102+ Left t2' => Left (Branch2 t1 k' t2')

103+ Right (a, b, c) => Left (Branch3 t1 k' a b c)

104+treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =

105+ if k <= k1 then

106+ case treeInsert' k v t1 of

107+ Left t1' => Left (Branch3 t1' k1 t2 k2 t3)

108+ Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3)

109+ else

110+ if k <= k2 then

111+ case treeInsert' k v t2 of

112+ Left t2' => Left (Branch3 t1 k1 t2' k2 t3)

113+ Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3)

114+ else

115+ case treeInsert' k v t3 of

116+ Left t3' => Left (Branch3 t1 k1 t2 k2 t3')

117+ Right (a, b, c) => Right (Branch2 t1 k2 t2, k2, Branch2 a b c)

118+

119+treeInsert : Ord k => k -> v -> Tree n k v -> Either (Tree n k v) (Tree (S n) k v)

120+treeInsert k v t =

121+ case treeInsert' k v t of

122+ Left t' => Left t'

123+ Right (a, b, c) => Right (Branch2 a b c)

124+

125+delType : Nat -> Type -> Type -> Type

126+delType O k v = ()

127+delType (S n) k v = Tree n k v

128+

129+treeDelete : Ord k => k -> Tree n k v -> Either (Tree n k v) (delType n k v)

130+treeDelete k (Leaf k' v) =

131+ if k == k' then

132+ Right ()

133+ else

134+ Left (Leaf k' v)

135+treeDelete {n=S O} k (Branch2 t1 k' t2) =

136+ if k <= k' then

137+ case treeDelete k t1 of

138+ Left t1' => Left (Branch2 t1' k' t2)

139+ Right () => Right t2

140+ else

141+ case treeDelete k t2 of

142+ Left t2' => Left (Branch2 t1 k' t2')

143+ Right () => Right t1

144+treeDelete {n=S O} k (Branch3 t1 k1 t2 k2 t3) =

145+ if k <= k1 then

146+ case treeDelete k t1 of

147+ Left t1' => Left (Branch3 t1' k1 t2 k2 t3)

148+ Right () => Left (Branch2 t2 k2 t3)

149+ else if k <= k2 then

150+ case treeDelete k t2 of

151+ Left t2' => Left (Branch3 t1 k1 t2' k2 t3)

152+ Right () => Left (Branch2 t1 k1 t3)

153+ else

154+ case treeDelete k t3 of

155+ Left t3' => Left (Branch3 t1 k1 t2 k2 t3')

156+ Right () => Left (Branch2 t1 k1 t2)

157+treeDelete {n=S (S _)} k (Branch2 t1 k' t2) =

158+ if k <= k' then

159+ case treeDelete k t1 of

160+ Left t1' => Left (Branch2 t1' k' t2)

161+ Right t1' =>

162+ case t2 of

163+ Branch2 a b c => Right (Branch3 t1' k' a b c)

164+ Branch3 a b c d e => Left (branch4 t1' k' a b c d e)

165+ else

166+ case treeDelete k t2 of

167+ Left t2' => Left (Branch2 t1 k' t2')

168+ Right t2' =>

169+ case t1 of

170+ Branch2 a b c => Right (Branch3 a b c k' t2')

171+ Branch3 a b c d e => Left (branch4 a b c d e k' t2')

172+treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =

173+ if k <= k1 then

174+ case treeDelete k t1 of

175+ Left t1' => Left (Branch3 t1' k1 t2 k2 t3)

176+ Right t1' => Left (merge1 t1' k1 t2 k2 t3)

177+ else if k <= k2 then

178+ case treeDelete k t2 of

179+ Left t2' => Left (Branch3 t1 k1 t2' k2 t3)

180+ Right t2' => Left (merge2 t1 k1 t2' k2 t3)

181+ else

182+ case treeDelete k t3 of

183+ Left t3' => Left (Branch3 t1 k1 t2 k2 t3')

184+ Right t3' => Left (merge3 t1 k1 t2 k2 t3')

185+

186+-- FIXME: this is very inefficient

187+treeToList : Ord k => Tree n k v -> List (k, v)

188+treeToList (Leaf k v) = [(k, v)]

189+treeToList (Branch2 t1 _ t2) = treeToList t1 ++ treeToList t2

190+treeToList (Branch3 t1 _ t2 _ t3) = treeToList t1 ++ treeToList t2 ++ treeToList t3

191+

192+data SortedMap : Type -> Type -> Type where

193+ Empty : SortedMap k v

194+ M : (n:Nat) -> Tree n k v -> SortedMap k v

195+

196+empty : SortedMap k v

197+empty = Empty

198+

199+lookup : Ord k => k -> SortedMap k v -> Maybe v

200+lookup _ Empty = Nothing

201+lookup k (M _ t) = treeLookup k t

202+

203+insert : Ord k => k -> v -> SortedMap k v -> SortedMap k v

204+insert k v Empty = M O (Leaf k v)

205+insert k v (M _ t) =

206+ case treeInsert k v t of

207+ Left t' => (M _ t')

208+ Right t' => (M _ t')

209+

210+delete : Ord k => k -> SortedMap k v -> SortedMap k v

211+delete _ Empty = Empty

212+delete k (M O t) =

213+ case treeDelete k t of

214+ Left t' => (M _ t')

215+ Right () => Empty

216+delete k (M (S _) t) =

217+ case treeDelete k t of

218+ Left t' => (M _ t')

219+ Right t' => (M _ t')

220+

221+fromList : Ord k => List (k, v) -> SortedMap k v

222+fromList l = foldl (flip (uncurry insert)) empty l

223+

224+toList : Ord k => SortedMap k v -> List (k, v)

225+toList Empty = []

226+toList (M _ t) = treeToList t

227+

228+instance Functor (Tree n k) where

229+ fmap f (Leaf k v) = Leaf k (f v)

230+ fmap f (Branch2 t1 k t2) = Branch2 (fmap f t1) k (fmap f t2)

231+ fmap f (Branch3 t1 k1 t2 k2 t3) = Branch3 (fmap f t1) k1 (fmap f t2) k2 (fmap f t3)

232+

233+instance Functor (SortedMap k) where

234+ fmap _ Empty = Empty

235+ fmap f (M _ t) = M _ (fmap f t)

lib/Data/SortedSet.idrnew file+25

@@ -0,0 +1,25 @@

1+module Data.SortedSet

2+

3+import Data.SortedMap

4+

5+-- TODO: add intersection, union, difference

6+

7+data SortedSet k = SetWrapper (Data.SortedMap.SortedMap k ())

8+

9+empty : SortedSet k

10+empty = SetWrapper Data.SortedMap.empty

11+

12+insert : Ord k => k -> SortedSet k -> SortedSet k

13+insert k (SetWrapper m) = SetWrapper (Data.SortedMap.insert k () m)

14+

15+delete : Ord k => k -> SortedSet k -> SortedSet k

16+delete k (SetWrapper m) = SetWrapper (Data.SortedMap.delete k m)

17+

18+contains : Ord k => k -> SortedSet k -> Bool

19+contains k (SetWrapper m) = isJust (Data.SortedMap.lookup k m)

20+

21+fromList : Ord k => List k -> SortedSet k

22+fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))

23+

24+toList : Ord k => SortedSet k -> List k

25+toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)

lib/Data/Vect/Quantifiers.idrnew file+47

@@ -0,0 +1,47 @@

1+module Data.Vect.Quantifiers

2+

3+data Any : (P : a -> Type) -> Vect a n -> Type where

4+ Here : {P : a -> Type} -> {xs : Vect a n} -> P x -> Any P (x :: xs)

5+ There : {P : a -> Type} -> {xs : Vect a n} -> Any P xs -> Any P (x :: xs)

6+

7+anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_

8+anyNilAbsurd Here impossible

9+anyNilAbsurd There impossible

10+

11+anyElim : {xs : Vect a n} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b

12+anyElim _ f (Here p) = f p

13+anyElim f _ (There p) = f p

14+

15+any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (Any P xs)

16+any _ Nil = No anyNilAbsurd

17+any p (x::xs) with (p x)

18+ | Yes prf = Yes (Here prf)

19+ | No prf =

20+ case any p xs of

21+ Yes prf' => Yes (There prf')

22+ No prf' => No (anyElim prf' prf)

23+

24+data All : (P : a -> Type) -> Vect a n -> Type where

25+ Nil : {P : a -> Type} -> All P Nil

26+ (::) : {P : a -> Type} -> {xs : Vect a n} -> P x -> All P xs -> All P (x :: xs)

27+

28+negAnyAll : {P : a -> Type} -> {xs : Vect a n} -> Not (Any P xs) -> All (\x => Not (P x)) xs

29+negAnyAll {xs=Nil} _ = Nil

30+negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))

31+

32+notAllHere : {P : a -> Type} -> {xs : Vect a n} -> Not (P x) -> All P (x :: xs) -> _|_

33+notAllHere _ Nil impossible

34+notAllHere np (p :: _) = np p

35+

36+notAllThere : {P : a -> Type} -> {xs : Vect a n} -> Not (All P xs) -> All P (x :: xs) -> _|_

37+notAllThere _ Nil impossible

38+notAllThere np (_ :: ps) = np ps

39+

40+all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect a n) -> Dec (All P xs)

41+all _ Nil = Yes Nil

42+all d (x::xs) with (d x)

43+ | No prf = No (notAllHere prf)

44+ | Yes prf =

45+ case all d xs of

46+ Yes prf' => Yes (prf :: prf')

47+ No prf' => No (notAllThere prf')

lib/Decidable/Decidable.idrnew file+19

@@ -0,0 +1,19 @@

1+module Decidable.Decidable

2+

3+%access public

4+

5+--------------------------------------------------------------------------------

6+-- Typeclass for decidable n-ary Relations

7+--------------------------------------------------------------------------------

8+

9+using (t : Type)

10+ class Rel (p : t) where

11+ total liftRel : (Type -> Type) -> Type

12+

13+ class (Rel p) => Decidable (p : t) where

14+ total decide : liftRel Dec

15+

16+using (P : Type, p : P)

17+ data Given : Dec P -> Type where

18+ always : Given (Yes p)

19+

lib/Decidable/Equality.idr+1−1

@@ -75,7 +75,7 @@ total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _

7575leftNotRight refl impossible

7676

7777instance (DecEq a, DecEq b) => DecEq (Either a b) where

78− decEq {b=b} (Left x') (Left y') with (decEq x' y')

78+ decEq (Left x') (Left y') with (decEq x' y')

7979 | Yes p = Yes $ cong p

8080 | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h

8181 decEq (Right x') (Right y') with (decEq x' y')

lib/Decidable/Order.idrnew file+77

@@ -0,0 +1,77 @@

1+module Decidable.Order

2+

3+import Decidable.Decidable

4+import Decidable.Equality

5+

6+--------------------------------------------------------------------------------

7+-- Utility Lemmas

8+--------------------------------------------------------------------------------

9+

10+--------------------------------------------------------------------------------

11+-- Preorders and Posets

12+--------------------------------------------------------------------------------

13+

14+class Preorder t (po : t -> t -> Type) where

15+ total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c

16+ total reflexive : (a : t) -> po a a

17+

18+class (Preorder t po) => Poset t (po : t -> t -> Type) where

19+ total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

20+

21+--------------------------------------------------------------------------------

22+-- Natural numbers

23+--------------------------------------------------------------------------------

24+

25+data NatLTE : Nat -> Nat -> Type where

26+ nEqn : NatLTE n n

27+ nLTESm : NatLTE n m -> NatLTE n (S m)

28+

29+total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->

30+ NatLTE m n -> NatLTE n o ->

31+ NatLTE m o

32+NatLTEIsTransitive m n n mLTEn (nEqn) = mLTEn

33+NatLTEIsTransitive m n (S o) mLTEn (nLTESm nLTEo)

34+ = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)

35+

36+total NatLTEIsReflexive : (n : Nat) -> NatLTE n n

37+NatLTEIsReflexive _ = nEqn

38+

39+instance Preorder Nat NatLTE where

40+ transitive = NatLTEIsTransitive

41+ reflexive = NatLTEIsReflexive

42+

43+total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) -> po m n -> po n m -> m = n

44+NatLTEIsAntisymmetric n n nEqn nEqn = refl

45+NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible

46+NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible

47+

48+instance Poset Nat NatLTE where

49+ antisymmetric = NatLTEIsAntisymmetric

50+

51+total zeroNeverGreater : {n : Nat} -> NatLTE (S n) O -> _|_

52+zeroNeverGreater {n} (nLTESm _) impossible

53+zeroNeverGreater {n} nEqn impossible

54+

55+total

56+nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_

57+nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)

58+nGTSm {n} {m} disprf (nEqn) impossible

59+

60+total

61+decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)

62+decideNatLTE O O = Yes nEqn

63+decideNatLTE (S x) O = No zeroNeverGreater

64+decideNatLTE x (S y) with (decEq x (S y))

65+ | Yes eq = rewrite eq in Yes nEqn

66+ | No _ with (decideNatLTE x y)

67+ | Yes nLTEm = Yes (nLTESm nLTEm)

68+ | No nGTm = No (nGTSm nGTm)

69+

70+instance Rel NatLTE where

71+ liftRel P = (n : Nat) -> (m : Nat) -> P (NatLTE n m)

72+

73+instance Decidable NatLTE where

74+ decide = decideNatLTE

75+

76+lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)

77+lte m n = decide {p = NatLTE} m n

lib/Language/Reflection/Utils.idrnew file+185

@@ -0,0 +1,185 @@

1+module Language.Reflection.Utils

2+

3+--------------------------------------------------------

4+-- Tactic construction conveniences

5+--------------------------------------------------------

6+

7+seq : List Tactic -> Tactic

8+seq [] = GoalType "This is an impossible case" Trivial

9+seq [t] = t

10+seq (t::ts) = t `Seq` seq ts

11+

12+try : List Tactic -> Tactic

13+try [] = GoalType "This is an impossible case" Trivial

14+try [t] = t

15+try (t::ts) = t `Try` seq ts

16+

17+

18+--------------------------------------------------------

19+-- For use in tactic scripts

20+--------------------------------------------------------

21+mkPair : a -> b -> (a, b)

22+mkPair a b = (a, b)

23+

24+

25+--------------------------------------------------------

26+-- Tools for constructing proof terms directly

27+--------------------------------------------------------

28+

29+getUName : TTName -> Maybe String

30+getUName (UN n) = Just n

31+getUName (NS n ns) = getUName n

32+getUName _ = Nothing

33+

34+unApply : TT -> (TT, List TT)

35+unApply t = unA t []

36+ where unA : TT -> List TT -> (TT, List TT)

37+ unA (App fn arg) args = unA fn (arg::args)

38+ unA tm args = (tm, args)

39+

40+mkApp : TT -> List TT -> TT

41+mkApp tm [] = tm

42+mkApp tm (a::as) = mkApp (App tm a) as

43+

44+binderTy : (Eq t) => Binder t -> t

45+binderTy (Lam t) = t

46+binderTy (Pi t) = t

47+binderTy (Let t1 t2) = t1

48+binderTy (NLet t1 t2) = t1

49+binderTy (Hole t) = t

50+binderTy (GHole t) = t

51+binderTy (Guess t1 t2) = t1

52+binderTy (PVar t) = t

53+binderTy (PVTy t) = t

54+

55+instance Show TTName where

56+ show (UN str) = "(UN " ++ str ++ ")"

57+ show (NS n ns) = "(NS " ++ show n ++ " " ++ show ns ++ ")"

58+ show (MN i str) = "(MN " ++ show i ++ " " ++ show str ++ ")"

59+ show NErased = "NErased"

60+

61+instance Eq TTName where

62+ (UN str1) == (UN str2) = str1 == str2

63+ (NS n ns) == (NS n' ns') = n == n' && ns == ns'

64+ (MN i str) == (MN i' str') = i == i' && str == str'

65+ NErased == NErased = True

66+ x == y = False

67+

68+instance Show TTUExp where

69+ show (UVar i) = "(UVar " ++ show i ++ ")"

70+ show (UVal i) = "(UVal " ++ show i ++ ")"

71+

72+instance Eq TTUExp where

73+ (UVar i) == (UVar j) = i == j

74+ (UVal i) == (UVal j) = i == j

75+ x == y = False

76+

77+instance Show Const where

78+ show (I i) = "(I " ++ show i ++ ")"

79+ show (BI n) = "(BI " ++ show n ++ ")"

80+ show (Fl f) = "(Fl " ++ show f ++ ")"

81+ show (Ch c) = "(Ch " ++ show c ++ ")"

82+ show (Str str) = "(Str " ++ show str ++ ")"

83+ show IType = "IType"

84+ show BIType = "BIType"

85+ show FlType = "FlType"

86+ show ChType = "ChType"

87+ show StrType = "StrType"

88+ show (B8 b) = "(B8 ...)"

89+ show (B16 b) = "(B16 ...)"

90+ show (B32 b) = "(B32 ...)"

91+ show (B64 b) = "(B64 ...)"

92+ show B8Type = "B8Type"

93+ show B16Type = "B16Type"

94+ show B32Type = "B32Type"

95+ show B64Type = "B64Type"

96+ show PtrType = "PtrType"

97+ show VoidType = "VoidType"

98+ show Forgot = "Forgot"

99+

100+instance Eq Const where

101+ (I i) == (I i') = i == i'

102+ (BI n) == (BI n') = n == n'

103+ (Fl f) == (Fl f') = f == f'

104+ (Ch c) == (Ch c') = c == c'

105+ (Str str) == (Str str') = str == str'

106+ IType == IType = True

107+ BIType == BIType = True

108+ FlType == FlType = True

109+ ChType == ChType = True

110+ StrType == StrType = True

111+ (B8 b) == (B8 b') = False -- FIXME: b == b'

112+ (B16 b) == (B16 b') = False -- FIXME: b == b'

113+ (B32 b) == (B32 b') = False -- FIXME: b == b'

114+ (B64 b) == (B64 b') = False -- FIXME: b == b'

115+ B8Type == B8Type = True

116+ B16Type == B16Type = True

117+ B32Type == B32Type = True

118+ B64Type == B64Type = True

119+ PtrType == PtrType = True

120+ VoidType == VoidType = True

121+ Forgot == Forgot = True

122+ x == y = False

123+

124+instance Show NameType where

125+ show Bound = "Bound"

126+ show Ref = "Ref"

127+ show (DCon t ar) = "(DCon " ++ show t ++ " " ++ show ar ++ ")"

128+ show (TCon t ar) = "(TCon " ++ show t ++ " " ++ show ar ++ ")"

129+

130+instance Eq NameType where

131+ Bound == Bound = True

132+ Ref == Ref = True

133+ (DCon t ar) == (DCon t' ar') = t == t' && ar == ar'

134+ (TCon t ar) == (TCon t' ar') = t == t' && ar == ar'

135+ x == y = False

136+

137+instance (Show a) => Show (Binder a) where

138+ show (Lam t) = "(Lam " ++ show t ++ ")"

139+ show (Pi t) = "(Pi " ++ show t ++ ")"

140+ show (Let t1 t2) = "(Let " ++ show t1 ++ " " ++ show t2 ++ ")"

141+ show (NLet t1 t2) = "(NLet " ++ show t1 ++ " " ++ show t2 ++ ")"

142+ show (Hole t) = "(Hole " ++ show t ++ ")"

143+ show (GHole t) = "(GHole " ++ show t ++ ")"

144+ show (Guess t1 t2) = "(Guess " ++ show t1 ++ " " ++ show t2 ++ ")"

145+ show (PVar t) = "(PVar " ++ show t ++ ")"

146+ show (PVTy t) = "(PVTy " ++ show t ++ ")"

147+

148+instance (Eq a) => Eq (Binder a) where

149+ (Lam t) == (Lam t') = t == t'

150+ (Pi t) == (Pi t') = t == t'

151+ (Let t1 t2) == (Let t1' t2') = t1 == t1' && t2 == t2'

152+ (NLet t1 t2) == (NLet t1' t2') = t1 == t1' && t2 == t2'

153+ (Hole t) == (Hole t') = t == t'

154+ (GHole t) == (GHole t') = t == t'

155+ (Guess t1 t2) == (Guess t1' t2') = t1 == t1' && t2 == t2'

156+ (PVar t) == (PVar t') = t == t'

157+ (PVTy t) == (PVTy t') = t == t'

158+ x == y = False

159+

160+instance Show TT where

161+ show = my_show

162+ where %assert_total my_show : TT -> String

163+ my_show (P nt n t) = "(P " ++ show nt ++ " " ++ show n ++ " " ++ show t ++ ")"

164+ my_show (V i) = "(V " ++ show i ++ ")"

165+ my_show (Bind n b t) = "(Bind " ++ show n ++ " " ++ show b ++ " " ++ show t ++ ")"

166+ my_show (App t1 t2) = "(App " ++ show t1 ++ " " ++ show t2 ++ ")"

167+ my_show (TConst c) = "(TConst " ++ show c ++ ")"

168+ my_show (Proj tm i) = "(Proj " ++ show tm ++ " " ++ show i ++ ")"

169+ my_show Erased = "Erased"

170+ my_show Impossible = "Impossible"

171+ my_show (TType u) = "(TType " ++ show u ++ ")"

172+

173+instance Eq TT where

174+ a == b = equalp a b

175+ where %assert_total equalp : TT -> TT -> Bool

176+ equalp (P nt n t) (P nt' n' t') = nt == nt' && n == n' && t == t'

177+ equalp (V i) (V i') = i == i'

178+ equalp (Bind n b t) (Bind n' b' t') = n == n' && b == b' && t == t'

179+ equalp (App t1 t2) (App t1' t2') = t1 == t1' && t2 == t2'

180+ equalp (TConst c) (TConst c') = c == c'

181+ equalp (Proj tm i) (Proj tm' i') = tm == tm' && i == i'

182+ equalp Erased Erased = True

183+ equalp Impossible Impossible = True

184+ equalp (TType u) (TType u') = u == u'

185+ equalp x y = False

lib/Prelude.idr+11−2

@@ -178,6 +178,15 @@ atan x = prim__floatATan x

178178atan2 : Float -> Float -> Float

179179atan2 y x = atan (y/x)

180180

181+sinh : Float -> Float

182+sinh x = (exp x - exp (-x)) / 2

183+

184+cosh : Float -> Float

185+cosh x = (exp x + exp (-x)) / 2

186+

187+tanh : Float -> Float

188+tanh x = sinh x / cosh x

189+

181190sqrt : Float -> Float

182191sqrt x = prim__floatSqrt x

183192

@@ -189,12 +198,12 @@ ceiling x = prim__floatCeil x

189198

190199---- Ranges

191200

192−%assert_total

201+partial abstract

193202count : (Ord a, Num a) => a -> a -> a -> List a

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

195204 else []

196205

197−partial

206+partial abstract

198207countFrom : (Ord a, Num a) => a -> a -> List a

199208countFrom a inc = a :: lazy (countFrom (a + inc) inc)

200209

lib/Providers.idr+4−3

@@ -1,8 +1,9 @@

11module Providers

22

33public

4−data Provider a = Provide (IO a) | Error (IO String)

4+data Provider a = Provide a | Error String

55

66partial public

7−unProv : Provider a -> a

8−unProv (Provide x) = unsafePerformIO x

7+unProv : IO (Provider a) -> a

8+unProv p = case unsafePerformIO p of

9+ Provide x => x

lib/base.ipkg+4−2

@@ -13,15 +13,17 @@ modules = Builtins, Prelude, IO, System,

1313

1414 System.Concurrency.Raw, System.Concurrency.Process,

1515

16− Decidable.Equality,

16+ Decidable.Equality, Decidable.Decidable, Decidable.Order,

1717

1818 Uninhabited,

1919

2020 Providers,

2121

22− Language.Reflection,

22+ Language.Reflection, Language.Reflection.Utils,

2323

2424 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,

25+ Data.SortedMap, Data.SortedSet, Data.BoundedList,

26+ Data.Vect.Quantifiers,

2527

2628 Control.Monad.Identity, Control.Monad.State, Control.Category,

2729 Control.Arrow,

rts/Makefile+4−4

@@ -2,15 +2,15 @@ include ../config.mk

22

33OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_stdfgn.o idris_bitstring.o idris_opts.o idris_stats.o

44HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_stdfgn.h idris_bitstring.h idris_opts.h idris_stats.h

5−CFLAGS = -O2 -Wall

5+CFLAGS = -O2 -Wall -fPIC

66

77ifneq ($(GMP_INCLUDE_DIR),)

8− CFLAGS += -isystem $(GMP_INCLUDE_DIR)

8+ CFLAGS += -isystem $(GMP_INCLUDE_DIR)

99endif

1010

1111LIBTARGET = libidris_rts.a

1212

13−check : $(LIBTARGET)

13+check : $(LIBTARGET) $(DYLIBTARGET)

1414

1515$(LIBTARGET) : $(OBJS)

1616 ar r $(LIBTARGET) $(OBJS)

@@ -21,7 +21,7 @@ install : .PHONY

2121 install $(LIBTARGET) $(HDRS) $(TARGET)

2222

2323clean : .PHONY

24− rm -f $(OBJS) $(LIBTARGET)

24+ rm -f $(OBJS) $(LIBTARGET) $(DYLIBTARGET)

2525

2626idris_rts.o: idris_rts.h

2727

rts/idris_rts.c+45

@@ -186,6 +186,34 @@ VAL MKPTRc(VM* vm, void* ptr) {

186186 return cl;

187187}

188188

189+VAL MKB8(VM* vm, uint8_t bits8) {

190+ Closure* cl = allocate(vm, sizeof(Closure), 1);

191+ SETTY(cl, BITS8);

192+ cl -> info.bits8 = bits8;

193+ return cl;

194+}

195+

196+VAL MKB16(VM* vm, uint16_t bits16) {

197+ Closure* cl = allocate(vm, sizeof(Closure), 1);

198+ SETTY(cl, BITS16);

199+ cl -> info.bits16 = bits16;

200+ return cl;

201+}

202+

203+VAL MKB32(VM* vm, uint32_t bits32) {

204+ Closure* cl = allocate(vm, sizeof(Closure), 1);

205+ SETTY(cl, BITS32);

206+ cl -> info.bits32 = bits32;

207+ return cl;

208+}

209+

210+VAL MKB64(VM* vm, uint64_t bits64) {

211+ Closure* cl = allocate(vm, sizeof(Closure), 1);

212+ SETTY(cl, BITS64);

213+ cl -> info.bits64 = bits64;

214+ return cl;

215+}

216+

189217void PROJECT(VM* vm, VAL r, int loc, int arity) {

190218 int i;

191219 for(i = 0; i < arity; ++i) {

@@ -243,6 +271,23 @@ void dumpVal(VAL v) {

243271

244272}

245273

274+void idris_memset(void* ptr, i_int offset, VAL c, i_int size) {

275+ memset(((uint8_t*)ptr) + offset, c->info.bits8, size);

276+}

277+

278+int idris_peek(void* ptr, i_int offset) {

279+ uint8_t res = *(((uint8_t*)ptr) + offset);

280+ return (int)res;

281+}

282+

283+void idris_poke(void* ptr, i_int offset, VAL data) {

284+ *(((uint8_t*)ptr) + offset) = data->info.bits8;

285+}

286+

287+void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size) {

288+ memmove(dest + dest_offset, src + src_offset, size);

289+}

290+

246291VAL idris_castIntStr(VM* vm, VAL i) {

247292 Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16, 0);

248293 SETTY(cl, STRING);

rts/idris_rts.h+10

@@ -148,6 +148,10 @@ typedef intptr_t i_int;

148148VAL MKFLOAT(VM* vm, double val);

149149VAL MKSTR(VM* vm, char* str);

150150VAL MKPTR(VM* vm, void* ptr);

151+VAL MKB8(VM* vm, uint8_t b);

152+VAL MKB16(VM* vm, uint16_t b);

153+VAL MKB32(VM* vm, uint32_t b);

154+VAL MKB64(VM* vm, uint64_t b);

151155

152156// following versions don't take a lock when allocating

153157VAL MKFLOATc(VM* vm, double val);

@@ -203,6 +207,12 @@ VAL idris_castStrInt(VM* vm, VAL i);

203207VAL idris_castFloatStr(VM* vm, VAL i);

204208VAL idris_castStrFloat(VM* vm, VAL i);

205209

210+// Raw memory manipulation

211+void idris_memset(void* ptr, i_int offset, VAL c, i_int size);

212+int idris_peek(void* ptr, i_int offset);

213+void idris_poke(void* ptr, i_int offset, VAL data);

214+void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size);

215+

206216// String primitives

207217

208218VAL idris_concat(VM* vm, VAL l, VAL r);

rts/idris_stdfgn.h−1

@@ -8,7 +8,6 @@ void putStr(char* str);

88

99void* fileOpen(char* f, char* mode);

1010void fileClose(void* h);

11−//char* freadStr(void* h);

1211void fputStr(void*h, char* str);

1312

1413int isNull(void* ptr);

src/Core/CaseTree.hs+4−4

@@ -14,11 +14,11 @@ import Debug.Trace

1414data CaseDef = CaseDef [Name] SC [Term]

1515 deriving Show

1616

17−data SC' t = Case Name [CaseAlt' t] -- invariant: lowest tags first

18− | ProjCase t [CaseAlt' t] -- special case for projections

17+data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first

18+ | ProjCase t [CaseAlt' t] -- ^ special case for projections

1919 | STerm t

20− | UnmatchedCase String -- error message

21− | ImpossibleCase -- already checked to be impossible

20+ | UnmatchedCase String -- ^ error message

21+ | ImpossibleCase -- ^ already checked to be impossible

2222 deriving (Eq, Ord, Functor)

2323{-!

2424deriving instance Binary SC

src/Core/CoreParser.hs+1−1

@@ -466,7 +466,7 @@ idrisMakeTokenParser languageDef

466466

467467 number base baseDigit

468468 = do{ digits <- many1 baseDigit

469− ; let n = foldl (\x d -> base*x + toInteger (digitToInt d)) 0 digits

469+ ; let n = foldl' (\x d -> base*x + toInteger (digitToInt d)) 0 digits

470470 ; seq n (return n)

471471 }

472472

src/Core/Elaborate.hs+16−3

@@ -171,7 +171,7 @@ checkInjective (tm, l, r) = do ctxt <- get_context

171171 if isInj ctxt tm then return ()

172172 else lift $ tfail (NotInjective tm l r)

173173 where isInj ctxt (P _ n _)

174− | isConName Nothing n ctxt = True

174+ | isConName n ctxt = True

175175 isInj ctxt (App f a) = isInj ctxt f

176176 isInj ctxt (Constant _) = True

177177 isInj ctxt (TType _) = True

@@ -210,7 +210,7 @@ unique_hole' reusable n

210210uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux Name

211211uniqueNameCtxt ctxt n hs

212212 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs

213− | [_] <- lookupTy Nothing n ctxt = uniqueNameCtxt ctxt (nextName n) hs

213+ | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs

214214 | otherwise = return n

215215

216216elog :: String -> Elab' aux ()

@@ -356,7 +356,7 @@ prepare_apply fn imps =

356356 mkClaims _ _ _ _

357357 | Var n <- fn

358358 = do ctxt <- get_context

359− case lookupTy Nothing n ctxt of

359+ case lookupTy n ctxt of

360360 [] -> lift $ tfail $ NoSuchVariable n

361361 _ -> fail $ "Too many arguments for " ++ show fn

362362 | otherwise = fail $ "Too many arguments for " ++ show fn

@@ -525,6 +525,19 @@ arg n tyhole = do ty <- unique_hole tyhole

525525 claim ty RType

526526 forall n (Var ty)

527527

528+-- try a tactic, if it adds any unification problem, return an error

529+no_errors :: Elab' aux () -> Elab' aux ()

530+no_errors tac

531+ = do ps <- get_probs

532+ tac

533+ ps' <- get_probs

534+ if (length ps' > length ps) then

535+ case reverse ps' of

536+ ((x,y,env,err) : _) ->

537+ let env' = map (\(x, b) -> (x, binderTy b)) env in

538+ lift $ tfail $ CantUnify False x y err env' 0

539+ else return ()

540+

528541-- Try a tactic, if it fails, try another

529542try :: Elab' aux a -> Elab' aux a -> Elab' aux a

530543try t1 t2 = try' t1 t2 False

src/Core/Evaluate.hs+34−34

@@ -9,7 +9,7 @@ module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

99 addDatatype, addCasedef, simplifyCasedef, addOperator,

1010 lookupNames, lookupTy, lookupP, lookupDef, lookupVal,

1111 lookupTotal, lookupTyEnv, isConName, isFnName,

12− Value(..)) where

12+ Value(..), Quote(..), evalState, initEval) where

1313

1414import Debug.Trace

1515import Control.Monad.State

@@ -149,7 +149,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

149149 ev ntimes_in stk top env (P Ref n ty)

150150 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

151151 | (True, ntimes) <- usable simpl n ntimes_in

152− = do let val = lookupDefAcc Nothing n atRepl ctxt

152+ = do let val = lookupDefAcc n atRepl ctxt

153153 case val of

154154 [(Function _ tm, Public)] ->

155155 ev ntimes (n:stk) True env tm

@@ -220,7 +220,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

220220 _ -> return $ unload env f args

221221 | (True, ntimes) <- usable simpl n ntimes_in

222222 = traceWhen traceon (show stk) $

223− do let val = lookupDefAcc Nothing n atRepl ctxt

223+ do let val = lookupDefAcc n atRepl ctxt

224224 case val of

225225 [(CaseOp inl inr _ _ _ ns tree _ _, acc)]

226226 | acc == Public -> -- unoptimised version

@@ -243,7 +243,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

243243 apply ntimes stk top env f [] = return f

244244

245245-- specApply stk env f@(VP Ref n ty) args

246−-- = case lookupCtxt Nothing n statics of

246+-- = case lookupCtxt n statics of

247247-- [as] -> if or as

248248-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $

249249-- return $ unload env f args

@@ -397,7 +397,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

397397 ev :: [HNF] -> TT Name -> Eval HNF

398398 ev env (P _ n ty)

399399 | Just (Let t v) <- lookup n genv = ev env v

400− ev env (P Ref n ty) = case lookupDef Nothing n ctxt of

400+ ev env (P Ref n ty) = case lookupDef n ctxt of

401401 [Function _ t] -> ev env t

402402 [TyDecl nt ty] -> return $ HP nt n ty

403403 [CaseOp inl _ _ _ _ [] tree _ _] ->

@@ -430,7 +430,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

430430 app <- apply env sc' as

431431 wknH (-1) app

432432 apply env (HP Ref n ty) args

433− | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt

433+ | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef n ctxt

434434 = do c <- evCase env ns args tree

435435 case c of

436436 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

@@ -565,7 +565,7 @@ convEq ctxt = ceq [] where

565565 caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True

566566 caseeq ps _ _ = return False

567567

568− sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of

568+ sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of

569569 ([Function _ xdef], [Function _ ydef])

570570 -> ceq ((x,y):ps) xdef ydef

571571 ([CaseOp _ _ _ _ _ _ xdef _ _],

@@ -669,7 +669,7 @@ data Context = MkContext {

669669 uconstraints :: [UConstraint],

670670 next_tvar :: Int,

671671 definitions :: Ctxt (Def, Accessibility, Totality)

672− }

672+ } deriving Show

673673

674674-- | The initial empty context

675675initContext = MkContext [] 0 emptyContext

@@ -730,7 +730,7 @@ addCasedef :: Name -> Bool -> Bool -> Bool -> Bool ->

730730 Type -> Context -> Context

731731addCasedef n alwaysInline tcase covering asserted ps_in ps psrt ty uctxt

732732 = let ctxt = definitions uctxt

733− access = case lookupDefAcc Nothing n False uctxt of

733+ access = case lookupDefAcc n False uctxt of

734734 [(_, acc)] -> acc

735735 _ -> Public

736736 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,

@@ -747,7 +747,7 @@ addCasedef n alwaysInline tcase covering asserted ps_in ps psrt ty uctxt

747747simplifyCasedef :: Name -> Context -> Context

748748simplifyCasedef n uctxt

749749 = let ctxt = definitions uctxt

750− ctxt' = case lookupCtxt Nothing n ctxt of

750+ ctxt' = case lookupCtxt n ctxt of

751751 [(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->

752752 ctxt -- nothing to simplify (or already done...)

753753 [(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->

@@ -780,40 +780,40 @@ addOperator n ty a op uctxt

780780

781781tfst (a, _, _) = a

782782

783−lookupNames :: Maybe [String] -> Name -> Context -> [Name]

784−lookupNames root n ctxt

785− = let ns = lookupCtxtName root n (definitions ctxt) in

783+lookupNames :: Name -> Context -> [Name]

784+lookupNames n ctxt

785+ = let ns = lookupCtxtName n (definitions ctxt) in

786786 map fst ns

787787

788−lookupTy :: Maybe [String] -> Name -> Context -> [Type]

789−lookupTy root n ctxt

790− = do def <- lookupCtxt root n (definitions ctxt)

788+lookupTy :: Name -> Context -> [Type]

789+lookupTy n ctxt

790+ = do def <- lookupCtxt n (definitions ctxt)

791791 case tfst def of

792792 (Function ty _) -> return ty

793793 (TyDecl _ ty) -> return ty

794794 (Operator ty _ _) -> return ty

795795 (CaseOp _ _ ty _ _ _ _ _ _) -> return ty

796796

797−isConName :: Maybe [String] -> Name -> Context -> Bool

798−isConName root n ctxt

799− = or $ do def <- lookupCtxt root n (definitions ctxt)

797+isConName :: Name -> Context -> Bool

798+isConName n ctxt

799+ = or $ do def <- lookupCtxt n (definitions ctxt)

800800 case tfst def of

801801 (TyDecl (DCon _ _) _) -> return True

802802 (TyDecl (TCon _ _) _) -> return True

803803 _ -> return False

804804

805−isFnName :: Maybe [String] -> Name -> Context -> Bool

806−isFnName root n ctxt

807− = or $ do def <- lookupCtxt root n (definitions ctxt)

805+isFnName :: Name -> Context -> Bool

806+isFnName n ctxt

807+ = or $ do def <- lookupCtxt n (definitions ctxt)

808808 case tfst def of

809809 (Function _ _) -> return True

810810 (Operator _ _ _) -> return True

811811 (CaseOp _ _ _ _ _ _ _ _ _) -> return True

812812 _ -> return False

813813

814−lookupP :: Maybe [String] -> Name -> Context -> [Term]

815−lookupP root n ctxt

816− = do def <- lookupCtxt root n (definitions ctxt)

814+lookupP :: Name -> Context -> [Term]

815+lookupP n ctxt

816+ = do def <- lookupCtxt n (definitions ctxt)

817817 p <- case def of

818818 (Function ty tm, a, _) -> return (P Ref n ty, a)

819819 (TyDecl nt ty, a, _) -> return (P nt n ty, a)

@@ -823,22 +823,22 @@ lookupP root n ctxt

823823 Hidden -> []

824824 _ -> return (fst p)

825825

826−lookupDef :: Maybe [String] -> Name -> Context -> [Def]

827−lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt)

826+lookupDef :: Name -> Context -> [Def]

827+lookupDef n ctxt = map tfst $ lookupCtxt n (definitions ctxt)

828828

829−lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context ->

829+lookupDefAcc :: Name -> Bool -> Context ->

830830 [(Def, Accessibility)]

831−lookupDefAcc root n mkpublic ctxt

832− = map mkp $ lookupCtxt root n (definitions ctxt)

831+lookupDefAcc n mkpublic ctxt

832+ = map mkp $ lookupCtxt n (definitions ctxt)

833833 where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)

834834

835835lookupTotal :: Name -> Context -> [Totality]

836−lookupTotal n ctxt = map mkt $ lookupCtxt Nothing n (definitions ctxt)

836+lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

837837 where mkt (d, a, t) = t

838838

839−lookupVal :: Maybe [String] -> Name -> Context -> [Value]

840−lookupVal root n ctxt

841− = do def <- lookupCtxt root n (definitions ctxt)

839+lookupVal :: Name -> Context -> [Value]

840+lookupVal n ctxt

841+ = do def <- lookupCtxt n (definitions ctxt)

842842 case tfst def of

843843 (Function _ htm) -> return (veval ctxt [] htm)

844844 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

src/Core/Execute.hs+438−76

@@ -1,3 +1,4 @@

1+{-# LANGUAGE PatternGuards, ExistentialQuantification #-}

12module Core.Execute (execute) where

23

34import Idris.AbsSyntax

@@ -5,104 +6,456 @@ import Idris.AbsSyntaxTree

56

67import Core.TT

78import Core.Evaluate

9+import Core.CaseTree

810

911import Debug.Trace

1012

1113import Util.DynamicLinker

14+import Util.System

1215

1316import Control.Applicative hiding (Const)

1417import Control.Monad.Trans

18+import Control.Monad.Trans.State.Strict

19+import Control.Monad.Trans.Error

1520import Control.Monad

1621import Data.Maybe

22+import qualified Data.Map as M

1723

1824import Foreign.LibFFI

1925import Foreign.C.String

2026import Foreign.Marshal.Alloc (free)

27+import Foreign.Ptr

28+

29+import System.IO

30+

31+

32+data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

33+

34+data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs

35+ , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness

36+ , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad

37+ , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

38+ }

39+

40+data ExecVal = EP NameType Name ExecVal

41+ | EV Int

42+ | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)

43+ | EApp ExecVal ExecVal

44+ | EType UExp

45+ | EErased

46+ | EConstant Const

47+ | forall a. EPtr (Ptr a)

48+ | EThunk Int

49+ | EHandle Handle

50+

51+instance Show ExecVal where

52+ show (EP _ n _) = show n

53+ show (EV i) = "!!V" ++ show i ++ "!!"

54+ show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"

55+ show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

56+ show (EType _) = "Type"

57+ show EErased = "[__]"

58+ show (EConstant c) = show c

59+ show (EPtr p) = "<<ptr " ++ show p ++ ">>"

60+ show (EThunk i) = "<<thunk " ++ show i ++ ">>"

61+ show (EHandle h) = "<<handle " ++ show h ++ ">>"

62+

63+toTT :: ExecVal -> Exec Term

64+toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

65+toTT (EV i) = return $ V i

66+toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

67+ b' <- fixBinder b

68+ Bind n b' <$> toTT body'

69+ where fixBinder (Lam t) = Lam <$> toTT t

70+ fixBinder (Pi t) = Pi <$> toTT t

71+ fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

72+ fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

73+ fixBinder (Hole t) = Hole <$> toTT t

74+ fixBinder (GHole t) = GHole <$> toTT t

75+ fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

76+ fixBinder (PVar t) = PVar <$> toTT t

77+ fixBinder (PVTy t) = PVTy <$> toTT t

78+toTT (EApp e1 e2) = do e1' <- toTT e1

79+ e2' <- toTT e2

80+ return $ App e1' e2'

81+toTT (EType u) = return $ TType u

82+toTT EErased = return Erased

83+toTT (EConstant c) = return (Constant c)

84+toTT (EThunk i) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(force i) >>= toTT

85+toTT (EHandle _) = return Erased

86+

87+unApplyV :: ExecVal -> (ExecVal, [ExecVal])

88+unApplyV tm = ua [] tm

89+ where ua args (EApp f a) = ua (a:args) f

90+ ua args t = (t, args)

91+

92+mkEApp :: ExecVal -> [ExecVal] -> ExecVal

93+mkEApp f [] = f

94+mkEApp f (a:args) = mkEApp (EApp f a) args

95+

96+initState :: Idris ExecState

97+initState = do ist <- getIState

98+ return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)

99+

100+type Exec = ErrorT String (StateT ExecState IO)

101+

102+runExec :: Exec a -> ExecState -> IO (Either String a)

103+runExec ex st = fst <$> runStateT (runErrorT ex) st

104+

105+getExecState :: Exec ExecState

106+getExecState = lift get

107+

108+putExecState :: ExecState -> Exec ()

109+putExecState = lift . put

110+

111+execFail :: String -> Exec a

112+execFail = throwError

113+

114+execIO :: IO a -> Exec a

115+execIO = lift . lift

116+

117+delay :: ExecEnv -> Context -> Term -> Exec ExecVal

118+delay env ctxt tm =

119+ do st <- getExecState

120+ let i = exec_next_thunk st

121+ putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)

122+ , exec_next_thunk = exec_next_thunk st + 1

123+ }

124+ return $ EThunk i

125+

126+force :: Int -> Exec ExecVal

127+force i = do st <- getExecState

128+ case M.lookup i (exec_thunks st) of

129+ Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm

130+ case tm' of

131+ EThunk i ->

132+ do res <- force i

133+ update res i

134+ return res

135+ _ -> do update tm' i

136+ return tm'

137+ Just (Forced tm) -> return tm

138+ Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"

139+ where update :: ExecVal -> Int -> Exec ()

140+ update tm i = do est <- getExecState

141+ putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }

142+

143+tryForce :: ExecVal -> Exec ExecVal

144+tryForce (EThunk i) = force i

145+tryForce tm = return tm

146+

147+debugThunks :: Exec ()

148+debugThunks = do st <- getExecState

149+ execIO $ putStrLn (take 4000 (show (exec_thunks st)))

150+

151+execute :: Term -> Idris Term

152+execute tm = do est <- initState

153+ ctxt <- getContext

154+ res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm

155+ toTT res

156+ case res of

157+ Left err -> fail err

158+ Right tm' -> return tm'

159+

160+ioWrap :: ExecVal -> ExecVal

161+ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]

162+

163+ioUnit :: ExecVal

164+ioUnit = ioWrap (EP Ref unitCon EErased)

165+

166+type ExecEnv = [(Name, ExecVal)]

167+

168+doExec :: ExecEnv -> Context -> Term -> Exec ExecVal

169+doExec env ctxt p@(P Ref n ty) =

170+ do let val = lookupDef n ctxt

171+ case val of

172+ [Function _ tm] -> doExec env ctxt tm

173+ [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def

174+ [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later

175+ [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

176+ doExec env ctxt tm

177+ [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)

178+ thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

179+doExec env ctxt p@(P Bound n ty) =

180+ case lookup n env of

181+ Nothing -> execFail "not found"

182+ Just tm -> return tm

183+doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)

184+doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)

185+doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

186+ | otherwise = execFail "env too small"

187+doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

188+ doExec ((n, v'):env) ctxt body

189+doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

190+doExec env ctxt tm@(Bind n b body) = return $

191+ EBind n (fmap (\_->EErased) b)

192+ (\arg -> doExec ((n, arg):env) ctxt body)

193+doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)

194+doExec env ctxt (Constant c) = return (EConstant c)

195+doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

196+ doExec env ctxt ((x:xs) !! i)

197+doExec env ctxt Erased = return EErased

198+doExec env ctxt Impossible = fail "Tried to execute an impossible case"

199+doExec env ctxt (TType u) = return (EType u)

200+

201+execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal

202+execApp env ctxt (f, args) = do newF <- doExec env ctxt f

203+ laziness <- (++ repeat False) <$> (getLaziness newF)

204+ newArgs <- mapM argExec (zip args laziness)

205+ execApp' env ctxt newF newArgs

206+ where getLaziness (EP _ (UN "lazy") _) = return [False, True]

207+ getLaziness (EP _ n _) = do est <- getExecState

208+ let argInfo = exec_implicits est

209+ case lookupCtxtName n argInfo of

210+ [] -> return (repeat False)

211+ [ps] -> return $ map lazyarg (snd ps)

212+ many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)

213+ getLaziness _ = return (repeat False) -- ok due to zip above

214+ argExec :: (Term, Bool) -> Exec ExecVal

215+ argExec (tm, False) = doExec env ctxt tm

216+ argExec (tm, True) = delay env ctxt tm

217+

218+

219+execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

220+execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls

221+execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =

222+ execApp' env ctxt v rest

223+

224+execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =

225+ do v'' <- tryForce v'

226+ res <- execApp' env ctxt k [v''] >>= tryForce

227+ execApp' env ctxt res rest

228+execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =

229+ do v' <- tryForce v

230+ execApp' env ctxt (mkEApp con [tp, v']) rest

231+

232+-- Special cases arising from not having access to the C RTS in the interpreter

233+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)

234+ | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)

235+ execApp' env ctxt ioUnit rest

236+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

237+ | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of

238+ "r" -> return ReadMode

239+ "w" -> return WriteMode

240+ "a" -> return AppendMode

241+ "rw" -> return ReadWriteMode

242+ "wr" -> return ReadWriteMode

243+ "r+" -> return ReadWriteMode

244+ _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)

245+ h <- execIO $ openFile f m

246+ execApp' env ctxt (ioWrap (EHandle h)) rest

247+

248+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)

249+ | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h

250+ let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

251+ execApp' env ctxt res rest

252+

253+execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)

254+ | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h

255+ execApp' env ctxt ioUnit rest

256+

257+

258+execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn

259+ , length xs >= length argTs =

260+ do res <- stepForeign (ty:fn:take (length argTs) xs)

261+ case res of

262+ Nothing -> fail "Could not call foreign function"

263+ Just r -> return (mkEApp r (drop (length argTs) xs))

264+ | otherwise = return (mkEApp f args)

265+

266+execApp' env ctxt f@(EP _ n _) args =

267+ do let val = lookupDef n ctxt

268+ case val of

269+ [Function _ tm] -> fail "should already have been eval'd"

270+ [TyDecl nt ty] -> return $ mkEApp f args

271+ [Operator tp arity op] ->

272+ if length args >= arity

273+ then do args' <- mapM tryForce $ take arity args

274+ case getOp n args' of

275+ Just res -> do r <- res

276+ execApp' env ctxt r (drop arity args)

277+ Nothing -> return (mkEApp f args)

278+ else return (mkEApp f args)

279+ [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

280+ do rhs <- doExec env ctxt tm

281+ execApp' env ctxt rhs args

282+ [CaseOp _ _ _ _ _ ns sc _ _] ->

283+ do res <- execCase env ctxt ns sc args

284+ return $ fromMaybe (mkEApp f args) res

285+ thing -> return $ mkEApp f args

286+ where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

287+ getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =

288+ primRes I (i1 + i2)

289+ getOp (UN "prim__charToInt") [EConstant (Ch c)] =

290+ primRes I (fromEnum c)

291+ getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =

292+ primRes Str (s1 ++ s2)

293+ getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =

294+ primResBool (c1 == c2)

295+ getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =

296+ primResBool (i1 == i2)

297+ getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =

298+ primResBool (s1 == s2)

299+ getOp (UN "prim__intToFloat") [EConstant (I i)] =

300+ primRes Fl (fromRational (toRational i))

301+ getOp (UN "prim__intToStr") [EConstant (I i)] =

302+ primRes Str (show i)

303+ getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =

304+ primResBool (i1 < i2)

305+ getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =

306+ primRes BI (i1 * i2)

307+ getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =

308+ primRes Fl (i1 * i2)

309+ getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =

310+ primRes I (i1 * i2)

311+ getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =

312+ Just $ do line <- execIO getLine

313+ return (EConstant (Str line))

314+ getOp (UN "prim__readString") [EHandle h] =

315+ Just $ do contents <- execIO $ hGetLine h

316+ return (EConstant (Str contents))

317+ getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =

318+ primRes Str (c:s)

319+ getOp (UN "prim__strHead") [EConstant (Str (c:s))] =

320+ primRes Ch c

321+ getOp (UN "prim__strRev") [EConstant (Str s)] =

322+ primRes Str (reverse s)

323+ getOp (UN "prim__strTail") [EConstant (Str (c:s))] =

324+ primRes Str s

325+ getOp (UN "prim__subFloat") [EConstant (Fl i1), EConstant (Fl i2)] =

326+ primRes Fl (i1 - i2)

327+ getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =

328+ primRes I (i1 - i2)

329+ getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing

330+

331+ primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)

332+ primRes constr = Just . return . EConstant . constr

333+

334+ primResBool :: Bool -> Maybe (Exec ExecVal)

335+ primResBool b = primRes I (if b then 1 else 0)

336+

337+execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

338+ let (f', as) = unApplyV ret

339+ execApp' env ctxt f' (as ++ args)

340+execApp' env ctxt (EThunk i) args = do f <- force i

341+ execApp' env ctxt f args

342+execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)

343+execApp' env ctxt f args = return (mkEApp f args)

344+

345+

346+

347+

348+

349+-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,

350+-- evaluates them, then begins the checks for matching cases.

351+execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)

352+execCase env ctxt ns sc args =

353+ let arity = length ns in

354+ if arity <= length args

355+ then do let amap = zip ns args

356+ caseRes <- execCase' env ctxt amap sc

357+ case caseRes of

358+ Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

359+ Nothing -> return Nothing

360+ else return Nothing

361+

362+-- | Take bindings and a case tree and examines them, executing the matching case if possible.

363+execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)

364+execCase' env ctxt amap (UnmatchedCase _) = return Nothing

365+execCase' env ctxt amap (STerm tm) =

366+ Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

367+execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

368+ do tm' <- tryForce tm

369+ case chooseAlt tm' alts of

370+ Just (newCase, newBindings) ->

371+ let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

372+ execCase' env ctxt amap' newCase

373+ Nothing -> return Nothing

374+

375+chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])

376+chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])

377+chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])

378+chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm

379+ , cn == n = Just (sc, zip ns args)

380+ | otherwise = chooseAlt tm alts

381+chooseAlt tm (_:alts) = chooseAlt tm alts

382+chooseAlt _ [] = Nothing

21383

22−-- | Attempt to perform a side effect. Return either Just the next step in

23−-- evaluation (after performing the side effect through IO), or Nothing if no

24−-- IO was performed.

25−--

26−-- This function is exceedingly generous about what it will accept in order to

27−-- enable convenient testing at the REPL.

28−step :: TT Name -> Idris (Maybe (TT Name))

29−step tm = step' (unApply tm)

30− where step' (P _ (UN "unsafePerformIO") _, [_, arg] ) = step arg -- Only step if arg can be stepped

31− step' (P _ (UN "mkForeign") _, args) = stepForeign args

32− step' (P _ (UN "prim__IO") _, [_, arg]) = return (Just arg)

33− step' (P _ (UN "prim__readString") _, [(P _ (UN "prim__stdin") _)]) =

34− do line <- lift $ getLine

35− return . Just . Constant . Str $ line

36− step' _ = return Nothing

37−

38−-- | Perform side effects until no more can be performed, then return the

39−-- resulting term (possibly the argument).

40−execute :: TT Name -> Idris (TT Name)

41−execute tm = case unApply tm of

42− (P _ (UN "unsafePerformIO") _, [_, arg] ) -> execute' arg

43− _ -> return tm

44− where execute' tm = do stepped <- step tm

45− case stepped of

46− Nothing -> return tm

47− Just tm' -> execute' tm'

48384

49385

50386

52388

389+idrisType :: FTy -> ExecVal

390+idrisType FUnit = EP Ref unitTy EErased

391+idrisType ft = EConstant (idr ft)

392+ where idr FInt = IType

393+ idr FFloat = FlType

394+ idr FChar = ChType

395+ idr FString = StrType

396+ idr FPtr = PtrType

397+

53398data Foreign = FFun String [FTy] FTy deriving Show

54399

55−call :: Foreign -> [TT Name] -> Idris (Maybe (TT Name))

56−call (FFun name argTypes retType) args = do fn <- findForeign name

57− case fn of

58− Nothing -> return Nothing

59− Just f -> return . Just =<< call' f args retType

60− where call' :: ForeignFun -> [TT Name] -> FTy -> Idris (TT Name)

61− call' (Fun _ h) args FInt = do res <- lift $ callFFI h retCInt (prepArgs args)

62− return (Constant (I (fromIntegral res)))

63− call' (Fun _ h) args FFloat = do res <- lift $ callFFI h retCDouble (prepArgs args)

64− return (Constant (Fl (realToFrac res)))

65− call' (Fun _ h) args FChar = do res <- lift $ callFFI h retCChar (prepArgs args)

66− return (Constant (Ch (castCCharToChar res)))

67− call' (Fun _ h) args FString = do res <- lift $ callFFI h retCString (prepArgs args)

68− hStr <- lift $ peekCString res

400+

401+call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)

402+call (FFun name argTypes retType) args =

403+ do fn <- findForeign name

404+ case fn of

405+ Nothing -> return Nothing

406+ Just f -> do res <- call' f args retType

407+ return . Just . ioWrap $ res

408+ where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal

409+ call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)

410+ return (EConstant (I (fromIntegral res)))

411+ call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)

412+ return (EConstant (Fl (realToFrac res)))

413+ call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)

414+ return (EConstant (Ch (castCCharToChar res)))

415+ call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)

416+ hStr <- execIO $ peekCString res

69417-- lift $ free res

70− return (Constant (Str hStr))

71−-- awaiting Const constructor for pointers

72−-- call' (Fun _ h) args FPtr = do res <- lift $ callFFI h retPtr (prepArgs args)

73−-- return (Constant (Ch (castCCharToChar res)))

74− call' (Fun _ h) args FUnit = do res <- lift $ callFFI h retVoid (prepArgs args)

75− return (P Ref unitCon (P Ref unitTy (TType (UVal 0)))) -- FIXME check universe level

418+ return (EConstant (Str hStr))

419+

420+ call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)

421+ return (EPtr res)

422+ call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)

423+ return (EP Ref unitCon EErased)

424+-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)

425+

76426

77427 prepArgs = map prepArg

78− prepArg (Constant (I i)) = argCInt (fromIntegral i)

79− prepArg (Constant (Fl f)) = argCDouble (realToFrac f)

80− prepArg (Constant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

81− prepArg (Constant (Str s)) = argString s

428+ prepArg (EConstant (I i)) = argCInt (fromIntegral i)

429+ prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)

430+ prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

431+ prepArg (EConstant (Str s)) = argString s

432+ prepArg (EPtr p) = argPtr p

433+ prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined

82434

83435

84436

85−foreignFromTT :: TT Name -> Maybe Foreign

86−foreignFromTT t = case (unApply t) of

87− (_, [(Constant (Str name)), args, ret]) ->

88− do argTy <- unList args

437+foreignFromTT :: ExecVal -> Maybe Foreign

438+foreignFromTT t = case (unApplyV t) of

439+ (_, [(EConstant (Str name)), args, ret]) ->

440+ do argTy <- unEList args

89441 argFTy <- sequence $ map getFTy argTy

90442 retFTy <- getFTy ret

91443 return $ FFun name argFTy retFTy

92− _ -> Nothing

93−

94−getFTy :: TT Name -> Maybe FTy

95−getFTy (P _ (UN t) _) = case t of

96− "FInt" -> Just FInt

97− "FFloat" -> Just FFloat

98− "FChar" -> Just FChar

99− "FString" -> Just FString

100− "FPtr" -> Just FPtr

101− "FUnit" -> Just FUnit

102− _ -> Nothing

444+ _ -> trace "failed to construct ffun" Nothing

445+

446+getFTy :: ExecVal -> Maybe FTy

447+getFTy (EP _ (UN t) _) =

448+ case t of

449+ "FInt" -> Just FInt

450+ "FFloat" -> Just FFloat

451+ "FChar" -> Just FChar

452+ "FString" -> Just FString

453+ "FPtr" -> Just FPtr

454+ "FUnit" -> Just FUnit

455+ _ -> Nothing

103456getFTy _ = Nothing

104457

105−unList :: TT Name -> Maybe [TT Name]

458+unList :: Term -> Maybe [Term]

106459unList tm = case unApply tm of

107460 (nil, [_]) -> Just []

108461 (cons, ([_, x, xs])) ->

@@ -110,11 +463,20 @@ unList tm = case unApply tm of

110463 return $ x:rest

111464 (f, args) -> Nothing

112465

113−toConst :: TT Name -> Maybe Const

466+unEList :: ExecVal -> Maybe [ExecVal]

467+unEList tm = case unApplyV tm of

468+ (nil, [_]) -> Just []

469+ (cons, ([_, x, xs])) ->

470+ do rest <- unEList xs

471+ return $ x:rest

472+ (f, args) -> Nothing

473+

474+

475+toConst :: Term -> Maybe Const

114476toConst (Constant c) = Just c

115477toConst _ = Nothing

116478

117−stepForeign :: [TT Name] -> Idris (Maybe (TT Name))

479+stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)

118480stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn

119481 f' <- case (call <$> ffun) of

120482 Just f -> f args

@@ -130,15 +492,15 @@ mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs

130492 Just x'' -> return (x'':rest)

131493 Nothing -> return rest

132494

133−findForeign :: String -> Idris (Maybe ForeignFun)

134−findForeign fn = do i <- getIState

135− let libs = idris_dynamic_libs i

136− fns <- mapMaybeM (lift . tryLoadFn fn) libs

495+findForeign :: String -> Exec (Maybe ForeignFun)

496+findForeign fn = do est <- getExecState

497+ let libs = exec_dynamic_libs est

498+ fns <- mapMaybeM getFn libs

137499 case fns of

138500 [f] -> return (Just f)

139− [] -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" not found"

501+ [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"

140502 return Nothing

141− fs -> do iputStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++

142− show (length fs) ++ " occurrences."

503+ fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++

504+ show (length fs) ++ " occurrences."

143505 return Nothing

144−

506+ where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)

src/Core/ProofShell.hs+1−1

@@ -41,7 +41,7 @@ processCommand (Eval t) state =

4141 (state, show nf ++ " : " ++ show ty)

4242 err -> (state, show err)

4343processCommand (Print n) state =

44− case lookupDef Nothing n (ctxt state) of

44+ case lookupDef n (ctxt state) of

4545 [tm] -> (state, show tm)

4646 _ -> (state, "No such name")

4747processCommand (Tac e) state

src/Core/ProofState.hs+1−1

@@ -162,7 +162,7 @@ unify' ctxt env topx topy =

162162-- -- " in " ++ show env ++

163163-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

164164-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"

165−-- -- ++ show (pterm ps)

165+-- ++ show (pterm ps)

166166-- ++ "\n----------") $

167167 case fails of

168168-- [] -> return u

src/Core/TT.hs+9−6

@@ -244,8 +244,8 @@ addDef n v ctxt = case Map.lookup (nsroot n) ctxt of

244244

245245-}

246246

247−lookupCtxtName :: Maybe [String] -> Name -> Ctxt a -> [(Name, a)]

248−lookupCtxtName nspace n ctxt = case Map.lookup (nsroot n) ctxt of

247+lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]

248+lookupCtxtName n ctxt = case Map.lookup (nsroot n) ctxt of

249249 Just xs -> filterNS (Map.toList xs)

250250 Nothing -> []

251251 where

@@ -258,12 +258,12 @@ lookupCtxtName nspace n ctxt = case Map.lookup (nsroot n) ctxt of

258258 nsmatch (NS _ _) _ = False

259259 nsmatch looking found = True

260260

261−lookupCtxt :: Maybe [String] -> Name -> Ctxt a -> [a]

262−lookupCtxt ns n ctxt = map snd (lookupCtxtName ns n ctxt)

261+lookupCtxt :: Name -> Ctxt a -> [a]

262+lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)

263263

264264updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

265265updateDef n f ctxt

266− = let ds = lookupCtxtName Nothing n ctxt in

266+ = let ds = lookupCtxtName n ctxt in

267267 foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds

268268

269269toAlist :: Ctxt a -> [(Name, a)]

@@ -430,7 +430,10 @@ instance Show UConstraint where

430430

431431type UCs = (Int, [UConstraint])

432432

433−data NameType = Bound | Ref | DCon Int Int | TCon Int Int

433+data NameType = Bound

434+ | Ref

435+ | DCon Int Int -- ^ Data constructor; Ints are tag and arity

436+ | TCon Int Int -- ^ Type constructor; Ints are tag and arity

434437 deriving (Show, Ord)

435438{-!

436439deriving instance Binary NameType

src/Core/Typecheck.hs+1−1

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

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

6161 chk env (Var n)

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

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

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

6464 | otherwise = do lift $ tfail $ NoSuchVariable n

6565 chk env (RApp f a)

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

src/IRTS/CodegenC.hs+1−1

@@ -48,7 +48,7 @@ codegenC defs out exec incs objs libs dbg

4848 incFlags <- getIncFlags

4949 let gcc = comp ++ " " ++

5050 gccDbg dbg ++

51− " -I. " ++ objs ++ " -x c " ++

51+ " -I. " ++ objs ++ " -x c " ++

5252 (if (exec == Executable) then "" else " -c ") ++

5353 " " ++ tmpn ++

5454 " " ++ libFlags ++

src/IRTS/CodegenJava.hs+12−6

@@ -15,7 +15,7 @@ import qualified Control.Monad.Trans as T

1515import Control.Monad.Trans.State

1616import Data.Char

1717import Data.Maybe (fromJust)

18−import Data.List (isPrefixOf, isSuffixOf, intercalate)

18+import Data.List (isPrefixOf, isSuffixOf, intercalate, foldl')

1919import qualified Data.Text as T

2020import qualified Data.Text.IO as TIO

2121import Language.Java.Parser

@@ -255,7 +255,7 @@ mkMainMethod =

255255 )

256256

257257mergeInnerClasses :: [Decl] -> [Decl]

258−mergeInnerClasses = foldl mergeInner []

258+mergeInnerClasses = foldl' mergeInner []

259259 where

260260 mergeInner ((decl@(MemberDecl (MemberClassDecl (ClassDecl priv name targs ext imp (ClassBody body))))):decls)

261261 decl'@(MemberDecl (MemberClassDecl (ClassDecl _ name' _ ext' imp' (ClassBody body'))))

@@ -418,6 +418,12 @@ mkIdentifier (UN name) =

418418 cleanReserved "idris_K" = "_idris_K"

419419 cleanReserved "idris_flipK" = "_idris_flipK"

420420 cleanReserved "idris_assignStack" = "_idris_assignStack"

421+ cleanReserved "free" = "_free"

422+ cleanReserved "malloc" = "_malloc"

423+ cleanReserved "idris_memset" = "_idris_memset"

424+ cleanReserved "idris_peek" = "_idris_peek"

425+ cleanReserved "idris_poke" = "_idris_poke"

426+ cleanReserved "idris_memmove" = "_idris_memmove"

421427

422428 cleanReserved x = x

423429

@@ -1253,10 +1259,10 @@ mkExp (SConst BIType) = return $ mkClass bigIntegerType

12531259mkExp (SConst FlType) = return $ mkClass doubleType

12541260mkExp (SConst ChType) = return $ mkClass charType

12551261mkExp (SConst StrType) = return $ mkClass stringType

1256−mkExp (SConst (B8 x)) = return $ mkPrimitive "Byte" (Int (toInteger x))

1257−mkExp (SConst (B16 x)) = return $ mkPrimitive "Short" (Int (toInteger x))

1262+mkExp (SConst (B8 x)) = return $ mkPrimitive "Byte" (String (show x))

1263+mkExp (SConst (B16 x)) = return $ mkPrimitive "Short" (String (show x))

12581264mkExp (SConst (B32 x)) = return $ mkPrimitive "Integer" (Int (toInteger x))

1259−mkExp (SConst (B64 x)) = return $ mkPrimitive "Long" (Int (toInteger x))

1265+mkExp (SConst (B64 x)) = return $ mkPrimitive "Long" (String (show x))

12601266mkExp (SConst (B8Type))= return $ mkClass byteType

12611267mkExp (SConst (B16Type)) = return $ mkClass shortType

12621268mkExp (SConst (B32Type)) = return $ mkClass integerType

@@ -1513,4 +1519,4 @@ mkExp (SError err) =

15131519 []

15141520 (Ident "throwSelf")

15151521 []

1516−mkExp other = error (show other)

1522+mkExp other = error (show other)

src/IRTS/CodegenJavaScript.hs+2−1

@@ -139,6 +139,7 @@ translateConstant ChType = "__IDRRT__.Char"

139139translateConstant StrType = "__IDRRT__.String"

140140translateConstant BIType = "__IDRRT__.Integer"

141141translateConstant FlType = "__IDRRT__.Float"

142+translateConstant PtrType = "__IDRRT__.Ptr"

142143translateConstant Forgot = "__IDRRT__.Forgot"

143144translateConstant c =

144145 "(function(){throw 'Unimplemented Const: " ++ show c ++ "';})()"

@@ -450,7 +451,7 @@ translateCase var (SConstCase ty e)

450451 | IType <- ty = matchHelper "Int"

451452 | BIType <- ty = matchHelper "Integer"

452453 | FlType <- ty = matchHelper "Float"

453− | PtrType <- ty = matchHelper "Pointer"

454+ | PtrType <- ty = matchHelper "Ptr"

454455 | Forgot <- ty = matchHelper "Forgot"

455456 where

456457 matchHelper tyName = translateTypeMatch var tyName e

src/IRTS/Compiler.hs+3−3

@@ -98,7 +98,7 @@ irMain tm = do i <- ir tm

9898allNames :: [Name] -> Name -> Idris [Name]

9999allNames ns n | n `elem` ns = return []

100100allNames ns n = do i <- getIState

101− case lookupCtxt Nothing n (idris_callgraph i) of

101+ case lookupCtxt n (idris_callgraph i) of

102102 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))

103103 return (nub (n : concat more))

104104 _ -> return [n]

@@ -205,12 +205,12 @@ instance ToIR (TT Name) where

205205 Just tm -> return tm

206206 _ -> do

207207 let collapse

208− = case lookupCtxt Nothing n

208+ = case lookupCtxt n

209209 (idris_optimisation i) of

210210 [oi] -> collapsible oi

211211 _ -> False

212212 let unused

213− = case lookupCtxt Nothing n

213+ = case lookupCtxt n

214214 (idris_callgraph i) of

215215 [CGInfo _ _ _ _ unusedpos] ->

216216 unusedpos

src/IRTS/Defunctionalise.hs+2−2

@@ -80,14 +80,14 @@ addApps defs (n, LFun _ _ args e)

8080-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e

8181 aa env (LApp tc (LV (Glob n)) args)

8282 = do args' <- mapM (aa env) args

83− case lookupCtxt Nothing n defs of

83+ case lookupCtxt n defs of

8484 [LConstructor _ i ar] -> return $ DApp tc n args'

8585 [LFun _ _ as _] -> let arity = length as in

8686 fixApply tc n args' arity

8787 [] -> return $ chainAPPLY (DV (Glob n)) args'

8888 aa env (LLazyApp n args)

8989 = do args' <- mapM (aa env) args

90− case lookupCtxt Nothing n defs of

90+ case lookupCtxt n defs of

9191 [LConstructor _ i ar] -> return $ DApp False n args'

9292 [LFun _ _ as _] -> let arity = length as in

9393 fixLazyApply n args' arity

src/IRTS/Simplified.hs+7−7

@@ -46,7 +46,7 @@ simplify :: Bool -> DExp -> State (DDefs, Int) SExp

4646simplify tl (DV (Loc i)) = return (SV (Loc i))

4747simplify tl (DV (Glob x))

4848 = do ctxt <- ldefs

49− case lookupCtxt Nothing x ctxt of

49+ case lookupCtxt x ctxt of

5050 [DConstructor _ t 0] -> return $ SCon t x []

5151 _ -> return $ SV (Glob x)

5252simplify tl (DApp tc n args) = do args' <- mapM sVar args

@@ -88,7 +88,7 @@ simplify tl (DError str) = return $ SError str

8888

8989sVar (DV (Glob x))

9090 = do ctxt <- ldefs

91− case lookupCtxt Nothing x ctxt of

91+ case lookupCtxt x ctxt of

9292 [DConstructor _ t 0] -> sVar (DC t x [])

9393 _ -> return (Glob x, Nothing)

9494sVar (DV x) = return (x, Nothing)

@@ -136,7 +136,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

136136 sc env (SV (Glob n)) =

137137 case lookup n (reverse env) of -- most recent first

138138 Just i -> do lvar i; return (SV (Loc i))

139− Nothing -> case lookupCtxt Nothing n ctxt of

139+ Nothing -> case lookupCtxt n ctxt of

140140 [DConstructor _ i ar] ->

141141 if True -- ar == 0

142142 then return (SCon i n [])

@@ -146,7 +146,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

146146 [] -> fail $ "Codegen error: No such variable " ++ show n

147147 sc env (SApp tc f args)

148148 = do args' <- mapM (scVar env) args

149− case lookupCtxt Nothing f ctxt of

149+ case lookupCtxt f ctxt of

150150 [DConstructor n tag ar] ->

151151 if True -- (ar == length args)

152152 then return $ SCon tag n args'

@@ -160,7 +160,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

160160 return $ SForeign l ty f args'

161161 sc env (SCon tag f args)

162162 = do args' <- mapM (scVar env) args

163− case lookupCtxt Nothing f ctxt of

163+ case lookupCtxt f ctxt of

164164 [DConstructor n tag ar] ->

165165 if True -- (ar == length args)

166166 then return $ SCon tag n args'

@@ -197,7 +197,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

197197 scVar env (Glob n) =

198198 case lookup n (reverse env) of -- most recent first

199199 Just i -> do lvar i; return (Loc i)

200− Nothing -> case lookupCtxt Nothing n ctxt of

200+ Nothing -> case lookupCtxt n ctxt of

201201 [DConstructor _ i ar] ->

202202 fail $ "Codegen error : can't pass constructor here"

203203 [_] -> return (Glob n)

@@ -207,7 +207,7 @@ scopecheck ctxt envTop tm = sc envTop tm where

207207

208208 scalt env (SConCase _ i n args e)

209209 = do let env' = env ++ zip args [length env..]

210− tag <- case lookupCtxt Nothing n ctxt of

210+ tag <- case lookupCtxt n ctxt of

211211 [DConstructor _ i ar] ->

212212 if True -- (length args == ar)

213213 then return i

src/Idris/AbsSyntax.hs+24−20

@@ -24,7 +24,7 @@ import Data.Either

2424import Debug.Trace

2525

2626import Util.Pretty

27−

27+import Util.System

2828

2929getContext :: Idris Context

3030getContext = do i <- getIState; return (tt_ctxt i)

@@ -41,13 +41,15 @@ getLibs = do i <- getIState; return (idris_libs i)

4141addLib :: String -> Idris ()

4242addLib f = do i <- getIState; putIState $ i { idris_libs = f : idris_libs i }

4343

44−addDyLib :: String -> Idris ()

45−addDyLib lib = do i <- getIState

46− handle <- lift $ tryLoadLib lib

47− case handle of

48− Nothing -> fail $ "Could not load dynamic lib \"" ++ lib ++ "\""

49− Just x -> do let libs = idris_dynamic_libs i

50− putIState $ i { idris_dynamic_libs = x:libs }

44+addDyLib :: [String] -> Idris (Either DynamicLib String)

45+addDyLib libs = do i <- getIState

46+ handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) libs

47+ case msum handle of

48+ Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++

49+ concat (intersperse "," libs) ++ "\"")

50+ Just x -> do let ls = idris_dynamic_libs i

51+ putIState $ i { idris_dynamic_libs = x:ls }

52+ return (Left x)

5153

5254addHdr :: String -> Idris ()

5355addHdr f = do i <- getIState; putIState $ i { idris_hdrs = f : idris_hdrs i }

@@ -88,7 +90,7 @@ getCoercionsTo i ty =

8890 findCoercions fn cs

8991 where findCoercions t [] = []

9092 findCoercions t (n : ns) =

91− let ps = case lookupTy Nothing n (tt_ctxt i) of

93+ let ps = case lookupTy n (tt_ctxt i) of

9294 [ty] -> case unApply (getRetTy ty) of

9395 (t', _) ->

9496 if t == t' then [n] else []

@@ -119,7 +121,7 @@ addToCalledG n ns = return () -- TODO

119121addInstance :: Bool -> Name -> Name -> Idris ()

120122addInstance int n i

121123 = do ist <- getIState

122− case lookupCtxt Nothing n (idris_classes ist) of

124+ case lookupCtxt n (idris_classes ist) of

123125 [CI a b c d ins] ->

124126 do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)

125127 putIState $ ist { idris_classes = cs }

@@ -139,7 +141,7 @@ addInstance int n i

139141addClass :: Name -> ClassInfo -> Idris ()

140142addClass n i

141143 = do ist <- getIState

142− let i' = case lookupCtxt Nothing n (idris_classes ist) of

144+ let i' = case lookupCtxt n (idris_classes ist) of

143145 [c] -> c { class_instances = class_instances i }

144146 _ -> i

145147 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }

@@ -193,7 +195,7 @@ getName = do i <- getIState;

193195checkUndefined :: FC -> Name -> Idris ()

194196checkUndefined fc n

195197 = do i <- getContext

196− case lookupTy Nothing n i of

198+ case lookupTy n i of

197199 (_:_) -> fail $ show fc ++ ":" ++

198200 show n ++ " already defined"

199201 _ -> return ()

@@ -201,7 +203,7 @@ checkUndefined fc n

201203isUndefined :: FC -> Name -> Idris Bool

202204isUndefined fc n

203205 = do i <- getContext

204− case lookupTy Nothing n i of

206+ case lookupTy n i of

205207 (_:_) -> return False

206208 _ -> return True

207209

@@ -641,7 +643,7 @@ getPriority :: IState -> PTerm -> Int

641643getPriority i tm = 1 -- pri tm

642644 where

643645 pri (PRef _ n) =

644− case lookupP Nothing n (tt_ctxt i) of

646+ case lookupP n (tt_ctxt i) of

645647 ((P (DCon _ _) _ _):_) -> 1

646648 ((P (TCon _ _) _ _):_) -> 1

647649 ((P Ref _ _):_) -> 1

@@ -882,9 +884,9 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

882884

883885aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm

884886aiFn inpat True ist fc f []

885− = case lookupDef Nothing f (tt_ctxt ist) of

887+ = case lookupDef f (tt_ctxt ist) of

886888 [] -> Right $ PPatvar fc f

887− alts -> let ialts = lookupCtxt Nothing f (idris_implicits ist) in

889+ alts -> let ialts = lookupCtxt f (idris_implicits ist) in

888890 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $

889891 if (not (vname f) || tcname f

890892 || any constructor alts || any allImp ialts)

@@ -904,7 +906,7 @@ aiFn inpat expat ist fc f as

904906 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

905907aiFn inpat expat ist fc f as

906908 -- This is where namespaces get resolved by adding PAlternative

907− = case lookupCtxtName Nothing f (idris_implicits ist) of

909+ = case lookupCtxtName f (idris_implicits ist) of

908910 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

909911 [] -> if f `elem` idris_metavars ist

910912 then Right $ PApp fc (PRef fc f) as

@@ -949,7 +951,7 @@ stripLinear :: IState -> PTerm -> PTerm

949951stripLinear i tm = evalState (sl tm) [] where

950952 sl :: PTerm -> State [Name] PTerm

951953 sl (PRef fc f)

952− | (_:_) <- lookupTy Nothing f (tt_ctxt i)

954+ | (_:_) <- lookupTy f (tt_ctxt i)

953955 = return $ PRef fc f

954956 | otherwise = do ns <- get

955957 if (f `elem` ns)

@@ -1074,14 +1076,16 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

10741076-- match (PRef _ n) (PRef _ n') | n == n' = return []

10751077-- | otherwise = Nothing

10761078 match (PRef f n) (PApp _ x []) = match (PRef f n) x

1079+ match (PPatvar f n) xr = match (PRef f n) xr

1080+ match xr (PPatvar f n) = match xr (PRef f n)

10771081 match (PApp _ x []) (PRef f n) = match x (PRef f n)

10781082 match (PRef _ n) tm@(PRef _ n')

10791083 | n == n' && not names &&

1080− (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)

1084+ (not (isConName n (tt_ctxt i)) || tm == Placeholder)

10811085 = return [(n, tm)]

10821086 | n == n' = return []

10831087 match (PRef _ n) tm

1084− | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)

1088+ | not names && (not (isConName n (tt_ctxt i)) || tm == Placeholder)

10851089 = return [(n, tm)]

10861090 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

10871091 mr <- match' r r'

src/Idris/AbsSyntaxTree.hs+39−5

@@ -887,10 +887,10 @@ prettyImp impl = prettySe 10

887887 bracket p 1 $

888888 prettySe 1 f <+>

889889 if impl then

890− foldl fS empty as

890+ foldl' fS empty as

891891 -- foldr (<+>) empty $ map prettyArgS as

892892 else

893− foldl fSe empty args

893+ foldl' fSe empty args

894894 -- foldr (<+>) empty $ map prettyArgSe args

895895 where

896896 fS l r =

@@ -979,7 +979,7 @@ prettyImp impl = prettySe 10

979979showImp :: Bool -> PTerm -> String

980980showImp impl tm = se 10 tm where

981981 se p (PQuote r) = "![" ++ show r ++ "]"

982− se p (PPatvar fc n) = show n

982+ se p (PPatvar fc n) = if impl then show n ++ "[p]" else show n

983983 se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"

984984 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"

985985 else showbasic n

@@ -1014,6 +1014,9 @@ showImp impl tm = se 10 tm where

10141014 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc

10151015 se p (PPi (TacImp _ _ s _) n ty sc)

10161016 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc

1017+ se p e

1018+ | Just str <- slist p e = str

1019+ | Just num <- snat p e = show num

10171020 se p (PApp _ (PRef _ f) [])

10181021 | not impl = show f

10191022 se p (PApp _ (PRef _ op@(UN (f:_))) args)

@@ -1052,6 +1055,37 @@ showImp impl tm = se 10 tm where

10521055 se p (PCoerced t) = se p t

10531056-- se p x = "Not implemented"

10541057

1058+ slist' p (PApp _ (PRef _ nil) _)

1059+ | nsroot nil == UN "Nil" = Just []

1060+ slist' p (PApp _ (PRef _ cons) args)

1061+ | nsroot cons == UN "::",

1062+ (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

1063+ all isImp imps,

1064+ Just tl' <- slist' p tl

1065+ = Just (hd:tl')

1066+ where

1067+ isImp (PImp {}) = True

1068+ isImp _ = False

1069+ slist' _ _ = Nothing

1070+

1071+ slist p e | Just es <- slist' p e = Just $

1072+ case es of [] -> "[]"

1073+ [x] -> "[" ++ se p x ++ "]"

1074+ xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"

1075+ slist _ _ = Nothing

1076+

1077+ -- since Prelude is always imported, S & O are unqualified iff they're the

1078+ -- Nat ones.

1079+ snat p (PRef _ o)

1080+ | show o == (natns++"O") || show o == "O" = Just 0

1081+ snat p (PApp _ s [PExp {getTm=n}])

1082+ | show s == (natns++"S") || show s == "S",

1083+ Just n' <- snat p n

1084+ = Just $ 1 + n'

1085+ snat _ _ = Nothing

1086+

1087+ natns = "Prelude.Nat."

1088+

10551089 sArg (PImp _ _ n tm _) = siArg (n, tm)

10561090 sArg (PExp _ _ tm _) = seArg tm

10571091 sArg (PConstraint _ _ tm _) = scArg tm

@@ -1128,7 +1162,7 @@ namesIn uvars ist tm = nub $ ni [] tm

11281162 where

11291163 ni env (PRef _ n)

11301164 | not (n `elem` env)

1131− = case lookupTy Nothing n (tt_ctxt ist) of

1165+ = case lookupTy n (tt_ctxt ist) of

11321166 [] -> [n]

11331167 _ -> if n `elem` (map fst uvars) then [n] else []

11341168 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

@@ -1152,7 +1186,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

11521186 where

11531187 ni env (PRef _ n)

11541188 | n `elem` vars && not (n `elem` env)

1155− = case lookupTy Nothing n (tt_ctxt ist) of

1189+ = case lookupTy n (tt_ctxt ist) of

11561190 [] -> [n]

11571191 _ -> []

11581192 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

src/Idris/Coverage.hs+25−25

@@ -38,7 +38,7 @@ mkPatTm t = do i <- getIState

3838 evalStateT (toTT timp) 0

3939 where

4040 toTT (PRef _ n) = do i <- lift getIState

41− case lookupDef Nothing n (tt_ctxt i) of

41+ case lookupDef n (tt_ctxt i) of

4242 [TyDecl nt _] -> return $ P nt n Erased

4343 _ -> return $ P Ref n Erased

4444 toTT (PApp _ t args) = do t' <- toTT t

@@ -107,9 +107,9 @@ expandAlts :: IState -> [CaseAlt] -> SC -> Idris [CaseAlt]

107107expandAlts i all@(ConstCase c _ : alts) def

108108 = return $ all ++ [DefaultCase def]

109109expandAlts i all@(ConCase n _ _ _ : alts) def

110− | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)

110+ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)

111111 = do let tyn = getTy n (tt_ctxt i)

112− case lookupCtxt Nothing tyn (idris_datatypes i) of

112+ case lookupCtxt tyn (idris_datatypes i) of

113113 (TI ns _ _: _) -> do let ps = map mkPat ns

114114 return $ addAlts ps (altsFor all) all

115115 _ -> return all

@@ -127,13 +127,13 @@ expandAlts i all@(ConCase n _ _ _ : alts) def

127127 argList i = take i (map (\x -> (MN x "ign")) [0..])

128128

129129 getTy n ctxt

130− = case lookupTy Nothing n ctxt of

130+ = case lookupTy n ctxt of

131131 (t : _) -> case unApply (getRetTy t) of

132132 (P _ tyn _, _) -> tyn

133133 x -> error $ "Can't happen getTy 1 " ++ show (n, x)

134134 _ -> error "Can't happen getTy 2"

135135

136− mkPat x = case lookupCtxt Nothing x (idris_implicits i) of

136+ mkPat x = case lookupCtxt x (idris_implicits i) of

137137 (pargs : _)

138138 -> (x, length pargs)

139139 _ -> error "Can't happen - genAll"

@@ -160,7 +160,7 @@ genClauses fc n xs given

160160 logLvl 10 $ show argss ++ "\n" ++ show all_args

161161 logLvl 10 $ "Original: \n" ++

162162 showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)

163− let parg = case lookupCtxt Nothing n (idris_implicits i) of

163+ let parg = case lookupCtxt n (idris_implicits i) of

164164 (p : _) -> p

165165 _ -> repeat (pexp Placeholder)

166166 let tryclauses = mkClauses parg all_args

@@ -217,8 +217,8 @@ genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of

217217 [] -> [Placeholder]

218218 xs -> nub xs

219219 where

220− conForm (PApp _ (PRef fc n) _) = isConName Nothing n (tt_ctxt i)

221− conForm (PRef fc n) = isConName Nothing n (tt_ctxt i)

220+ conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i)

221+ conForm (PRef fc n) = isConName n (tt_ctxt i)

222222 conForm _ = False

223223

224224 otherPats :: PTerm -> [PTerm]

@@ -227,22 +227,22 @@ genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of

227227 otherPats arg = return Placeholder

228228

229229 ops fc n xs o

230− | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)

230+ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)

231231 = do xs' <- mapM otherPats (map getTm xs)

232232 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)

233233 let tyn = getTy n (tt_ctxt i)

234− case lookupCtxt Nothing tyn (idris_datatypes i) of

234+ case lookupCtxt tyn (idris_datatypes i) of

235235 (TI ns _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

236236 _ -> [p]

237237 ops fc n arg o = return Placeholder

238238

239− getTy n ctxt = case lookupTy Nothing n ctxt of

239+ getTy n ctxt = case lookupTy n ctxt of

240240 (t : _) -> case unApply (getRetTy t) of

241241 (P _ tyn _, _) -> tyn

242242 x -> error $ "Can't happen getTy 1 " ++ show (n, x)

243243 _ -> error "Can't happen getTy 2"

244244

245− mkPat fc x = case lookupCtxt Nothing x (idris_implicits i) of

245+ mkPat fc x = case lookupCtxt x (idris_implicits i) of

246246 (pargs : _)

247247 -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)

248248 _ -> error "Can't happen - genAll"

@@ -306,7 +306,7 @@ calcProd i fc n pats = do patsprod <- mapM prodRec pats

306306

307307 cotype ty

308308 | (P _ t _, _) <- unApply (getRetTy ty)

309− = case lookupCtxt Nothing t (idris_datatypes i) of

309+ = case lookupCtxt t (idris_datatypes i) of

310310 [TI _ True _] -> True

311311 _ -> False

312312 | otherwise = False

@@ -315,7 +315,7 @@ calcTotality :: [Name] -> FC -> Name -> [([Name], Term, Term)]

315315 -> Idris Totality

316316calcTotality path fc n pats

317317 = do i <- getIState

318− let opts = case lookupCtxt Nothing n (idris_flags i) of

318+ let opts = case lookupCtxt n (idris_flags i) of

319319 [fs] -> fs

320320 _ -> []

321321 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

@@ -339,12 +339,12 @@ checkTotality path fc n

339339 updateContext (simplifyCasedef n)

340340 ctxt <- getContext

341341 i <- getIState

342− let opts = case lookupCtxt Nothing n (idris_flags i) of

342+ let opts = case lookupCtxt n (idris_flags i) of

343343 [fs] -> fs

344344 _ -> []

345345 t' <- case t of

346346 Unchecked ->

347− case lookupDef Nothing n ctxt of

347+ case lookupDef n ctxt of

348348 [CaseOp _ _ _ _ pats _ _ _ _] ->

349349 do t' <- if AssertTotal `elem` opts

350350 then return $ Total []

@@ -378,7 +378,7 @@ checkTotality path fc n

378378

379379 warnPartial n t

380380 = do i <- getIState

381− case lookupDef Nothing n (tt_ctxt i) of

381+ case lookupDef n (tt_ctxt i) of

382382 [x] -> do

383383 iputStrLn $ show fc ++ ":Warning - " ++ show n ++ " is " ++ show t

384384-- ++ "\n" ++ show x

@@ -407,8 +407,8 @@ checkDeclTotality (fc, n)

407407buildSCG :: (FC, Name) -> Idris ()

408408buildSCG (_, n) = do

409409 ist <- getIState

410− case lookupCtxt Nothing n (idris_callgraph ist) of

411− [cg] -> case lookupDef Nothing n (tt_ctxt ist) of

410+ case lookupCtxt n (idris_callgraph ist) of

411+ [cg] -> case lookupDef n (tt_ctxt ist) of

412412 [CaseOp _ _ _ _ _ args sc _ _] ->

413413 do logLvl 3 $ "Building SCG for " ++ show n ++ " from\n"

414414 ++ show sc

@@ -442,7 +442,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

442442 -- how the arguments relate - either Smaller or Unknown

443443 argRels :: Name -> [(Name, SizeChange)]

444444 argRels n = let ctxt = tt_ctxt ist

445− [ty] = lookupTy Nothing n ctxt -- must exist!

445+ [ty] = lookupTy n ctxt -- must exist!

446446 P _ nty _ = fst (unApply (getRetTy ty))

447447 args = map snd (getArgTys ty) in

448448 map (getRel nty) (map (fst . unApply . getRetTy) args)

@@ -503,7 +503,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

503503checkSizeChange :: Name -> Idris Totality

504504checkSizeChange n = do

505505 ist <- getIState

506− case lookupCtxt Nothing n (idris_callgraph ist) of

506+ case lookupCtxt n (idris_callgraph ist) of

507507 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)

508508 logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++

509509 "from " ++ show (scg cg) ++ "\n" ++

@@ -530,7 +530,7 @@ mkMultiPaths ist path cg

530530 where extend (nextf, args)

531531 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]

532532 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)

533− = case lookupCtxt Nothing nextf (idris_callgraph ist) of

533+ = case lookupCtxt nextf (idris_callgraph ist) of

534534 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)

535535 _ -> [ reverse ((nextf, args) : path) ]

536536 | otherwise = [ reverse ((nextf, args) : path) ]

@@ -538,7 +538,7 @@ mkMultiPaths ist path cg

538538-- do (nextf, args) <- cg

539539-- if ((nextf, args) `elem` path)

540540-- then return (reverse ((nextf, args) : path))

541−-- else case lookupCtxt Nothing nextf (idris_callgraph ist) of

541+-- else case lookupCtxt nextf (idris_callgraph ist) of

542542-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)

543543-- _ -> return (reverse ((nextf, args) : path))

544544

@@ -562,12 +562,12 @@ checkMP ist i mp = if i > 0

562562-- = Partial BelieveMe

563563 -- if we get to a constructor, it's fine as long as it's strictly positive

564564 tryPath desc path ((f, _) :es) arg

565− | [TyDecl (DCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)

565+ | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)

566566 = case lookupTotal f (tt_ctxt ist) of

567567 [Total _] -> Unchecked -- okay so far

568568 [Partial _] -> Partial (Other [f])

569569 x -> error (show x)

570− | [TyDecl (TCon _ _) _] <- lookupDef Nothing f (tt_ctxt ist)

570+ | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)

571571 = Total []

572572 tryPath desc path (e@(f, args) : es) arg

573573 | e `elem` es && allNothing args = Partial (Mutual [f])

src/Idris/DataOpts.hs+10−10

@@ -17,7 +17,7 @@ import Debug.Trace

1717forceArgs :: Name -> Type -> Idris ()

1818forceArgs n t = do i <- getIState

1919 let fargs = force i 0 t

20− copt <- case lookupCtxt Nothing n (idris_optimisation i) of

20+ copt <- case lookupCtxt n (idris_optimisation i) of

2121 [] -> return $ Optimise False [] []

2222 (op:_) -> return op

2323 let opts = addDef n (copt { forceable = fargs }) (idris_optimisation i)

@@ -38,7 +38,7 @@ forceArgs n t = do i <- getIState

3838

3939 collapsibleIn i t

4040 | (P _ tn _, _) <- unApply t

41− = case lookupCtxt Nothing tn (idris_optimisation i) of

41+ = case lookupCtxt tn (idris_optimisation i) of

4242 [oi] -> collapsible oi

4343 _ -> False

4444 | otherwise = False

@@ -68,7 +68,7 @@ collapseCons ty cons =

6868 setCollapsible n

6969 = do i <- getIState

7070 iLOG $ show n ++ " collapsible"

71− case lookupCtxt Nothing n (idris_optimisation i) of

71+ case lookupCtxt n (idris_optimisation i) of

7272 (oi:_) -> do let oi' = oi { collapsible = True }

7373 let opts = addDef n oi' (idris_optimisation i)

7474 putIState (i { idris_optimisation = opts })

@@ -79,15 +79,15 @@ collapseCons ty cons =

7979

8080 forceRec :: IState -> (Name, [Type]) -> Idris Bool

8181 forceRec i (n, ts)

82− = case lookupCtxt Nothing n (idris_optimisation i) of

82+ = case lookupCtxt n (idris_optimisation i) of

8383 (oi:_) -> checkFR (forceable oi) 0 ts

8484 _ -> return False

8585 checkFR fs i [] = return True

8686 checkFR fs i (_ : xs) | i `elem` fs = checkFR fs (i + 1) xs

8787 checkFR fs i (t : xs)

8888 -- must be recursive or type is not collapsible

89− = do let rt = getRetTy t

90− if (ty `elem` freeNames rt)

89+ = do let (rtf, rta) = unApply $ getRetTy t

90+ if (ty `elem` freeNames rtf)

9191 then checkFR fs (i+1) xs

9292 else return False

9393

@@ -161,7 +161,7 @@ instance Optimisable Raw where

161161 | (Var n, args) <- raw_unapply t -- MAGIC HERE

162162 = do args' <- mapM applyOpts args

163163 i <- getIState

164− case lookupCtxt Nothing n (idris_optimisation i) of

164+ case lookupCtxt n (idris_optimisation i) of

165165 (oi:_) -> return $ applyDataOpt oi n args'

166166 _ -> return (raw_apply (Var n) args')

167167 | otherwise = do f' <- applyOpts f

@@ -202,14 +202,14 @@ applyDataOpt oi n args

202202instance Optimisable (TT Name) where

203203 applyOpts c@(P (DCon t arity) n _)

204204 = do i <- getIState

205− case lookupCtxt Nothing n (idris_optimisation i) of

205+ case lookupCtxt n (idris_optimisation i) of

206206 (oi:_) -> return $ applyDataOptRT oi n t arity []

207207 _ -> return c

208208 applyOpts t@(App f a)

209209 | (c@(P (DCon t arity) n _), args) <- unApply t -- MAGIC HERE

210210 = do args' <- mapM applyOpts args

211211 i <- getIState

212− case lookupCtxt Nothing n (idris_optimisation i) of

212+ case lookupCtxt n (idris_optimisation i) of

213213 (oi:_) -> do return $ applyDataOptRT oi n t arity args'

214214 _ -> return (mkApp c args')

215215 | otherwise = do f' <- applyOpts f

@@ -224,7 +224,7 @@ instance Optimisable (TT Name) where

224224

225225 stripCollapsed (Bind n (PVar x) t) | (P _ ty _, _) <- unApply x

226226 = do i <- getIState

227− case lookupCtxt Nothing ty (idris_optimisation i) of

227+ case lookupCtxt ty (idris_optimisation i) of

228228 [oi] -> if collapsible oi

229229 then do t' <- stripCollapsed t

230230 return (Bind n (PVar x) (instantiate Erased t'))

src/Idris/Delaborate.hs+56−34

@@ -7,6 +7,7 @@ module Idris.Delaborate where

77

88import Idris.AbsSyntax

99import Core.TT

10+import Core.Evaluate

1011

1112import Debug.Trace

1213

@@ -15,54 +16,75 @@ bugaddr = "https://github.com/edwinb/Idris-dev/issues"

1516delab :: IState -> Term -> PTerm

1617delab i tm = delab' i tm False

1718

19+delabTy :: IState -> Name -> PTerm

20+delabTy i n

21+ = case lookupTy n (tt_ctxt i) of

22+ (ty:_) -> case lookupCtxt n (idris_implicits i) of

23+ (imps:_) -> delabTy' i imps ty False

24+ _ -> delabTy' i [] ty False

25+

1826delab' :: IState -> Term -> Bool -> PTerm

19−delab' ist tm fullname = de [] tm

27+delab' i t f = delabTy' i [] t f

28+

29+delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

30+ -> Term -> Bool -> PTerm

31+delabTy' ist imps tm fullname = de [] imps tm

2032 where

2133 un = FC "(val)" 0

2234

23− de env (App f a) = deFn env f [a]

24− de env (V i) | i < length env = PRef un (snd (env!!i))

25− | otherwise = PRef un (UN ("v" ++ show i ++ ""))

26− de env (P _ n _) | n == unitTy = PTrue un

27− | n == unitCon = PTrue un

28− | n == falseTy = PFalse un

29− | Just n' <- lookup n env = PRef un n'

30− | otherwise = PRef un (dens n)

31− de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de ((n,n):env) sc)

32− de env (Bind n (Pi ty) sc) = PPi expl n (de env ty) (de ((n,n):env) sc)

33− de env (Bind n (Let ty val) sc)

34− = PLet n (de env ty) (de env val) (de ((n,n):env) sc)

35− de env (Bind n (Hole ty) sc) = de ((n, UN "[__]"):env) sc

36− de env (Bind n (Guess ty val) sc) = de ((n, UN "[__]"):env) sc

37− de env (Bind n _ sc) = de ((n,n):env) sc

38− de env (Constant i) = PConstant i

39− de env Erased = Placeholder

40− de env Impossible = Placeholder

41− de env (TType i) = PType

35+ de env _ (App f a) = deFn env f [a]

36+ de env _ (V i) | i < length env = PRef un (snd (env!!i))

37+ | otherwise = PRef un (UN ("v" ++ show i ++ ""))

38+ de env _ (P _ n _) | n == unitTy = PTrue un

39+ | n == unitCon = PTrue un

40+ | n == falseTy = PFalse un

41+ | Just n' <- lookup n env = PRef un n'

42+ | otherwise = PRef un (dens n)

43+ de env _ (Bind n (Lam ty) sc)

44+ = PLam n (de env [] ty) (de ((n,n):env) [] sc)

45+ de env (PImp _ _ _ _ _:is) (Bind n (Pi ty) sc)

46+ = PPi impl n (de env [] ty) (de ((n,n):env) is sc)

47+ de env (PConstraint _ _ _ _:is) (Bind n (Pi ty) sc)

48+ = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

49+ de env (PTacImplicit _ _ _ tac _ _:is) (Bind n (Pi ty) sc)

50+ = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is sc)

51+ de env _ (Bind n (Pi ty) sc)

52+ = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

53+ de env _ (Bind n (Let ty val) sc)

54+ = PLet n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

55+ de env _ (Bind n (Hole ty) sc) = de ((n, UN "[__]"):env) [] sc

56+ de env _ (Bind n (Guess ty val) sc) = de ((n, UN "[__]"):env) [] sc

57+ de env _ (Bind n _ sc) = de ((n,n):env) [] sc

58+ de env _ (Constant i) = PConstant i

59+ de env _ Erased = Placeholder

60+ de env _ Impossible = Placeholder

61+ de env _ (TType i) = PType

4262

4363 dens x | fullname = x

44− dens ns@(NS n _) = case lookupCtxt Nothing n (idris_implicits ist) of

64+ dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

4565 [_] -> n -- just one thing

4666 _ -> ns

4767 dens n = n

4868

4969 deFn env (App f a) args = deFn env f (a:args)

50− deFn env (P _ n _) [l,r] | n == pairTy = PPair un (de env l) (de env r)

51− | n == eqCon = PRefl un (de env r)

52− | n == UN "lazy" = de env r

70+ deFn env (P _ n _) [l,r]

71+ | n == pairTy = PPair un (de env [] l) (de env [] r)

72+ | n == eqCon = PRefl un (de env [] r)

73+ | n == UN "lazy" = de env [] r

5374 deFn env (P _ n _) [ty, Bind x (Lam _) r]

54− | n == UN "Exists"

55− = PDPair un (PRef un x) (de env ty)

56− (de ((x,x):env) (instantiate (P Bound x ty) r))

57− deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)

58− | n == eqTy = PEq un (de env l) (de env r)

59− | n == UN "Ex_intro" = PDPair un (de env l) Placeholder

60− (de env r)

61− deFn env (P _ n _) args = mkPApp (dens n) (map (de env) args)

62− deFn env f args = PApp un (de env f) (map pexp (map (de env) args))

75+ | n == UN "Exists"

76+ = PDPair un (PRef un x) (de env [] ty)

77+ (de ((x,x):env) [] (instantiate (P Bound x ty) r))

78+ deFn env (P _ n _) [_,_,l,r]

79+ | n == pairCon = PPair un (de env [] l) (de env [] r)

80+ | n == eqTy = PEq un (de env [] l) (de env [] r)

81+ | n == UN "Ex_intro" = PDPair un (de env [] l) Placeholder

82+ (de env [] r)

83+ deFn env (P _ n _) args = mkPApp (dens n) (map (de env []) args)

84+ deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

6385

6486 mkPApp n args

65− | [imps] <- lookupCtxt Nothing n (idris_implicits ist)

87+ | [imps] <- lookupCtxt n (idris_implicits ist)

6688 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

6789 | otherwise = PApp un (PRef un n) (map pexp args)

6890

src/Idris/Docs.hs+6−6

@@ -65,9 +65,9 @@ instance Show Doc where

6565getDocs :: Name -> Idris Doc

6666getDocs n

6767 = do i <- getIState

68− case lookupCtxt Nothing n (idris_classes i) of

68+ case lookupCtxt n (idris_classes i) of

6969 [ci] -> docClass n ci

70− _ -> case lookupCtxt Nothing n (idris_datatypes i) of

70+ _ -> case lookupCtxt n (idris_datatypes i) of

7171 [ti] -> docData n ti

7272 _ -> do fd <- docFun n

7373 return (FunDoc fd)

@@ -81,7 +81,7 @@ docData n ti

8181docClass :: Name -> ClassInfo -> Idris Doc

8282docClass n ci

8383 = do i <- getIState

84− let docstr = case lookupCtxt Nothing n (idris_docstrings i) of

84+ let docstr = case lookupCtxt n (idris_docstrings i) of

8585 [str] -> str

8686 _ -> ""

8787 mdocs <- mapM docFun (map fst (class_methods ci))

@@ -90,13 +90,13 @@ docClass n ci

9090docFun :: Name -> Idris FunDoc

9191docFun n

9292 = do i <- getIState

93− let docstr = case lookupCtxt Nothing n (idris_docstrings i) of

93+ let docstr = case lookupCtxt n (idris_docstrings i) of

9494 [str] -> str

9595 _ -> ""

96− let ty = case lookupTy Nothing n (tt_ctxt i) of

96+ let ty = case lookupTy n (tt_ctxt i) of

9797 (t : _) -> t

9898 let argnames = map fst (getArgTys ty)

99− let args = case lookupCtxt Nothing n (idris_implicits i) of

99+ let args = case lookupCtxt n (idris_implicits i) of

100100 [args] -> zip argnames args

101101 _ -> []

102102 let infixes = idris_infixes i

src/Idris/ElabDecls.hs+75−53

@@ -69,7 +69,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

6969 let nty' = normalise ctxt [] nty

7070 let (t, _) = unApply (getRetTy nty')

7171 let corec = case t of

72− P _ rcty _ -> case lookupCtxt Nothing rcty (idris_datatypes i) of

72+ P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

7373 [TI _ True _] -> True

7474 _ -> False

7575 _ -> False

@@ -93,14 +93,14 @@ elabPostulate info syn doc fc opts n ty

9393 -- make sure it's collapsible, so it is never needed at run time

9494 -- start by getting the elaborated type

9595 ctxt <- getContext

96− fty <- case lookupTy Nothing n ctxt of

96+ fty <- case lookupTy n ctxt of

9797 [] -> tclift $ tfail $ (At fc (NoTypeDecl n)) -- can't happen!

9898 [ty] -> return ty

9999 ist <- getIState

100100 let (ap, _) = unApply (getRetTy (normalise ctxt [] fty))

101101 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

102102 let postOK = case ap of

103− P _ tn _ -> case lookupCtxt Nothing tn

103+ P _ tn _ -> case lookupCtxt tn

104104 (idris_optimisation ist) of

105105 [oi] -> collapsible oi

106106 _ -> False

@@ -147,7 +147,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

147147 ttag <- getName

148148 i <- getIState

149149 let as = map (const Nothing) (getArgTys cty)

150− let params = findParams (zip as (repeat True)) (map snd cons)

150+ let params = findParams (map snd cons)

151151 logLvl 2 $ "Parameters : " ++ show params

152152 putIState (i { idris_datatypes = addDef n (TI (map fst cons) codata params)

153153 (idris_datatypes i) })

@@ -161,32 +161,53 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

161161 where

162162 -- parameters are names which are unchanged across the structure,

163163 -- which appear exactly once in the return type of a constructor

164− findParams :: [(Maybe Name, Bool)] -> [Type] -> [Int]

165− findParams ps [] = mapMaybe (\ ((x, y), n) ->

166− if y then Just n else Nothing)

167− (zip ps [0..])

168− findParams ps (t : ts) = findParams (updateParams ps t) ts

169−

170− updateParams ps (Bind n (Pi t) sc)

171− = updateParams (updateParams ps (instantiate (P Bound n t) sc)) t

172− updateParams ps tm@(App f a)

173− | (P _ fn _, args) <- unApply tm

174− = if fn == n

175− then updateParamsA ps args (tail args)

176− else updateParams (updateParams ps f) a

177− | otherwise = updateParams (updateParams ps f) a

178− updateParams ps _ = ps

179−

180− updateParamsA ((mn, _) : ns) (p@(P _ n' _) : args) all

181− | n' `elem` concatMap freeNames all

182− = (mn, False) : updateParamsA ns args (p : all)

183− updateParamsA ((Nothing, b) : ns) (p@(P _ n' _) : args) all

184− = (Just n', b) : updateParamsA ns args (p : all)

185− updateParamsA ((Just p, b) : ns) (tm@(P _ n' _) : args) all

186− = (Just n', b && p == n') : updateParamsA ns args (tm : all)

187− updateParamsA ((mn, _) : ns) (p : args) all

188− = (mn, False) : updateParamsA ns args (p : all)

189− updateParamsA ps args all = ps

164+

165+ -- First, find all applications of the constructor, then check over

166+ -- them for repeated arguments

167+

168+ findParams :: [Type] -> [Int]

169+ findParams ts = let allapps = concatMap getDataApp ts in

170+ paramPos allapps

171+

172+ paramPos [] = []

173+ paramPos (args : rest)

174+ = dropNothing $ keepSame (zip [0..] args) rest

175+

176+ dropNothing [] = []

177+ dropNothing ((x, Nothing) : ts) = dropNothing ts

178+ dropNothing ((x, _) : ts) = x : dropNothing ts

179+

180+ keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->

181+ [(Int, Maybe Name)]

182+ keepSame as [] = as

183+ keepSame as (args : rest) = keepSame (update as args) rest

184+ where

185+ update [] _ = []

186+ update _ [] = []

187+ update ((n, Just x) : as) (Just x' : args)

188+ | x == x' = (n, Just x) : update as args

189+ update ((n, _) : as) (_ : args) = (n, Nothing) : update as args

190+

191+ getDataApp :: Type -> [[Maybe Name]]

192+ getDataApp f@(App _ _)

193+ | (P _ d _, args) <- unApply f

194+ = if (d == n) then [mParam args args] else []

195+ getDataApp (Bind n (Pi t) sc)

196+ = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)

197+ getDataApp _ = []

198+

199+ -- keep the arguments which are single names, which don't appear

200+ -- elsewhere

201+

202+ mParam args [] = []

203+ mParam args (P Bound n _ : rest)

204+ | count n args == 1

205+ = Just n : mParam args rest

206+ where count n [] = 0

207+ count n (t : ts)

208+ | n `elem` freeNames t = 1 + count n ts

209+ | otherwise = count n ts

210+ mParam args (_ : rest) = Nothing : mParam args rest

190211

191212-- | Elaborate a type provider

192213elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()

@@ -202,11 +223,11 @@ elabProvider info syn fc n ty tm

202223 " as " ++ show using

203224 (e', et) <- elabVal toplevel False using

204225 ctxt <- getContext

205− let e'' = normaliseAll ctxt [] e'

206− logLvl 1 $ "Term is " ++ show e''

226+ let str = show e' in

227+ logLvl 1 $ "Term is " ++ if length str > 200 then (take 200 str) ++ "..." else str

207228 let et' = normaliseAll ctxt [] et

208229 elabType info syn "" fc [] n ty

209− rhs <- execute e''

230+ rhs <- execute e'

210231 logLvl 1 $ "Normalized " ++ show n ++ "'s RHS to " ++ show rhs

211232 providerError rhs

212233 elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i rhs) []]

@@ -219,10 +240,10 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

219240 = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])

220241 cty' <- implicit syn cn cty

221242 i <- getIState

222− cty <- case lookupTy Nothing cn (tt_ctxt i) of

243+ cty <- case lookupTy cn (tt_ctxt i) of

223244 [t] -> return (delab i t)

224245 _ -> fail "Something went inexplicably wrong"

225− cimp <- case lookupCtxt Nothing cn (idris_implicits i) of

246+ cimp <- case lookupCtxt cn (idris_implicits i) of

226247 [imps] -> return imps

227248 let ptys = getProjs [] (renameBs cimp cty)

228249 let ptys_u = getProjs [] cty

@@ -363,7 +384,7 @@ elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

363384elabClauses info fc opts n_in cs = let n = liftname info n_in in

364385 do ctxt <- getContext

365386 -- Check n actually exists, with no definition yet

366− let tys = lookupTy Nothing n ctxt

387+ let tys = lookupTy n ctxt

367388 checkUndefined n ctxt

368389 unless (length tys > 1) $ do

369390 fty <- case tys of

@@ -380,7 +401,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

380401 logLvl 5 $ "Checking collapsibility of " ++ show (ap, fty)

381402 -- FIXME: Really ought to only do this for total functions!

382403 let doNothing = case ap of

383− P _ tn _ -> case lookupCtxt Nothing tn

404+ P _ tn _ -> case lookupCtxt tn

384405 (idris_optimisation ist) of

385406 [oi] -> collapsible oi

386407 _ -> False

@@ -388,7 +409,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

388409 solveDeferred n

389410 ist <- getIState

390411 when doNothing $

391− case lookupCtxt Nothing n (idris_optimisation ist) of

412+ case lookupCtxt n (idris_optimisation ist) of

392413 [oi] -> do let opts = addDef n (oi { collapsible = True })

393414 (idris_optimisation ist)

394415 putIState (ist { idris_optimisation = opts })

@@ -430,6 +451,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

430451 else return []

431452 let pcover = null pmissing

432453 logLvl 2 $ "Optimising patterns"

454+ logLvl 5 $ show optpdef

433455 pdef' <- applyOpts optpdef

434456 logLvl 2 $ "Optimised patterns"

435457 logLvl 5 $ show pdef'

@@ -459,7 +481,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

459481 ctxt <- getContext

460482 ist <- getIState

461483 putIState (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) })

462− case lookupTy (namespace info) n ctxt of

484+ case lookupTy n ctxt of

463485 [ty] -> do updateContext (addCasedef n (inlinable opts)

464486 tcase knowncovering

465487 (AssertTotal `elem` opts)

@@ -470,7 +492,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

470492 totcheck (fc, n)

471493 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

472494 i <- getIState

473− case lookupDef Nothing n (tt_ctxt i) of

495+ case lookupDef n (tt_ctxt i) of

474496 (CaseOp _ _ _ _ _ scargs sc scargs' sc' : _) ->

475497 do let calls = findCalls sc' scargs'

476498 let used = findUsedArgs sc' scargs'

@@ -486,7 +508,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

486508 [] -> return ()

487509 return ()

488510 where

489− checkUndefined n ctxt = case lookupDef Nothing n ctxt of

511+ checkUndefined n ctxt = case lookupDef n ctxt of

490512 [] -> return ()

491513 [TyDecl _ _] -> return ()

492514 _ -> tclift $ tfail (At fc (AlreadyDefined n))

@@ -571,10 +593,10 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

571593 -- pattern bindings

572594 i <- getIState

573595 -- get the parameters first, to pass through to any where block

574− let fn_ty = case lookupTy Nothing fname (tt_ctxt i) of

596+ let fn_ty = case lookupTy fname (tt_ctxt i) of

575597 [t] -> t

576598 _ -> error "Can't happen (elabClause function type)"

577− let fn_is = case lookupCtxt Nothing fname (idris_implicits i) of

599+ let fn_is = case lookupCtxt fname (idris_implicits i) of

578600 [t] -> t

579601 _ -> []

580602 let params = getParamsInType i [] fn_is fn_ty

@@ -678,7 +700,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

678700 = getParamsInType i (n : env) is (instantiate (P Bound n t) sc)

679701 getParamsInType i env is tm@(App f a)

680702 | (P _ tn _, args) <- unApply tm

681− = case lookupCtxt Nothing tn (idris_datatypes i) of

703+ = case lookupCtxt tn (idris_datatypes i) of

682704 [t] -> nub $ paramNames args env (param_pos t) ++

683705 getParamsInType i env is f ++

684706 getParamsInType i env is a

@@ -711,7 +733,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

711733 -- Build the LHS as an "Infer", and pull out its type and

712734 -- pattern bindings

713735 i <- getIState

714− let lhs = addImpl i lhs_in

736+ let lhs = addImplPat i lhs_in

715737 logLvl 5 ("LHS: " ++ showImp True lhs)

716738 ((lhs', dlhs, []), _) <-

717739 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

@@ -809,18 +831,18 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

809831

810832 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

811833 = do i <- getIState

812− let tm = addImpl i tm_in

834+ let tm = addImplPat i tm_in

813835 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

814836 showImp True toplhs)

815837 case matchClause i toplhs tm of

816− Left _ -> fail $ show fc ++ "with clause does not match top level"

838+ Left f -> fail $ show fc ++ ":with clause does not match top level"

817839 Right mvars ->

818840 do logLvl 3 ("Match vars : " ++ show mvars)

819841 lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

820842 return $ PClause fc wname lhs ws rhs wheres

821843 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)

822844 = do i <- getIState

823− let tm = addImpl i tm_in

845+ let tm = addImplPat i tm_in

824846 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

825847 showImp True toplhs)

826848 withs' <- mapM (mkAuxC wname toplhs ns ns') withs

@@ -954,7 +976,7 @@ elabClass info syn doc fc constraints tn ps ds

954976 let conn = case con of

955977 PRef _ n -> n

956978 PApp _ (PRef _ n) _ -> n

957− let conn' = case lookupCtxtName Nothing conn (idris_classes i) of

979+ let conn' = case lookupCtxtName conn (idris_classes i) of

958980 [(n, _)] -> n

959981 _ -> conn

960982 addInstance False conn' cfn

@@ -1015,7 +1037,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

10151037 [PDecl] -> Idris ()

10161038elabInstance info syn fc cs n ps t expn ds

10171039 = do i <- getIState

1018− (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

1040+ (n, ci) <- case lookupCtxtName n (idris_classes i) of

10191041 [c] -> return c

10201042 _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

10211043 let constraint = PApp fc (PRef fc n) (map pexp ps)

@@ -1075,7 +1097,7 @@ elabInstance info syn fc cs n ps t expn ds

10751097 checkNotOverlapping i t n

10761098 | take 2 (show n) == "@@" = return ()

10771099 | otherwise

1078− = case lookupTy Nothing n (tt_ctxt i) of

1100+ = case lookupTy n (tt_ctxt i) of

10791101 [t'] -> let tret = getRetType t

10801102 tret' = getRetType (delab i t') in

10811103 case matchClause i tret' tret of

@@ -1112,7 +1134,7 @@ elabInstance info syn fc cs n ps t expn ds

11121134 | PRef _ n <- getTm p

11131135 = do ps' <- getWParams ps

11141136 ctxt <- getContext

1115− case lookupP Nothing n ctxt of

1137+ case lookupP n ctxt of

11161138 [] -> return (pimp n (PRef fc n) : ps')

11171139 _ -> return ps'

11181140 getWParams (_ : ps) = getWParams ps

@@ -1247,7 +1269,7 @@ elabDecl' what info d@(PClauses f o n ps)

12471269 | what /= ETypes

12481270 = do iLOG $ "Elaborating clause " ++ show n

12491271 i <- getIState -- get the type options too

1250− let o' = case lookupCtxt Nothing n (idris_flags i) of

1272+ let o' = case lookupCtxt n (idris_flags i) of

12511273 [fs] -> fs

12521274 [] -> []

12531275 elabClauses info f (o ++ o') n ps

src/Idris/ElabTerm.hs+17−15

@@ -211,7 +211,7 @@ elab ist info pattern tcgen fn tm

211211 elab' ina (PPatvar fc n) | pattern = patvar n

212212 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

213213 = do ctxt <- get_context

214− let defined = case lookupTy Nothing n ctxt of

214+ let defined = case lookupTy n ctxt of

215215 [] -> False

216216 _ -> True

217217 -- this is to stop us resolve type classes recursively

@@ -221,7 +221,7 @@ elab ist info pattern tcgen fn tm

221221 then do apply (Var n) []; solve

222222 else try (do apply (Var n) []; solve)

223223 (patvar n)

224− where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

224+ where inparamBlock n = case lookupCtxtName n (inblock info) of

225225 [] -> False

226226 _ -> True

227227 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

@@ -334,7 +334,7 @@ elab ist info pattern tcgen fn tm

334334 elab' (ina, g) tm@(PApp fc (PRef _ f) args')

335335 = do let args = {- case lookupCtxt f (inblock info) of

336336 Just ps -> (map (pexp . (PRef fc)) ps ++ args')

337− _ ->-} args'

337+ _ -> -} args'

338338-- newtm <- mkSpecialised ist fc f (map getTm args') tm

339339 env <- get_env

340340 if (f `elem` map fst env && length args' == 1)

@@ -350,11 +350,11 @@ elab ist info pattern tcgen fn tm

350350 let isinf = f == inferCon || tcname f

351351 -- if f is a type class, we need to know its arguments so that

352352 -- we can unify with them

353− case lookupCtxt Nothing f (idris_classes ist) of

353+ case lookupCtxt f (idris_classes ist) of

354354 [] -> return ()

355355 _ -> mapM_ setInjective (map getTm args')

356356 ctxt <- get_context

357− let guarded = isConName Nothing f ctxt

357+ let guarded = isConName f ctxt

358358 ns <- apply (Var f) (map isph args)

359359 ptm <- get_term

360360 g <- goal

@@ -547,7 +547,7 @@ pruneAlt xs = map prune xs

547547pruneByType :: Term -> Context -> [PTerm] -> [PTerm]

548548pruneByType (P _ n _) c as

549549-- if the goal type is polymorphic, keep e

550− | [] <- lookupTy Nothing n c = as

550+ | [] <- lookupTy n c = as

551551 | otherwise

552552 = let asV = filter (headIs True n) as

553553 as' = filter (headIs False n) as in

@@ -563,7 +563,7 @@ pruneByType (P _ n _) c as

563563 headIs _ _ _ = True -- keep if it's not an application

564564

565565 typeHead var f f'

566− = case lookupTy Nothing f' c of

566+ = case lookupTy f' c of

567567 [ty] -> let ty' = normalise c [] ty in

568568 case unApply (getRetTy ty') of

569569 (P _ ftyn _, _) -> ftyn == f

@@ -596,7 +596,7 @@ trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")

596596findInstances :: IState -> Term -> [Name]

597597findInstances ist t

598598 | (P _ n _, _) <- unApply t

599− = case lookupCtxt Nothing n (idris_classes ist) of

599+ = case lookupCtxt n (idris_classes ist) of

600600 [CI _ _ _ _ ins] -> ins

601601 _ -> []

602602 | otherwise = []

@@ -658,7 +658,7 @@ resolveTC depth fn ist

658658-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist

659659-- else do

660660 -- if there's a hole in the goal, don't even try

661− let imps = case lookupCtxtName Nothing n (idris_implicits ist) of

661+ let imps = case lookupCtxtName n (idris_implicits ist) of

662662 [] -> []

663663 [args] -> map isImp (snd args) -- won't be overloaded!

664664 ps <- get_probs

@@ -695,10 +695,12 @@ collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)

695695collectDeferred t = return t

696696

697697-- Running tactics directly

698+-- if a tactic adds unification problems, return an error

698699

699700runTac :: Bool -> IState -> PTactic -> ElabD ()

700−runTac autoSolve ist tac = do env <- get_env

701− runT (fmap (addImplBound ist (map fst env)) tac)

701+runTac autoSolve ist tac

702+ = do env <- get_env

703+ no_errors $ runT (fmap (addImplBound ist (map fst env)) tac)

702704 where

703705 runT (Intro []) = do g <- goal

704706 attack; intro (bname g)

@@ -716,7 +718,7 @@ runTac autoSolve ist tac = do env <- get_env

716718 runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm

717719 when autoSolve solveAll

718720 runT (Refine fn [])

719− = do (fn', imps) <- case lookupCtxtName Nothing fn (idris_implicits ist) of

721+ = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

720722 [] -> do a <- envArgs fn

721723 return (fn, a)

722724 -- FIXME: resolve ambiguities

@@ -1200,7 +1202,7 @@ solveAll = try (do solve; solveAll) (return ())

12001202mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm

12011203mkSpecialised i fc n args def

12021204 = do let tm' = def

1203− case lookupCtxt Nothing n (idris_statics i) of

1205+ case lookupCtxt n (idris_statics i) of

12041206 [] -> return tm'

12051207 [as] -> if (not (or as)) then return tm' else

12061208 mkSpecDecl i n (zip args as) tm'

@@ -1227,8 +1229,8 @@ mkSpecDecl i n pargs tm'

12271229 cg = idris_callgraph i

12281230

12291231 staticFnNames tm | (P _ f _, as) <- unApply tm

1230− = if not (isFnName Nothing f ctxt) then []

1231− else case lookupCtxt Nothing f cg of

1232+ = if not (isFnName f ctxt) then []

1233+ else case lookupCtxt f cg of

12321234 [ns] -> f : f : [] --(ns \\ [f])

12331235 [] -> [f,f]

12341236 _ -> []

src/Idris/IBC.hs+40−26

@@ -18,6 +18,8 @@ import Control.Monad.State hiding (get, put)

1818import System.FilePath

1919import System.Directory

2020

21+import Debug.Trace

22+

2123import Paths_idris

2224

2325ibcVersion :: Word8

@@ -48,6 +50,7 @@ data IBCFile = IBCFile { ver :: Word8,

4850 ibc_docstrings :: [(Name, String)],

4951 ibc_coercions :: [Name]

5052 }

53+ deriving Show

5154{-!

5255deriving instance Binary IBCFile

5356!-}

@@ -82,28 +85,28 @@ mkIBC (i:is) f = do ist <- getIState

8285 mkIBC is f'

8386

8487ibc i (IBCFix d) f = return f { ibc_fixes = d : ibc_fixes f }

85−ibc i (IBCImp n) f = case lookupCtxt Nothing n (idris_implicits i) of

88+ibc i (IBCImp n) f = case lookupCtxt n (idris_implicits i) of

8689 [v] -> return f { ibc_implicits = (n,v): ibc_implicits f }

8790 _ -> fail "IBC write failed"

8891ibc i (IBCStatic n) f

89− = case lookupCtxt Nothing n (idris_statics i) of

92+ = case lookupCtxt n (idris_statics i) of

9093 [v] -> return f { ibc_statics = (n,v): ibc_statics f }

9194 _ -> fail "IBC write failed"

9295ibc i (IBCClass n) f

93− = case lookupCtxt Nothing n (idris_classes i) of

96+ = case lookupCtxt n (idris_classes i) of

9497 [v] -> return f { ibc_classes = (n,v): ibc_classes f }

9598 _ -> fail "IBC write failed"

9699ibc i (IBCInstance int n ins) f

97100 = return f { ibc_instances = (int,n,ins): ibc_instances f }

98101ibc i (IBCDSL n) f

99− = case lookupCtxt Nothing n (idris_dsls i) of

102+ = case lookupCtxt n (idris_dsls i) of

100103 [v] -> return f { ibc_dsls = (n,v): ibc_dsls f }

101104 _ -> fail "IBC write failed"

102105ibc i (IBCData n) f

103− = case lookupCtxt Nothing n (idris_datatypes i) of

106+ = case lookupCtxt n (idris_datatypes i) of

104107 [v] -> return f { ibc_datatypes = (n,v): ibc_datatypes f }

105108 _ -> fail "IBC write failed"

106−ibc i (IBCOpt n) f = case lookupCtxt Nothing n (idris_optimisation i) of

109+ibc i (IBCOpt n) f = case lookupCtxt n (idris_optimisation i) of

107110 [v] -> return f { ibc_optimise = (n,v): ibc_optimise f }

108111 _ -> fail "IBC write failed"

109112ibc i (IBCSyntax n) f = return f { ibc_syntax = n : ibc_syntax f }

@@ -113,13 +116,13 @@ ibc i (IBCObj n) f = return f { ibc_objs = n : ibc_objs f }

113116ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }

114117ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

115118ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

116−ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

119+ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of

117120 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

118121 _ -> fail "IBC write failed"

119−ibc i (IBCDoc n) f = case lookupCtxt Nothing n (idris_docstrings i) of

122+ibc i (IBCDoc n) f = case lookupCtxt n (idris_docstrings i) of

120123 [v] -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }

121124 _ -> fail "IBC write failed"

122−ibc i (IBCCG n) f = case lookupCtxt Nothing n (idris_callgraph i) of

125+ibc i (IBCCG n) f = case lookupCtxt n (idris_callgraph i) of

123126 [v] -> return f { ibc_cg = (n,v) : ibc_cg f }

124127 _ -> fail "IBC write failed"

125128ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

@@ -246,7 +249,11 @@ pLibs :: [String] -> Idris ()

246249pLibs ls = mapM_ addLib ls

247250

248251pDyLibs :: [String] -> Idris ()

249−pDyLibs ls = mapM_ addDyLib ls

252+pDyLibs ls = do res <- mapM (addDyLib . return) ls

253+ mapM_ checkLoad res

254+ return ()

255+ where checkLoad (Left _) = return ()

256+ checkLoad (Right err) = fail err

250257

251258pHdrs :: [String] -> Idris ()

252259pHdrs hs = mapM_ addHdr hs

@@ -327,16 +334,21 @@ instance Binary FC where

327334

328335instance Binary Name where

329336 put x

330− = case x of

331− UN x1 -> do putWord8 0

332− put x1

333− NS x1 x2 -> do putWord8 1

337+ = {-# SCC "putName" #-}

338+ case x of

339+ UN x1 -> {-# SCC "putUN" #-}

340+ do putWord8 0

341+ {-# SCC "putNString" #-} put x1

342+ NS x1 x2 -> {-# SCC "putNS" #-}

343+ do putWord8 1

334344 put x1

335345 put x2

336− MN x1 x2 -> do putWord8 2

346+ MN x1 x2 -> {-# SCC "putMN" #-}

347+ do putWord8 2

337348 put x1

338349 put x2

339− NErased -> putWord8 3

350+ NErased -> {-# SCC "putNErased" #-}

351+ putWord8 3

340352 get

341353 = do i <- getWord8

342354 case i of

@@ -528,9 +540,10 @@ instance Binary NameType where

528540 _ -> error "Corrupted binary data for NameType"

529541

530542

531−instance (Binary n) => Binary (TT n) where

543+instance {-(Binary n) =>-} Binary (TT Name) where

532544 put x

533− = case x of

545+ = {-# SCC "putTT" #-}

546+ case x of

534547 P x1 x2 x3 -> do putWord8 0

535548 put x1

536549 put x2

@@ -613,7 +626,8 @@ instance Binary SC where

613626

614627instance Binary CaseAlt where

615628 put x

616− = case x of

629+ = {-# SCC "putCaseAlt" #-}

630+ case x of

617631 ConCase x1 x2 x3 x4 -> do putWord8 0

618632 put x1

619633 put x2

@@ -642,17 +656,16 @@ instance Binary CaseAlt where

642656

643657instance Binary Def where

644658 put x

645− = case x of

659+ = {-# SCC "putDef" #-}

660+ case x of

646661 Function x1 x2 -> do putWord8 0

647662 put x1

648663 put x2

649664 TyDecl x1 x2 -> do putWord8 1

650665 put x1

651666 put x2

652− Operator x1 x2 x3 -> do putWord8 2

653− put x1

654− put x2

655− put x3

667+ -- all primitives just get added at the start, don't write

668+ Operator x1 x2 x3 -> do return ()

656669 CaseOp x1 x2 x3 x3a x4 x5 x6 x7 x8 ->

657670 do putWord8 3

658671 put x1

@@ -750,8 +763,9 @@ instance Binary Totality where

750763 _ -> error "Corrupted binary data for Totality"

751764

752765instance Binary IBCFile where

753− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)

754− = do put x1

766+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24)

767+ = {-# SCC "putIBCFile" #-}

768+ do put x1

755769 put x2

756770 put x3

757771 put x4

src/Idris/Parser.hs+19−11

@@ -30,6 +30,7 @@ import qualified Text.Parsec.Token as PTok

3030import Data.List

3131import Data.List.Split(splitOn)

3232import Control.Monad.State

33+import Control.Monad.Error

3334import Debug.Trace

3435import Data.Maybe

3536import System.FilePath

@@ -273,7 +274,7 @@ pfc = do s <- getPosition

273274pImport :: IParser String

274275pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')

275276 return (toPath f)

276− where toPath n = foldl1 (</>) $ splitOn "." n

277+ where toPath n = foldl1' (</>) $ splitOn "." n

277278

278279-- | A program is a list of declarations, possibly with associated

279280-- documentation strings.

@@ -613,7 +614,6 @@ pNoExtExpr syn =

613614 <|> pRewriteTerm syn

614615 <|> pPi syn

615616 <|> pDoBlock syn

616− <|> pComprehension syn

617617

618618pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm

619619pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))

@@ -763,6 +763,7 @@ pSimpleExpr syn =

763763 fc <- pfc

764764 return (PInferRef fc x))

765765 <|> try (pList syn)

766+ <|> try (pComprehension syn)

766767 <|> try (pAlt syn)

767768 <|> try (pIdiom syn)

768769 <|> try (do lchar '('

@@ -881,7 +882,7 @@ pApp syn = do f <- pSimpleExpr syn

881882 return (dslify i $ PApp fc f args)

882883 where

883884 dslify i (PApp fc (PRef _ f) [a])

884− | [d] <- lookupCtxt Nothing f (idris_dsls i)

885+ | [d] <- lookupCtxt f (idris_dsls i)

885886 = desugar (syn { dsl_info = d }) i (getTm a)

886887 dslify i t = t

887888

@@ -975,7 +976,9 @@ pLet syn = try (do reserved "let"; n <- pName;

975976 return (PCase fc v [(pat, sc)]))

976977

977978pPi syn =

978− try (do lazy <- option False (do lchar '|'; return True)

979+ try (do lazy <- if implicitAllowed syn -- laziness is top level only

980+ then option False (do lchar '|'; return True)

981+ else return False

979982 st <- pStatic

980983 lchar '('; xt <- tyDeclList syn; lchar ')'

981984 doc <- option "" (pDocComment '^')

@@ -1361,7 +1364,8 @@ pClause syn

13611364 cargs <- many (pConstraintArg syn)

13621365 iargs <- many (pImplicitArg (syn { inPattern = True } ))

13631366 fc <- pfc

1364− args <- many (pArgExpr syn)

1367+ args <- many (try (pImplicitArg (syn { inPattern = True } ))

1368+ <|> (fmap pexp (pArgExpr syn)))

13651369 wargs <- many (pWExpr syn)

13661370 rhs <- pRHS syn n

13671371 ist <- getState

@@ -1373,7 +1377,7 @@ pClause syn

13731377 do pTerminator

13741378 return ([], [])]

13751379 let capp = PApp fc (PRef fc n)

1376− (iargs ++ cargs ++ map pexp args)

1380+ (iargs ++ cargs ++ args)

13771381 ist <- getState

13781382 setState (ist { lastParse = Just n })

13791383 return $ PClause fc n capp wargs rhs wheres)

@@ -1399,10 +1403,11 @@ pClause syn

13991403 cargs <- many (pConstraintArg syn)

14001404 iargs <- many (pImplicitArg (syn { inPattern = True } ))

14011405 fc <- pfc

1402− args <- many (pArgExpr syn)

1406+ args <- many (try (pImplicitArg (syn { inPattern = True } ))

1407+ <|> (fmap pexp (pArgExpr syn)))

14031408 wargs <- many (pWExpr syn)

14041409 let capp = PApp fc (PRef fc n)

1405− (iargs ++ cargs ++ map pexp args)

1410+ (iargs ++ cargs ++ args)

14061411 ist <- getState

14071412 setState (ist { lastParse = Just n })

14081413 reserved "with"

@@ -1510,9 +1515,12 @@ pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;

15101515 putIState (i { default_total = tot }))])

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

15121517 return [PDirective (setLogLevel (fromInteger i))])

1513− <|> try (do lchar '%'; reserved "dynamic"; lib <- strlit;

1514− return [PDirective (do addIBC (IBCDyLib lib)

1515− addDyLib lib)])

1518+ <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 strlit (lchar ',');

1519+ return [PDirective (do added <- addDyLib libs

1520+ case added of

1521+ Left lib -> addIBC (IBCDyLib (lib_name lib))

1522+ Right msg ->

1523+ fail $ msg)])

15161524 <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";

15171525 return [PDirective (addLangExt TypeProviders)])

15181526

src/Idris/Primitives.hs+1

@@ -439,6 +439,7 @@ p_floatFloor = p_fPrim (fromInteger . floor)

439439p_floatCeil = p_fPrim (fromInteger . ceiling)

440440

441441p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))

442+p_strLen _ = Nothing

442443p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)

443444p_strHead _ = Nothing

444445p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)

src/Idris/Prover.hs+1−1

@@ -26,7 +26,7 @@ prover :: Bool -> Name -> Idris ()

2626prover lit x =

2727 do ctxt <- getContext

2828 i <- getIState

29− case lookupTy Nothing x ctxt of

29+ case lookupTy x ctxt of

3030 [t] -> if elem x (idris_metavars i)

3131 then prove ctxt lit x t

3232 else fail $ show x ++ " is not a metavariable"

src/Idris/Providers.hs+7−13

@@ -1,3 +1,4 @@

1+{-# LANGUAGE PatternGuards #-}

12module Idris.Providers where

23

34import Core.TT

@@ -19,16 +20,9 @@ unProv fc tm = PApp fc (PRef fc $ NS (UN "unProv") ["Providers"]) [PExp 0 False

1920

2021-- | Handle an error, if the type provider returned an error. Otherwise do nothing.

2122providerError :: TT Name -> Idris ()

22−providerError tm = case unApply tm of

23− (P _ (NS (UN "unProv") ["Providers"]) _, [_, tm']) ->

24− case unApply tm' of

25− (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) ->

26− do str <- execute err

27− case (unApply str) of

28− (Constant (Str msg), []) ->

29− ierror . ProviderError $ msg

30− (P _ (UN "prim__IO") _, [_, (Constant (Str msg))]) ->

31− ierror . ProviderError $ msg

32− _ -> fail "Error in type provider."

33− _ -> return ()

34− _ -> return ()

23+providerError tm | (P _ unProv_case _, _:_:tm':_) <- unApply tm

24+ , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply tm' =

25+ case err of

26+ Constant (Str msg) -> ierror . ProviderError $ msg

27+ _ -> fail "Error in type provider"

28+ | otherwise = return ()

src/Idris/REPL.hs+36−26

@@ -129,7 +129,7 @@ resolveProof :: Name -> Idris Name

129129resolveProof n'

130130 = do i <- getIState

131131 ctxt <- getContext

132− n <- case lookupNames Nothing n' ctxt of

132+ n <- case lookupNames n' ctxt of

133133 [x] -> return x

134134 [] -> return n'

135135 ns -> fail $ pshow i (CantResolveAlts (map show ns))

@@ -196,21 +196,21 @@ process fn (ExecVal t)

196196 = do ctxt <- getContext

197197 ist <- getIState

198198 (tm, ty) <- elabVal toplevel False t

199− let tm' = normaliseAll ctxt [] tm

199+-- let tm' = normaliseAll ctxt [] tm

200200 let ty' = normaliseAll ctxt [] ty

201− res <- execute tm'

201+ res <- execute tm

202202 imp <- impShow

203203 iputStrLn (showImp imp (delab ist res) ++ " : " ++

204204 showImp imp (delab ist ty'))

205205 return ()

206206process fn (Check (PRef _ n))

207− = do ctxt <- getContext

208− ist <- getIState

209− imp <- impShow

210− case lookupTy Nothing n ctxt of

211− ts@(_:_) -> mapM_ (\t -> iputStrLn $ show n ++ " : " ++

212− showImp imp (delab ist t)) ts

213− [] -> iputStrLn $ "No such variable " ++ show n

207+ = do ctxt <- getContext

208+ ist <- getIState

209+ imp <- impShow

210+ case lookupNames n ctxt of

211+ ts@(_:_) -> mapM_ (\n -> iputStrLn $ show n ++ " : " ++

212+ showImp imp (delabTy ist n)) ts

213+ [] -> iputStrLn $ "No such variable " ++ show n

214214process fn (Check t) = do (tm, ty) <- elabVal toplevel False t

215215 ctxt <- getContext

216216 ist <- getIState

@@ -220,7 +220,7 @@ process fn (Check t) = do (tm, ty) <- elabVal toplevel False t

220220 showImp imp (delab ist ty))

221221

222222process fn (DocStr n) = do i <- getIState

223− case lookupCtxtName Nothing n (idris_docstrings i) of

223+ case lookupCtxtName n (idris_docstrings i) of

224224 [] -> iputStrLn $ "No documentation for " ++ show n

225225 ns -> mapM_ showDoc ns

226226 where showDoc (n, d)

@@ -237,8 +237,8 @@ process fn Universes = do i <- getIState

237237 OK _ -> iputStrLn "Universes OK"

238238process fn (Defn n) = do i <- getIState

239239 iputStrLn "Compiled patterns:\n"

240− liftIO $ print (lookupDef Nothing n (tt_ctxt i))

241− case lookupCtxt Nothing n (idris_patdefs i) of

240+ liftIO $ print (lookupDef n (tt_ctxt i))

241+ case lookupCtxt n (idris_patdefs i) of

242242 [] -> return ()

243243 [d] -> do iputStrLn "Original definiton:\n"

244244 mapM_ (printCase i) d

@@ -255,25 +255,25 @@ process fn (TotCheck n) = do i <- getIState

255255 _ -> return ()

256256process fn (DebugInfo n)

257257 = do i <- getIState

258− let oi = lookupCtxtName Nothing n (idris_optimisation i)

258+ let oi = lookupCtxtName n (idris_optimisation i)

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

260− let si = lookupCtxt Nothing n (idris_statics i)

260+ let si = lookupCtxt n (idris_statics i)

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

262− let di = lookupCtxt Nothing n (idris_datatypes i)

262+ let di = lookupCtxt n (idris_datatypes i)

263263 when (not (null di)) $ iputStrLn (show di)

264− let d = lookupDef Nothing n (tt_ctxt i)

264+ let d = lookupDef n (tt_ctxt i)

265265 when (not (null d)) $ liftIO $

266266 do print (head d)

267− let cg = lookupCtxtName Nothing n (idris_callgraph i)

267+ let cg = lookupCtxtName n (idris_callgraph i)

268268 findUnusedArgs (map fst cg)

269269 i <- getIState

270− let cg' = lookupCtxtName Nothing n (idris_callgraph i)

270+ let cg' = lookupCtxtName n (idris_callgraph i)

271271 sc <- checkSizeChange n

272272 iputStrLn $ "Size change: " ++ show sc

273273 when (not (null cg')) $ do iputStrLn "Call graph:\n"

274274 iputStrLn (show cg')

275275process fn (Info n) = do i <- getIState

276− case lookupCtxt Nothing n (idris_classes i) of

276+ case lookupCtxt n (idris_classes i) of

277277 [c] -> classInfo c

278278 _ -> iputStrLn "Not a class"

279279process fn (Search t) = iputStrLn "Not implemented"

@@ -299,8 +299,17 @@ process fn (RmProof n')

299299 let ms = idris_metavars i

300300 putIState $ i { idris_metavars = n : ms }

301301

302−process fn (AddProof prf)

303− = do let fb = fn ++ "~"

302+process fn' (AddProof prf)

303+ = do fn <- do

304+ ex <- liftIO $ doesFileExist fn'

305+ let fnExt = fn' <.> "idr"

306+ exExt <- liftIO $ doesFileExist fnExt

307+ if ex

308+ then return fn'

309+ else if exExt

310+ then return fnExt

311+ else fail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"

312+ let fb = fn ++ "~"

304313 liftIO $ copyFile fn fb -- make a backup in case something goes wrong!

305314 prog <- liftIO $ readFile fb

306315 i <- getIState

@@ -330,7 +339,7 @@ process fn (ShowProof n')

330339process fn (Prove n')

331340 = do ctxt <- getContext

332341 ist <- getIState

333− n <- case lookupNames Nothing n' ctxt of

342+ n <- case lookupNames n' ctxt of

334343 [x] -> return x

335344 [] -> return n'

336345 ns -> fail $ pshow ist (CantResolveAlts (map show ns))

@@ -381,7 +390,7 @@ process fn (Pattelab t)

381390 iputStrLn $ show tm ++ "\n\n : " ++ show ty

382391

383392process fn (Missing n) = do i <- getIState

384− case lookupDef Nothing n (tt_ctxt i) of

393+ case lookupDef n (tt_ctxt i) of

385394 [CaseOp _ _ _ _ _ args t _ _]

386395 -> do tms <- genMissing n args t

387396 iputStrLn (showSep "\n" (map (showImp True) tms))

@@ -431,7 +440,7 @@ dumpInstance :: Name -> Idris ()

431440dumpInstance n = do i <- getIState

432441 ctxt <- getContext

433442 imp <- impShow

434− case lookupTy Nothing n ctxt of

443+ case lookupTy n ctxt of

435444 ts -> mapM_ (\t -> iputStrLn $ showImp imp (delab i t)) ts

436445

437446showTotal t@(Partial (Other ns)) i

@@ -552,6 +561,7 @@ idrisMain opts =

552561 [] -> setIBCSubDir ""

553562 (d:_) -> setIBCSubDir d

554563 setImportDirs importdirs

564+

555565 addPkgDir "base"

556566 mapM_ addPkgDir pkgdirs

557567 elabPrims

@@ -636,7 +646,7 @@ getLanguageExt (Extension e) = Just e

636646getLanguageExt _ = Nothing

637647

638648opt :: (Opt -> Maybe a) -> [Opt] -> [a]

639−opt = mapMaybe

649+opt = mapMaybe

640650

641651ver = showVersion version

642652

src/Idris/REPLParser.hs+1−1

@@ -66,7 +66,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

6666 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

6767 <|> do eof; return NOP

6868

69− where toPath n = foldl1 (</>) $ splitOn "." n

69+ where toPath n = foldl1' (</>) $ splitOn "." n

7070

7171pOption :: IParser Opt

7272pOption = do discard (symbol "errorcontext"); return ErrContext

src/Idris/UnusedArgs.hs+2−2

@@ -15,7 +15,7 @@ findUnusedArgs ns = mapM_ traceUnused ns

1515traceUnused :: Name -> Idris ()

1616traceUnused n

1717 = do i <- getIState

18− case lookupCtxt Nothing n (idris_callgraph i) of

18+ case lookupCtxt n (idris_callgraph i) of

1919 [CGInfo args calls scg usedns _] ->

2020 do let argpos = zip args [0..]

2121 let fargs = concatMap (getFargpos calls) argpos

@@ -39,7 +39,7 @@ used path g j

3939 | otherwise

4040 = do logLvl 5 $ (show ((g, j) : path))

4141 i <- getIState

42− case lookupCtxt Nothing g (idris_callgraph i) of

42+ case lookupCtxt g (idris_callgraph i) of

4343 [CGInfo args calls scg usedns unused] ->

4444 if (j >= length args)

4545 then -- overapplied, assume used

src/Main.hs+3

@@ -29,6 +29,7 @@ import Idris.Imports

2929import Idris.Error

3030

3131import Util.System ( getLibFlags, getIdrisLibDir, getIncFlags )

32+import Util.DynamicLinker

3233

3334import Pkg.Package

3435

@@ -94,3 +95,5 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

9495 "\t--link Show C library directories and exit (for C linking)\n" ++

9596 "\t--include Show C include directories and exit (for C linking)\n" ++

9697 "\t--target [target] Type the target: C, Java, bytecode, javascript, node\n"

98+

99+

src/Pkg/Package.hs+3−3

@@ -71,7 +71,7 @@ buildMods :: [Opt] -> [Name] -> IO ()

7171buildMods opts ns = do let f = map (toPath . show) ns

7272 idris (map Filename f ++ opts)

7373 return ()

74− where toPath n = foldl1 (</>) $ splitOn "." n

74+ where toPath n = foldl1' (</>) $ splitOn "." n

7575

7676testLib :: Bool -> String -> String -> IO Bool

7777testLib warn p f

@@ -93,7 +93,7 @@ rmIBC :: Name -> IO ()

9393rmIBC m = rmFile $ toIBCFile m

9494

9595toIBCFile (UN n) = n ++ ".ibc"

96−toIBCFile (NS n ns) = foldl1 (</>) (reverse (toIBCFile n : ns))

96+toIBCFile (NS n ns) = foldl1' (</>) (reverse (toIBCFile n : ns))

9797

9898installIBC :: String -> Name -> IO ()

9999installIBC p m = do let f = toIBCFile m

@@ -105,7 +105,7 @@ installIBC p m = do let f = toIBCFile m

105105 copyFile f (destdir </> takeFileName f)

106106 return ()

107107 where getDest (UN n) = ""

108− getDest (NS n ns) = foldl1 (</>) (reverse (getDest n : ns))

108+ getDest (NS n ns) = foldl1' (</>) (reverse (getDest n : ns))

109109

110110installObj :: String -> String -> IO ()

111111installObj p o = do d <- getDataDir

src/Util/DynamicLinker.hs+25−4

@@ -4,8 +4,14 @@

44module Util.DynamicLinker where

55

66import Foreign.LibFFI

7−import Foreign.Ptr (nullPtr, FunPtr, nullFunPtr)

7+import Foreign.Ptr (nullPtr, FunPtr, nullFunPtr,castPtrToFunPtr)

8+#ifndef WINDOWS

89import System.Posix.DynamicLinker

10+#else

11+import System.Win32.DLL

12+import System.Win32.Types

13+type DL = HMODULE

14+#endif

915

1016hostDynamicLibExt :: String

1117#ifdef LINUX

@@ -16,22 +22,37 @@ hostDynamicLibExt = "dylib"

1622hostDynamicLibExt = "dll"

1723#endif

1824

25+data ForeignFun = forall a. Fun { fun_name :: String

26+ , fun_handle :: FunPtr a

27+ }

28+

1929data DynamicLib = Lib { lib_name :: String

2030 , lib_handle :: DL

2131 }

2232

33+#ifndef WINDOWS

2334tryLoadLib :: String -> IO (Maybe DynamicLib)

2435tryLoadLib lib = do handle <- dlopen (lib ++ "." ++ hostDynamicLibExt) [RTLD_NOW]

2536 if undl handle == nullPtr

2637 then return Nothing

2738 else return . Just $ Lib lib handle

2839

29−data ForeignFun = forall a. Fun { fun_name :: String

30− , fun_handle :: FunPtr a

31− }

3240

3341tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)

3442tryLoadFn fn (Lib _ h) = do cFn <- dlsym h fn

3543 if cFn == nullFunPtr

3644 then return Nothing

3745 else return . Just $ Fun fn cFn

46+#else

47+tryLoadLib :: String -> IO (Maybe DynamicLib)

48+tryLoadLib lib = do handle <- loadLibrary (lib ++ "." ++ hostDynamicLibExt)

49+ if handle == nullPtr

50+ then return Nothing

51+ else return . Just $ Lib lib handle

52+

53+tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)

54+tryLoadFn fn (Lib _ h) = do cFn <- getProcAddress h fn

55+ if cFn == nullPtr

56+ then return Nothing

57+ else return . Just $ Fun fn (castPtrToFunPtr cFn)

58+#endif

src/Util/System.hs+1−1

@@ -1,7 +1,7 @@

11{-# LANGUAGE CPP #-}

22module Util.System(tempfile,withTempdir,environment,getCC,

33 getLibFlags,getIdrisLibDir,getIncFlags,rmFile,

4− getMvn,getExecutablePom) where

4+ getMvn,getExecutablePom,catchIO) where

55

66-- System helper functions.

77import Control.Monad (when)

test/README+4

@@ -22,5 +22,9 @@ Tests:

2222020: implicit conversions

2323021: effects

2424022: dynamic C library loading and interpreter IO

25+023: trivial (non-I/O) type providers

26+024: interpreter I/O

27+025: memory effects

28+026: simple file-I/O-based type provider

2529

2630regxxx: various regression tests

test/reg017/expectednew file+1

@@ -0,0 +1 @@

1+ssssO

test/reg017/reg017.idrnew file+13

@@ -0,0 +1,13 @@

1+module Main

2+

3+foo : { t : Type } ->

4+ (a : t) ->

5+ { default tactics { refine refl; solve; } prfA : a = a } ->

6+ (b : Nat) ->

7+ (c : Nat) ->

8+ { default tactics { refine refl; solve; } prfBC : b = c } ->

9+ Nat

10+foo {t} a {prfA = p} b c {prfBC} = b

11+

12+main : IO ()

13+main = print $ foo 3 4 4

test/reg017/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris $@ reg017.idr -o reg017

3+./reg017

4+rm -f reg017 *.ibc

test/test022/test022.idr+1−1

@@ -1,6 +1,6 @@

11module Main

22

3−%dynamic "libm"

3+%dynamic "dummy", "libm", "msvcrt"

44

55x : Float

66x = unsafePerformIO (mkForeign (FFun "sin" [FFloat] FFloat) 1.6)

test/test023/test023.idr+4−4

@@ -7,8 +7,8 @@ import Providers

77%language TypeProviders

88

99-- Provide the Unit type

10−goodProvider : Provider Type

11−goodProvider = Provide (return (the Type ()))

10+goodProvider : IO (Provider Type)

11+goodProvider = return (Provide (the Type ()))

1212

1313%provide (Unit : Type) with goodProvider

1414

@@ -16,8 +16,8 @@ foo : Unit

1616foo = ()

1717

1818-- Always fail

19−badProvider : Provider Type

20−badProvider = Error (return "Always fails")

19+badProvider : IO (Provider Type)

20+badProvider = return (Error "Always fails")

2121

2222%provide (t : Type) with badProvider

2323

test/test024/expectednew file+3

@@ -0,0 +1,3 @@

1+Type checking ./test024.idr

2+testtest

3+() : ()

test/test024/inputnew file+2

@@ -0,0 +1,2 @@

1+:x unsafePerformIO main

2+test

test/test024/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris --quiet test024.idr < input

3+rm -f *.ibc

test/test024/test024.idrnew file+6

@@ -0,0 +1,6 @@

1+module Main

2+

3+main : IO ()

4+main = do l <- getLine

5+ let ll = l ++ l

6+ putStrLn ll

test/test025/expectednew file+1

@@ -0,0 +1 @@

1+[1, 2, 3, 4]

test/test025/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris -p effects $@ test025.idr -o test025

3+./test025

4+rm -f test025 *.ibc

test/test025/test025.idrnew file+34

@@ -0,0 +1,34 @@

1+module Main

2+

3+import Effects

4+import Effect.Memory

5+import Control.IOExcept

6+

7+MemoryIO : Type -> Type -> Type -> Type

8+MemoryIO td ts r = Eff (IOExcept String) [ Dst ::: RAW_MEMORY td

9+ , Src ::: RAW_MEMORY ts ] r

10+

11+inpVect : Vect Bits8 5

12+inpVect = map prim__intToB8 [0, 1, 2, 3, 5]

13+

14+sub1 : Vect Bits8 n -> Vect Bits8 n

15+sub1 xs = map (prim__intToB8 . (\ x => x - 1) . prim__B32ToInt . prim__sextB8_32) xs

16+

17+testMemory : MemoryIO () () (Vect Int 4)

18+testMemory = do Src :- allocate 5

19+ Src :- poke 0 inpVect oh

20+ Dst :- allocate 5

21+ Dst :- initialize (prim__intToB8 1) 2 oh

22+ move 2 2 3 oh oh

23+ Src :- free

24+ end <- Dst :- peek 4 1 oh

25+ Dst :- poke 4 (sub1 end) oh

26+ res <- Dst :- peek 1 4 oh

27+ Dst :- free

28+ return (map (prim__B32ToInt . prim__sextB8_32) res)

29+

30+main : IO ()

31+main = do ioe_run (run [Dst := (), Src := ()] testMemory)

32+ (\err => print err) (\ok => print ok)

33+

34+

test/test026/expectednew file+3

@@ -0,0 +1,3 @@

1+Type checking ./test026.idr

2+2 : Int

3+2 : Nat

test/test026/inputnew file+2

@@ -0,0 +1,2 @@

1+foo

2+bar

test/test026/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris --quiet test026.idr < input

3+rm -f *.ibc

test/test026/test026.idrnew file+26

@@ -0,0 +1,26 @@

1+module Main

2+

3+-- Simple test case for trivial type providers.

4+

5+import Providers

6+

7+%language TypeProviders

8+

9+strToType : String -> Type

10+strToType "Int" = Int

11+strToType _ = Nat

12+

13+-- If the file contains "Int", provide Int as a type, otherwise provide Nat

14+fromFile : String -> IO (Provider Type)

15+fromFile fname = do str <- readFile fname

16+ return (Provide (strToType str))

17+

18+%provide (T1 : Type) with fromFile "theType"

19+%provide (T2 : Type) with fromFile "theOtherType"

20+

21+foo : T1

22+foo = 2

23+

24+bar : T2

25+bar = 2

26+

test/test026/theOtherTypenew file+1

@@ -0,0 +1 @@

1+Nat

test/test026/theTypenew file+1

@@ -0,0 +1 @@

1+Int

tutorial/idris-tutorial.tex+1

@@ -11,6 +11,7 @@

1111\input{library.ltx}

1212

1313\newcommand{\Idris}{\textsc{Idris}}

14+\newcommand{\version}{0.9.8}

1415

1516\title{Programming in \Idris{}: a tutorial}

1617\author{Edwin Brady \\ \url{eb@cs.st-andrews.ac.uk}}

tutorial/interp.tex+2−2

@@ -339,12 +339,12 @@ type to another if possible. Here, it converts a string to

339339an integer, giving 0 if the input is invalid. An example run of this program

340340at the \Idris{} interactive environment is shown in Figure \ref{factrun}.

341341

342−\begin{SaveVerbatim}{factrun}

342+\begin{SaveVerbatim}[commandchars=^\{\}]{factrun}

343343

344344$ idris interp.idr

345345 ____ __ _

346346 / _/___/ /____(_)____

347− / // __ / ___/ / ___/ Version 0.9.7

347+ / // __ / ___/ / ___/ Version ^version{}

348348 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

349349 /___/\__,_/_/ /_/____/ Type :? for help

350350

tutorial/intro.tex+1−1

@@ -62,7 +62,7 @@ verifying systems software.

6262\subsection{Example Code}

6363

6464This tutorial includes some example code, which has been tested with \Idris{} version

65−0.9.7. The files are available in the \Idris{} distribution,

65+\version{}. The files are available in the \Idris{} distribution,

6666so that you can try them out easily,

6767under \texttt{tutorial/examples}. However, it is strongly recommended that you

6868type them in yourself, rather than simply loading and reading them.

tutorial/starting.tex+6−6

@@ -74,12 +74,12 @@ interactive environment.

7474Entering \texttt{idris} at the shell prompt starts up the interactive

7575environment. You should see something like the following:

7676

77−\begin{SaveVerbatim}{prompt1}

77+\begin{SaveVerbatim}[commandchars=^\{\}]{prompt1}

7878

7979$ idris

8080 ____ __ _

8181 / _/___/ /____(_)____

82− / // __ / ___/ / ___/ Version 0.9.7

82+ / // __ / ___/ / ___/ Version ^version{}

8383 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

8484 /___/\__,_/_/ /_/____/ Type :? for help

8585

@@ -98,8 +98,8 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which

9898\texttt{hello.idr} is loaded, the type of \texttt{main} is checked and then

9999the program is compiled to the executable \texttt{hello}.

100100

101−\begin{SaveVerbatim}{cmds}

102−Idris version 0.9.7

101+\begin{SaveVerbatim}[commandchars=\\\{\}]{cmds}

102+Idris version \version{}

103103-------------------

104104

105105 Command Arguments Purpose

@@ -129,12 +129,12 @@ Idris version 0.9.7

129129\codefigs{cmds}{Interactive environment commands}

130130

131131

132−\begin{SaveVerbatim}{run1}

132+\begin{SaveVerbatim}[commandchars=^\{\}]{run1}

133133

134134$ idris hello.idr

135135 ____ __ _

136136 / _/___/ /____(_)____

137− / // __ / ___/ / ___/ Version 0.9.7

137+ / // __ / ___/ / ___/ Version ^version{}

138138 _/ // /_/ / / / (__ ) http://www.idris-lang.org/

139139 /___/\__,_/_/ /_/____/ Type :? for help

140140