git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/betteroperatormessage

Conflicts: test/reg050/expected

commit769bae3cb4e803fc5723316dda86460f8717d3b2 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateSun 1 Mar 2015, 20:54 (12 years ago) parentef906d341711c7
15 files changed+155−73
compare with master
unifiedsplit
.travis.yml+6 CITATION.md+29 contribs/lib/SQLite3/Makefile+2−3 contribs/lib/SQLite3/Sqlite3.idr+42−48 rts/Makefile+1−1 rts/windows/idris_stdfgn.c+10−3 rts/windows/win_utils.c+21 src/Idris/AbsSyntax.hs+4 src/Idris/CmdOptions.hs+1−1 src/Idris/Elab/Data.hs+4−2 src/Idris/ParseHelpers.hs+8−10 src/Idris/Parser.hs+16 src/Idris/REPL.hs+4−2 src/Pkg/PParser.hs+2−2 src/Util/System.hs+5−1
.travis.yml+6
@@ -1,4 +1,10 @@
11language: 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+
28before_install:
39 - sudo add-apt-repository --yes ppa:h-rayflood/llvm
410 - 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
77 idris testunit.idr -o sqltest
88
99sqlite3api.o : sqlite3api.c
10− gcc -c sqlite3api.c
10+ gcc -I . -c sqlite3api.c
1111
1212sqlite3api.so: sqlite3api.c
13− gcc -fPIC -o sqlite3api.so -shared sqlite3api.c
13+ gcc -I . -fPIC -o sqlite3api.so -shared sqlite3api.c
1414
1515all : sqltest sqlite3api.o
16−
contribs/lib/SQLite3/Sqlite3.idr+42−48
@@ -1,8 +1,9 @@
11module Sqlite3
2−import Sqlexpr
3−
2+import public Sqlexpr
43
54%lib C "sqlite3"
5+-- %link C "sqlite3.o"
6+-- %include C "sqlite3.h"
67%link C "sqlite3api.o"
78%include C "sqlite3api.h"
89
@@ -59,7 +60,7 @@ instance Monad DB where
5960 Left err => return (Left err)
6061 Right v => case k v of
6162 MkDB k' => k')
62− return x = MkDB (return (Right x))
63+ --return x = MkDB (return (Right x))
6364
6465fail : String -> DB a
6566fail err = MkDB (return (Left err))
@@ -83,7 +84,7 @@ runDB (MkDB f) = do f' <- f
8384-----------------------------------------------------------------------------
8485
8586open_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)
8788 return (MkDBPointer x)
8889
8990-----------------------------------------------------------------------------
@@ -91,7 +92,7 @@ open_db name = do x <- liftIO (mkForeign (FFun "sqlite3_open_idr" [FString] FPtr
9192-----------------------------------------------------------------------------
9293
9394close_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)
9596
9697-----------------------------------------------------------------------------
9798-- | Wrapper around prepare, step and finalize.
@@ -99,7 +100,7 @@ close_db (MkDBPointer pointer) = liftIO (mkForeign (FFun "sqlite3_close_idr" [FP
99100
100101exec_db : DBPointer -> String -> DB Int
101102exec_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)
103104 if (x == 1)
104105 then fail "Could not execute."
105106 else return x
@@ -110,7 +111,7 @@ exec_db (MkDBPointer pointer) stmt = do
110111
111112exec_db_v2 : StmtPtr -> DB Int
112113exec_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)
114115 if (x == 21)
115116 then fail "No data returned."
116117 else return x
@@ -122,8 +123,7 @@ exec_db_v2 (MkStmtPtr pointer) = do
122123-----------------------------------------------------------------------------
123124
124125get_error : DBPointer -> IO String
125−get_error (MkDBPointer pointer) = mkForeign (FFun "sqlite3_get_error" [FPtr] FString) pointer
126−
126+get_error (MkDBPointer pointer) = foreign FFI_C "sqlite3_get_error" (Ptr -> IO String) pointer
127127
128128-----------------------------------------------------------------------------
129129-- | 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
133133
134134prepare_db : DBPointer -> String -> DB StmtPtr
135135prepare_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)
137137 flag <- liftIO (nullPtr result)
138138 if flag
139139 then fail "Error occured while preparing"
@@ -147,8 +147,8 @@ prepare_db (MkDBPointer pointer) cmd = do
147147
148148step_db : StmtPtr -> DB Int
149149step_db (MkStmtPtr pointer)= do
150− x <- liftIO (mkForeign (FFun "sqlite3_step_idr" [FPtr] FInt)pointer)
151− if ( x == 101)
150+ x <- liftIO (foreign FFI_C "sqlite3_step_idr" (Ptr -> IO Int) pointer)
151+ if (x == 101)
152152 then fail "SQLITE_DONE"
153153 else return x
154154
@@ -159,7 +159,7 @@ step_db (MkStmtPtr pointer)= do
159159
160160finalize_db : StmtPtr -> DB Int
161161finalize_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)
163163 if (x /= 0)
164164 then fail "Could not finalize"
165165 else return x
@@ -170,7 +170,7 @@ finalize_db (MkStmtPtr pointer) = do
170170
171171reset_db : StmtPtr -> DB Int
172172reset_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)
174174 if (x /= 0)
175175 then fail "Could not reset"
176176 else return x
@@ -181,38 +181,34 @@ reset_db (MkStmtPtr pointer) = do
181181
182182column_count : DBPointer -> IO (Either String Int)
183183column_count (MkDBPointer pointer) = do
184− x <- mkForeign (FFun "sqlite3_column_count_idr" [FPtr] FInt) pointer
185− return $ if (x == 0 )
184+ x <- foreign FFI_C "sqlite3_column_count_idr" (Ptr -> IO Int) pointer
185+ return $ if (x == 0)
186186 then Left "No Data"
187187 else (Right x)
188188
189189column_name : DBPointer -> Int -> IO String
190190column_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
192192
193193column_decltype : DBPointer -> Int -> IO String
194194column_decltype (MkDBPointer pointer) iCol =
195− mkForeign (FFun "sqlite3_column_decltype_idr" [FPtr, FInt] FString) pointer iCol
196−
195+ foreign FFI_C "sqlite3_column_decltype_idr" (Ptr -> Int -> IO String) pointer iCol
197196
198197column_bytes : DBPointer -> Int -> IO Int
199198column_bytes (MkDBPointer pointer) iCol =
200− mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FInt) pointer iCol
201−
199+ foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO Int) pointer iCol
202200
203201column_blob : DBPointer -> Int -> IO String
204202column_blob (MkDBPointer pointer) iCol =
205− mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FString) pointer iCol
206−
203+ foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO String) pointer iCol
207204
208205column_text : DBPointer -> Int -> IO String
209206column_text (MkDBPointer pointer) iCol =
210− mkForeign (FFun "sqlite3_column_text_idr" [FPtr, FInt] FString) pointer iCol
211−
207+ foreign FFI_C "sqlite3_column_text_idr" (Ptr -> Int -> IO String) pointer iCol
212208
213209column_Int : DBPointer -> Int -> IO Int
214210column_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
216212
217213-----------------------------------------------------------------------------
218214-- | These routines support some of SQLite backup functions.
@@ -220,22 +216,21 @@ column_Int (MkDBPointer pointer) iCol =
220216
221217backup_init : DBPointer -> String -> DBPointer -> String -> IO DBPointer
222218backup_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)
224220 des_pointer destName src_pointer srcName
225221 return (MkDBPointer x)
226222
227223backup_step : DBPointer -> Int -> IO Int
228224backup_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
230226
231227backup_finish : DBPointer -> IO Int
232228backup_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
234230
235231backup_remaining : DBPointer -> IO Int
236232backup_remaining (MkDBPointer pointer) =
237− mkForeign (FFun "sqlite3_backup_remaining_idr" [FPtr] FInt) pointer
238−
233+ foreign FFI_C "sqlite3_backup_remaining_idr" (Ptr -> IO Int) pointer
239234
240235-----------------------------------------------------------------------------
241236-- | Use of this interface is not recommended.
@@ -246,19 +241,18 @@ backup_remaining (MkDBPointer pointer) =
246241
247242get_table : DBPointer -> String -> DB TBPointer
248243get_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)
250245 flag <- liftIO (nullPtr x)
251246 if flag
252247 then do x <- liftIO(get_error_table pointer) ; fail x
253248 else return (MkTBPointer x)
254249 where
255250 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
257252 return x
258253
259−
260254free_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
262256 return ()
263257
264258-----------------------------------------------------------------------------
@@ -267,11 +261,11 @@ free_table (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_free_table_i
267261-----------------------------------------------------------------------------
268262
269263num_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
271265 return x
272266
273267num_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
275269 return x
276270
277271-----------------------------------------------------------------------------
@@ -280,11 +274,11 @@ num_col (MkTBPointer pointer) = do x <- mkForeign (FFun "sqlite3_get_num_col" [F
280274-----------------------------------------------------------------------------
281275
282276num_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
284278 return x
285279
286280num_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
288282 return x
289283
290284-----------------------------------------------------------------------------
@@ -299,18 +293,18 @@ get_data (MkDBPointer pointer) row col = do
299293 helper ty
300294 where get_data_type : Ptr ->Int -> Int -> IO Int
301295 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
303297 get_data_val_int : Ptr -> Int -> IO Int
304298 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
306300
307301 get_data_val_text : Ptr -> Int -> IO String
308302 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
310304
311305 get_data_val_float : Ptr -> Int -> IO Float
312306 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
314308
315309 helper : Int -> IO DBVal
316310 helper 1 = do i <- get_data_val_int pointer col ; return (DBInt i)
@@ -360,7 +354,7 @@ strcat str1 str2 = str1 ++ str2
360354
361355bind_int : StmtPtr -> Int -> Int -> DB StmtPtr
362356bind_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)
364358 flag <- liftIO (nullPtr x)
365359 if flag
366360 then fail "Could not bind int."
@@ -369,7 +363,7 @@ bind_int (MkStmtPtr pointer) indexval val = do
369363
370364bind_float : StmtPtr -> Int -> Float -> DB StmtPtr
371365bind_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)
373367 flag <- liftIO (nullPtr x)
374368 if flag
375369 then fail "Could not bind float."
@@ -377,7 +371,7 @@ bind_float (MkStmtPtr pointer) indexval val = do
377371
378372bind_text : StmtPtr -> String -> Int -> Int -> DB StmtPtr
379373bind_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)
381375 pointer text indexval lengthval)
382376 flag <- liftIO(nullPtr x)
383377 if flag
@@ -386,7 +380,7 @@ bind_text (MkStmtPtr pointer) text indexval lengthval = do
386380
387381bind_null : StmtPtr -> Int -> DB StmtPtr
388382bind_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)
390384 flag <- liftIO (nullPtr x)
391385 if flag
392386 then fail "Could not bind null."
@@ -397,7 +391,7 @@ bind_null (MkStmtPtr pointer) indexval = do
397391-----------------------------------------------------------------------------
398392
399393strlen : 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)
401395
402396instance Show DBVal where
403397 show (DBInt i) = "Int val: " ++ show i ++ "\n"
rts/Makefile+1−1
@@ -18,7 +18,7 @@ endif
1818endif
1919
2020ifeq ($(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
2222else
2323 OBJS += idris_stdfgn.o idris_net.o
2424endif
rts/windows/idris_stdfgn.c+10−3
@@ -5,9 +5,12 @@
55#include <fcntl.h>
66#include <stdio.h>
77#include <time.h>
8+#include <io.h>
89
910extern char** environ;
1011
12+int win_fpoll(void* h);
13+
1114void putStr(char* str) {
1215 printf("%s", str);
1316}
@@ -32,14 +35,18 @@ int fileError(void* h) {
3235 return ferror(f);
3336}
3437
35−void fputStr(void* h, char* str) {
38+int idris_writeStr(void* h, char* str) {
3639 FILE* f = (FILE*)h;
37− fputs(str, f);
40+ if (fputs(str, f)) {
41+ return 0;
42+ } else {
43+ return -1;
44+ }
3845}
3946
4047int fpoll(void* h)
4148{
42− return 0;
49+ return win_fpoll(h);
4350}
4451
4552void* 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
17141714 return (a' : as')
17151715 slAlts ns [] = return []
17161716 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')
17171721 sl (PApp fc fn args) = do -- Just the args, fn isn't matchable as a var
17181722 args' <- mapM slA args
17191723 return $ PApp fc fn args'
src/Idris/CmdOptions.hs+1−1
@@ -26,7 +26,7 @@ runArgParser = do opts <- execParser $ info parser
2626 idrisProgDesc = PP.vsep [PP.empty,
2727 PP.text "Idris is a general purpose pure functional programming language with dependent",
2828 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.",
3030 PP.text "It is compiled, with eager evaluation. Its features are influenced by Haskell",
3131 PP.text "and ML.",
3232 PP.empty,
src/Idris/Elab/Data.hs+4−2
@@ -316,11 +316,13 @@ elabCaseFun ind paramPos n ty cons info = do
316316 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
317317 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
318318 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)
320321 -- Do not elaborate clauses if there aren't any
321322 case eliminatorClauses of
322323 [] -> 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)
324326 where elimLog :: String -> EliminatorState ()
325327 elimLog s = State.lift (logLvl 2 s)
326328
src/Idris/ParseHelpers.hs+8−10
@@ -105,30 +105,28 @@ isEol :: Char -> Bool
105105isEol '\n' = True
106106isEol _ = False
107107
108+-- | A parser that succeeds at the end of the line
108109eol :: MonadicParsing m => m ()
109110eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"
110111
111112{- | Consumes a single-line comment
112113
113114@
114− SingleLineComment_t ::= '--' EOL_t
115− | '--' ~DocCommentMarker_t ~EOL_t* EOL_t
116− ;
115+ SingleLineComment_t ::= '--' ~EOL_t* EOL_t ;
117116@
118117 -}
119118singleLineComment :: MonadicParsing m => m ()
120−singleLineComment = try (string "--" *> eol *> pure ())
121− <|> try (string "--" *> many simpleWhiteSpace *>
122− many (satisfy (not . isEol)) *>
123− eol *> pure ())
124− <?> ""
119+singleLineComment = (string "--" *>
120+ many (satisfy (not . isEol)) *>
121+ eol *> pure ())
122+ <?> "single-line comment"
125123
126124{- | Consumes a multi-line comment
127125
128126@
129127 MultiLineComment_t ::=
130128 '{ -- }'
131− | '{ -' ~DocCommentMarker_t InCommentChars_t
129+ | '{ -' InCommentChars_t
132130 ;
133131@
134132
@@ -154,7 +152,7 @@ multiLineComment = try (string "{-" *> (string "-}") *> pure ())
154152 startEnd :: String
155153 startEnd = "{}-"
156154
157−{-| Parses a documentation comment (similar to haddock) given a marker character
155+{-| Parses a documentation comment
158156
159157@
160158 DocComment_t ::= '|||' ~EOL_t* EOL_t
src/Idris/Parser.hs+16
@@ -1315,8 +1315,24 @@ loadSource lidr f toline
13151315 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
13161316 let syntax = defaultSyntax{ syn_namespace = reverse mname,
13171317 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
13181322 ds' <- parseProg syntax f file pos
13191323
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+
13201336 -- Parsing done, now process declarations
13211337
13221338 let ds = namespaces mname ds'
src/Idris/REPL.hs+4−2
@@ -821,7 +821,7 @@ process fn (Undefine names) = undefine names
821821 -- Keep track of which names you've removed so you can
822822 -- print them out to the user afterward
823823 undefine names = undefine' names []
824− undefine' [] list = do iRenderOutput $ printUndefinedNames list
824+ undefine' [] list = do iRenderResult $ printUndefinedNames list
825825 return ()
826826 undefine' (n:names) already = do
827827 allDefined <- idris_repl_defs `fmap` get
@@ -1104,10 +1104,12 @@ process fn Execute
11041104 (tmpn, tmph) <- runIO tempfile
11051105 runIO $ hClose tmph
11061106 t <- codegen
1107+ -- gcc adds .exe when it builds windows programs
1108+ progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn
11071109 ir <- compile t tmpn m
11081110 runIO $ generate t (fst (head (idris_imported ist))) ir
11091111 case idris_outputmode ist of
1110− RawOutput h -> do runIO $ rawSystem tmpn []
1112+ RawOutput h -> do runIO $ rawSystem progName []
11111113 return ()
11121114 IdeMode n h -> runIO . hPutStrLn h $
11131115 IdeMode.convSExp "run-program" tmpn n)
src/Pkg/PParser.hs+2−2
@@ -16,7 +16,7 @@ import Idris.CmdOptions
1616import Control.Monad.State.Strict
1717import Control.Applicative
1818
19−import System.Info (os)
19+import Util.System
2020
2121
2222type PParser = StateT PkgDesc IdrisInnerParser
@@ -63,7 +63,7 @@ pClause :: PParser ()
6363pClause = do reserved "executable"; lchar '=';
6464 exec <- iName []
6565 st <- get
66− put (st { execout = Just (if os `elem` ["win32", "mingw32", "cygwin32"]
66+ put (st { execout = Just (if isWindows
6767 then ((show exec) ++ ".exe")
6868 else ( show exec )
6969 ) })
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
22
33-- System helper functions.
44import Control.Monad (when)
@@ -9,6 +9,7 @@ import System.Directory (getTemporaryDirectory
99 )
1010import System.FilePath ((</>), normalise)
1111import System.IO
12+import System.Info
1213import System.IO.Error
1314import Control.Exception as CE
1415
@@ -18,6 +19,9 @@ catchIO = CE.catch
1819throwIO :: IOError -> IO a
1920throwIO = CE.throw
2021
22+isWindows :: Bool
23+isWindows = os `elem` ["win32", "mingw32", "cygwin32"]
24+
2125tempfile :: IO (FilePath, Handle)
2226tempfile = do dir <- getTemporaryDirectory
2327 openTempFile (normalise dir) "idris"