8f93b00 · Idris-dev · git.iko.soy

CHANGELOG+6−5

compare with master

unifiedsplit

@@ -4,12 +4,13 @@ New in 0.9.12:

4* Proof search now works for metavariables in types, giving some interactive

5 type inference.

6* New 'Lazy' type, replacing laziness annotations.

7−* JavaScript and Node codegen now understand the %include directive

7+* JavaScript and Node codegen now understand the %include directive.

8−* Concept up 'null' is now understood in the JavaScript and Node codegen

8+* Concept up 'null' is now understood in the JavaScript and Node codegen.

9−* Lots of performance patches for generated JavaScript

9+* Lots of performance patches for generated JavaScript.

10* New commands :eval (:e) and :type (:t) in the prover, which either normalise

11− or show the type of expressions

11+ or show the type of expressions.

12−* Allow type providers to return postulates in addition to terms

12+* Allow type providers to return postulates in addition to terms.

13+* Syntax for dealing with match failure in <- and pattern matching let.

13* New syntax for inline documentation. Documentation starts with |||, and

14* New syntax for inline documentation. Documentation starts with |||, and

14 arguments are documented by preceding their name with @. Example:

15 arguments are documented by preceding their name with @. Example:

15||| Add two natural numbers

16||| Add two natural numbers

Makefile+1−1

@@ -39,7 +39,7 @@ relib: lib_clean

39 $(CABAL) install $(CABALFLAGS)

40

41linecount:

