b359c3f · Idris-dev · git.iko.soy

CHANGELOG.md+21

compare with master

unifiedsplit

@@ -2,8 +2,29 @@

2

3## Language updates

4

5+* `rewrite` can now be used to rewrite equalities on functions over

6+ dependent types

5* `rewrite` can now be given an optional rewriting lemma, with the syntax

7* `rewrite` can now be given an optional rewriting lemma, with the syntax

6 `rewrite [rule] using [rewrite_lemma] in [scope]`.

8 `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`.

7

28

8## Miscellaneous updates

29## Miscellaneous updates

9

30

idris.cabal+3

@@ -325,6 +325,9 @@ Extra-source-files:

325 test/reg070/run

326 test/reg070/*.idr

327 test/reg070/expected

328+ test/reg071/run

329+ test/reg071/*.idr

330+ test/reg071/expected

328

331

329 test/basic001/run

332 test/basic001/run

330 test/basic001/*.idr

333 test/basic001/*.idr

libs/contrib/Network/Socket.idr+5−5

@@ -1,7 +1,7 @@

1−-- Time to do this properly.

1+||| Time to do this properly.

2−-- Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.

2+||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.

3−-- (C) SimonJF, MIT Licensed, 2014

3+||| (C) SimonJF, MIT Licensed, 2014

4−module IdrisNet.Socket

4+module Network.Socket

5

6%include C "idris_net.h"

7%include C "sys/types.h"

@@ -140,7 +140,7 @@ record Socket where

140 descriptor : SocketDescriptor

141 family : SocketFamily

142 socketType : SocketType

143− protocalNumber : ProtocolNumber

143+ protocolNumber : ProtocolNumber

144

145||| Creates a UNIX socket with the given family, socket type and protocol

146||| 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

730carith (FCon i)

731 | i == sUN "C_IntChar" = "char"

732 | i == sUN "C_IntNative" = "int"

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"

733−carith t = error "Can't happen: Not an exportable arithmetic type"

737+carith t = error $ "Can't happen: Not an exportable arithmetic type " ++ show t

734

738

735cdesc (FStr s) = s

739cdesc (FStr s) = s

736cdesc s = error "Can't happen: Not a valid C name"

740cdesc 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

565 | otherwise = checkSize a ps (i + 1)

566 checkSize a [] i = Nothing

567

568− -- the smaller thing we find must be the same type as <a>, and

568+ -- the smaller thing we find must be defined in the same group of mutally

569− -- not be coinductive - so carry the type of the constructor we've

569+ -- defined types as <a>, and not be coinductive - so carry the type of

570− -- gone under.

570+ -- the constructor we've gone under.

571

572 smaller (Just tyn) a (t, Just tyt)

573 | a == t = isInductive (fst (unApply (getRetTy tyn)))

@@ -587,10 +587,10 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

587 Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist

588

589 isInductive (P _ nty _) (P _ nty' _) =

590− let co = case lookupCtxt nty (idris_datatypes ist) of

590+ let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of

591− [TI _ x _ _ _] -> x

591+ [TI _ x _ _ muts] -> (x, muts)

592− _ -> False in

592+ _ -> (False, []) in

593− nty == nty' && not co

593+ (nty == nty' || any (== nty') muts) && not co

594 isInductive _ _ = False

595

596 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)

191 _ -> do mapM_ (elabDecl ETypes info) ps

192 mapM_ (elabDecl EDefns info) ps

193 -- record mutually defined data definitions

194− let datans = concatMap declared (filter isDataDecl ps)

194+ let datans = concatMap declared (getDataDecls ps)

195 mapM_ (setMutData datans) datans

196 logElab 1 $ "Rechecking for positivity " ++ show datans

197 mapM_ (\x -> do setTotality x Unchecked) datans

@@ -208,6 +208,13 @@ elabDecl' what info (PMutual f ps)

208 where isDataDecl (PData _ _ _ _ _ _) = True

209 isDataDecl _ = False

210

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+

211 setMutData ns n

218 setMutData ns n

212 = do i <- getIState

219 = do i <- getIState

213 case lookupCtxt n (idris_datatypes i) of

220 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