git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of git://github.com/idris-lang/Idris-dev into partial-eval
commit869e6ca751bd6fcd2abca374033b6c3b1cd6bf73 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 4 Oct 2014, 18:25 (12 years ago) parent37748ceb65a1c2
16 files changed+341−276
compare with master
unifiedsplit
libs/base/Data/List.idr+9−1 libs/base/Data/Vect/Quantifiers.idr+24−2 libs/base/Data/ZZ.idr+18−9 libs/base/Language/Reflection.idr+11−9 libs/base/Network/Socket.idr+51−37 libs/prelude/Builtins.idr+15−13 libs/prelude/Prelude.idr+8 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/Docs.hs+3−3 src/Idris/ElabQuasiquote.hs+125−122 src/Idris/ElabTerm.hs+44−60 src/Idris/IBC.hs+1−1 src/Idris/ParseExpr.hs+5−5 src/Idris/Parser.hs+7−2 src/Idris/REPL.hs+11−6 src/Pkg/Package.hs+7−4
libs/base/Data/List.idr+9−1
@@ -2,9 +2,17 @@ module Data.List
22
33%access public
44
5−||| A proof that some element is found in a list
5+||| A proof that some element is found in a list.
6+|||
7+||| Example: `the (Elem "bar" ["foo", "bar", "baz"]) (tactics { search })`
68data Elem : a -> List a -> Type where
9+ ||| A proof that the element is at the front of the list.
10+ |||
11+ ||| Example: `the (Elem "a" ["a", "b"]) Here`
712 Here : Elem x (x :: xs)
13+ ||| A proof that the element is after the front of the list
14+ |||
15+ ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`
816 There : Elem x xs -> Elem x (y :: xs)
917
1018instance Uninhabited (Elem {a} x []) where
libs/base/Data/Vect/Quantifiers.idr+24−2
@@ -1,9 +1,15 @@
11module Data.Vect.Quantifiers
22
3+||| A proof that some element of a vector satisfies some property
4+|||
5+||| @ P the property to be satsified
36data Any : (P : a -> Type) -> Vect n a -> Type where
7+ ||| A proof that the satisfying element is the first one in the `Vect`
48 Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)
9+ ||| A proof that the satsifying element is in the tail of the `Vect`
510 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
611
12+||| No element of an empty vector satisfies any property
713anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
814anyNilAbsurd (Here _) impossible
915anyNilAbsurd (There _) impossible
@@ -15,7 +21,13 @@ anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) ->
1521anyElim _ f (Here p) = f p
1622anyElim f _ (There p) = f p
1723
18−any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)
24+||| Given a decision procedure for a property, determine if an element of a
25+||| vector satisfies it.
26+|||
27+||| @ P the property to be satisfied
28+||| @ dec the decision procedure
29+||| @ xs the vector to examine
30+any : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)
1931any _ Nil = No anyNilAbsurd
2032any p (x::xs) with (p x)
2133 | Yes prf = Yes (Here prf)
@@ -24,10 +36,14 @@ any p (x::xs) with (p x)
2436 Yes prf' => Yes (There prf')
2537 No prf' => No (anyElim prf' prf)
2638
39+||| A proof that all elements of a vector satisfy a property. It is a list of
40+||| proofs, corresponding element-wise to the `Vect`.
2741data All : (P : a -> Type) -> Vect n a -> Type where
2842 Nil : {P : a -> Type} -> All P Nil
2943 (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs)
3044
45+||| If there does not exist an element that satifies the property, then it is
46+||| the case that all elements do not satisfy.
3147negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => Not (P x)) xs
3248negAnyAll {xs=Nil} _ = Nil
3349negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
@@ -40,7 +56,13 @@ notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :
4056notAllThere _ Nil impossible
4157notAllThere np (_ :: ps) = np ps
4258
43−all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
59+||| Given a decision procedure for a property, decide whether all elements of
60+||| a vector satisfy it.
61+|||
62+||| @ P the property
63+||| @ dec the decision procedure
64+||| @ xs the vector to examine
65+all : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
4466all _ Nil = Yes Nil
4567all d (x::xs) with (d x)
4668 | No prf = No (notAllHere prf)
libs/base/Data/ZZ.idr+18−9
@@ -7,14 +7,18 @@ import Data.Sign
77%access public
88
99
10−||| An integer is either a positive nat or the negated successor of a nat.
11−||| Zero is arbitrarily chosen to be positive.
10+||| An integer is either a positive `Nat` or the negated successor of a `Nat`.
11+|||
12+||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen
13+||| to be positive.
14+|||
1215data ZZ = Pos Nat | NegS Nat
1316
1417instance Signed ZZ where
1518 sign (Pos _) = Plus
1619 sign (NegS _) = Minus
1720
21+||| Take the absolute value of a `ZZ`
1822absZ : ZZ -> Nat
1923absZ (Pos n) = n
2024absZ (NegS n) = S n
@@ -23,28 +27,32 @@ instance Show ZZ where
2327 show (Pos n) = show n
2428 show (NegS n) = "-" ++ show (S n)
2529
26−negZ : ZZ -> ZZ
27−negZ (Pos Z) = Pos Z
28−negZ (Pos (S n)) = NegS n
29−negZ (NegS n) = Pos (S n)
30+instance Neg ZZ where
31+ negate (Pos Z) = Pos Z
32+ negate (Pos (S n)) = NegS n
33+ negate (NegS n) = Pos (S n)
3034
3135negNat : Nat -> ZZ
3236negNat Z = Pos Z
3337negNat (S n) = NegS n
3438
39+
40+||| Construct a `ZZ` as the difference of two `Nat`s
3541minusNatZ : Nat -> Nat -> ZZ
3642minusNatZ n Z = Pos n
3743minusNatZ Z (S m) = NegS m
3844minusNatZ (S n) (S m) = minusNatZ n m
3945
46+||| Add two `ZZ`s. Consider using `(+) {a=ZZ}`.
4047plusZ : ZZ -> ZZ -> ZZ
4148plusZ (Pos n) (Pos m) = Pos (n + m)
4249plusZ (NegS n) (NegS m) = NegS (S (n + m))
4350plusZ (Pos n) (NegS m) = minusNatZ n (S m)
4451plusZ (NegS n) (Pos m) = minusNatZ m (S n)
4552
53+||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
4654subZ : ZZ -> ZZ -> ZZ
47−subZ n m = plusZ n (negZ m)
55+subZ n m = plusZ n (negate m)
4856
4957instance Eq ZZ where
5058 (Pos n) == (Pos m) = n == m
@@ -58,13 +66,14 @@ instance Ord ZZ where
5866 compare (Pos _) (NegS _) = GT
5967 compare (NegS _) (Pos _) = LT
6068
61−
69+||| Multiply two `ZZ`s. Consider using `(*) {a=ZZ}`.
6270multZ : ZZ -> ZZ -> ZZ
6371multZ (Pos n) (Pos m) = Pos $ n * m
6472multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
6573multZ (NegS n) (Pos m) = negNat $ (S n) * m
6674multZ (Pos n) (NegS m) = negNat $ n * (S m)
6775
76+||| Convert an `Integer` to an inductive representation.
6877fromInt : Integer -> ZZ
6978fromInt n = if n < 0
7079 then NegS $ fromInteger {a=Nat} ((-n) - 1)
@@ -100,7 +109,7 @@ natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
100109 -> n * m = x -> (Pos n) * (Pos m) = Pos x
101110natMultZMult n m x h = cong h
102111
103−doubleNegElim : (z : ZZ) -> negZ (negZ z) = z
112+doubleNegElim : (z : ZZ) -> negate (negate z) = z
104113doubleNegElim (Pos Z) = Refl
105114doubleNegElim (Pos (S n)) = Refl
106115doubleNegElim (NegS Z) = Refl
libs/base/Language/Reflection.idr+11−9
@@ -79,20 +79,22 @@ reflectConstant = toConst
7979
8080
8181||| Types of named references
82−data NameType = Bound
83− -- ^ reference which is just bound, e.g. by intro
84− | Ref
85− -- ^ reference to a variable
86− | DCon Int Int
87− -- ^ constructor with tag and number
88− | TCon Int Int
89− -- ^ type constructor with tag and number
82+data NameType =
83+ ||| A reference which is just bound, e.g. by intro
84+ Bound |
85+ ||| A reference to a de Bruijn-indexed variable
86+ Ref |
87+ ||| Data constructor with tag and number
88+ DCon Int Int |
89+ ||| Type constructor with tag and number
90+ TCon Int Int
91+
9092%name NameType nt, nt'
9193
9294||| Types annotations for bound variables in different
9395||| binding contexts
9496data Binder a = Lam a
95− | Pi a a
97+ | Pi a a
9698 | Let a a
9799 | NLet a a
98100 | Hole a
libs/base/Network/Socket.idr+51−37
@@ -4,8 +4,8 @@
44module IdrisNet.Socket
55
66%include C "idris_net.h"
7−%include C "sys/types.h"
8−%include C "sys/socket.h"
7+%include C "sys/types.h"
8+%include C "sys/socket.h"
99%include C "netdb.h"
1010
1111%access public
@@ -16,12 +16,17 @@ ByteLength = Int
1616class ToCode a where
1717 toCode : a -> Int
1818
19−-- Socket Families.
20−-- The ones that people might actually use. We're not going to need US Government
21−-- proprietary ones...
22−data SocketFamily = AF_UNSPEC -- Unspecified
23− | AF_INET -- IP / UDP etc. IPv4
24− | AF_INET6 -- IP / UDP etc. IPv6
19+||| Socket Families
20+|||
21+||| The ones that people might actually use. We're not going to need US
22+||| Government proprietary ones.
23+data SocketFamily =
24+ ||| Unspecified
25+ AF_UNSPEC |
26+ ||| IP / UDP etc. IPv4
27+ AF_INET |
28+ ||| IP / UDP etc. IPv6
29+ AF_INET6
2530
2631instance Show SocketFamily where
2732 show AF_UNSPEC = "AF_UNSPEC"
@@ -36,11 +41,16 @@ instance ToCode SocketFamily where
3641getSocketFamily : Int -> Maybe SocketFamily
3742getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
3843
39−-- Socket Types.
40−data SocketType = NotASocket -- Not a socket, used in certain operations
41− | Stream -- TCP
42− | Datagram -- UDP
43− | RawSocket -- Raw sockets. A guy can dream.
44+||| Socket Types.
45+data SocketType =
46+ ||| Not a socket, used in certain operations
47+ NotASocket |
48+ ||| TCP
49+ Stream |
50+ ||| UDP
51+ Datagram |
52+ ||| Raw sockets
53+ RawSocket
4454
4555instance Show SocketType where
4656 show NotASocket = "Not a socket"
@@ -60,15 +70,17 @@ data RecvfromStructPtr = RFPtr Ptr
6070data BufPtr = BPtr Ptr
6171data SockaddrPtr = SAPtr Ptr
6272
63−-- Protocol Number. Generally good enough to just set it to 0.
73+||| Protocol Number.
74+|||
75+||| Generally good enough to just set it to 0.
6476ProtocolNumber : Type
6577ProtocolNumber = Int
6678
67−-- SocketError: Error thrown by a socket operation
79+||| SocketError: Error thrown by a socket operation
6880SocketError : Type
6981SocketError = Int
7082
71−-- SocketDescriptor: Native C Socket Descriptor
83+||| SocketDescriptor: Native C Socket Descriptor
7284SocketDescriptor : Type
7385SocketDescriptor = Int
7486
@@ -86,7 +98,7 @@ instance Show SocketAddress where
8698Port : Type
8799Port = Int
88100
89−-- Backlog used within listen() call -- number of incoming calls
101+||| Backlog used within listen() call -- number of incoming calls
90102BACKLOG : Int
91103BACKLOG = 20
92104
@@ -109,7 +121,7 @@ record UDPAddrInfo : Type where
109121 (remote_port : Port) ->
110122 UDPAddrInfo
111123
112−-- Frees a given pointer
124+||| Frees a given pointer
113125public
114126sock_free : BufPtr -> IO ()
115127sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
@@ -118,12 +130,14 @@ public
118130sockaddr_free : SockaddrPtr -> IO ()
119131sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
120132
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.
133+||| Allocates an amount of memory given by the ByteLength parameter.
134+|||
135+||| Used to allocate a mutable pointer to be given to the Recv functions.
123136public
124137sock_alloc : ByteLength -> IO BufPtr
125138sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
126139
140+||| The metadata about a socket
127141record Socket : Type where
128142 MkSocket : (descriptor : SocketDescriptor) ->
129143 (family : SocketFamily) ->
@@ -131,20 +145,21 @@ record Socket : Type where
131145 (protocolNumber : ProtocolNumber) ->
132146 Socket
133147
148+||| Get the C error number
134149getErrno : IO Int
135150getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
136151
137−-- Creates a UNIX socket with the given family, socket type and protocol number.
138−-- Returns either a socket or an error.
152+||| Creates a UNIX socket with the given family, socket type and protocol
153+||| number. Returns either a socket or an error.
139154socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
140155socket sf st pn = do
141156 socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
142157 if socket_res == -1 then -- error
143158 map Left getErrno
144− else
159+ else
145160 return $ Right (MkSocket socket_res sf st pn)
146161
147−
162+||| Close a socket
148163close : Socket -> IO ()
149164close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
150165
@@ -153,18 +168,18 @@ saString : (Maybe SocketAddress) -> String
153168saString (Just sa) = show sa
154169saString Nothing = ""
155170
156−-- Binds a socket to the given socket address and port.
157−-- Returns 0 on success, an error code otherwise.
171+||| Binds a socket to the given socket address and port.
172+||| Returns 0 on success, an error code otherwise.
158173bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
159174bind sock addr port = do
160− bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)
175+ bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)
161176 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)
162177 if bind_res == (-1) then -- error
163178 getErrno
164179 else return 0 -- Success
165180
166−-- Connects to a given address and port.
167−-- Returns 0 on success, and an error number on error.
181+||| Connects to a given address and port.
182+||| Returns 0 on success, and an error number on error.
168183connect : Socket -> SocketAddress -> Port -> IO Int
169184connect sock addr port = do
170185 conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
@@ -173,7 +188,7 @@ connect sock addr port = do
173188 getErrno
174189 else return 0
175190
176−-- Listens on a bound socket.
191+||| Listens on a bound socket.
177192listen : Socket -> IO Int
178193listen sock = do
179194 listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
@@ -181,7 +196,7 @@ listen sock = do
181196 getErrno
182197 else return 0
183198
184−-- Parses a textual representation of an IPv4 address into a SocketAddress
199+||| Parses a textual representation of an IPv4 address into a SocketAddress
185200parseIPv4 : String -> SocketAddress
186201parseIPv4 str = case splitted of
187202 (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
@@ -194,7 +209,7 @@ parseIPv4 str = case splitted of
194209 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
195210
196211
197−-- Retrieves a socket address from a sockaddr pointer
212+||| Retrieves a socket address from a sockaddr pointer
198213getSockAddr : SockaddrPtr -> IO SocketAddress
199214getSockAddr (SAPtr ptr) = do
200215 addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
@@ -256,13 +271,13 @@ recv sock len = do
256271 return $ Right (payload, recv_res)
257272
258273
259−-- Sends the data in a given memory location
274+||| Sends the data in a given memory location
260275sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
261276sendBuf sock (BPtr ptr) len = do
262277 send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
263278 if send_res == (-1) then
264279 map Left getErrno
265− else
280+ else
266281 return $ Right send_res
267282
268283recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
@@ -313,7 +328,7 @@ recvFrom sock bl = do
313328 recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)
314329 (descriptor sock) bl
315330 let recv_ptr' = RFPtr recv_ptr
316− if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
331+ if !(nullPtr recv_ptr) then
317332 map Left getErrno
318333 else do
319334 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
@@ -332,7 +347,7 @@ recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrI
332347recvFromBuf sock (BPtr ptr) bl = do
333348 recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl
334349 let recv_ptr' = RFPtr recv_ptr
335− if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
350+ if !(nullPtr recv_ptr) then
336351 map Left getErrno
337352 else do
338353 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
@@ -345,5 +360,4 @@ recvFromBuf sock (BPtr ptr) bl = do
345360 freeRecvfromStruct recv_ptr'
346361 return $ Right (MkUDPAddrInfo addr port, result + 1)
347362
348−
349363
libs/prelude/Builtins.idr+15−13
@@ -5,11 +5,10 @@
55
66||| The canonical single-element type, also known as the trivially
77||| true proposition.
8−%elim
9− data Unit =
10− ||| The trivial constructor for `()`.
11− MkUnit
12−
8+%elim data Unit =
9+ ||| The trivial constructor for `()`.
10+ MkUnit
11+
1312||| The non-dependent pair type, also known as conjunction.
1413||| @A the type of the left elements in the pair
1514||| @B the type of the left elements in the pair
@@ -18,10 +17,15 @@ data Pair : (A : Type) -> (B : Type) -> Type where
1817 ||| @a the left element of the pair
1918 ||| @b the right element of the pair
2019 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
21−
22−||| Dependent pairs, in their internal representation
23−||| @ a the type of the witness
24−||| @ P the type of the proof
20+
21+||| Dependent pairs
22+|||
23+||| Dependent pairs represent existential quantification - they consist of a
24+||| witness for the existential claim and a proof that the property holds for
25+||| it. Another way to see dependent pairs is as just data - for instance, the
26+||| length of a vector paired with that vector.
27+|||
28+||| @ a the type of the witness @ P the type of the proof
2529data Sigma : (a : Type) -> (P : a -> Type) -> Type where
2630 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
2731
@@ -43,7 +47,6 @@ infix 5 ~=~
4347(~=~) : (x : a) -> (y : b) -> Type
4448(~=~) x y = (=) _ _ x y
4549
46−-- ------------------------------------------------------ [ For rewrite tactic ]
4750||| Perform substitution in a term according to some equality.
4851|||
4952||| This is used by the `rewrite` tactic and term.
@@ -95,7 +98,7 @@ namespace Ownership
9598 ||| A read-only version of a unique value
9699 data Borrowed : UniqueType -> NullType where
97100 Read : {a : UniqueType} -> a -> Borrowed a
98−
101+
99102 ||| Make a read-only version of a unique value, which can be passed to another
100103 ||| function without the unique value being consumed.
101104 implicit
@@ -104,7 +107,7 @@ namespace Ownership
104107
105108par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type
106109 -- is better in any case?
107−par (Delay x) = x
110+par (Delay x) = x
108111
109112malloc : Int -> a -> a
110113malloc size x = x -- compiled specially
@@ -135,4 +138,3 @@ believe_me x = prim__believe_me _ _ x
135138public %assert_total
136139really_believe_me : a -> b
137140really_believe_me x = prim__believe_me _ _ x
138−
libs/prelude/Prelude.idr+8
@@ -494,6 +494,7 @@ getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
494494
495495---- some basic file handling
496496
497+||| A file handle
497498abstract
498499data File = FHandle Ptr
499500
@@ -592,6 +593,7 @@ partial
592593do_feof : Ptr -> IO Int
593594do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
594595
596+||| Check if a file handle has reached the end
595597feof : File -> IO Bool
596598feof (FHandle h) = do eof <- do_feof h
597599 return (not (eof == 0))
@@ -608,6 +610,7 @@ fpoll : File -> IO Bool
608610fpoll (FHandle h) = do p <- mkForeign (FFun "fpoll" [FPtr] FInt) h
609611 return (p > 0)
610612
613+||| Check if a foreign pointer is null
611614partial
612615nullPtr : Ptr -> IO Bool
613616nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
@@ -630,6 +633,10 @@ validFile : File -> IO Bool
630633validFile (FHandle h) = do x <- nullPtr h
631634 return (not x)
632635
636+||| Loop while some test is true
637+|||
638+||| @ test the condition of the loop
639+||| @ body the loop body
633640partial -- obviously
634641while : (test : IO Bool) -> (body : IO ()) -> IO ()
635642while t b = do v <- t
@@ -637,6 +644,7 @@ while t b = do v <- t
637644 while t b
638645 else return ()
639646
647+||| Read the contents of a file into a string
640648partial -- no error checking!
641649readFile : String -> IO String
642650readFile fn = do h <- openFile fn Read
src/Idris/AbsSyntaxTree.hs+2−2
@@ -1020,14 +1020,14 @@ data SyntaxInfo = Syn { using :: [Using],
10201020 maxline :: Maybe Int,
10211021 mut_nesting :: Int,
10221022 dsl_info :: DSL,
1023− syn_in_quasiquote :: Bool }
1023+ syn_in_quasiquote :: Int }
10241024 deriving Show
10251025{-!
10261026deriving instance NFData SyntaxInfo
10271027deriving instance Binary SyntaxInfo
10281028!-}
10291029
1030−defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL False
1030+defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
10311031
10321032expandNS :: SyntaxInfo -> Name -> Name
10331033expandNS syn n@(NS _ _) = n
src/Idris/Docs.hs+3−3
@@ -15,7 +15,9 @@ import Data.List
1515import qualified Data.Text as T
1616
1717-- TODO: Only include names with public/abstract accessibility
18−
18+--
19+-- Issue #1573 on the Issue tracker.
20+-- https://github.com/idris-lang/Idris-dev/issues/1573
1921data FunDoc = FD Name (Docstring (Maybe Term))
2022 [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))] -- args: name, ty, implicit, docs
2123 PTerm -- function type
@@ -203,5 +205,3 @@ pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "ty
203205 t (Str _) = PConstant StrType
204206 t (Ch c) = PConstant $ AType (ATInt ITChar)
205207 t _ = PType
206−
207−
src/Idris/ElabQuasiquote.hs+125−122
@@ -5,167 +5,170 @@ import Idris.Core.TT
55import Idris.AbsSyntax
66
77
8−extract1 :: (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
9−extract1 c tm = do (tm', ex) <- extractUnquotes tm
10− return (c tm', ex)
8+extract1 :: Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
9+extract1 n c tm = do (tm', ex) <- extractUnquotes n tm
10+ return (c tm', ex)
1111
12−extract2 :: (PTerm -> PTerm -> a) -> PTerm -> PTerm -> Elab' aux (a, [(Name, PTerm)])
13−extract2 c a b = do (a', ex1) <- extractUnquotes a
14− (b', ex2) <- extractUnquotes b
15− return (c a' b', ex1 ++ ex2)
12+extract2 :: Int -> (PTerm -> PTerm -> a) -> PTerm -> PTerm -> Elab' aux (a, [(Name, PTerm)])
13+extract2 n c a b = do (a', ex1) <- extractUnquotes n a
14+ (b', ex2) <- extractUnquotes n b
15+ return (c a' b', ex1 ++ ex2)
1616
17−extractTUnquotes :: PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
18−extractTUnquotes (Rewrite t) = extract1 Rewrite t
19−extractTUnquotes (Induction t) = extract1 Induction t
20−extractTUnquotes (LetTac n t) = extract1 (LetTac n) t
21−extractTUnquotes (LetTacTy n t1 t2) = extract2 (LetTacTy n) t1 t2
22−extractTUnquotes (Exact tm) = extract1 Exact tm
23−extractTUnquotes (Try tac1 tac2)
24− = do (tac1', ex1) <- extractTUnquotes tac1
25− (tac2', ex2) <- extractTUnquotes tac2
17+extractTUnquotes :: Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
18+extractTUnquotes n (Rewrite t) = extract1 n Rewrite t
19+extractTUnquotes n (Induction t) = extract1 n Induction t
20+extractTUnquotes n (LetTac name t) = extract1 n (LetTac name) t
21+extractTUnquotes n (LetTacTy name t1 t2) = extract2 n (LetTacTy name) t1 t2
22+extractTUnquotes n (Exact tm) = extract1 n Exact tm
23+extractTUnquotes n (Try tac1 tac2)
24+ = do (tac1', ex1) <- extractTUnquotes n tac1
25+ (tac2', ex2) <- extractTUnquotes n tac2
2626 return (Try tac1' tac2', ex1 ++ ex2)
27−extractTUnquotes (TSeq tac1 tac2)
28− = do (tac1', ex1) <- extractTUnquotes tac1
29− (tac2', ex2) <- extractTUnquotes tac2
27+extractTUnquotes n (TSeq tac1 tac2)
28+ = do (tac1', ex1) <- extractTUnquotes n tac1
29+ (tac2', ex2) <- extractTUnquotes n tac2
3030 return (TSeq tac1' tac2', ex1 ++ ex2)
31−extractTUnquotes (ApplyTactic t) = extract1 ApplyTactic t
32−extractTUnquotes (ByReflection t) = extract1 ByReflection t
33−extractTUnquotes (Reflect t) = extract1 Reflect t
34−extractTUnquotes (GoalType s tac)
35− = do (tac', ex) <- extractTUnquotes tac
31+extractTUnquotes n (ApplyTactic t) = extract1 n ApplyTactic t
32+extractTUnquotes n (ByReflection t) = extract1 n ByReflection t
33+extractTUnquotes n (Reflect t) = extract1 n Reflect t
34+extractTUnquotes n (GoalType s tac)
35+ = do (tac', ex) <- extractTUnquotes n tac
3636 return (GoalType s tac', ex)
37−extractTUnquotes (TCheck t) = extract1 TCheck t
38−extractTUnquotes (TEval t) = extract1 TEval t
39−extractTUnquotes tac = return (tac, []) -- the rest don't contain PTerms
37+extractTUnquotes n (TCheck t) = extract1 n TCheck t
38+extractTUnquotes n (TEval t) = extract1 n TEval t
39+extractTUnquotes n tac = return (tac, []) -- the rest don't contain PTerms
4040
41−extractPArgUnquotes :: PArg -> Elab' aux (PArg, [(Name, PTerm)])
42−extractPArgUnquotes (PImp p m opts n t) =
43− do (t', ex) <- extractUnquotes t
41+extractPArgUnquotes :: Int -> PArg -> Elab' aux (PArg, [(Name, PTerm)])
42+extractPArgUnquotes d (PImp p m opts n t) =
43+ do (t', ex) <- extractUnquotes d t
4444 return (PImp p m opts n t', ex)
45−extractPArgUnquotes (PExp p opts n t) =
46− do (t', ex) <- extractUnquotes t
45+extractPArgUnquotes d (PExp p opts n t) =
46+ do (t', ex) <- extractUnquotes d t
4747 return (PExp p opts n t', ex)
48−extractPArgUnquotes (PConstraint p opts n t) =
49− do (t', ex) <- extractUnquotes t
48+extractPArgUnquotes d (PConstraint p opts n t) =
49+ do (t', ex) <- extractUnquotes d t
5050 return (PConstraint p opts n t', ex)
51−extractPArgUnquotes (PTacImplicit p opts n scpt t) =
52− do (scpt', ex1) <- extractUnquotes scpt
53− (t', ex2) <- extractUnquotes t
51+extractPArgUnquotes d (PTacImplicit p opts n scpt t) =
52+ do (scpt', ex1) <- extractUnquotes d scpt
53+ (t', ex2) <- extractUnquotes d t
5454 return (PTacImplicit p opts n scpt' t', ex1 ++ ex2)
5555
56−extractDoUnquotes :: PDo -> Elab' aux (PDo, [(Name, PTerm)])
57−extractDoUnquotes (DoExp fc tm)
58− = do (tm', ex) <- extractUnquotes tm
56+extractDoUnquotes :: Int -> PDo -> Elab' aux (PDo, [(Name, PTerm)])
57+extractDoUnquotes d (DoExp fc tm)
58+ = do (tm', ex) <- extractUnquotes d tm
5959 return (DoExp fc tm', ex)
60−extractDoUnquotes (DoBind fc n tm)
61− = do (tm', ex) <- extractUnquotes tm
60+extractDoUnquotes d (DoBind fc n tm)
61+ = do (tm', ex) <- extractUnquotes d tm
6262 return (DoBind fc n tm', ex)
63−extractDoUnquotes (DoBindP fc t t' alts)
63+extractDoUnquotes d (DoBindP fc t t' alts)
6464 = fail "Pattern-matching binds cannot be quasiquoted"
65−extractDoUnquotes (DoLet fc n v b)
66− = do (v', ex1) <- extractUnquotes v
67− (b', ex2) <- extractUnquotes b
65+extractDoUnquotes d (DoLet fc n v b)
66+ = do (v', ex1) <- extractUnquotes d v
67+ (b', ex2) <- extractUnquotes d b
6868 return (DoLet fc n v' b', ex1 ++ ex2)
69−extractDoUnquotes (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"
69+extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"
7070
7171
72−extractUnquotes :: PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
73−extractUnquotes (PLam n ty body)
74− = do (ty', ex1) <- extractUnquotes ty
75− (body', ex2) <- extractUnquotes body
76− return (PLam n ty' body', ex1 ++ ex2)
77−extractUnquotes (PPi plicity n ty body)
78− = do (ty', ex1) <- extractUnquotes ty
79− (body', ex2) <- extractUnquotes body
80− return (PPi plicity n ty' body', ex1 ++ ex2)
81−extractUnquotes (PLet n ty val body)
82− = do (ty', ex1) <- extractUnquotes ty
83− (val', ex2) <- extractUnquotes val
84− (body', ex3) <- extractUnquotes body
85− return (PLet n ty' val' body', ex1 ++ ex2 ++ ex3)
86−extractUnquotes (PTyped tm ty)
87− = do (tm', ex1) <- extractUnquotes tm
88− (ty', ex2) <- extractUnquotes ty
72+extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
73+extractUnquotes n (PLam name ty body)
74+ = do (ty', ex1) <- extractUnquotes n ty
75+ (body', ex2) <- extractUnquotes n body
76+ return (PLam name ty' body', ex1 ++ ex2)
77+extractUnquotes n (PPi plicity name ty body)
78+ = do (ty', ex1) <- extractUnquotes n ty
79+ (body', ex2) <- extractUnquotes n body
80+ return (PPi plicity name ty' body', ex1 ++ ex2)
81+extractUnquotes n (PLet name ty val body)
82+ = do (ty', ex1) <- extractUnquotes n ty
83+ (val', ex2) <- extractUnquotes n val
84+ (body', ex3) <- extractUnquotes n body
85+ return (PLet name ty' val' body', ex1 ++ ex2 ++ ex3)
86+extractUnquotes n (PTyped tm ty)
87+ = do (tm', ex1) <- extractUnquotes n tm
88+ (ty', ex2) <- extractUnquotes n ty
8989 return (PTyped tm' ty', ex1 ++ ex2)
90−extractUnquotes (PApp fc f args)
91− = do (f', ex1) <- extractUnquotes f
92− args' <- mapM extractPArgUnquotes args
90+extractUnquotes n (PApp fc f args)
91+ = do (f', ex1) <- extractUnquotes n f
92+ args' <- mapM (extractPArgUnquotes n) args
9393 let (args'', exs) = unzip args'
9494 return (PApp fc f' args'', ex1 ++ concat exs)
95−extractUnquotes (PAppBind fc f args)
96− = do (f', ex1) <- extractUnquotes f
97− args' <- mapM extractPArgUnquotes args
95+extractUnquotes n (PAppBind fc f args)
96+ = do (f', ex1) <- extractUnquotes n f
97+ args' <- mapM (extractPArgUnquotes n) args
9898 let (args'', exs) = unzip args'
9999 return (PAppBind fc f' args'', ex1 ++ concat exs)
100−extractUnquotes (PCase fc expr cases)
101− = do (expr', ex1) <- extractUnquotes expr
100+extractUnquotes n (PCase fc expr cases)
101+ = do (expr', ex1) <- extractUnquotes n expr
102102 let (pats, rhss) = unzip cases
103− (pats', exs1) <- fmap unzip $ mapM extractUnquotes pats
104− (rhss', exs2) <- fmap unzip $ mapM extractUnquotes rhss
103+ (pats', exs1) <- fmap unzip $ mapM (extractUnquotes n) pats
104+ (rhss', exs2) <- fmap unzip $ mapM (extractUnquotes n) rhss
105105 return (PCase fc expr' (zip pats' rhss'), ex1 ++ concat exs1 ++ concat exs2)
106−extractUnquotes (PRefl fc x)
107− = do (x', ex) <- extractUnquotes x
106+extractUnquotes n (PRefl fc x)
107+ = do (x', ex) <- extractUnquotes n x
108108 return (PRefl fc x', ex)
109−extractUnquotes (PEq fc at bt a b)
110− = do (at', ex1) <- extractUnquotes at
111− (bt', ex2) <- extractUnquotes bt
112− (a', ex1) <- extractUnquotes a
113− (b', ex2) <- extractUnquotes b
109+extractUnquotes n (PEq fc at bt a b)
110+ = do (at', ex1) <- extractUnquotes n at
111+ (bt', ex2) <- extractUnquotes n bt
112+ (a', ex1) <- extractUnquotes n a
113+ (b', ex2) <- extractUnquotes n b
114114 return (PEq fc at' bt' a' b', ex1 ++ ex2)
115−extractUnquotes (PRewrite fc x y z)
116− = do (x', ex1) <- extractUnquotes x
117− (y', ex2) <- extractUnquotes y
115+extractUnquotes n (PRewrite fc x y z)
116+ = do (x', ex1) <- extractUnquotes n x
117+ (y', ex2) <- extractUnquotes n y
118118 case z of
119− Just zz -> do (z', ex3) <- extractUnquotes zz
119+ Just zz -> do (z', ex3) <- extractUnquotes n zz
120120 return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)
121121 Nothing -> return (PRewrite fc x' y' Nothing, ex1 ++ ex2)
122−extractUnquotes (PPair fc info l r)
123− = do (l', ex1) <- extractUnquotes l
124− (r', ex2) <- extractUnquotes r
122+extractUnquotes n (PPair fc info l r)
123+ = do (l', ex1) <- extractUnquotes n l
124+ (r', ex2) <- extractUnquotes n r
125125 return (PPair fc info l' r', ex1 ++ ex2)
126−extractUnquotes (PDPair fc info a b c)
127− = do (a', ex1) <- extractUnquotes a
128− (b', ex2) <- extractUnquotes b
129− (c', ex3) <- extractUnquotes c
126+extractUnquotes n (PDPair fc info a b c)
127+ = do (a', ex1) <- extractUnquotes n a
128+ (b', ex2) <- extractUnquotes n b
129+ (c', ex3) <- extractUnquotes n c
130130 return (PDPair fc info a' b' c', ex1 ++ ex2 ++ ex3)
131−extractUnquotes (PAlternative b alts)
132− = do alts' <- mapM extractUnquotes alts
131+extractUnquotes n (PAlternative b alts)
132+ = do alts' <- mapM (extractUnquotes n) alts
133133 let (alts'', exs) = unzip alts'
134134 return (PAlternative b alts'', concat exs)
135−extractUnquotes (PHidden tm)
136− = do (tm', ex) <- extractUnquotes tm
135+extractUnquotes n (PHidden tm)
136+ = do (tm', ex) <- extractUnquotes n tm
137137 return (PHidden tm', ex)
138−extractUnquotes (PGoal fc a n b)
139− = do (a', ex1) <- extractUnquotes a
140− (b', ex2) <- extractUnquotes b
141− return (PGoal fc a' n b', ex1 ++ ex2)
142−extractUnquotes (PDoBlock steps)
143− = do steps' <- mapM extractDoUnquotes steps
138+extractUnquotes n (PGoal fc a name b)
139+ = do (a', ex1) <- extractUnquotes n a
140+ (b', ex2) <- extractUnquotes n b
141+ return (PGoal fc a' name b', ex1 ++ ex2)
142+extractUnquotes n (PDoBlock steps)
143+ = do steps' <- mapM (extractDoUnquotes n) steps
144144 let (steps'', exs) = unzip steps'
145145 return (PDoBlock steps'', concat exs)
146−extractUnquotes (PIdiom fc tm)
147− = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes tm
148−extractUnquotes (PProof tacs)
149− = do (tacs', exs) <- fmap unzip $ mapM extractTUnquotes tacs
146+extractUnquotes n (PIdiom fc tm)
147+ = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes n tm
148+extractUnquotes n (PProof tacs)
149+ = do (tacs', exs) <- fmap unzip $ mapM (extractTUnquotes n) tacs
150150 return (PProof tacs', concat exs)
151−extractUnquotes (PTactics tacs)
152− = do (tacs', exs) <- fmap unzip $ mapM extractTUnquotes tacs
151+extractUnquotes n (PTactics tacs)
152+ = do (tacs', exs) <- fmap unzip $ mapM (extractTUnquotes n) tacs
153153 return (PTactics tacs', concat exs)
154−extractUnquotes (PElabError err) = fail "Can't quasiquote an error"
155−extractUnquotes (PCoerced tm)
156− = do (tm', ex) <- extractUnquotes tm
154+extractUnquotes n (PElabError err) = fail "Can't quasiquote an error"
155+extractUnquotes n (PCoerced tm)
156+ = do (tm', ex) <- extractUnquotes n tm
157157 return (PCoerced tm', ex)
158−extractUnquotes (PDisamb ns tm)
159− = do (tm', ex) <- extractUnquotes tm
158+extractUnquotes n (PDisamb ns tm)
159+ = do (tm', ex) <- extractUnquotes n tm
160160 return (PDisamb ns tm', ex)
161−extractUnquotes (PUnifyLog tm)
162− = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes tm
163−extractUnquotes (PNoImplicits tm)
164− = fmap (\(tm', ex) -> (PNoImplicits tm', ex)) $ extractUnquotes tm
165−extractUnquotes (PQuasiquote _ _) = fail "Nested quasiquotes not supported"
166−extractUnquotes (PUnquote tm) =
167− do n <- getNameFrom (sMN 0 "unquotation")
168− return (PRef (fileFC "(unquote)") n, [(n, tm)])
169−extractUnquotes x = return (x, []) -- no subterms!
161+extractUnquotes n (PUnifyLog tm)
162+ = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes n tm
163+extractUnquotes n (PNoImplicits tm)
164+ = fmap (\(tm', ex) -> (PNoImplicits tm', ex)) $ extractUnquotes n tm
165+extractUnquotes n (PQuasiquote tm goal)
166+ = fmap (\(tm', ex) -> (PQuasiquote tm' goal, ex)) $ extractUnquotes (n+1) tm
167+extractUnquotes n (PUnquote tm)
168+ | n == 0 = do n <- getNameFrom (sMN 0 "unquotation")
169+ return (PRef (fileFC "(unquote)") n, [(n, tm)])
170+ | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
171+ extractUnquotes (n-1) tm
172+extractUnquotes n x = return (x, []) -- no subterms!
170173
171174
src/Idris/ElabTerm.hs+44−60
@@ -18,7 +18,7 @@ import Idris.Core.Typecheck (check, recheck)
1818import Idris.ErrReverse (errReverse)
1919import Idris.ElabQuasiquote (extractUnquotes)
2020import Idris.Elab.Utils
21−import qualified Util.Pretty as U
21+import qualified Util.Pretty as U
2222
2323import Control.Applicative ((<$>))
2424import Control.Monad
@@ -76,9 +76,9 @@ build ist info emode opts fn tm
7676 u <- getUnifyLog
7777 hs <- get_holes
7878
79− when (not pattern) $
79+ when (not pattern) $
8080 traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++
81− "Remaining problems:\n" ++ qshow probs) $
81+ "Remaining problems:\n" ++ qshow probs) $
8282 do unify_all; matchProblems True; unifyProblems
8383
8484 probs <- get_probs
@@ -99,7 +99,7 @@ build ist info emode opts fn tm
9999 else return (tm, ds, is)
100100 where pattern = emode == ELHS
101101 tydecl = emode == ETyDecl
102−
102+
103103 mkPat = do hs <- get_holes
104104 tm <- get_term
105105 case hs of
@@ -197,14 +197,14 @@ elab ist info emode opts fn tm
197197 -- ++ "\nholes " ++ show hs
198198 -- ++ "\nproblems " ++ show ps
199199 -- ++ "\n-----------\n") $
200− --trace ("ELAB " ++ show t') $
200+ --trace ("ELAB " ++ show t') $
201201 let fc = fileFC "Force"
202202 env <- get_env
203203 handleError (forceErr env)
204204 (elab' ina t')
205205 (elab' ina (PApp fc (PRef fc (sUN "Force"))
206206 [pimp (sUN "t") Placeholder True,
207− pimp (sUN "a") Placeholder True,
207+ pimp (sUN "a") Placeholder True,
208208 pexp ct])) True
209209
210210 forceErr env (CantUnify _ t t' _ _ _)
@@ -240,9 +240,9 @@ elab ist info emode opts fn tm
240240 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
241241 elab' ina PType = do apply RType []; solve
242242 elab' ina (PUniverse u) = do apply (RUType u) []; solve
243−-- elab' (_,_,inty) (PConstant c)
243+-- elab' (_,_,inty) (PConstant c)
244244-- | constType c && pattern && not reflection && not inty
245−-- = lift $ tfail (Msg "Typecase is not allowed")
245+-- = lift $ tfail (Msg "Typecase is not allowed")
246246 elab' ina (PConstant c) = do apply (RConstant c) []; solve
247247 elab' ina (PQuote r) = do fill r; solve
248248 elab' ina (PTrue fc _) =
@@ -338,7 +338,7 @@ elab ist info emode opts fn tm
338338-- elab' (_, _, inty) (PRef fc f)
339339-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
340340-- = lift $ tfail (Msg "Typecase is not allowed")
341− elab' (ina, guarded, inty, qq) (PRef fc n)
341+ elab' (ina, guarded, inty, qq) (PRef fc n)
342342 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq
343343 = do ctxt <- get_context
344344 let defined = case lookupTy n ctxt of
@@ -363,7 +363,7 @@ elab ist info emode opts fn tm
363363 = do -- if n is a type constructor name, this makes no sense...
364364 ctxt <- get_context
365365 when (isTConName n ctxt) $
366− lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
366+ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
367367 checkPiGoal n
368368 attack; intro (Just n);
369369 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
@@ -373,7 +373,7 @@ elab ist info emode opts fn tm
373373 -- if n is a type constructor name, this makes no sense...
374374 ctxt <- get_context
375375 when (isTConName n ctxt) $
376− lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
376+ lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
377377 checkPiGoal n
378378 claim tyn RType
379379 explicit tyn
@@ -539,7 +539,7 @@ elab ist info emode opts fn tm
539539 sortBy cmpArg (zip ns args)
540540 ulog <- getUnifyLog
541541 elabArgs ist (ina || not isinf, guarded, inty, qq)
542− [] fc False f ns'
542+ [] fc False f ns'
543543 (f == sUN "Force")
544544 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
545545 solve
@@ -558,7 +558,7 @@ elab ist info emode opts fn tm
558558 else movelast n)
559559 (ivs' \\ ivs)
560560 where -- normal < alternatives < lambdas < rewrites < tactic < default tactic
561− -- reason for lambdas after alternatives is that having
561+ -- reason for lambdas after alternatives is that having
562562 -- the alternative resolved can help with typechecking the lambda
563563 -- or the rewrite. Rewrites/tactics need as much information
564564 -- as possible about the type.
@@ -568,7 +568,7 @@ elab ist info emode opts fn tm
568568 | constraint x && not (constraint y) = LT
569569 | constraint y && not (constraint x) = GT
570570 | otherwise
571− = compare (conDepth 0 (getTm x) + priority x + alt x)
571+ = compare (conDepth 0 (getTm x) + priority x + alt x)
572572 (conDepth 0 (getTm y) + priority y + alt y)
573573 where alt t = case getTm t of
574574 PAlternative False _ -> 5
@@ -581,14 +581,14 @@ elab ist info emode opts fn tm
581581
582582 constraint (PConstraint _ _ _ _) = True
583583 constraint _ = False
584−
584+
585585 -- Score a point for every level where there is a non-constructor
586586 -- function (so higher score --> done later)
587587 -- Only relevant when on lhs
588588 conDepth d t | not pattern = 0
589589 conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0
590590 | otherwise = max (100 - d) 1
591− conDepth d (PApp _ f as)
591+ conDepth d (PApp _ f as)
592592 = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))
593593 conDepth d (PPatvar _ _) = 0
594594 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)
@@ -602,7 +602,7 @@ elab ist info emode opts fn tm
602602 Nothing -> return ()
603603 Just b ->
604604 case unApply (binderTy b) of
605− (P _ c _, args) ->
605+ (P _ c _, args) ->
606606 case lookupCtxt c (idris_classes ist) of
607607 [] -> return ()
608608 _ -> -- type class, set as injective
@@ -615,7 +615,7 @@ elab ist info emode opts fn tm
615615 probs <- get_probs
616616 traceWhen ulog (qshow probs) $ return ()
617617 _ -> return ()
618−
618+
619619 setinjArg (P _ n _) = setinj n
620620 setinjArg _ = return ()
621621
@@ -634,7 +634,7 @@ elab ist info emode opts fn tm
634634 solve
635635 elab' ina Placeholder = do (h : hs) <- get_holes
636636 movelast h
637− elab' ina (PMetavar n) =
637+ elab' ina (PMetavar n) =
638638 do ptm <- get_term
639639 -- When building the metavar application, leave out the unique
640640 -- names which have been used elsewhere in the term, since we
@@ -699,21 +699,6 @@ elab ist info emode opts fn tm
699699 args <- get_env
700700 envU <- mapM (getKind args) args
701701 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
702−-- ++ allNamesIn scr
703−
704− -- in the definition we build for the case, only pass through
705− -- names which are directly used, type class constraints, and
706− -- variables any of these depend on
707− -- FIXME: This probably doesn't help us, but leaving it in
708− -- temporarily (but commented out). If this comment is still
709− -- here in master, please delete the code!
710−-- let directUse = filter (\n -> usedIn namesUsedInRHS n
711−-- || tcName (binderTy (snd n))) args
712−-- let args' = args -- chaseDeps args (map fst directUse) directUse
713−-- let argsDropped = map fst $
714−-- filter (\(n, _) -> case lookup n args' of
715−-- Nothing -> True
716−-- _ -> False) args
717702
718703 -- Drop the unique arguments used in the scrutinee (since it's
719704 -- not valid to use them again anyway)
@@ -724,7 +709,7 @@ elab ist info emode opts fn tm
724709 let cname' = mkN cname
725710-- elab' ina (PMetavar cname')
726711 attack; defer argsDropped cname'; solve
727−
712+
728713 -- if the scrutinee is one of the 'args' in env, we should
729714 -- inspect it directly, rather than adding it as a new argument
730715 let newdef = PClauses fc [] cname'
@@ -748,10 +733,10 @@ elab ist info emode opts fn tm
748733 Just u -> u
749734 _ -> False
750735
751− getKind env (n, _)
736+ getKind env (n, _)
752737 = case lookup n env of
753738 Nothing -> return (n, False) -- can't happen, actually...
754− Just b ->
739+ Just b ->
755740 do ty <- get_type (forget (binderTy b))
756741 case ty of
757742 UType UniqueType -> return (n, True)
@@ -764,8 +749,8 @@ elab ist info emode opts fn tm
764749 _ -> False
765750 tcName _ = False
766751
767− usedIn ns (n, b)
768− = n `elem` ns
752+ usedIn ns (n, b)
753+ = n `elem` ns
769754 || any (\x -> x `elem` ns) (allTTNames (binderTy b))
770755
771756 -- FIXME: This probably doesn't help us here, but leaving
@@ -791,7 +776,7 @@ elab ist info emode opts fn tm
791776 = do -- First extract the unquoted subterms, replacing them with fresh
792777 -- names in the quasiquoted term. Claim their reflections to be
793778 -- of type TT.
794− (t, unq) <- extractUnquotes t
779+ (t, unq) <- extractUnquotes 0 t
795780 let unquoteNames = map fst unq
796781 mapM_ (flip claim (Var tt)) unquoteNames
797782
@@ -872,7 +857,7 @@ elab ist info emode opts fn tm
872857 isScr (PRef _ n) (n', b) = (n', (n == n', b))
873858 isScr _ (n', b) = (n', (False, b))
874859
875− caseBlock :: FC -> Name ->
860+ caseBlock :: FC -> Name ->
876861 [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]
877862 caseBlock fc n env opts
878863 = let args' = findScr env
@@ -882,12 +867,12 @@ elab ist info emode opts fn tm
882867 where -- Find the variable we want as the scrutinee and mark it as
883868 -- 'True'. If the scrutinee is in the environment, match on that
884869 -- otherwise match on the new argument we're adding.
885− findScr ((n, (True, t)) : xs)
870+ findScr ((n, (True, t)) : xs)
886871 = (n, (True, t)) : scrName n xs
887− findScr [(n, (_, t))] = [(n, (True, t))]
872+ findScr [(n, (_, t))] = [(n, (True, t))]
888873 findScr (x : xs) = x : findScr xs
889874 -- [] can't happen since scrutinee is in the environment!
890−
875+
891876 -- To make sure top level pattern name remains in scope, put
892877 -- it at the end of the environment
893878 scrName n [] = []
@@ -931,7 +916,7 @@ elab ist info emode opts fn tm
931916 _ -> return t
932917 where
933918 mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)
934− mkDelay env t
919+ mkDelay env t
935920 = let fc = fileFC "Delay" in
936921 addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))
937922 [pexp t])
@@ -998,10 +983,10 @@ elab ist info emode opts fn tm
998983 failed' <- -- trace (show (n, t, hs, tm)) $
999984 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
1000985 case holeName `elem` hs of
1001− True -> do focus holeName;
986+ True -> do focus holeName;
1002987 g <- goal
1003988 ulog <- getUnifyLog
1004− traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
989+ traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
1005990 elab ina t; return failed
1006991 False -> return failed
1007992 done_elaborating_arg f argName
@@ -1057,7 +1042,7 @@ pruneByType env t c as
10571042 getName (PRef _ n) = Just n
10581043 getName (PApp _ f _) = getName f
10591044 getName _ = Nothing
1060−
1045+
10611046pruneByType env (P _ n _) c as
10621047-- if the goal type is polymorphic, keep e
10631048 | [] <- lookupTy n c = as
@@ -1098,11 +1083,11 @@ trivial' ist
10981083 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
10991084proofSearch' ist rec depth prv top n hints
11001085 = do unifyProblems
1101− proofSearch rec prv depth
1086+ proofSearch rec prv depth
11021087 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
11031088
11041089resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()
1105−resolveTC = resTC' []
1090+resolveTC = resTC' []
11061091
11071092resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"
11081093resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True
@@ -1112,7 +1097,7 @@ resTC' tcs defaultOn depth topg fn ist
11121097 ptm <- get_term
11131098 ulog <- getUnifyLog
11141099 hs <- get_holes
1115− traceWhen ulog ("Resolving class " ++ show g) $
1100+ traceWhen ulog ("Resolving class " ++ show g) $
11161101 try' (trivial' ist)
11171102 (do t <- goal
11181103 let (tc, ttypes) = unApply t
@@ -1129,7 +1114,7 @@ resTC' tcs defaultOn depth topg fn ist
11291114
11301115 -- HACK! Rather than giving a special name, better to have some kind
11311116 -- of flag in ClassInfo structure
1132− chaser (UN nm)
1117+ chaser (UN nm)
11331118 | ('@':'@':_) <- str nm = True -- old way
11341119 chaser (SN (ParentN _ _)) = True
11351120 chaser (NS n _) = chaser n
@@ -1173,7 +1158,7 @@ resTC' tcs defaultOn depth topg fn ist
11731158 args <- map snd <$> try' (apply (Var n) imps)
11741159 (match_apply (Var n) imps) True
11751160 ps' <- get_probs
1176− when (length ps < length ps' || unrecoverable ps') $
1161+ when (length ps < length ps' || unrecoverable ps') $
11771162 fail "Can't apply type class"
11781163-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
11791164 mapM_ (\ (_,n) -> do focus n
@@ -1181,7 +1166,7 @@ resTC' tcs defaultOn depth topg fn ist
11811166 let (tc', ttype) = unApply t'
11821167 let got = fst (unApply t)
11831168 let depth' = if tc' `elem` tcs
1184− then depth - 1 else depth
1169+ then depth - 1 else depth
11851170 resTC' (got : tcs) defaultOn depth' topg fn ist)
11861171 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
11871172 -- if there's any arguments left, we've failed to resolve
@@ -1232,11 +1217,11 @@ case_ ind autoSolve ist fn tm = do
12321217-- if a tactic adds unification problems, return an error
12331218
12341219runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()
1235−runTac autoSolve ist fn tac
1220+runTac autoSolve ist fn tac
12361221 = do env <- get_env
12371222 g <- goal
12381223 let tac' = fmap (addImplBound ist (map fst env)) tac
1239− if autoSolve
1224+ if autoSolve
12401225 then runT tac'
12411226 else no_errors (runT tac')
12421227 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
@@ -1398,11 +1383,11 @@ runTac autoSolve ist fn tac
13981383 letbind scriptvar scriptTy (Var script)
13991384 focus script
14001385 ptm <- get_term
1401− elab ist toplevel ERHS [] (sMN 0 "tac")
1386+ elab ist toplevel ERHS [] (sMN 0 "tac")
14021387 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
14031388 (script', _) <- get_type_val (Var scriptvar)
14041389 -- now that we have the script apply
1405− -- it to the reflected goal
1390+ -- it to the reflected goal
14061391 restac <- getNameFrom (sMN 0 "restac")
14071392 claim restac tacticTy
14081393 focus restac
@@ -1482,7 +1467,7 @@ reify _ t = fail ("Unknown tactic " ++ show t)
14821467
14831468reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
14841469reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
1485−reifyApp _ t [Constant (I i)]
1470+reifyApp _ t [Constant (I i)]
14861471 | t == reflm "Search" = return (ProofSearch True True i Nothing [])
14871472reifyApp _ t [x]
14881473 | t == reflm "Refine" = do n <- reifyTTName x
@@ -2223,4 +2208,3 @@ envTupleType
22232208 ]
22242209
22252210solveAll = try (do solve; solveAll) (return ())
2226−
src/Idris/IBC.hs+1−1
@@ -1293,7 +1293,7 @@ instance Binary SyntaxInfo where
12931293 x5 <- get
12941294 x6 <- get
12951295 x7 <- get
1296− return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 False)
1296+ return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 0)
12971297
12981298instance (Binary t) => Binary (PClause' t) where
12991299 put x
src/Idris/ParseExpr.hs+5−5
@@ -605,9 +605,9 @@ constraintArg syn = do symbol "@{"
605605
606606-}
607607quasiquote :: SyntaxInfo -> IdrisParser PTerm
608−quasiquote syn = do guard (not (syn_in_quasiquote syn))
609− symbol "`("
610− e <- expr syn { syn_in_quasiquote = True , inPattern = False}
608+quasiquote syn = do symbol "`("
609+ e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,
610+ inPattern = False }
611611 g <- optional $ do
612612 symbol ":"
613613 expr syn { inPattern = False } -- don't allow antiquotes
@@ -621,9 +621,9 @@ quasiquote syn = do guard (not (syn_in_quasiquote syn))
621621
622622-}
623623unquote :: SyntaxInfo -> IdrisParser PTerm
624−unquote syn = do guard (syn_in_quasiquote syn)
624+unquote syn = do guard (syn_in_quasiquote syn > 0)
625625 symbol "~"
626− e <- simpleExpr syn { syn_in_quasiquote = False }
626+ e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }
627627 return $ PUnquote e
628628 <?> "unquotation"
629629
src/Idris/Parser.hs+7−2
@@ -399,6 +399,9 @@ NameTimesList ::=
399399@
400400-}
401401-- FIXME: Check compatability for function options (i.e. partal/total)
402+--
403+-- Issue #1574 on the issue tracker.
404+-- https://github.com/idris-lang/Idris-dev/issues/1574
402405fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
403406fnOpts opts
404407 = do reserved "total"; fnOpts (TotalFn : opts)
@@ -914,7 +917,7 @@ clause syn
914917
915918{-| Parses with pattern
916919
917−@
920+@
918921WExpr ::= '|' Expr';
919922@
920923-}
@@ -1161,6 +1164,8 @@ parseProg syn fname input mrk
11611164 case runparser mainProg i fname input of
11621165 Failure doc -> do -- FIXME: Get error location from trifecta
11631166 -- this can't be the solution!
1167+ -- Issue #1575 on the issue tracker.
1168+ -- https://github.com/idris-lang/Idris-dev/issues/1575
11641169 let (fc, msg) = findFC doc
11651170 i <- getIState
11661171 case idris_outputmode i of
@@ -1272,7 +1277,7 @@ loadSource lidr f toline
12721277 putIState (i { default_access = Hidden, module_aliases = modAliases })
12731278 clearIBC -- start a new .ibc file
12741279 -- record package info in .ibc
1275− imps <- allImportDirs
1280+ imps <- allImportDirs
12761281 mapM_ addIBC (map IBCImportDir imps)
12771282 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
12781283 let syntax = defaultSyntax{ syn_namespace = reverse mname,
src/Idris/REPL.hs+11−6
@@ -727,7 +727,7 @@ process fn (NewDefn decls) = do
727727 getClauseName (PClause fc name whole with rhs whereBlock) = name
728728 getClauseName (PWith fc name whole with rhs whereBlock) = name
729729 defineName :: [PDecl] -> Idris ()
730− defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do
730+ defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do
731731 elabDecl EAll recinfo tyDecl
732732 elabClauses recinfo fc opts name (concatMap getClauses decls)
733733 setReplDefined (Just name)
@@ -767,7 +767,7 @@ process fn (NewDefn decls) = do
767767 fixClauses :: PDecl' t -> PDecl' t
768768 fixClauses (PClauses fc opts _ css@(clause:cs)) =
769769 PClauses fc opts (getClauseName clause) css
770− fixClauses (PInstance syn fc constraints cls parms ty instName decls) =
770+ fixClauses (PInstance syn fc constraints cls parms ty instName decls) =
771771 PInstance syn fc constraints cls parms ty instName (map fixClauses decls)
772772 fixClauses decl = decl
773773
@@ -777,10 +777,10 @@ process fn (Undefine names) = undefine names
777777 undefine [] = do
778778 allDefined <- idris_repl_defs `fmap` get
779779 undefine' allDefined []
780− -- Keep track of which names you've removed so you can
780+ -- Keep track of which names you've removed so you can
781781 -- print them out to the user afterward
782782 undefine names = undefine' names []
783− undefine' [] list = do iRenderOutput $ printUndefinedNames list
783+ undefine' [] list = do iRenderOutput $ printUndefinedNames list
784784 return ()
785785 undefine' (n:names) already = do
786786 allDefined <- idris_repl_defs `fmap` get
@@ -794,12 +794,12 @@ process fn (Undefine names) = undefine names
794794 -- smart detection of exactly what kind of name we're undefining.
795795 fputState (ctxt_lookup n . known_classes) Nothing
796796 fmodifyState repl_definitions (delete n)
797− undefClosure n =
797+ undefClosure n =
798798 do replDefs <- idris_repl_defs `fmap` get
799799 callGraph <- whoCalls n
800800 let users = case lookup n callGraph of
801801 Just ns -> nub ns
802− Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)
802+ Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)
803803 undefinedJustNow <- concat `fmap` mapM undefClosure users
804804 undefOne n
805805 return (nub (n : undefinedJustNow))
@@ -1361,6 +1361,8 @@ loadInputs inputs toline -- furthest line to read in input source files
13611361 iWarn f $ pprintErr i e'
13621362 ProgramLineComment -> return () -- fail elsewhere
13631363 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1364+ -- Issue #1576 on the issue tracker.
1365+ -- https://github.com/idris-lang/Idris-dev/issues/1576
13641366 iWarn emptyFC $ pprintErr i e)
13651367 where -- load all files, stop if any fail
13661368 tryLoad :: Bool -> [IFileType] -> Idris ()
@@ -1382,6 +1384,9 @@ loadInputs inputs toline -- furthest line to read in input source files
13821384 inew <- getIState
13831385 -- FIXME: Save these in IBC to avoid this hack! Need to
13841386 -- preserve it all from source inputs
1387+ --
1388+ -- Issue #1577 on the issue tracker.
1389+ -- https://github.com/idris-lang/Idris-dev/issues/1577
13851390 let tidata = idris_tyinfodata inew
13861391 let patdefs = idris_patdefs inew
13871392 ok <- noErrors
src/Pkg/Package.hs+7−4
@@ -63,10 +63,10 @@ buildPkg warnonly (install, fp)
6363 -- Also give up if there are metavariables to solve
6464 case (map fst (idris_metavars ist) \\ primDefs) of
6565 _ -> when install $ installPkg pkgdesc
66−-- ms -> do if install
66+-- ms -> do if install
6767-- then putStrLn "Can't install: there are undefined metavariables:"
6868-- else putStrLn "There are undefined metavariables:"
69−-- putStrLn $ "\t" ++ show ms
69+-- putStrLn $ "\t" ++ show ms
7070-- exitWith (ExitFailure 1)
7171
7272-- | Type check packages only
@@ -107,7 +107,7 @@ replPkg fp = do orig <- getIState
107107 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
108108
109109 if (f /= "")
110− then idrisMain ((Filename f) : opts)
110+ then idrisMain ((Filename f) : opts)
111111 else iputStrLn "Can't start REPL: no main module given"
112112 runIO $ setCurrentDirectory dir
113113
@@ -129,6 +129,9 @@ cleanPkg fp
129129-- | Generate IdrisDoc for package
130130-- TODO: Handle case where module does not contain a matching namespace
131131-- E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins
132+--
133+-- Issue number #1572 on the issue tracker
134+-- https://github.com/idris-lang/Idris-dev/issues/1572
132135documentPkg :: FilePath -- ^ Path to .ipkg file.
133136 -> IO ()
134137documentPkg fp =
@@ -143,7 +146,7 @@ documentPkg fp =
143146 make (makefile pkgdesc)
144147 setCurrentDirectory $ pkgDir
145148 let run l = runErrorT . (execStateT l)
146− load [] = return ()
149+ load [] = return ()
147150 load (f:fs) = do loadModule f; load fs
148151 loader = do idrisMain opts; load fs
149152 idrisInstance <- run loader idrisInit