42− wc -l src/Idris/*.hs src/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs

42+ wc -l src/Idris/*.hs src/Idris/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs

43

44#Note: this doesn't yet link to Hackage properly

45doc: dist/setup-config

src/Idris/AbsSyntaxTree.hs+2−2

@@ -737,7 +737,7 @@ type PTactic = PTactic' PTerm

737

738data PDo' t = DoExp FC t

739 | DoBind FC Name t

740− | DoBindP FC t t

740+ | DoBindP FC t t [(t,t)]

741 | DoLet FC Name t t

742 | DoLetP FC t t

743 deriving (Eq, Functor)

@@ -749,7 +749,7 @@ deriving instance NFData PDo'

749instance Sized a => Sized (PDo' a) where

750 size (DoExp fc t) = 1 + size fc + size t

751 size (DoBind fc nm t) = 1 + size fc + size nm + size t

752− size (DoBindP fc l r) = 1 + size fc + size l + size r

752+ size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts

753 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r

754 size (DoLetP fc l r) = 1 + size fc + size l + size r

755

src/Idris/DSL.hs+2−2

@@ -57,10 +57,10 @@ expandDo dsl (PDoBlock ds)

57 block b [a] = PElabError (Msg "Last statement in do block must be an expression")

58 block b (DoBind fc n tm : rest)

59 = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]

60− block b (DoBindP fc p tm : rest)

60+ block b (DoBindP fc p tm alts : rest)

61 = PApp fc b [pexp tm, pexp (PLam (sMN 0 "bpat") Placeholder

62 (PCase fc (PRef fc (sMN 0 "bpat"))

63− [(p, block b rest)]))]

63+ ((p, block b rest) : alts)))]

64 block b (DoLet fc n ty tm : rest)

65 = PLet n ty tm (block b rest)

66 block b (DoLetP fc p tm : rest)

src/Idris/DeepSeq.hs+1−1

@@ -226,7 +226,7 @@ instance (NFData t) => NFData (PTactic' t) where

226instance (NFData t) => NFData (PDo' t) where

227 rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

228 rnf (DoBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

229− rnf (DoBindP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

229+ rnf (DoBindP x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

230 rnf (DoLet x1 x2 x3 x4)

231 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

232 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

src/Idris/IBC.hs+8−6

@@ -25,7 +25,7 @@ import Codec.Compression.Zlib (compress)

25import Util.Zlib (decompressEither)

26

27ibcVersion :: Word8

28−ibcVersion = 62

28+ibcVersion = 63

29

30

31data IBCFile = IBCFile { ver :: Word8,

@@ -1878,10 +1878,11 @@ instance (Binary t) => Binary (PDo' t) where

1878 put x1

1879 put x2

1880 put x3

1881− DoBindP x1 x2 x3 -> do putWord8 2

1881+ DoBindP x1 x2 x3 x4 -> do putWord8 2

1882− put x1

1882+ put x1

1883− put x2

1883+ put x2

1884− put x3

1884+ put x3

1885+ put x4

1885 DoLet x1 x2 x3 x4 -> do putWord8 3

1886 DoLet x1 x2 x3 x4 -> do putWord8 3

1886 put x1

1887 put x1

1887 put x2

1888 put x2

@@ -1904,7 +1905,8 @@ instance (Binary t) => Binary (PDo' t) where

1904 2 -> do x1 <- get

1905 2 -> do x1 <- get

1905 x2 <- get

1906 x2 <- get

1906 x3 <- get

1907 x3 <- get

1908+ x4 <- get

1907− return (DoBindP x1 x2 x3)

1909+ return (DoBindP x1 x2 x3 x4)

1908 3 -> do x1 <- get

1910 3 -> do x1 <- get

1909 x2 <- get

1911 x2 <- get

1910 x3 <- get

1912 x3 <- get

src/Idris/ParseExpr.hs+25−6

@@ -167,7 +167,9 @@ extension syn (Rule ssym ptm _)

167 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds

168 upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)

169 : upd (dropn n ns) ds

170+ upd ns (DoBindP fc i t ts : ds)

170− upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)

171+ = DoBindP fc (update ns i) (update ns t)

172+ (map (\(l,r) -> (update ns l, update ns r)) ts)

171 : upd ns ds

173 : upd ns ds

172 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)

174 upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)

173 : upd ns ds

175 : upd ns ds

@@ -736,16 +738,22 @@ TypeSig' ::=

736@

738@

737 -}

739 -}

738let_ :: SyntaxInfo -> IdrisParser PTerm

740let_ :: SyntaxInfo -> IdrisParser PTerm

739−let_ syn = try (do reserved "let"; n <- name;

741+let_ syn = try (do reserved "let"; fc <- getFC; n <- name;

740 ty <- option Placeholder (do lchar ':'; expr' syn)

742 ty <- option Placeholder (do lchar ':'; expr' syn)

741 lchar '='

743 lchar '='

742 v <- expr syn

744 v <- expr syn

745+ ts <- option [] (do lchar '|'

746+ sepBy1 (do_alt syn) (lchar '|'))

743 reserved "in"; sc <- expr syn

747 reserved "in"; sc <- expr syn

748+ case ts of

744− return (PLet n ty v sc))

749+ [] -> return (PLet n ty v sc)

750+ alts -> return (PCase fc v ((PRef fc n, sc) : ts)))

745 <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )

751 <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )

746 symbol "="; v <- expr syn

752 symbol "="; v <- expr syn

753+ ts <- option [] (do lchar '|'

754+ sepBy1 (do_alt syn) (lchar '|'))

747 reserved "in"; sc <- expr syn

755 reserved "in"; sc <- expr syn

748− return (PCase fc v [(pat, sc)]))

756+ return (PCase fc v ((pat, sc) : ts)))

749 <?> "let binding"

757 <?> "let binding"

750

758

751{- | Parses a quote goal

759{- | Parses a quote goal

@@ -967,17 +975,28 @@ do_ syn

967 symbol "<-"

975 symbol "<-"

968 fc <- getFC

976 fc <- getFC

969 e <- expr syn;

977 e <- expr syn;

970− return (DoBind fc i e))

978+ option (DoBind fc i e)

979+ (do lchar '|'

980+ ts <- sepBy1 (do_alt syn) (lchar '|')

981+ return (DoBindP fc (PRef fc i) e ts)))

971 <|> try (do i <- expr' syn

982 <|> try (do i <- expr' syn

972 symbol "<-"

983 symbol "<-"

973 fc <- getFC

984 fc <- getFC

974 e <- expr syn;

985 e <- expr syn;

986+ option (DoBindP fc i e [])

987+ (do lchar '|'

988+ ts <- sepBy1 (do_alt syn) (lchar '|')

975− return (DoBindP fc i e))

989+ return (DoBindP fc i e ts)))

976 <|> do e <- expr syn

990 <|> do e <- expr syn

977 fc <- getFC

991 fc <- getFC

978 return (DoExp fc e)

992 return (DoExp fc e)

979 <?> "do block expression"

993 <?> "do block expression"

980

994

995+do_alt syn = do l <- expr' syn

996+ symbol "=>"

997+ r <- expr' syn

998+ return (l, r)

999+

981{- | Parses an expression in idiom brackets

1000{- | Parses an expression in idiom brackets

982@

1001@

983Idiom ::= '[|' Expr '|]';

1002Idiom ::= '[|' Expr '|]';

test/Makefile+3−3

@@ -8,13 +8,13 @@ test: $(TESTS)

8 @perl ./runtest.pl $(patsubst %.test,%,$@)

9

10test_java:

11− perl ./runtest.pl without buffer001 --codegen Java

11+ perl ./runtest.pl without sugar004 buffer001 --codegen Java

12

13test_js:

14− @perl ./runtest.pl without reg029 io001 dsl002 io003 effects001 effects002 buffer001 bounded001 --codegen node

14+ @perl ./runtest.pl without sugar004 reg029 io001 dsl002 io003 effects001 effects002 buffer001 bounded001 --codegen node

15

16test_llvm:

17− @perl ./runtest.pl without io003 buffer001 --codegen llvm

17+ @perl ./runtest.pl without sugar004 io003 buffer001 --codegen llvm

18

19update:

20 /usr/bin/env perl ./runtest.pl all -u

test/sugar004/expectednew file+3

@@ -0,0 +1,3 @@

1+No arguments!

2+42

3+Too many arguments!

test/sugar004/runnew file+6

@@ -0,0 +1,6 @@

1+#!/usr/bin/env bash

2+idris $@ sugar004.idr -o sugar004

3+./sugar004

4+./sugar004 42

5+./sugar004 42 100

6+rm -f sugar004 *.ibc

test/sugar004/sugar004.idrnew file+36

@@ -0,0 +1,36 @@

1+module Main

2+

3+import System

4+

5+total

6+foo : Maybe Int -> Int

7+foo x = let Just x' = x | Nothing => 100 in x'

8+

9+main : IO ()

10+main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!"

11+ | (x :: y :: _) => putStrLn "Too many arguments!"

12+ print (foo (Just (cast a)))

13+

14+{-

15+

16+let pat = val | <alternatives> in x'

17+

18+...becomes...

19+

20+case val of

21+ pat => x'

22+ <alternatives>

23+

24+do pat <- val | <alternatives>

25+ p

26+

27+...becomes...

28+

29+do x <- val

30+ case x of

31+ pat => p

32+ <alternatives>

33+

34+-}

35+

36+