git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of https://github.com/idris-lang/Idris-dev into fix/dsym-gitignore
commitb359c3f314a0b677cf1673a588c219b42fff79ea authorAhmad Salim Al-Sibahi <asal@itu.dk> dateMon 4 Apr 2016, 22:05 (11 years ago) parentff2033a5134aeb
10 files changed+85−14
compare with master
unifiedsplit
CHANGELOG.md+21 idris.cabal+3 libs/contrib/Network/Socket.idr+5−5 src/IRTS/CodegenC.hs+5−1 src/Idris/Coverage.hs+7−7 src/Idris/ElabDecls.hs+8−1 test/proof011/proof011a.idr+14 test/reg071/expected test/reg071/reg071.idr+19 test/reg071/run+3
CHANGELOG.md+21
@@ -2,8 +2,29 @@
22
33## Language updates
44
5+* `rewrite` can now be used to rewrite equalities on functions over
6+ dependent types
57* `rewrite` can now be given an optional rewriting lemma, with the syntax
68 `rewrite [rule] using [rewrite_lemma] in [scope]`.
9+* Experimental extended `with` syntax, which allows calling functions defined
10+ in a with block directly. For example:
11+
12+ ```
13+ data SnocList : List a -> Type where
14+ Empty : SnocList []
15+ Snoc : SnocList xs -> SnocList (xs ++ [x])
16+
17+ snocList : (xs : List a) -> SnocList a
18+
19+ my_reverse : List a -> List a
20+ my_reverse xs with (snocList xs)
21+ my_reverse [] | Empty = []
22+ my_reverse (ys ++ [x]) | (Snoc p) = x :: my_reverse ys | p
23+ ```
24+
25+ The `| p` on the right hand side means that the `with` block function will
26+ be called directly, so the recursive structure of `SnocList` can direct the
27+ recursion structure of `my_reverse`.
728
829## Miscellaneous updates
930
idris.cabal+3
@@ -325,6 +325,9 @@ Extra-source-files:
325325 test/reg070/run
326326 test/reg070/*.idr
327327 test/reg070/expected
328+ test/reg071/run
329+ test/reg071/*.idr
330+ test/reg071/expected
328331
329332 test/basic001/run
330333 test/basic001/*.idr
libs/contrib/Network/Socket.idr+5−5
@@ -1,7 +1,7 @@
1−-- Time to do this properly.
2−-- Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
3−-- (C) SimonJF, MIT Licensed, 2014
4−module IdrisNet.Socket
1+||| Time to do this properly.
2+||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
3+||| (C) SimonJF, MIT Licensed, 2014
4+module Network.Socket
55
66%include C "idris_net.h"
77%include C "sys/types.h"
@@ -140,7 +140,7 @@ record Socket where
140140 descriptor : SocketDescriptor
141141 family : SocketFamily
142142 socketType : SocketType
143− protocalNumber : ProtocolNumber
143+ protocolNumber : ProtocolNumber
144144
145145||| Creates a UNIX socket with the given family, socket type and protocol
146146||| number. Returns either a socket or an error.
src/IRTS/CodegenC.hs+5−1
@@ -730,7 +730,11 @@ ctype t = error "Can't happen: Not a valid interface type " ++ show t
730730carith (FCon i)
731731 | i == sUN "C_IntChar" = "char"
732732 | i == sUN "C_IntNative" = "int"
733−carith t = error "Can't happen: Not an exportable arithmetic type"
733+ | i == sUN "C_IntBits8" = "uint8_t"
734+ | i == sUN "C_IntBits16" = "uint16_t"
735+ | i == sUN "C_IntBits32" = "uint32_t"
736+ | i == sUN "C_IntBits64" = "uint64_t"
737+carith t = error $ "Can't happen: Not an exportable arithmetic type " ++ show t
734738
735739cdesc (FStr s) = s
736740cdesc s = error "Can't happen: Not a valid C name"
src/Idris/Coverage.hs+7−7
@@ -565,9 +565,9 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
565565 | otherwise = checkSize a ps (i + 1)
566566 checkSize a [] i = Nothing
567567
568− -- the smaller thing we find must be the same type as <a>, and
569− -- not be coinductive - so carry the type of the constructor we've
570− -- gone under.
568+ -- the smaller thing we find must be defined in the same group of mutally
569+ -- defined types as <a>, and not be coinductive - so carry the type of
570+ -- the constructor we've gone under.
571571
572572 smaller (Just tyn) a (t, Just tyt)
573573 | a == t = isInductive (fst (unApply (getRetTy tyn)))
@@ -587,10 +587,10 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
587587 Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
588588
589589 isInductive (P _ nty _) (P _ nty' _) =
590− let co = case lookupCtxt nty (idris_datatypes ist) of
591− [TI _ x _ _ _] -> x
592− _ -> False in
593− nty == nty' && not co
590+ let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of
591+ [TI _ x _ _ muts] -> (x, muts)
592+ _ -> (False, []) in
593+ (nty == nty' || any (== nty') muts) && not co
594594 isInductive _ _ = False
595595
596596 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
src/Idris/ElabDecls.hs+8−1
@@ -191,7 +191,7 @@ elabDecl' what info (PMutual f ps)
191191 _ -> do mapM_ (elabDecl ETypes info) ps
192192 mapM_ (elabDecl EDefns info) ps
193193 -- record mutually defined data definitions
194− let datans = concatMap declared (filter isDataDecl ps)
194+ let datans = concatMap declared (getDataDecls ps)
195195 mapM_ (setMutData datans) datans
196196 logElab 1 $ "Rechecking for positivity " ++ show datans
197197 mapM_ (\x -> do setTotality x Unchecked) datans
@@ -208,6 +208,13 @@ elabDecl' what info (PMutual f ps)
208208 where isDataDecl (PData _ _ _ _ _ _) = True
209209 isDataDecl _ = False
210210
211+ getDataDecls (PNamespace _ _ ds : decls)
212+ = getDataDecls ds ++ getDataDecls decls
213+ getDataDecls (d : decls)
214+ | isDataDecl d = d : getDataDecls decls
215+ | otherwise = getDataDecls decls
216+ getDataDecls [] = []
217+
211218 setMutData ns n
212219 = do i <- getIState
213220 case lookupCtxt n (idris_datatypes i) of
test/proof011/proof011a.idrnew file+14
@@ -0,0 +1,14 @@
1+import Data.Vect
2+
3+total
4+vassoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect p a) ->
5+ xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
6+vassoc [] ys zs = Refl
7+vassoc (x :: xs) ys zs
8+ = rewrite vassoc xs ys zs in Refl
9+total
10+vassoc' : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect p a) ->
11+ xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
12+vassoc' [] ys zs = Refl
13+vassoc' (x :: xs) ys zs
14+ = rewrite vassoc xs ys xs in Refl
test/reg071/expectednew file

No changes to the content.

test/reg071/reg071.idrnew file+19
@@ -0,0 +1,19 @@
1+mutual
2+ data Odd : Type where
3+ MkOdd : Even -> Odd
4+
5+ data Even : Type where
6+ MkEven : Odd -> Even
7+ EvenZ : Even
8+
9+mutual
10+ total
11+ countEven : Even -> Nat
12+ countEven (MkEven x) = countOdd x
13+ countEven EvenZ = Z
14+
15+ total
16+ countOdd : Odd -> Nat
17+ countOdd (MkOdd x) = S (countEven x)
18+
19+
test/reg071/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ reg071.idr --check
3+rm -f *.ibc