on master help sign in
Merge branch 'master' into parenthasizeInfix

Conflicts: src/Idris/REPL.hs

commitc4eca4f8b82690210ba9f4f8276f15ac3c472edc authorbmsherman <bmsherman@users.noreply.github.com> dateSat 21 Jun 2014, 12:48 (12 years ago) parent7d3894376f8684
101 files changed+2390−1468
CHANGELOG+6−1 CONTRIBUTORS+1 Makefile+6−1 config.mk+1−2 contribs/idrislang.sty+4−1 idris.cabal+15−12 libs/Makefile+18−2 libs/base/Data/HVect.idr+5−5 libs/base/Language/Reflection.idr+3−1 libs/base/Makefile+10−3 libs/base/Network/Socket.idr+139−36 libs/base/Providers.idr−9 libs/effects/Effects.idr+51−30 libs/effects/Makefile+13−5 libs/neweffects/Effect/Default.idr+44 libs/oldeffects/Effect/Exception.idr → libs/neweffects/Effect/Exception.idr+7−5 libs/neweffects/Effect/File.idr+128 libs/oldeffects/Effect/Memory.idr → libs/neweffects/Effect/Memory.idr+38−32 libs/oldeffects/Effect/Monad.idr → libs/neweffects/Effect/Monad.idr+4−4 libs/neweffects/Effect/Random.idr+47 libs/oldeffects/Effect/Select.idr → libs/neweffects/Effect/Select.idr+5−5 libs/oldeffects/Effect/State.idr → libs/neweffects/Effect/State.idr+12−12 libs/neweffects/Effect/StdIO.idr+60 libs/neweffects/Effect/System.idr+38 libs/neweffects/Effects.idr+292 libs/oldeffects/Makefile → libs/neweffects/Makefile+3−3 libs/oldeffects/oldeffects.ipkg → libs/neweffects/effects.ipkg+4−3 libs/oldeffects/Effect/File.idr−69 libs/oldeffects/Effect/Random.idr−25 libs/oldeffects/Effect/StdIO.idr−60 libs/oldeffects/Effects.idr−308 libs/prelude/Makefile+11−4 libs/prelude/Prelude/Algebra.idr+1−1 libs/prelude/Prelude/Bool.idr+1−1 libs/prelude/Prelude/List.idr+9 libs/prelude/Prelude/Nat.idr+34 libs/prelude/Prelude/Stream.idr+1−1 libs/prelude/Prelude/Strings.idr+5−1 libs/prelude/Prelude/Vect.idr+11−16 rts/idris_gc.c+11−2 rts/idris_heap.c+8−1 rts/idris_net.c+190−23 rts/idris_net.h+34−1 rts/idris_rts.c+23−11 rts/idris_rts.h+13−9 rts/windows/idris_net.c+1−1 src/IRTS/CodegenC.hs+1 src/IRTS/CodegenJava.hs+8−5 src/IRTS/Java/JTypes.hs+31 src/IRTS/Java/Pom.hs+7−1 src/Idris/AbsSyntax.hs+9−8 src/Idris/AbsSyntaxTree.hs+37−26 src/Idris/Colours.hs+15−8 src/Idris/Completion.hs+2−1 src/Idris/Core/Binary.hs+356 src/Idris/Core/CaseTree.hs+3 src/Idris/Core/Elaborate.hs+7−4 src/Idris/Core/Evaluate.hs+23−5 src/Idris/Core/ProofState.hs+26−12 src/Idris/Core/TT.hs+3−2 src/Idris/DSL.hs+8−1 src/Idris/DeepSeq.hs+10−9 src/Idris/Delaborate.hs+61−19 src/Idris/Docs.hs+4−4 src/Idris/ElabDecls.hs+34−24 src/Idris/ElabTerm.hs+33−13 src/Idris/Erasure.hs+1−1 src/Idris/IBC.hs+11−348 src/Idris/IdeSlave.hs+26−4 src/Idris/IdrisDoc.hs+2−1 src/Idris/Interactive.hs+4−4 src/Idris/Output.hs+1−33 src/Idris/ParseData.hs+9−6 src/Idris/ParseExpr.hs+12−6 src/Idris/Parser.hs+14−13 src/Idris/Prover.hs+96−84 src/Idris/Providers.hs+1−7 src/Idris/REPL.hs+122−45 src/Idris/REPLParser.hs+1−1 test/Makefile+1−1 test/dsl003/DSLPi.idr+38 test/dsl003/expected+2 test/dsl003/run+3 test/ffi005/Postulate.idr+3−3 test/ffi005/Postulate2.idr−13 test/ffi005/Postulate3.idr−13 test/ffi005/expected−2 test/ffi005/run−7 test/reg008/expected test/reg008/reg008.idr−15 test/reg008/run−3 test/reg029/Reg029Wrapper.java+17 test/reg029/reg029.idr+1 test/reg029/run+12−2 test/reg034/expected+2−2 test/reg043/expected−1 test/reg043/run−3 test/reg045/expected+1 test/reg045/reg045.idr+19 test/reg045/run+4 test/tutorial006/expected+2−2
CHANGELOG+6−1
@@ -1,8 +1,13 @@
11New in 0.9.14:
22--------------
3+* Tactic for case analysis in proofs
4+* Induction and case tactic now work on expressions
35* Support for running tests for a package with the tests section of .ipkg files and the
46 --testpkg command-line option
5−
7+* Clearly distinguish between type providers and postulate providers at the use site
8+* Allow dependent function syntax to be overridden in dsl blocks, similarly to
9+ functions and let. The keyword for this is "pi".
10+* Experimental 'neweffects' library, with simplified API
611
712New in 0.9.13:
813--------------
CONTRIBUTORS+1
@@ -3,6 +3,7 @@ Thanks to the following for their help and contributions:
33Ozgur Akgun
44Ahmad Salim Al-Sibahi
55Edward Chadwick Amsden
6+Jan Bessai
67Nicola Botta
78Edwin Brady
89David Raymond Christiansen
Makefile+6−1
@@ -1,4 +1,4 @@
1−.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib test_c test
1+.PHONY: build configure doc install linecount nodefault pinstall lib_clean relib test_c test lib_doc lib_doc_clean
22
33include config.mk
44-include custom.mk
@@ -45,6 +45,11 @@ linecount:
4545doc: dist/setup-config
4646 $(CABAL) haddock --hyperlink-source --html --hoogle --html-location="http://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"
4747
48+lib_doc:
49+ $(MAKE) -C libs IDRIS=../../dist/build/idris/idris doc
50+
51+lib_doc_clean:
52+ $(MAKE) -C libs IDRIS=../../dist/build/idris/idris doc_clean
4853
4954dist/setup-config:
5055 $(CABAL) configure $(CABALFLAGS)
config.mk+1−2
@@ -1,6 +1,6 @@
11CC ?=cc
22CABAL :=cabal
3−CFLAGS :=-O2 -Wall $(CFLAGS)
3+CFLAGS :=-O2 -Wall -DHAS_PTHREAD $(CFLAGS)
44#CABALFLAGS :=
55## Disable building of Effects
66#CABALFLAGS :=-f NoEffects
@@ -35,4 +35,3 @@ else
3535 SHLIB_SUFFIX :=.so
3636endif
3737endif
38−
contribs/idrislang.sty+4−1
@@ -25,6 +25,7 @@
2525\RequirePackage{listings}
2626\RequirePackage{xspace}
2727\RequirePackage{textcomp}
28+\RequirePackage{setspace}
2829%% ----------------------------------------------------------------- [ Options ]
2930\newboolean{literate}
3031\setboolean{literate}{false}
@@ -117,7 +118,9 @@
117118 \lstset{language=idris}}
118119 \ifthenelse{\boolean{numbers}}{%
119120 \lstset{style=numbers, #1}}{%
120− \lstset{style=default, #1}}}{}
121+ \lstset{style=default, #1}}
122+ \singlespacing
123+ }{}
121124%% ---------------------------------------------------------- [ Input Listings ]
122125%% Command to add externally defined Idris code to the document.
123126\newcommand{\inputIdrisListing}[2][]{%
idris.cabal+15−12
@@ -1,5 +1,5 @@
11Name: idris
2−Version: 0.9.13
2+Version: 0.9.13.1
33License: BSD3
44License-file: LICENSE
55Author: Edwin Brady
@@ -100,10 +100,10 @@ Extra-source-files:
100100 libs/effects/Effect/*.idr
101101 libs/effects/*.idr
102102
103− libs/oldeffects/Makefile
104− libs/oldeffects/oldeffects.ipkg
105− libs/oldeffects/Effect/*.idr
106− libs/oldeffects/*.idr
103+ libs/neweffects/Makefile
104+ libs/neweffects/effects.ipkg
105+ libs/neweffects/Effect/*.idr
106+ libs/neweffects/*.idr
107107
108108 llvm/*.c
109109 llvm/Makefile
@@ -131,9 +131,6 @@ Extra-source-files:
131131 test/reg007/run
132132 test/reg007/*.lidr
133133 test/reg007/expected
134− test/reg008/run
135− test/reg008/*.idr
136− test/reg008/expected
137134 test/reg009/run
138135 test/reg009/*.lidr
139136 test/reg009/expected
@@ -237,11 +234,12 @@ Extra-source-files:
237234 test/reg042/run
238235 test/reg042/*.idr
239236 test/reg042/expected
240− test/reg043/run
241− test/reg043/expected
242237 test/reg044/run
243238 test/reg044/*.idr
244239 test/reg044/expected
240+ test/reg045/run
241+ test/reg045/*.idr
242+ test/reg045/expected
245243
246244 test/basic001/run
247245 test/basic001/*.idr
@@ -286,6 +284,9 @@ Extra-source-files:
286284 test/dsl002/test
287285 test/dsl002/*.idr
288286 test/dsl002/expected
287+ test/dsl003/run
288+ test/dsl003/*.idr
289+ test/dsl003/expected
289290
290291 test/effects001/run
291292 test/effects001/*.idr
@@ -513,7 +514,8 @@ Flag release
513514Library
514515 hs-source-dirs: src
515516 Exposed-modules:
516− Idris.Core.CaseTree
517+ Idris.Core.Binary
518+ , Idris.Core.CaseTree
517519 , Idris.Core.Constraints
518520 , Idris.Core.DeepSeq
519521 , Idris.Core.Elaborate
@@ -610,6 +612,7 @@ Library
610612 , annotated-wl-pprint >= 0.5.3
611613 , ansi-terminal
612614 , ansi-wl-pprint
615+ , base64-bytestring
613616 , binary
614617 , blaze-html >= 0.6.1.3
615618 , blaze-markup >= 0.5.2.1 && < 0.7.0.0
@@ -639,7 +642,7 @@ Library
639642 , xml
640643 , deepseq
641644 , zlib
642− , optparse-applicative
645+ , optparse-applicative >= 0.8
643646 Extensions: MultiParamTypeClasses
644647 , FunctionalDependencies
645648 , FlexibleContexts
libs/Makefile+18−2
@@ -2,16 +2,32 @@ build:
22 $(MAKE) -C prelude build
33 $(MAKE) -C base build
44 $(MAKE) -C effects build
5+ $(MAKE) -C neweffects build
56
67
78install:
89 $(MAKE) -C prelude install
910 $(MAKE) -C base install
1011 $(MAKE) -C effects install
12+ $(MAKE) -C neweffects install
1113
1214clean:
1315 $(MAKE) -C prelude clean
1416 $(MAKE) -C base clean
1517 $(MAKE) -C effects clean
16−
17−.PHONY: build install clean
18+ $(MAKE) -C neweffects clean
19+
20+doc:
21+ $(MAKE) -C prelude doc
22+ $(MAKE) -C base doc
23+ $(MAKE) -C effects doc
24+ $(MAKE) -C neweffects doc
25+
26+doc_clean:
27+ $(MAKE) -C prelude doc_clean
28+ $(MAKE) -C base doc_clean
29+ $(MAKE) -C effects doc_clean
30+ $(MAKE) -C neweffects doc_clean
31+
32+
33+.PHONY: build install clean doc doc_clean
libs/base/Data/HVect.idr+5−5
@@ -52,21 +52,21 @@ using (k : Nat, ts : Vect k Type)
5252 shows (x::xs) = show x :: shows xs
5353
5454 instance (Shows k ts) => Show (HVect ts) where
55− show xs = show (shows xs)
55+ show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]"
5656
5757 ||| Extract an arbitrary element of the correct type.
5858 ||| @ t the goal type
59− get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
59+ get : {default tactics { search 100; } p : Elem t ts} -> HVect ts -> t
6060 get {p = Here} (x::xs) = x
6161 get {p = There p'} (x::xs) = get {p = p'} xs
6262
6363 ||| Replace an element with the correct type.
64− put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
64+ put : {default tactics { search 100; } p : Elem t ts} -> t -> HVect ts -> HVect ts
6565 put {p = Here} y (x::xs) = y :: xs
6666 put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
6767
68− ||| Replace an element with the correct type.
69− update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
68+ ||| Update an element with the correct type.
69+ update : {default tactics { search 100; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
7070 update {p = Here} f (x::xs) = f x :: xs
7171 update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
7272
libs/base/Language/Reflection.idr+3−1
@@ -192,8 +192,10 @@ data Tactic = Try Tactic Tactic
192192 -- ^ focus a named hole
193193 | Rewrite TT
194194 -- ^ rewrite using the reflected rep. of a equality proof
195− | Induction TTName
195+ | Induction TT
196196 -- ^ do induction on the particular expression
197+ | Case TT
198+ -- ^ do case analysis on particular expression
197199 | LetTac TTName TT
198200 -- ^ name a reflected term
199201 | LetTacTy TTName TT TT
libs/base/Makefile+10−3
@@ -1,16 +1,23 @@
11IDRIS := idris
2+PKG := base
23
34build:
4− $(IDRIS) --build base.ipkg
5+ $(IDRIS) --build ${PKG}.ipkg
56
67install:
7− $(IDRIS) --install base.ipkg
8+ $(IDRIS) --install ${PKG}.ipkg
89
910clean:
10− $(IDRIS) --clean base.ipkg
11+ $(IDRIS) --clean ${PKG}.ipkg
1112
1213rebuild: clean build
1314
15+doc:
16+ ${IDRIS} --mkdoc ${PKG}.ipkg
17+
18+doc_clean:
19+ rm -rf ${PKG}_doc
20+
1421linecount:
1522 find . -name '*.idr' | xargs wc -l
1623
libs/base/Network/Socket.idr+139−36
@@ -1,10 +1,10 @@
11-- Time to do this properly.
22-- Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
33-- (C) SimonJF, MIT Licensed, 2014
4−module Network.Socket
4+module IdrisNet.Socket
55
66%include C "idris_net.h"
7−%include C "sys/types.h" -- Pushing my luck, might need to re-export everything
7+%include C "sys/types.h"
88%include C "sys/socket.h"
99%include C "netdb.h"
1010
@@ -54,6 +54,12 @@ instance ToCode SocketType where
5454 toCode Datagram = 2
5555 toCode Raw = 3
5656
57+
58+data RecvStructPtr = RSPtr Ptr
59+data RecvfromStructPtr = RFPtr Ptr
60+data BufPtr = BPtr Ptr
61+data SockaddrPtr = SAPtr Ptr
62+
5763-- Protocol Number. Generally good enough to just set it to 0.
5864ProtocolNumber : Type
5965ProtocolNumber = Int
@@ -88,16 +94,35 @@ BACKLOG = 20
8894EAGAIN : Int
8995EAGAIN = 11
9096
91−-- Allocates an amount of memory given by the ByteLength parameter.
92−-- Used to allocate a mutable pointer to be given to the Recv functions.
93−private
94−alloc : ByteLength -> IO Ptr
95−alloc bl = mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
97+-- TODO: Expand to non-string payloads
98+record UDPRecvData : Type where
99+ MkUDPRecvData :
100+ (remote_addr : SocketAddress) ->
101+ (remote_port : Port) ->
102+ (recv_data : String) ->
103+ (data_len : Int) ->
104+ UDPRecvData
105+
106+record UDPAddrInfo : Type where
107+ MkUDPAddrInfo :
108+ (remote_addr : SocketAddress) ->
109+ (remote_port : Port) ->
110+ UDPAddrInfo
96111
97112-- Frees a given pointer
98−private
99−free : Ptr -> IO ()
100−free ptr = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
113+public
114+sock_free : BufPtr -> IO ()
115+sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
116+
117+public
118+sockaddr_free : SockaddrPtr -> IO ()
119+sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
120+
121+-- Allocates an amount of memory given by the ByteLength parameter.
122+-- Used to allocate a mutable pointer to be given to the Recv functions.
123+public
124+sock_alloc : ByteLength -> IO BufPtr
125+sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
101126
102127record Socket : Type where
103128 MkSocket : (descriptor : SocketDescriptor) ->
@@ -123,12 +148,17 @@ socket sf st pn = do
123148close : Socket -> IO ()
124149close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
125150
151+private
152+saString : (Maybe SocketAddress) -> String
153+saString (Just sa) = show sa
154+saString Nothing = ""
155+
126156-- Binds a socket to the given socket address and port.
127157-- Returns 0 on success, an error code otherwise.
128−bind : Socket -> SocketAddress -> Port -> IO Int
158+bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
129159bind sock addr port = do
130160 bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)
131− (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)
161+ (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)
132162 if bind_res == (-1) then -- error
133163 getErrno
134164 else return 0 -- Success
@@ -152,11 +182,10 @@ listen sock = do
152182 else return 0
153183
154184-- Parses a textual representation of an IPv4 address into a SocketAddress
155−private
156185parseIPv4 : String -> SocketAddress
157186parseIPv4 str = case splitted of
158− (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
159− _ => InvalidAddress
187+ (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
188+ _ => InvalidAddress
160189 where toInt' : String -> Integer
161190 toInt' = cast
162191 toInt : String -> Int
@@ -166,32 +195,30 @@ parseIPv4 str = case splitted of
166195
167196
168197-- Retrieves a socket address from a sockaddr pointer
169−private
170−getSockAddr : Ptr -> IO SocketAddress
171−getSockAddr ptr = do
198+getSockAddr : SockaddrPtr -> IO SocketAddress
199+getSockAddr (SAPtr ptr) = do
172200 addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
173− -- FIXME: Is this really a safe assertion? Depends where the Ptr came
174− -- from!
175− assert_total $ case getSocketFamily addr_family_int of
201+ -- putStrLn $ "Addr family int: " ++ (show addr_family_int)
202+ -- ASSUMPTION: Foreign call returns a valid int
203+ assert_total (case getSocketFamily addr_family_int of
176204 Just AF_INET => do
177205 ipv4_addr <- mkForeign (FFun "idrnet_sockaddr_ipv4" [FPtr] FString) ptr
178206 return $ parseIPv4 ipv4_addr
179207 Just AF_INET6 => return IPv6Addr
180− Just AF_UNSPEC => return IPv6Addr -- FIXME: Horrible hack
208+ Just AF_UNSPEC => return InvalidAddress)
181209
182−-- Accepts a connection from a listening socket.
183210accept : Socket -> IO (Either SocketError (Socket, SocketAddress))
184211accept sock = do
185212 -- We need a pointer to a sockaddr structure. This is then passed into
186213 -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
187− sockaddr_ptr <- mkForeign (FFun "idrnet_create_sockaddr" [] FPtr)
214+ sockaddr_ptr <- mkForeign (FFun "idrnet_create_sockaddr" [] FPtr)
188215 accept_res <- mkForeign (FFun "idrnet_accept" [FInt, FPtr] FInt) (descriptor sock) sockaddr_ptr
189216 if accept_res == (-1) then
190217 map Left getErrno
191218 else do
192219 let (MkSocket _ fam ty p_num) = sock
193− sockaddr <- getSockAddr sockaddr_ptr
194− free sockaddr_ptr
220+ sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
221+ sockaddr_free (SAPtr sockaddr_ptr)
195222 return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
196223
197224send : Socket -> String -> IO (Either SocketError ByteLength)
@@ -202,10 +229,12 @@ send sock dat = do
202229 else
203230 return $ Right send_res
204231
205−private
206−freeRecvStruct : Ptr -> IO ()
207−freeRecvStruct p = mkForeign (FFun "idrnet_free_recv_struct" [FPtr] FUnit) p
208232
233+freeRecvStruct : RecvStructPtr -> IO ()
234+freeRecvStruct (RSPtr p) = mkForeign (FFun "idrnet_free_recv_struct" [FPtr] FUnit) p
235+
236+freeRecvfromStruct : RecvfromStructPtr -> IO ()
237+freeRecvfromStruct (RFPtr p) = mkForeign (FFun "idrnet_free_recvfrom_struct" [FPtr] FUnit) p
209238
210239recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
211240recv sock len = do
@@ -215,32 +244,106 @@ recv sock len = do
215244 recv_res <- mkForeign (FFun "idrnet_get_recv_res" [FPtr] FInt) recv_struct_ptr
216245 if recv_res == (-1) then do
217246 errno <- getErrno
218− freeRecvStruct recv_struct_ptr
247+ freeRecvStruct (RSPtr recv_struct_ptr)
219248 return $ Left errno
220249 else
221250 if recv_res == 0 then do
222− freeRecvStruct recv_struct_ptr
251+ freeRecvStruct (RSPtr recv_struct_ptr)
223252 return $ Left 0
224253 else do
225254 payload <- mkForeign (FFun "idrnet_get_recv_payload" [FPtr] FString) recv_struct_ptr
226− freeRecvStruct recv_struct_ptr
255+ freeRecvStruct (RSPtr recv_struct_ptr)
227256 return $ Right (payload, recv_res)
228257
229258
230259-- Sends the data in a given memory location
231−sendBuf : Socket -> Ptr -> ByteLength -> IO (Either SocketError ByteLength)
232−sendBuf sock ptr len = do
260+sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
261+sendBuf sock (BPtr ptr) len = do
233262 send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
234263 if send_res == (-1) then
235264 map Left getErrno
236265 else
237266 return $ Right send_res
238267
239−recvBuf : Socket -> Ptr -> ByteLength -> IO (Either SocketError ByteLength)
240−recvBuf sock ptr len = do
268+recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
269+recvBuf sock (BPtr ptr) len = do
241270 recv_res <- mkForeign (FFun "idrnet_recv_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
242271 if (recv_res == (-1)) then
243272 map Left getErrno
244273 else
245274 return $ Right recv_res
246275
276+sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)
277+sendTo sock addr p dat = do
278+ sendto_res <- mkForeign (FFun "idrnet_sendto" [FInt, FString, FString, FInt, FInt] FInt)
279+ (descriptor sock) dat (show addr) p (toCode $ family sock)
280+ if sendto_res == (-1) then
281+ map Left getErrno
282+ else
283+ return $ Right sendto_res
284+
285+
286+sendToBuf : Socket -> SocketAddress -> Port -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
287+sendToBuf sock addr p (BPtr dat) len = do
288+ sendto_res <- mkForeign (FFun "idrnet_sendto_buf" [FInt, FPtr, FInt, FString, FInt, FInt] FInt)
289+ (descriptor sock) dat len (show addr) p (toCode $ family sock)
290+ if sendto_res == (-1) then
291+ map Left getErrno
292+ else
293+ return $ Right sendto_res
294+
295+
296+foreignGetRecvfromPayload : RecvfromStructPtr -> IO String
297+foreignGetRecvfromPayload (RFPtr p) = mkForeign (FFun "idrnet_get_recvfrom_payload" [FPtr] FString) p
298+
299+foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress
300+foreignGetRecvfromAddr (RFPtr p) = do
301+ sockaddr_ptr <- map SAPtr $ mkForeign (FFun "idrnet_get_recvfrom_sockaddr" [FPtr] FPtr) p
302+ getSockAddr sockaddr_ptr
303+
304+
305+foreignGetRecvfromPort : RecvfromStructPtr -> IO Port
306+foreignGetRecvfromPort (RFPtr p) = do
307+ sockaddr_ptr <- mkForeign (FFun "idrnet_get_recvfrom_sockaddr" [FPtr] FPtr) p
308+ port <- mkForeign (FFun "idrnet_sockaddr_ipv4_port" [FPtr] FInt) sockaddr_ptr
309+ return port
310+
311+recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))
312+recvFrom sock bl = do
313+ recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)
314+ (descriptor sock) bl
315+ let recv_ptr' = RFPtr recv_ptr
316+ if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
317+ map Left getErrno
318+ else do
319+ result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
320+ if result == -1 then do
321+ freeRecvfromStruct recv_ptr'
322+ map Left getErrno
323+ else do
324+ payload <- foreignGetRecvfromPayload recv_ptr'
325+ port <- foreignGetRecvfromPort recv_ptr'
326+ addr <- foreignGetRecvfromAddr recv_ptr'
327+ freeRecvfromStruct recv_ptr'
328+ return $ Right (MkUDPAddrInfo addr port, payload, result)
329+
330+
331+recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrInfo, ByteLength))
332+recvFromBuf sock (BPtr ptr) bl = do
333+ recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl
334+ let recv_ptr' = RFPtr recv_ptr
335+ if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
336+ map Left getErrno
337+ else do
338+ result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
339+ if result == -1 then do
340+ freeRecvfromStruct recv_ptr'
341+ map Left getErrno
342+ else do
343+ port <- foreignGetRecvfromPort recv_ptr'
344+ addr <- foreignGetRecvfromAddr recv_ptr'
345+ freeRecvfromStruct recv_ptr'
346+ return $ Right (MkUDPAddrInfo addr port, result + 1)
347+
348+
349+
libs/base/Providers.idr−9
@@ -11,26 +11,17 @@ data Provider : (a : Type) -> Type where
1111 ||| @ msg the error message
1212 Error : (msg : String) -> Provider a
1313
14− ||| Postulate the goal type
15− Postulate : Provider a
16−
1714-- instances
1815instance Functor Provider where
1916 map f (Provide a) = Provide (f a)
2017 map f (Error err) = Error err
21− map f Postulate = Postulate
2218
2319instance Applicative Provider where
2420 (Provide f) <$> (Provide x) = Provide (f x)
2521 (Provide f) <$> (Error err) = Error err
26− (Provide f) <$> Postulate = Postulate
2722 (Error err) <$> _ = Error err
28− Postulate <$> (Error err) = Error err
29− Postulate <$> _ = Postulate
3023 pure = Provide
3124
32−-- is this correct for Postulate?
3325instance Monad Provider where
3426 (Provide x) >>= f = f x
3527 (Error err) >>= _ = Error err
36− Postulate >>= f = Postulate
libs/effects/Effects.idr+51−30
@@ -10,7 +10,7 @@ import Effect.Default
1010%access public
1111-- ----------------------------------------------------------------- [ Effects ]
1212||| The Effect type describes effectful computations.
13−|||
13+|||
1414||| This type is parameterised by:
1515||| + The input resource.
1616||| + The return type of the computation.
@@ -28,11 +28,11 @@ data EFFECT : Type where
2828||| underlying computation context `m` for execution.
2929class Handler (e : Effect) (m : Type -> Type) where
3030 ||| How to handle the effect.
31− |||
31+ |||
3232 ||| @ r The resource being handled.
3333 ||| @ eff The effect to be applied.
3434 ||| @ k The continuation to pass the result of the effect
35− covering handle : (r : res) -> (eff : e t res resk) ->
35+ covering handle : (r : res) -> (eff : e t res resk) ->
3636 (k : ((x : t) -> resk x -> m a)) -> m a
3737
3838||| Get the resource type (handy at the REPL to find out about an effect)
@@ -48,7 +48,7 @@ resourceType (MkEff t e) = t
4848syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
4949
5050-- The state transition is dependent on a result `b`, a bound variable.
51−syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
51+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
5252 = eff inst (\b => outst)
5353
5454--- A simple state transition
@@ -69,7 +69,7 @@ namespace Env
6969 data Env : (m : Type -> Type) -> List EFFECT -> Type where
7070 Nil : Env m Nil
7171 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
72−
72+
7373data EffElem : Effect -> Type ->
7474 List EFFECT -> Type where
7575 Here : EffElem x a (MkEff a x :: xs)
@@ -130,7 +130,7 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
130130
131131-- ------------------------------------------------- [ The Language of Effects ]
132132||| Definition of an Effect.
133−|||
133+|||
134134||| @ m The computation context
135135||| @ x The return type of the result.
136136||| @ es The list of allowed side-effects.
@@ -142,7 +142,7 @@ data Eff : (m : Type -> Type)
142142 value : a -> Eff m a xs (\v => xs)
143143 with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
144144 Eff m a xs xs'
145− ebind : Eff m a xs xs' ->
145+ ebind : Eff m a xs xs' ->
146146 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
147147 callP : (prf : EffElem e a xs) ->
148148 (eff : e t a b) ->
@@ -151,25 +151,25 @@ data Eff : (m : Type -> Type)
151151 liftP : (prf : SubList ys xs) ->
152152 Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
153153 newInit : Handler e m =>
154− res ->
154+ res ->
155155 Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
156156 Eff m a xs (\v => xs')
157157 catch : Catchable m err =>
158158 Eff m a xs xs' -> (err -> Eff m a xs xs') ->
159159 Eff m a xs xs'
160160
161− (:-) : (l : ty) ->
162− Eff m t [x] xs' -> -- [x] (\v => xs) ->
161+ (:-) : (l : ty) ->
162+ Eff m t [x] xs' -> -- [x] (\v => xs) ->
163163 Eff m t [l ::: x] (\v => map (l :::) (xs' v))
164164
165−(>>=) : Eff m a xs xs' ->
165+(>>=) : Eff m a xs xs' ->
166166 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
167−(>>=) = ebind
167+(>>=) = ebind
168168
169169-- namespace SimpleBind
170−-- (>>=) : Eff m a xs (\v => xs) ->
170+-- (>>=) : Eff m a xs (\v => xs) ->
171171-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
172−-- (>>=) = ebind
172+-- (>>=) = ebind
173173
174174||| Run a subprogram which results in an effect state the same as the input.
175175staticEff : Eff m a xs (\v => xs) -> Eff m a xs (\v => xs)
@@ -192,7 +192,7 @@ pure = 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)
197197(<$>) prog v = do fn <- prog
198198 arg <- v
@@ -215,7 +215,7 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
215215
216216eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
217217eff env (value x) k = k x env
218−eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
218+eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
219219eff env (prog `ebind` c) k
220220 = eff env prog (\p', env' => eff env' (c p') k)
221221eff env (callP prf effP) k = execEff env prf effP k
@@ -249,44 +249,65 @@ syntax MkDefaultEnv = with Env
249249
250250call : {a, b: _} -> {e : Effect} ->
251251 (eff : e t a b) ->
252− {default tactics { search 100; }
253− prf : EffElem e a xs} ->
252+ {auto prf : EffElem e a xs} ->
254253 Eff m t xs (\v => updateResTy v xs prf eff)
255254call e {prf} = callP prf e
256255
257256implicit
258257lift : Eff m t ys ys' ->
259− {default tactics { search 100; }
260− prf : SubList ys xs} ->
258+ {auto prf : SubList ys xs} ->
261259 Eff m t xs (\v => updateWith (ys' v) xs prf)
262260lift e {prf} = liftP prf e
263261
264262
265263new : Handler e m =>
266− {default default r : res} ->
264+ {default default r : res} ->
267265 Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
268266 Eff m a xs (\v => xs')
269267new {r} e = newInit r e
270268
271269-- --------------------------------------------------------- [ Running Effects ]
272270
273−||| Run an effectful program
274−run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
271+||| Run an effectful program.
272+|||
273+||| The content (`m`) in which to run the program is taken from the environment in which the program is called.
274+||| The `env` argument is implicit and initialised automatically.
275+|||
276+||| @prog The effectful program to run.
277+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> (prog : Eff m a xs xs') -> m a
275278run {env} prog = eff env prog (\r, env => pure r)
276279
277−runPure : {default MkDefaultEnv env : Env id xs} -> Eff id a xs xs' -> a
280+||| Run an effectful program in the identity context `id`.
281+|||
282+||| A helper function useful for when the given context is 'pure'.
283+||| The `env` argument is implicit and initialised automatically.
284+|||
285+||| @prog The effectful program to run.
286+runPure : {default MkDefaultEnv env : Env id xs} -> (prog : Eff id a xs xs') -> a
278287runPure {env} prog = eff env prog (\r, env => r)
279288
280−runInit : Applicative m => Env m xs -> Eff m a xs xs' -> m a
289+||| Run an effectful program with a default value for the environment context.
290+|||
291+||| This is useful for when no default value exists for a given resource type.
292+|||
293+||| @val The default value for the resource type.
294+||| @prog The effectful program to run.
295+runInit : Applicative m => (val : Env m xs) -> (prog : Eff m a xs xs') -> m a
281296runInit env prog = eff env prog (\r, env => pure r)
282297
283−runPureInit : Env id xs -> Eff id a xs xs' -> a
298+||| Run an effectful program in the identity context `id` with a given default value for the environment context.
299+|||
300+||| A helper function useful for when the given context is 'pure'.
301+|||
302+||| @val The default value for the resource type.
303+||| @prog The effectful program to run.
304+runPureInit : (val : Env id xs) -> (prog : Eff id a xs xs') -> a
284305runPureInit env prog = eff env prog (\r, env => r)
285306
286307runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a
287308runWith inj env prog = eff env prog (\r, env => inj r)
288309
289−runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
310+runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
290311 m (x : a ** Env m (xs' x))
291312runEnv env prog = eff env prog (\r, env => pure (r ** env))
292313
@@ -297,9 +318,9 @@ mapE f [] = pure []
297318mapE f (x :: xs) = [| f x :: mapE f xs |]
298319
299320
300−mapVE : Applicative m =>
301− (a -> {xs} Eff m b) ->
302− Vect n a ->
321+mapVE : Applicative m =>
322+ (a -> {xs} Eff m b) ->
323+ Vect n a ->
303324 {xs} Eff m (Vect n b)
304325mapVE f [] = pure []
305326mapVE f (x :: xs) = [| f x :: mapVE f xs |]
libs/effects/Makefile+13−5
@@ -1,14 +1,22 @@
1−IDRIS := idris
1+IDRIS := idris
2+
3+PKG := effects
24
35build:
4− $(IDRIS) --build effects.ipkg
6+ $(IDRIS) --build ${PKG}.ipkg
57
68clean:
7− $(IDRIS) --clean effects.ipkg
9+ $(IDRIS) --clean ${PKG}.ipkg
810
911install:
10− $(IDRIS) --install effects.ipkg
12+ $(IDRIS) --install ${PKG}.ipkg
1113
1214rebuild: clean build
1315
14−.PHONY: build clean install rebuild
16+doc:
17+ $(IDRIS) --mkdoc ${PKG}.ipkg
18+
19+doc_clean:
20+ rm -rf ${PKG}_doc
21+
22+.PHONY: build clean install rebuild doc doc_clean
libs/neweffects/Effect/Default.idrnew file+44
@@ -0,0 +1,44 @@
1+module Default
2+
3+class Default a where
4+ default : a
5+
6+instance Default Int where
7+ default = 0
8+
9+instance Default Integer where
10+ default = 0
11+
12+instance Default Float where
13+ default = 0
14+
15+instance Default Nat where
16+ default = 0
17+
18+instance Default Char where
19+ default = '\0'
20+
21+instance Default String where
22+ default = ""
23+
24+instance Default Bool where
25+ default = False
26+
27+instance Default () where
28+ default = ()
29+
30+instance (Default a, Default b) => Default (a, b) where
31+ default = (default, default)
32+
33+instance Default (Maybe a) where
34+ default = Nothing
35+
36+instance Default (List a) where
37+ default = []
38+
39+instance Default a => Default (Vect n a) where
40+ default = mkDef _ where
41+ mkDef : (n : Nat) -> Vect n a
42+ mkDef Z = []
43+ mkDef (S k) = default :: mkDef k
44+
libs/oldeffects/Effect/Exception.idr → libs/neweffects/Effect/Exception.idrrenamed+7−5
@@ -4,12 +4,15 @@ import Effects
44import System
55import Control.IOExcept
66
7−data Exception : Type -> Type -> Type -> Type -> Type where
8− Raise : a -> Exception a () () b
7+data Exception : Type -> Effect where
8+ Raise : a -> { () } Exception a b
99
1010instance Handler (Exception a) Maybe where
1111 handle _ (Raise e) k = Nothing
1212
13+instance Handler (Exception a) List where
14+ handle _ (Raise e) k = []
15+
1316instance Show a => Handler (Exception a) IO where
1417 handle _ (Raise e) k = do print e
1518 believe_me (exit 1)
@@ -23,9 +26,8 @@ instance Handler (Exception a) (Either a) where
2326EXCEPTION : Type -> EFFECT
2427EXCEPTION t = MkEff () (Exception t)
2528
26−raise : a -> Eff m [EXCEPTION a] b
27−raise err = Raise err
28−
29+raise : a -> { [EXCEPTION a ] } Eff b
30+raise err = call $ Raise err
2931
3032
3133
libs/neweffects/Effect/File.idrnew file+128
@@ -0,0 +1,128 @@
1+-- -------------------------------------------------------- [ Effectful FileIO ]
2+module Effect.File
3+
4+import Effects
5+import Control.IOExcept
6+
7+
8+||| A Dependent type to describe File Handles. File handles are
9+||| parameterised with the current state of the file: Closed; Open for
10+||| reading; and Open for writing.
11+|||
12+||| @ m The file mode.
13+data OpenFile : (m : Mode) -> Type where
14+ FH : File -> OpenFile m
15+
16+openOK : Mode -> Bool -> Type
17+openOK m True = OpenFile m
18+openOK m False = ()
19+
20+-- ------------------------------------------------------------ [ The Protocol ]
21+
22+||| Here the protocol for resource access is defined as an effect.
23+||| The state transitions diagram for the protocol is as follows:
24+|||
25+||| digraph G {
26+|||
27+||| empty; read; write; // States
28+|||
29+||| empty -> read [label="Open R"];
30+||| read -> empty [label="Close"];
31+||| read -> read [label="ReadLine"];
32+||| read -> read [label="EOF"];
33+|||
34+||| empty -> write [label="Open W"];
35+||| write -> empty [label="Close"];
36+||| write -> write [label="WriteLine"];
37+|||
38+||| }
39+data FileIO : Effect where
40+ ||| Open a file with the specified mode.
41+ |||
42+ ||| Opening a file successful moves the state from 'empty' to the
43+ ||| specified mode. If not successful the state is still 'empty'.
44+ |||
45+ ||| @ fname The file name to be opened.
46+ ||| @ m The file mode.
47+ Open : (fname: String)
48+ -> (m : Mode)
49+ -> {() ==> {res} if res
50+ then OpenFile m
51+ else ()} FileIO Bool
52+
53+ ||| Close a file.
54+ |||
55+ ||| Closing a file moves the state from Open to closed.
56+ Close : {OpenFile m ==> ()} FileIO ()
57+
58+ ||| Read a line from the file.
59+ |||
60+ ||| Only files that are open for reading can be read.
61+ ReadLine : {OpenFile Read} FileIO String
62+
63+ ||| Write a line to a file.
64+ |||
65+ ||| Only file that are open for writing can be written to.
66+ WriteLine : String -> {OpenFile Write} FileIO ()
67+
68+ ||| End of file?
69+ |||
70+ ||| Only files open for reading can be tested for EOF
71+ EOF : {OpenFile Read} FileIO Bool
72+
73+-- ------------------------------------------------------------ [ The Handlers ]
74+
75+--- An implementation of the resource access protocol for the IO Context.
76+instance Handler FileIO IO where
77+ handle () (Open fname m) k = do h <- openFile fname m
78+ valid <- validFile h
79+ if valid then k True (FH h)
80+ else k False ()
81+ handle (FH h) Close k = do closeFile h
82+ k () ()
83+ handle (FH h) ReadLine k = do str <- fread h
84+ k str (FH h)
85+ handle (FH h) (WriteLine str) k = do fwrite h str
86+ k () (FH h)
87+ handle (FH h) EOF k = do e <- feof h
88+ k e (FH h)
89+
90+-- -------------------------------------------------------------- [ The Effect ]
91+FILE_IO : Type -> EFFECT
92+FILE_IO t = MkEff t FileIO
93+
94+-- ------------------------------------------------------------ [ The Bindings ]
95+--
96+-- Bind the IO context handlers to functions. These functions will run
97+-- in the IO context.
98+--
99+
100+||| Open a file with the specified mode.
101+|||
102+||| @ fname The file name to be opened.
103+||| @ m The file mode.
104+open : (fname : String)
105+ -> (m : Mode)
106+ -> { [FILE_IO ()] ==> [FILE_IO (if result
107+ then OpenFile m
108+ else ())] } Eff Bool
109+open f m = call $ Open f m
110+
111+
112+||| Close a file.
113+close : { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff ()
114+close = call $ Close
115+
116+||| Read a line from the file.
117+readLine : { [FILE_IO (OpenFile Read)] } Eff String
118+readLine = call $ ReadLine
119+
120+||| Write a line to a file.
121+writeLine : String -> { [FILE_IO (OpenFile Write)] } Eff ()
122+writeLine str = call $ WriteLine str
123+
124+||| End of file?
125+eof : { [FILE_IO (OpenFile Read)] } Eff Bool
126+eof = call $ EOF
127+
128+-- --------------------------------------------------------------------- [ EOF ]
libs/oldeffects/Effect/Memory.idr → libs/neweffects/Effect/Memory.idrrenamed+38−32
@@ -12,29 +12,30 @@ data MemoryChunk : Nat -> Nat -> Type where
1212abstract
1313data RawMemory : Effect where
1414 Allocate : (n : Nat) ->
15− RawMemory () (MemoryChunk n 0) ()
16− Free : RawMemory (MemoryChunk n i) () ()
15+ RawMemory () () (\v => MemoryChunk n 0)
16+ Free : RawMemory () (MemoryChunk n i) (\v => ())
1717 Initialize : Bits8 ->
1818 (size : Nat) ->
1919 so (i + size <= n) ->
20− RawMemory (MemoryChunk n i) (MemoryChunk n (i + size)) ()
20+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))
2121 Peek : (offset : Nat) ->
2222 (size : Nat) ->
2323 so (offset + size <= i) ->
24− RawMemory (MemoryChunk n i) (MemoryChunk n i) (Vect size Bits8)
24+ RawMemory (Vect size Bits8)
25+ (MemoryChunk n i) (\v => MemoryChunk n i)
2526 Poke : (offset : Nat) ->
2627 (Vect size Bits8) ->
2728 so (offset <= i && offset + size <= n) ->
28− RawMemory (MemoryChunk n i) (MemoryChunk n (max i (offset + size))) ()
29+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
2930 Move : (src : MemoryChunk src_size src_init) ->
3031 (dst_offset : Nat) ->
3132 (src_offset : Nat) ->
3233 (size : Nat) ->
3334 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
3435 so (src_offset + size <= src_init) ->
35− RawMemory (MemoryChunk dst_size dst_init)
36− (MemoryChunk dst_size (max dst_init (dst_offset + size))) ()
37− GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (MemoryChunk n i)
36+ RawMemory () (MemoryChunk dst_size dst_init)
37+ (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
38+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
3839
3940private
4041do_malloc : Nat -> IOExcept String Ptr
@@ -79,58 +80,61 @@ do_poke ptr offset (b::bs)
7980instance Handler RawMemory (IOExcept String) where
8081 handle () (Allocate n) k
8182 = do ptr <- do_malloc n
82− k (CH ptr) ()
83− handle (CH ptr) (Initialize {i} c size _) k
84− = ioe_lift (do_memset ptr i c size) $> k (CH ptr) ()
83+ k () (CH ptr)
84+ handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k
85+ = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)
8586 handle (CH ptr) (Free) k
8687 = ioe_lift (do_free ptr) $> k () ()
8788 handle (CH ptr) (Peek offset size _) k
8889 = do res <- ioe_lift (do_peek ptr offset size)
89− k (CH ptr) res
90+ k res (CH ptr)
9091 handle (CH ptr) (Poke offset content _) k
9192 = do ioe_lift (do_poke ptr offset content)
92− k (CH ptr) ()
93+ k () (CH ptr)
9394 handle (CH dest_ptr) (Move (CH src_ptr) dest_offset src_offset size _ _) k
9495 = do ioe_lift (do_memmove dest_ptr src_ptr dest_offset src_offset size)
95− k (CH dest_ptr) ()
96+ k () (CH dest_ptr)
9697 handle chunk (GetRawPtr) k
9798 = k chunk chunk
9899
99100RAW_MEMORY : Type -> EFFECT
100101RAW_MEMORY t = MkEff t RawMemory
101102
102−allocate : (n : Nat) -> EffM m [RAW_MEMORY ()] [RAW_MEMORY (MemoryChunk n 0)] ()
103−allocate size = Allocate size
103+allocate : (n : Nat) ->
104+ Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
105+allocate size = call $ Allocate size
104106
105107initialize : {i : Nat} ->
106108 {n : Nat} ->
107109 Bits8 ->
108110 (size : Nat) ->
109111 so (i + size <= n) ->
110− EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (i + size))] ()
111−initialize c size prf = Initialize c size prf
112+ Eff () [RAW_MEMORY (MemoryChunk n i)]
113+ (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
114+initialize c size prf = call $ Initialize c size prf
112115
113−free : EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY ()] ()
114−free = Free
116+free : Eff () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])
117+free = call Free
115118
116119peek : {i : Nat} ->
117120 (offset : Nat) ->
118121 (size : Nat) ->
119122 so (offset + size <= i) ->
120− Eff m [RAW_MEMORY (MemoryChunk n i)] (Vect size Bits8)
121−peek offset size prf = Peek offset size prf
123+ { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
124+peek offset size prf = call $ Peek offset size prf
122125
123126poke : {n : Nat} ->
124127 {i : Nat} ->
125128 (offset : Nat) ->
126129 Vect size Bits8 ->
127130 so (offset <= i && offset + size <= n) ->
128− EffM m [RAW_MEMORY (MemoryChunk n i)] [RAW_MEMORY (MemoryChunk n (max i (offset + size)))] ()
129−poke offset content prf = Poke offset content prf
131+ Eff () [RAW_MEMORY (MemoryChunk n i)]
132+ (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
133+poke offset content prf = call $ Poke offset content prf
130134
131135private
132−getRawPtr : Eff m [RAW_MEMORY (MemoryChunk n i)] (MemoryChunk n i)
133−getRawPtr = GetRawPtr
136+getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
137+getRawPtr = call $ GetRawPtr
134138
135139private
136140move' : {dst_size : Nat} ->
@@ -142,10 +146,10 @@ move' : {dst_size : Nat} ->
142146 (size : Nat) ->
143147 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
144148 so (src_offset + size <= src_init) ->
145− EffM m [RAW_MEMORY (MemoryChunk dst_size dst_init)]
146− [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))] ()
149+ Eff () [RAW_MEMORY (MemoryChunk dst_size dst_init)]
150+ (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])
147151move' src_ptr dst_offset src_offset size dst_bounds src_bounds
148− = Move src_ptr dst_offset src_offset size dst_bounds src_bounds
152+ = call $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds
149153
150154data MoveDescriptor = Dst | Src
151155
@@ -158,10 +162,12 @@ move : {dst_size : Nat} ->
158162 (size : Nat) ->
159163 so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
160164 so (src_offset + size <= src_init) ->
161− EffM m [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)
165+ Eff ()
166+ [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)
162167 , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]
163− [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))
164− , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)] ()
168+ (\v =>
169+ [ Dst ::: RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))
170+ , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)])
165171move dst_offset src_offset size dst_bounds src_bounds
166172 = do src_ptr <- Src :- getRawPtr
167173 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
libs/oldeffects/Effect/Monad.idr → libs/neweffects/Effect/Monad.idrrenamed+4−4
@@ -5,17 +5,17 @@ import Effects
55-- Eff is a monad too, so we can happily use it in a monad transformer.
66
77using (xs : List EFFECT, m : Type -> Type)
8− instance Functor (EffM m xs xs) where
8+ instance Functor (\a => EffM m a xs (\v => xs)) where
99 map f prog = do t <- prog
1010 value (f t)
1111
12− instance Applicative (EffM m xs xs) where
12+ instance Applicative (\a => EffM m a xs (\v => xs)) where
1313 pure = value
1414 (<$>) f a = do f' <- f
1515 a' <- a
1616 value (f' a')
1717
18− instance Monad (EffM m xs xs) where
19− (>>=) = ebind
18+ instance Monad (\a => Eff m a xs (\v => xs)) where
19+ (>>=) = Effects.(>>=)
2020
2121
libs/neweffects/Effect/Random.idrnew file+47
@@ -0,0 +1,47 @@
1+module Effect.Random
2+
3+import Effects
4+
5+data Random : Effect where
6+ getRandom : { Integer } Random Integer
7+ setSeed : Integer -> { Integer } Random ()
8+
9+using (m : Type -> Type)
10+ instance Handler Random m where
11+ handle seed getRandom k
12+ = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in
13+ k seed' seed'
14+ handle seed (setSeed n) k = k () n
15+
16+RND : EFFECT
17+RND = MkEff Integer Random
18+
19+||| Generates a random Integer in a given range
20+rndInt : Integer -> Integer -> { [RND] } Eff Integer
21+rndInt lower upper = do v <- call $ getRandom
22+ return (v `prim__sremBigInt` (upper - lower) + lower)
23+
24+||| Generate a random number in Fin (S `k`)
25+|||
26+||| Note that rndFin k takes values 0, 1, ..., k.
27+rndFin : (k : Nat) -> { [RND] } Eff (Fin (S k))
28+rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))
29+ return (toFin v)
30+ where toFin : Integer -> Fin (S k)
31+ toFin x = case integerToFin x (S k) of
32+ Just v => v
33+ Nothing => toFin (assert_smaller x (x - cast (S k)))
34+
35+||| Select a random element from a vector
36+rndSelect' : Vect (S k) a -> { [RND] } Eff a
37+rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)
38+
39+||| Select a random element from a list, or Nothing if the list is empty
40+rndSelect : List a -> { [RND] } Eff (Maybe a)
41+rndSelect [] = return Nothing
42+rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))
43+
44+||| Sets the random seed
45+srand : Integer -> { [RND] } Eff ()
46+srand n = call $ setSeed n
47+
libs/oldeffects/Effect/Select.idr → libs/neweffects/Effect/Select.idrrenamed+5−5
@@ -3,21 +3,21 @@ module Effect.Select
33import Effects
44
55data Selection : Effect where
6− Select : List a -> Selection () () a
6+ Select : List a -> { () } Selection a
77
88instance Handler Selection Maybe where
99 handle _ (Select xs) k = tryAll xs where
1010 tryAll [] = Nothing
11− tryAll (x :: xs) = case k () x of
11+ tryAll (x :: xs) = case k x () of
1212 Nothing => tryAll xs
1313 Just v => Just v
1414
1515instance Handler Selection List where
16− handle r (Select xs) k = concatMap (k r) xs
16+ handle r (Select xs) k = concatMap (\x => k x r) xs
1717
1818SELECT : EFFECT
1919SELECT = MkEff () Selection
2020
21−select : List a -> Eff m [SELECT] a
22−select xs = Select xs
21+select : List a -> { [SELECT] } Eff a
22+select xs = call $ Select xs
2323
libs/oldeffects/Effect/State.idr → libs/neweffects/Effect/State.idrrenamed+12−12
@@ -5,33 +5,33 @@ import Effects
55%access public
66
77data State : Effect where
8− Get : State a a a
9− Put : b -> State a b ()
8+ Get : { a } State a
9+ Put : b -> { a ==> b } State ()
1010
1111using (m : Type -> Type)
1212 instance Handler State m where
1313 handle st Get k = k st st
14− handle st (Put n) k = k n ()
14+ handle st (Put n) k = k () n
1515
1616STATE : Type -> EFFECT
1717STATE t = MkEff t State
1818
19−get : Eff m [STATE x] x
20−get = Get
19+get : { [STATE x] } Eff x
20+get = call $ Get
2121
22−put : x -> Eff m [STATE x] ()
23−put val = Put val
22+put : x -> { [STATE x] } Eff ()
23+put val = call $ Put val
2424
25−putM : y -> EffM m [STATE x] [STATE y] ()
26−putM val = Put val
25+putM : y -> { [STATE x] ==> [STATE y] } Eff ()
26+putM val = call $ Put val
2727
28−update : (x -> x) -> Eff m [STATE x] ()
28+update : (x -> x) -> { [STATE x] } Eff ()
2929update f = put (f !get)
3030
31−updateM : (x -> y) -> EffM m [STATE x] [STATE y] ()
31+updateM : (x -> y) -> { [STATE x] ==> [STATE y] } Eff ()
3232updateM f = putM (f !get)
3333
34−locally : x -> Eff m [STATE x] t -> Eff m [STATE y] t
34+locally : x -> ({ [STATE x] } Eff t) -> { [STATE y] } Eff t
3535locally newst prog = do st <- get
3636 putM newst
3737 val <- prog
libs/neweffects/Effect/StdIO.idrnew file+60
@@ -0,0 +1,60 @@
1+module Effect.StdIO
2+
3+import Effects
4+import Control.IOExcept
5+
6+-------------------------------------------------------------
7+-- IO effects internals
8+-------------------------------------------------------------
9+
10+||| The internal representation of StdIO effects
11+data StdIO : Effect where
12+ PutStr : String -> { () } StdIO ()
13+ GetStr : { () } StdIO String
14+ PutCh : Char -> { () } StdIO ()
15+ GetCh : { () } StdIO Char
16+
17+
18+-------------------------------------------------------------
19+-- IO effects handlers
20+-------------------------------------------------------------
21+
22+instance Handler StdIO IO where
23+ handle () (PutStr s) k = do putStr s; k () ()
24+ handle () GetStr k = do x <- getLine; k x ()
25+ handle () (PutCh c) k = do putChar c; k () ()
26+ handle () GetCh k = do x <- getChar; k x ()
27+
28+instance Handler StdIO (IOExcept a) where
29+ handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()
30+ handle () GetStr k = do x <- ioe_lift $ getLine; k x ()
31+ handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
32+ handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
33+
34+-------------------------------------------------------------
35+--- The Effect and associated functions
36+-------------------------------------------------------------
37+
38+STDIO : EFFECT
39+STDIO = MkEff () StdIO
40+
41+||| Write a string to standard output.
42+putStr : String -> { [STDIO] } Eff ()
43+putStr s = call $ PutStr s
44+
45+||| Write a character to standard output.
46+putChar : Char -> { [STDIO] } Eff ()
47+putChar c = call $ PutCh c
48+
49+||| Write a string to standard output, terminating with a newline.
50+putStrLn : String -> { [STDIO] } Eff ()
51+putStrLn s = putStr (s ++ "\n")
52+
53+||| Read a string from standard input.
54+getStr : { [STDIO] } Eff String
55+getStr = call $ GetStr
56+
57+||| Read a character from standard input.
58+getChar : { [STDIO] } Eff Char
59+getChar = call $ GetCh
60+
libs/neweffects/Effect/System.idrnew file+38
@@ -0,0 +1,38 @@
1+module Effect.System
2+
3+-- Various system interaction features (this is not necessarily the right way
4+-- to split them up, I just need some of them now :))
5+
6+import Effects
7+import System
8+import Control.IOExcept
9+
10+data System : Effect where
11+ Args : { () } System (List String)
12+ Time : { () } System Int
13+ GetEnv : String -> { () } System (Maybe String)
14+
15+instance Handler System IO where
16+ handle () Args k = do x <- getArgs; k x ()
17+ handle () Time k = do x <- time; k x ()
18+ handle () (GetEnv s) k = do x <- getEnv s; k x ()
19+
20+instance Handler System (IOExcept a) where
21+ handle () Args k = do x <- ioe_lift getArgs; k x ()
22+ handle () Time k = do x <- ioe_lift time; k x ()
23+ handle () (GetEnv s) k = do x <- ioe_lift $ getEnv s; k x ()
24+
25+--- The Effect and associated functions
26+
27+SYSTEM : EFFECT
28+SYSTEM = MkEff () System
29+
30+getArgs : { [SYSTEM] } Eff (List String)
31+getArgs = call Args
32+
33+time : { [SYSTEM] } Eff Int
34+time = call Time
35+
36+getEnv : String -> { [SYSTEM] } Eff (Maybe String)
37+getEnv s = call $ GetEnv s
38+
libs/neweffects/Effects.idrnew file+292
@@ -0,0 +1,292 @@
1+module Effects
2+
3+import Language.Reflection
4+import Control.Catchable
5+import Effect.Default
6+
7+--- Effectful computations are described as algebraic data types that
8+--- explain how an effect is interpreted in some underlying context.
9+
10+%access public
11+-- ----------------------------------------------------------------- [ Effects ]
12+||| The Effect type describes effectful computations.
13+|||
14+||| This type is parameterised by:
15+||| + The input resource.
16+||| + The return type of the computation.
17+||| + The computation to run on the resource.
18+Effect : Type
19+Effect = (x : Type) -> Type -> (x -> Type) -> Type
20+
21+||| The `EFFECT` Data type describes how to promote the Effect
22+||| description into a concrete effect.
23+%error_reverse
24+data EFFECT : Type where
25+ MkEff : Type -> Effect -> EFFECT
26+
27+||| Handler classes describe how an effect `e` is translated to the
28+||| underlying computation context `m` for execution.
29+class Handler (e : Effect) (m : Type -> Type) where
30+ ||| How to handle the effect.
31+ |||
32+ ||| @ r The resource being handled.
33+ ||| @ eff The effect to be applied.
34+ ||| @ k The continuation to pass the result of the effect
35+ covering handle : (r : res) -> (eff : e t res resk) ->
36+ (k : ((x : t) -> resk x -> m a)) -> m a
37+
38+||| Get the resource type (handy at the REPL to find out about an effect)
39+resourceType : EFFECT -> Type
40+resourceType (MkEff t e) = t
41+
42+-- --------------------------------------------------------- [ Syntactic Sugar ]
43+
44+-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
45+-- up to a small number of parameters...)
46+
47+-- No state transition
48+syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
49+
50+-- The state transition is dependent on a result `b`, a bound variable.
51+syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
52+ = eff inst (\b => outst)
53+
54+--- A simple state transition
55+syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
56+
57+-- --------------------------------------- [ Properties and Proof Construction ]
58+using (xs : List a, ys : List a)
59+ data SubList : List a -> List a -> Type where
60+ SubNil : SubList {a} [] []
61+ Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
62+ Drop : SubList xs ys -> SubList xs (x :: ys)
63+
64+ subListId : SubList xs xs
65+ subListId {xs = Nil} = SubNil
66+ subListId {xs = x :: xs} = Keep subListId
67+
68+namespace Env
69+ data Env : (m : Type -> Type) -> List EFFECT -> Type where
70+ Nil : Env m Nil
71+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
72+
73+data EffElem : Effect -> Type ->
74+ List EFFECT -> Type where
75+ Here : EffElem x a (MkEff a x :: xs)
76+ There : EffElem x a xs -> EffElem x a (y :: xs)
77+
78+||| make an environment corresponding to a sub-list
79+dropEnv : Env m ys -> SubList xs ys -> Env m xs
80+dropEnv [] SubNil = []
81+dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
82+dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
83+
84+updateWith : (ys' : List a) -> (xs : List a) ->
85+ SubList ys xs -> List a
86+updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
87+updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
88+updateWith [] [] SubNil = []
89+updateWith (y :: ys) [] SubNil = y :: ys
90+updateWith [] (x :: xs) (Keep rest) = []
91+
92+||| Put things back, replacing old with new in the sub-environment
93+rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
94+ Env m xs -> Env m (updateWith ys' xs prf)
95+rebuildEnv [] SubNil env = env
96+rebuildEnv (x :: xs) SubNil env = x :: xs
97+rebuildEnv [] (Keep rest) (y :: env) = []
98+rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
99+rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
100+
101+
102+-- -------------------------------------------------- [ The Effect EDSL itself ]
103+
104+updateResTy : (val : t) ->
105+ (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
106+ List EFFECT
107+updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
108+updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
109+
110+infix 5 :::, :-, :=
111+
112+data LRes : lbl -> Type -> Type where
113+ (:=) : (x : lbl) -> res -> LRes x res
114+
115+(:::) : lbl -> EFFECT -> EFFECT
116+(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e
117+
118+using (lbl : Type)
119+ instance Default a => Default (LRes lbl a) where
120+ default = lbl := default
121+
122+private
123+unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
124+unlabel {m} {x = MkEff a eff} [l := v] = [v]
125+
126+private
127+relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
128+relabel {xs = []} l [] = []
129+relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
130+
131+-- ------------------------------------------------- [ The Language of Effects ]
132+||| Definition of a language of effectful programs.
133+|||
134+||| @ x The return type of the result.
135+||| @ es The list of allowed side-effects.
136+||| @ ce Function to compute a new list of allowed side-effects.
137+data Eff : (x : Type)
138+ -> (es : List EFFECT)
139+ -> (ce : x -> List EFFECT) -> Type where
140+ value : a -> Eff a xs (\v => xs)
141+ with_val : (val : a) -> Eff () xs (\v => xs' val) ->
142+ Eff a xs xs'
143+ ebind : Eff a xs xs' ->
144+ ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
145+ callP : (prf : EffElem e a xs) ->
146+ (eff : e t a b) ->
147+ Eff t xs (\v => updateResTy v xs prf eff)
148+
149+ liftP : (prf : SubList ys xs) ->
150+ Eff t ys ys' -> Eff t xs (\v => updateWith (ys' v) xs prf)
151+
152+ (:-) : (l : ty) ->
153+ Eff t [x] xs' -> -- [x] (\v => xs) ->
154+ Eff t [l ::: x] (\v => map (l :::) (xs' v))
155+
156+(>>=) : Eff a xs xs' ->
157+ ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
158+(>>=) = ebind
159+
160+-- namespace SimpleBind
161+-- (>>=) : Eff m a xs (\v => xs) ->
162+-- ((val : a) -> Eff m b xs xs') -> Eff m b xs xs'
163+-- (>>=) = ebind
164+
165+||| Run a subprogram which results in an effect state the same as the input.
166+staticEff : Eff a xs (\v => xs) -> Eff a xs (\v => xs)
167+staticEff = id
168+
169+||| Explicitly give the expected set of result effects for an effectful
170+||| operation.
171+toEff : .(xs' : List EFFECT) -> Eff a xs (\v => xs') -> Eff a xs (\v => xs')
172+toEff xs' = id
173+
174+return : a -> Eff a xs (\v => xs)
175+return x = value x
176+
177+-- ------------------------------------------------------ [ for idiom brackets ]
178+
179+infixl 2 <$>
180+
181+pure : a -> Eff a xs (\v => xs)
182+pure = value
183+
184+syntax pureM [val] = with_val val (pure ())
185+
186+(<$>) : Eff (a -> b) xs (\v => xs) ->
187+ Eff a xs (\v => xs) -> Eff b xs (\v => xs)
188+(<$>) prog v = do fn <- prog
189+ arg <- v
190+ return (fn arg)
191+
192+-- ---------------------------------------------------------- [ an interpreter ]
193+
194+private
195+execEff : Env m xs -> (p : EffElem e res xs) ->
196+ (eff : e a res resk) ->
197+ ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
198+execEff (val :: env) Here eff' k
199+ = handle val eff' (\v, res => k v (res :: env))
200+-- FIXME: Teach the elaborator to propagate parameters here
201+execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
202+ = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))
203+
204+-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
205+-- updates can be propagated even through failing computations?
206+
207+eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
208+eff env (value x) k = k x env
209+eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
210+eff env (prog `ebind` c) k
211+ = eff env prog (\p', env' => eff env' (c p') k)
212+eff env (callP prf effP) k = execEff env prf effP k
213+eff env (liftP prf effP) k
214+ = let env' = dropEnv env prf in
215+ eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
216+-- FIXME:
217+-- xs is needed explicitly because otherwise the pattern binding for
218+-- 'l' appears too late. Solution seems to be to reorder patterns at the
219+-- end so that everything is in scope when it needs to be.
220+eff {xs = [l ::: x]} env (l :- prog) k
221+ = let env' = unlabel env in
222+ eff env' prog (\p', envk => k p' (relabel l envk))
223+
224+-- yuck :) Haven't got type class instances working nicely in tactic
225+-- proofs yet, and 'search' can't be told about any hints yet,
226+-- so just brute force it.
227+syntax MkDefaultEnv = with Env
228+ (| [], [default], [default, default],
229+ [default, default, default],
230+ [default, default, default, default],
231+ [default, default, default, default, default],
232+ [default, default, default, default, default, default],
233+ [default, default, default, default, default, default, default],
234+ [default, default, default, default, default, default, default, default] |)
235+
236+call : {a, b: _} -> {e : Effect} ->
237+ (eff : e t a b) ->
238+ {default tactics { search 100; }
239+ prf : EffElem e a xs} ->
240+ Eff t xs (\v => updateResTy v xs prf eff)
241+call e {prf} = callP prf e
242+
243+implicit
244+lift : Eff t ys ys' ->
245+ {default tactics { search 100; }
246+ prf : SubList ys xs} ->
247+ Eff t xs (\v => updateWith (ys' v) xs prf)
248+lift e {prf} = liftP prf e
249+
250+
251+-- --------------------------------------------------------- [ Running Effects ]
252+
253+||| Run an effectful program
254+run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff a xs xs' -> m a
255+run {env} prog = eff env prog (\r, env => pure r)
256+
257+runPure : {default MkDefaultEnv env : Env id xs} -> Eff a xs xs' -> a
258+runPure {env} prog = eff env prog (\r, env => r)
259+
260+runInit : Applicative m => Env m xs -> Eff a xs xs' -> m a
261+runInit env prog = eff env prog (\r, env => pure r)
262+
263+runPureInit : Env id xs -> Eff a xs xs' -> a
264+runPureInit env prog = eff env prog (\r, env => r)
265+
266+runWith : (a -> m a) -> Env m xs -> Eff a xs xs' -> m a
267+runWith inj env prog = eff env prog (\r, env => inj r)
268+
269+runEnv : Applicative m => Env m xs -> Eff a xs xs' ->
270+ m (x : a ** Env m (xs' x))
271+runEnv env prog = eff env prog (\r, env => pure (r ** env))
272+
273+-- ----------------------------------------------- [ some higher order things ]
274+
275+mapE : Applicative m => (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
276+mapE f [] = pure []
277+mapE f (x :: xs) = [| f x :: mapE f xs |]
278+
279+
280+mapVE : Applicative m =>
281+ (a -> {xs} Eff b) ->
282+ Vect n a ->
283+ {xs} Eff (Vect n b)
284+mapVE f [] = pure []
285+mapVE f (x :: xs) = [| f x :: mapVE f xs |]
286+
287+
288+when : Applicative m => Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
289+when True e = Force e
290+when False e = pure ()
291+
292+-- --------------------------------------------------------------------- [ EOF ]
libs/oldeffects/Makefile → libs/neweffects/Makefilerenamed+3−3
@@ -1,13 +1,13 @@
11IDRIS := idris
22
33build:
4− $(IDRIS) --build oldeffects.ipkg
4+ $(IDRIS) --build effects.ipkg
55
66clean:
7− $(IDRIS) --clean oldeffects.ipkg
7+ $(IDRIS) --clean effects.ipkg
88
99install:
10− $(IDRIS) --install oldeffects.ipkg
10+ $(IDRIS) --install effects.ipkg
1111
1212rebuild: clean build
1313
libs/oldeffects/oldeffects.ipkg → libs/neweffects/effects.ipkgrenamed+4−3
@@ -1,8 +1,9 @@
1−package oldeffects
1+package neweffects
22
33opts = "--nobasepkgs -i ../prelude -i ../base"
4−modules = Effects,
4+modules = Effects, Effect.Default,
5+
56 Effect.Exception, Effect.File, Effect.State,
67 Effect.Random, Effect.StdIO, Effect.Select,
7− Effect.Memory, Effect.Monad
8+ Effect.Memory, Effect.System
89
libs/oldeffects/Effect/File.idrdeleted−69
@@ -1,69 +0,0 @@
1−module Effect.File
2−
3−import Effects
4−import Control.IOExcept
5−
6−data OpenFile : Mode -> Type where
7− FH : File -> OpenFile m
8−
9−data FileIO : Effect where
10− Open : String -> (m : Mode) -> FileIO () (Either () (OpenFile m)) Bool
11− Close : FileIO (OpenFile m) () ()
12−
13− ReadLine : FileIO (OpenFile Read) (OpenFile Read) String
14− WriteLine : String -> FileIO (OpenFile Write) (OpenFile Write) ()
15− EOF : FileIO (OpenFile Read) (OpenFile Read) Bool
16−
17−
18−instance Handler FileIO IO where
19− handle () (Open fname m) k = do h <- openFile fname m
20− valid <- validFile h
21− if valid then k (Right (FH h)) True
22− else k (Left ()) False
23− handle (FH h) Close k = do closeFile h
24− k () ()
25− handle (FH h) ReadLine k = do str <- fread h
26− k (FH h) str
27− handle (FH h) (WriteLine str) k = do fwrite h str
28− k (FH h) ()
29− handle (FH h) EOF k = do e <- feof h
30− k (FH h) e
31−
32−instance Handler FileIO (IOExcept String) where
33− handle () (Open fname m) k
34− = do h <- ioe_lift (openFile fname m)
35− valid <- ioe_lift (validFile h)
36− if valid then k (Right (FH h)) True
37− else k (Left ()) False
38− handle (FH h) Close k = do ioe_lift (closeFile h); k () ()
39− handle (FH h) ReadLine k = do str <- ioe_lift (fread h)
40− k (FH h) str
41− handle (FH h) (WriteLine str) k = do ioe_lift (fwrite h str)
42− k (FH h) ()
43− handle (FH h) EOF k = do e <- ioe_lift (feof h)
44− k (FH h) e
45−
46−FILE_IO : Type -> EFFECT
47−FILE_IO t = MkEff t FileIO
48−
49−open : Handler FileIO e =>
50− String -> (m : Mode) -> EffM e [FILE_IO ()]
51− [FILE_IO (Either () (OpenFile m))] Bool
52−open f m = Open f m
53−
54−close : Handler FileIO e =>
55− EffM e [FILE_IO (OpenFile m)] [FILE_IO ()] ()
56−close = Close
57−
58−readLine : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] String
59−readLine = ReadLine
60−
61−writeLine : Handler FileIO e => String -> Eff e [FILE_IO (OpenFile Write)] ()
62−writeLine str = WriteLine str
63−
64−eof : Handler FileIO e => Eff e [FILE_IO (OpenFile Read)] Bool
65−eof = EOF
66−
67−
68−
69−
libs/oldeffects/Effect/Random.idrdeleted−25
@@ -1,25 +0,0 @@
1−module Effect.Random
2−
3−import Effects
4−
5−data Random : Type -> Type -> Type -> Type where
6− getRandom : Random Integer Integer Integer
7− setSeed : Integer -> Random Integer Integer ()
8−
9−using (m : Type -> Type)
10− instance Handler Random m where
11− handle seed getRandom k
12− = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in
13− k seed' seed'
14− handle seed (setSeed n) k = k n ()
15−
16−RND : EFFECT
17−RND = MkEff Integer Random
18−
19−rndInt : Integer -> Integer -> Eff m [RND] Integer
20−rndInt lower upper = do v <- getRandom
21− return (v `prim__sremBigInt` (upper - lower) + lower)
22−
23−srand : Integer -> Eff m [RND] ()
24−srand n = setSeed n
25−
libs/oldeffects/Effect/StdIO.idrdeleted−60
@@ -1,60 +0,0 @@
1−module Effect.StdIO
2−
3−import Effects
4−import Control.IOExcept
5−
6−data StdIO : Effect where
7− PutStr : String -> StdIO () () ()
8− GetStr : StdIO () () String
9−
10−instance Handler StdIO IO where
11− handle () (PutStr s) k = do putStr s; k () ()
12− handle () GetStr k = do x <- getLine; k () x
13−
14−instance Handler StdIO (IOExcept a) where
15− handle () (PutStr s) k = do ioe_lift (putStr s); k () ()
16− handle () GetStr k = do x <- ioe_lift getLine; k () x
17−
18−-- Handle effects in a pure way, for simulating IO for unit testing/proof
19−
20−data IOStream a = MkStream (List String -> (a, List String))
21−
22−instance Handler StdIO IOStream where
23− handle () (PutStr s) k
24− = MkStream (\x => case k () () of
25− MkStream f => let (res, str) = f x in
26− (res, s :: str))
27− handle {a} () GetStr k
28− = MkStream (\x => case x of
29− [] => cont "" []
30− (t :: ts) => cont t ts)
31− where
32− cont : String -> List String -> (a, List String)
33− cont t ts = case k () t of
34− MkStream f => f ts
35−
36−--- The Effect and associated functions
37−
38−STDIO : EFFECT
39−STDIO = MkEff () StdIO
40−
41−putStr : Handler StdIO e => String -> Eff e [STDIO] ()
42−putStr s = PutStr s
43−
44−putStrLn : Handler StdIO e => String -> Eff e [STDIO] ()
45−putStrLn s = putStr (s ++ "\n")
46−
47−getStr : Handler StdIO e => Eff e [STDIO] String
48−getStr = GetStr
49−
50−mkStrFn : Env IOStream xs ->
51− Eff IOStream xs a ->
52− List String -> (a, List String)
53−mkStrFn {a} env p input = case mkStrFn' of
54− MkStream f => f input
55− where injStream : a -> IOStream a
56− injStream v = MkStream (\x => (v, []))
57− mkStrFn' : IOStream a
58− mkStrFn' = runWith injStream env p
59−
60−
libs/oldeffects/Effects.idrdeleted−308
@@ -1,308 +0,0 @@
1−module Effects
2−
3−import Language.Reflection
4−import Control.Catchable
5−
6−%access public
7−
8−---- Effects
9−
10−Effect : Type
11−Effect = Type -> Type -> Type -> Type
12−
13−%error_reverse
14−data EFFECT : Type where
15− MkEff : Type -> Effect -> EFFECT
16−
17−class Handler (e : Effect) (m : Type -> Type) where
18− handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a
19−
20−---- Properties and proof construction
21−
22−using (xs : List a, ys : List a)
23− data SubList : List a -> List a -> Type where
24− SubNil : SubList {a} [] []
25− Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
26− Drop : SubList xs ys -> SubList xs (x :: ys)
27−
28− subListId : SubList xs xs
29− subListId {xs = Nil} = SubNil
30− subListId {xs = x :: xs} = Keep subListId
31−
32−data Env : (m : Type -> Type) -> List EFFECT -> Type where
33− Nil : Env m Nil
34− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
35−
36−data EffElem : (Type -> Type -> Type -> Type) -> Type ->
37− List EFFECT -> Type where
38− Here : EffElem x a (MkEff a x :: xs)
39− There : EffElem x a xs -> EffElem x a (y :: xs)
40−
41−-- make an environment corresponding to a sub-list
42−dropEnv : Env m ys -> SubList xs ys -> Env m xs
43−dropEnv [] SubNil = []
44−dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
45−dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
46−
47−updateWith : (ys' : List a) -> (xs : List a) ->
48− SubList ys xs -> List a
49−updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
50−updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
51−updateWith [] [] SubNil = []
52−updateWith (y :: ys) [] SubNil = y :: ys
53−updateWith [] (x :: xs) (Keep rest) = []
54−
55−-- put things back, replacing old with new in the sub-environment
56−rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
57− Env m xs -> Env m (updateWith ys' xs prf)
58−rebuildEnv [] SubNil env = env
59−rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
60−rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
61−rebuildEnv (x :: xs) SubNil [] = x :: xs
62−
63−---- The Effect EDSL itself ----
64−
65−-- some proof automation
66−
67−%reflection
68−reflectListEffElem : List a -> Tactic
69−reflectListEffElem [] = Refine "Here" `Seq` Solve
70−reflectListEffElem (x :: xs)
71− = Try (Refine "Here" `Seq` Solve)
72− (Refine "There" `Seq` (Solve `Seq` reflectListEffElem xs))
73−-- TMP HACK! FIXME!
74−-- The evaluator needs a 'function case' to know its a reflection function
75−-- until we propagate that information! Without this, the _ case won't get
76−-- matched.
77−reflectListEffElem (x ++ y) = Refine "Here" `Seq` Solve
78−reflectListEffElem _ = Refine "Here" `Seq` Solve
79−
80−%reflection
81−reflectSubList : List a -> Tactic
82−reflectSubList [] = Refine "SubNil" `Seq` Solve
83−reflectSubList (x :: xs)
84− = Try (Refine "subListId" `Seq` Solve)
85− (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))
86− (Refine "Drop" `Seq` (Solve `Seq` reflectSubList xs)))
87−reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve
88−reflectSubList _ = Refine "subListId" `Seq` Solve
89−
90−%reflection
91−reflectEff : (P : Type) -> Tactic
92−reflectEff (EffElem m a xs)
93− = reflectListEffElem xs `Seq` Solve
94−reflectEff (SubList xs ys)
95− = reflectSubList ys `Seq` Solve
96−
97−updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
98− List EFFECT
99−updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs
100−updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n
101−
102−updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
103− List EFFECT
104−updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
105−updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
106−
107−infix 5 :::, :-, :=
108−
109−data LRes : lbl -> Type -> Type where
110− (:=) : (x : lbl) -> res -> LRes x res
111−
112−(:::) : lbl -> EFFECT -> EFFECT
113−(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff
114−
115−private
116−unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
117−unlabel {m} {x = MkEff a eff} [l := v] = [v]
118−
119−private
120−relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]
121−relabel {x = MkEff a eff} l [v] = [l := v]
122−
123−-- the language of Effects
124−
125−data EffM : (m : Type -> Type) ->
126− List EFFECT -> List EFFECT -> Type -> Type where
127− value : a -> EffM m xs xs a
128− ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
129− effect : (prf : EffElem e a xs) ->
130− (eff : e a b t) ->
131− EffM m xs (updateResTy xs prf eff) t
132− lift : (prf : SubList ys xs) ->
133− EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
134− new : Handler e m =>
135− res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->
136− EffM m xs xs' a
137− test : (prf : EffElem e (Either l r) xs) ->
138− EffM m (updateResTyImm xs prf l) xs' t ->
139− EffM m (updateResTyImm xs prf r) xs' t ->
140− EffM m xs xs' t
141− test_lbl : {x : lbl} ->
142− (prf : EffElem e (LRes x (Either l r)) xs) ->
143− EffM m (updateResTyImm xs prf (LRes x l)) xs' t ->
144− EffM m (updateResTyImm xs prf (LRes x r)) xs' t ->
145− EffM m xs xs' t
146− catch : Catchable m err =>
147− EffM m xs xs' a -> (err -> EffM m xs xs' a) ->
148− EffM m xs xs' a
149− (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t
150−
151−syntax [tag] ":!" [val] = !(tag :- val)
152−
153−-- Eff : List (EFFECT m) -> Type -> Type
154−
155−-- For making proofs implicitly for 'test' and 'test_lbl'
156−
157−syntax if_valid then [e] else [t] =
158− test (tactics { byReflection reflectEff; }) t e
159−
160−syntax if_valid [lbl] then [e] else [t] =
161− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
162−
163−syntax if_error then [t] else [e] =
164− test (tactics { byReflection reflectEff; }) t e
165−
166−syntax if_error [lbl] then [t] else [e] =
167− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
168−
169−-- These may read better in some contexts
170−
171−syntax if_right then [e] else [t] =
172− test (tactics { byReflection reflectEff; }) t e
173−
174−syntax if_right [lbl] then [e] else [t] =
175− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
176−
177−syntax if_left then [t] else [e] =
178− test (tactics { byReflection reflectEff; }) t e
179−
180−syntax if_left [lbl] then [t] else [e] =
181− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
182−
183−
184−-- for 'do' notation
185−
186−return : a -> EffM m xs xs a
187−return x = value x
188−
189−(>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
190−(>>=) = ebind
191−
192−-- for idiom brackets
193−
194−infixl 2 <$>
195−
196−pure : a -> EffM m xs xs a
197−pure = value
198−
199−(<$>) : EffM m xs xs (a -> b) -> EffM m xs xs a -> EffM m xs xs b
200−(<$>) prog v = do fn <- prog
201− arg <- v
202− return (fn arg)
203−
204−-- an interpreter
205−
206−private
207−execEff : Env m xs -> (p : EffElem e res xs) ->
208− (eff : e res b a) ->
209− (Env m (updateResTy xs p eff) -> a -> m t) -> m t
210−execEff (val :: env) Here eff' k
211− = handle val eff' (\res, v => k (res :: env) v)
212−execEff {e} {res} {b} {a} (val :: env) (There p) eff k
213− = execEff {e} {res} {b} {a} env p eff (\env', v => k (val :: env') v)
214−
215−private
216−testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->
217− (Env m (updateResTyImm xs p l) -> m b) ->
218− (Env m (updateResTyImm xs p r) -> m b) ->
219− m b
220−testEff (Left err :: env) Here lk rk = lk (err :: env)
221−testEff (Right ok :: env) Here lk rk = rk (ok :: env)
222−testEff (val :: env) (There p) lk rk
223− = testEff env p (\envk => lk (val :: envk))
224− (\envk => rk (val :: envk))
225−
226−private
227−testEffLbl : {x : lblTy} ->
228− Env m xs -> (p : EffElem e (LRes x (Either l r)) xs) ->
229− (Env m (updateResTyImm xs p (LRes x l)) -> m b) ->
230− (Env m (updateResTyImm xs p (LRes x r)) -> m b) ->
231− m b
232−testEffLbl ((lbl := Left err) :: env) Here lk rk = lk ((lbl := err) :: env)
233−testEffLbl ((lbl := Right ok) :: env) Here lk rk = rk ((lbl := ok) :: env)
234−testEffLbl (val :: env) (There p) lk rk
235− = testEffLbl env p (\envk => lk (val :: envk))
236− (\envk => rk (val :: envk))
237−
238−-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
239−-- updates can be propagated even through failing computations?
240−
241−eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b
242−eff env (value x) k = k env x
243−eff env (prog `ebind` c) k
244− = eff env prog (\env', p' => eff env' (c p') k)
245−eff env (effect prf effP) k = execEff env prf effP k
246−eff env (lift prf effP) k
247− = let env' = dropEnv env prf in
248− eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')
249−eff env (new r prog) k
250− = eff (r :: env) prog (\(v :: envk), p' => k envk p')
251−eff env (test prf l r) k
252− = testEff env prf (\envk => eff envk l k) (\envk => eff envk r k)
253−eff env (test_lbl prf l r) k
254− = testEffLbl env prf (\envk => eff envk l k) (\envk => eff envk r k)
255−eff env (catch prog handler) k
256− = catch (eff env prog k)
257− (\e => eff env (handler e) k)
258−-- FIXME:
259−-- xs is needed explicitly because otherwise the pattern binding for
260−-- 'l' appears too late. Solution seems to be to reorder patterns at the
261−-- end so that everything is in scope when it needs to be.
262−eff {xs = [l ::: x]} env (l :- prog) k
263− = let env' = unlabel env in
264− eff env' prog (\envk, p' => k (relabel l envk) p')
265−
266−implicit
267−lift' : EffM m ys ys' t ->
268− {default tactics { byReflection reflectEff; }
269− prf : SubList ys xs} ->
270− EffM m xs (updateWith ys' xs prf) t
271−lift' e {prf} = lift prf e
272−
273−implicit
274−effect' : {a, b: _} -> {e : Effect} ->
275− (eff : e a b t) ->
276− {default tactics { byReflection reflectEff; }
277− prf : EffElem e a xs} ->
278− EffM m xs (updateResTy xs prf eff) t
279−effect' e {prf} = effect prf e
280−
281−
282−run : Applicative m => Env m xs -> EffM m xs xs' a -> m a
283−run env prog = eff env prog (\env, r => pure r)
284−
285−runEnv : Applicative m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)
286−runEnv env prog = eff env prog (\env, r => pure (env, r))
287−
288−runPure : Env id xs -> EffM id xs xs' a -> a
289−runPure env prog = eff env prog (\env, r => r)
290−
291−-- runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)
292−-- runPureEnv env prog = eff env prog (\env, r => (env, r))
293−
294−runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a
295−runWith inj env prog = eff env prog (\env, r => inj r)
296−
297−Eff : (Type -> Type) -> List EFFECT -> Type -> Type
298−Eff m xs t = EffM m xs xs t
299−
300−-- some higher order things
301−
302−mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)
303−mapE f [] = pure []
304−mapE f (x :: xs) = [| f x :: mapE f xs |]
305−
306−when : Applicative m => Bool -> Lazy (Eff m xs ()) -> Eff m xs ()
307−when True e = e
308−when False e = pure ()
libs/prelude/Makefile+11−4
@@ -1,17 +1,24 @@
11IDRIS := idris
2+PKG := prelude
23
34build:
4− $(IDRIS) --build prelude.ipkg
5+ $(IDRIS) --build ${PKG}.ipkg
56
67install:
7− $(IDRIS) --install prelude.ipkg
8+ $(IDRIS) --install ${PKG}.ipkg
89
910clean:
10− $(IDRIS) --clean prelude.ipkg
11+ $(IDRIS) --clean ${PKG}.ipkg
1112
1213rebuild: clean build
1314
1415linecount:
1516 find . -name '*.idr' | xargs wc -l
1617
17−.PHONY: build install clean rebuild linecount
18+doc:
19+ $(IDRIS) --mkdoc ${PKG}.ipkg
20+
21+doc_clean:
22+ rm -rf ${PKG}_doc
23+
24+.PHONY: build install clean rebuild linecount doc
libs/prelude/Prelude/Algebra.idr+1−1
@@ -106,7 +106,7 @@ class AbelianGroup a => Ring a where
106106class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
107107 total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
108108 total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
109− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
109+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (c <*> r)
110110
111111||| Sets equipped with two binary operations, one associative and commutative
112112||| supplied with a neutral element, and the other associative supplied with a
libs/prelude/Prelude/Bool.idr+1−1
@@ -5,7 +5,7 @@ import Builtins
55import Prelude.Uninhabited
66
77||| Boolean Data Type
8−data Bool = False | True
8+%case data Bool = False | True
99
1010||| The underlying implementation of the if ... then ... else ... syntax
1111||| @ b the condition on the if
libs/prelude/Prelude/List.idr+9
@@ -557,6 +557,12 @@ tails xs = xs :: case xs of
557557 [] => []
558558 _ :: xs' => tails xs'
559559
560+splitOn : Eq a => a -> List a -> List (List a)
561+splitOn a = split (== a)
562+
563+replaceOn : Eq a => a -> a -> List a -> List a
564+replaceOn a b l = map (\c => if c == a then b else c) l
565+
560566--------------------------------------------------------------------------------
561567-- Predicates
562568--------------------------------------------------------------------------------
@@ -579,6 +585,9 @@ isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
579585isSuffixOf : Eq a => List a -> List a -> Bool
580586isSuffixOf = isSuffixOfBy (==)
581587
588+isInfixOf : Eq a => List a -> List a -> Bool
589+isInfixOf n h = any (isPrefixOf n) (tails h)
590+
582591--------------------------------------------------------------------------------
583592-- Sorting
584593--------------------------------------------------------------------------------
libs/prelude/Prelude/Nat.idr+34
@@ -110,6 +110,22 @@ LT left right = LTE (S left) right
110110total GT : Nat -> Nat -> Type
111111GT left right = LT right left
112112
113+||| A successor is never less than or equal zero
114+succNotLTEzero : Not (S m `LTE` Z)
115+succNotLTEzero lteZero impossible
116+
117+||| If two numbers are ordered, their predecessors are too
118+fromLteSucc : (S m `LTE` S n) -> (m `LTE` n)
119+fromLteSucc (lteSucc x) = x
120+
121+||| A decision procedure for `LTE`
122+isLTE : (m, n : Nat) -> Dec (m `LTE` n)
123+isLTE Z n = Yes lteZero
124+isLTE (S k) Z = No succNotLTEzero
125+isLTE (S k) (S j) with (isLTE k j)
126+ isLTE (S k) (S j) | (Yes prf) = Yes (lteSucc prf)
127+ isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)
128+
113129||| Boolean test than one Nat is less than or equal to another
114130total lte : Nat -> Nat -> Bool
115131lte Z right = True
@@ -312,6 +328,24 @@ lcm _ Z = Z
312328lcm Z _ = Z
313329lcm x y = divNat (x * y) (gcd x y)
314330
331+
332+--------------------------------------------------------------------------------
333+-- An informative comparison view
334+--------------------------------------------------------------------------------
335+data CmpNat : Nat -> Nat -> Type where
336+ cmpLT : (y : _) -> CmpNat x (x + S y)
337+ cmpEQ : CmpNat x x
338+ cmpGT : (x : _) -> CmpNat (y + S x) y
339+
340+total cmp : (x, y : Nat) -> CmpNat x y
341+cmp Z Z = cmpEQ
342+cmp Z (S k) = cmpLT _
343+cmp (S k) Z = cmpGT _
344+cmp (S x) (S y) with (cmp x y)
345+ cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k
346+ cmp (S x) (S x) | cmpEQ = cmpEQ
347+ cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k
348+
315349--------------------------------------------------------------------------------
316350-- Properties
317351--------------------------------------------------------------------------------
libs/prelude/Prelude/Stream.idr+1−1
@@ -85,7 +85,7 @@ scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
8585||| Produce a Stream of (corecursive) right folds of tails of the given Stream
8686||| @ f the combining function
8787||| @ xs the Stream to fold up
88−-- Reusing the head of the corecursion in the obvious way doesn’t productivity check
88+-- Reusing the head of the corecursion in the obvious way doesn't productivity check
8989scanr : (f : a -> Inf b -> b) -> (xs : Stream a) -> Stream b
9090scanr f (x :: Delay xs) = f x (foldr f xs) :: scanr f xs
9191
libs/prelude/Prelude/Strings.idr+5−1
@@ -218,9 +218,13 @@ lines s = map pack $ lines' $ unpack s
218218
219219partial
220220foldr1 : (a -> a -> a) -> List a -> a
221−foldr1 f [x] = x
221+foldr1 _ [x] = x
222222foldr1 f (x::xs) = f x (foldr1 f xs)
223223
224+partial
225+foldl1 : (a -> a -> a) -> List a -> a
226+foldl1 f (x::xs) = foldl f x xs
227+
224228||| Joins the character lists by spaces into a single character list.
225229|||
226230||| Idris> unwords' [['A'], ['B', 'C'], ['D'], ['E']]
libs/prelude/Prelude/Vect.idr+11−16
@@ -100,17 +100,15 @@ updateAt (fS k) f (x::xs) = x :: updateAt k f xs
100100
101101||| Get the first m elements of a Vect
102102||| @ m the number of elements to take
103−take : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a
104−take (fS k) [] = FinZElim k
105−take fZ _ = []
106−take (fS k) (x::xs) = x :: take k xs
103+take : (n : Nat) -> Vect (n + m) a -> Vect n a
104+take Z xs = []
105+take (S k) (x :: xs) = x :: take k xs
107106
108107||| Remove the first m elements of a Vect
109108||| @ m the number of elements to remove
110−drop : (m : Fin (S n)) -> Vect n a -> Vect (n - cast m) a
111−drop (fS k) [] = FinZElim k
112−drop fZ xs ?= xs
113−drop (fS k) (x::xs) = drop k xs
109+drop : (n : Nat) -> Vect (n + m) a -> Vect m a
110+drop Z xs = xs
111+drop (S k) (x :: xs) = drop k xs
114112
115113--------------------------------------------------------------------------------
116114-- Transformations
@@ -260,10 +258,13 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
260258concat [] = []
261259concat (v::vs) = v ++ concat vs
262260
263−||| Fold without seeding the accumulator
261+||| Foldr without seeding the accumulator
264262foldr1 : (t -> t -> t) -> Vect (S n) t -> t
265263foldr1 f (x::xs) = foldr f x xs
266264
265+||| Foldl without seeding the accumulator
266+foldl1 : (t -> t -> t) -> Vect (S n) t -> t
267+foldl1 f (x::xs) = foldl f x xs
267268--------------------------------------------------------------------------------
268269-- Scans
269270--------------------------------------------------------------------------------
@@ -404,7 +405,7 @@ nub = nubBy (==)
404405||| It is equivalent to (take n xs, drop n xs)
405406||| @ m the index to split at
406407||| @ xs the Vect to split in two
407−splitAt : {n : Nat} -> (m : Fin (S n)) -> (xs : Vect n a) -> (Vect (cast m) a, Vect (n - cast m) a)
408+splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
408409splitAt n xs = (take n xs, drop n xs)
409410
410411--------------------------------------------------------------------------------
@@ -486,12 +487,6 @@ vectAppendAssociative (x :: xs) ys zs =
486487-- Proofs
487488--------------------------------------------------------------------------------
488489
489−Prelude.Vect.drop_lemma_1 = proof {
490− intros;
491− rewrite sym (minusZeroRight n);
492− trivial;
493−}
494−
495490Prelude.Vect.reverse'_lemma_1 = proof {
496491 intros;
497492 rewrite prf;
rts/idris_gc.c+11−2
@@ -103,7 +103,14 @@ void idris_gc(VM* vm) {
103103 free(vm->heap.old);
104104
105105 vm->heap.heap = newheap;
106− vm->heap.next = newheap;
106+#ifdef FORCE_ALIGNMENT
107+ if (((i_int)(vm->heap.heap)&1) == 1) {
108+ vm->heap.next = newheap + 1;
109+ } else
110+#endif
111+ {
112+ vm->heap.next = newheap;
113+ }
107114 vm->heap.end = newheap + vm->heap.size;
108115
109116 VAL* root;
@@ -111,10 +118,12 @@ void idris_gc(VM* vm) {
111118 for(root = vm->valstack; root < vm->valstack_top; ++root) {
112119 *root = copy(vm, *root);
113120 }
121+
122+#ifdef HAS_PTHREAD
114123 for(root = vm->inbox_ptr; root < vm->inbox_write; ++root) {
115124 *root = copy(vm, *root);
116125 }
117−
126+#endif
118127 vm->ret = copy(vm, vm->ret);
119128 vm->reg1 = copy(vm, vm->reg1);
120129
rts/idris_heap.c+8−1
@@ -16,7 +16,14 @@ void alloc_heap(Heap * h, size_t heap_size)
1616 }
1717
1818 h->heap = mem;
19− h->next = h->heap;
19+#ifdef FORCE_ALIGNMENT
20+ if (((i_int)(h->heap)&1) == 1) {
21+ h->next = h->heap + 1;
22+ } else
23+#endif
24+ {
25+ h->next = h->heap;
26+ }
2027 h->end = h->heap + heap_size;
2128
2229 h->size = heap_size;
rts/idris_net.c+190−23
@@ -1,6 +1,7 @@
11// C-Side of the Idris network library
22// (C) Simon Fowler, 2014
33// MIT Licensed. Have fun!
4+#include "idris_net.h"
45#include <errno.h>
56#include <netdb.h>
67#include <stdbool.h>
@@ -12,7 +13,21 @@
1213#include <netinet/in.h>
1314#include <arpa/inet.h>
1415
15−#include "idris_net.h"
16+void buf_htonl(void* buf, int len) {
17+ int* buf_i = (int*) buf;
18+ int i;
19+ for (i = 0; i < (len / sizeof(int)) + 1; i++) {
20+ buf_i[i] = htonl(buf_i[i]);
21+ }
22+}
23+
24+void buf_ntohl(void* buf, int len) {
25+ int* buf_i = (int*) buf;
26+ int i;
27+ for (i = 0; i < (len / sizeof(int)) + 1; i++) {
28+ buf_i[i] = ntohl(buf_i[i]);
29+ }
30+}
1631
1732void* idrnet_malloc(int size) {
1833 return malloc(size);
@@ -22,9 +37,12 @@ void idrnet_free(void* ptr) {
2237 free(ptr);
2338}
2439
25−int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {
40+// We call this from quite a few functions. Given a textual host and an int port,
41+// populates a struct addrinfo.
42+int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port,
43+ int family, int socket_type) {
44+
2645 struct addrinfo hints;
27− struct addrinfo* address_res;
2846 // Convert port into string
2947 char str_port[8];
3048 sprintf(str_port, "%d", port);
@@ -38,43 +56,42 @@ int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {
3856 // then we want to instruct the C library to fill in the IP automatically
3957 if (strlen(host) == 0) {
4058 hints.ai_flags = AI_PASSIVE; // fill in IP automatically
41− }
59+ return getaddrinfo(NULL, str_port, &hints, address_res);
60+ }
61+ return getaddrinfo(host, str_port, &hints, address_res);
4262
43− int addr_res = getaddrinfo(host, str_port, &hints, &address_res);
63+}
64+
65+int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {
66+ struct addrinfo* address_res;
67+ int addr_res = idrnet_getaddrinfo(&address_res, host, port, family, socket_type);
4468 if (addr_res == -1) {
69+ //printf("Lib err: bind getaddrinfo\n");
4570 return -1;
4671 }
4772
4873 int bind_res = bind(sockfd, address_res->ai_addr, address_res->ai_addrlen);
4974 if (bind_res == -1) {
75+ //freeaddrinfo(address_res);
76+ //printf("Lib err: bind\n");
5077 return -1;
5178 }
52−
5379 return 0;
5480}
5581
5682int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port) {
57− char str_port[8];
58− sprintf(str_port, "%d", port);
59− struct addrinfo hints;
6083 struct addrinfo* remote_host;
61−
62− // Set up hints structure for getaddrinfo
63− memset(&hints, 0, sizeof(hints));
64− hints.ai_family = family;
65− hints.ai_socktype = socket_type;
66−
67− // Get info about the remote host (DNS lookup etc)
68− int addr_res = getaddrinfo(host, str_port, &hints, &remote_host);
84+ int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, socket_type);
6985 if (addr_res == -1) {
7086 return -1;
7187 }
7288
7389 int connect_res = connect(sockfd, remote_host->ai_addr, remote_host->ai_addrlen);
7490 if (connect_res == -1) {
91+ freeaddrinfo(remote_host);
7592 return -1;
7693 }
77−
94+ freeaddrinfo(remote_host);
7895 return 0;
7996}
8097
@@ -88,9 +105,15 @@ char* idrnet_sockaddr_ipv4(void* sockaddr) {
88105 struct sockaddr_in* addr = (struct sockaddr_in*) sockaddr;
89106 char* ip_addr = (char*) malloc(sizeof(char) * INET_ADDRSTRLEN);
90107 inet_ntop(AF_INET, &(addr->sin_addr), ip_addr, INET_ADDRSTRLEN);
108+ //printf("Lib: ip_addr: %s\n", ip_addr);
91109 return ip_addr;
92110}
93111
112+int idrnet_sockaddr_ipv4_port(void* sockaddr) {
113+ struct sockaddr_in* addr = (struct sockaddr_in*) addr;
114+ return ((int) ntohs(addr->sin_port));
115+}
116+
94117void* idrnet_create_sockaddr() {
95118 return malloc(sizeof(struct sockaddr_storage));
96119}
@@ -108,33 +131,43 @@ int idrnet_send(int sockfd, char* data) {
108131}
109132
110133int idrnet_send_buf(int sockfd, void* data, int len) {
111− return send(sockfd, data, len, 0);
134+ void* buf_cpy = malloc(len);
135+ memset(buf_cpy, 0, len);
136+ memcpy(buf_cpy, data, len);
137+ buf_htonl(buf_cpy, len);
138+ int res = send(sockfd, buf_cpy, len, 0);
139+ free(buf_cpy);
140+ return res;
112141}
113142
114143void* idrnet_recv(int sockfd, int len) {
115144 idrnet_recv_result* res_struct =
116145 (idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));
117−
118146 char* buf = malloc(len + 1);
147+ memset(buf, 0, len + 1);
119148 int recv_res = recv(sockfd, buf, len, 0);
120149 res_struct->result = recv_res;
121150
122151 if (recv_res > 0) { // Data was received
123152 buf[recv_res + 1] = 0x00; // Null-term, so Idris can interpret it
124153 }
125− res_struct->payload = (void*) buf;
154+ res_struct->payload = buf;
126155 return (void*) res_struct;
127156}
128157
129158int idrnet_recv_buf(int sockfd, void* buf, int len) {
130− return recv(sockfd, buf, len, 0);
159+ int recv_res = recv(sockfd, buf, len, 0);
160+ if (recv_res != -1) {
161+ buf_ntohl(buf, len);
162+ }
163+ return recv_res;
131164}
132165
133166int idrnet_get_recv_res(void* res_struct) {
134167 return (((idrnet_recv_result*) res_struct)->result);
135168}
136169
137−void* idrnet_get_recv_payload(void* res_struct) {
170+char* idrnet_get_recv_payload(void* res_struct) {
138171 return (((idrnet_recv_result*) res_struct)->payload);
139172}
140173
@@ -151,3 +184,137 @@ int idrnet_errno() {
151184 return errno;
152185}
153186
187+
188+int idrnet_sendto(int sockfd, char* data, char* host, int port, int family) {
189+
190+ struct addrinfo* remote_host;
191+ int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, SOCK_DGRAM);
192+ if (addr_res == -1) {
193+ return -1;
194+ }
195+
196+ int send_res = sendto(sockfd, data, strlen(data), 0,
197+ remote_host->ai_addr, remote_host->ai_addrlen);
198+ freeaddrinfo(remote_host);
199+ return send_res;
200+}
201+
202+int idrnet_sendto_buf(int sockfd, void* buf, int buf_len, char* host, int port, int family) {
203+
204+ struct addrinfo* remote_host;
205+ int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, SOCK_DGRAM);
206+ if (addr_res == -1) {
207+ //printf("lib err: sendto getaddrinfo \n");
208+ return -1;
209+ }
210+
211+ buf_htonl(buf, buf_len);
212+
213+ int send_res = sendto(sockfd, buf, buf_len, 0,
214+ remote_host->ai_addr, remote_host->ai_addrlen);
215+ if (send_res == -1) {
216+ perror("lib err: sendto \n");
217+ }
218+ //freeaddrinfo(remote_host);
219+ return send_res;
220+}
221+
222+
223+
224+void* idrnet_recvfrom(int sockfd, int len) {
225+/*
226+ * int recvfrom(int sockfd, void *buf, int len, unsigned int flags,
227+ struct sockaddr *from, int *fromlen);
228+*/
229+ // Allocate the required structures, and nuke them
230+ struct sockaddr_storage* remote_addr =
231+ (struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));
232+ char* buf = (char*) malloc(len + 1);
233+ idrnet_recvfrom_result* ret =
234+ (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));
235+ memset(remote_addr, 0, sizeof(struct sockaddr_storage));
236+ memset(buf, 0, len + 1);
237+ memset(ret, 0, sizeof(idrnet_recvfrom_result));
238+ socklen_t fromlen = sizeof(struct sockaddr_storage);
239+
240+ int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);
241+ ret->result = recv_res;
242+ // Check for failure...
243+ if (recv_res == -1) {
244+ free(buf);
245+ free(remote_addr);
246+ } else {
247+ // If data was received, process and populate
248+ ret->result = recv_res;
249+ ret->remote_addr = remote_addr;
250+ // Ensure the last byte is NULL, since in this mode we're sending strings
251+ buf[len] = 0x00;
252+ ret->payload = (void*) buf;
253+ }
254+
255+ return ret;
256+}
257+
258+
259+void* idrnet_recvfrom_buf(int sockfd, void* buf, int len) {
260+ // Allocate the required structures, and nuke them
261+ struct sockaddr_storage* remote_addr =
262+ (struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));
263+ idrnet_recvfrom_result* ret =
264+ (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));
265+ memset(remote_addr, 0, sizeof(struct sockaddr_storage));
266+ memset(ret, 0, sizeof(idrnet_recvfrom_result));
267+ socklen_t fromlen = 0;
268+
269+ int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);
270+ // Check for failure... But don't free the buffer! Not our job.
271+ ret->result = recv_res;
272+ if (recv_res == -1) {
273+ free(remote_addr);
274+ }
275+ // Payload will be NULL -- since it's been put into the user-specified buffer. We
276+ // still need the return struct to get our hands on the remote address, though.
277+ if (recv_res > 0) {
278+ buf_ntohl(buf, len);
279+ ret->payload = NULL;
280+ ret->remote_addr = remote_addr;
281+ }
282+ return ret;
283+}
284+
285+int idrnet_get_recvfrom_res(void* res_struct) {
286+ return (((idrnet_recvfrom_result*) res_struct)->result);
287+}
288+
289+char* idrnet_get_recvfrom_payload(void* res_struct) {
290+ return (((idrnet_recvfrom_result*) res_struct)->payload);
291+}
292+
293+void* idrnet_get_recvfrom_sockaddr(void* res_struct) {
294+ idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;
295+ return recv_struct->remote_addr;
296+}
297+
298+int idrnet_get_recvfrom_port(void* res_struct) {
299+ idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;
300+ if (recv_struct->remote_addr != NULL) {
301+ struct sockaddr_in* remote_addr_in =
302+ (struct sockaddr_in*) recv_struct->remote_addr;
303+ return ((int) ntohs(remote_addr_in->sin_port));
304+ }
305+ return -1;
306+}
307+
308+void idrnet_free_recvfrom_struct(void* res_struct) {
309+ idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;
310+ if (recv_struct != NULL) {
311+ if (recv_struct->payload != NULL) {
312+ free(recv_struct->payload);
313+ }
314+ if (recv_struct->remote_addr != NULL) {
315+ free(recv_struct->remote_addr);
316+ }
317+ }
318+}
319+
320+
rts/idris_net.h+34−1
@@ -1,11 +1,22 @@
11#ifndef IDRISNET_H
22#define IDRISNET_H
33
4+struct sockaddr_storage;
5+struct addrinfo;
6+
47typedef struct idrnet_recv_result {
58 int result;
69 void* payload;
710} idrnet_recv_result;
811
12+// Same type of thing as idrnet_recv_result, but for UDP, so stores some
13+// address information
14+typedef struct idrnet_recvfrom_result {
15+ int result;
16+ void* payload;
17+ struct sockaddr_storage* remote_addr;
18+} idrnet_recvfrom_result;
19+
920// Memory management functions
1021void* idrnet_malloc(int size);
1122void idrnet_free(void* ptr);
@@ -22,6 +33,7 @@ int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port
2233// Accessor functions for struct_sockaddr
2334int idrnet_sockaddr_family(void* sockaddr);
2435char* idrnet_sockaddr_ipv4(void* sockaddr);
36+int idrnet_sockaddr_ipv4_port(void* sockaddr);
2537void* idrnet_create_sockaddr();
2638
2739// Accept
@@ -37,8 +49,29 @@ void* idrnet_recv(int sockfd, int len);
3749// Receives directly into a buffer
3850int idrnet_recv_buf(int sockfd, void* buf, int len);
3951
52+// UDP Send
53+int idrnet_sendto(int sockfd, char* data, char* host, int port, int family);
54+int idrnet_sendto_buf(int sockfd, void* buf, int buf_len, char* host, int port, int family);
55+
56+
57+// UDP Receive
58+void* idrnet_recvfrom(int sockfd, int len);
59+void* idrnet_recvfrom_buf(int sockfd, void* buf, int len);
60+
4061// Receive structure accessors
4162int idrnet_get_recv_res(void* res_struct);
42−void* idrnet_get_recv_payload(void* res_struct);
63+char* idrnet_get_recv_payload(void* res_struct);
4364void idrnet_free_recv_struct(void* res_struct);
65+
66+// Recvfrom structure accessors
67+int idrnet_get_recvfrom_res(void* res_struct);
68+char* idrnet_get_recvfrom_payload(void* res_struct);
69+void* idrnet_get_recvfrom_sockaddr(void* res_struct);
70+void idrnet_free_recvfrom_struct(void* res_struct);
71+
72+
73+int idrnet_getaddrinfo(struct addrinfo** address_res, char* host,
74+ int port, int family, int socket_type);
75+
76+
4477#endif
rts/idris_rts.c+23−11
@@ -1,10 +1,11 @@
11#include <stdlib.h>
22#include <stdio.h>
33#include <string.h>
4−#include <unistd.h>
54#include <stdarg.h>
65#include <assert.h>
6+#ifdef HAS_PTHREAD
77#include <pthread.h>
8+#endif
89
910#include "idris_rts.h"
1011#include "idris_gc.h"
@@ -30,7 +31,7 @@ VM* init_vm(int stack_size, size_t heap_size,
3031
3132 vm->ret = NULL;
3233 vm->reg1 = NULL;
33−
34+#ifdef HAS_PTHREAD
3435 vm->inbox = malloc(1024*sizeof(VAL));
3536 memset(vm->inbox, 0, 1024*sizeof(VAL));
3637 vm->inbox_end = vm->inbox + 1024;
@@ -53,7 +54,7 @@ VM* init_vm(int stack_size, size_t heap_size,
5354
5455 vm->max_threads = max_threads;
5556 vm->processes = 0;
56−
57+#endif
5758 STATS_LEAVE_INIT(vm->stats)
5859 return vm;
5960}
@@ -61,14 +62,16 @@ VM* init_vm(int stack_size, size_t heap_size,
6162Stats terminate(VM* vm) {
6263 Stats stats = vm->stats;
6364 STATS_ENTER_EXIT(stats)
64−
65+#ifdef HAS_PTHREAD
6566 free(vm->inbox);
67+#endif
6668 free(vm->valstack);
6769 free_heap(&(vm->heap));
68−
70+#ifdef HAS_PTHREAD
6971 pthread_mutex_destroy(&(vm -> inbox_lock));
7072 pthread_mutex_destroy(&(vm -> inbox_block));
7173 pthread_cond_destroy(&(vm -> inbox_waiting));
74+#endif
7275 free(vm);
7376
7477 STATS_LEAVE_EXIT(stats)
@@ -79,18 +82,21 @@ void idris_requireAlloc(VM* vm, size_t size) {
7982 if (!(vm->heap.next + size < vm->heap.end)) {
8083 idris_gc(vm);
8184 }
82−
85+#ifdef HAS_PTHREAD
8386 int lock = vm->processes > 0;
8487 if (lock) { // We only need to lock if we're in concurrent mode
8588 pthread_mutex_lock(&vm->alloc_lock);
8689 }
90+#endif
8791}
8892
8993void idris_doneAlloc(VM* vm) {
94+#ifdef HAS_PTHREAD
9095 int lock = vm->processes > 0;
9196 if (lock) { // We only need to lock if we're in concurrent mode
9297 pthread_mutex_unlock(&vm->alloc_lock);
9398 }
99+#endif
94100}
95101
96102int space(VM* vm, size_t size) {
@@ -99,16 +105,18 @@ int space(VM* vm, size_t size) {
99105
100106void* allocate(VM* vm, size_t size, int outerlock) {
101107// return malloc(size);
108+#ifdef HAS_PTHREAD
102109 int lock = vm->processes > 0 && !outerlock;
103110
104111 if (lock) { // not message passing
105112 pthread_mutex_lock(&vm->alloc_lock);
106113 }
114+#endif
107115
108116 if ((size & 7)!=0) {
109117 size = 8 + ((size >> 3) << 3);
110118 }
111−
119+
112120 size_t chunk_size = size + sizeof(size_t);
113121
114122 if (vm->heap.next + chunk_size < vm->heap.end) {
@@ -120,16 +128,19 @@ void* allocate(VM* vm, size_t size, int outerlock) {
120128 assert(vm->heap.next <= vm->heap.end);
121129
122130 memset(ptr, 0, size);
123−
131+#ifdef HAS_PTHREAD
124132 if (lock) { // not message passing
125133 pthread_mutex_unlock(&vm->alloc_lock);
126134 }
135+#endif
127136 return ptr;
128137 } else {
129138 idris_gc(vm);
139+#ifdef HAS_PTHREAD
130140 if (lock) { // not message passing
131141 pthread_mutex_unlock(&vm->alloc_lock);
132142 }
143+#endif
133144 return allocate(vm, size, 0);
134145 }
135146
@@ -187,7 +198,7 @@ VAL MKPTR(VM* vm, void* ptr) {
187198 return cl;
188199}
189200
190−VAL MKMPTR(VM* vm, void* ptr, int size) {
201+VAL MKMPTR(VM* vm, void* ptr, size_t size) {
191202 Closure* cl = allocate(vm, sizeof(Closure) +
192203 sizeof(ManagedPtr) + size, 0);
193204 SETTY(cl, MANAGEDPTR);
@@ -222,7 +233,7 @@ VAL MKPTRc(VM* vm, void* ptr) {
222233 return cl;
223234}
224235
225−VAL MKMPTRc(VM* vm, void* ptr, int size) {
236+VAL MKMPTRc(VM* vm, void* ptr, size_t size) {
226237 Closure* cl = allocate(vm, sizeof(Closure) +
227238 sizeof(ManagedPtr) + size, 1);
228239 SETTY(cl, MANAGEDPTR);
@@ -760,6 +771,7 @@ typedef struct {
760771 VAL arg;
761772} ThreadData;
762773
774+#ifdef HAS_PTHREAD
763775void* runThread(void* arg) {
764776 ThreadData* td = (ThreadData*)arg;
765777 VM* vm = td->vm;
@@ -949,7 +961,7 @@ VAL idris_recvMessage(VM* vm) {
949961
950962 return msg;
951963}
952−
964+#endif
953965int __idris_argc;
954966char **__idris_argv;
955967
rts/idris_rts.h+13−9
@@ -4,9 +4,10 @@
44#include <stdlib.h>
55#include <stdio.h>
66#include <string.h>
7−#include <unistd.h>
87#include <stdarg.h>
8+#ifdef HAS_PTHREAD
99#include <pthread.h>
10+#endif
1011#include <stdint.h>
1112
1213#include "idris_heap.h"
@@ -23,13 +24,13 @@ typedef enum {
2324typedef struct Closure *VAL;
2425
2526typedef struct {
26− int tag_arity;
27+ uint32_t tag_arity;
2728 VAL args[];
2829} con;
2930
3031typedef struct {
3132 VAL str;
32− int offset;
33+ size_t offset;
3334} StrOffset;
3435
3536typedef struct {
@@ -49,7 +50,10 @@ typedef struct {
4950typedef struct Closure {
5051// Use top 16 bits of ty for saying which heap value is in
5152// Bottom 16 bits for closure type
52− ClosureType ty;
53+//
54+// NOTE: ty can not have type ClosureType because ty must be a
55+// uint32_t but enum is platform dependent
56+ uint32_t ty;
5357 union {
5458 con c;
5559 int i;
@@ -73,7 +77,7 @@ typedef struct {
7377 VAL* stack_max;
7478
7579 Heap heap;
76−
80+#ifdef HAS_PTHREAD
7781 pthread_mutex_t inbox_lock;
7882 pthread_mutex_t inbox_block;
7983 pthread_mutex_t alloc_lock;
@@ -87,7 +91,7 @@ typedef struct {
8791
8892 int processes; // Number of child processes
8993 int max_threads; // maximum number of threads to run in parallel
90−
94+#endif
9195 Stats stats;
9296
9397 VAL ret;
@@ -170,7 +174,7 @@ typedef intptr_t i_int;
170174VAL MKFLOAT(VM* vm, double val);
171175VAL MKSTR(VM* vm, const char* str);
172176VAL MKPTR(VM* vm, void* ptr);
173−VAL MKMPTR(VM* vm, void* ptr, int size);
177+VAL MKMPTR(VM* vm, void* ptr, size_t size);
174178VAL MKB8(VM* vm, uint8_t b);
175179VAL MKB16(VM* vm, uint16_t b);
176180VAL MKB32(VM* vm, uint32_t b);
@@ -181,7 +185,7 @@ VAL MKFLOATc(VM* vm, double val);
181185VAL MKSTROFFc(VM* vm, StrOffset* off);
182186VAL MKSTRc(VM* vm, char* str);
183187VAL MKPTRc(VM* vm, void* ptr);
184−VAL MKMPTRc(VM* vm, void* ptr, int size);
188+VAL MKMPTRc(VM* vm, void* ptr, size_t size);
185189VAL MKBUFFERc(VM* vm, Buffer* buf);
186190
187191char* GETSTROFF(VAL stroff);
@@ -208,7 +212,7 @@ void idris_doneAlloc(VM* vm);
208212#define allocCon(cl, vm, t, a, o) \
209213 cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*a, o); \
210214 SETTY(cl, CON); \
211− cl->info.c.tag_arity = ((t) << 8) + (a);
215+ cl->info.c.tag_arity = ((t) << 8) | (a);
212216
213217void* vmThread(VM* callvm, func f, VAL arg);
214218
rts/windows/idris_net.c+1−1
@@ -177,7 +177,7 @@ int idrnet_get_recv_res(void* res_struct) {
177177 return (((idrnet_recv_result*) res_struct)->result);
178178}
179179
180−void* idrnet_get_recv_payload(void* res_struct) {
180+char* idrnet_get_recv_payload(void* res_struct) {
181181 return (((idrnet_recv_result*) res_struct)->payload);
182182}
183183
src/IRTS/CodegenC.hs+1
@@ -68,6 +68,7 @@ codegenC' defs out exec incs objs libs flags dbg
6868 let gcc = comp ++ " " ++
6969 gccDbg dbg ++ " " ++
7070 gccFlags ++
71+ " -DHAS_PTHREAD " ++
7172 " -I. " ++ objs ++ " -x c " ++
7273 (if (exec == Executable) then "" else " -c ") ++
7374 " " ++ tmpn ++
src/IRTS/CodegenJava.hs+8−5
@@ -169,7 +169,7 @@ jarHeader =
169169 ++ "if test -n \"$JAVA_HOME\"; then\n"
170170 ++ " java=\"$JAVA_HOME/bin/java\"\n"
171171 ++ "fi\n"
172− ++ "exec \"$java\" $java_args -jar $MYSELF \"$@\""
172+ ++ "exec \"$java\" $java_args -jar $MYSELF \"$@\"\n"
173173 ++ "exit 1\n"
174174
175175-----------------------------------------------------------------------
@@ -312,6 +312,7 @@ mkCompilationUnit globalInit defs hdrs out = do
312312 , ImportDecl True idrisPrelude True
313313 , ImportDecl False bigInteger False
314314 , ImportDecl False runtimeException False
315+ , ImportDecl False byteBuffer False
315316 ] ++ otherHdrs
316317 )
317318 <$> mkTypeDecl clsName globalInit defs
@@ -320,6 +321,7 @@ mkCompilationUnit globalInit defs hdrs out = do
320321 idrisPrelude = J.Name $ map Ident ["org", "idris", "rts", "Prelude"]
321322 bigInteger = J.Name $ map Ident ["java", "math", "BigInteger"]
322323 runtimeException = J.Name $ map Ident ["java", "lang", "RuntimeException"]
324+ byteBuffer = J.Name $ map Ident ["java", "nio", "ByteBuffer"]
323325 otherHdrs = map ( (\ name -> ImportDecl False name False)
324326 . J.Name
325327 . map (Ident . T.unpack)
@@ -386,9 +388,7 @@ mkMainMethod =
386388 "main"
387389 [FormalParam [] (array stringType) False (VarId $ Ident "args")]
388390 $ Block [ BlockStmt . ExpStmt
389− $ call "idris_initArgs" [ (threadType ~> "currentThread") []
390− , jConst "args"
391− ]
391+ $ call "idris_initArgs" [ jConst "args" ]
392392 , BlockStmt . ExpStmt $ call (mangle' (sMN 0 "runMain")) []
393393 ]
394394
@@ -484,6 +484,8 @@ mkExp pp (SOp LFork [arg]) =
484484 (mkThread arg) >>= ppExp pp
485485mkExp pp (SOp LPar [arg]) =
486486 (Nothing <>@! arg) >>= ppExp pp
487+mkExp pp (SOp LRegisterPtr [ptr, i]) =
488+ (Nothing <>@! ptr) >>= ppExp pp
487489mkExp pp (SOp LNoOp args) =
488490 (Nothing <>@! (last args)) >>= ppExp pp
489491mkExp pp (SOp LNullPtr args) =
@@ -707,6 +709,7 @@ mkConstant c@(AType x) = ClassLit (Just $ box (constType c))
707709mkConstant c@(StrType ) = ClassLit (Just $ stringType)
708710mkConstant c@(PtrType ) = ClassLit (Just $ objectType)
709711mkConstant c@(ManagedPtrType) = ClassLit (Just $ objectType)
712+mkConstant c@(BufferType) = ClassLit (Just $ bufferType)
710713mkConstant c@(VoidType ) = ClassLit (Just $ voidType)
711714mkConstant c@(Forgot ) = ClassLit (Just $ objectType)
712715
@@ -744,7 +747,7 @@ mkForeign pp (LANG_JAVA callType) resTy text params
744747
745748mkPrimitiveFunction :: PrimFn -> [LVar] -> CodeGeneration Exp
746749mkPrimitiveFunction op args =
747− (\ args -> (primFnType ~> opName op) args)
750+ (\ args -> (primFnType ~> opName op) (endiannessArguments op ++ args))
748751 <$> sequence (zipWith (\ a t -> (Just t) <>@! a) args (sourceTypes op))
749752
750753mkThread :: LVar -> CodeGeneration Exp
src/IRTS/Java/JTypes.hs+31
@@ -33,6 +33,9 @@ doubleType = PrimType DoubleT
3333array :: J.Type -> J.Type
3434array t = RefType . ArrayType $ t
3535
36+addressType :: J.Type
37+addressType = longType
38+
3639-----------------------------------------------------------------------
3740-- Boxed types
3841
@@ -48,6 +51,10 @@ stringType :: J.Type
4851stringType =
4952 RefType . ClassRefType $ ClassType [(Ident "String", [])]
5053
54+bufferType :: J.Type
55+bufferType =
56+ RefType . ClassRefType $ ClassType [(Ident "ByteBuffer", [])]
57+
5158threadType :: J.Type
5259threadType =
5360 RefType . ClassRefType $ ClassType [(Ident "Thread", [])]
@@ -132,6 +139,9 @@ runtimeExceptionType :: J.Type
132139runtimeExceptionType =
133140 RefType . ClassRefType $ ClassType [(Ident "RuntimeException", [])]
134141
142+-----------------------------------------------------------------------
143+-- Integer types
144+
135145nativeTyToJType :: NativeTy -> J.Type
136146nativeTyToJType IT8 = byteType
137147nativeTyToJType IT16 = shortType
@@ -219,6 +229,7 @@ opName x
219229 | (LFloatInt to) <- x = "LFloatInt" ++ (suffixFor to)
220230 | (LStrInt to) <- x = "LStrInt" ++ (suffixFor to)
221231 | (LChInt to) <- x = "LChInt" ++ (suffixFor to)
232+ | (LPeek to _) <- x = "LPeek" ++ (suffixFor to)
222233 | otherwise = takeWhile ((/=) ' ') $ show x
223234 where
224235 suffixFor (ITFixed nt) = show nt
@@ -291,10 +302,30 @@ sourceTypes (LStrRev) = [stringType]
291302sourceTypes (LStdIn) = []
292303sourceTypes (LStdOut) = []
293304sourceTypes (LStdErr) = []
305+sourceTypes (LAllocate) = [addressType]
306+sourceTypes (LAppendBuffer) =
307+ [bufferType, addressType, addressType, addressType, addressType, bufferType]
308+sourceTypes (LSystemInfo) = [integerType]
309+sourceTypes (LAppend nt _) = [bufferType, addressType, addressType, intTyToJType nt]
310+sourceTypes (LPeek _ _) = [bufferType, addressType]
294311sourceTypes (LFork) = [objectType]
295312sourceTypes (LPar) = [objectType]
296313sourceTypes (LVMPtr) = []
297314sourceTypes (LNullPtr) = [objectType]
298315sourceTypes (LNoOp) = repeat objectType
299316
317+-----------------------------------------------------------------------
318+-- Endianess markers
300319
320+endiannessConstant :: Endianness -> Exp
321+endiannessConstant c =
322+ ExpName . Name . map Ident $ ["java", "nio", "ByteOrder", endiannessConstant' c]
323+ where
324+ endiannessConstant' BE = "BIG_ENDIAN"
325+ endiannessConstant' LE = "LITTLE_ENDIAN"
326+ endiannessConstant' (IRTS.Lang.Native) = endiannessConstant' BE
327+
328+endiannessArguments :: PrimFn -> [Exp]
329+endiannessArguments (LAppend _ end) = [endiannessConstant end]
330+endiannessArguments (LPeek _ end) = [endiannessConstant end]
331+endiannessArguments _ = []
src/IRTS/Java/Pom.hs+7−1
@@ -3,6 +3,9 @@ module IRTS.Java.Pom (pomString) where
33import Data.List (unfoldr)
44import Text.XML.Light
55
6+-----------------------------------------------------------------------
7+-- String <-> XML processing
8+
69uattr :: String -> String -> Attr
710uattr k v = Attr (QName k Nothing Nothing) v
811
@@ -31,6 +34,9 @@ groupArtifactVersion g a v = [
3134pomString :: String -> String -> [String] -> String
3235pomString c a d = ppElement $ pom c a d
3336
37+-----------------------------------------------------------------------
38+-- The pom template for idris projects
39+
3440pom :: String -> String -> [String] -> Element
3541pom clsName artifactName dependencies = unode "project" ([
3642 uattr "xmlns" "http://maven.apache.org/POM/4.0.0",
@@ -49,7 +55,7 @@ pom clsName artifactName dependencies = unode "project" ([
4955 unode "skipTest" "true"
5056 ],
5157 unode "dependencies" (
52− dependency "org.idris-lang" "idris" "0.9.10-alpha-2" :
58+ dependency "org.idris-lang" "idris" "0.9.14" :
5359 map parseToDep dependencies
5460 ),
5561 unode "build" [
src/Idris/AbsSyntax.hs+9−8
@@ -278,7 +278,7 @@ addNameHint ty n
278278 ty' <- case lookupCtxtName ty (idris_implicits i) of
279279 [(tyn, _)] -> return tyn
280280 [] -> throwError (NoSuchVariable ty)
281− tyns -> throwError (CantResolveAlts (map show (map fst tyns)))
281+ tyns -> throwError (CantResolveAlts (map fst tyns))
282282 let ns' = case lookupCtxt ty' (idris_namehints i) of
283283 [ns] -> ns ++ [n]
284284 _ -> [n]
@@ -778,13 +778,14 @@ setColour :: ColourType -> IdrisColour -> Idris ()
778778setColour ct c = do i <- getIState
779779 let newTheme = setColour' ct c (idris_colourTheme i)
780780 putIState $ i { idris_colourTheme = newTheme }
781− where setColour' KeywordColour c t = t { keywordColour = c }
782− setColour' BoundVarColour c t = t { boundVarColour = c }
783− setColour' ImplicitColour c t = t { implicitColour = c }
784− setColour' FunctionColour c t = t { functionColour = c }
785− setColour' TypeColour c t = t { typeColour = c }
786− setColour' DataColour c t = t { dataColour = c }
787− setColour' PromptColour c t = t { promptColour = c }
781+ where setColour' KeywordColour c t = t { keywordColour = c }
782+ setColour' BoundVarColour c t = t { boundVarColour = c }
783+ setColour' ImplicitColour c t = t { implicitColour = c }
784+ setColour' FunctionColour c t = t { functionColour = c }
785+ setColour' TypeColour c t = t { typeColour = c }
786+ setColour' DataColour c t = t { dataColour = c }
787+ setColour' PromptColour c t = t { promptColour = c }
788+ setColour' PostulateColour c t = t { postulateColour = c }
788789
789790logLvl :: Int -> String -> Idris ()
790791logLvl l str = do i <- getIState
src/Idris/AbsSyntaxTree.hs+37−26
@@ -485,18 +485,20 @@ dictionary = elem Dictionary
485485
486486
487487-- | Data declaration options
488−data DataOpt = Codata -- Set if the the data-type is coinductive
489− | DefaultEliminator -- Set if an eliminator should be generated for data type
488+data DataOpt = Codata -- ^ Set if the the data-type is coinductive
489+ | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
490+ | DefaultCaseFun -- ^ Set if a case function should be generated for data type
490491 | DataErrRev
491492 deriving (Show, Eq)
492493
493494type DataOpts = [DataOpt]
494495
495496-- | Type provider - what to provide
496−data ProvideWhat = ProvTerm -- ^ only allow providing terms
497− | ProvPostulate -- ^ only allow postulates
498− | ProvAny -- ^ either is ok
499− deriving (Show, Eq)
497+data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
498+ | ProvPostulate t -- ^ goal type must be Type, so only term
499+ deriving (Show, Eq, Functor)
500+
501+type ProvideWhat = ProvideWhat' PTerm
500502
501503-- | Top-level declarations such as compiler directives, definitions,
502504-- datatypes and typeclasses.
@@ -530,7 +532,7 @@ data PDecl' t
530532 | PSyntax FC Syntax -- ^ Syntax definition
531533 | PMutual FC [PDecl' t] -- ^ Mutual block
532534 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
533− | PProvider SyntaxInfo FC ProvideWhat Name t t -- ^ Type provider. The first t is the type, the second is the term
535+ | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
534536 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
535537 -- bool is True, lhs and rhs must be convertible
536538 deriving Functor
@@ -738,7 +740,8 @@ mapPT f t = f (mpt t) where
738740
739741data PTactic' t = Intro [Name] | Intros | Focus Name
740742 | Refine Name [Bool] | Rewrite t | DoUnify
741− | Induction Name
743+ | Induction t
744+ | CaseTac t
742745 | Equiv t
743746 | MatchRefine Name
744747 | LetTac Name t | LetTacTy Name t t
@@ -903,7 +906,8 @@ data DSL' t = DSL { dsl_bind :: t,
903906 index_first :: Maybe t,
904907 index_next :: Maybe t,
905908 dsl_lambda :: Maybe t,
906− dsl_let :: Maybe t
909+ dsl_let :: Maybe t,
910+ dsl_pi :: Maybe t
907911 }
908912 deriving (Show, Functor)
909913{-!
@@ -947,6 +951,7 @@ initDSL = DSL (PRef f (sUN ">>="))
947951 Nothing
948952 Nothing
949953 Nothing
954+ Nothing
950955 where f = fileFC "(builtin)"
951956
952957data Using = UImplicit Name PTerm
@@ -1149,15 +1154,20 @@ consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
11491154consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
11501155 theme = idris_colourTheme ist
11511156 in case () of
1152− _ | isDConName n ctxt -> colouriseData theme
1153− _ | isFnName n ctxt -> colouriseFun theme
1154− _ | isTConName n ctxt -> colouriseType theme
1155− _ | otherwise -> id -- don't colourise unknown names
1157+ _ | isDConName n ctxt -> colouriseData theme
1158+ _ | isFnName n ctxt -> colouriseFun theme
1159+ _ | isTConName n ctxt -> colouriseType theme
1160+ _ | isPostulateName n ist -> colourisePostulate theme
1161+ _ | otherwise -> id -- don't colourise unknown names
11561162consoleDecorate ist (AnnFC _) = id
11571163consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
11581164 where colour BoldText = IdrisColour Nothing True False True False
11591165 colour UnderlineText = IdrisColour Nothing True True False False
11601166 colour ItalicText = IdrisColour Nothing True False False True
1167+consoleDecorate ist (AnnTerm _ _) = id
1168+
1169+isPostulateName :: Name -> IState -> Bool
1170+isPostulateName n ist = S.member n (idris_postulates ist)
11611171
11621172-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
11631173prettyImp :: PPOption -- ^^ pretty printing options
@@ -1165,6 +1175,8 @@ prettyImp :: PPOption -- ^^ pretty printing options
11651175 -> Doc OutputAnnotation
11661176prettyImp impl = pprintPTerm impl [] [] []
11671177
1178+-- | Serialise something to base64 using its Binary instance.
1179+
11681180-- | Do the right thing for rendering a term in an IState
11691181prettyIst :: IState -> PTerm -> Doc OutputAnnotation
11701182prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
@@ -1185,7 +1197,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
11851197 prettySe p bnd e
11861198 | Just str <- slist p bnd e = str
11871199 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1188− prettySe p bnd (PRef fc n) = prettyNamePossParen True (ppopt_impl ppo) bnd n
1200+ prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
11891201 prettySe p bnd (PLam n ty sc) =
11901202 bracket p 2 . group . align . hang 2 $
11911203 text "\\" <> bindingOf n False <+> text "=>" <$>
@@ -1229,9 +1241,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
12291241 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
12301242 | UN nm <- basename f
12311243 , not (ppopt_impl ppo) && null (getExps args) =
1232− prettyNamePossParen True (ppopt_impl ppo) bnd f
1244+ prettyName True (ppopt_impl ppo) bnd f
12331245 prettySe p bnd (PAppBind _ (PRef _ f) [])
1234− | not (ppopt_impl ppo) = text "!" <> prettyNamePossParen True (ppopt_impl ppo) bnd f
1246+ | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
12351247 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
12361248 | UN nm <- basename op
12371249 , not (tnull nm) &&
@@ -1244,7 +1256,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
12441256 (l:r:rest) -> bracket p 1 $
12451257 enclose lparen rparen (inFix l r) <+>
12461258 align (group (vsep (map (prettyArgSe bnd) rest)))
1247− where opName isPrefix = prettyNamePossParen isPrefix (ppopt_impl ppo) bnd op
1259+ where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
12481260 f = getFixity (opStr op)
12491261 left l = case f of
12501262 Nothing -> prettySe (-1) bnd l
@@ -1422,7 +1434,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
14221434
14231435prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation
14241436prettyDocumentedIst ist (name, ty, docs) =
1425− prettyNamePossParen True True [] name <+> colon <+> align (prettyIst ist ty) <$>
1437+ prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
14261438 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)
14271439
14281440-- | Pretty-printer helper for the binding site of a name
@@ -1432,13 +1444,13 @@ bindingOf :: Name -- ^^ the bound name
14321444bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
14331445
14341446-- | Pretty-printer helper for names that attaches the correct annotations
1435−prettyNamePossParen
1447+prettyName
14361448 :: Bool -- ^^ whether the name should be parenthasized if it is an infix operator
14371449 -> Bool -- ^^ whether to show namespaces
14381450 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
14391451 -> Name -- ^^ the name to pprint
14401452 -> Doc OutputAnnotation
1441−prettyNamePossParen infixParen showNS bnd n
1453+prettyName infixParen showNS bnd n
14421454 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
14431455 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
14441456 where fullName = text nameSpace <> parenthasize (text (baseName n))
@@ -1456,10 +1468,6 @@ prettyNamePossParen infixParen showNS bnd n
14561468 parenthasize = if isInfix && infixParen then enclose lparen rparen else id
14571469
14581470
1459−prettyName :: Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
1460−prettyName = prettyNamePossParen False
1461−
1462−
14631471showCImp :: PPOption -> PClause -> Doc OutputAnnotation
14641472showCImp ppo (PClause _ n l ws r w)
14651473 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
@@ -1478,7 +1486,7 @@ showCImp ppo (PWith _ n l ws r w)
14781486showDImp :: PPOption -> PData -> Doc OutputAnnotation
14791487showDImp ppo (PDatadecl n ty cons)
14801488 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1481− (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyNamePossParen True False [] n <+> colon <+> prettyImp ppo t) cons))
1489+ (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
14821490
14831491showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
14841492showDecls o ds = vsep (map (showDeclImp o) ds)
@@ -1666,7 +1674,10 @@ namesIn uvars ist tm = nub $ ni [] tm
16661674 _ -> if n `elem` (map fst uvars) then [n] else []
16671675 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
16681676 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1669− ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1677+ ni env (PCase _ c os) = ni env c ++
1678+ -- names in 'os', not counting the names bound in the cases
1679+ (nub (concatMap (ni env) (map snd os))
1680+ \\ nub (concatMap (ni env) (map fst os)))
16701681 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
16711682 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
16721683 ni env (PEq _ l r) = ni env l ++ ni env r
src/Idris/Colours.hs+15−8
@@ -2,7 +2,7 @@ module Idris.Colours (
22 IdrisColour(..),
33 ColourTheme(..),
44 defaultTheme,
5− colouriseKwd, colouriseBound, colouriseImplicit,
5+ colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate,
66 colouriseType, colouriseFun, colouriseData, colouriseKeyword,
77 colourisePrompt, colourise, ColourType(..)) where
88
@@ -19,13 +19,14 @@ data IdrisColour = IdrisColour { colour :: Maybe Color
1919mkColour :: Color -> IdrisColour
2020mkColour c = IdrisColour (Just c) True False False False
2121
22−data ColourTheme = ColourTheme { keywordColour :: IdrisColour
23− , boundVarColour :: IdrisColour
24− , implicitColour :: IdrisColour
25− , functionColour :: IdrisColour
26− , typeColour :: IdrisColour
27− , dataColour :: IdrisColour
28− , promptColour :: IdrisColour
22+data ColourTheme = ColourTheme { keywordColour :: IdrisColour
23+ , boundVarColour :: IdrisColour
24+ , implicitColour :: IdrisColour
25+ , functionColour :: IdrisColour
26+ , typeColour :: IdrisColour
27+ , dataColour :: IdrisColour
28+ , promptColour :: IdrisColour
29+ , postulateColour :: IdrisColour
2930 }
3031 deriving (Eq, Show)
3132
@@ -38,6 +39,7 @@ defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True False True
3839 , typeColour = mkColour Blue
3940 , dataColour = mkColour Red
4041 , promptColour = IdrisColour Nothing True False True False
42+ , postulateColour = IdrisColour (Just Green) True False True False
4143 }
4244
4345-- | Set the colour of a string using POSIX escape codes
@@ -74,6 +76,10 @@ colourisePrompt t = colourise (promptColour t)
7476colouriseKeyword :: ColourTheme -> String -> String
7577colouriseKeyword t = colourise (keywordColour t)
7678
79+colourisePostulate :: ColourTheme -> String -> String
80+colourisePostulate t = colourise (postulateColour t)
81+
82+
7783data ColourType = KeywordColour
7884 | BoundVarColour
7985 | ImplicitColour
@@ -81,4 +87,5 @@ data ColourType = KeywordColour
8187 | TypeColour
8288 | DataColour
8389 | PromptColour
90+ | PostulateColour
8491 deriving (Eq, Show, Bounded, Enum)
src/Idris/Completion.hs+2−1
@@ -44,7 +44,8 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
4444 , ("reflect", Just ExprTArg)
4545 , ("fill", Just ExprTArg)
4646 , ("try", Just AltsTArg)
47− , ("induction", Just NameTArg)
47+ , ("induction", Just ExprTArg)
48+ , ("case", Just ExprTArg)
4849 , (":t", Just ExprTArg)
4950 , (":type", Just ExprTArg)
5051 , (":e", Just ExprTArg)
src/Idris/Core/Binary.hsnew file+356
@@ -0,0 +1,356 @@
1+{-| Binary instances for the core datatypes -}
2+module Idris.Core.Binary where
3+
4+import Data.Binary
5+import Data.Vector.Binary
6+import qualified Data.Text as T
7+
8+import Idris.Core.TT
9+
10+----- Generated by 'derive'
11+
12+instance Binary FC where
13+ put (FC x1 (x2, x3) (x4, x5))
14+ = do put x1
15+ put (x2 * 65536 + x3)
16+ put (x4 * 65536 + x5)
17+ get
18+ = do x1 <- get
19+ x2x3 <- get
20+ x4x5 <- get
21+ return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))
22+
23+
24+instance Binary Name where
25+ put x
26+ = case x of
27+ UN x1 -> do putWord8 0
28+ put x1
29+ NS x1 x2 -> do putWord8 1
30+ put x1
31+ put x2
32+ MN x1 x2 -> do putWord8 2
33+ put x1
34+ put x2
35+ NErased -> putWord8 3
36+ SN x1 -> do putWord8 4
37+ put x1
38+ SymRef x1 -> do putWord8 5
39+ put x1
40+ get
41+ = do i <- getWord8
42+ case i of
43+ 0 -> do x1 <- get
44+ return (UN x1)
45+ 1 -> do x1 <- get
46+ x2 <- get
47+ return (NS x1 x2)
48+ 2 -> do x1 <- get
49+ x2 <- get
50+ return (MN x1 x2)
51+ 3 -> return NErased
52+ 4 -> do x1 <- get
53+ return (SN x1)
54+ 5 -> do x1 <- get
55+ return (SymRef x1)
56+ _ -> error "Corrupted binary data for Name"
57+
58+instance Binary T.Text where
59+ put x = put (str x)
60+ get = do x <- get
61+ return (txt x)
62+
63+instance Binary SpecialName where
64+ put x
65+ = case x of
66+ WhereN x1 x2 x3 -> do putWord8 0
67+ put x1
68+ put x2
69+ put x3
70+ InstanceN x1 x2 -> do putWord8 1
71+ put x1
72+ put x2
73+ ParentN x1 x2 -> do putWord8 2
74+ put x1
75+ put x2
76+ MethodN x1 -> do putWord8 3
77+ put x1
78+ CaseN x1 -> do putWord8 4; put x1
79+ ElimN x1 -> do putWord8 5; put x1
80+ InstanceCtorN x1 -> do putWord8 6; put x1
81+ get
82+ = do i <- getWord8
83+ case i of
84+ 0 -> do x1 <- get
85+ x2 <- get
86+ x3 <- get
87+ return (WhereN x1 x2 x3)
88+ 1 -> do x1 <- get
89+ x2 <- get
90+ return (InstanceN x1 x2)
91+ 2 -> do x1 <- get
92+ x2 <- get
93+ return (ParentN x1 x2)
94+ 3 -> do x1 <- get
95+ return (MethodN x1)
96+ 4 -> do x1 <- get
97+ return (CaseN x1)
98+ 5 -> do x1 <- get
99+ return (ElimN x1)
100+ 6 -> do x1 <- get
101+ return (InstanceCtorN x1)
102+ _ -> error "Corrupted binary data for SpecialName"
103+
104+
105+instance Binary Const where
106+ put x
107+ = case x of
108+ I x1 -> do putWord8 0
109+ put x1
110+ BI x1 -> do putWord8 1
111+ put x1
112+ Fl x1 -> do putWord8 2
113+ put x1
114+ Ch x1 -> do putWord8 3
115+ put x1
116+ Str x1 -> do putWord8 4
117+ put x1
118+ B8 x1 -> putWord8 5 >> put x1
119+ B16 x1 -> putWord8 6 >> put x1
120+ B32 x1 -> putWord8 7 >> put x1
121+ B64 x1 -> putWord8 8 >> put x1
122+
123+ (AType (ATInt ITNative)) -> putWord8 9
124+ (AType (ATInt ITBig)) -> putWord8 10
125+ (AType ATFloat) -> putWord8 11
126+ (AType (ATInt ITChar)) -> putWord8 12
127+ StrType -> putWord8 13
128+ PtrType -> putWord8 14
129+ Forgot -> putWord8 15
130+ (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive
131+ (AType (ATInt (ITVec ity count))) -> do
132+ putWord8 20
133+ putWord8 (fromIntegral . fromEnum $ ity)
134+ putWord8 (fromIntegral count)
135+
136+ B8V x1 -> putWord8 21 >> put x1
137+ B16V x1 -> putWord8 22 >> put x1
138+ B32V x1 -> putWord8 23 >> put x1
139+ B64V x1 -> putWord8 24 >> put x1
140+ BufferType -> putWord8 25
141+ ManagedPtrType -> putWord8 26
142+ get
143+ = do i <- getWord8
144+ case i of
145+ 0 -> do x1 <- get
146+ return (I x1)
147+ 1 -> do x1 <- get
148+ return (BI x1)
149+ 2 -> do x1 <- get
150+ return (Fl x1)
151+ 3 -> do x1 <- get
152+ return (Ch x1)
153+ 4 -> do x1 <- get
154+ return (Str x1)
155+ 5 -> fmap B8 get
156+ 6 -> fmap B16 get
157+ 7 -> fmap B32 get
158+ 8 -> fmap B64 get
159+
160+ 9 -> return (AType (ATInt ITNative))
161+ 10 -> return (AType (ATInt ITBig))
162+ 11 -> return (AType ATFloat)
163+ 12 -> return (AType (ATInt ITChar))
164+ 13 -> return StrType
165+ 14 -> return PtrType
166+ 15 -> return Forgot
167+
168+ 16 -> return (AType (ATInt (ITFixed IT8)))
169+ 17 -> return (AType (ATInt (ITFixed IT16)))
170+ 18 -> return (AType (ATInt (ITFixed IT32)))
171+ 19 -> return (AType (ATInt (ITFixed IT64)))
172+
173+ 20 -> do
174+ e <- getWord8
175+ c <- getWord8
176+ return (AType (ATInt (ITVec (toEnum . fromIntegral $ e) (fromIntegral c))))
177+
178+ 21 -> fmap B8V get
179+ 22 -> fmap B16V get
180+ 23 -> fmap B32V get
181+ 24 -> fmap B64V get
182+ 25 -> return BufferType
183+ 26 -> return ManagedPtrType
184+
185+ _ -> error "Corrupted binary data for Const"
186+
187+
188+instance Binary Raw where
189+ put x
190+ = case x of
191+ Var x1 -> do putWord8 0
192+ put x1
193+ RBind x1 x2 x3 -> do putWord8 1
194+ put x1
195+ put x2
196+ put x3
197+ RApp x1 x2 -> do putWord8 2
198+ put x1
199+ put x2
200+ RType -> putWord8 3
201+ RConstant x1 -> do putWord8 4
202+ put x1
203+ RForce x1 -> do putWord8 5
204+ put x1
205+ get
206+ = do i <- getWord8
207+ case i of
208+ 0 -> do x1 <- get
209+ return (Var x1)
210+ 1 -> do x1 <- get
211+ x2 <- get
212+ x3 <- get
213+ return (RBind x1 x2 x3)
214+ 2 -> do x1 <- get
215+ x2 <- get
216+ return (RApp x1 x2)
217+ 3 -> return RType
218+ 4 -> do x1 <- get
219+ return (RConstant x1)
220+ 5 -> do x1 <- get
221+ return (RForce x1)
222+ _ -> error "Corrupted binary data for Raw"
223+
224+
225+instance (Binary b) => Binary (Binder b) where
226+ put x
227+ = case x of
228+ Lam x1 -> do putWord8 0
229+ put x1
230+ Pi x1 -> do putWord8 1
231+ put x1
232+ Let x1 x2 -> do putWord8 2
233+ put x1
234+ put x2
235+ NLet x1 x2 -> do putWord8 3
236+ put x1
237+ put x2
238+ Hole x1 -> do putWord8 4
239+ put x1
240+ GHole x1 x2 -> do putWord8 5
241+ put x1
242+ put x2
243+ Guess x1 x2 -> do putWord8 6
244+ put x1
245+ put x2
246+ PVar x1 -> do putWord8 7
247+ put x1
248+ PVTy x1 -> do putWord8 8
249+ put x1
250+ get
251+ = do i <- getWord8
252+ case i of
253+ 0 -> do x1 <- get
254+ return (Lam x1)
255+ 1 -> do x1 <- get
256+ return (Pi x1)
257+ 2 -> do x1 <- get
258+ x2 <- get
259+ return (Let x1 x2)
260+ 3 -> do x1 <- get
261+ x2 <- get
262+ return (NLet x1 x2)
263+ 4 -> do x1 <- get
264+ return (Hole x1)
265+ 5 -> do x1 <- get
266+ x2 <- get
267+ return (GHole x1 x2)
268+ 6 -> do x1 <- get
269+ x2 <- get
270+ return (Guess x1 x2)
271+ 7 -> do x1 <- get
272+ return (PVar x1)
273+ 8 -> do x1 <- get
274+ return (PVTy x1)
275+ _ -> error "Corrupted binary data for Binder"
276+
277+
278+instance Binary NameType where
279+ put x
280+ = case x of
281+ Bound -> putWord8 0
282+ Ref -> putWord8 1
283+ DCon x1 x2 -> do putWord8 2
284+ put (x1 * 65536 + x2)
285+ TCon x1 x2 -> do putWord8 3
286+ put (x1 * 65536 + x2)
287+ get
288+ = do i <- getWord8
289+ case i of
290+ 0 -> return Bound
291+ 1 -> return Ref
292+ 2 -> do x1x2 <- get
293+ return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
294+ 3 -> do x1x2 <- get
295+ return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
296+ _ -> error "Corrupted binary data for NameType"
297+
298+
299+instance {- (Binary n) => -} Binary (TT Name) where
300+ put x
301+ = {-# SCC "putTT" #-}
302+ case x of
303+ P x1 x2 x3 -> do putWord8 0
304+ put x1
305+ put x2
306+-- put x3
307+ V x1 -> if (x1 >= 0 && x1 < 256)
308+ then do putWord8 1
309+ putWord8 (toEnum (x1 + 1))
310+ else do putWord8 9
311+ put x1
312+ Bind x1 x2 x3 -> do putWord8 2
313+ put x1
314+ put x2
315+ put x3
316+ App x1 x2 -> do putWord8 3
317+ put x1
318+ put x2
319+ Constant x1 -> do putWord8 4
320+ put x1
321+ Proj x1 x2 -> do putWord8 5
322+ put x1
323+ putWord8 (toEnum (x2 + 1))
324+ Erased -> putWord8 6
325+ TType x1 -> do putWord8 7
326+ put x1
327+ Impossible -> putWord8 8
328+ get
329+ = do i <- getWord8
330+ case i of
331+ 0 -> do x1 <- get
332+ x2 <- get
333+-- x3 <- get
334+ return (P x1 x2 Erased)
335+ 1 -> do x1 <- getWord8
336+ return (V ((fromEnum x1) - 1))
337+ 2 -> do x1 <- get
338+ x2 <- get
339+ x3 <- get
340+ return (Bind x1 x2 x3)
341+ 3 -> do x1 <- get
342+ x2 <- get
343+ return (App x1 x2)
344+ 4 -> do x1 <- get
345+ return (Constant x1)
346+ 5 -> do x1 <- get
347+ x2 <- getWord8
348+ return (Proj x1 ((fromEnum x2)-1))
349+ 6 -> return Erased
350+ 7 -> do x1 <- get
351+ return (TType x1)
352+ 8 -> return Impossible
353+ 9 -> do x1 <- get
354+ return (V x1)
355+ _ -> error "Corrupted binary data for TT"
356+
src/Idris/Core/CaseTree.hs+3
@@ -336,6 +336,9 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
336336toPat :: Bool -> Bool -> [Term] -> [Pat]
337337toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
338338 where
339+ toPat' (P (DCon t a) nm@(UN n) _) [_,_,arg]
340+ | n == txt "Delay" = do arg' <- toPat' arg []
341+ return $ PCon nm t [PAny, PAny, arg']
339342 toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args
340343 return $ PCon n t args'
341344 -- n + 1
src/Idris/Core/Elaborate.hs+7−4
@@ -371,8 +371,11 @@ expandLet n v = processTactic' (ExpandLet n v)
371371rewrite :: Raw -> Elab' aux ()
372372rewrite tm = processTactic' (Rewrite tm)
373373
374−induction :: Name -> Elab' aux ()
375−induction nm = processTactic' (Induction nm)
374+induction :: Raw -> Elab' aux ()
375+induction tm = processTactic' (Induction tm)
376+
377+casetac :: Raw -> Elab' aux ()
378+casetac tm = processTactic' (CaseTac tm)
376379
377380equiv :: Raw -> Elab' aux ()
378381equiv tm = processTactic' (Equiv tm)
@@ -709,7 +712,7 @@ tryWhen False a b = a
709712
710713
711714-- Try a selection of tactics. Exactly one must work, all others must fail
712−tryAll :: [(Elab' aux a, String)] -> Elab' aux a
715+tryAll :: [(Elab' aux a, Name)] -> Elab' aux a
713716tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs
714717 where
715718 cantResolve :: Elab' aux a
@@ -718,7 +721,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs
718721 tryAll' :: [Elab' aux a] -> -- successes
719722 Int -> -- most problems
720723 (Elab' aux a, Int) -> -- smallest failure
721− [(Elab' aux a, String)] -> -- still to try
724+ [(Elab' aux a, Name)] -> -- still to try
722725 Elab' aux a
723726 tryAll' [res] pmax _ [] = res
724727 tryAll' (_:_) pmax _ [] = cantResolve
src/Idris/Core/Evaluate.hs+23−5
@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
88 Context, initContext, ctxtAlist, uconstraints, next_tvar,
99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
1010 addDatatype, addCasedef, simplifyCasedef, addOperator,
11− lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,
11+ lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,
1212 mapDefCtxt,
1313 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
1414 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where
@@ -868,14 +868,32 @@ lookupNames n ctxt
868868 = let ns = lookupCtxtName n (definitions ctxt) in
869869 map fst ns
870870
871−lookupTy :: Name -> Context -> [Type]
872−lookupTy n ctxt
873− = do def <- lookupCtxt n (definitions ctxt)
874− case tfst def of
871+-- | Get the list of pairs of fully-qualified names and their types that match some name
872+lookupTyName :: Name -> Context -> [(Name, Type)]
873+lookupTyName n ctxt = do
874+ (name, def) <- lookupCtxtName n (definitions ctxt)
875+ ty <- case tfst def of
875876 (Function ty _) -> return ty
876877 (TyDecl _ ty) -> return ty
877878 (Operator ty _ _) -> return ty
878879 (CaseOp _ ty _ _ _ _) -> return ty
880+ return (name, ty)
881+
882+-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.
883+lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)
884+lookupTyNameExact n ctxt = case lookupTyName n ctxt of
885+ [x] -> Just x
886+ _ -> Nothing
887+
888+-- | Get the types that match some name
889+lookupTy :: Name -> Context -> [Type]
890+lookupTy n ctxt = map snd (lookupTyName n ctxt)
891+
892+-- | Get the single type that matches some name precisely
893+lookupTyExact :: Name -> Context -> Maybe Type
894+lookupTyExact n ctxt = case lookupTy n ctxt of
895+ [t] -> Just t
896+ _ -> Nothing
879897
880898isConName :: Name -> Context -> Bool
881899isConName n ctxt = isTConName n ctxt || isDConName n ctxt
src/Idris/Core/ProofState.hs+26−12
@@ -72,7 +72,8 @@ data Tactic = Attack
7272 | LetBind Name Raw Raw
7373 | ExpandLet Name Term
7474 | Rewrite Raw
75− | Induction Name
75+ | Induction Raw
76+ | CaseTac Raw
7677 | Equiv Raw
7778 | PatVar Name
7879 | PatBind Name
@@ -661,13 +662,16 @@ mkP lt l r (Bind n b sc)
661662 b { binderTy = ty' }
662663mkP lt l r x = x
663664
664−induction :: Name -> RunTactic
665−induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
666− (tmv, tmt) <- lift $ check ctxt env (Var nm)
665+casetac :: Raw -> Bool -> RunTactic
666+casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
667+ (tmv, tmt) <- lift $ check ctxt env tm
667668 let tmt' = normalise ctxt env tmt
669+ let (tacn, tacstr, tactt) = if induction
670+ then (ElimN, "an eliminator", "induction")
671+ else (CaseN, "a case function", "case analysis")
668672 case unApply tmt' of
669673 (P _ tnm _, tyargs) -> do
670− case lookupTy (SN (ElimN tnm)) ctxt of
674+ case lookupTy (SN (tacn tnm)) ctxt of
671675 [elimTy] -> do
672676 param_pos <- case lookupMetaInformation tnm ctxt of
673677 [DataMI param_pos] -> return param_pos
@@ -683,9 +687,14 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
683687 let indxargs = drop (length restargs - length indicies) $ restargs
684688 let scr = last $ tail args'
685689 let indxnames = makeIndexNames indicies
686− prop <- replaceIndicies indxnames indicies $ Bind nm (Lam tmt') t
690+ currentNames <- query $ allTTNames . pterm
691+ let tmnm = case tm of
692+ Var nm -> uniqueNameCtxt ctxt nm currentNames
693+ _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames
694+ let tmvar = P Bound tmnm tmt'
695+ prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)
687696 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (pterm ps)) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (pterm ps))) consargs)
688− let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0)))
697+ let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))
689698 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))
690699 action (\ps -> ps {holes = holes ps \\ [x]})
691700 mapM_ addConsHole (reverse consargs')
@@ -693,9 +702,9 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
693702 (scv, sct) <- lift $ check ctxt env res'
694703 let scv' = specialise ctxt env [] scv
695704 return scv'
696− [] -> fail $ "Induction needs an eliminator for " ++ show tnm
697− xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show tnm
698− _ -> fail "Unkown type for induction"
705+ [] -> fail $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm
706+ xs -> fail $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
707+ _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"
699708 where scname = sMN 0 "scarg"
700709 makeConsArg (nm, ty) = P Bound nm ty
701710 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
@@ -709,7 +718,7 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
709718 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)
710719 let var = P Bound idnm idxt
711720 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs
712−induction tm ctxt env _ = do fail "Can't do induction here"
721+induction tm induction ctxt env _ = do fail "Can't do induction here"
713722
714723
715724equiv :: Raw -> RunTactic
@@ -823,6 +832,10 @@ updateEnv ns [] = []
823832updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
824833
825834updateError [] err = err
835+updateError ns (At f e) = At f (updateError ns e)
836+updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)
837+updateError ns (ElaboratingArg f a env e)
838+ = ElaboratingArg f a env (updateError ns e)
826839updateError ns (CantUnify b l r e xs sc)
827840 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
828841updateError ns e = e
@@ -987,7 +1000,8 @@ process t h = tactic (Just h) (mktac t)
9871000 mktac (LetBind n t v) = letbind n t v
9881001 mktac (ExpandLet n b) = expandLet n b
9891002 mktac (Rewrite t) = rewrite t
990− mktac (Induction t) = induction t
1003+ mktac (Induction t) = casetac t True
1004+ mktac (CaseTac t) = casetac t False
9911005 mktac (Equiv t) = equiv t
9921006 mktac (PatVar n) = patvar n
9931007 mktac (PatBind n) = patbind n
src/Idris/Core/TT.hs+3−2
@@ -83,7 +83,7 @@ instance Show FC where
8383 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec
8484
8585-- | Output annotation for pretty-printed name - decides colour
86−data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput
86+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput
8787
8888-- | Text formatting output
8989data TextFormatting = BoldText | ItalicText | UnderlineText
@@ -99,6 +99,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St
9999 | AnnKeyword
100100 | AnnFC FC
101101 | AnnTextFmt TextFormatting
102+ | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term
102103
103104-- | Used for error reflection
104105data ErrorReportPart = TextPart String
@@ -133,7 +134,7 @@ data Err' t
133134 | NoTypeDecl Name
134135 | NotInjective t t t
135136 | CantResolve t
136− | CantResolveAlts [String]
137+ | CantResolveAlts [Name]
137138 | IncompleteTerm t
138139 | UniverseError
139140 | ProgramLineComment
src/Idris/DSL.hs+8−1
@@ -29,6 +29,10 @@ expandDo dsl (PLet n ty v tm)
2929 = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in
3030 expandDo dsl sc
3131expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
32+expandDo dsl (PPi p n ty tm)
33+ | Just pi <- dsl_pi dsl
34+ = let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in
35+ expandDo dsl sc
3236expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
3337expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
3438 (map (fmap (expandDo dsl)) args)
@@ -88,7 +92,10 @@ var dsl n t i = v' i t where
8892 | Nothing <- dsl_let dsl
8993 = PLet n (v' i ty) (v' i val) (v' i sc)
9094 | otherwise = PLet n (v' i ty) (v' i val) (v' (i + 1) sc)
91− v' i (PPi p n ty sc) = PPi p n (v' i ty) (v' i sc)
95+ v' i (PPi p n ty sc)
96+ | Nothing <- dsl_pi dsl
97+ = PPi p n (v' i ty) (v' i sc)
98+ | otherwise = PPi p n (v' i ty) (v' (i+1) sc)
9299 v' i (PTyped l r) = PTyped (v' i l) (v' i r)
93100 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)
94101 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)
src/Idris/DeepSeq.hs+10−9
@@ -119,6 +119,7 @@ instance NFData FnOpt where
119119instance NFData DataOpt where
120120 rnf Codata = ()
121121 rnf DefaultEliminator = ()
122+ rnf DefaultCaseFun = ()
122123
123124instance (NFData t) => NFData (PDecl' t) where
124125 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
@@ -156,16 +157,14 @@ instance (NFData t) => NFData (PDecl' t) where
156157 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
157158 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
158159 rnf (PDirective x1) = ()
159− rnf (PProvider x1 x2 x3 x4 x5 x6)
160− = rnf x1 `seq`
161− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
160+ rnf (PProvider x1 x2 x3 x4)
161+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
162162 rnf (PTransform x1 x2 x3 x4)
163163 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
164164
165−instance NFData ProvideWhat where
166− rnf ProvAny = ()
167− rnf ProvTerm = ()
168− rnf ProvPostulate = ()
165+instance NFData t => NFData (ProvideWhat' t) where
166+ rnf (ProvTerm ty tm) = rnf ty `seq` rnf tm `seq` ()
167+ rnf (ProvPostulate tm) = rnf tm `seq` ()
169168
170169instance NFData PunInfo where
171170 rnf x = x `seq` ()
@@ -238,6 +237,7 @@ instance (NFData t) => NFData (PTactic' t) where
238237 rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
239238 rnf (Rewrite x1) = rnf x1 `seq` ()
240239 rnf (Induction x1) = rnf x1 `seq` ()
240+ rnf (CaseTac x1) = rnf x1 `seq` ()
241241 rnf (Equiv x1) = rnf x1 `seq` ()
242242 rnf (MatchRefine x1) = rnf x1 `seq` ()
243243 rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
@@ -293,12 +293,13 @@ instance NFData TypeInfo where
293293 rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
294294
295295instance (NFData t) => NFData (DSL' t) where
296− rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)
296+ rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
297297 = rnf x1 `seq`
298298 rnf x2 `seq`
299299 rnf x3 `seq`
300300 rnf x4 `seq`
301− rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()
301+ rnf x5 `seq`
302+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()
302303
303304instance NFData SynContext where
304305 rnf PatternSyntax = ()
src/Idris/Delaborate.hs+61−19
@@ -1,5 +1,5 @@
11{-# LANGUAGE PatternGuards #-}
2−module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pprintErr) where
2+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', fancifyAnnots, pprintDelab, pprintDelabTy, pprintErr) where
33
44-- Convert core TT back into high level syntax, primarily for display
55-- purposes.
@@ -9,6 +9,7 @@ import Util.Pretty
99import Idris.AbsSyntax
1010import Idris.Core.TT
1111import Idris.Core.Evaluate
12+import Idris.Docstrings (overview, renderDocstring)
1213import Idris.ErrReverse
1314
1415import Data.List (intersperse)
@@ -134,6 +135,20 @@ errorIndent = 8
134135indented :: Doc a -> Doc a
135136indented = nest errorIndent . (line <>)
136137
138+-- | Pretty-print a core term using delaboration
139+pprintDelab :: IState -> Term -> Doc OutputAnnotation
140+pprintDelab ist tm = annotate (AnnTerm [] tm)
141+ (prettyIst ist (delab ist tm))
142+
143+-- | Pretty-print the type of some name
144+pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
145+pprintDelabTy i n
146+ = case lookupTy n (tt_ctxt i) of
147+ (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
148+ case lookupCtxt n (idris_implicits i) of
149+ (imps:_) -> delabTy' i imps ty False False
150+ _ -> delabTy' i [] ty False False
151+
137152pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
138153pprintTerm ist = pprintTerm' ist []
139154
@@ -150,8 +165,8 @@ pprintErr' i (InternalMsg s) =
150165 text ("Please consider reporting at " ++ bugaddr)
151166 ]
152167pprintErr' i (CantUnify _ x y e sc s) =
153− text "Can't unify" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x)) <$>
154− text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y)) <>
168+ text "Can't unify" <> indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i x))) <$>
169+ text "with" <> indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) sc) (delab i y))) <>
155170 case e of
156171 Msg "" -> empty
157172 _ -> line <> line <> text "Specifically:" <>
@@ -159,46 +174,46 @@ pprintErr' i (CantUnify _ x y e sc s) =
159174 if (opt_errContext (idris_options i)) then showSc i sc else empty
160175pprintErr' i (CantConvert x y env) =
161176 text "Can't convert" <>
162− indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <$>
177+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <$>
163178 text "with" <>
164− indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y)) <>
179+ indented (annTm y (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i y))) <>
165180 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
166181pprintErr' i (CantSolveGoal x env) =
167182 text "Can't solve goal " <>
168− indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x)) <>
183+ indented (annTm x (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i x))) <>
169184 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
170185pprintErr' i (UnifyScope n out tm env) =
171186 text "Can't unify" <> indented (annName n) <+>
172− text "with" <> indented (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
173− text "as" <> indented (annName out) <> text "is not in scope" <>
187+ text "with" <> indented (annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm))) <+>
188+ text "as" <> indented (annName out) <> text "is not in scope" <>
174189 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
175190pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
176191pprintErr' i (NonFunctionType f ty) =
177− pprintTerm i (delab i f) <+>
192+ annTm f (pprintTerm i (delab i f)) <+>
178193 text "does not have a function type" <+>
179194 parens (pprintTerm i (delab i ty))
180195pprintErr' i (NotEquality tm ty) =
181− pprintTerm i (delab i tm) <+>
196+ annTm tm (pprintTerm i (delab i tm)) <+>
182197 text "does not have an equality type" <+>
183− parens (pprintTerm i (delab i ty))
198+ annTm ty (parens (pprintTerm i (delab i ty)))
184199pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
185200pprintErr' i (CantIntroduce ty) =
186− text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)
201+ text "Can't use lambda here: type is" <+> annTm ty (pprintTerm i (delab i ty))
187202pprintErr' i (InfiniteUnify x tm env) =
188203 text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+>
189− pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm) <+>
204+ annTm tm (pprintTerm' i (map (\ (n, b) -> (n, False)) env) (delab i tm)) <+>
190205 text "would lead to infinite value" <>
191206 if (opt_errContext (idris_options i)) then line <> showSc i env else empty
192207pprintErr' i (NotInjective p x y) =
193− text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>
194− text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>
195− pprintTerm i (delab i y)
208+ text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>
209+ text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>
210+ annTm y (pprintTerm i (delab i y))
196211pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
197212pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
198− align (cat (punctuate (comma <> space) (map text as)))
213+ align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))
199214pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
200215pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
201−pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)
216+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))
202217pprintErr' i UniverseError = text "Universe inconsistency"
203218pprintErr' i ProgramLineComment = text "Program line next to comment"
204219pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"
@@ -207,7 +222,7 @@ pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <
207222pprintErr' i (AlreadyDefined n) = annName n<+>
208223 text "is already defined"
209224pprintErr' i (ProofSearchFail e) = pprintErr' i e
210−pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> pprintTerm i (delab i tm)
225+pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> annTm tm (pprintTerm i (delab i tm))
211226pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
212227pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
213228 annName' n (showqual i n) <> colon <$>
@@ -258,6 +273,33 @@ annName n = annName' n (showbasic n)
258273annName' :: Name -> String -> Doc OutputAnnotation
259274annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)
260275
276+annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
277+annTm tm = annotate (AnnTerm [] tm)
278+
279+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
280+fancifyAnnots ist annot@(AnnName n _ _ _) =
281+ do let ctxt = tt_ctxt ist
282+ docs = docOverview ist n
283+ ty = Just (getTy ist n)
284+ case () of
285+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty
286+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty
287+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty
288+ _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty
289+ _ | isPostulateName n ist -> AnnName n (Just PostulateOutput) docs ty
290+ _ | otherwise -> annot
291+ where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
292+ docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)
293+ let o = overview (fst docs)
294+ -- TODO make width configurable
295+ out = displayS . renderPretty 1.0 50 $ renderDocstring o
296+ return (out "")
297+ getTy :: IState -> Name -> String -- fails if name not already extant!
298+ getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
299+ delabTy ist n
300+ in (displayS . renderPretty 1.0 50 $ theTy) ""
301+fancifyAnnots _ annot = annot
302+
261303showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation
262304showSc i [] = empty
263305showSc i xs = line <> line <> text "In context:" <>
src/Idris/Docs.hs+4−4
@@ -37,7 +37,7 @@ showDoc d | nullDocstring d = empty
3737
3838pprintFD :: IState -> FunDoc -> Doc OutputAnnotation
3939pprintFD ist (FD n doc args ty f)
40− = nest 4 (prettyNamePossParen True (ppopt_impl ppo) [] n <+> colon <+>
40+ = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>
4141 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
4242 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
4343 renderDocstring doc <$>
@@ -79,7 +79,7 @@ pprintDocs ist (DataDoc t args)
7979 else nest 4 (text "Constructors:" <> line <>
8080 vsep (map (pprintFD ist) args))
8181pprintDocs ist (ClassDoc n doc meths params instances superclasses)
82− = nest 4 (text "Type class" <+> prettyNamePossParen True (ppopt_impl ppo) [] n <>
82+ = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>
8383 if nullDocstring doc then empty else line <> renderDocstring doc)
8484 <> line <$>
8585 nest 4 (text "Parameters:" <$> prettyParameters)
@@ -131,8 +131,8 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)
131131 (subclasses, instances') = partition isSubclass instances
132132
133133 prettyParameters = if any (isJust . snd) params
134− then vsep (map (\(nm,md) -> prettyNamePossParen True False params' nm <+> maybe empty showDoc md) params)
135− else hsep (punctuate comma (map (prettyNamePossParen True False params' . fst) params))
134+ then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty showDoc md) params)
135+ else hsep (punctuate comma (map (prettyName True False params' . fst) params))
136136
137137getDocs :: Name -> Idris Docs
138138getDocs n
src/Idris/ElabDecls.hs+34−24
@@ -283,7 +283,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
283283
284284 -- create an eliminator
285285 when (DefaultEliminator `elem` opts) $
286− evalStateT (elabEliminator params n t dcons info) Map.empty
286+ evalStateT (elabCaseFun True params n t dcons info) Map.empty
287+ -- create a case function
288+ when (DefaultCaseFun `elem` opts) $
289+ evalStateT (elabCaseFun False params n t dcons info) Map.empty
287290 where
288291 setDetaggable :: Name -> Idris ()
289292 setDetaggable n = do
@@ -369,11 +372,13 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
369372type EliminatorState = StateT (Map.Map String Int) Idris
370373
371374-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
372−elabEliminator :: [Int] -> Name -> PTerm ->
375+-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function
376+-- rename to caseFun to match updated intend
377+elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->
373378 [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->
374379 ElabInfo -> EliminatorState ()
375−elabEliminator paramPos n ty cons info = do
376− elimLog $ "Elaborating eliminator"
380+elabCaseFun ind paramPos n ty cons info = do
381+ elimLog $ "Elaborating case function"
377382 put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))
378383 let (cnstrs, _) = splitPi ty
379384 let (splittedTy@(pms, idxs)) = splitPms cnstrs
@@ -381,7 +386,8 @@ elabEliminator paramPos n ty cons info = do
381386 motiveIdxs <- namePis False idxs
382387 let motive = mkMotive n paramPos generalParams motiveIdxs
383388 consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do
384− name <- freshName $ "elim_" ++ simpleName cnm
389+ let casefunt = if ind then "elim_" else "case_"
390+ name <- freshName $ casefunt ++ simpleName cnm
385391 consTerm <- extractConsTerm c generalParams
386392 return (name, expl, consTerm)) cons
387393 scrutineeIdxs <- namePis False idxs
@@ -392,11 +398,11 @@ elabEliminator paramPos n ty cons info = do
392398 let clauseConsElimArgs = map getPiName consTerms
393399 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
394400 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
395− let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy
401+ let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy
396402 elimLog elimSig
397403 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
398404 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
399− elimLog $ "-- eliminator definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
405+ elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
400406 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
401407 -- Do not elaborate clauses if there aren't any
402408 case eliminatorClauses of
@@ -406,10 +412,10 @@ elabEliminator paramPos n ty cons info = do
406412 elimLog s = State.lift (logLvl 2 s)
407413
408414 elimFC :: FC
409− elimFC = fileFC "(eliminator)"
415+ elimFC = fileFC "(casefun)"
410416
411417 elimDeclName :: Name
412− elimDeclName = SN $ ElimN n
418+ elimDeclName = if ind then SN . ElimN $ n else SN . CaseN $ n
413419
414420 applyNS :: Name -> [String] -> Name
415421 applyNS n [] = n
@@ -560,7 +566,7 @@ elabEliminator paramPos n ty cons info = do
560566 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
561567 consArgs <- namePis False args
562568 let recArgs = findRecArgs consArgs
563− let recMotives = map applyRecMotive recArgs
569+ let recMotives = if ind then map applyRecMotive recArgs else []
564570 let (_, consIdxs) = splitArgPms resTy
565571 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
566572 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
@@ -600,7 +606,7 @@ elabEliminator paramPos n ty cons info = do
600606 consArgs <- namePis False args
601607 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
602608 let recArgs = findRecArgs consArgs
603− let recElims = map applyRecElim recArgs
609+ let recElims = if ind then map applyRecElim recArgs else []
604610 let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)
605611 return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []
606612 where applyRecElim :: (Name, Plicity, PTerm) -> PArg
@@ -681,8 +687,8 @@ elabPrims = do mapM_ (elabDecl EAll toplevel)
681687
682688
683689-- | Elaborate a type provider
684−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> PTerm -> PTerm -> Idris ()
685−elabProvider info syn fc what n ty tm
690+elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()
691+elabProvider info syn fc what n
686692 = do i <- getIState
687693 -- Ensure that the experimental extension is enabled
688694 unless (TypeProviders `elem` idris_language_extensions i) $
@@ -692,12 +698,17 @@ elabProvider info syn fc what n ty tm
692698 ctxt <- getContext
693699
694700 -- First elaborate the expected type (and check that it's a type)
695− (ty', typ) <- elabVal toplevel False ty
701+ -- The goal type for a postulate is always Type.
702+ (ty', typ) <- case what of
703+ ProvTerm ty p -> elabVal toplevel False ty
704+ ProvPostulate _ -> elabVal toplevel False PType
696705 unless (isTType typ) $
697706 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)
698707
699708 -- Elaborate the provider term to TT and check that the type matches
700− (e, et) <- elabVal toplevel False tm
709+ (e, et) <- case what of
710+ ProvTerm _ tm -> elabVal toplevel False tm
711+ ProvPostulate tm -> elabVal toplevel False tm
701712 unless (isProviderOf (normalise ctxt [] ty') et) $
702713 ifail $ "Expected provider type IO (Provider (" ++
703714 show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
@@ -715,17 +726,14 @@ elabProvider info syn fc what n ty tm
715726
716727 case provided of
717728 Provide tm
718− | what `elem` [ProvTerm, ProvAny] ->
729+ | ProvTerm ty _ <- what ->
719730 do -- Finally add a top-level definition of the provided term
720731 elabType info syn emptyDocstring [] fc [] n ty
721732 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]
722733 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
723− | otherwise ->
724− ierror . Msg $ "Attempted to provide a term where a postulate was expected."
725− Postulate
726− | what `elem` [ProvPostulate, ProvAny] ->
734+ | ProvPostulate _ <- what ->
727735 do -- Add the postulate
728− elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n ty
736+ elabPostulate info syn (parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)
729737 logLvl 3 $ "Elaborated provided postulate " ++ show n
730738 | otherwise ->
731739 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
@@ -961,6 +969,8 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
961969 def' <- checkDef fc defer
962970 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
963971 addDeferred def''
972+ mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
973+
964974 mapM_ (elabCaseBlock info []) is
965975 ctxt <- getContext
966976 (cty, _) <- recheckC fc [] t'
@@ -2042,7 +2052,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
20422052 [c] -> return c
20432053 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
20442054 cs -> tclift $ tfail $ At fc
2045− (CantResolveAlts (map (show . fst) cs))
2055+ (CantResolveAlts (map fst cs))
20462056 let constraint = PApp fc (PRef fc n) (map pexp ps)
20472057 let iname = mkiname n ps expn
20482058 let emptyclass = null (class_methods ci)
@@ -2408,10 +2418,10 @@ elabDecl' _ info (PDSL n dsl)
24082418 addIBC (IBCDSL n)
24092419elabDecl' what info (PDirective i)
24102420 | what /= EDefns = i
2411−elabDecl' what info (PProvider syn fc provWhat n tp tm)
2421+elabDecl' what info (PProvider syn fc provWhat n)
24122422 | what /= EDefns
24132423 = do iLOG $ "Elaborating type provider " ++ show n
2414− elabProvider info syn fc provWhat n tp tm
2424+ elabProvider info syn fc provWhat n
24152425elabDecl' what info (PTransform fc safety old new)
24162426 = elabTransform info fc safety old new
24172427elabDecl' _ _ _ = return () -- skipped this time
src/Idris/ElabTerm.hs+33−13
@@ -70,7 +70,7 @@ build ist info pattern opts fn tm
7070
7171 when (not pattern) $
7272 traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++
73− "Remaining problems:\n" ++ show probs) $
73+ "Remaining problems:\n" ++ qshow probs) $
7474 do unify_all; matchProblems True; unifyProblems
7575
7676 probs <- get_probs
@@ -271,10 +271,10 @@ elab ist info pattern opts fn tm
271271 let as' = pruneByType (map fst env) tc ctxt as
272272-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $
273273 tryAll (zip (map (elab' ina) as') (map showHd as'))
274− where showHd (PApp _ (PRef _ n) _) = show n
275− showHd (PRef _ n) = show n
276− showHd (PApp _ h _) = show h
277− showHd x = show x
274+ where showHd (PApp _ (PRef _ n) _) = n
275+ showHd (PRef _ n) = n
276+ showHd (PApp _ h _) = showHd h
277+ showHd x = NErased -- We probably should do something better than this here
278278 elab' ina (PAlternative False as)
279279 = trySeq as
280280 where -- if none work, take the error from the first
@@ -956,6 +956,24 @@ collectDeferred top (Bind n b t) = do b' <- cdb b
956956collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)
957957collectDeferred top t = return t
958958
959+case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
960+case_ ind autoSolve ist fn tm = do
961+ attack
962+ tyn <- getNameFrom (sMN 0 "ity")
963+ claim tyn RType
964+ valn <- getNameFrom (sMN 0 "ival")
965+ claim valn (Var tyn)
966+ letn <- getNameFrom (sMN 0 "irule")
967+ letbind letn (Var tyn) (Var valn)
968+ focus valn
969+ elab ist toplevel False [] (sMN 0 "tac") tm
970+ env <- get_env
971+ let (Just binding) = lookup letn env
972+ let val = binderVal binding
973+ if ind then induction (forget val)
974+ else casetac (forget val)
975+ when autoSolve solveAll
976+
959977-- Running tactics directly
960978-- if a tactic adds unification problems, return an error
961979
@@ -991,7 +1009,7 @@ runTac autoSolve ist fn tac
9911009 ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)
9921010 let tacs = map (\ (fn', imps) ->
9931011 (match_apply (Var fn') (map (\x -> (x, 0)) imps),
994− show fn')) fnimps
1012+ fn')) fnimps
9951013 tryAll tacs
9961014 when autoSolve solveAll
9971015 where envArgs n = do e <- get_env
@@ -1007,7 +1025,7 @@ runTac autoSolve ist fn tac
10071025 ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)
10081026 let tacs = map (\ (fn', imps) ->
10091027 (apply (Var fn') (map (\x -> (x, 0)) imps),
1010− show fn')) fnimps
1028+ fn')) fnimps
10111029 tryAll tacs
10121030 when autoSolve solveAll
10131031 where isImp (PImp _ _ _ _ _) = True
@@ -1046,9 +1064,10 @@ runTac autoSolve ist fn tac
10461064 elab ist toplevel False [] (sMN 0 "tac") tm
10471065 rewrite (Var letn)
10481066 when autoSolve solveAll
1049− runT (Induction nm)
1050− = do induction nm
1051− when autoSolve solveAll
1067+ runT (Induction tm) -- let bind tm, similar to the others
1068+ = case_ True autoSolve ist fn tm
1069+ runT (CaseTac tm)
1070+ = case_ False autoSolve ist fn tm
10521071 runT (LetTac n tm)
10531072 = do attack
10541073 tyn <- getNameFrom (sMN 0 "letty")
@@ -1214,7 +1233,8 @@ reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist
12141233reifyApp ist t [Constant (Str n), x]
12151234 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
12161235reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
1217−reifyApp _ t [n] | t == reflm "Induction" = liftM Induction (reifyTTName n)
1236+reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
1237+reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')
12181238reifyApp ist t [t']
12191239 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
12201240reifyApp ist t [t']
@@ -1609,8 +1629,8 @@ reflectErr (NotInjective t1 t2 t3) =
16091629 ]
16101630reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
16111631reflectErr (CantResolveAlts ss) =
1612− raw_apply (Var $ reflErrName "CantResolve")
1613− [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]
1632+ raw_apply (Var $ reflErrName "CantResolveAlts")
1633+ [rawList (Var $ (sUN "String")) (map Var ss)]
16141634reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
16151635reflectErr UniverseError = Var $ reflErrName "UniverseError"
16161636reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
src/Idris/Erasure.hs+1−1
@@ -109,7 +109,7 @@ performUsageAnalysis = do
109109 getMainName ist = case lookupCtxtName n (idris_implicits ist) of
110110 [(n', _)] -> Right n'
111111 [] -> Left (NoSuchVariable n)
112− more -> Left (CantResolveAlts (map (show . fst) more))
112+ more -> Left (CantResolveAlts (map fst more))
113113 where
114114 n = sNS (sUN "main") ["Main"]
115115
src/Idris/IBC.hs+11−348
@@ -4,6 +4,7 @@ module Idris.IBC where
44
55import Idris.Core.Evaluate
66import Idris.Core.TT
7+import Idris.Core.Binary
78import Idris.Core.CaseTree
89import Idris.AbsSyntax
910import Idris.Imports
@@ -617,352 +618,6 @@ instance Binary CGInfo where
617618 x4 <- get
618619 x5 <- get
619620 return (CGInfo x1 x2 [] x4 x5)
620−
621−instance Binary FC where
622− put (FC x1 (x2, x3) (x4, x5))
623− = do put x1
624− put (x2 * 65536 + x3)
625− put (x4 * 65536 + x5)
626− get
627− = do x1 <- get
628− x2x3 <- get
629− x4x5 <- get
630− return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))
631−
632−
633−instance Binary Name where
634− put x
635− = case x of
636− UN x1 -> do putWord8 0
637− put x1
638− NS x1 x2 -> do putWord8 1
639− put x1
640− put x2
641− MN x1 x2 -> do putWord8 2
642− put x1
643− put x2
644− NErased -> putWord8 3
645− SN x1 -> do putWord8 4
646− put x1
647− SymRef x1 -> do putWord8 5
648− put x1
649− get
650− = do i <- getWord8
651− case i of
652− 0 -> do x1 <- get
653− return (UN x1)
654− 1 -> do x1 <- get
655− x2 <- get
656− return (NS x1 x2)
657− 2 -> do x1 <- get
658− x2 <- get
659− return (MN x1 x2)
660− 3 -> return NErased
661− 4 -> do x1 <- get
662− return (SN x1)
663− 5 -> do x1 <- get
664− return (SymRef x1)
665− _ -> error "Corrupted binary data for Name"
666−
667−instance Binary T.Text where
668− put x = put (str x)
669− get = do x <- get
670− return (txt x)
671−
672−instance Binary SpecialName where
673− put x
674− = case x of
675− WhereN x1 x2 x3 -> do putWord8 0
676− put x1
677− put x2
678− put x3
679− InstanceN x1 x2 -> do putWord8 1
680− put x1
681− put x2
682− ParentN x1 x2 -> do putWord8 2
683− put x1
684− put x2
685− MethodN x1 -> do putWord8 3
686− put x1
687− CaseN x1 -> do putWord8 4; put x1
688− ElimN x1 -> do putWord8 5; put x1
689− InstanceCtorN x1 -> do putWord8 6; put x1
690− get
691− = do i <- getWord8
692− case i of
693− 0 -> do x1 <- get
694− x2 <- get
695− x3 <- get
696− return (WhereN x1 x2 x3)
697− 1 -> do x1 <- get
698− x2 <- get
699− return (InstanceN x1 x2)
700− 2 -> do x1 <- get
701− x2 <- get
702− return (ParentN x1 x2)
703− 3 -> do x1 <- get
704− return (MethodN x1)
705− 4 -> do x1 <- get
706− return (CaseN x1)
707− 5 -> do x1 <- get
708− return (ElimN x1)
709− 6 -> do x1 <- get
710− return (InstanceCtorN x1)
711− _ -> error "Corrupted binary data for SpecialName"
712−
713−
714−instance Binary Const where
715− put x
716− = case x of
717− I x1 -> do putWord8 0
718− put x1
719− BI x1 -> do putWord8 1
720− put x1
721− Fl x1 -> do putWord8 2
722− put x1
723− Ch x1 -> do putWord8 3
724− put x1
725− Str x1 -> do putWord8 4
726− put x1
727− B8 x1 -> putWord8 5 >> put x1
728− B16 x1 -> putWord8 6 >> put x1
729− B32 x1 -> putWord8 7 >> put x1
730− B64 x1 -> putWord8 8 >> put x1
731−
732− (AType (ATInt ITNative)) -> putWord8 9
733− (AType (ATInt ITBig)) -> putWord8 10
734− (AType ATFloat) -> putWord8 11
735− (AType (ATInt ITChar)) -> putWord8 12
736− StrType -> putWord8 13
737− PtrType -> putWord8 14
738− Forgot -> putWord8 15
739− (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive
740− (AType (ATInt (ITVec ity count))) -> do
741− putWord8 20
742− putWord8 (fromIntegral . fromEnum $ ity)
743− putWord8 (fromIntegral count)
744−
745− B8V x1 -> putWord8 21 >> put x1
746− B16V x1 -> putWord8 22 >> put x1
747− B32V x1 -> putWord8 23 >> put x1
748− B64V x1 -> putWord8 24 >> put x1
749− BufferType -> putWord8 25
750− ManagedPtrType -> putWord8 26
751− get
752− = do i <- getWord8
753− case i of
754− 0 -> do x1 <- get
755− return (I x1)
756− 1 -> do x1 <- get
757− return (BI x1)
758− 2 -> do x1 <- get
759− return (Fl x1)
760− 3 -> do x1 <- get
761− return (Ch x1)
762− 4 -> do x1 <- get
763− return (Str x1)
764− 5 -> fmap B8 get
765− 6 -> fmap B16 get
766− 7 -> fmap B32 get
767− 8 -> fmap B64 get
768−
769− 9 -> return (AType (ATInt ITNative))
770− 10 -> return (AType (ATInt ITBig))
771− 11 -> return (AType ATFloat)
772− 12 -> return (AType (ATInt ITChar))
773− 13 -> return StrType
774− 14 -> return PtrType
775− 15 -> return Forgot
776−
777− 16 -> return (AType (ATInt (ITFixed IT8)))
778− 17 -> return (AType (ATInt (ITFixed IT16)))
779− 18 -> return (AType (ATInt (ITFixed IT32)))
780− 19 -> return (AType (ATInt (ITFixed IT64)))
781−
782− 20 -> do
783− e <- getWord8
784− c <- getWord8
785− return (AType (ATInt (ITVec (toEnum . fromIntegral $ e) (fromIntegral c))))
786−
787− 21 -> fmap B8V get
788− 22 -> fmap B16V get
789− 23 -> fmap B32V get
790− 24 -> fmap B64V get
791− 25 -> return BufferType
792− 26 -> return ManagedPtrType
793−
794− _ -> error "Corrupted binary data for Const"
795−
796−
797−instance Binary Raw where
798− put x
799− = case x of
800− Var x1 -> do putWord8 0
801− put x1
802− RBind x1 x2 x3 -> do putWord8 1
803− put x1
804− put x2
805− put x3
806− RApp x1 x2 -> do putWord8 2
807− put x1
808− put x2
809− RType -> putWord8 3
810− RConstant x1 -> do putWord8 4
811− put x1
812− RForce x1 -> do putWord8 5
813− put x1
814− get
815− = do i <- getWord8
816− case i of
817− 0 -> do x1 <- get
818− return (Var x1)
819− 1 -> do x1 <- get
820− x2 <- get
821− x3 <- get
822− return (RBind x1 x2 x3)
823− 2 -> do x1 <- get
824− x2 <- get
825− return (RApp x1 x2)
826− 3 -> return RType
827− 4 -> do x1 <- get
828− return (RConstant x1)
829− 5 -> do x1 <- get
830− return (RForce x1)
831− _ -> error "Corrupted binary data for Raw"
832−
833−
834−instance (Binary b) => Binary (Binder b) where
835− put x
836− = case x of
837− Lam x1 -> do putWord8 0
838− put x1
839− Pi x1 -> do putWord8 1
840− put x1
841− Let x1 x2 -> do putWord8 2
842− put x1
843− put x2
844− NLet x1 x2 -> do putWord8 3
845− put x1
846− put x2
847− Hole x1 -> do putWord8 4
848− put x1
849− GHole x1 x2 -> do putWord8 5
850− put x1
851− put x2
852− Guess x1 x2 -> do putWord8 6
853− put x1
854− put x2
855− PVar x1 -> do putWord8 7
856− put x1
857− PVTy x1 -> do putWord8 8
858− put x1
859− get
860− = do i <- getWord8
861− case i of
862− 0 -> do x1 <- get
863− return (Lam x1)
864− 1 -> do x1 <- get
865− return (Pi x1)
866− 2 -> do x1 <- get
867− x2 <- get
868− return (Let x1 x2)
869− 3 -> do x1 <- get
870− x2 <- get
871− return (NLet x1 x2)
872− 4 -> do x1 <- get
873− return (Hole x1)
874− 5 -> do x1 <- get
875− x2 <- get
876− return (GHole x1 x2)
877− 6 -> do x1 <- get
878− x2 <- get
879− return (Guess x1 x2)
880− 7 -> do x1 <- get
881− return (PVar x1)
882− 8 -> do x1 <- get
883− return (PVTy x1)
884− _ -> error "Corrupted binary data for Binder"
885−
886−
887−instance Binary NameType where
888− put x
889− = case x of
890− Bound -> putWord8 0
891− Ref -> putWord8 1
892− DCon x1 x2 -> do putWord8 2
893− put (x1 * 65536 + x2)
894− TCon x1 x2 -> do putWord8 3
895− put (x1 * 65536 + x2)
896− get
897− = do i <- getWord8
898− case i of
899− 0 -> return Bound
900− 1 -> return Ref
901− 2 -> do x1x2 <- get
902− return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
903− 3 -> do x1x2 <- get
904− return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
905− _ -> error "Corrupted binary data for NameType"
906−
907−
908−instance {- (Binary n) => -} Binary (TT Name) where
909− put x
910− = {-# SCC "putTT" #-}
911− case x of
912− P x1 x2 x3 -> do putWord8 0
913− put x1
914− put x2
915−-- put x3
916− V x1 -> if (x1 >= 0 && x1 < 256)
917− then do putWord8 1
918− putWord8 (toEnum (x1 + 1))
919− else do putWord8 9
920− put x1
921− Bind x1 x2 x3 -> do putWord8 2
922− put x1
923− put x2
924− put x3
925− App x1 x2 -> do putWord8 3
926− put x1
927− put x2
928− Constant x1 -> do putWord8 4
929− put x1
930− Proj x1 x2 -> do putWord8 5
931− put x1
932− putWord8 (toEnum (x2 + 1))
933− Erased -> putWord8 6
934− TType x1 -> do putWord8 7
935− put x1
936− Impossible -> putWord8 8
937− get
938− = do i <- getWord8
939− case i of
940− 0 -> do x1 <- get
941− x2 <- get
942−-- x3 <- get
943− return (P x1 x2 Erased)
944− 1 -> do x1 <- getWord8
945− return (V ((fromEnum x1) - 1))
946− 2 -> do x1 <- get
947− x2 <- get
948− x3 <- get
949− return (Bind x1 x2 x3)
950− 3 -> do x1 <- get
951− x2 <- get
952− return (App x1 x2)
953− 4 -> do x1 <- get
954− return (Constant x1)
955− 5 -> do x1 <- get
956− x2 <- getWord8
957− return (Proj x1 ((fromEnum x2)-1))
958− 6 -> return Erased
959− 7 -> do x1 <- get
960− return (TType x1)
961− 8 -> return Impossible
962− 9 -> do x1 <- get
963− return (V x1)
964− _ -> error "Corrupted binary data for TT"
965−
966621instance Binary SC where
967622 put x
968623 = case x of
@@ -1264,11 +919,13 @@ instance Binary DataOpt where
1264919 Codata -> putWord8 0
1265920 DefaultEliminator -> putWord8 1
1266921 DataErrRev -> putWord8 2
922+ DefaultCaseFun -> putWord8 3
1267923 get = do i <- getWord8
1268924 case i of
1269925 0 -> return Codata
1270926 1 -> return DefaultEliminator
1271927 2 -> return DataErrRev
928+ 3 -> return DefaultCaseFun
1272929
1273930instance Binary FnOpt where
1274931 put x
@@ -1968,6 +1625,8 @@ instance (Binary t) => Binary (PTactic' t) where
19681625 put x4
19691626 put x5
19701627 DoUnify -> putWord8 22
1628+ CaseTac x1 -> do putWord8 23
1629+ put x1
19711630 get
19721631 = do i <- getWord8
19731632 case i of
@@ -2016,6 +1675,8 @@ instance (Binary t) => Binary (PTactic' t) where
20161675 x5 <- get
20171676 return (ProofSearch x1 x2 x3 x4 x5)
20181677 22 -> return DoUnify
1678+ 23 -> do x1 <- get
1679+ return (CaseTac x1)
20191680 _ -> error "Corrupted binary data for PTactic'"
20201681
20211682
@@ -2191,7 +1852,7 @@ instance Binary Syntax where
21911852 return (Rule x1 x2 x3)
21921853
21931854instance (Binary t) => Binary (DSL' t) where
2194− put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)
1855+ put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
21951856 = do put x1
21961857 put x2
21971858 put x3
@@ -2201,6 +1862,7 @@ instance (Binary t) => Binary (DSL' t) where
22011862 put x7
22021863 put x8
22031864 put x9
1865+ put x10
22041866 get
22051867 = do x1 <- get
22061868 x2 <- get
@@ -2211,7 +1873,8 @@ instance (Binary t) => Binary (DSL' t) where
22111873 x7 <- get
22121874 x8 <- get
22131875 x9 <- get
2214− return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)
1876+ x10 <- get
1877+ return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
22151878
22161879instance Binary SSymbol where
22171880 put x
src/Idris/IdeSlave.hs+26−4
@@ -5,12 +5,16 @@ module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand
55import Text.Printf
66import Numeric
77import Data.List
8+import qualified Data.Binary as Binary
9+import qualified Data.ByteString.Base64 as Base64
10+import qualified Data.ByteString.Lazy as Lazy
811import qualified Data.ByteString.UTF8 as UTF8
912-- import qualified Data.Text as T
1013import Text.Trifecta hiding (Err)
1114import Text.Trifecta.Delta
1215
1316import Idris.Core.TT
17+import Idris.Core.Binary
1418
1519import Control.Applicative hiding (Const)
1620
@@ -74,10 +78,11 @@ instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>
7478 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]
7579
7680instance SExpable NameOutput where
77− toSExp TypeOutput = SymbolAtom "type"
78− toSExp FunOutput = SymbolAtom "function"
79− toSExp DataOutput = SymbolAtom "data"
80− toSExp MetavarOutput = SymbolAtom "metavar"
81+ toSExp TypeOutput = SymbolAtom "type"
82+ toSExp FunOutput = SymbolAtom "function"
83+ toSExp DataOutput = SymbolAtom "data"
84+ toSExp MetavarOutput = SymbolAtom "metavar"
85+ toSExp PostulateOutput = SymbolAtom "postulate"
8186
8287maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
8388maybeProps [] = []
@@ -127,6 +132,14 @@ instance SExpable OutputAnnotation where
127132 BoldText -> "bold"
128133 ItalicText -> "italic"
129134 UnderlineText -> "underline"
135+ toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]
136+
137+encodeTerm :: [(Name, Bool)] -> Term -> String
138+encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
139+ (bnd, tm)
140+
141+decodeTerm :: String -> ([(Name, Bool)], Term)
142+decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
130143
131144instance SExpable FC where
132145 toSExp (FC f (sl, sc) (el, ec)) =
@@ -184,6 +197,9 @@ data IdeSlaveCommand = REPLCompletions String
184197 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
185198 | WhoCalls String
186199 | CallsWho String
200+ | TermNormalise [(Name, Bool)] Term
201+ | TermShowImplicits [(Name, Bool)] Term
202+ | TermNoImplicits [(Name, Bool)] Term
187203
188204sexpToCommand :: SExp -> Maybe IdeSlaveCommand
189205sexpToCommand (SexpList (x:[])) = sexpToCommand x
@@ -220,6 +236,12 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
220236sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
221237sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
222238sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)
239+sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
240+ Just (TermNormalise bnd tm)
241+sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
242+ Just (TermShowImplicits bnd tm)
243+sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
244+ Just (TermNoImplicits bnd tm)
223245sexpToCommand _ = Nothing
224246
225247parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/IdrisDoc.hs+2−1
@@ -334,7 +334,8 @@ extractPTactic (Intro ns) = ns
334334extractPTactic (Focus n) = [n]
335335extractPTactic (Refine n _) = [n]
336336extractPTactic (Rewrite p) = extract p
337−extractPTactic (Induction n) = [n]
337+extractPTactic (Induction p) = extract p
338+extractPTactic (CaseTac p) = extract p
338339extractPTactic (Equiv p) = extract p
339340extractPTactic (MatchRefine n) = [n]
340341extractPTactic (LetTac n p) = n : extract p
src/Idris/Interactive.hs+4−4
@@ -162,7 +162,7 @@ doProofSearch h fn updatefile rec l n hints (Just depth)
162162 mn <- case lookupNames n ctxt of
163163 [x] -> return x
164164 [] -> return n
165− ns -> ierror (CantResolveAlts (map show ns))
165+ ns -> ierror (CantResolveAlts ns)
166166 i <- getIState
167167 let (top, envlen, _) = case lookup mn (idris_metavars i) of
168168 Just (t, e, False) -> (t, e, False)
@@ -242,10 +242,10 @@ makeLemma h fn updatefile l n
242242 let isProv = checkProv tyline (show n)
243243
244244 ctxt <- getContext
245− mty <- case lookupTy n ctxt of
246− [t] -> return t
245+ mty <- case lookupTyName n ctxt of
246+ [(_,t)] -> return t
247247 [] -> ierror (NoSuchVariable n)
248− ns -> ierror (CantResolveAlts (map show ns))
248+ ns -> ierror (CantResolveAlts (map fst ns))
249249 i <- getIState
250250
251251 if (not isProv) then do
src/Idris/Output.hs+1−33
@@ -74,7 +74,7 @@ ihPrintFunTypes h bnd n overloads = do ist <- getIState
7474 let infixes = idris_infixes ist
7575 let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
7676 ihRenderResult h output
77− where fullName n = prettyNamePossParen True True bnd n
77+ where fullName n = prettyName True True bnd n
7878 ppOverload ppo infixes n tm =
7979 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)
8080
@@ -84,38 +84,6 @@ ihRenderResult h d = do ist <- getIState
8484 RawOutput -> consoleDisplayAnnotated h d
8585 IdeSlave n -> ideSlaveReturnAnnotated n h d
8686
87−makeAnnName :: IState -> Name -> Maybe OutputAnnotation
88−makeAnnName ist n
89− | isDConName n ctxt = annName DataOutput
90− | isFnName n ctxt = annName FunOutput
91− | isTConName n ctxt = annName TypeOutput
92− | isMetavarName n ist = annName MetavarOutput
93− | otherwise = Nothing
94− where ctxt = tt_ctxt ist
95− docs = docOverview ist n
96− ty = Just (getTy ist n)
97−
98− annName :: NameOutput -> Maybe OutputAnnotation
99− annName nameType = Just (AnnName n (Just nameType) docs ty)
100− docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
101− docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)
102− let o = overview (fst docs)
103− -- TODO make width configurable
104− out = displayS . renderPretty 1.0 50 $ renderDocstring o
105− return (out "")
106− getTy :: IState -> Name -> String -- fails if name not already extant!
107− getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
108− delabTy ist n
109− in (displayS . renderPretty 1.0 50 $ theTy) ""
110−
111−
112−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
113−fancifyAnnots ist annot@(AnnName n _ _ _) = case makeAnnName ist n of
114− Just fancyAnnot -> fancyAnnot
115− Nothing -> annot
116−fancifyAnnots _ annot = annot
117−
118−
11987ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()
12088ideSlaveReturnWithStatus status n h out = do
12189 ist <- getIState
src/Idris/ParseData.hs+9−6
@@ -79,12 +79,13 @@ dataI :: IdrisParser DataOpts
7979dataI = do reserved "data"; return []
8080 <|> do reserved "codata"; return [Codata]
8181
82−{- | Parses if a data should not have a default eliminator
82+{- | Parses if a data should not have a default eliminator
8383DefaultEliminator ::= 'noelim'?
8484 -}
8585dataOpts :: DataOpts -> IdrisParser DataOpts
8686dataOpts opts
87− = do reserved "%elim"; dataOpts (DefaultEliminator : opts)
87+ = do reserved "%elim"; dataOpts (DefaultEliminator : DefaultCaseFun : opts)
88+ <|> do reserved "%case"; dataOpts (DefaultCaseFun : opts)
8889 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)
8990 <|> return opts
9091 <?> "data options"
@@ -129,7 +130,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
129130 let tyn = expandNS syn tyn_in
130131 option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do
131132 try (lchar '=') <|> do reserved "where"
132− let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "
133+ let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "
133134 let n = show tyn_in ++ " "
134135 let s = kw ++ n
135136 let as = concat (intersperse " " $ map show args) ++ " "
@@ -209,12 +210,14 @@ dsl syn = do reserved "dsl"
209210 first = lookup "index_first" bs
210211 next = lookup "index_next" bs
211212 leto = lookup "let" bs
212− lambda = lookup "lambda" bs in
213+ lambda = lookup "lambda" bs
214+ pi = lookup "pi" bs in
213215 initDSL { dsl_var = var,
214216 index_first = first,
215217 index_next = next,
216218 dsl_lambda = lambda,
217− dsl_let = leto }
219+ dsl_let = leto,
220+ dsl_pi = pi }
218221
219222{- | Checks DSL for errors -}
220223-- FIXME: currently does nothing, check if DSL is really sane
@@ -235,6 +238,6 @@ overload syn = do o <- identifier <|> do reserved "let"
235238 t <- expr syn
236239 return (o, t)
237240 <?> "dsl overload declaratioN"
238− where overloadable = ["let","lambda","index_first","index_next","variable"]
241+ where overloadable = ["let","lambda","pi","index_first","index_next","variable"]
239242
240243
src/Idris/ParseExpr.hs+12−6
@@ -816,7 +816,7 @@ pi syn =
816816 symbol "->"
817817 sc <- expr syn
818818 return (bindList (PPi
819− (TacImp [] Dynamic (PTactics [Trivial]))) xt sc)) <|> (do
819+ (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)) <|> (do
820820 try (lchar '{' *> reserved "default")
821821 when (st == Static) $ fail "default tactic constraints can not be lazy or static"
822822 script <- simpleExpr syn
@@ -1033,9 +1033,10 @@ do_ syn
10331033 <?> "do block expression"
10341034
10351035do_alt syn = do l <- expr' syn
1036− symbol "=>"
1037− r <- expr' syn
1038− return (l, r)
1036+ option (Placeholder, l)
1037+ (do symbol "=>"
1038+ r <- expr' syn
1039+ return (l, r))
10391040
10401041{- | Parses an expression in idiom brackets
10411042@
@@ -1136,6 +1137,7 @@ Tactic ::= 'intro' NameList?
11361137 | 'refine' Name Imp+
11371138 | 'mrefine' Name
11381139 | 'rewrite' Expr
1140+ | 'induction' Expr
11391141 | 'equiv' Expr
11401142 | 'let' Name ':' Expr' '=' Expr
11411143 | 'let' Name '=' Expr
@@ -1183,8 +1185,12 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (
11831185 <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);
11841186 i <- get
11851187 return $ Rewrite (desugar syn i t)
1186− <|> do reserved "induction"; nm <- (indentPropHolds gtProp *> fnName);
1187− return $ Induction nm
1188+ <|> do reserved "case"; t <- (indentPropHolds gtProp *> expr syn);
1189+ i <- get
1190+ return $ CaseTac (desugar syn i t)
1191+ <|> do reserved "induction"; t <- (indentPropHolds gtProp *> expr syn);
1192+ i <- get
1193+ return $ Induction (desugar syn i t)
11881194 <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);
11891195 i <- get
11901196 return $ Equiv (desugar syn i t)
src/Idris/Parser.hs+14−13
@@ -1034,7 +1034,7 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st
10341034 case lookupCtxtName n (idris_implicits i) of
10351035 [(n', _)] -> return n'
10361036 [] -> throwError (NoSuchVariable n)
1037− more -> throwError (CantResolveAlts (map (show . fst) more))
1037+ more -> throwError (CantResolveAlts (map fst more))
10381038
10391039pLangExt :: IdrisParser LanguageExt
10401040pLangExt = (reserved "TypeProviders" >> return TypeProviders)
@@ -1061,19 +1061,20 @@ ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
10611061 -}
10621062provider :: SyntaxInfo -> IdrisParser [PDecl]
10631063provider syn = do try (lchar '%' *> reserved "provide");
1064− what <- provideWhat
1065− lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1066− fc <- getFC
1067− reserved "with"
1068− e <- expr syn
1069− return [PProvider syn fc what n t e]
1064+ provideTerm <|> providePostulate
10701065 <?> "type provider"
1071− where provideWhat :: IdrisParser ProvideWhat
1072− provideWhat = option ProvAny
1073− ( ((reserved "proof" <|> reserved "term" <|> reserved "type") *>
1074− pure ProvTerm)
1075− <|> (reserved "postulate" *> pure ProvPostulate)
1076− <?> "provider variety")
1066+ where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'
1067+ fc <- getFC
1068+ reserved "with"
1069+ e <- expr syn <?> "provider expression"
1070+ return [PProvider syn fc (ProvTerm t e) n]
1071+ providePostulate = do reserved "postulate"
1072+ n <- fnName
1073+ fc <- getFC
1074+ reserved "with"
1075+ e <- expr syn <?> "provider expression"
1076+ return [PProvider syn fc (ProvPostulate e) n]
1077+
10771078{- | Parses a transform
10781079
10791080@
src/Idris/Prover.hs+96−84
@@ -63,9 +63,10 @@ prove opt ctxt lit n ty
6363 ideslavePutSExp "start-proof-mode" n
6464 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
6565 iLOG $ "Adding " ++ show tm
66− iputStrLn $ showProof lit n prf
6766 i <- getIState
68− ideslavePutSExp "end-proof-mode" n
67+ case idris_outputmode i of
68+ IdeSlave _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)
69+ _ -> iputStrLn $ showProof lit n prf
6970 let proofs = proof_list i
7071 putIState (i { proof_list = (n, prf) : proofs })
7172 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
@@ -85,6 +86,11 @@ prove opt ctxt lit n ty
8586 [([], P Ref n ty, ptm)]
8687 [([], P Ref n ty, ptm')] ty)
8788 solveDeferred n
89+ case idris_outputmode i of
90+ IdeSlave n ->
91+ runIO . putStrLn $
92+ convSExp "return" (SymbolAtom "ok", "") n
93+ _ -> return ()
8894
8995elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
9096elabStep st e = case runStateT eCheck st of
@@ -101,7 +107,7 @@ elabStep st e = case runStateT eCheck st of
101107
102108dumpState :: IState -> ProofState -> Idris ()
103109dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
104− do rendered <- iRender $ prettyNamePossParen True False [] nm <> colon <+> text "No more goals."
110+ do rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
105111 iputGoal rendered
106112dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) = do
107113 let OK ty = goalAtFocus ps
@@ -115,7 +121,9 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =
115121 where
116122 ppo = ppOptionIst ist
117123
118− tPretty bnd t = pprintPTerm ppo bnd [] (idris_infixes ist) $ delab ist t
124+ tPretty bnd t = annotate (AnnTerm bnd t) .
125+ pprintPTerm ppo bnd [] (idris_infixes ist) $
126+ delab ist t
119127
120128 assumptionNames :: Env -> [Name]
121129 assumptionNames = map fst
@@ -171,7 +179,7 @@ receiveInput e =
171179 ideslavePutSExp "return" good
172180 receiveInput e
173181 Just (Interpret cmd) -> return (Just cmd)
174− Nothing -> return Nothing
182+ _ -> return Nothing
175183
176184ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
177185ploop fn d prompt prf e h
@@ -198,91 +206,95 @@ ploop fn d prompt prf e h
198206 case cmd of
199207 Success Abandon -> do iPrintError ""; ifail "Abandoned"
200208 _ -> return ()
201− (d, st, done, prf') <- idrisCatch
209+ (d, st, done, prf', res) <- idrisCatch
202210 (case cmd of
203− Failure err -> do iPrintError (show err)
204− return (False, e, False, prf)
211+ Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
205212 Success Undo -> do (_, st) <- elabStep e loadState
206− iPrintResult ""
207− return (True, st, False, init prf)
208− Success ProofState -> do iPrintResult ""
209− return (True, e, False, prf)
213+ return (True, st, False, init prf, Right "")
214+ Success ProofState -> return (True, e, False, prf, Right "")
210215 Success ProofTerm -> do tm <- lifte e get_term
211− iPrintResult $ "TT: " ++ show tm ++ "\n"
212− return (False, e, False, prf)
216+ iputStrLn $ "TT: " ++ show tm ++ "\n"
217+ return (False, e, False, prf, Right "")
213218 Success Qed -> do hs <- lifte e get_holes
214219 when (not (null hs)) $ ifail "Incomplete proof"
215− iPrintResult "Proof completed!"
216− return (False, e, True, prf)
217− Success (TCheck (PRef _ n)) ->
218− do ctxt <- getContext
219− ist <- getIState
220− imp <- impShow
221− idrisCatch (do
222− let h = idris_outh ist
223− OK env = envAtFocus (proof e)
224− ctxt' = envCtxt env ctxt
225− bnd = map (\x -> (fst x, False)) env
226− ist' = ist { tt_ctxt = ctxt' }
227− putIState ist'
228− -- Unlike the REPL, metavars have no special treatment, to
229− -- make it easier to see how to prove with them.
230− case lookupNames n ctxt' of
231− [] -> ihPrintError h $ "No such variable " ++ show n
232− ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
233− putIState ist
234− return (False, e, False, prf))
235− (\err -> do putIState ist ; ierror err)
236− Success (TCheck t) ->
237− do ist <- getIState
238− ctxt <- getContext
239− idrisCatch (do
240− let OK env = envAtFocus (proof e)
241− ctxt' = envCtxt env ctxt
242− putIState ist { tt_ctxt = ctxt' }
243− (tm, ty) <- elabVal toplevel False t
244− let ppo = ppOptionIst ist
245− ty' = normaliseC ctxt [] ty
246− h = idris_outh ist
247− infixes = idris_infixes ist
248− case tm of
249− TType _ ->
250− ihPrintTermWithType h (prettyImp ppo PType) type1Doc
251− _ -> let bnd = map (\x -> (fst x, False)) env in
252− ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
253− (pprintPTerm ppo bnd [] infixes (delab ist ty))
254− putIState ist
255− return (False, e, False, prf))
256− (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
257− Success (TEval t) -> withErrorReflection $
258− do ctxt <- getContext
259− ist <- getIState
260− idrisCatch (do
261− let OK env = envAtFocus (proof e)
262− ctxt' = envCtxt env ctxt
263− ist' = ist { tt_ctxt = ctxt' }
264− bnd = map (\x -> (fst x, False)) env
265− putIState ist'
266− (tm, ty) <- elabVal toplevel False t
267− let tm' = force (normaliseAll ctxt' env tm)
268− ty' = force (normaliseAll ctxt' env ty)
269− ppo = ppOption (idris_options ist')
270− infixes = idris_infixes ist
271− tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
272− tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
273− ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
274− putIState ist
275− return (False, e, False, prf))
276− (\err -> do putIState ist ; ierror err)
220+ iputStrLn "Proof completed!"
221+ return (False, e, True, prf, Right "")
222+ Success (TCheck (PRef _ n)) -> checkNameType n
223+ Success (TCheck t) -> checkType t
224+ Success (TEval t) -> evalTerm t e
277225 Success tac -> do (_, e) <- elabStep e saveState
278226 (_, st) <- elabStep e (runTac autoSolve i fn tac)
279−-- trace (show (problems (proof st))) $
280− iPrintResult ""
281− return (True, st, False, prf ++ [step]))
282− (\err -> do iPrintError (pshow i err)
283− return (False, e, False, prf))
227+ return (True, st, False, prf ++ [step], Right ""))
228+ (\err -> return (False, e, False, prf, Left err))
284229 ideslavePutSExp "write-proof-state" (prf', length prf')
285− if done then do (tm, _) <- elabStep st get_term
286− return (tm, prf')
287− else ploop fn d prompt prf' st h'
230+ case res of
231+ Left err -> do iPrintError (pshow i err)
232+ ploop fn d prompt prf' st h'
233+ Right ok ->
234+ if done then do (tm, _) <- elabStep st get_term
235+ return (tm, prf')
236+ else do iPrintResult ok
237+ ploop fn d prompt prf' st h'
288238 where envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env
239+ checkNameType n = do
240+ ctxt <- getContext
241+ ist <- getIState
242+ imp <- impShow
243+ idrisCatch (do
244+ let h = idris_outh ist
245+ OK env = envAtFocus (proof e)
246+ ctxt' = envCtxt env ctxt
247+ bnd = map (\x -> (fst x, False)) env
248+ ist' = ist { tt_ctxt = ctxt' }
249+ putIState ist'
250+ -- Unlike the REPL, metavars have no special treatment, to
251+ -- make it easier to see how to prove with them.
252+ case lookupNames n ctxt' of
253+ [] -> ihPrintError h $ "No such variable " ++ show n
254+ ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)
255+ putIState ist
256+ return (False, e, False, prf, Right ""))
257+ (\err -> do putIState ist ; ierror err)
258+
259+ checkType t = do
260+ ist <- getIState
261+ ctxt <- getContext
262+ idrisCatch (do
263+ let OK env = envAtFocus (proof e)
264+ ctxt' = envCtxt env ctxt
265+ putIState ist { tt_ctxt = ctxt' }
266+ (tm, ty) <- elabVal toplevel False t
267+ let ppo = ppOptionIst ist
268+ ty' = normaliseC ctxt [] ty
269+ h = idris_outh ist
270+ infixes = idris_infixes ist
271+ case tm of
272+ TType _ ->
273+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc
274+ _ -> let bnd = map (\x -> (fst x, False)) env in
275+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
276+ (pprintPTerm ppo bnd [] infixes (delab ist ty))
277+ putIState ist
278+ return (False, e, False, prf, Right ""))
279+ (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
280+
281+ evalTerm t e = withErrorReflection $
282+ do ctxt <- getContext
283+ ist <- getIState
284+ idrisCatch (do
285+ let OK env = envAtFocus (proof e)
286+ ctxt' = envCtxt env ctxt
287+ ist' = ist { tt_ctxt = ctxt' }
288+ bnd = map (\x -> (fst x, False)) env
289+ putIState ist'
290+ (tm, ty) <- elabVal toplevel False t
291+ let tm' = force (normaliseAll ctxt' env tm)
292+ ty' = force (normaliseAll ctxt' env ty)
293+ ppo = ppOption (idris_options ist')
294+ infixes = idris_infixes ist
295+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
296+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
297+ ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
298+ putIState ist
299+ return (False, e, False, prf, Right ""))
300+ (\err -> do putIState ist ; ierror err)
src/Idris/Providers.hs+1−7
@@ -11,16 +11,14 @@ import Debug.Trace
1111
1212-- | Wrap a type provider in the type of type providers
1313providerTy :: FC -> PTerm -> PTerm
14−providerTy fc tm
14+providerTy fc tm
1515 = PApp fc (PRef fc $ sUN "Provider") [PExp 0 [] (sMN 0 "pvarg") tm]
1616
1717ioret = sUN "prim_io_return"
1818ermod = sNS (sUN "Error") ["Providers"]
1919prmod = sNS (sUN "Provide") ["Providers"]
20−posmod = sNS (sUN "Postulate") ["Providers"]
2120
2221data Provided a = Provide a
23− | Postulate
2422 deriving (Show, Eq, Functor)
2523
2624-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.
@@ -35,10 +33,6 @@ getProvided fc tm | (P _ pioret _, [tp, result]) <- unApply tm
3533 , (P _ nm _, [_, res]) <- unApply result
3634 , pioret == ioret && nm == prmod
3735 = return . Provide $ res
38− | (P _ pioret _, [tp, result]) <- unApply tm
39− , (P _ nm _, [_]) <- unApply result
40− , pioret == ioret && nm == posmod
41− = return Postulate
4236 | otherwise = ifail $ "Internal type provider error: result was not " ++
4337 "IO (Provider a), or perhaps missing normalisation."
4438
src/Idris/REPL.hs+122−45
@@ -240,11 +240,25 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =
240240 i <- getIState
241241 case parseCmd i "(input)" cmd of
242242 Failure err -> iPrintError $ show (fixColour c err)
243− Success (Prove n') -> do iPrintResult ""
244− idrisCatch
245− (process stdout fn (Prove n'))
246− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
247− isetPrompt (mkPrompt mods)
243+ Success (Prove n') ->
244+ idrisCatch
245+ (do process stdout fn (Prove n')
246+ isetPrompt (mkPrompt mods)
247+ case idris_outputmode i of
248+ IdeSlave n -> -- signal completion of proof to ide
249+ runIO . hPutStrLn stdout $
250+ IdeSlave.convSExp "return"
251+ (IdeSlave.SymbolAtom "ok", "")
252+ n
253+ _ -> return ())
254+ (\e -> do ist <- getIState
255+ isetPrompt (mkPrompt mods)
256+ case idris_outputmode i of
257+ IdeSlave n ->
258+ runIO . hPutStrLn stdout $
259+ IdeSlave.convSExp "abandon-proof" "Abandoned" n
260+ _ -> return ()
261+ ihRenderError stdout $ pprintErr ist e)
248262 Success cmd -> idrisCatch
249263 (ideslaveProcess fn cmd)
250264 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)
@@ -328,34 +342,63 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
328342 do ist <- getIState
329343 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
330344 let ppo = ppOptionIst ist
331− let mvarTys = map (delabTy ist) mvs
332− let res = (IdeSlave.SymbolAtom "ok",
333− zipWith (\ n (prems, concl) -> (n, prems, concl))
334− (map (IdeSlave.StringAtom . show) mvs)
335− (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))
336− runIO . putStrLn $ IdeSlave.convSExp "return" res id
337− where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
338− getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
339− in ((n, t):prems, conc)
340− getGoal tm = ([], tm)
341− sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)
342− -> ([(String, String, SpanList OutputAnnotation)],
343− (String, SpanList OutputAnnotation))
344− sexpGoal ist cols ppo ns ([], concl) =
345− let infixes = idris_infixes ist
346− concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
347− pprintPTerm ppo (zip ns (repeat False)) [] infixes concl
348− in ([], concl')
349− sexpGoal ist cols ppo ns ((n, t):ps, concl) =
350− let n' = case n of
351− NS (UN nm) ns -> str nm
352− UN nm | ('_':'_':_) <- str nm -> "_"
353− | otherwise -> str nm
354− _ -> "_"
355− (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
356− pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t
357− rest = sexpGoal ist cols ppo (n:ns) (ps, concl)
358− in ((n', t', spans) : fst rest, snd rest)
345+ -- splitMvs is a list of pairs of names and their split types
346+ let splitMvs = mapSnd (splitPi ist) (mvTys ist mvs)
347+ -- mvOutput is the pretty-printed version ready for conversion to SExpr
348+ let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $
349+ mapPair show
350+ (\(hs, c, pc) ->
351+ let bnd = [ n | (n,_,_) <- hs ] in
352+ let bnds = inits bnd in
353+ (map (\(bnd, h) -> processPremise ist bnd h)
354+ (zip bnds hs),
355+ render ist bnd c pc))
356+ splitMvs
357+ runIO . putStrLn $
358+ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", mvOutput) id
359+ where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
360+ mapSnd f xs = zip (map fst xs) (map (f . snd) xs)
361+
362+ -- | Split a function type into a pair of premises, conclusion.
363+ -- Each maintains both the original and delaborated versions.
364+ splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
365+ splitPi ist (Bind n (Pi t) rest) =
366+ let (hs, c, pc) = splitPi ist rest in
367+ ((n, t, delabTy' ist [] t False False):hs,
368+ c, delabTy' ist [] c False False)
369+ splitPi ist tm = ([], tm, delabTy' ist [] tm False False)
370+
371+ -- | Get the types of a list of metavariable names
372+ mvTys :: IState -> [Name] -> [(Name, Type)]
373+ mvTys ist = mapSnd vToP . mapMaybe (flip lookupTyNameExact (tt_ctxt ist))
374+
375+ -- | Show a type and its corresponding PTerm in a format suitable
376+ -- for the IDE - that is, pretty-printed and annotated.
377+ render :: IState -> [Name] -> Type -> PTerm -> (String, SpanList OutputAnnotation)
378+ render ist bnd t pt =
379+ let prettyT = pprintPTerm (ppOptionIst ist)
380+ (zip bnd (repeat False))
381+ []
382+ (idris_infixes ist)
383+ pt
384+ in
385+ displaySpans .
386+ renderPretty 0.9 cols .
387+ fmap (fancifyAnnots ist) .
388+ annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $
389+ prettyT
390+
391+ -- | Juggle the bits of a premise to prepare for output.
392+ processPremise :: IState
393+ -> [Name] -- ^ the names to highlight as bound
394+ -> (Name, Type, PTerm)
395+ -> (String,
396+ String,
397+ SpanList OutputAnnotation)
398+ processPremise ist bnd (n, t, pt) =
399+ let (out, spans) = render ist bnd t pt in
400+ (show n , out, spans)
401+
359402runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
360403 case splitName n of
361404 Left err -> iPrintError err
@@ -367,7 +410,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
367410 where pn ist = displaySpans .
368411 renderPretty 0.9 1000 .
369412 fmap (fancifyAnnots ist) .
370− prettyNamePossParen True True []
413+ prettyName True True []
371414runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =
372415 case splitName n of
373416 Left err -> iPrintError err
@@ -379,7 +422,41 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =
379422 where pn ist = displaySpans .
380423 renderPretty 0.9 1000 .
381424 fmap (fancifyAnnots ist) .
382− prettyNamePossParen True True []
425+ prettyName True True []
426+
427+runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise bnd tm) =
428+ do ctxt <- getContext
429+ ist <- getIState
430+ let tm' = force (normaliseAll ctxt [] tm)
431+ ptm = annotate (AnnTerm bnd tm')
432+ (pprintPTerm (ppOptionIst ist)
433+ bnd
434+ []
435+ (idris_infixes ist)
436+ (delab ist tm'))
437+ msg = (IdeSlave.SymbolAtom "ok",
438+ displaySpans .
439+ renderPretty 0.9 80 .
440+ fmap (fancifyAnnots ist) $ ptm)
441+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id
442+runIdeSlaveCommand id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =
443+ ideSlaveForceTermImplicits id bnd True tm
444+runIdeSlaveCommand id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
445+ ideSlaveForceTermImplicits id bnd False tm
446+
447+-- | Show a term for IDESlave with the specified implicitness
448+ideSlaveForceTermImplicits :: Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
449+ideSlaveForceTermImplicits id bnd impl tm =
450+ do ist <- getIState
451+ let expl = annotate (AnnTerm bnd tm)
452+ (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })
453+ bnd [] (idris_infixes ist)
454+ (delab ist tm))
455+ msg = (IdeSlave.SymbolAtom "ok",
456+ displaySpans .
457+ renderPretty 0.9 80 .
458+ fmap (fancifyAnnots ist) $ expl)
459+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id
383460
384461splitName :: String -> Either String Name
385462splitName s = case reverse $ splitOn "." s of
@@ -512,7 +589,7 @@ resolveProof n'
512589 n <- case lookupNames n' ctxt of
513590 [x] -> return x
514591 [] -> return n'
515− ns -> ierror (CantResolveAlts (map show ns))
592+ ns -> ierror (CantResolveAlts ns)
516593 return n
517594
518595removeProof :: Name -> Idris ()
@@ -580,8 +657,8 @@ process h fn (Eval t)
580657 ist <- getIState
581658 logLvl 3 $ "Raw: " ++ show (tm', ty')
582659 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
583− let tmDoc = prettyIst ist (delab ist tm')
584− tyDoc = prettyIst ist (delab ist ty')
660+ let tmDoc = pprintDelab ist tm'
661+ tyDoc = pprintDelab ist ty'
585662 ihPrintTermWithType h tmDoc tyDoc
586663
587664process h fn (ExecVal t)
@@ -639,8 +716,8 @@ process h fn (Check t)
639716 case tm of
640717 TType _ ->
641718 ihPrintTermWithType h (prettyIst ist PType) type1Doc
642− _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))
643− (prettyIst ist (delab ist ty))
719+ _ -> ihPrintTermWithType h (pprintDelab ist tm)
720+ (pprintDelab ist ty)
644721
645722process h fn (DocStr (Left n))
646723 = do ist <- getIState
@@ -795,7 +872,7 @@ process h fn (Prove n')
795872 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')
796873 [(n, (_,_,False))] -> return n
797874 [(_, (_,_,True))] -> ierror (Msg $ "Declarations not solvable using prover")
798− ns -> ierror (CantResolveAlts (map show ns))
875+ ns -> ierror (CantResolveAlts (map fst ns))
799876 prover (lit fn) n
800877 -- recheck totality
801878 i <- getIState
@@ -928,8 +1005,8 @@ process h fn (WhoCalls n) =
9281005 ist <- getIState
9291006 ihRenderResult h . vsep $
9301007 map (\(n, ns) ->
931− text "Callers of" <+> prettyNamePossParen True True [] n <$>
932− indent 1 (vsep (map ((text "*" <+>) . align . prettyNamePossParen True True []) ns)))
1008+ text "Callers of" <+> prettyName True True [] n <$>
1009+ indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
9331010 calls
9341011
9351012process h fn (CallsWho n) =
@@ -937,8 +1014,8 @@ process h fn (CallsWho n) =
9371014 ist <- getIState
9381015 ihRenderResult h . vsep $
9391016 map (\(n, ns) ->
940− prettyNamePossParen True True [] n <+> text "calls:" <$>
941− indent 1 (vsep (map ((text "*" <+>) . align . prettyNamePossParen True True []) ns)))
1017+ prettyName True True [] n <+> text "calls:" <$>
1018+ indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))
9421019 calls
9431020-- IdrisDoc
9441021process h fn (MakeDoc s) =
src/Idris/REPLParser.hs+1−1
@@ -184,7 +184,7 @@ pColourMod = try (P.symbol "vivid" >> return doVivid)
184184 doNoItalic i = i { italic = False }
185185 doSetColour c i = i { colour = c }
186186
187−
187+-- | Generate the colour type names using the default Show instance.
188188colourTypes :: [(String, ColourType)]
189189colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $
190190 enumFromTo minBound maxBound
test/Makefile+1−1
@@ -8,7 +8,7 @@ test: $(TESTS)
88 @perl ./runtest.pl $(patsubst %.test,%,$@)
99
1010test_java:
11− perl ./runtest.pl without sugar004 buffer001 --codegen Java
11+ @perl ./runtest.pl without --codegen Java
1212
1313test_js:
1414 @perl ./runtest.pl without sugar004 reg029 io001 dsl002 io003 effects001 effects002 buffer001 --codegen node
test/dsl003/DSLPi.idrnew file+38
@@ -0,0 +1,38 @@
1+module DSLPi
2+
3+data Ty = BOOL | INT | UNIT | ARR Ty Ty
4+
5+dsl simple_type
6+ pi = ARR
7+
8+test1 : simple_type (BOOL -> INT -> UNIT) = BOOL `ARR` (INT `ARR` UNIT)
9+test1 = refl
10+
11+using (vars : Vect n Ty)
12+ infix 2 ===
13+
14+ data Expr : Vect n Ty -> Ty -> Type where
15+ Var : (i : Fin n) -> Expr vars (index i vars)
16+ (===) : Expr vars t -> Expr vars t -> Expr vars BOOL
17+
18+ data Spec : Vect n Ty -> Type where
19+ ForAll : (t : Ty) -> Spec (t :: vars) -> Spec vars
20+ ItHolds : Expr vars BOOL -> Spec vars
21+
22+ implicit exprSpec : Expr vars BOOL -> Spec vars
23+ exprSpec = ItHolds
24+
25+dsl specs
26+ pi = ForAll
27+ variable = Var
28+ index_first = fZ
29+ index_next = fS
30+
31+test2 : Spec []
32+test2 = specs ((x, y : INT) -> x === y)
33+
34+test3 : Spec []
35+test3 = ForAll INT . ForAll INT . ItHolds $ Var (fS fZ) === Var fZ
36+
37+test4 : test2 = test3
38+test4 = refl
test/dsl003/expectednew file+2
@@ -0,0 +1,2 @@
1+ForAll INT (ForAll INT (ItHolds (Var (fS fZ) === Var fZ))) : Spec []
2+refl : ARR BOOL (ARR INT UNIT) = ARR BOOL (ARR INT UNIT)
test/dsl003/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --nocolour --check DSLPi.idr -e test1 -e test2
3+rm -f *.ibc
test/ffi005/Postulate.idr+3−3
@@ -4,10 +4,10 @@ import Providers
44
55%language TypeProviders
66
7−bad : IO (Provider _|_)
8−bad = pure Postulate
7+bad : IO (Provider Type)
8+bad = return $ pure _|_
99
10−%provide (oops : _|_) with bad
10+%provide postulate oops with bad
1111
1212main : IO ()
1313main = putStrLn "oops"
test/ffi005/Postulate2.idrdeleted−13
@@ -1,13 +0,0 @@
1−module Main
2−
3−import Providers
4−
5−%language TypeProviders
6−
7−bad : IO (Provider _|_)
8−bad = pure Postulate
9−
10−%provide postulate (oops : _|_) with bad
11−
12−main : IO ()
13−main = putStrLn "oops"
test/ffi005/Postulate3.idrdeleted−13
@@ -1,13 +0,0 @@
1−module Main
2−
3−import Providers
4−
5−%language TypeProviders
6−
7−bad : IO (Provider _|_)
8−bad = pure Postulate
9−
10−%provide term (oops : _|_) with bad
11−
12−main : IO ()
13−main = putStrLn "oops"
test/ffi005/expected−2
@@ -1,3 +1 @@
11oops
2−oops
3−Attempted to provide a postulate where a term was expected.
test/ffi005/run−7
@@ -3,10 +3,3 @@
33idris $@ Postulate.idr -o postulate
44./postulate
55rm -f postulate *.ibc
6−
7−idris $@ Postulate2.idr -o postulate
8−./postulate
9−rm -f postulate *.ibc
10−
11−idris $@ Postulate3.idr -o postulate
12−rm -f postulate *.ibc
test/reg008/expecteddeleted

No changes to the content.

test/reg008/reg008.idrdeleted−15
@@ -1,15 +0,0 @@
1−module NatCmp
2−
3−data Cmp : Nat -> Nat -> Type where
4− cmpLT : (y : _) -> Cmp x (x + S y)
5− cmpEQ : Cmp x x
6− cmpGT : (x : _) -> Cmp (y + S x) y
7−
8−total cmp : (x, y : Nat) -> Cmp x y
9−cmp Z Z = cmpEQ
10−cmp Z (S k) = cmpLT _
11−cmp (S k) Z = cmpGT _
12−cmp (S x) (S y) with (cmp x y)
13− cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k
14− cmp (S x) (S x) | cmpEQ = cmpEQ
15− cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k
test/reg008/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−idris $@ reg008.idr --check
3−rm -f *.ibc
test/reg029/Reg029Wrapper.javanew file+17
@@ -0,0 +1,17 @@
1+import java.util.Map;
2+
3+/**
4+ * The Java back end uses properties
5+ * instead of environment variables.
6+ * This wrapper loads the env variables
7+ * into the standard set of properties.
8+ */
9+public class Reg029Wrapper {
10+ public static void main(String args[]) {
11+ Map<String, String> env = System.getenv();
12+ for (String key : env.keySet()) {
13+ System.setProperty(key, env.get(key));
14+ }
15+ reg029.main(args);
16+ }
17+}
test/reg029/reg029.idr+1
@@ -2,6 +2,7 @@ module Main
22
33import System
44
5+-- necessary to find the getenv symbol
56%dynamic "libm"
67
78main : IO ()
test/reg029/run+12−2
@@ -1,7 +1,17 @@
11#!/usr/bin/env bash
2+
23idris $@ reg029.idr -o reg029
34unset IDRIS_REG029_NONEXISTENT_VAR
45export IDRIS_REG029_EXISTENT_VAR='exists!'
5−./reg029
6+
7+IsJava=`echo "$@" | grep -E "\-\-codegen([[:space:]]+)Java\>"`
8+if [ -z "$IsJava" ]
9+then
10+ ./reg029
11+else
12+ javac -cp reg029:. Reg029Wrapper.java
13+ java -cp reg029:. Reg029Wrapper
14+fi
615idris $@ reg029.idr --execute
7−rm -f reg029 *.ibc
16+rm -f reg029 *.ibc *.class
17+
test/reg034/expected+2−2
@@ -1,7 +1,7 @@
11reg034.idr:6:5:When elaborating left hand side of bar:
22When elaborating an application of main.bar:
33 Can't unify
4− x = x
4+ length ys = length ys
55 with
66 length xs = length ys
77
@@ -13,7 +13,7 @@ When elaborating an application of main.bar:
1313reg034.idr:9:5:When elaborating left hand side of foo:
1414When elaborating an application of main.foo:
1515 Can't unify
16− x = x
16+ f y = f y
1717 with
1818 f x = f y
1919
test/reg043/expecteddeleted−1
@@ -1 +0,0 @@
1−take : (m : Fin 3) -> Vect 2 Nat -> Vect (finToNat m) Nat
test/reg043/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−idris $@ --nocolour -e "Vect.take {n=2} {a=Nat}"
3−
test/reg045/expectednew file+1
@@ -0,0 +1 @@
1+[1, 2, 3]
test/reg045/reg045.idrnew file+19
@@ -0,0 +1,19 @@
1+module Main
2+
3+data ListZ : Type -> Type where
4+ (::) : a -> Lazy (ListZ a) -> ListZ a
5+ Nil : ListZ a
6+
7+instance Show a => Show (ListZ a) where
8+ show xs = "[" ++ show' "" xs ++ "]"
9+ where
10+ show' acc Nil = acc
11+ show' acc (x :: Nil) = acc ++ show x
12+ show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
13+
14+foo : ListZ Nat
15+foo = (1 :: 2 :: 3 :: Nil)
16+
17+main : IO ()
18+main = print foo
19+
test/reg045/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ reg045.idr -o reg045
3+./reg045
4+rm -f reg045 *.ibc
test/tutorial006/expected+2−2
@@ -1,13 +1,13 @@
11tutorial006a.idr:3:23:When elaborating right hand side of vapp:
22When elaborating argument xs to constructor Prelude.Vect.:::
33 Can't unify
4− Vect (n + m) a
4+ Vect (n + n) a
55 with
66 Vect (plus n m) a
77
88 Specifically:
99 Can't unify
10− plus n m
10+ plus n n
1111 with
1212 plus n m
1313tutorial006b.idr:10:10:When elaborating right hand side of Main.parity: