git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of git://github.com/idris-lang/Idris-dev into partial-eval
869e6caEdwin Brady
libs/base/Data/List.idr+9−1
compare with master
unifiedsplit
@@ -2,9 +2,17 @@ module Data.List
2
2
3%access public
3%access public
4
4
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 })`
6data Elem : a -> List a -> Type where
8data 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`
7 Here : Elem x (x :: xs)
12 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)`
8 There : Elem x xs -> Elem x (y :: xs)
16 There : Elem x xs -> Elem x (y :: xs)
9
17
10instance Uninhabited (Elem {a} x []) where
18instance Uninhabited (Elem {a} x []) where
libs/base/Data/Vect/Quantifiers.idr+24−2
@@ -1,9 +1,15 @@
1module Data.Vect.Quantifiers
1module Data.Vect.Quantifiers
2
2
3+||| A proof that some element of a vector satisfies some property
4+|||
5+||| @ P the property to be satsified
3data Any : (P : a -> Type) -> Vect n a -> Type where
6data Any : (P : a -> Type) -> Vect n a -> Type where
7+ ||| A proof that the satisfying element is the first one in the `Vect`
4 Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)
8 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`
5 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
10 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
6
11
12+||| No element of an empty vector satisfies any property
7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
13anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8anyNilAbsurd (Here _) impossible
14anyNilAbsurd (Here _) impossible
9anyNilAbsurd (There _) impossible
15anyNilAbsurd (There _) impossible
@@ -15,7 +21,13 @@ anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) ->
15anyElim _ f (Here p) = f p
21anyElim _ f (Here p) = f p
16anyElim f _ (There p) = f p
22anyElim f _ (There p) = f p
17
23
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
18−any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)
30+any : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)
19any _ Nil = No anyNilAbsurd
31any _ Nil = No anyNilAbsurd
20any p (x::xs) with (p x)
32any p (x::xs) with (p x)
21 | Yes prf = Yes (Here prf)
33 | Yes prf = Yes (Here prf)
@@ -24,10 +36,14 @@ any p (x::xs) with (p x)
24 Yes prf' => Yes (There prf')
36 Yes prf' => Yes (There prf')
25 No prf' => No (anyElim prf' prf)
37 No prf' => No (anyElim prf' prf)
26
38
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`.
27data All : (P : a -> Type) -> Vect n a -> Type where
41data All : (P : a -> Type) -> Vect n a -> Type where
28 Nil : {P : a -> Type} -> All P Nil
42 Nil : {P : a -> Type} -> All P Nil
29 (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs)
43 (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs)
30
44
45+||| If there does not exist an element that satifies the property, then it is
46+||| the case that all elements do not satisfy.
31negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => Not (P x)) xs
47negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => Not (P x)) xs
32negAnyAll {xs=Nil} _ = Nil
48negAnyAll {xs=Nil} _ = Nil
33negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
49negAnyAll {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 :
40notAllThere _ Nil impossible
56notAllThere _ Nil impossible
41notAllThere np (_ :: ps) = np ps
57notAllThere np (_ :: ps) = np ps
42
58
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
43−all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
65+all : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
44all _ Nil = Yes Nil
66all _ Nil = Yes Nil
45all d (x::xs) with (d x)
67all d (x::xs) with (d x)
46 | No prf = No (notAllHere prf)
68 | No prf = No (notAllHere prf)
libs/base/Data/ZZ.idr+18−9
@@ -7,14 +7,18 @@ import Data.Sign
7%access public
7%access public
8
8
9
9
10−||| An integer is either a positive nat or the negated successor of a nat.
10+||| An integer is either a positive `Nat` or the negated successor of a `Nat`.
11+|||
11−||| Zero is arbitrarily chosen to be positive.
12+||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen
13+||| to be positive.
14+|||
12data ZZ = Pos Nat | NegS Nat
15data ZZ = Pos Nat | NegS Nat
13
16
14instance Signed ZZ where
17instance Signed ZZ where
15 sign (Pos _) = Plus
18 sign (Pos _) = Plus
16 sign (NegS _) = Minus
19 sign (NegS _) = Minus
17
20
21+||| Take the absolute value of a `ZZ`
18absZ : ZZ -> Nat
22absZ : ZZ -> Nat
19absZ (Pos n) = n
23absZ (Pos n) = n
20absZ (NegS n) = S n
24absZ (NegS n) = S n
@@ -23,28 +27,32 @@ instance Show ZZ where
23 show (Pos n) = show n
27 show (Pos n) = show n
24 show (NegS n) = "-" ++ show (S n)
28 show (NegS n) = "-" ++ show (S n)
25
29
26−negZ : ZZ -> ZZ
30+instance Neg ZZ where
27−negZ (Pos Z) = Pos Z
31+ negate (Pos Z) = Pos Z
28−negZ (Pos (S n)) = NegS n
32+ negate (Pos (S n)) = NegS n
29−negZ (NegS n) = Pos (S n)
33+ negate (NegS n) = Pos (S n)
30
34
31negNat : Nat -> ZZ
35negNat : Nat -> ZZ
32negNat Z = Pos Z
36negNat Z = Pos Z
33negNat (S n) = NegS n
37negNat (S n) = NegS n
34
38
39+
40+||| Construct a `ZZ` as the difference of two `Nat`s
35minusNatZ : Nat -> Nat -> ZZ
41minusNatZ : Nat -> Nat -> ZZ
36minusNatZ n Z = Pos n
42minusNatZ n Z = Pos n
37minusNatZ Z (S m) = NegS m
43minusNatZ Z (S m) = NegS m
38minusNatZ (S n) (S m) = minusNatZ n m
44minusNatZ (S n) (S m) = minusNatZ n m
39
45
46+||| Add two `ZZ`s. Consider using `(+) {a=ZZ}`.
40plusZ : ZZ -> ZZ -> ZZ
47plusZ : ZZ -> ZZ -> ZZ
41plusZ (Pos n) (Pos m) = Pos (n + m)
48plusZ (Pos n) (Pos m) = Pos (n + m)
42plusZ (NegS n) (NegS m) = NegS (S (n + m))
49plusZ (NegS n) (NegS m) = NegS (S (n + m))
43plusZ (Pos n) (NegS m) = minusNatZ n (S m)
50plusZ (Pos n) (NegS m) = minusNatZ n (S m)
44plusZ (NegS n) (Pos m) = minusNatZ m (S n)
51plusZ (NegS n) (Pos m) = minusNatZ m (S n)
45
52
53+||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
46subZ : ZZ -> ZZ -> ZZ
54subZ : ZZ -> ZZ -> ZZ
47−subZ n m = plusZ n (negZ m)
55+subZ n m = plusZ n (negate m)
48
56
49instance Eq ZZ where
57instance Eq ZZ where
50 (Pos n) == (Pos m) = n == m
58 (Pos n) == (Pos m) = n == m
@@ -58,13 +66,14 @@ instance Ord ZZ where
58 compare (Pos _) (NegS _) = GT
66 compare (Pos _) (NegS _) = GT
59 compare (NegS _) (Pos _) = LT
67 compare (NegS _) (Pos _) = LT
60
68
61−
69+||| Multiply two `ZZ`s. Consider using `(*) {a=ZZ}`.
62multZ : ZZ -> ZZ -> ZZ
70multZ : ZZ -> ZZ -> ZZ
63multZ (Pos n) (Pos m) = Pos $ n * m
71multZ (Pos n) (Pos m) = Pos $ n * m
64multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
72multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
65multZ (NegS n) (Pos m) = negNat $ (S n) * m
73multZ (NegS n) (Pos m) = negNat $ (S n) * m
66multZ (Pos n) (NegS m) = negNat $ n * (S m)
74multZ (Pos n) (NegS m) = negNat $ n * (S m)
67
75
76+||| Convert an `Integer` to an inductive representation.
68fromInt : Integer -> ZZ
77fromInt : Integer -> ZZ
69fromInt n = if n < 0
78fromInt n = if n < 0
70 then NegS $ fromInteger {a=Nat} ((-n) - 1)
79 then NegS $ fromInteger {a=Nat} ((-n) - 1)
@@ -100,7 +109,7 @@ natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
100 -> n * m = x -> (Pos n) * (Pos m) = Pos x
109 -> n * m = x -> (Pos n) * (Pos m) = Pos x
101natMultZMult n m x h = cong h
110natMultZMult n m x h = cong h
102
111
103−doubleNegElim : (z : ZZ) -> negZ (negZ z) = z
112+doubleNegElim : (z : ZZ) -> negate (negate z) = z
104doubleNegElim (Pos Z) = Refl
113doubleNegElim (Pos Z) = Refl
105doubleNegElim (Pos (S n)) = Refl
114doubleNegElim (Pos (S n)) = Refl
106doubleNegElim (NegS Z) = Refl
115doubleNegElim (NegS Z) = Refl
libs/base/Language/Reflection.idr+11−9
@@ -79,20 +79,22 @@ reflectConstant = toConst
79
79
80
80
81||| Types of named references
81||| Types of named references
82−data NameType = Bound
82+data NameType =
83− -- ^ reference which is just bound, e.g. by intro
83+ ||| A reference which is just bound, e.g. by intro
84− | Ref
84+ Bound |
85− -- ^ reference to a variable
85+ ||| A reference to a de Bruijn-indexed variable
86+ Ref |
87+ ||| Data constructor with tag and number
86− | DCon Int Int
88+ DCon Int Int |
87− -- ^ constructor with tag and number
89+ ||| Type constructor with tag and number
88− | TCon Int Int
90+ TCon Int Int
89− -- ^ type constructor with tag and number
91+
90%name NameType nt, nt'
92%name NameType nt, nt'
91
93
92||| Types annotations for bound variables in different
94||| Types annotations for bound variables in different
93||| binding contexts
95||| binding contexts
94data Binder a = Lam a
96data Binder a = Lam a
95− | Pi a a
97+ | Pi a a
96 | Let a a
98 | Let a a
97 | NLet a a
99 | NLet a a
98 | Hole a
100 | Hole a
libs/base/Network/Socket.idr+51−37
@@ -4,8 +4,8 @@
4module IdrisNet.Socket
4module IdrisNet.Socket
5
5
6%include C "idris_net.h"
6%include C "idris_net.h"
7−%include C "sys/types.h"
7+%include C "sys/types.h"
8−%include C "sys/socket.h"
8+%include C "sys/socket.h"
9%include C "netdb.h"
9%include C "netdb.h"
10
10
11%access public
11%access public
@@ -16,12 +16,17 @@ ByteLength = Int
16class ToCode a where
16class ToCode a where
17 toCode : a -> Int
17 toCode : a -> Int
18
18
19−-- Socket Families.
19+||| Socket Families
20+|||
20−-- The ones that people might actually use. We're not going to need US Government
21+||| The ones that people might actually use. We're not going to need US
21−-- proprietary ones...
22+||| Government proprietary ones.
22−data SocketFamily = AF_UNSPEC -- Unspecified
23+data SocketFamily =
24+ ||| Unspecified
25+ AF_UNSPEC |
26+ ||| IP / UDP etc. IPv4
23− | AF_INET -- IP / UDP etc. IPv4
27+ AF_INET |
28+ ||| IP / UDP etc. IPv6
24− | AF_INET6 -- IP / UDP etc. IPv6
29+ AF_INET6
25
30
26instance Show SocketFamily where
31instance Show SocketFamily where
27 show AF_UNSPEC = "AF_UNSPEC"
32 show AF_UNSPEC = "AF_UNSPEC"
@@ -36,11 +41,16 @@ instance ToCode SocketFamily where
36getSocketFamily : Int -> Maybe SocketFamily
41getSocketFamily : Int -> Maybe SocketFamily
37getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
42getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
38
43
39−-- Socket Types.
44+||| Socket Types.
45+data SocketType =
40−data SocketType = NotASocket -- Not a socket, used in certain operations
46+ ||| Not a socket, used in certain operations
47+ NotASocket |
41− | Stream -- TCP
48+ ||| TCP
49+ Stream |
42− | Datagram -- UDP
50+ ||| UDP
51+ Datagram |
43− | RawSocket -- Raw sockets. A guy can dream.
52+ ||| Raw sockets
53+ RawSocket
44
54
45instance Show SocketType where
55instance Show SocketType where
46 show NotASocket = "Not a socket"
56 show NotASocket = "Not a socket"
@@ -60,15 +70,17 @@ data RecvfromStructPtr = RFPtr Ptr
60data BufPtr = BPtr Ptr
70data BufPtr = BPtr Ptr
61data SockaddrPtr = SAPtr Ptr
71data SockaddrPtr = SAPtr Ptr
62
72
73+||| Protocol Number.
74+|||
63−-- Protocol Number. Generally good enough to just set it to 0.
75+||| Generally good enough to just set it to 0.
64ProtocolNumber : Type
76ProtocolNumber : Type
65ProtocolNumber = Int
77ProtocolNumber = Int
66
78
67−-- SocketError: Error thrown by a socket operation
79+||| SocketError: Error thrown by a socket operation
68SocketError : Type
80SocketError : Type
69SocketError = Int
81SocketError = Int
70
82
71−-- SocketDescriptor: Native C Socket Descriptor
83+||| SocketDescriptor: Native C Socket Descriptor
72SocketDescriptor : Type
84SocketDescriptor : Type
73SocketDescriptor = Int
85SocketDescriptor = Int
74
86
@@ -86,7 +98,7 @@ instance Show SocketAddress where
86Port : Type
98Port : Type
87Port = Int
99Port = Int
88
100
89−-- Backlog used within listen() call -- number of incoming calls
101+||| Backlog used within listen() call -- number of incoming calls
90BACKLOG : Int
102BACKLOG : Int
91BACKLOG = 20
103BACKLOG = 20
92
104
@@ -109,7 +121,7 @@ record UDPAddrInfo : Type where
109 (remote_port : Port) ->
121 (remote_port : Port) ->
110 UDPAddrInfo
122 UDPAddrInfo
111
123
112−-- Frees a given pointer
124+||| Frees a given pointer
113public
125public
114sock_free : BufPtr -> IO ()
126sock_free : BufPtr -> IO ()
115sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
127sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
@@ -118,12 +130,14 @@ public
118sockaddr_free : SockaddrPtr -> IO ()
130sockaddr_free : SockaddrPtr -> IO ()
119sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
131sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
120
132
121−-- Allocates an amount of memory given by the ByteLength parameter.
133+||| Allocates an amount of memory given by the ByteLength parameter.
134+|||
122−-- Used to allocate a mutable pointer to be given to the Recv functions.
135+||| Used to allocate a mutable pointer to be given to the Recv functions.
123public
136public
124sock_alloc : ByteLength -> IO BufPtr
137sock_alloc : ByteLength -> IO BufPtr
125sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
138sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
126
139
140+||| The metadata about a socket
127record Socket : Type where
141record Socket : Type where
128 MkSocket : (descriptor : SocketDescriptor) ->
142 MkSocket : (descriptor : SocketDescriptor) ->
129 (family : SocketFamily) ->
143 (family : SocketFamily) ->
@@ -131,20 +145,21 @@ record Socket : Type where
131 (protocolNumber : ProtocolNumber) ->
145 (protocolNumber : ProtocolNumber) ->
132 Socket
146 Socket
133
147
148+||| Get the C error number
134getErrno : IO Int
149getErrno : IO Int
135getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
150getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
136
151
137−-- Creates a UNIX socket with the given family, socket type and protocol number.
152+||| Creates a UNIX socket with the given family, socket type and protocol
138−-- Returns either a socket or an error.
153+||| number. Returns either a socket or an error.
139socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
154socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
140socket sf st pn = do
155socket sf st pn = do
141 socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
156 socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
142 if socket_res == -1 then -- error
157 if socket_res == -1 then -- error
143 map Left getErrno
158 map Left getErrno
144− else
159+ else
145 return $ Right (MkSocket socket_res sf st pn)
160 return $ Right (MkSocket socket_res sf st pn)
146
161
147−
162+||| Close a socket
148close : Socket -> IO ()
163close : Socket -> IO ()
149close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
164close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
150
165
@@ -153,18 +168,18 @@ saString : (Maybe SocketAddress) -> String
153saString (Just sa) = show sa
168saString (Just sa) = show sa
154saString Nothing = ""
169saString Nothing = ""
155
170
156−-- Binds a socket to the given socket address and port.
171+||| Binds a socket to the given socket address and port.
157−-- Returns 0 on success, an error code otherwise.
172+||| Returns 0 on success, an error code otherwise.
158bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
173bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
159bind sock addr port = do
174bind 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)
161 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)
176 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)
162 if bind_res == (-1) then -- error
177 if bind_res == (-1) then -- error
163 getErrno
178 getErrno
164 else return 0 -- Success
179 else return 0 -- Success
165
180
166−-- Connects to a given address and port.
181+||| Connects to a given address and port.
167−-- Returns 0 on success, and an error number on error.
182+||| Returns 0 on success, and an error number on error.
168connect : Socket -> SocketAddress -> Port -> IO Int
183connect : Socket -> SocketAddress -> Port -> IO Int
169connect sock addr port = do
184connect sock addr port = do
170 conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
185 conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
@@ -173,7 +188,7 @@ connect sock addr port = do
173 getErrno
188 getErrno
174 else return 0
189 else return 0
175
190
176−-- Listens on a bound socket.
191+||| Listens on a bound socket.
177listen : Socket -> IO Int
192listen : Socket -> IO Int
178listen sock = do
193listen sock = do
179 listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
194 listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
@@ -181,7 +196,7 @@ listen sock = do
181 getErrno
196 getErrno
182 else return 0
197 else return 0
183
198
184−-- Parses a textual representation of an IPv4 address into a SocketAddress
199+||| Parses a textual representation of an IPv4 address into a SocketAddress
185parseIPv4 : String -> SocketAddress
200parseIPv4 : String -> SocketAddress
186parseIPv4 str = case splitted of
201parseIPv4 str = case splitted of
187 (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
202 (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
@@ -194,7 +209,7 @@ parseIPv4 str = case splitted of
194 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
209 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
195
210
196
211
197−-- Retrieves a socket address from a sockaddr pointer
212+||| Retrieves a socket address from a sockaddr pointer
198getSockAddr : SockaddrPtr -> IO SocketAddress
213getSockAddr : SockaddrPtr -> IO SocketAddress
199getSockAddr (SAPtr ptr) = do
214getSockAddr (SAPtr ptr) = do
200 addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
215 addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
@@ -256,13 +271,13 @@ recv sock len = do
256 return $ Right (payload, recv_res)
271 return $ Right (payload, recv_res)
257
272
258
273
259−-- Sends the data in a given memory location
274+||| Sends the data in a given memory location
260sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
275sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
261sendBuf sock (BPtr ptr) len = do
276sendBuf sock (BPtr ptr) len = do
262 send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
277 send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
263 if send_res == (-1) then
278 if send_res == (-1) then
264 map Left getErrno
279 map Left getErrno
265− else
280+ else
266 return $ Right send_res
281 return $ Right send_res
267
282
268recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
283recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
@@ -313,7 +328,7 @@ recvFrom sock bl = do
313 recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)
328 recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)
314 (descriptor sock) bl
329 (descriptor sock) bl
315 let recv_ptr' = RFPtr recv_ptr
330 let recv_ptr' = RFPtr recv_ptr
316− if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
331+ if !(nullPtr recv_ptr) then
317 map Left getErrno
332 map Left getErrno
318 else do
333 else do
319 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
334 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
@@ -332,7 +347,7 @@ recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrI
332recvFromBuf sock (BPtr ptr) bl = do
347recvFromBuf sock (BPtr ptr) bl = do
333 recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl
348 recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl
334 let recv_ptr' = RFPtr recv_ptr
349 let recv_ptr' = RFPtr recv_ptr
335− if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
350+ if !(nullPtr recv_ptr) then
336 map Left getErrno
351 map Left getErrno
337 else do
352 else do
338 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
353 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
@@ -345,5 +360,4 @@ recvFromBuf sock (BPtr ptr) bl = do
345 freeRecvfromStruct recv_ptr'
360 freeRecvfromStruct recv_ptr'
346 return $ Right (MkUDPAddrInfo addr port, result + 1)
361 return $ Right (MkUDPAddrInfo addr port, result + 1)
347
362
348−
349
363
libs/prelude/Builtins.idr+15−13
@@ -5,11 +5,10 @@
5
5
6||| The canonical single-element type, also known as the trivially
6||| The canonical single-element type, also known as the trivially
7||| true proposition.
7||| true proposition.
8−%elim
9− data Unit =
8+%elim data Unit =
10− ||| The trivial constructor for `()`.
9+ ||| The trivial constructor for `()`.
11− MkUnit
10+ MkUnit
12−
11+
13||| The non-dependent pair type, also known as conjunction.
12||| The non-dependent pair type, also known as conjunction.
14||| @A the type of the left elements in the pair
13||| @A the type of the left elements in the pair
15||| @B the type of the left elements in the pair
14||| @B the type of the left elements in the pair
@@ -18,10 +17,15 @@ data Pair : (A : Type) -> (B : Type) -> Type where
18 ||| @a the left element of the pair
17 ||| @a the left element of the pair
19 ||| @b the right element of the pair
18 ||| @b the right element of the pair
20 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
19 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
21−
20+
22−||| Dependent pairs, in their internal representation
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+|||
23−||| @ a the type of the witness
28+||| @ a the type of the witness @ P the type of the proof
24−||| @ P the type of the proof
25data Sigma : (a : Type) -> (P : a -> Type) -> Type where
29data Sigma : (a : Type) -> (P : a -> Type) -> Type where
26 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
30 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
27
31
@@ -43,7 +47,6 @@ infix 5 ~=~
43(~=~) : (x : a) -> (y : b) -> Type
47(~=~) : (x : a) -> (y : b) -> Type
44(~=~) x y = (=) _ _ x y
48(~=~) x y = (=) _ _ x y
45
49
46−-- ------------------------------------------------------ [ For rewrite tactic ]
47||| Perform substitution in a term according to some equality.
50||| Perform substitution in a term according to some equality.
48|||
51|||
49||| This is used by the `rewrite` tactic and term.
52||| This is used by the `rewrite` tactic and term.
@@ -95,7 +98,7 @@ namespace Ownership
95 ||| A read-only version of a unique value
98 ||| A read-only version of a unique value
96 data Borrowed : UniqueType -> NullType where
99 data Borrowed : UniqueType -> NullType where
97 Read : {a : UniqueType} -> a -> Borrowed a
100 Read : {a : UniqueType} -> a -> Borrowed a
98−
101+
99 ||| Make a read-only version of a unique value, which can be passed to another
102 ||| Make a read-only version of a unique value, which can be passed to another
100 ||| function without the unique value being consumed.
103 ||| function without the unique value being consumed.
101 implicit
104 implicit
@@ -104,7 +107,7 @@ namespace Ownership
104
107
105par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type
108par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type
106 -- is better in any case?
109 -- is better in any case?
107−par (Delay x) = x
110+par (Delay x) = x
108
111
109malloc : Int -> a -> a
112malloc : Int -> a -> a
110malloc size x = x -- compiled specially
113malloc size x = x -- compiled specially
@@ -135,4 +138,3 @@ believe_me x = prim__believe_me _ _ x
135public %assert_total
138public %assert_total
136really_believe_me : a -> b
139really_believe_me : a -> b
137really_believe_me x = prim__believe_me _ _ x
140really_believe_me x = prim__believe_me _ _ x
138−
libs/prelude/Prelude.idr+8
@@ -494,6 +494,7 @@ getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
494
494
495---- some basic file handling
495---- some basic file handling
496
496
497+||| A file handle
497abstract
498abstract
498data File = FHandle Ptr
499data File = FHandle Ptr
499
500
@@ -592,6 +593,7 @@ partial
592do_feof : Ptr -> IO Int
593do_feof : Ptr -> IO Int
593do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
594do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
594
595
596+||| Check if a file handle has reached the end
595feof : File -> IO Bool
597feof : File -> IO Bool
596feof (FHandle h) = do eof <- do_feof h
598feof (FHandle h) = do eof <- do_feof h
597 return (not (eof == 0))
599 return (not (eof == 0))
@@ -608,6 +610,7 @@ fpoll : File -> IO Bool
608fpoll (FHandle h) = do p <- mkForeign (FFun "fpoll" [FPtr] FInt) h
610fpoll (FHandle h) = do p <- mkForeign (FFun "fpoll" [FPtr] FInt) h
609 return (p > 0)
611 return (p > 0)
610
612
613+||| Check if a foreign pointer is null
611partial
614partial
612nullPtr : Ptr -> IO Bool
615nullPtr : Ptr -> IO Bool
613nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
616nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
@@ -630,6 +633,10 @@ validFile : File -> IO Bool
630validFile (FHandle h) = do x <- nullPtr h
633validFile (FHandle h) = do x <- nullPtr h
631 return (not x)
634 return (not x)
632
635
636+||| Loop while some test is true
637+|||
638+||| @ test the condition of the loop
639+||| @ body the loop body
633partial -- obviously
640partial -- obviously
634while : (test : IO Bool) -> (body : IO ()) -> IO ()
641while : (test : IO Bool) -> (body : IO ()) -> IO ()
635while t b = do v <- t
642while t b = do v <- t
@@ -637,6 +644,7 @@ while t b = do v <- t
637 while t b
644 while t b
638 else return ()
645 else return ()
639
646
647+||| Read the contents of a file into a string
640partial -- no error checking!
648partial -- no error checking!
641readFile : String -> IO String
649readFile : String -> IO String
642readFile fn = do h <- openFile fn Read
650readFile fn = do h <- openFile fn Read
src/Idris/AbsSyntaxTree.hs+2−2
@@ -1020,14 +1020,14 @@ data SyntaxInfo = Syn { using :: [Using],
1020 maxline :: Maybe Int,
1020 maxline :: Maybe Int,
1021 mut_nesting :: Int,
1021 mut_nesting :: Int,
1022 dsl_info :: DSL,
1022 dsl_info :: DSL,
1023− syn_in_quasiquote :: Bool }
1023+ syn_in_quasiquote :: Int }
1024 deriving Show
1024 deriving Show
1025{-!
1025{-!
1026deriving instance NFData SyntaxInfo
1026deriving instance NFData SyntaxInfo
1027deriving instance Binary SyntaxInfo
1027deriving instance Binary SyntaxInfo
1028!-}
1028!-}
1029
1029
1030−defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL False
1030+defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1031
1031
1032expandNS :: SyntaxInfo -> Name -> Name
1032expandNS :: SyntaxInfo -> Name -> Name
1033expandNS syn n@(NS _ _) = n
1033expandNS syn n@(NS _ _) = n
src/Idris/Docs.hs+3−3
@@ -15,7 +15,9 @@ import Data.List
15import qualified Data.Text as T
15import qualified Data.Text as T
16
16
17-- TODO: Only include names with public/abstract accessibility
17-- 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
19data FunDoc = FD Name (Docstring (Maybe Term))
21data FunDoc = FD Name (Docstring (Maybe Term))
20 [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))] -- args: name, ty, implicit, docs
22 [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))] -- args: name, ty, implicit, docs
21 PTerm -- function type
23 PTerm -- function type
@@ -203,5 +205,3 @@ pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "ty
203 t (Str _) = PConstant StrType
205 t (Str _) = PConstant StrType
204 t (Ch c) = PConstant $ AType (ATInt ITChar)
206 t (Ch c) = PConstant $ AType (ATInt ITChar)
205 t _ = PType
207 t _ = PType
206−
207−
src/Idris/ElabQuasiquote.hs+125−122
@@ -5,167 +5,170 @@ import Idris.Core.TT
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6
6
7
7
8−extract1 :: (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
8+extract1 :: Int -> (PTerm -> a) -> PTerm -> Elab' aux (a, [(Name, PTerm)])
9−extract1 c tm = do (tm', ex) <- extractUnquotes tm
9+extract1 n c tm = do (tm', ex) <- extractUnquotes n tm
10− return (c tm', ex)
10+ return (c tm', ex)
11
11
12−extract2 :: (PTerm -> PTerm -> a) -> PTerm -> PTerm -> Elab' aux (a, [(Name, PTerm)])
12+extract2 :: Int -> (PTerm -> PTerm -> a) -> PTerm -> PTerm -> Elab' aux (a, [(Name, PTerm)])
13−extract2 c a b = do (a', ex1) <- extractUnquotes a
13+extract2 n c a b = do (a', ex1) <- extractUnquotes n a
14− (b', ex2) <- extractUnquotes b
14+ (b', ex2) <- extractUnquotes n b
15− return (c a' b', ex1 ++ ex2)
15+ return (c a' b', ex1 ++ ex2)
16
16
17−extractTUnquotes :: PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
17+extractTUnquotes :: Int -> PTactic -> Elab' aux (PTactic, [(Name, PTerm)])
18−extractTUnquotes (Rewrite t) = extract1 Rewrite t
18+extractTUnquotes n (Rewrite t) = extract1 n Rewrite t
19−extractTUnquotes (Induction t) = extract1 Induction t
19+extractTUnquotes n (Induction t) = extract1 n Induction t
20−extractTUnquotes (LetTac n t) = extract1 (LetTac n) t
20+extractTUnquotes n (LetTac name t) = extract1 n (LetTac name) t
21−extractTUnquotes (LetTacTy n t1 t2) = extract2 (LetTacTy n) t1 t2
21+extractTUnquotes n (LetTacTy name t1 t2) = extract2 n (LetTacTy name) t1 t2
22−extractTUnquotes (Exact tm) = extract1 Exact tm
22+extractTUnquotes n (Exact tm) = extract1 n Exact tm
23−extractTUnquotes (Try tac1 tac2)
23+extractTUnquotes n (Try tac1 tac2)
24− = do (tac1', ex1) <- extractTUnquotes tac1
24+ = do (tac1', ex1) <- extractTUnquotes n tac1
25− (tac2', ex2) <- extractTUnquotes tac2
25+ (tac2', ex2) <- extractTUnquotes n tac2
26 return (Try tac1' tac2', ex1 ++ ex2)
26 return (Try tac1' tac2', ex1 ++ ex2)
27−extractTUnquotes (TSeq tac1 tac2)
27+extractTUnquotes n (TSeq tac1 tac2)
28− = do (tac1', ex1) <- extractTUnquotes tac1
28+ = do (tac1', ex1) <- extractTUnquotes n tac1
29− (tac2', ex2) <- extractTUnquotes tac2
29+ (tac2', ex2) <- extractTUnquotes n tac2
30 return (TSeq tac1' tac2', ex1 ++ ex2)
30 return (TSeq tac1' tac2', ex1 ++ ex2)
31−extractTUnquotes (ApplyTactic t) = extract1 ApplyTactic t
31+extractTUnquotes n (ApplyTactic t) = extract1 n ApplyTactic t
32−extractTUnquotes (ByReflection t) = extract1 ByReflection t
32+extractTUnquotes n (ByReflection t) = extract1 n ByReflection t
33−extractTUnquotes (Reflect t) = extract1 Reflect t
33+extractTUnquotes n (Reflect t) = extract1 n Reflect t
34−extractTUnquotes (GoalType s tac)
34+extractTUnquotes n (GoalType s tac)
35− = do (tac', ex) <- extractTUnquotes tac
35+ = do (tac', ex) <- extractTUnquotes n tac
36 return (GoalType s tac', ex)
36 return (GoalType s tac', ex)
37−extractTUnquotes (TCheck t) = extract1 TCheck t
37+extractTUnquotes n (TCheck t) = extract1 n TCheck t
38−extractTUnquotes (TEval t) = extract1 TEval t
38+extractTUnquotes n (TEval t) = extract1 n TEval t
39−extractTUnquotes tac = return (tac, []) -- the rest don't contain PTerms
39+extractTUnquotes n tac = return (tac, []) -- the rest don't contain PTerms
40
40
41−extractPArgUnquotes :: PArg -> Elab' aux (PArg, [(Name, PTerm)])
41+extractPArgUnquotes :: Int -> PArg -> Elab' aux (PArg, [(Name, PTerm)])
42−extractPArgUnquotes (PImp p m opts n t) =
42+extractPArgUnquotes d (PImp p m opts n t) =
43− do (t', ex) <- extractUnquotes t
43+ do (t', ex) <- extractUnquotes d t
44 return (PImp p m opts n t', ex)
44 return (PImp p m opts n t', ex)
45−extractPArgUnquotes (PExp p opts n t) =
45+extractPArgUnquotes d (PExp p opts n t) =
46− do (t', ex) <- extractUnquotes t
46+ do (t', ex) <- extractUnquotes d t
47 return (PExp p opts n t', ex)
47 return (PExp p opts n t', ex)
48−extractPArgUnquotes (PConstraint p opts n t) =
48+extractPArgUnquotes d (PConstraint p opts n t) =
49− do (t', ex) <- extractUnquotes t
49+ do (t', ex) <- extractUnquotes d t
50 return (PConstraint p opts n t', ex)
50 return (PConstraint p opts n t', ex)
51−extractPArgUnquotes (PTacImplicit p opts n scpt t) =
51+extractPArgUnquotes d (PTacImplicit p opts n scpt t) =
52− do (scpt', ex1) <- extractUnquotes scpt
52+ do (scpt', ex1) <- extractUnquotes d scpt
53− (t', ex2) <- extractUnquotes t
53+ (t', ex2) <- extractUnquotes d t
54 return (PTacImplicit p opts n scpt' t', ex1 ++ ex2)
54 return (PTacImplicit p opts n scpt' t', ex1 ++ ex2)
55
55
56−extractDoUnquotes :: PDo -> Elab' aux (PDo, [(Name, PTerm)])
56+extractDoUnquotes :: Int -> PDo -> Elab' aux (PDo, [(Name, PTerm)])
57−extractDoUnquotes (DoExp fc tm)
57+extractDoUnquotes d (DoExp fc tm)
58− = do (tm', ex) <- extractUnquotes tm
58+ = do (tm', ex) <- extractUnquotes d tm
59 return (DoExp fc tm', ex)
59 return (DoExp fc tm', ex)
60−extractDoUnquotes (DoBind fc n tm)
60+extractDoUnquotes d (DoBind fc n tm)
61− = do (tm', ex) <- extractUnquotes tm
61+ = do (tm', ex) <- extractUnquotes d tm
62 return (DoBind fc n tm', ex)
62 return (DoBind fc n tm', ex)
63−extractDoUnquotes (DoBindP fc t t' alts)
63+extractDoUnquotes d (DoBindP fc t t' alts)
64 = fail "Pattern-matching binds cannot be quasiquoted"
64 = fail "Pattern-matching binds cannot be quasiquoted"
65−extractDoUnquotes (DoLet fc n v b)
65+extractDoUnquotes d (DoLet fc n v b)
66− = do (v', ex1) <- extractUnquotes v
66+ = do (v', ex1) <- extractUnquotes d v
67− (b', ex2) <- extractUnquotes b
67+ (b', ex2) <- extractUnquotes d b
68 return (DoLet fc n v' b', ex1 ++ ex2)
68 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"
70
70
71
71
72−extractUnquotes :: PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
72+extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
73−extractUnquotes (PLam n ty body)
73+extractUnquotes n (PLam name ty body)
74− = do (ty', ex1) <- extractUnquotes ty
74+ = do (ty', ex1) <- extractUnquotes n ty
75− (body', ex2) <- extractUnquotes body
75+ (body', ex2) <- extractUnquotes n body
76− return (PLam n ty' body', ex1 ++ ex2)
76+ return (PLam name ty' body', ex1 ++ ex2)
77−extractUnquotes (PPi plicity n ty body)
77+extractUnquotes n (PPi plicity name ty body)
78− = do (ty', ex1) <- extractUnquotes ty
78+ = do (ty', ex1) <- extractUnquotes n ty
79− (body', ex2) <- extractUnquotes body
79+ (body', ex2) <- extractUnquotes n body
80− return (PPi plicity n ty' body', ex1 ++ ex2)
80+ return (PPi plicity name ty' body', ex1 ++ ex2)
81−extractUnquotes (PLet n ty val body)
81+extractUnquotes n (PLet name ty val body)
82− = do (ty', ex1) <- extractUnquotes ty
82+ = do (ty', ex1) <- extractUnquotes n ty
83− (val', ex2) <- extractUnquotes val
83+ (val', ex2) <- extractUnquotes n val
84− (body', ex3) <- extractUnquotes body
84+ (body', ex3) <- extractUnquotes n body
85− return (PLet n ty' val' body', ex1 ++ ex2 ++ ex3)
85+ return (PLet name ty' val' body', ex1 ++ ex2 ++ ex3)
86−extractUnquotes (PTyped tm ty)
86+extractUnquotes n (PTyped tm ty)
87− = do (tm', ex1) <- extractUnquotes tm
87+ = do (tm', ex1) <- extractUnquotes n tm
88− (ty', ex2) <- extractUnquotes ty
88+ (ty', ex2) <- extractUnquotes n ty
89 return (PTyped tm' ty', ex1 ++ ex2)
89 return (PTyped tm' ty', ex1 ++ ex2)
90−extractUnquotes (PApp fc f args)
90+extractUnquotes n (PApp fc f args)
91− = do (f', ex1) <- extractUnquotes f
91+ = do (f', ex1) <- extractUnquotes n f
92− args' <- mapM extractPArgUnquotes args
92+ args' <- mapM (extractPArgUnquotes n) args
93 let (args'', exs) = unzip args'
93 let (args'', exs) = unzip args'
94 return (PApp fc f' args'', ex1 ++ concat exs)
94 return (PApp fc f' args'', ex1 ++ concat exs)
95−extractUnquotes (PAppBind fc f args)
95+extractUnquotes n (PAppBind fc f args)
96− = do (f', ex1) <- extractUnquotes f
96+ = do (f', ex1) <- extractUnquotes n f
97− args' <- mapM extractPArgUnquotes args
97+ args' <- mapM (extractPArgUnquotes n) args
98 let (args'', exs) = unzip args'
98 let (args'', exs) = unzip args'
99 return (PAppBind fc f' args'', ex1 ++ concat exs)
99 return (PAppBind fc f' args'', ex1 ++ concat exs)
100−extractUnquotes (PCase fc expr cases)
100+extractUnquotes n (PCase fc expr cases)
101− = do (expr', ex1) <- extractUnquotes expr
101+ = do (expr', ex1) <- extractUnquotes n expr
102 let (pats, rhss) = unzip cases
102 let (pats, rhss) = unzip cases
103− (pats', exs1) <- fmap unzip $ mapM extractUnquotes pats
103+ (pats', exs1) <- fmap unzip $ mapM (extractUnquotes n) pats
104− (rhss', exs2) <- fmap unzip $ mapM extractUnquotes rhss
104+ (rhss', exs2) <- fmap unzip $ mapM (extractUnquotes n) rhss
105 return (PCase fc expr' (zip pats' rhss'), ex1 ++ concat exs1 ++ concat exs2)
105 return (PCase fc expr' (zip pats' rhss'), ex1 ++ concat exs1 ++ concat exs2)
106−extractUnquotes (PRefl fc x)
106+extractUnquotes n (PRefl fc x)
107− = do (x', ex) <- extractUnquotes x
107+ = do (x', ex) <- extractUnquotes n x
108 return (PRefl fc x', ex)
108 return (PRefl fc x', ex)
109−extractUnquotes (PEq fc at bt a b)
109+extractUnquotes n (PEq fc at bt a b)
110− = do (at', ex1) <- extractUnquotes at
110+ = do (at', ex1) <- extractUnquotes n at
111− (bt', ex2) <- extractUnquotes bt
111+ (bt', ex2) <- extractUnquotes n bt
112− (a', ex1) <- extractUnquotes a
112+ (a', ex1) <- extractUnquotes n a
113− (b', ex2) <- extractUnquotes b
113+ (b', ex2) <- extractUnquotes n b
114 return (PEq fc at' bt' a' b', ex1 ++ ex2)
114 return (PEq fc at' bt' a' b', ex1 ++ ex2)
115−extractUnquotes (PRewrite fc x y z)
115+extractUnquotes n (PRewrite fc x y z)
116− = do (x', ex1) <- extractUnquotes x
116+ = do (x', ex1) <- extractUnquotes n x
117− (y', ex2) <- extractUnquotes y
117+ (y', ex2) <- extractUnquotes n y
118 case z of
118 case z of
119− Just zz -> do (z', ex3) <- extractUnquotes zz
119+ Just zz -> do (z', ex3) <- extractUnquotes n zz
120 return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)
120 return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)
121 Nothing -> return (PRewrite fc x' y' Nothing, ex1 ++ ex2)
121 Nothing -> return (PRewrite fc x' y' Nothing, ex1 ++ ex2)
122−extractUnquotes (PPair fc info l r)
122+extractUnquotes n (PPair fc info l r)
123− = do (l', ex1) <- extractUnquotes l
123+ = do (l', ex1) <- extractUnquotes n l
124− (r', ex2) <- extractUnquotes r
124+ (r', ex2) <- extractUnquotes n r
125 return (PPair fc info l' r', ex1 ++ ex2)
125 return (PPair fc info l' r', ex1 ++ ex2)
126−extractUnquotes (PDPair fc info a b c)
126+extractUnquotes n (PDPair fc info a b c)
127− = do (a', ex1) <- extractUnquotes a
127+ = do (a', ex1) <- extractUnquotes n a
128− (b', ex2) <- extractUnquotes b
128+ (b', ex2) <- extractUnquotes n b
129− (c', ex3) <- extractUnquotes c
129+ (c', ex3) <- extractUnquotes n c
130 return (PDPair fc info a' b' c', ex1 ++ ex2 ++ ex3)
130 return (PDPair fc info a' b' c', ex1 ++ ex2 ++ ex3)
131−extractUnquotes (PAlternative b alts)
131+extractUnquotes n (PAlternative b alts)
132− = do alts' <- mapM extractUnquotes alts
132+ = do alts' <- mapM (extractUnquotes n) alts
133 let (alts'', exs) = unzip alts'
133 let (alts'', exs) = unzip alts'
134 return (PAlternative b alts'', concat exs)
134 return (PAlternative b alts'', concat exs)
135−extractUnquotes (PHidden tm)
135+extractUnquotes n (PHidden tm)
136− = do (tm', ex) <- extractUnquotes tm
136+ = do (tm', ex) <- extractUnquotes n tm
137 return (PHidden tm', ex)
137 return (PHidden tm', ex)
138−extractUnquotes (PGoal fc a n b)
138+extractUnquotes n (PGoal fc a name b)
139− = do (a', ex1) <- extractUnquotes a
139+ = do (a', ex1) <- extractUnquotes n a
140− (b', ex2) <- extractUnquotes b
140+ (b', ex2) <- extractUnquotes n b
141− return (PGoal fc a' n b', ex1 ++ ex2)
141+ return (PGoal fc a' name b', ex1 ++ ex2)
142−extractUnquotes (PDoBlock steps)
142+extractUnquotes n (PDoBlock steps)
143− = do steps' <- mapM extractDoUnquotes steps
143+ = do steps' <- mapM (extractDoUnquotes n) steps
144 let (steps'', exs) = unzip steps'
144 let (steps'', exs) = unzip steps'
145 return (PDoBlock steps'', concat exs)
145 return (PDoBlock steps'', concat exs)
146−extractUnquotes (PIdiom fc tm)
146+extractUnquotes n (PIdiom fc tm)
147− = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes tm
147+ = fmap (\(tm', ex) -> (PIdiom fc tm', ex)) $ extractUnquotes n tm
148−extractUnquotes (PProof tacs)
148+extractUnquotes n (PProof tacs)
149− = do (tacs', exs) <- fmap unzip $ mapM extractTUnquotes tacs
149+ = do (tacs', exs) <- fmap unzip $ mapM (extractTUnquotes n) tacs
150 return (PProof tacs', concat exs)
150 return (PProof tacs', concat exs)
151−extractUnquotes (PTactics tacs)
151+extractUnquotes n (PTactics tacs)
152− = do (tacs', exs) <- fmap unzip $ mapM extractTUnquotes tacs
152+ = do (tacs', exs) <- fmap unzip $ mapM (extractTUnquotes n) tacs
153 return (PTactics tacs', concat exs)
153 return (PTactics tacs', concat exs)
154−extractUnquotes (PElabError err) = fail "Can't quasiquote an error"
154+extractUnquotes n (PElabError err) = fail "Can't quasiquote an error"
155−extractUnquotes (PCoerced tm)
155+extractUnquotes n (PCoerced tm)
156− = do (tm', ex) <- extractUnquotes tm
156+ = do (tm', ex) <- extractUnquotes n tm
157 return (PCoerced tm', ex)
157 return (PCoerced tm', ex)
158−extractUnquotes (PDisamb ns tm)
158+extractUnquotes n (PDisamb ns tm)
159− = do (tm', ex) <- extractUnquotes tm
159+ = do (tm', ex) <- extractUnquotes n tm
160 return (PDisamb ns tm', ex)
160 return (PDisamb ns tm', ex)
161−extractUnquotes (PUnifyLog tm)
161+extractUnquotes n (PUnifyLog tm)
162− = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes tm
162+ = fmap (\(tm', ex) -> (PUnifyLog tm', ex)) $ extractUnquotes n tm
163−extractUnquotes (PNoImplicits tm)
163+extractUnquotes n (PNoImplicits tm)
164− = fmap (\(tm', ex) -> (PNoImplicits tm', ex)) $ extractUnquotes tm
164+ = fmap (\(tm', ex) -> (PNoImplicits tm', ex)) $ extractUnquotes n tm
165−extractUnquotes (PQuasiquote _ _) = fail "Nested quasiquotes not supported"
165+extractUnquotes n (PQuasiquote tm goal)
166+ = fmap (\(tm', ex) -> (PQuasiquote tm' goal, ex)) $ extractUnquotes (n+1) tm
166−extractUnquotes (PUnquote tm) =
167+extractUnquotes n (PUnquote tm)
167− do n <- getNameFrom (sMN 0 "unquotation")
168+ | n == 0 = do n <- getNameFrom (sMN 0 "unquotation")
168− return (PRef (fileFC "(unquote)") n, [(n, tm)])
169+ return (PRef (fileFC "(unquote)") n, [(n, tm)])
170+ | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
169−extractUnquotes x = return (x, []) -- no subterms!
171+ extractUnquotes (n-1) tm
172+extractUnquotes n x = return (x, []) -- no subterms!
170
173
171
174
src/Idris/ElabTerm.hs+44−60
@@ -18,7 +18,7 @@ import Idris.Core.Typecheck (check, recheck)
18import Idris.ErrReverse (errReverse)
18import Idris.ErrReverse (errReverse)
19import Idris.ElabQuasiquote (extractUnquotes)
19import Idris.ElabQuasiquote (extractUnquotes)
20import Idris.Elab.Utils
20import Idris.Elab.Utils
21−import qualified Util.Pretty as U
21+import qualified Util.Pretty as U
22
22
23import Control.Applicative ((<$>))
23import Control.Applicative ((<$>))
24import Control.Monad
24import Control.Monad
@@ -76,9 +76,9 @@ build ist info emode opts fn tm
76 u <- getUnifyLog
76 u <- getUnifyLog
77 hs <- get_holes
77 hs <- get_holes
78
78
79− when (not pattern) $
79+ when (not pattern) $
80 traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++
80 traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++
81− "Remaining problems:\n" ++ qshow probs) $
81+ "Remaining problems:\n" ++ qshow probs) $
82 do unify_all; matchProblems True; unifyProblems
82 do unify_all; matchProblems True; unifyProblems
83
83
84 probs <- get_probs
84 probs <- get_probs
@@ -99,7 +99,7 @@ build ist info emode opts fn tm
99 else return (tm, ds, is)
99 else return (tm, ds, is)
100 where pattern = emode == ELHS
100 where pattern = emode == ELHS
101 tydecl = emode == ETyDecl
101 tydecl = emode == ETyDecl
102−
102+
103 mkPat = do hs <- get_holes
103 mkPat = do hs <- get_holes
104 tm <- get_term
104 tm <- get_term
105 case hs of
105 case hs of
@@ -197,14 +197,14 @@ elab ist info emode opts fn tm
197 -- ++ "\nholes " ++ show hs
197 -- ++ "\nholes " ++ show hs
198 -- ++ "\nproblems " ++ show ps
198 -- ++ "\nproblems " ++ show ps
199 -- ++ "\n-----------\n") $
199 -- ++ "\n-----------\n") $
200− --trace ("ELAB " ++ show t') $
200+ --trace ("ELAB " ++ show t') $
201 let fc = fileFC "Force"
201 let fc = fileFC "Force"
202 env <- get_env
202 env <- get_env
203 handleError (forceErr env)
203 handleError (forceErr env)
204 (elab' ina t')
204 (elab' ina t')
205 (elab' ina (PApp fc (PRef fc (sUN "Force"))
205 (elab' ina (PApp fc (PRef fc (sUN "Force"))
206 [pimp (sUN "t") Placeholder True,
206 [pimp (sUN "t") Placeholder True,
207− pimp (sUN "a") Placeholder True,
207+ pimp (sUN "a") Placeholder True,
208 pexp ct])) True
208 pexp ct])) True
209
209
210 forceErr env (CantUnify _ t t' _ _ _)
210 forceErr env (CantUnify _ t t' _ _ _)
@@ -240,9 +240,9 @@ elab ist info emode opts fn tm
240 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
240 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
241 elab' ina PType = do apply RType []; solve
241 elab' ina PType = do apply RType []; solve
242 elab' ina (PUniverse u) = do apply (RUType u) []; solve
242 elab' ina (PUniverse u) = do apply (RUType u) []; solve
243−-- elab' (_,_,inty) (PConstant c)
243+-- elab' (_,_,inty) (PConstant c)
244-- | constType c && pattern && not reflection && not inty
244-- | constType c && pattern && not reflection && not inty
245−-- = lift $ tfail (Msg "Typecase is not allowed")
245+-- = lift $ tfail (Msg "Typecase is not allowed")
246 elab' ina (PConstant c) = do apply (RConstant c) []; solve
246 elab' ina (PConstant c) = do apply (RConstant c) []; solve
247 elab' ina (PQuote r) = do fill r; solve
247 elab' ina (PQuote r) = do fill r; solve
248 elab' ina (PTrue fc _) =
248 elab' ina (PTrue fc _) =
@@ -338,7 +338,7 @@ elab ist info emode opts fn tm
338-- elab' (_, _, inty) (PRef fc f)
338-- elab' (_, _, inty) (PRef fc f)
339-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
339-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
340-- = lift $ tfail (Msg "Typecase is not allowed")
340-- = 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)
342 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq
342 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq
343 = do ctxt <- get_context
343 = do ctxt <- get_context
344 let defined = case lookupTy n ctxt of
344 let defined = case lookupTy n ctxt of
@@ -363,7 +363,7 @@ elab ist info emode opts fn tm
363 = do -- if n is a type constructor name, this makes no sense...
363 = do -- if n is a type constructor name, this makes no sense...
364 ctxt <- get_context
364 ctxt <- get_context
365 when (isTConName n ctxt) $
365 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")
367 checkPiGoal n
367 checkPiGoal n
368 attack; intro (Just n);
368 attack; intro (Just n);
369 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
369 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
@@ -373,7 +373,7 @@ elab ist info emode opts fn tm
373 -- if n is a type constructor name, this makes no sense...
373 -- if n is a type constructor name, this makes no sense...
374 ctxt <- get_context
374 ctxt <- get_context
375 when (isTConName n ctxt) $
375 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")
377 checkPiGoal n
377 checkPiGoal n
378 claim tyn RType
378 claim tyn RType
379 explicit tyn
379 explicit tyn
@@ -539,7 +539,7 @@ elab ist info emode opts fn tm
539 sortBy cmpArg (zip ns args)
539 sortBy cmpArg (zip ns args)
540 ulog <- getUnifyLog
540 ulog <- getUnifyLog
541 elabArgs ist (ina || not isinf, guarded, inty, qq)
541 elabArgs ist (ina || not isinf, guarded, inty, qq)
542− [] fc False f ns'
542+ [] fc False f ns'
543 (f == sUN "Force")
543 (f == sUN "Force")
544 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
544 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
545 solve
545 solve
@@ -558,7 +558,7 @@ elab ist info emode opts fn tm
558 else movelast n)
558 else movelast n)
559 (ivs' \\ ivs)
559 (ivs' \\ ivs)
560 where -- normal < alternatives < lambdas < rewrites < tactic < default tactic
560 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
562 -- the alternative resolved can help with typechecking the lambda
562 -- the alternative resolved can help with typechecking the lambda
563 -- or the rewrite. Rewrites/tactics need as much information
563 -- or the rewrite. Rewrites/tactics need as much information
564 -- as possible about the type.
564 -- as possible about the type.
@@ -568,7 +568,7 @@ elab ist info emode opts fn tm
568 | constraint x && not (constraint y) = LT
568 | constraint x && not (constraint y) = LT
569 | constraint y && not (constraint x) = GT
569 | constraint y && not (constraint x) = GT
570 | otherwise
570 | otherwise
571− = compare (conDepth 0 (getTm x) + priority x + alt x)
571+ = compare (conDepth 0 (getTm x) + priority x + alt x)
572 (conDepth 0 (getTm y) + priority y + alt y)
572 (conDepth 0 (getTm y) + priority y + alt y)
573 where alt t = case getTm t of
573 where alt t = case getTm t of
574 PAlternative False _ -> 5
574 PAlternative False _ -> 5
@@ -581,14 +581,14 @@ elab ist info emode opts fn tm
581
581
582 constraint (PConstraint _ _ _ _) = True
582 constraint (PConstraint _ _ _ _) = True
583 constraint _ = False
583 constraint _ = False
584−
584+
585 -- Score a point for every level where there is a non-constructor
585 -- Score a point for every level where there is a non-constructor
586 -- function (so higher score --> done later)
586 -- function (so higher score --> done later)
587 -- Only relevant when on lhs
587 -- Only relevant when on lhs
588 conDepth d t | not pattern = 0
588 conDepth d t | not pattern = 0
589 conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0
589 conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0
590 | otherwise = max (100 - d) 1
590 | otherwise = max (100 - d) 1
591− conDepth d (PApp _ f as)
591+ conDepth d (PApp _ f as)
592 = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))
592 = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))
593 conDepth d (PPatvar _ _) = 0
593 conDepth d (PPatvar _ _) = 0
594 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)
594 conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)
@@ -602,7 +602,7 @@ elab ist info emode opts fn tm
602 Nothing -> return ()
602 Nothing -> return ()
603 Just b ->
603 Just b ->
604 case unApply (binderTy b) of
604 case unApply (binderTy b) of
605− (P _ c _, args) ->
605+ (P _ c _, args) ->
606 case lookupCtxt c (idris_classes ist) of
606 case lookupCtxt c (idris_classes ist) of
607 [] -> return ()
607 [] -> return ()
608 _ -> -- type class, set as injective
608 _ -> -- type class, set as injective
@@ -615,7 +615,7 @@ elab ist info emode opts fn tm
615 probs <- get_probs
615 probs <- get_probs
616 traceWhen ulog (qshow probs) $ return ()
616 traceWhen ulog (qshow probs) $ return ()
617 _ -> return ()
617 _ -> return ()
618−
618+
619 setinjArg (P _ n _) = setinj n
619 setinjArg (P _ n _) = setinj n
620 setinjArg _ = return ()
620 setinjArg _ = return ()
621
621
@@ -634,7 +634,7 @@ elab ist info emode opts fn tm
634 solve
634 solve
635 elab' ina Placeholder = do (h : hs) <- get_holes
635 elab' ina Placeholder = do (h : hs) <- get_holes
636 movelast h
636 movelast h
637− elab' ina (PMetavar n) =
637+ elab' ina (PMetavar n) =
638 do ptm <- get_term
638 do ptm <- get_term
639 -- When building the metavar application, leave out the unique
639 -- When building the metavar application, leave out the unique
640 -- names which have been used elsewhere in the term, since we
640 -- names which have been used elsewhere in the term, since we
@@ -699,21 +699,6 @@ elab ist info emode opts fn tm
699 args <- get_env
699 args <- get_env
700 envU <- mapM (getKind args) args
700 envU <- mapM (getKind args) args
701 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
701 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
717
702
718 -- Drop the unique arguments used in the scrutinee (since it's
703 -- Drop the unique arguments used in the scrutinee (since it's
719 -- not valid to use them again anyway)
704 -- not valid to use them again anyway)
@@ -724,7 +709,7 @@ elab ist info emode opts fn tm
724 let cname' = mkN cname
709 let cname' = mkN cname
725-- elab' ina (PMetavar cname')
710-- elab' ina (PMetavar cname')
726 attack; defer argsDropped cname'; solve
711 attack; defer argsDropped cname'; solve
727−
712+
728 -- if the scrutinee is one of the 'args' in env, we should
713 -- if the scrutinee is one of the 'args' in env, we should
729 -- inspect it directly, rather than adding it as a new argument
714 -- inspect it directly, rather than adding it as a new argument
730 let newdef = PClauses fc [] cname'
715 let newdef = PClauses fc [] cname'
@@ -748,10 +733,10 @@ elab ist info emode opts fn tm
748 Just u -> u
733 Just u -> u
749 _ -> False
734 _ -> False
750
735
751− getKind env (n, _)
736+ getKind env (n, _)
752 = case lookup n env of
737 = case lookup n env of
753 Nothing -> return (n, False) -- can't happen, actually...
738 Nothing -> return (n, False) -- can't happen, actually...
754− Just b ->
739+ Just b ->
755 do ty <- get_type (forget (binderTy b))
740 do ty <- get_type (forget (binderTy b))
756 case ty of
741 case ty of
757 UType UniqueType -> return (n, True)
742 UType UniqueType -> return (n, True)
@@ -764,8 +749,8 @@ elab ist info emode opts fn tm
764 _ -> False
749 _ -> False
765 tcName _ = False
750 tcName _ = False
766
751
767− usedIn ns (n, b)
752+ usedIn ns (n, b)
768− = n `elem` ns
753+ = n `elem` ns
769 || any (\x -> x `elem` ns) (allTTNames (binderTy b))
754 || any (\x -> x `elem` ns) (allTTNames (binderTy b))
770
755
771 -- FIXME: This probably doesn't help us here, but leaving
756 -- FIXME: This probably doesn't help us here, but leaving
@@ -791,7 +776,7 @@ elab ist info emode opts fn tm
791 = do -- First extract the unquoted subterms, replacing them with fresh
776 = do -- First extract the unquoted subterms, replacing them with fresh
792 -- names in the quasiquoted term. Claim their reflections to be
777 -- names in the quasiquoted term. Claim their reflections to be
793 -- of type TT.
778 -- of type TT.
794− (t, unq) <- extractUnquotes t
779+ (t, unq) <- extractUnquotes 0 t
795 let unquoteNames = map fst unq
780 let unquoteNames = map fst unq
796 mapM_ (flip claim (Var tt)) unquoteNames
781 mapM_ (flip claim (Var tt)) unquoteNames
797
782
@@ -872,7 +857,7 @@ elab ist info emode opts fn tm
872 isScr (PRef _ n) (n', b) = (n', (n == n', b))
857 isScr (PRef _ n) (n', b) = (n', (n == n', b))
873 isScr _ (n', b) = (n', (False, b))
858 isScr _ (n', b) = (n', (False, b))
874
859
875− caseBlock :: FC -> Name ->
860+ caseBlock :: FC -> Name ->
876 [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]
861 [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]
877 caseBlock fc n env opts
862 caseBlock fc n env opts
878 = let args' = findScr env
863 = let args' = findScr env
@@ -882,12 +867,12 @@ elab ist info emode opts fn tm
882 where -- Find the variable we want as the scrutinee and mark it as
867 where -- Find the variable we want as the scrutinee and mark it as
883 -- 'True'. If the scrutinee is in the environment, match on that
868 -- 'True'. If the scrutinee is in the environment, match on that
884 -- otherwise match on the new argument we're adding.
869 -- otherwise match on the new argument we're adding.
885− findScr ((n, (True, t)) : xs)
870+ findScr ((n, (True, t)) : xs)
886 = (n, (True, t)) : scrName n xs
871 = (n, (True, t)) : scrName n xs
887− findScr [(n, (_, t))] = [(n, (True, t))]
872+ findScr [(n, (_, t))] = [(n, (True, t))]
888 findScr (x : xs) = x : findScr xs
873 findScr (x : xs) = x : findScr xs
889 -- [] can't happen since scrutinee is in the environment!
874 -- [] can't happen since scrutinee is in the environment!
890−
875+
891 -- To make sure top level pattern name remains in scope, put
876 -- To make sure top level pattern name remains in scope, put
892 -- it at the end of the environment
877 -- it at the end of the environment
893 scrName n [] = []
878 scrName n [] = []
@@ -931,7 +916,7 @@ elab ist info emode opts fn tm
931 _ -> return t
916 _ -> return t
932 where
917 where
933 mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)
918 mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)
934− mkDelay env t
919+ mkDelay env t
935 = let fc = fileFC "Delay" in
920 = let fc = fileFC "Delay" in
936 addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))
921 addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))
937 [pexp t])
922 [pexp t])
@@ -998,10 +983,10 @@ elab ist info emode opts fn tm
998 failed' <- -- trace (show (n, t, hs, tm)) $
983 failed' <- -- trace (show (n, t, hs, tm)) $
999 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
984 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
1000 case holeName `elem` hs of
985 case holeName `elem` hs of
1001− True -> do focus holeName;
986+ True -> do focus holeName;
1002 g <- goal
987 g <- goal
1003 ulog <- getUnifyLog
988 ulog <- getUnifyLog
1004− traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
989+ traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
1005 elab ina t; return failed
990 elab ina t; return failed
1006 False -> return failed
991 False -> return failed
1007 done_elaborating_arg f argName
992 done_elaborating_arg f argName
@@ -1057,7 +1042,7 @@ pruneByType env t c as
1057 getName (PRef _ n) = Just n
1042 getName (PRef _ n) = Just n
1058 getName (PApp _ f _) = getName f
1043 getName (PApp _ f _) = getName f
1059 getName _ = Nothing
1044 getName _ = Nothing
1060−
1045+
1061pruneByType env (P _ n _) c as
1046pruneByType env (P _ n _) c as
1062-- if the goal type is polymorphic, keep e
1047-- if the goal type is polymorphic, keep e
1063 | [] <- lookupTy n c = as
1048 | [] <- lookupTy n c = as
@@ -1098,11 +1083,11 @@ trivial' ist
1098 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
1083 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
1099proofSearch' ist rec depth prv top n hints
1084proofSearch' ist rec depth prv top n hints
1100 = do unifyProblems
1085 = do unifyProblems
1101− proofSearch rec prv depth
1086+ proofSearch rec prv depth
1102 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
1087 (elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
1103
1088
1104resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()
1089resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()
1105−resolveTC = resTC' []
1090+resolveTC = resTC' []
1106
1091
1107resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"
1092resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"
1108resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True
1093resTC' 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
1112 ptm <- get_term
1097 ptm <- get_term
1113 ulog <- getUnifyLog
1098 ulog <- getUnifyLog
1114 hs <- get_holes
1099 hs <- get_holes
1115− traceWhen ulog ("Resolving class " ++ show g) $
1100+ traceWhen ulog ("Resolving class " ++ show g) $
1116 try' (trivial' ist)
1101 try' (trivial' ist)
1117 (do t <- goal
1102 (do t <- goal
1118 let (tc, ttypes) = unApply t
1103 let (tc, ttypes) = unApply t
@@ -1129,7 +1114,7 @@ resTC' tcs defaultOn depth topg fn ist
1129
1114
1130 -- HACK! Rather than giving a special name, better to have some kind
1115 -- HACK! Rather than giving a special name, better to have some kind
1131 -- of flag in ClassInfo structure
1116 -- of flag in ClassInfo structure
1132− chaser (UN nm)
1117+ chaser (UN nm)
1133 | ('@':'@':_) <- str nm = True -- old way
1118 | ('@':'@':_) <- str nm = True -- old way
1134 chaser (SN (ParentN _ _)) = True
1119 chaser (SN (ParentN _ _)) = True
1135 chaser (NS n _) = chaser n
1120 chaser (NS n _) = chaser n
@@ -1173,7 +1158,7 @@ resTC' tcs defaultOn depth topg fn ist
1173 args <- map snd <$> try' (apply (Var n) imps)
1158 args <- map snd <$> try' (apply (Var n) imps)
1174 (match_apply (Var n) imps) True
1159 (match_apply (Var n) imps) True
1175 ps' <- get_probs
1160 ps' <- get_probs
1176− when (length ps < length ps' || unrecoverable ps') $
1161+ when (length ps < length ps' || unrecoverable ps') $
1177 fail "Can't apply type class"
1162 fail "Can't apply type class"
1178-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
1163-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
1179 mapM_ (\ (_,n) -> do focus n
1164 mapM_ (\ (_,n) -> do focus n
@@ -1181,7 +1166,7 @@ resTC' tcs defaultOn depth topg fn ist
1181 let (tc', ttype) = unApply t'
1166 let (tc', ttype) = unApply t'
1182 let got = fst (unApply t)
1167 let got = fst (unApply t)
1183 let depth' = if tc' `elem` tcs
1168 let depth' = if tc' `elem` tcs
1184− then depth - 1 else depth
1169+ then depth - 1 else depth
1185 resTC' (got : tcs) defaultOn depth' topg fn ist)
1170 resTC' (got : tcs) defaultOn depth' topg fn ist)
1186 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
1171 (filter (\ (x, y) -> not x) (zip (map fst imps) args))
1187 -- if there's any arguments left, we've failed to resolve
1172 -- if there's any arguments left, we've failed to resolve
@@ -1232,11 +1217,11 @@ case_ ind autoSolve ist fn tm = do
1232-- if a tactic adds unification problems, return an error
1217-- if a tactic adds unification problems, return an error
1233
1218
1234runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()
1219runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()
1235−runTac autoSolve ist fn tac
1220+runTac autoSolve ist fn tac
1236 = do env <- get_env
1221 = do env <- get_env
1237 g <- goal
1222 g <- goal
1238 let tac' = fmap (addImplBound ist (map fst env)) tac
1223 let tac' = fmap (addImplBound ist (map fst env)) tac
1239− if autoSolve
1224+ if autoSolve
1240 then runT tac'
1225 then runT tac'
1241 else no_errors (runT tac')
1226 else no_errors (runT tac')
1242 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
1227 (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
@@ -1398,11 +1383,11 @@ runTac autoSolve ist fn tac
1398 letbind scriptvar scriptTy (Var script)
1383 letbind scriptvar scriptTy (Var script)
1399 focus script
1384 focus script
1400 ptm <- get_term
1385 ptm <- get_term
1401− elab ist toplevel ERHS [] (sMN 0 "tac")
1386+ elab ist toplevel ERHS [] (sMN 0 "tac")
1402 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
1387 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
1403 (script', _) <- get_type_val (Var scriptvar)
1388 (script', _) <- get_type_val (Var scriptvar)
1404 -- now that we have the script apply
1389 -- now that we have the script apply
1405− -- it to the reflected goal
1390+ -- it to the reflected goal
1406 restac <- getNameFrom (sMN 0 "restac")
1391 restac <- getNameFrom (sMN 0 "restac")
1407 claim restac tacticTy
1392 claim restac tacticTy
1408 focus restac
1393 focus restac
@@ -1482,7 +1467,7 @@ reify _ t = fail ("Unknown tactic " ++ show t)
1482
1467
1483reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
1468reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
1484reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
1469reifyApp 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)]
1486 | t == reflm "Search" = return (ProofSearch True True i Nothing [])
1471 | t == reflm "Search" = return (ProofSearch True True i Nothing [])
1487reifyApp _ t [x]
1472reifyApp _ t [x]
1488 | t == reflm "Refine" = do n <- reifyTTName x
1473 | t == reflm "Refine" = do n <- reifyTTName x
@@ -2223,4 +2208,3 @@ envTupleType
2223 ]
2208 ]
2224
2209
2225solveAll = try (do solve; solveAll) (return ())
2210solveAll = try (do solve; solveAll) (return ())
2226−
src/Idris/IBC.hs+1−1
@@ -1293,7 +1293,7 @@ instance Binary SyntaxInfo where
1293 x5 <- get
1293 x5 <- get
1294 x6 <- get
1294 x6 <- get
1295 x7 <- get
1295 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)
1297
1297
1298instance (Binary t) => Binary (PClause' t) where
1298instance (Binary t) => Binary (PClause' t) where
1299 put x
1299 put x
src/Idris/ParseExpr.hs+5−5
@@ -605,9 +605,9 @@ constraintArg syn = do symbol "@{"
605
605
606-}
606-}
607quasiquote :: SyntaxInfo -> IdrisParser PTerm
607quasiquote :: SyntaxInfo -> IdrisParser PTerm
608−quasiquote syn = do guard (not (syn_in_quasiquote syn))
608+quasiquote syn = do symbol "`("
609− symbol "`("
610− e <- expr syn { syn_in_quasiquote = True , inPattern = False}
609+ e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,
610+ inPattern = False }
611 g <- optional $ do
611 g <- optional $ do
612 symbol ":"
612 symbol ":"
613 expr syn { inPattern = False } -- don't allow antiquotes
613 expr syn { inPattern = False } -- don't allow antiquotes
@@ -621,9 +621,9 @@ quasiquote syn = do guard (not (syn_in_quasiquote syn))
621
621
622-}
622-}
623unquote :: SyntaxInfo -> IdrisParser PTerm
623unquote :: SyntaxInfo -> IdrisParser PTerm
624−unquote syn = do guard (syn_in_quasiquote syn)
624+unquote syn = do guard (syn_in_quasiquote syn > 0)
625 symbol "~"
625 symbol "~"
626− e <- simpleExpr syn { syn_in_quasiquote = False }
626+ e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }
627 return $ PUnquote e
627 return $ PUnquote e
628 <?> "unquotation"
628 <?> "unquotation"
629
629
src/Idris/Parser.hs+7−2
@@ -399,6 +399,9 @@ NameTimesList ::=
399@
399@
400-}
400-}
401-- FIXME: Check compatability for function options (i.e. partal/total)
401-- 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
402fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
405fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
403fnOpts opts
406fnOpts opts
404 = do reserved "total"; fnOpts (TotalFn : opts)
407 = do reserved "total"; fnOpts (TotalFn : opts)
@@ -914,7 +917,7 @@ clause syn
914
917
915{-| Parses with pattern
918{-| Parses with pattern
916
919
917−@
920+@
918WExpr ::= '|' Expr';
921WExpr ::= '|' Expr';
919@
922@
920-}
923-}
@@ -1161,6 +1164,8 @@ parseProg syn fname input mrk
1161 case runparser mainProg i fname input of
1164 case runparser mainProg i fname input of
1162 Failure doc -> do -- FIXME: Get error location from trifecta
1165 Failure doc -> do -- FIXME: Get error location from trifecta
1163 -- this can't be the solution!
1166 -- this can't be the solution!
1167+ -- Issue #1575 on the issue tracker.
1168+ -- https://github.com/idris-lang/Idris-dev/issues/1575
1164 let (fc, msg) = findFC doc
1169 let (fc, msg) = findFC doc
1165 i <- getIState
1170 i <- getIState
1166 case idris_outputmode i of
1171 case idris_outputmode i of
@@ -1272,7 +1277,7 @@ loadSource lidr f toline
1272 putIState (i { default_access = Hidden, module_aliases = modAliases })
1277 putIState (i { default_access = Hidden, module_aliases = modAliases })
1273 clearIBC -- start a new .ibc file
1278 clearIBC -- start a new .ibc file
1274 -- record package info in .ibc
1279 -- record package info in .ibc
1275− imps <- allImportDirs
1280+ imps <- allImportDirs
1276 mapM_ addIBC (map IBCImportDir imps)
1281 mapM_ addIBC (map IBCImportDir imps)
1277 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1282 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]
1278 let syntax = defaultSyntax{ syn_namespace = reverse mname,
1283 let syntax = defaultSyntax{ syn_namespace = reverse mname,
src/Idris/REPL.hs+11−6
@@ -727,7 +727,7 @@ process fn (NewDefn decls) = do
727 getClauseName (PClause fc name whole with rhs whereBlock) = name
727 getClauseName (PClause fc name whole with rhs whereBlock) = name
728 getClauseName (PWith fc name whole with rhs whereBlock) = name
728 getClauseName (PWith fc name whole with rhs whereBlock) = name
729 defineName :: [PDecl] -> Idris ()
729 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
731 elabDecl EAll recinfo tyDecl
731 elabDecl EAll recinfo tyDecl
732 elabClauses recinfo fc opts name (concatMap getClauses decls)
732 elabClauses recinfo fc opts name (concatMap getClauses decls)
733 setReplDefined (Just name)
733 setReplDefined (Just name)
@@ -767,7 +767,7 @@ process fn (NewDefn decls) = do
767 fixClauses :: PDecl' t -> PDecl' t
767 fixClauses :: PDecl' t -> PDecl' t
768 fixClauses (PClauses fc opts _ css@(clause:cs)) =
768 fixClauses (PClauses fc opts _ css@(clause:cs)) =
769 PClauses fc opts (getClauseName clause) css
769 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) =
771 PInstance syn fc constraints cls parms ty instName (map fixClauses decls)
771 PInstance syn fc constraints cls parms ty instName (map fixClauses decls)
772 fixClauses decl = decl
772 fixClauses decl = decl
773
773
@@ -777,10 +777,10 @@ process fn (Undefine names) = undefine names
777 undefine [] = do
777 undefine [] = do
778 allDefined <- idris_repl_defs `fmap` get
778 allDefined <- idris_repl_defs `fmap` get
779 undefine' allDefined []
779 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
781 -- print them out to the user afterward
781 -- print them out to the user afterward
782 undefine names = undefine' names []
782 undefine names = undefine' names []
783− undefine' [] list = do iRenderOutput $ printUndefinedNames list
783+ undefine' [] list = do iRenderOutput $ printUndefinedNames list
784 return ()
784 return ()
785 undefine' (n:names) already = do
785 undefine' (n:names) already = do
786 allDefined <- idris_repl_defs `fmap` get
786 allDefined <- idris_repl_defs `fmap` get
@@ -794,12 +794,12 @@ process fn (Undefine names) = undefine names
794 -- smart detection of exactly what kind of name we're undefining.
794 -- smart detection of exactly what kind of name we're undefining.
795 fputState (ctxt_lookup n . known_classes) Nothing
795 fputState (ctxt_lookup n . known_classes) Nothing
796 fmodifyState repl_definitions (delete n)
796 fmodifyState repl_definitions (delete n)
797− undefClosure n =
797+ undefClosure n =
798 do replDefs <- idris_repl_defs `fmap` get
798 do replDefs <- idris_repl_defs `fmap` get
799 callGraph <- whoCalls n
799 callGraph <- whoCalls n
800 let users = case lookup n callGraph of
800 let users = case lookup n callGraph of
801 Just ns -> nub ns
801 Just ns -> nub ns
802− Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)
802+ Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)
803 undefinedJustNow <- concat `fmap` mapM undefClosure users
803 undefinedJustNow <- concat `fmap` mapM undefClosure users
804 undefOne n
804 undefOne n
805 return (nub (n : undefinedJustNow))
805 return (nub (n : undefinedJustNow))
@@ -1361,6 +1361,8 @@ loadInputs inputs toline -- furthest line to read in input source files
1361 iWarn f $ pprintErr i e'
1361 iWarn f $ pprintErr i e'
1362 ProgramLineComment -> return () -- fail elsewhere
1362 ProgramLineComment -> return () -- fail elsewhere
1363 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1363 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
1364+ -- Issue #1576 on the issue tracker.
1365+ -- https://github.com/idris-lang/Idris-dev/issues/1576
1364 iWarn emptyFC $ pprintErr i e)
1366 iWarn emptyFC $ pprintErr i e)
1365 where -- load all files, stop if any fail
1367 where -- load all files, stop if any fail
1366 tryLoad :: Bool -> [IFileType] -> Idris ()
1368 tryLoad :: Bool -> [IFileType] -> Idris ()
@@ -1382,6 +1384,9 @@ loadInputs inputs toline -- furthest line to read in input source files
1382 inew <- getIState
1384 inew <- getIState
1383 -- FIXME: Save these in IBC to avoid this hack! Need to
1385 -- FIXME: Save these in IBC to avoid this hack! Need to
1384 -- preserve it all from source inputs
1386 -- preserve it all from source inputs
1387+ --
1388+ -- Issue #1577 on the issue tracker.
1389+ -- https://github.com/idris-lang/Idris-dev/issues/1577
1385 let tidata = idris_tyinfodata inew
1390 let tidata = idris_tyinfodata inew
1386 let patdefs = idris_patdefs inew
1391 let patdefs = idris_patdefs inew
1387 ok <- noErrors
1392 ok <- noErrors
src/Pkg/Package.hs+7−4
@@ -63,10 +63,10 @@ buildPkg warnonly (install, fp)
63 -- Also give up if there are metavariables to solve
63 -- Also give up if there are metavariables to solve
64 case (map fst (idris_metavars ist) \\ primDefs) of
64 case (map fst (idris_metavars ist) \\ primDefs) of
65 _ -> when install $ installPkg pkgdesc
65 _ -> when install $ installPkg pkgdesc
66−-- ms -> do if install
66+-- ms -> do if install
67-- then putStrLn "Can't install: there are undefined metavariables:"
67-- then putStrLn "Can't install: there are undefined metavariables:"
68-- else putStrLn "There are undefined metavariables:"
68-- else putStrLn "There are undefined metavariables:"
69−-- putStrLn $ "\t" ++ show ms
69+-- putStrLn $ "\t" ++ show ms
70-- exitWith (ExitFailure 1)
70-- exitWith (ExitFailure 1)
71
71
72-- | Type check packages only
72-- | Type check packages only
@@ -107,7 +107,7 @@ replPkg fp = do orig <- getIState
107 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
107 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc
108
108
109 if (f /= "")
109 if (f /= "")
110− then idrisMain ((Filename f) : opts)
110+ then idrisMain ((Filename f) : opts)
111 else iputStrLn "Can't start REPL: no main module given"
111 else iputStrLn "Can't start REPL: no main module given"
112 runIO $ setCurrentDirectory dir
112 runIO $ setCurrentDirectory dir
113
113
@@ -129,6 +129,9 @@ cleanPkg fp
129-- | Generate IdrisDoc for package
129-- | Generate IdrisDoc for package
130-- TODO: Handle case where module does not contain a matching namespace
130-- TODO: Handle case where module does not contain a matching namespace
131-- E.g. from prelude.ipkg: IO, Prelude.Chars, Builtins
131-- 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
132documentPkg :: FilePath -- ^ Path to .ipkg file.
135documentPkg :: FilePath -- ^ Path to .ipkg file.
133 -> IO ()
136 -> IO ()
134documentPkg fp =
137documentPkg fp =
@@ -143,7 +146,7 @@ documentPkg fp =
143 make (makefile pkgdesc)
146 make (makefile pkgdesc)
144 setCurrentDirectory $ pkgDir
147 setCurrentDirectory $ pkgDir
145 let run l = runErrorT . (execStateT l)
148 let run l = runErrorT . (execStateT l)
146− load [] = return ()
149+ load [] = return ()
147 load (f:fs) = do loadModule f; load fs
150 load (f:fs) = do loadModule f; load fs
148 loader = do idrisMain opts; load fs
151 loader = do idrisMain opts; load fs
149 idrisInstance <- run loader idrisInit
152 idrisInstance <- run loader idrisInit