a13b22c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'lambda-impossible' of https://github.com/Melvar/Idris-dev into Melvar-lambda-impossible

commita13b22ca9dc37f0efdd53a28b6953a82ff72f3c2 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 31 Mar 2015, 11:24 (12 years ago) parent5c8c1d3 9560761

7 files changed+81−10

compare with master

unifiedsplit

idris.cabal+3 src/Idris/ParseExpr.hs+21−8 src/Idris/Parser.hs+2−2 test/totality009/TestLambdaImpossible.idr+29 test/totality009/TestLambdaPossible.idr+13 test/totality009/expected+8 test/totality009/run+5

idris.cabal+3

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

611611 test/totality008/run

612612 test/totality008/*.idr

613613 test/totality008/expected

614+ test/totality009/run

615+ test/totality009/*.idr

616+ test/totality009/expected

614617

615618 test/tutorial001/run

616619 test/tutorial001/*.idr

src/Idris/ParseExpr.hs+21−8

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

234234 <|> app syn

235235 <?> "expression"

236236

237+{- | Parses the "impossible" keyword

238+@

239+Impossible ::= 'impossible'

240+@

241+-}

242+impossible :: IdrisParser PTerm

243+impossible = PImpossible <$ reserved "impossible"

244+

237245{- | Parses a case expression

238246@

239247CaseExpr ::=

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

250258{- | Parses a case in a case expression

251259@

252260CaseOption ::=

253− Expr '=>' Expr Terminator

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

254262 ;

255263@

256264-}

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

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

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

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

260268 return (lhs, r)

261269 <?> "case option"

262270

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

732740{- | Parses a lambda expression

733741@

734742Lambda ::=

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

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

743+ '\\' TypeOptDeclList LambdaTail

744+ | '\\' SimpleExprList LambdaTail

737745 ;

738746@

739747@

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

742750 | SimpleExpr ',' SimpleExprList

743751 ;

744752@

753+@

754+LambdaTail ::=

755+ Impossible

756+ | '=>' Expr

757+@

745758-}

746759lambda :: SyntaxInfo -> IdrisParser PTerm

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

748761 (do xt <- try $ tyOptDeclList syn

749762 fc <- getFC

750− symbol "=>"

751− sc <- expr syn

763+ sc <- lambdaTail

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

753765 ps <- sepBy (do fc <- getFC

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

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

756− symbol "=>"

757− sc <- expr syn

768+ sc <- lambdaTail

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

759770 <?> "lambda expression"

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

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

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

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

765776 [(x, pmList xs sc)])

777+ lambdaTail :: IdrisParser PTerm

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

766779

767780{- | Parses a term rewrite expression

768781@

src/Idris/Parser.hs+2−2

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

815815@

816816RHS ::= '=' Expr

817817 | '?=' RHSName? Expr

818− | 'impossible'

818+ | Impossible

819819 ;

820820@

821821

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

831831 return n)

832832 r <- expr syn

833833 return (addLet fc name r)

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

834+ <|> impossible

835835 <?> "function right hand side"

836836 where mkN :: Name -> Name

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

test/totality009/TestLambdaImpossible.idrnew file+29

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

1+module TestLambdaImpossible

3+%default total

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

4+data Nool : Bool -> Type where

5+ Flase : Nool False

6+ Ture : Nool True

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