git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' into wip/tactical
commit20e602829a90e0bffc5e58e490c6bf174274b221 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 2 Mar 2015, 14:02 (12 years ago) parentcbbdb3e8ab9f72
59 files changed+391−240
compare with master
unifiedsplit
.travis.yml+6 CHANGELOG+12−1 CITATION.md+29 contribs/lib/SQLite3/Makefile+2−3 contribs/lib/SQLite3/Sqlite3.idr+43−49 contribs/lib/SimpleParser/SimpleParser.idr+1−1 libs/base/Control/Arrow.idr+1−1 libs/base/Control/IOExcept.idr+2−2 libs/base/Control/Monad/Identity.idr+1−1 libs/base/Control/Monad/RWS.idr+1−1 libs/base/Control/Monad/Reader.idr+1−1 libs/base/Control/Monad/State.idr+1−1 libs/base/Control/Monad/Writer.idr+1−1 libs/base/Data/Erased.idr+1−1 libs/base/Data/Matrix.idr+29−29 libs/base/Data/Morphisms.idr+1−1 libs/base/Data/VectType.idr+1−1 libs/base/Network/Cgi.idr+1−1 libs/base/Providers.idr+3−3 libs/base/System/Concurrency/Process.idr+1−1 libs/effects/Effect/Memory.idr+12−12 libs/effects/Effect/Monad.idr+1−1 libs/effects/Effects.idr+3−3 libs/oldeffects/Effect/Monad.idr+1−1 libs/oldeffects/Effects.idr+3−3 libs/prelude/Language/Reflection/Tactical.idr+1−1 libs/prelude/Prelude.idr+8−8 libs/prelude/Prelude/Algebra.idr+37−37 libs/prelude/Prelude/Applicative.idr+17−17 libs/prelude/Prelude/Functor.idr+8 libs/prelude/Prelude/Monad.idr+1−1 libs/prelude/Prelude/Stream.idr+1−1 libs/prelude/Prelude/Traversable.idr+2−2 rts/Makefile+1−1 rts/windows/idris_stdfgn.c+10−3 rts/windows/win_utils.c+21 samples/interp.idr+2−2 src/Idris/AbsSyntax.hs+8−1 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/CmdOptions.hs+1−1 src/Idris/DSL.hs+28−6 src/Idris/Elab/Clause.hs+3−3 src/Idris/Elab/Data.hs+4−2 src/Idris/ElabTerm.hs+9−1 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 test/dsl001/test001.idr+4−1 test/dsl002/Resimp.idr+6−1 test/dsl003/DSLPi.idr+8−2 test/reg027/reg027.idr+1−1 test/reg050/expected+8−7 test/reg053/four.idr+1−1 test/sourceLocation001/SourceLoc.idr+3−1 test/sourceLocation001/expected+2−2 test/sugar001/test007.idr+1−1 test/tutorial003/tutorial003.idr+1−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
CHANGELOG+12−1
@@ -8,7 +8,18 @@ New in 0.9.17:
88* Quasiquotation supports the generation of Language.Reflection.Raw terms
99 in addition to Language.Reflection.TT. Types are used for disambiguation,
1010 defaulting to TT at the REPL.
11−
11+* Library operators have been renamed for consistency with Haskell. In
12+ particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is
13+ now an alias for Functor.map. Correspondingly, ($>) and (<$) have
14+ been renamed to (<*) and (*>). The cascading effects of this rename
15+ are that Algebra.(<*>) has been renamed to Algebra.(<.>) and
16+ Matrix.(<.>) is now Matrix.(<:>).
17+* Binding forms in DSL notation are now given an extra argument: a
18+ reflected representation of the name that the user chose.
19+ Specifically, the rewritten lambda, pi, and let binders will now get
20+ an extra argument of type TTName. This allows more understandable
21+ dynamic errors in DSL code and more readable code generation results.
22+
1223New in 0.9.16:
1324--------------
1425* Inductive-inductive definitions are now supported (i.e. simultaneously
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+43−49
@@ -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
@@ -47,7 +48,7 @@ instance Functor DB where
4748
4849instance Applicative DB where
4950 pure = MkDB . return . Right
50− (MkDB f) <$> (MkDB x) = MkDB (do f' <- f
51+ (MkDB f) <*> (MkDB x) = MkDB (do f' <- f
5152 case f' of
5253 Left err => return (Left err)
5354 Right op => x >>= (return . map op))
@@ -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"
contribs/lib/SimpleParser/SimpleParser.idr+1−1
@@ -30,7 +30,7 @@ instance Functor Parser where
3030
3131instance Applicative Parser where
3232 pure v = P (\inp => Right (v, inp))
33− a <$> b = P (\inp => do (f, rest) <- parse a inp
33+ a <*> b = P (\inp => do (f, rest) <- parse a inp
3434 (x, rest') <- parse b rest
3535 pure ((f x), rest'))
3636
libs/base/Control/Arrow.idr+1−1
@@ -95,7 +95,7 @@ instance Arrow a => Functor (ArrowMonad a) where
9595
9696instance Arrow a => Applicative (ArrowMonad a) where
9797 pure x = MkArrowMonad $ arrow $ \_ => x
98− (MkArrowMonad f) <$> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
98+ (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
9999
100100instance ArrowApply a => Monad (ArrowMonad a) where
101101 (MkArrowMonad m) >>= f =
libs/base/Control/IOExcept.idr+2−2
@@ -10,8 +10,8 @@ instance Functor (IOExcept e) where
1010
1111instance Applicative (IOExcept e) where
1212 pure x = ioM (pure (pure x))
13− (ioM f) <$> (ioM a) = ioM (do f' <- f; a' <- a
14− return (f' <$> a'))
13+ (ioM f) <*> (ioM a) = ioM (do f' <- f; a' <- a
14+ return (f' <*> a'))
1515
1616instance Monad (IOExcept e) where
1717 (ioM x) >>= k = ioM (do x' <- x;
libs/base/Control/Monad/Identity.idr+1−1
@@ -9,7 +9,7 @@ instance Functor Identity where
99instance Applicative Identity where
1010 pure x = Id x
1111
12− (Id f) <$> (Id g) = Id (f g)
12+ (Id f) <*> (Id g) = Id (f g)
1313
1414instance Monad Identity where
1515 (Id x) >>= k = k x
libs/base/Control/Monad/RWS.idr+1−1
@@ -21,7 +21,7 @@ instance Monad m => Functor (RWST r w s m) where
2121
2222instance (Monoid w, Monad m) => Applicative (RWST r w s m) where
2323 pure a = MkRWST $ \_,s => return (a, s, neutral)
24− (MkRWST f) <$> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s
24+ (MkRWST f) <*> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s
2525 (fn, ss, w') <- f r s
2626 return (fn a, ss, w <+> w)
2727
libs/base/Control/Monad/Reader.idr+1−1
@@ -27,7 +27,7 @@ instance Functor f => Functor (ReaderT r f) where
2727
2828instance Applicative m => Applicative (ReaderT r m) where
2929 pure = liftReaderT . pure
30− (RD f) <$> (RD v) = RD $ \r => f r <$> v r
30+ (RD f) <*> (RD v) = RD $ \r => f r <*> v r
3131
3232instance Alternative m => Alternative (ReaderT r m) where
3333 empty = liftReaderT empty
libs/base/Control/Monad/State.idr+1−1
@@ -25,7 +25,7 @@ instance Functor f => Functor (StateT s f) where
2525instance Monad f => Applicative (StateT s f) where
2626 pure x = ST (\st => pure (x, st))
2727
28− (ST f) <$> (ST a) = ST (\st => do (g, r) <- f st
28+ (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st
2929 (b, t) <- a r
3030 return (g b, t))
3131
libs/base/Control/Monad/Writer.idr+1−1
@@ -25,7 +25,7 @@ instance Functor f => Functor (WriterT w f) where
2525
2626instance (Monoid w, Applicative m) => Applicative (WriterT w m) where
2727 pure a = WR $ pure (a, neutral)
28− (WR f) <$> (WR v) = WR $ liftA2 merge f v where
28+ (WR f) <*> (WR v) = WR $ liftA2 merge f v where
2929 merge (fn, w) (a, w') = (fn a, w <+> w')
3030
3131instance (Monoid w, Alternative m) => Alternative (WriterT w m) where
libs/base/Data/Erased.idr+1−1
@@ -16,7 +16,7 @@ instance Functor Erased where
1616
1717instance Applicative Erased where
1818 pure = Erase
19− (<$>) (Erase f) (Erase x) = Erase (f x)
19+ (<*>) (Erase f) (Erase x) = Erase (f x)
2020
2121instance Monad Erased where
2222 (>>=) (Erase x) f = f x
libs/base/Data/Matrix.idr+29−29
@@ -7,13 +7,13 @@ import Data.Vect
77
88%default total
99
10−infixr 2 <.> -- vector inner product
10+infixr 2 <:> -- vector inner product
1111infixr 2 >< -- vector outer product
1212infixr 2 <<>> -- matrix commutator
1313infixr 2 >><< -- matrix anticommutator
1414infixl 3 <\> -- row times a matrix
1515infixr 4 </> -- matrix times a column
16−infixr 5 <> -- matrix multiplication
16+infixr 5 <> -- matrix multiplication
1717infixr 7 \&\ -- vector tensor product
1818infixr 7 <&> -- matrix tensor product
1919
@@ -26,14 +26,14 @@ instance Semigroup a => Semigroup (Vect n a) where
2626
2727instance Monoid a => Monoid (Vect n a) where
2828 neutral {n} = replicate n neutral
29−
29+
3030instance Group a => Group (Vect n a) where
3131 inverse = map inverse
3232
3333instance AbelianGroup a => AbelianGroup (Vect n a) where {}
3434
3535instance Ring a => Ring (Vect n a) where
36− (<*>) v w = zipWith (<*>) v w
36+ (<.>) v w = zipWith (<.>) v w
3737
3838instance RingWithUnity a => RingWithUnity (Vect n a) where
3939 unity {n} = replicate n unity
@@ -42,7 +42,7 @@ instance Field a => Field (Vect n a) where
4242 inverseM = map inverseM
4343
4444instance RingWithUnity a => Module a (Vect n a) where
45− (<#>) r v = map (r <*>) v
45+ (<#>) r v = map (r <.>) v
4646
4747instance RingWithUnity a => Module a (Vect n (Vect l a)) where
4848 (<#>) r m = map (r <#>) m
@@ -53,12 +53,12 @@ instance RingWithUnity a => Module a (Vect n (Vect l a)) where
5353-----------------------------------------------------------------------
5454
5555||| Inner product of ring vectors
56−(<.>) : Ring a => Vect n a -> Vect n a -> a
57−(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)
56+(<:>) : Ring a => Vect n a -> Vect n a -> a
57+(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)
5858
5959||| Tensor multiply (⊗) ring vectors
6060(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
61−(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
61+(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where
6262 orep : (n : Nat) -> Vect m a -> Vect (n * m) a
6363 orep n v = concat $ replicate n v
6464 oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
@@ -90,15 +90,15 @@ indices f1 f2 m = index f2 (index f1 m)
9090
9191||| Matrix times a column vector
9292(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
93−(</>) m v = map (v <.>) m
93+(</>) m v = map (v <:>) m
9494
9595||| Matrix times a row vector
9696(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
97−(<\>) r m = map (r <.>) $ transpose m
97+(<\>) r m = map (r <:>) $ transpose m
9898
9999||| Matrix multiplication
100−(<>) : Ring a => Matrix n k a ->
101− Matrix k m a ->
100+(<>) : Ring a => Matrix n k a ->
101+ Matrix k m a ->
102102 Matrix n m a
103103(<>) m1 m2 = map (<\> m2) m1
104104
@@ -110,11 +110,11 @@ indices f1 f2 m = index f2 (index f1 m)
110110 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
111111 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
112112
113−||| Cast a vector from a standard Vect to a proper n x 1 matrix
113+||| Cast a vector from a standard Vect to a proper n x 1 matrix
114114col : Vect n a -> Matrix n 1 a
115115col v = map (\x => [x]) v
116116
117−||| Cast a row from a standard Vect to a proper 1 x n matrix
117+||| Cast a row from a standard Vect to a proper 1 x n matrix
118118row : Vect n a -> Matrix 1 n a
119119row r = [r]
120120
@@ -157,11 +157,11 @@ instance Monoid Integer where
157157
158158instance Group Integer where
159159 inverse = (* -1)
160−
160+
161161instance AbelianGroup Integer
162162
163−instance Ring Integer where
164− (<*>) = (*)
163+instance Ring Integer where
164+ (<.>) = (*)
165165
166166instance RingWithUnity Integer where
167167 unity = 1
@@ -175,11 +175,11 @@ instance Monoid Int where
175175
176176instance Group Int where
177177 inverse = (* -1)
178−
178+
179179instance AbelianGroup Int
180180
181−instance Ring Int where
182− (<*>) = (*)
181+instance Ring Int where
182+ (<.>) = (*)
183183
184184instance RingWithUnity Int where
185185 unity = 1
@@ -193,11 +193,11 @@ instance Monoid Float where
193193
194194instance Group Float where
195195 inverse = (* -1)
196−
196+
197197instance AbelianGroup Float
198198
199−instance Ring Float where
200− (<*>) = (*)
199+instance Ring Float where
200+ (<.>) = (*)
201201
202202instance RingWithUnity Float where
203203 unity = 1
@@ -211,7 +211,7 @@ instance Semigroup Nat where
211211
212212instance Monoid Nat where
213213 neutral = 0
214−
214+
215215instance VerifiedSemigroup Nat where
216216 semigroupOpIsAssociative = plusAssociative
217217
@@ -228,12 +228,12 @@ instance Monoid ZZ where
228228
229229instance Group ZZ where
230230 inverse = (* -1)
231−
231+
232232instance AbelianGroup ZZ
233233
234−instance Ring ZZ where
235− (<*>) = (*)
236−
234+instance Ring ZZ where
235+ (<.>) = (*)
236+
237237instance RingWithUnity ZZ where
238238 unity = 1
239239
@@ -250,7 +250,7 @@ instance Group a => Group (Complex a) where
250250instance Ring a => AbelianGroup (Complex a) where {}
251251
252252instance Ring a => Ring (Complex a) where
253− (<*>) (a :+ b) (c :+ d) = (a <*> c <-> b <*> d) :+ (a <*> d <+> b <*> c)
253+ (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
254254
255255instance RingWithUnity a => RingWithUnity (Complex a) where
256256 unity = (unity :+ neutral)
libs/base/Data/Morphisms.idr+1−1
@@ -25,7 +25,7 @@ instance Functor (Morphism r) where
2525
2626instance Applicative (Morphism r) where
2727 pure a = Mor $ const a
28− (Mor f) <$> (Mor a) = Mor $ \r => f r $ a r
28+ (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r
2929
3030instance Monad (Morphism r) where
3131 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
libs/base/Data/VectType.idr+1−1
@@ -529,7 +529,7 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)
529529instance Applicative (Vect k) where
530530 pure = replicate _
531531
532− fs <$> vs = zipWith apply fs vs
532+ fs <*> vs = zipWith apply fs vs
533533
534534instance Monad (Vect n) where
535535 m >>= f = diag (map f m)
libs/base/Network/Cgi.idr+1−1
@@ -36,7 +36,7 @@ instance Functor CGI where
3636instance Applicative CGI where
3737 pure v = MkCGI (\s => return (v, s))
3838
39− (MkCGI a) <$> (MkCGI b) = MkCGI (\s => do (f, i) <- a s
39+ (MkCGI a) <*> (MkCGI b) = MkCGI (\s => do (f, i) <- a s
4040 (c, j) <- b i
4141 return (f c, j))
4242
libs/base/Providers.idr+3−3
@@ -17,9 +17,9 @@ instance Functor Provider where
1717 map f (Error err) = Error err
1818
1919instance Applicative Provider where
20− (Provide f) <$> (Provide x) = Provide (f x)
21− (Provide f) <$> (Error err) = Error err
22− (Error err) <$> _ = Error err
20+ (Provide f) <*> (Provide x) = Provide (f x)
21+ (Provide f) <*> (Error err) = Error err
22+ (Error err) <*> _ = Error err
2323 pure = Provide
2424
2525instance Monad Provider where
libs/base/System/Concurrency/Process.idr+1−1
@@ -19,7 +19,7 @@ instance Functor (Process msg) where
1919
2020instance Applicative (Process msg) where
2121 pure = Lift . return
22− (Lift f) <$> (Lift a) = Lift (f <$> a)
22+ (Lift f) <*> (Lift a) = Lift (f <*> a)
2323
2424instance Monad (Process msg) where
2525 (Lift io) >>= k = Lift (do x <- io
libs/effects/Effect/Memory.idr+12−12
@@ -24,11 +24,11 @@ data RawMemory : Effect where
2424 (size : Nat) ->
2525 So (offset + size <= i) ->
2626 RawMemory (Vect size Bits8)
27− (MemoryChunk n i) (\v => MemoryChunk n i)
27+ (MemoryChunk n i) (\v => MemoryChunk n i)
2828 Poke : (offset : Nat) ->
2929 (Vect size Bits8) ->
3030 So (offset <= i && offset + size <= n) ->
31− RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
31+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
3232 Move : (src : MemoryChunk src_size src_init) ->
3333 (dst_offset : Nat) ->
3434 (src_offset : Nat) ->
@@ -36,8 +36,8 @@ data RawMemory : Effect where
3636 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
3737 So (src_offset + size <= src_init) ->
3838 RawMemory () (MemoryChunk dst_size dst_init)
39− (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
40− GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
39+ (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
40+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
4141
4242private
4343do_malloc : Nat -> IOExcept String Ptr
@@ -84,9 +84,9 @@ instance Handler RawMemory (IOExcept String) where
8484 = do ptr <- do_malloc n
8585 k () (CH ptr)
8686 handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k
87− = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)
87+ = ioe_lift (do_memset ptr i c size) *> k () (CH ptr)
8888 handle (CH ptr) (Free) k
89− = ioe_lift (do_free ptr) $> k () ()
89+ = ioe_lift (do_free ptr) *> k () ()
9090 handle (CH ptr) (Peek offset size _) k
9191 = do res <- ioe_lift (do_peek ptr offset size)
9292 k res (CH ptr)
@@ -102,7 +102,7 @@ instance Handler RawMemory (IOExcept String) where
102102RAW_MEMORY : Type -> EFFECT
103103RAW_MEMORY t = MkEff t RawMemory
104104
105−allocate : (n : Nat) ->
105+allocate : (n : Nat) ->
106106 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
107107allocate size = call $ Allocate size
108108
@@ -111,7 +111,7 @@ initialize : {i : Nat} ->
111111 Bits8 ->
112112 (size : Nat) ->
113113 So (i + size <= n) ->
114− Eff () [RAW_MEMORY (MemoryChunk n i)]
114+ Eff () [RAW_MEMORY (MemoryChunk n i)]
115115 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
116116initialize c size prf = call $ Initialize c size prf
117117
@@ -122,7 +122,7 @@ peek : {i : Nat} ->
122122 (offset : Nat) ->
123123 (size : Nat) ->
124124 So (offset + size <= i) ->
125− { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
125+ { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
126126peek offset size prf = call $ Peek offset size prf
127127
128128poke : {n : Nat} ->
@@ -130,12 +130,12 @@ poke : {n : Nat} ->
130130 (offset : Nat) ->
131131 Vect size Bits8 ->
132132 So (offset <= i && offset + size <= n) ->
133− Eff () [RAW_MEMORY (MemoryChunk n i)]
133+ Eff () [RAW_MEMORY (MemoryChunk n i)]
134134 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
135135poke offset content prf = call $ Poke offset content prf
136136
137137private
138−getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
138+getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
139139getRawPtr = call $ GetRawPtr
140140
141141private
@@ -173,5 +173,5 @@ move : {dst_size : Nat} ->
173173move dst_offset src_offset size dst_bounds src_bounds
174174 = do src_ptr <- Src :- getRawPtr
175175 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
176− return ()
176+ return ()
177177
libs/effects/Effect/Monad.idr+1−1
@@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)
1111
1212 instance Applicative (\a => EffM m a xs (\v => xs)) where
1313 pure = value
14− (<$>) f a = do f' <- f
14+ (<*>) f a = do f' <- f
1515 a' <- a
1616 value (f' a')
1717
libs/effects/Effects.idr+3−3
@@ -174,7 +174,7 @@ return x = value x
174174
175175-- ------------------------------------------------------ [ for idiom brackets ]
176176
177−infixl 2 <$>
177+infixl 2 <*>
178178
179179pure : a -> Eff a xs (\v => xs)
180180pure = value
@@ -182,9 +182,9 @@ pure = value
182182pureM : (val : a) -> Eff a (xs val) xs
183183pureM = value
184184
185−(<$>) : Eff (a -> b) xs (\v => xs) ->
185+(<*>) : Eff (a -> b) xs (\v => xs) ->
186186 Eff a xs (\v => xs) -> Eff b xs (\v => xs)
187−(<$>) prog v = do fn <- prog
187+(<*>) prog v = do fn <- prog
188188 arg <- v
189189 return (fn arg)
190190
libs/oldeffects/Effect/Monad.idr+1−1
@@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)
1111
1212 instance Applicative (\a => EffM m a xs (\v => xs)) where
1313 pure = value
14− (<$>) f a = do f' <- f
14+ (<*>) f a = do f' <- f
1515 a' <- a
1616 value (f' a')
1717
libs/oldeffects/Effects.idr+3−3
@@ -185,16 +185,16 @@ return x = value x
185185
186186-- ------------------------------------------------------ [ for idiom brackets ]
187187
188−infixl 2 <$>
188+infixl 2 <*>
189189
190190pure : a -> Eff m a xs (\v => xs)
191191pure = value
192192
193193syntax pureM [val] = with_val val (pure ())
194194
195−(<$>) : Eff m (a -> b) xs (\v => xs) ->
195+(<*>) : Eff m (a -> b) xs (\v => xs) ->
196196 Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
197−(<$>) prog v = do fn <- prog
197+(<*>) prog v = do fn <- prog
198198 arg <- v
199199 return (fn arg)
200200
libs/prelude/Language/Reflection/Tactical.idr+1−1
@@ -45,7 +45,7 @@ instance Functor Tactical where
4545
4646instance Applicative Tactical where
4747 pure x = prim__PureTactical x
48− f <$> x = prim__BindTactical f $ \g =>
48+ f <*> x = prim__BindTactical f $ \g =>
4949 prim__BindTactical x $ \y =>
5050 prim__PureTactical $ g y
5151
libs/prelude/Prelude.idr+8−8
@@ -249,31 +249,31 @@ instance Functor (Either e) where
249249instance Applicative PrimIO where
250250 pure = prim_io_return
251251
252− am <$> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
252+ am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
253253
254254instance Applicative (IO' ffi) where
255255 pure x = io_return x
256− f <$> a = io_bind f (\f' =>
256+ f <*> a = io_bind f (\f' =>
257257 io_bind a (\a' =>
258258 io_return (f' a')))
259259
260260instance Applicative Maybe where
261261 pure = Just
262262
263− (Just f) <$> (Just a) = Just (f a)
264− _ <$> _ = Nothing
263+ (Just f) <*> (Just a) = Just (f a)
264+ _ <*> _ = Nothing
265265
266266instance Applicative (Either e) where
267267 pure = Right
268268
269− (Left a) <$> _ = Left a
270− (Right f) <$> (Right r) = Right (f r)
271− (Right _) <$> (Left l) = Left l
269+ (Left a) <*> _ = Left a
270+ (Right f) <*> (Right r) = Right (f r)
271+ (Right _) <*> (Left l) = Left l
272272
273273instance Applicative List where
274274 pure x = [x]
275275
276− fs <$> vs = concatMap (\f => map f vs) fs
276+ fs <*> vs = concatMap (\f => map f vs) fs
277277
278278---- Alternative instances
279279
libs/prelude/Prelude/Algebra.idr+37−37
@@ -5,7 +5,7 @@ import Builtins
55-- XXX: change?
66infixl 6 <->
77infixl 6 <+>
8−infixl 6 <*>
8+infixl 6 <.>
99infixl 5 <#>
1010
1111%access public
@@ -96,18 +96,18 @@ class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
9696||| + Inverse for `<+>`:
9797||| forall a, a <+> inverse a == neutral
9898||| forall a, inverse a <+> a == neutral
99−||| + Associativity of `<*>`:
100−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
101−||| + Distributivity of `<*>` and `<->`:
102−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
103−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
99+||| + Associativity of `<.>`:
100+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
101+||| + Distributivity of `<.>` and `<->`:
102+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
103+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
104104class AbelianGroup a => Ring a where
105− (<*>) : a -> a -> a
105+ (<.>) : a -> a -> a
106106
107107class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
108− total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
109− total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
110− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (c <*> r)
108+ total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
109+ total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
110+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
111111
112112||| Sets equipped with two binary operations, one associative and commutative
113113||| supplied with a neutral element, and the other associative supplied with a
@@ -124,20 +124,20 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
124124||| + Inverse for `<+>`:
125125||| forall a, a <+> inverse a == neutral
126126||| forall a, inverse a <+> a == neutral
127−||| + Associativity of `<*>`:
128−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
129−||| + Neutral for `<*>`:
130−||| forall a, a <*> unity == a
131−||| forall a, unity <*> a == a
132−||| + Distributivity of `<*>` and `<->`:
133−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
134−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
127+||| + Associativity of `<.>`:
128+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
129+||| + Neutral for `<.>`:
130+||| forall a, a <.> unity == a
131+||| forall a, unity <.> a == a
132+||| + Distributivity of `<.>` and `<->`:
133+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
134+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
135135class Ring a => RingWithUnity a where
136136 unity : a
137137
138138class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
139− total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
140− total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
139+ total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
140+ total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
141141
142142||| Sets equipped with a binary operation that is commutative, associative and
143143||| idempotent. Must satisfy the following laws:
@@ -281,31 +281,31 @@ class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, Verif
281281||| + Inverse for `<+>`:
282282||| forall a, a <+> inverse a == neutral
283283||| forall a, inverse a <+> a == neutral
284−||| + Associativity of `<*>`:
285−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
286−||| + Unity for `<*>`:
287−||| forall a, a <*> unity == a
288−||| forall a, unity <*> a == a
289−||| + InverseM of `<*>`:
290−||| forall a, a <*> inverseM a == unity
291−||| forall a, inverseM a <*> a == unity
292−||| + Distributivity of `<*>` and `<->`:
293−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
294−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
284+||| + Associativity of `<.>`:
285+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
286+||| + Unity for `<.>`:
287+||| forall a, a <.> unity == a
288+||| forall a, unity <.> a == a
289+||| + InverseM of `<.>`:
290+||| forall a, a <.> inverseM a == unity
291+||| forall a, inverseM a <.> a == unity
292+||| + Distributivity of `<.>` and `<->`:
293+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
294+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
295295class RingWithUnity a => Field a where
296296 inverseM : a -> a
297297
298298class (VerifiedRing a, Field a) => VerifiedField a where
299− total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
300− total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
299+ total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity
300+ total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity
301301
302302||| A module over a ring is an additive abelian group of 'vectors' endowed with a
303−||| scale operation multiplying vectors by ring elements, and distributivity laws
304−||| relating the scale operation to both ring addition and module addition.
303+||| scale operation multiplying vectors by ring elements, and distributivity laws
304+||| relating the scale operation to both ring addition and module addition.
305305||| Must satisfy the following laws:
306306|||
307307||| + Compatibility of scalar multiplication with ring multiplication:
308−||| forall a b v, a <#> (b <#> v) = (a <*> b) <#> v
308+||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v
309309||| + Ring unity is the identity element of scalar multiplication:
310310||| forall v, unity <#> v = v
311311||| + Distributivity of `<#>` and `<+>`:
@@ -315,7 +315,7 @@ class (RingWithUnity a, AbelianGroup b) => Module a b where
315315 (<#>) : a -> b -> b
316316
317317class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
318− total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <*> y) <#> v
318+ total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
319319 total moduleScalarUnityIsUnity : (v : b) -> unity <#> v = v
320320 total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
321321 total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
libs/prelude/Prelude/Applicative.idr+17−17
@@ -9,46 +9,46 @@ import Prelude.Functor
99
1010---- Applicative functors/Idioms
1111
12−infixl 2 <$>
12+infixl 2 <*>
1313
1414class Functor f => Applicative (f : Type -> Type) where
1515 pure : a -> f a
16− (<$>) : f (a -> b) -> f a -> f b
16+ (<*>) : f (a -> b) -> f a -> f b
1717
1818instance Applicative id where
1919 pure a = a
20− f <$> a = f a
20+ f <*> a = f a
2121
2222class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
2323 applicativeMap : (x : f a) -> (g : a -> b) ->
24− map g x = pure g <$> x
25− applicativeIdentity : (x : f a) -> pure id <$> x = x
24+ map g x = pure g <*> x
25+ applicativeIdentity : (x : f a) -> pure id <*> x = x
2626 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->
27− ((pure (.) <$> g2) <$> g1) <$> x = g2 <$> (g1 <$> x)
27+ ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)
2828 applicativeHomomorphism : (x : a) -> (g : a -> b) ->
29− (<$>) {f} (pure g) (pure x) = pure {f} (g x)
29+ (<*>) {f} (pure g) (pure x) = pure {f} (g x)
3030 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
31− g <$> pure x = pure (\g' : a -> b => g' x) <$> g
31+ g <*> pure x = pure (\g' : a -> b => g' x) <*> g
3232
33−infixl 2 <$
34−(<$) : Applicative f => f a -> f b -> f a
35−a <$ b = map const a <$> b
33+infixl 2 <*
34+(<*) : Applicative f => f a -> f b -> f a
35+a <* b = map const a <*> b
3636
37−infixl 2 $>
38−($>) : Applicative f => f a -> f b -> f b
39−a $> b = map (const id) a <$> b
37+infixl 2 *>
38+(*>) : Applicative f => f a -> f b -> f b
39+a *> b = map (const id) a <*> b
4040
4141||| Lift a function to an applicative
4242liftA : Applicative f => (a -> b) -> f a -> f b
43−liftA f a = pure f <$> a
43+liftA f a = pure f <*> a
4444
4545||| Lift a two-argument function to an applicative
4646liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c
47−liftA2 f a b = (map f a) <$> b
47+liftA2 f a b = (map f a) <*> b
4848
4949||| Lift a three-argument function to an applicative
5050liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
51−liftA3 f a b c = (map f a) <$> b <$> c
51+liftA3 f a b c = (map f a) <*> b <*> c
5252
5353infixl 3 <|>
5454class Applicative f => Alternative (f : Type -> Type) where
libs/prelude/Prelude/Functor.idr+8
@@ -10,6 +10,14 @@ class Functor (f : Type -> Type) where
1010 ||| @ m the morphism
1111 map : (m : a -> b) -> f a -> f b
1212
13+infixl 4 <$>
14+
15+||| An infix alias for `map`: the action of a functor on morphisms.
16+||| @ f the functor
17+||| @ m the morphism
18+(<$>) : Functor f => (m : a -> b) -> f a -> f b
19+m <$> x = map m x
20+
1321class Functor f => VerifiedFunctor (f : Type -> Type) where
1422 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x
1523 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
libs/prelude/Prelude/Monad.idr+1−1
@@ -16,7 +16,7 @@ class Applicative m => Monad (m : Type -> Type) where
1616
1717class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
1818 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
19− mf <$> mx = mf >>= \f =>
19+ mf <*> mx = mf >>= \f =>
2020 mx >>= \x =>
2121 pure (f x)
2222 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x
libs/prelude/Prelude/Stream.idr+1−1
@@ -111,7 +111,7 @@ scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs
111111
112112instance Applicative Stream where
113113 pure = repeat
114− (<$>) = zipWith apply
114+ (<*>) = zipWith apply
115115
116116instance Monad Stream where
117117 s >>= f = diag (map f s)
libs/prelude/Prelude/Traversable.idr+2−2
@@ -8,10 +8,10 @@ import Prelude.Foldable
88import Prelude.Functor
99
1010traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
11−traverse_ f = foldr (($>) . f) (pure ())
11+traverse_ f = foldr ((*>) . f) (pure ())
1212
1313sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
14−sequence_ = foldr ($>) (pure ())
14+sequence_ = foldr (*>) (pure ())
1515
1616for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
1717for_ = flip traverse_
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+}
samples/interp.idr+2−2
@@ -37,8 +37,8 @@ using (G : Vect n Ty)
3737 index_first = stop
3838 index_next = pop
3939
40− (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
41− (<$>) = \f, a => App f a
40+ (<*>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
41+ (<*>) = \f, a => App f a
4242
4343 pure : Expr G a -> Expr G a
4444 pure = id
src/Idris/AbsSyntax.hs+8−1
@@ -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'
@@ -1978,8 +1982,11 @@ shadow :: Name -> Name -> PTerm -> PTerm
19781982shadow n n' t = sm t where
19791983 sm (PRef fc x) | n == x = PRef fc n'
19801984 sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)
1981− sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
1985+ | otherwise = PLam fc x (sm t) sc
1986+ sm (PPi p x t sc) | n /= x = PPi p x (sm t) (sm sc)
1987+ | otherwise = PPi p x (sm t) sc
19821988 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)
1989+ | otherwise = PLet fc x (sm t) (sm v) sc
19831990 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
19841991 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
19851992 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
src/Idris/AbsSyntaxTree.hs+1−1
@@ -1157,7 +1157,7 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
11571157
11581158initDSL = DSL (PRef f (sUN ">>="))
11591159 (PRef f (sUN "return"))
1160− (PRef f (sUN "<$>"))
1160+ (PRef f (sUN "<*>"))
11611161 (PRef f (sUN "pure"))
11621162 Nothing
11631163 Nothing
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/DSL.hs+28−6
@@ -17,21 +17,43 @@ desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
1717desugar syn i t = let t' = expandDo (dsl_info syn) t in
1818 t' -- addImpl i t'
1919
20+mkTTName :: FC -> Name -> PTerm
21+mkTTName fc n =
22+ let mkList fc [] = PRef fc (sNS (sUN "Nil") ["List", "Prelude"])
23+ mkList fc (x:xs) = PApp fc (PRef fc (sNS (sUN "::") ["List", "Prelude"]))
24+ [ pexp (stringC x)
25+ , pexp (mkList fc xs)]
26+ stringC = PConstant . Str . str
27+ intC = PConstant . I
28+ reflm n = sNS (sUN n) ["Reflection", "Language"]
29+ in case n of
30+ UN nm -> PApp fc (PRef fc (reflm "UN")) [ pexp (stringC nm)]
31+ NS nm ns -> PApp fc (PRef fc (reflm "NS")) [ pexp (mkTTName fc nm)
32+ , pexp (mkList fc ns)]
33+ MN i nm -> PApp fc (PRef fc (reflm "MN")) [ pexp (intC i)
34+ , pexp (stringC nm)]
35+ otherwise -> PRef fc $ reflm "NErased"
36+
2037expandDo :: DSL -> PTerm -> PTerm
2138expandDo dsl (PLam fc n ty tm)
2239 | Just lam <- dsl_lambda dsl
23− = let sc = PApp fc lam [pexp (var dsl n tm 0)] in
24− expandDo dsl sc
40+ = let sc = PApp fc lam [ pexp (mkTTName fc n)
41+ , pexp (var dsl n tm 0)]
42+ in expandDo dsl sc
2543expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)
2644expandDo dsl (PLet fc n ty v tm)
2745 | Just letb <- dsl_let dsl
28− = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in
29− expandDo dsl sc
46+ = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)
47+ , pexp v
48+ , pexp (var dsl n tm 0)]
49+ in expandDo dsl sc
3050expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
3151expandDo dsl (PPi p n ty tm)
3252 | Just pi <- dsl_pi dsl
33− = let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in
34− expandDo dsl sc
53+ = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)
54+ , pexp ty
55+ , pexp (var dsl n tm 0)]
56+ in expandDo dsl sc
3557expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
3658expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
3759 (map (fmap (expandDo dsl)) args)
src/Idris/Elab/Clause.hs+3−3
@@ -648,9 +648,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
648648 -- Now build the RHS, using the type of the LHS as the goal.
649649 i <- getIState -- new implicits from where block
650650 logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
651− let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)
651+ let rhs = addImplBoundInf i (map fst newargs_all) (defs \\ decls)
652652 (expandParams decorate newargs defs (defs \\ decls) rhs_in)
653− logLvl 2 $ "RHS: " ++ showTmImpls rhs
653+ logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs
654654 ctxt <- getContext -- new context with where block added
655655 logLvl 5 "STARTING CHECK"
656656 ((rhs', defer, is, probs), _) <-
@@ -673,7 +673,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
673673 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)
674674
675675 logLvl 5 "DONE CHECK"
676− logLvl 2 $ "---> " ++ show rhs'
676+ logLvl 4 $ "---> " ++ show rhs'
677677 when (not (null defer)) $ iLOG $ "DEFERRED " ++
678678 show (map (\ (n, (_,_,t)) -> (n, t)) defer)
679679 def' <- checkDef fc defer
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/ElabTerm.hs+9−1
@@ -893,9 +893,17 @@ elab ist info emode opts fn tm
893893 -- Drop the unique arguments used in the term already
894894 -- and in the scrutinee (since it's
895895 -- not valid to use them again anyway)
896+ --
897+ -- Also drop unique arguments which don't appear explicitly
898+ -- in either case branch so they don't count as used
899+ -- unnecessarily (can only do this for unique things, since we
900+ -- assume they don't appear implicitly in types)
896901 ptm <- get_term
902+ let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
903+
897904 let argsDropped = filter (isUnique envU)
898− (nub $ allNamesIn scr ++ inApp ptm)
905+ (nub $ allNamesIn scr ++ inApp ptm ++
906+ inOpts)
899907
900908 let args' = filter (\(n, _) -> n `notElem` argsDropped) args
901909
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
@@ -1311,8 +1311,24 @@ loadSource lidr f toline
13111311 mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports]
13121312 let syntax = defaultSyntax{ syn_namespace = reverse mname,
13131313 maxline = toline }
1314+ ist <- getIState
1315+ -- Save the span from parsing the module header, because
1316+ -- an empty program parse might obliterate it.
1317+ let oldSpan = idris_parsedSpan ist
13141318 ds' <- parseProg syntax f file pos
13151319
1320+ case (ds', oldSpan) of
1321+ ([], Just fc) ->
1322+ -- If no program elements were parsed, we dind't
1323+ -- get a loaded region in the IBC file. That
1324+ -- means we need to add it back.
1325+ do ist <- getIState
1326+ putIState ist { idris_parsedSpan = oldSpan
1327+ , ibc_write = IBCParsedRegion fc :
1328+ ibc_write ist
1329+ }
1330+ _ -> return ()
1331+
13161332 -- Parsing done, now process declarations
13171333
13181334 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"
test/dsl001/test001.idr+4−1
@@ -35,8 +35,11 @@ using (G : Vect n Ty)
3535 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
3636 Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
3737
38+ lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)
39+ lam_ _ = Lam
40+
3841 dsl expr
39− lambda = Lam
42+ lambda = lam_
4043 variable = Var
4144 index_first = stop
4245 index_next = pop
test/dsl002/Resimp.idr+6−1
@@ -156,6 +156,11 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)
156156 = interp env v (\env', v' => do n <- v'
157157 interp env' (f n) k)
158158
159+ let_ : _ -> Creator (interpTy a) ->
160+ Res (a :: gam) (Val () :: gam') (R t) ->
161+ Res gam gam' (R t)
162+ let_ _ = Let
163+
159164-- run : {static} Res [] [] (R t) -> IO t
160165-- run prog = interp [] prog (\env, res => res)
161166
@@ -163,7 +168,7 @@ syntax run [prog] = interp [] prog (\env, res => res)
163168
164169dsl res
165170 variable = id
166− let = Let
171+ let = let_
167172 index_first = stop
168173 index_next = pop
169174
test/dsl003/DSLPi.idr+8−2
@@ -5,8 +5,11 @@ import Data.Vect
55
66data Ty = BOOL | INT | UNIT | ARR Ty Ty
77
8+arr_ : _ -> Ty -> Ty -> Ty
9+arr_ _ = ARR
10+
811dsl simple_type
9− pi = ARR
12+ pi = arr_
1013
1114test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)
1215test1 = Refl
@@ -25,8 +28,11 @@ using (vars : Vect n Ty)
2528 implicit exprSpec : Expr vars BOOL -> Spec vars
2629 exprSpec = ItHolds
2730
31+ forall_ : _ -> (t : Ty) -> Spec (t :: vars) -> Spec vars
32+ forall_ _ = ForAll
33+
2834dsl specs
29− pi = ForAll
35+ pi = forall_
3036 variable = Var
3137 index_first = FZ
3238 index_next = FS
test/reg027/reg027.idr+1−1
@@ -14,7 +14,7 @@ instance Functor IntFn where -- (\x => Int -> x) where
1414
1515instance Applicative (\x => Int -> x) where
1616 pure v = \x => v
17− (<$>) f a = \x => f x (a x)
17+ (<*>) f a = \x => f x (a x)
1818
1919instance Monad IntFn where
2020 f >>= k = \x => k (f x) x
test/reg050/expected+8−7
@@ -12,17 +12,18 @@ When elaborating an application of function Prelude.Monad.>>=:
1212 \{uv0} => argTy -> uv
1313./baddoublebang.idr:6:26: error: not
1414 a terminator, expected: "$",
15− "$>", "&&", "*", "+", "++", "-",
15+ "&&", "*", "*>", "+", "++", "-",
1616 "->", ".", "/", "/=", "::", ";",
17− "<", "<#>", "<$", "<$>", "<*>",
18− "<+>", "<->", "<<", "<=", "<|>",
19− "=", "==", ">", ">=", ">>",
20− ">>=", "\\\\", "`", "in", "||",
21− "~=~",
17+ "<", "<#>", "<$>", "<*", "<*>",
18+ "<+>", "<->", "<.>", "<<", "<=",
19+ "<|>", "=", "==", ">", ">=",
20+ ">>", ">>=", "\\\\", "`", "in",
21+ "||", "~=~",
2222 ambiguous use of a left-associative operator,
2323 ambiguous use of a non-associative operator,
2424 ambiguous use of a right-associative operator,
2525 end of input, function argument,
26− matching application expression
26+ matching application expression,
27+ single-line comment
2728doubleBang mmn = do pure !!mmn
2829 ^
test/reg053/four.idr+1−1
@@ -5,5 +5,5 @@ data FourFunctor y = Four y y y y
55traverseFourFunctor : Applicative f ->
66 (x -> f b) -> FourFunctor x -> f (FourFunctor b)
77traverseFourFunctor constr f (Four w x y z)
8− = pure Four <$> (f w) <$> (f x) <$> (f y) <$> (f z)
8+ = pure Four <*> (f w) <*> (f x) <*> (f y) <*> (f z)
99
test/sourceLocation001/SourceLoc.idr+3−1
@@ -54,6 +54,8 @@ using (ctxt : Vect n Ty)
5454 run (App f x) env = !(run f env) !(run x env)
5555 run (Die {loc}) _ = Left loc
5656
57+ lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')
58+ lam_ _ = Lam
5759
5860exec : Tm [] t -> IO ()
5961exec tm = case run tm [] of
@@ -64,7 +66,7 @@ dsl lang
6466 variable = Var
6567 index_first = FZ
6668 index_next = FS
67− lambda = Lam
69+ lambda = lam_
6870
6971testTerm1 : Tm [] (Arr U U)
7072testTerm1 = lang (\x=>Die)
test/sourceLocation001/expected+2−2
@@ -3,9 +3,9 @@ FileLoc "SourceLoc.idr" (16, 11) (16, 11)
33Testing using inline tactics
44FileLoc "SourceLoc.idr" (20, 17) (20, 17)
55Testing using metavariable with later definition
6−FileLoc "SourceLoc.idr" (96, 16) (96, 16)
6+FileLoc "SourceLoc.idr" (98, 16) (98, 16)
77-----------------------
88Success!
9−Error at FileLoc "SourceLoc.idr" (70, 23) (70, 23)
9+Error at FileLoc "SourceLoc.idr" (72, 23) (72, 23)
1010Success!
1111Success!
test/sugar001/test007.idr+1−1
@@ -19,7 +19,7 @@ instance Functor Eval where
1919instance Applicative Eval where
2020 pure x = MkEval (\e => Just x)
2121
22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where
22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where
2323 appAux : Maybe (a -> b) -> Maybe a -> Maybe b
2424 appAux (Just fx) (Just gx) = Just (fx gx)
2525 appAux _ _ = Nothing
test/tutorial003/tutorial003.idr+1−1
@@ -19,7 +19,7 @@ instance Functor Eval where
1919instance Applicative Eval where
2020 pure x = MkEval (\e => Just x)
2121
22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
2323 app : Maybe (a -> b) -> Maybe a -> Maybe b
2424 app (Just fx) (Just gx) = Just (fx gx)
2525 app _ _ = Nothing