a13b22c · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

611 test/totality008/run

612 test/totality008/*.idr

613 test/totality008/expected

614+ test/totality009/run

615+ test/totality009/*.idr

616+ test/totality009/expected

614

617

615 test/tutorial001/run

618 test/tutorial001/run

616 test/tutorial001/*.idr

619 test/tutorial001/*.idr

src/Idris/ParseExpr.hs+21−8

@@ -234,6 +234,14 @@ internalExpr syn =

234 <|> app syn

235 <?> "expression"

236

237+{- | Parses the "impossible" keyword

238+@

239+Impossible ::= 'impossible'

240+@

241+-}

242+impossible :: IdrisParser PTerm

243+impossible = PImpossible <$ reserved "impossible"

244+

237{- | Parses a case expression

245{- | Parses a case expression

238@

246@

239CaseExpr ::=

247CaseExpr ::=

@@ -250,13 +258,13 @@ caseExpr syn = do reserved "case"; fc <- getFC

250{- | Parses a case in a case expression

258{- | Parses a case in a case expression

251@

259@

252CaseOption ::=

260CaseOption ::=

253− Expr '=>' Expr Terminator

261+ Expr (Impossible | '=>' Expr) Terminator

254 ;

262 ;

255@

263@

256-}

264-}

257caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

265caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

258caseOption syn = do lhs <- expr (syn { inPattern = True })

266caseOption syn = do lhs <- expr (syn { inPattern = True })

259− symbol "=>"; r <- expr syn

267+ r <- impossible <|> symbol "=>" *> expr syn

260 return (lhs, r)

268 return (lhs, r)

261 <?> "case option"

269 <?> "case option"

262

270

@@ -732,8 +740,8 @@ typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else retu

732{- | Parses a lambda expression

740{- | Parses a lambda expression

733@

741@

734Lambda ::=

742Lambda ::=

735− '\\' TypeOptDeclList '=>' Expr

743+ '\\' TypeOptDeclList LambdaTail

736− | '\\' SimpleExprList '=>' Expr

744+ | '\\' SimpleExprList LambdaTail

737 ;

745 ;

738@

746@

739@

747@

@@ -742,19 +750,22 @@ SimpleExprList ::=

742 | SimpleExpr ',' SimpleExprList

750 | SimpleExpr ',' SimpleExprList

743 ;

751 ;

744@

752@

753+@

754+LambdaTail ::=

755+ Impossible

756+ | '=>' Expr

757+@

745-}

758-}

746lambda :: SyntaxInfo -> IdrisParser PTerm

759lambda :: SyntaxInfo -> IdrisParser PTerm

747lambda syn = do lchar '\\' <?> "lambda expression"

760lambda syn = do lchar '\\' <?> "lambda expression"

748 (do xt <- try $ tyOptDeclList syn

761 (do xt <- try $ tyOptDeclList syn

749 fc <- getFC

762 fc <- getFC

750− symbol "=>"

763+ sc <- lambdaTail

751− sc <- expr syn

752 return (bindList (PLam fc) xt sc)) <|> do

764 return (bindList (PLam fc) xt sc)) <|> do

753 ps <- sepBy (do fc <- getFC

765 ps <- sepBy (do fc <- getFC

754 e <- simpleExpr (syn { inPattern = True })

766 e <- simpleExpr (syn { inPattern = True })

755 return (fc, e)) (lchar ',')

767 return (fc, e)) (lchar ',')

756− symbol "=>"

768+ sc <- lambdaTail

757− sc <- expr syn

758 return (pmList (zip [0..] ps) sc)

769 return (pmList (zip [0..] ps) sc)

759 <?> "lambda expression"

770 <?> "lambda expression"

760 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

771 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

@@ -763,6 +774,8 @@ lambda syn = do lchar '\\' <?> "lambda expression"

763 = PLam fc (sMN i "lamp") Placeholder

774 = PLam fc (sMN i "lamp") Placeholder

764 (PCase fc (PRef fc (sMN i "lamp"))

775 (PCase fc (PRef fc (sMN i "lamp"))

765 [(x, pmList xs sc)])

776 [(x, pmList xs sc)])

777+ lambdaTail :: IdrisParser PTerm

778+ lambdaTail = impossible <|> symbol "=>" *> expr syn

766

779

767{- | Parses a term rewrite expression

780{- | Parses a term rewrite expression

768@

781@

src/Idris/Parser.hs+2−2

@@ -815,7 +815,7 @@ argExpr syn = let syn' = syn { inPattern = True } in

815@

816RHS ::= '=' Expr

817 | '?=' RHSName? Expr

818− | 'impossible'

818+ | Impossible

819 ;

820@

821

@@ -831,7 +831,7 @@ rhs syn n = do lchar '='; expr syn

831 return n)

832 r <- expr syn

833 return (addLet fc name r)

834− <|> do reserved "impossible"; return PImpossible

834+ <|> impossible

835 <?> "function right hand side"

836 where mkN :: Name -> Name

837 mkN (UN x) = if (tnull x || not (isAlpha (thead x)))

test/totality009/TestLambdaImpossible.idrnew file+29

@@ -0,0 +1,29 @@

1+module TestLambdaImpossible

2+

3+%default total

4+

5+eqBool : (x, y : Bool) -> Dec (x = y)

6+eqBool False False = Yes Refl

7+eqBool False True = No (\(Refl) impossible)

8+eqBool True False = No (\(Refl) impossible)

9+eqBool True True = Yes Refl

10+

11+data Elem : {a : Type} -> a -> Prelude.List.List a -> Type where

12+ Here : {a : Type} -> {x : a} -> {xs : List a} -> Elem x (x :: xs)

13+ There : {a : Type} -> {x, y : a} -> {xs : List a} -> Elem x xs -> Elem x (y :: xs)

14+

15+notHereNotThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))

16+notHereNotThere notEq notElem Here = notEq Refl

17+notHereNotThere notEq notElem (There elem) = notElem elem

18+

19+decElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)

20+decElem x [] = No (\Here impossible)

21+decElem x (y :: xs) with (decEq x y)

22+ decElem x (x :: xs) | (Yes Refl) = Yes Here

23+ decElem x (y :: xs) | (No notHere) with (decElem x xs)

24+ decElem x (y :: xs) | (No notHere) | (Yes prf) = Yes (There prf)

25+ decElem x (y :: xs) | (No notHere) | (No notThere) = No $ notHereNotThere notHere notThere

26+

27+notEta : ((a : Type) -> (b : Type) -> (f : a -> b) -> f = (\x => f x)) -> Void

28+notEta eta = case eta Nat Nat id of

29+ Refl impossible

test/totality009/TestLambdaPossible.idrnew file+13

@@ -0,0 +1,13 @@

1+||| Some functions that should be non-total, as detected with --warnpartial

2+module TestLambdaPossible

3+

4+data Nool : Bool -> Type where

5+ Flase : Nool False

6+ Ture : Nool True

7+

8+wrongPossible : Nool True -> Bool

9+wrongPossible = (\Flase impossible)

10+

11+wrongPossible' : Nool True -> Bool

12+wrongPossible' x = case x of

13+ Flase impossible

test/totality009/expectednew file+8

@@ -0,0 +1,8 @@

1+TestLambdaPossible.idr:9:25:Warning - TestLambdaPossible.case block in wrongPossible is not total as there are missing cases

2+TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible

3+TestLambdaPossible.idr:12:25:Warning - TestLambdaPossible.case block in wrongPossible' is not total as there are missing cases

4+TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible'

5+TestLambdaPossible.idr:9:15:Warning - TestLambdaPossible.case block in wrongPossible is not total as there are missing cases

6+TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible

7+TestLambdaPossible.idr:12:16:Warning - TestLambdaPossible.case block in wrongPossible' is not total as there are missing cases

8+TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible'

test/totality009/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+OPTS="--consolewidth infinite --nocolour"

3+idris "$@" $OPTS --check TestLambdaImpossible

4+idris "$@" $OPTS --check --warnpartial TestLambdaPossible

5+rm -f *.ibc