git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/betteroperatormessage
769bae3Ahmad Salim Al-Sibahi
.travis.yml+6
compare with master
unifiedsplit
@@ -1,4 +1,10 @@
1language: haskell
1language: haskell
2+ghc:
3+ # Idris won't build on 7.4 and earlier due to dependency
4+ # problems. 7.10 isn't yet supported on Travis.
5+ - 7.6
6+ - 7.8
7+
2before_install:
8before_install:
3 - sudo add-apt-repository --yes ppa:h-rayflood/llvm
9 - sudo add-apt-repository --yes ppa:h-rayflood/llvm
4 - sudo apt-get update -qq
10 - sudo apt-get update -qq
CITATION.mdnew file+29
@@ -0,0 +1,29 @@
1+# Citing `Idris`
2+
3+If you use `Idris` in your work we would prefer it if you would use the following reference in your work.
4+
5+## BibTeX
6+
7+```bibtex
8+@article{JFP:9060502,
9+ author = {BRADY,EDWIN},
10+ title = {Idris, a general-purpose dependently typed programming language: Design and implementation},
11+ journal = {Journal of Functional Programming},
12+ volume = {23},
13+ issue = {05},
14+ month = {9},
15+ year = {2013},
16+ issn = {1469-7653},
17+ pages = {552--593},
18+ numpages = {42},
19+ doi = {10.1017/S095679681300018X},
20+ URL = {http://journals.cambridge.org/article_S095679681300018X},
21+}
22+```
23+
24+## Textual
25+
26+ EDWIN BRADY (2013). Idris, a general-purpose dependently typed
27+ programming language: Design and implementation. Journal of
28+ Functional Programming, 23, pp
29+ 552-593. doi:10.1017/S095679681300018X.
contribs/lib/SQLite3/Makefile+2−3
@@ -7,10 +7,9 @@ sqltest : testunit.idr Sqlite3.idr sqlite3api.o
7 idris testunit.idr -o sqltest
7 idris testunit.idr -o sqltest
8
8
9sqlite3api.o : sqlite3api.c
9sqlite3api.o : sqlite3api.c
10− gcc -c sqlite3api.c
10+ gcc -I . -c sqlite3api.c
11
11
12sqlite3api.so: sqlite3api.c
12sqlite3api.so: sqlite3api.c
13− gcc -fPIC -o sqlite3api.so -shared sqlite3api.c
13+ gcc -I . -fPIC -o sqlite3api.so -shared sqlite3api.c
14
14
15all : sqltest sqlite3api.o
15all : sqltest sqlite3api.o
16−
contribs/lib/SQLite3/Sqlite3.idr+42−48
@@ -1,8 +1,9 @@
1module Sqlite3
1module Sqlite3
2−import Sqlexpr
2+import public Sqlexpr
3−
4
3
5%lib C "sqlite3"
4%lib C "sqlite3"
5+-- %link C "sqlite3.o"
6+-- %include C "sqlite3.h"
6%link C "sqlite3api.o"
7%link C "sqlite3api.o"
7%include C "sqlite3api.h"
8%include C "sqlite3api.h"
8
9
@@ -59,7 +60,7 @@ instance Monad DB where
59 Left err => return (Left err)
60 Left err => return (Left err)
60 Right v => case k v of
61 Right v => case k v of
61 MkDB k' => k')
62 MkDB k' => k')
62− return x = MkDB (return (Right x))
63+ --return x = MkDB (return (Right x))
63
64
64fail : String -> DB a
65fail : String -> DB a
65fail err = MkDB (return (Left err))
66fail err = MkDB (return (Left err))
@@ -83,7 +84,7 @@ runDB (MkDB f) = do f' <- f
83-----------------------------------------------------------------------------
84-----------------------------------------------------------------------------
84
85
85open_db : String -> DB DBPointer
86open_db : String -> DB DBPointer
86−open_db name = do x <- liftIO (mkForeign (FFun "sqlite3_open_idr" [FString] FPtr) name)
87+open_db name = do x <- liftIO (foreign FFI_C "sqlite3_open_idr" (String -> IO Ptr) name)
87 return (MkDBPointer x)
88 return (MkDBPointer x)
88
89
89-----------------------------------------------------------------------------
90-----------------------------------------------------------------------------
@@ -91,7 +92,7 @@ open_db name = do x <- liftIO (mkForeign (FFun "sqlite3_open_idr" [FString] FPtr
91-----------------------------------------------------------------------------
92-----------------------------------------------------------------------------
92
93
93close_db : DBPointer -> DB Int
94close_db : DBPointer -> DB Int
94−close_db (MkDBPointer pointer) = liftIO (mkForeign (FFun "sqlite3_close_idr" [FPtr] FInt) pointer)
95+close_db (MkDBPointer pointer) = liftIO (foreign FFI_C "sqlite3_close_idr" (Ptr -> IO Int) pointer)
95
96
96-----------------------------------------------------------------------------
97-----------------------------------------------------------------------------
97-- | Wrapper around prepare, step and finalize.
98-- | Wrapper around prepare, step and finalize.
@@ -99,7 +100,7 @@ close_db (MkDBPointer pointer) = liftIO (mkForeign (FFun "sqlite3_close_idr" [FP
99
100
100exec_db : DBPointer -> String -> DB Int
101exec_db : DBPointer -> String -> DB Int
101exec_db (MkDBPointer pointer) stmt = do
102exec_db (MkDBPointer pointer) stmt = do
102− x <- liftIO (mkForeign (FFun "sqlite3_exec_idr" [FPtr, FString] FInt) pointer stmt)
103+ x <- liftIO (foreign FFI_C "sqlite3_exec_idr" (Ptr -> String -> IO Int) pointer stmt)
103 if (x == 1)
104 if (x == 1)
104 then fail "Could not execute."
105 then fail "Could not execute."
105 else return x
106 else return x
@@ -110,7 +111,7 @@ exec_db (MkDBPointer pointer) stmt = do
110
111
111exec_db_v2 : StmtPtr -> DB Int
112exec_db_v2 : StmtPtr -> DB Int
112exec_db_v2 (MkStmtPtr pointer) = do
113exec_db_v2 (MkStmtPtr pointer) = do
113− x <- liftIO (mkForeign (FFun "exec_db" [FPtr] FInt) pointer)
114+ x <- liftIO (foreign FFI_C "exec_db" (Ptr -> IO Int) pointer)
114 if (x == 21)
115 if (x == 21)
115 then fail "No data returned."
116 then fail "No data returned."
116 else return x
117 else return x
@@ -122,8 +123,7 @@ exec_db_v2 (MkStmtPtr pointer) = do
122-----------------------------------------------------------------------------
123-----------------------------------------------------------------------------
123
124
124get_error : DBPointer -> IO String
125get_error : DBPointer -> IO String
125−get_error (MkDBPointer pointer) = mkForeign (FFun "sqlite3_get_error" [FPtr] FString) pointer
126+get_error (MkDBPointer pointer) = foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer
126−
127
127
128-----------------------------------------------------------------------------
128-----------------------------------------------------------------------------
129-- | Compiles the query inot a byte-code program in order to execute it.
129-- | Compiles the query inot a byte-code program in order to execute it.
@@ -133,7 +133,7 @@ get_error (MkDBPointer pointer) = mkForeign (FFun "sqlite3_get_error" [FPtr] FSt
133
133
134prepare_db : DBPointer -> String -> DB StmtPtr
134prepare_db : DBPointer -> String -> DB StmtPtr
135prepare_db (MkDBPointer pointer) cmd = do
135prepare_db (MkDBPointer pointer) cmd = do
136− result <- liftIO (mkForeign (FFun "sqlite3_prepare_idr" [FPtr, FString] FPtr) pointer cmd)
136+ result <- liftIO (foreign FFI_C "sqlite3_prepare_idr" (Ptr -> String -> IO Ptr) pointer cmd)
137 flag <- liftIO (nullPtr result)
137 flag <- liftIO (nullPtr result)
138 if flag
138 if flag
139 then fail "Error occured while preparing"
139 then fail "Error occured while preparing"
@@ -147,8 +147,8 @@ prepare_db (MkDBPointer pointer) cmd = do
147
147
148step_db : StmtPtr -> DB Int
148step_db : StmtPtr -> DB Int
149step_db (MkStmtPtr pointer)= do
149step_db (MkStmtPtr pointer)= do
150− x <- liftIO (mkForeign (FFun "sqlite3_step_idr" [FPtr] FInt)pointer)
150+ x <- liftIO (foreign FFI_C "sqlite3_step_idr" (Ptr -> IO Int) pointer)
151− if ( x == 101)
151+ if (x == 101)
152 then fail "SQLITE_DONE"
152 then fail "SQLITE_DONE"
153 else return x
153 else return x
154
154
@@ -159,7 +159,7 @@ step_db (MkStmtPtr pointer)= do
159
159
160finalize_db : StmtPtr -> DB Int
160finalize_db : StmtPtr -> DB Int
161finalize_db (MkStmtPtr pointer) = do
161finalize_db (MkStmtPtr pointer) = do
162− x <- liftIO (mkForeign (FFun "sqlite3_finalize_idr" [FPtr] FInt) pointer)
162+ x <- liftIO (foreign FFI_C "sqlite3_finalize_idr" (Ptr -> IO Int) pointer)
163 if (x /= 0)
163 if (x /= 0)
164 then fail "Could not finalize"
164 then fail "Could not finalize"
165 else return x
165 else return x
@@ -170,7 +170,7 @@ finalize_db (MkStmtPtr pointer) = do
170
170
171reset_db : StmtPtr -> DB Int
171reset_db : StmtPtr -> DB Int
172reset_db (MkStmtPtr pointer) = do
172reset_db (MkStmtPtr pointer) = do
173− x <- liftIO (mkForeign (FFun "sqlite3_reset_idr" [FPtr] FInt) pointer)
173+ x <- liftIO (foreign FFI_C "sqlite3_reset_idr" (Ptr -> IO Int) pointer)
174 if (x /= 0)
174 if (x /= 0)
175 then fail "Could not reset"
175 then fail "Could not reset"
176 else return x
176 else return x
@@ -181,38 +181,34 @@ reset_db (MkStmtPtr pointer) = do
181
181
182column_count : DBPointer -> IO (Either String Int)
182column_count : DBPointer -> IO (Either String Int)
183column_count (MkDBPointer pointer) = do
183column_count (MkDBPointer pointer) = do
184− x <- mkForeign (FFun "sqlite3_column_count_idr" [FPtr] FInt) pointer
184+ x <- foreign FFI_C "sqlite3_column_count_idr" (Ptr -> IO Int) pointer
185− return $ if (x == 0 )
185+ return $ if (x == 0)
186 then Left "No Data"
186 then Left "No Data"
187 else (Right x)
187 else (Right x)
188
188
189column_name : DBPointer -> Int -> IO String
189column_name : DBPointer -> Int -> IO String
190column_name (MkDBPointer pointer) iCol =
190column_name (MkDBPointer pointer) iCol =
191− mkForeign (FFun "sqlite3_column_name_idr" [FPtr, FInt] FString) pointer iCol
191+ foreign FFI_C "sqlite3_column_name_idr" (Ptr -> Int -> IO String) pointer iCol
192
192
193column_decltype : DBPointer -> Int -> IO String
193column_decltype : DBPointer -> Int -> IO String
194column_decltype (MkDBPointer pointer) iCol =
194column_decltype (MkDBPointer pointer) iCol =
195− mkForeign (FFun "sqlite3_column_decltype_idr" [FPtr, FInt] FString) pointer iCol
195+ foreign FFI_C "sqlite3_column_decltype_idr" (Ptr -> Int -> IO String) pointer iCol
196−
197
196
198column_bytes : DBPointer -> Int -> IO Int
197column_bytes : DBPointer -> Int -> IO Int
199column_bytes (MkDBPointer pointer) iCol =
198column_bytes (MkDBPointer pointer) iCol =
200− mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FInt) pointer iCol
199+ foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO Int) pointer iCol
201−
202
200
203column_blob : DBPointer -> Int -> IO String
201column_blob : DBPointer -> Int -> IO String
204column_blob (MkDBPointer pointer) iCol =
202column_blob (MkDBPointer pointer) iCol =
205− mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FString) pointer iCol
203+ foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO String) pointer iCol
206−
207
204
208column_text : DBPointer -> Int -> IO String
205column_text : DBPointer -> Int -> IO String
209column_text (MkDBPointer pointer) iCol =
206column_text (MkDBPointer pointer) iCol =
210− mkForeign (FFun "sqlite3_column_text_idr" [FPtr, FInt] FString) pointer iCol
207+ foreign FFI_C "sqlite3_column_text_idr" (Ptr -> Int -> IO String) pointer iCol
211−
212
208
213column_Int : DBPointer -> Int -> IO Int
209column_Int : DBPointer -> Int -> IO Int
214column_Int (MkDBPointer pointer) iCol =
210column_Int (MkDBPointer pointer) iCol =
215− mkForeign (FFun "sqlite3_column_int_idr" [FPtr, FInt] FInt) pointer iCol
211+ foreign FFI_C "sqlite3_column_int_idr" (Ptr -> Int -> IO Int) pointer iCol
216
212
217-----------------------------------------------------------------------------
213-----------------------------------------------------------------------------
218-- | These routines support some of SQLite backup functions.
214-- | These routines support some of SQLite backup functions.
@@ -220,22 +216,21 @@ column_Int (MkDBPointer pointer) iCol =
220
216
221backup_init : DBPointer -> String -> DBPointer -> String -> IO DBPointer
217backup_init : DBPointer -> String -> DBPointer -> String -> IO DBPointer
222backup_init (MkDBPointer des_pointer) destName (MkDBPointer src_pointer) srcName =
218backup_init (MkDBPointer des_pointer) destName (MkDBPointer src_pointer) srcName =
223− do x <- mkForeign (FFun "sqlite3_backup_init_idr" [FPtr,FString, FPtr, FString] FPtr)
219+ do x <- foreign FFI_C "sqlite3_backup_init_idr" (Ptr -> String -> Ptr -> String -> IO Ptr)
224 des_pointer destName src_pointer srcName
220 des_pointer destName src_pointer srcName
225 return (MkDBPointer x)
221 return (MkDBPointer x)
226
222
227backup_step : DBPointer -> Int -> IO Int
223backup_step : DBPointer -> Int -> IO Int
228backup_step (MkDBPointer pointer) nPage =
224backup_step (MkDBPointer pointer) nPage =
229− mkForeign (FFun "sqlite3_backup_step_idr" [FPtr, FInt] FInt) pointer nPage
225+ foreign FFI_C "sqlite3_backup_step_idr" (Ptr -> Int -> IO Int) pointer nPage
230
226
231backup_finish : DBPointer -> IO Int
227backup_finish : DBPointer -> IO Int
232backup_finish (MkDBPointer pointer) =
228backup_finish (MkDBPointer pointer) =
233− mkForeign (FFun "sqlite3_backup_finish_idr" [FPtr] FInt) pointer
229+ foreign FFI_C "sqlite3_backup_finish_idr" (Ptr -> IO Int) pointer
234
230
235backup_remaining : DBPointer -> IO Int
231backup_remaining : DBPointer -> IO Int
236backup_remaining (MkDBPointer pointer) =
232backup_remaining (MkDBPointer pointer) =
237− mkForeign (FFun "sqlite3_backup_remaining_idr" [FPtr] FInt) pointer
233+ foreign FFI_C "sqlite3_backup_remaining_idr" (Ptr -> IO Int) pointer
238−
239
234
240-----------------------------------------------------------------------------
235-----------------------------------------------------------------------------
241-- | Use of this interface is not recommended.
236-- | Use of this interface is not recommended.
@@ -246,19 +241,18 @@ backup_remaining (MkDBPointer pointer) =
246
241
247get_table : DBPointer -> String -> DB TBPointer
242get_table : DBPointer -> String -> DB TBPointer
248get_table (MkDBPointer pointer) name = do
243get_table (MkDBPointer pointer) name = do
249− x <- liftIO(mkForeign (FFun "sqlite3_get_table_idr" [FPtr, FString] FPtr) pointer name)
244+ x <- liftIO(foreign FFI_C "sqlite3_get_table_idr" (Ptr -> String -> IO Ptr) pointer name)
250 flag <- liftIO (nullPtr x)
245 flag <- liftIO (nullPtr x)
251 if flag
246 if flag
252 then do x <- liftIO(get_error_table pointer) ; fail x
247 then do x <- liftIO(get_error_table pointer) ; fail x
253 else return (MkTBPointer x)
248 else return (MkTBPointer x)
254 where
249 where
255 get_error_table : Ptr-> IO String
250 get_error_table : Ptr-> IO String
256− get_error_table pointer = do x <- mkForeign (FFun "sqlite3_get_error" [FPtr] FString) pointer
251+ get_error_table pointer = do x <- foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer
257 return x
252 return x
258
253
259−
260free_table : TBPointer -> IO ()
254free_table : TBPointer -> IO ()
261−free_table (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_free_table_idr" [FPtr] FUnit) pointer
255+free_table (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_free_table_idr" (Ptr -> IO ()) pointer
262 return ()
256 return ()
263
257
264-----------------------------------------------------------------------------
258-----------------------------------------------------------------------------
@@ -267,11 +261,11 @@ free_table (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_free_table_i
267-----------------------------------------------------------------------------
261-----------------------------------------------------------------------------
268
262
269num_row : TBPointer -> IO Int
263num_row : TBPointer -> IO Int
270−num_row (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_row" [FPtr] FInt) pointer
264+num_row (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_row" (Ptr -> IO Int) pointer
271 return x
265 return x
272
266
273num_col : TBPointer -> IO Int
267num_col : TBPointer -> IO Int
274−num_col (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col" [FPtr] FInt) pointer
268+num_col (MkTBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_col" (Ptr -> IO Int) pointer
275 return x
269 return x
276
270
277-----------------------------------------------------------------------------
271-----------------------------------------------------------------------------
@@ -280,11 +274,11 @@ num_col (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col" [F
280-----------------------------------------------------------------------------
274-----------------------------------------------------------------------------
281
275
282num_row_v2 : DBPointer -> IO Int
276num_row_v2 : DBPointer -> IO Int
283−num_row_v2 (MkDBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_row_v2" [FPtr] FInt) pointer
277+num_row_v2 (MkDBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_row_v2" (Ptr -> IO Int) pointer
284 return x
278 return x
285
279
286num_col_v2 : DBPointer -> IO Int
280num_col_v2 : DBPointer -> IO Int
287−num_col_v2 (MkDBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col_v2" [FPtr] FInt) pointer
281+num_col_v2 (MkDBPointer pointer) = do x <- foreign FFI_C "sqlite3_get_num_col_v2" (Ptr -> IO Int) pointer
288 return x
282 return x
289
283
290-----------------------------------------------------------------------------
284-----------------------------------------------------------------------------
@@ -299,18 +293,18 @@ get_data (MkDBPointer pointer) row col = do
299 helper ty
293 helper ty
300 where get_data_type : Ptr ->Int -> Int -> IO Int
294 where get_data_type : Ptr ->Int -> Int -> IO Int
301 get_data_type pointer row col =
295 get_data_type pointer row col =
302− mkForeign (FFun "sqlite3_get_data_type" [FPtr, FInt, FInt] FInt) pointer row col
296+ foreign FFI_C "sqlite3_get_data_type" (Ptr -> Int -> Int -> IO Int) pointer row col
303 get_data_val_int : Ptr -> Int -> IO Int
297 get_data_val_int : Ptr -> Int -> IO Int
304 get_data_val_int pointer col =
298 get_data_val_int pointer col =
305− mkForeign (FFun "sqlite3_get_val_int" [FPtr,FInt] FInt) pointer col
299+ foreign FFI_C "sqlite3_get_val_int" (Ptr -> Int -> IO Int) pointer col
306
300
307 get_data_val_text : Ptr -> Int -> IO String
301 get_data_val_text : Ptr -> Int -> IO String
308 get_data_val_text pointer col =
302 get_data_val_text pointer col =
309− mkForeign (FFun "sqlite3_get_val_text" [FPtr, FInt] FString) pointer col
303+ foreign FFI_C "sqlite3_get_val_text" (Ptr -> Int -> IO String) pointer col
310
304
311 get_data_val_float : Ptr -> Int -> IO Float
305 get_data_val_float : Ptr -> Int -> IO Float
312 get_data_val_float pointer col =
306 get_data_val_float pointer col =
313− mkForeign (FFun "sqlite3_get_float" [FPtr, FInt] FFloat) pointer col
307+ foreign FFI_C "sqlite3_get_float" (Ptr -> Int -> IO Float) pointer col
314
308
315 helper : Int -> IO DBVal
309 helper : Int -> IO DBVal
316 helper 1 = do i <- get_data_val_int pointer col ; return (DBInt i)
310 helper 1 = do i <- get_data_val_int pointer col ; return (DBInt i)
@@ -360,7 +354,7 @@ strcat str1 str2 = str1 ++ str2
360
354
361bind_int : StmtPtr -> Int -> Int -> DB StmtPtr
355bind_int : StmtPtr -> Int -> Int -> DB StmtPtr
362bind_int (MkStmtPtr pointer) indexval val = do
356bind_int (MkStmtPtr pointer) indexval val = do
363− x <- liftIO (mkForeign (FFun "sqlite3_bind_int_idr" [FPtr, FInt, FInt] FPtr) pointer indexval val)
357+ x <- liftIO (foreign FFI_C "sqlite3_bind_int_idr" (Ptr -> Int -> Int -> IO Ptr) pointer indexval val)
364 flag <- liftIO (nullPtr x)
358 flag <- liftIO (nullPtr x)
365 if flag
359 if flag
366 then fail "Could not bind int."
360 then fail "Could not bind int."
@@ -369,7 +363,7 @@ bind_int (MkStmtPtr pointer) indexval val = do
369
363
370bind_float : StmtPtr -> Int -> Float -> DB StmtPtr
364bind_float : StmtPtr -> Int -> Float -> DB StmtPtr
371bind_float (MkStmtPtr pointer) indexval val = do
365bind_float (MkStmtPtr pointer) indexval val = do
372− x <- liftIO (mkForeign (FFun "sqlite3_bind_float_idr" [FPtr, FInt, FFloat] FPtr) pointer indexval val)
366+ x <- liftIO (foreign FFI_C "sqlite3_bind_float_idr" (Ptr -> Int -> Float -> IO Ptr) pointer indexval val)
373 flag <- liftIO (nullPtr x)
367 flag <- liftIO (nullPtr x)
374 if flag
368 if flag
375 then fail "Could not bind float."
369 then fail "Could not bind float."
@@ -377,7 +371,7 @@ bind_float (MkStmtPtr pointer) indexval val = do
377
371
378bind_text : StmtPtr -> String -> Int -> Int -> DB StmtPtr
372bind_text : StmtPtr -> String -> Int -> Int -> DB StmtPtr
379bind_text (MkStmtPtr pointer) text indexval lengthval = do
373bind_text (MkStmtPtr pointer) text indexval lengthval = do
380− x <- liftIO (mkForeign (FFun "sqlite3_bind_text_idr" [FPtr, FString, FInt, FInt] FPtr)
374+ x <- liftIO (foreign FFI_C "sqlite3_bind_text_idr" (Ptr -> String -> Int -> Int -> IO Ptr)
381 pointer text indexval lengthval)
375 pointer text indexval lengthval)
382 flag <- liftIO(nullPtr x)
376 flag <- liftIO(nullPtr x)
383 if flag
377 if flag
@@ -386,7 +380,7 @@ bind_text (MkStmtPtr pointer) text indexval lengthval = do
386
380
387bind_null : StmtPtr -> Int -> DB StmtPtr
381bind_null : StmtPtr -> Int -> DB StmtPtr
388bind_null (MkStmtPtr pointer) indexval = do
382bind_null (MkStmtPtr pointer) indexval = do
389− x <- liftIO (mkForeign (FFun "sqlite3_bind_null_idr" [FPtr, FInt] FPtr) pointer indexval)
383+ x <- liftIO (foreign FFI_C "sqlite3_bind_null_idr" (Ptr -> Int -> IO Ptr) pointer indexval)
390 flag <- liftIO (nullPtr x)
384 flag <- liftIO (nullPtr x)
391 if flag
385 if flag
392 then fail "Could not bind null."
386 then fail "Could not bind null."
@@ -397,7 +391,7 @@ bind_null (MkStmtPtr pointer) indexval = do
397-----------------------------------------------------------------------------
391-----------------------------------------------------------------------------
398
392
399strlen : String -> DB Int
393strlen : String -> DB Int
400−strlen str = liftIO (mkForeign (FFun "strLength" [FString] FInt) str)
394+strlen str = liftIO (foreign FFI_C "strLength" (String -> IO Int) str)
401
395
402instance Show DBVal where
396instance Show DBVal where
403 show (DBInt i) = "Int val: " ++ show i ++ "\n"
397 show (DBInt i) = "Int val: " ++ show i ++ "\n"
rts/Makefile+1−1
@@ -18,7 +18,7 @@ endif
18endif
18endif
19
19
20ifeq ($(OS), windows)
20ifeq ($(OS), windows)
21− OBJS += windows/idris_stdfgn.o windows/idris_net.o
21+ OBJS += windows/idris_stdfgn.o windows/idris_net.o windows/win_utils.o
22else
22else
23 OBJS += idris_stdfgn.o idris_net.o
23 OBJS += idris_stdfgn.o idris_net.o
24endif
24endif
rts/windows/idris_stdfgn.c+10−3
@@ -5,9 +5,12 @@
5#include <fcntl.h>
5#include <fcntl.h>
6#include <stdio.h>
6#include <stdio.h>
7#include <time.h>
7#include <time.h>
8+#include <io.h>
8
9
9extern char** environ;
10extern char** environ;
10
11
12+int win_fpoll(void* h);
13+
11void putStr(char* str) {
14void putStr(char* str) {
12 printf("%s", str);
15 printf("%s", str);
13}
16}
@@ -32,14 +35,18 @@ int fileError(void* h) {
32 return ferror(f);
35 return ferror(f);
33}
36}
34
37
35−void fputStr(void* h, char* str) {
38+int idris_writeStr(void* h, char* str) {
36 FILE* f = (FILE*)h;
39 FILE* f = (FILE*)h;
37− fputs(str, f);
40+ if (fputs(str, f)) {
41+ return 0;
42+ } else {
43+ return -1;
44+ }
38}
45}
39
46
40int fpoll(void* h)
47int fpoll(void* h)
41{
48{
42− return 0;
49+ return win_fpoll(h);
43}
50}
44
51
45void* do_popen(const char* cmd, const char* mode) {
52void* do_popen(const char* cmd, const char* mode) {
rts/windows/win_utils.cnew file+21
@@ -0,0 +1,21 @@
1+#include <windows.h>
2+#include <io.h>
3+#include <stdio.h>
4+
5+// THis file exists to avoid clashes between windows.h and idris_rts.h
6+//
7+
8+int win_fpoll(void* h)
9+{
10+ HANDLE wh =(HANDLE) _get_osfhandle(_fileno((FILE*)h));
11+ if (wh == INVALID_HANDLE_VALUE) {
12+ return -1;
13+ }
14+ DWORD ret = WaitForSingleObject(wh, 1000);
15+ // Imitate the return values of select()
16+ if (ret == WAIT_OBJECT_0)
17+ return 1;
18+ if (ret == WAIT_TIMEOUT)
19+ return 0;
20+ return -1;
21+}
src/Idris/AbsSyntax.hs+4
@@ -1714,6 +1714,10 @@ stripLinear i tm = evalState (sl tm) [] where
1714 return (a' : as')
1714 return (a' : as')
1715 slAlts ns [] = return []
1715 slAlts ns [] = return []
1716 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
1716 sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')
1717+ sl (PDPair fc p l t r) = do l' <- sl l
1718+ t' <- sl t
1719+ r' <- sl r
1720+ return (PDPair fc p l' t' r')
1717 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1721 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
1718 args' <- mapM slA args
1722 args' <- mapM slA args
1719 return $ PApp fc fn args'
1723 return $ PApp fc fn args'
src/Idris/CmdOptions.hs+1−1
@@ -26,7 +26,7 @@ runArgParser = do opts <- execParser $ info parser
26 idrisProgDesc = PP.vsep [PP.empty,
26 idrisProgDesc = PP.vsep [PP.empty,
27 PP.text "Idris is a general purpose pure functional programming language with dependent",
27 PP.text "Idris is a general purpose pure functional programming language with dependent",
28 PP.text "types. Dependent types allow types to be predicated on values, meaning that",
28 PP.text "types. Dependent types allow types to be predicated on values, meaning that",
29− PP.text "some aspects of a program’s behaviour can be specified precisely in the type.",
29+ PP.text "some aspects of a program's behaviour can be specified precisely in the type.",
30 PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",
30 PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",
31 PP.text "and ML.",
31 PP.text "and ML.",
32 PP.empty,
32 PP.empty,
src/Idris/Elab/Data.hs+4−2
@@ -316,11 +316,13 @@ elabCaseFun ind paramPos n ty cons info = do
316 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
316 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
317 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
317 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
318 elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
318 elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
319− State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl) (\err -> return ())
319+ State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)
320+ (ierror . Elaborating "type declaration of " elimDeclName)
320 -- Do not elaborate clauses if there aren't any
321 -- Do not elaborate clauses if there aren't any
321 case eliminatorClauses of
322 case eliminatorClauses of
322 [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
323 [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
323− _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef) (\err -> return ())
324+ _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)
325+ (ierror . Elaborating "clauses of " elimDeclName)
324 where elimLog :: String -> EliminatorState ()
326 where elimLog :: String -> EliminatorState ()
325 elimLog s = State.lift (logLvl 2 s)
327 elimLog s = State.lift (logLvl 2 s)
326
328
src/Idris/ParseHelpers.hs+8−10
@@ -105,30 +105,28 @@ isEol :: Char -> Bool
105isEol '\n' = True
105isEol '\n' = True
106isEol _ = False
106isEol _ = False
107
107
108+-- | A parser that succeeds at the end of the line
108eol :: MonadicParsing m => m ()
109eol :: MonadicParsing m => m ()
109eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"
110eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"
110
111
111{- | Consumes a single-line comment
112{- | Consumes a single-line comment
112
113
113@
114@
114− SingleLineComment_t ::= '--' EOL_t
115+ SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;
115− | '--' ~DocCommentMarker_t ~EOL_t* EOL_t
116− ;
117@
116@
118 -}
117 -}
119singleLineComment :: MonadicParsing m => m ()
118singleLineComment :: MonadicParsing m => m ()
120−singleLineComment = try (string "--" *> eol *> pure ())
119+singleLineComment = (string "--" *>
121− <|> try (string "--" *> many simpleWhiteSpace *>
122− many (satisfy (not . isEol)) *>
120+ many (satisfy (not . isEol)) *>
123− eol *> pure ())
121+ eol *> pure ())
124− <?> ""
122+ <?> "single-line comment"
125
123
126{- | Consumes a multi-line comment
124{- | Consumes a multi-line comment
127
125
128@
126@
129 MultiLineComment_t ::=
127 MultiLineComment_t ::=
130 '{ -- }'
128 '{ -- }'
131− | '{ -' ~DocCommentMarker_t InCommentChars_t
129+ | '{ -' InCommentChars_t
132 ;
130 ;
133@
131@
134
132
@@ -154,7 +152,7 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())
154 startEnd :: String
152 startEnd :: String
155 startEnd = "{}-"
153 startEnd = "{}-"
156
154
157−{-| Parses a documentation comment (similar to haddock) given a marker character
155+{-| Parses a documentation comment
158
156
159@
157@
160 DocComment_t ::= '|||' ~EOL_t* EOL_t
158 DocComment_t ::= '|||' ~EOL_t* EOL_t
src/Idris/Parser.hs+16
@@ -1315,8 +1315,24 @@ loadSource lidr f toline
1315 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1315 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
1316 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1316 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1317 maxline = toline }
1317 maxline = toline }
1318+ ist <- getIState
1319+ -- Save the span from parsing the module header, because
1320+ -- an empty program parse might obliterate it.
1321+ let oldSpan = idris_parsedSpan ist
1318 ds' <- parseProg syntax f file pos
1322 ds' <- parseProg syntax f file pos
1319
1323
1324+ case (ds', oldSpan) of
1325+ ([], Just fc) ->
1326+ -- If no program elements were parsed, we dind't
1327+ -- get a loaded region in the IBC file. That
1328+ -- means we need to add it back.
1329+ do ist <- getIState
1330+ putIState ist { idris_parsedSpan = oldSpan
1331+ , ibc_write = IBCParsedRegion fc :
1332+ ibc_write ist
1333+ }
1334+ _ -> return ()
1335+
1320 -- Parsing done, now process declarations
1336 -- Parsing done, now process declarations
1321
1337
1322 let ds = namespaces mname ds'
1338 let ds = namespaces mname ds'
src/Idris/REPL.hs+4−2
@@ -821,7 +821,7 @@ process fn (Undefine names) = undefine names
821 -- Keep track of which names you've removed so you can
821 -- Keep track of which names you've removed so you can
822 -- print them out to the user afterward
822 -- print them out to the user afterward
823 undefine names = undefine' names []
823 undefine names = undefine' names []
824− undefine' [] list = do iRenderOutput $ printUndefinedNames list
824+ undefine' [] list = do iRenderResult $ printUndefinedNames list
825 return ()
825 return ()
826 undefine' (n:names) already = do
826 undefine' (n:names) already = do
827 allDefined <- idris_repl_defs `fmap` get
827 allDefined <- idris_repl_defs `fmap` get
@@ -1104,10 +1104,12 @@ process fn Execute
1104 (tmpn, tmph) <- runIO tempfile
1104 (tmpn, tmph) <- runIO tempfile
1105 runIO $ hClose tmph
1105 runIO $ hClose tmph
1106 t <- codegen
1106 t <- codegen
1107+ -- gcc adds .exe when it builds windows programs
1108+ progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn
1107 ir <- compile t tmpn m
1109 ir <- compile t tmpn m
1108 runIO $ generate t (fst (head (idris_imported ist))) ir
1110 runIO $ generate t (fst (head (idris_imported ist))) ir
1109 case idris_outputmode ist of
1111 case idris_outputmode ist of
1110− RawOutput h -> do runIO $ rawSystem tmpn []
1112+ RawOutput h -> do runIO $ rawSystem progName []
1111 return ()
1113 return ()
1112 IdeMode n h -> runIO . hPutStrLn h $
1114 IdeMode n h -> runIO . hPutStrLn h $
1113 IdeMode.convSExp "run-program" tmpn n)
1115 IdeMode.convSExp "run-program" tmpn n)
src/Pkg/PParser.hs+2−2
@@ -16,7 +16,7 @@ import Idris.CmdOptions
16import Control.Monad.State.Strict
16import Control.Monad.State.Strict
17import Control.Applicative
17import Control.Applicative
18
18
19−import System.Info (os)
19+import Util.System
20
20
21
21
22type PParser = StateT PkgDesc IdrisInnerParser
22type PParser = StateT PkgDesc IdrisInnerParser
@@ -63,7 +63,7 @@ pClause :: PParser ()
63pClause = do reserved "executable"; lchar '=';
63pClause = do reserved "executable"; lchar '=';
64 exec <- iName []
64 exec <- iName []
65 st <- get
65 st <- get
66− put (st { execout = Just (if os `elem` ["win32", "mingw32", "cygwin32"]
66+ put (st { execout = Just (if isWindows
67 then ((show exec) ++ ".exe")
67 then ((show exec) ++ ".exe")
68 else ( show exec )
68 else ( show exec )
69 ) })
69 ) })
src/Util/System.hs+5−1
@@ -1,4 +1,4 @@
1−module Util.System(tempfile,withTempdir,rmFile,catchIO) where
1+module Util.System(tempfile,withTempdir,rmFile,catchIO, isWindows) where
2
2
3-- System helper functions.
3-- System helper functions.
4import Control.Monad (when)
4import Control.Monad (when)
@@ -9,6 +9,7 @@ import System.Directory (getTemporaryDirectory
9 )
9 )
10import System.FilePath ((</>), normalise)
10import System.FilePath ((</>), normalise)
11import System.IO
11import System.IO
12+import System.Info
12import System.IO.Error
13import System.IO.Error
13import Control.Exception as CE
14import Control.Exception as CE
14
15
@@ -18,6 +19,9 @@ catchIO = CE.catch
18throwIO :: IOError -> IO a
19throwIO :: IOError -> IO a
19throwIO = CE.throw
20throwIO = CE.throw
20
21
22+isWindows :: Bool
23+isWindows = os `elem` ["win32", "mingw32", "cygwin32"]
24+
21tempfile :: IO (FilePath, Handle)
25tempfile :: IO (FilePath, Handle)
22tempfile = do dir <- getTemporaryDirectory
26tempfile = do dir <- getTemporaryDirectory
23 openTempFile (normalise dir) "idris"
27 openTempFile (normalise dir) "idris"