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

git.iko.soy/Idris-dev

Syntax for failures in pattern matching let/<-

let pat = val | <alternatives> in x' ...becomes... case val of pat => x' <alternatives> do pat <- val | <alternatives> p ...becomes... do x <- val case x of pat => p <alternatives> So in particular, large effectful functions can deal with failure inline rather than having lots of nested case blocks, e.g. main : IO () main = do [p, a] <- getArgs | [p] => putStrLn "No arguments!" | (x :: y :: _) => putStrLn "Too many arguments!" print (foo (Just (cast a)))

commit8f93b003075cdd477457464e6ec89231bdb04b0b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 7 Mar 2014, 20:57 (13 years ago) parentb2b5545

11 files changed+93−26

compare with master

unifiedsplit

CHANGELOG+6−5 Makefile+1−1 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/DSL.hs+2−2 src/Idris/DeepSeq.hs+1−1 src/Idris/IBC.hs+8−6 src/Idris/ParseExpr.hs+25−6 test/Makefile+3−3 test/sugar004/expected+3 test/sugar004/run+6 test/sugar004/sugar004.idr+36

CHANGELOG+6−5

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

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

55 type inference.

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

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

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

9−* Lots of performance patches for generated JavaScript

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

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

9+* Lots of performance patches for generated JavaScript.

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

11− or show the type of expressions

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

11+ or show the type of expressions.

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

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

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

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

1516||| Add two natural numbers

Makefile+1−1

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

3939 $(CABAL) install $(CABALFLAGS)

4040

4141linecount:

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

4343

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

4545doc: dist/setup-config

src/Idris/AbsSyntaxTree.hs+2−2

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

737737

738738data PDo' t = DoExp FC t

739739 | DoBind FC Name t

740− | DoBindP FC t t

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

741741 | DoLet FC Name t t

742742 | DoLetP FC t t

743743 deriving (Eq, Functor)

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

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

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

751751 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

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

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

755755

src/Idris/DSL.hs+2−2

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

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

5858 block b (DoBind fc n tm : rest)

5959 = 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)

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

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

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

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

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

6565 = PLet n ty tm (block b rest)

6666 block b (DoLetP fc p tm : rest)

src/Idris/DeepSeq.hs+1−1

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

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

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

228228 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` ()

230230 rnf (DoLet x1 x2 x3 x4)

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

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

2525import Util.Zlib (decompressEither)

2626

2727ibcVersion :: Word8

28−ibcVersion = 62

28+ibcVersion = 63

2929

3030

3131data IBCFile = IBCFile { ver :: Word8,

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

18781878 put x1

18791879 put x2

18801880 put x3

1881− DoBindP x1 x2 x3 -> do putWord8 2

1882− put x1

1883− put x2

1884− put x3

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

1882+ put x1

1883+ put x2

1884+ put x3

1885+ put x4

18851886 DoLet x1 x2 x3 x4 -> do putWord8 3

18861887 put x1

18871888 put x2

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

19041905 2 -> do x1 <- get

19051906 x2 <- get

19061907 x3 <- get

1907− return (DoBindP x1 x2 x3)

1908+ x4 <- get

1909+ return (DoBindP x1 x2 x3 x4)

19081910 3 -> do x1 <- get

19091911 x2 <- get

19101912 x3 <- get

src/Idris/ParseExpr.hs+25−6

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

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

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

169169 : upd (dropn n ns) ds

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

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

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

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

171173 : upd ns ds

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

173175 : upd ns ds

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

736738@

737739 -}

738740let_ :: SyntaxInfo -> IdrisParser PTerm

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

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

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

741743 lchar '='

742744 v <- expr syn

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

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

743747 reserved "in"; sc <- expr syn

744− return (PLet n ty v sc))

748+ case ts of

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

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

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

746752 symbol "="; v <- expr syn

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

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

747755 reserved "in"; sc <- expr syn

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

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

749757 <?> "let binding"

750758

751759{- | Parses a quote goal

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

967975 symbol "<-"

968976 fc <- getFC

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

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

972983 symbol "<-"

973984 fc <- getFC

974985 e <- expr syn;

975− return (DoBindP fc i e))

986+ option (DoBindP fc i e [])

987+ (do lchar '|'

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

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

976990 <|> do e <- expr syn

977991 fc <- getFC

978992 return (DoExp fc e)

979993 <?> "do block expression"

980994

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

996+ symbol "=>"

997+ r <- expr' syn

998+ return (l, r)

999+

9811000{- | Parses an expression in idiom brackets

9821001@

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

test/Makefile+3−3

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

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

1010test_java:

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

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

1212

1313test_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

1515

1616test_llvm:

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

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

1818

1919update:

2020 /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

3+import System

5+total

6+foo : Maybe Int -> Int

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

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+