19495ed · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check patterns are inaccessible

commit19495ed3a1bd7980883de5ae4d38327e9cf5bda0 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 24 Apr 2012, 14:57 (15 years ago) parent489ea6f

10 files changed+46−15

compare with master

unifiedsplit

src/Core/CaseTree.hs+22−9 src/Core/Evaluate.hs+3−3 src/Core/TT.hs+3 src/Idris/Delaborate.hs+1 src/Idris/ElabDecls.hs+2−2 src/Idris/Prover.hs+1−1 test/README+1 test/test012/expected+1 test/test012/run+2 test/test012/test012a.idr+10

src/Core/CaseTree.hs+22−9

@@ -53,19 +53,32 @@ namesUsed sc = nub $ nu' [] sc where

5353 nut ps (Bind n b sc) = nut (n:ps) sc

5454 nut ps _ = []

5555

56−simpleCase :: Bool -> Bool -> [([Name], Term, Term)] -> CaseDef

57−simpleCase tc cover []

58− = CaseDef [] (UnmatchedCase "No pattern clauses") []

59−simpleCase tc cover cs

60− = let pats = map (\ (avs, l, r) -> (toPats tc l, (l, r))) cs

61− numargs = length (fst (head pats))

62− ns = take numargs args

63− (tree, st) = runState (match ns pats (defaultCase cover)) ([], numargs) in

64− CaseDef ns (prune tree) (fst st)

56+simpleCase :: Bool -> Bool -> FC -> [([Name], Term, Term)] -> TC CaseDef

57+simpleCase tc cover fc []

58+ = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

59+simpleCase tc cover fc cs

60+ = let pats = map (\ (avs, l, r) -> (avs, toPats tc l, (l, r))) cs

61+ chkPats = mapM chkAccessible pats in

62+ case chkPats of

63+ OK pats ->

64+ let numargs = length (fst (head pats))

65+ ns = take numargs args

66+ (tree, st) = runState

67+ (match ns pats (defaultCase cover)) ([], numargs) in

68+ return $ CaseDef ns (prune tree) (fst st)

69+ Error err -> Error (At fc err)

6570 where args = map (\i -> MN i "e") [0..]

6671 defaultCase True = STerm Erased

6772 defaultCase False = UnmatchedCase "Error"

6873

74+ chkAccessible (avs, l, c) = do mapM_ (acc l) avs

75+ return (l, c)

76+

77+ acc [] n = Error (Inaccessible n)

78+ acc (PV x : xs) n | x == n = OK ()

79+ acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

80+ acc (_ : xs) n = acc xs n

81+

6982data Pat = PCon Name Int [Pat]

7083 | PConst Const

7184 | PV Name

src/Core/Evaluate.hs+3−3

@@ -679,9 +679,9 @@ addCasedef :: Name -> Bool -> Bool -> Bool ->

679679addCasedef n alwaysInline tcase covering ps psrt ty uctxt

680680 = let ctxt = definitions uctxt

681681 ps' = ps -- simpl ps in

682− ctxt' = case (simpleCase tcase covering ps',

683− simpleCase tcase covering psrt) of

684− (CaseDef args sc _, CaseDef args' sc' _) ->

682+ ctxt' = case (simpleCase tcase covering (FC "" 0) ps',

683+ simpleCase tcase covering (FC "" 0) psrt) of

684+ (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

685685 let inl = alwaysInline in

686686 addDef n (CaseOp inl ty ps args sc args' sc',

687687 Public, Unchecked) ctxt in

src/Core/TT.hs+3

@@ -50,6 +50,7 @@ data Err = Msg String

5050 | IncompleteTerm Term

5151 | UniverseError

5252 | ProgramLineComment

53+ | Inaccessible Name

5354 | At FC Err

5455 deriving Eq

5556

@@ -63,6 +64,7 @@ instance Sized Err where

6364 size UniverseError = 1

6465 size ProgramLineComment = 1

6566 size (At fc err) = size fc + size err

67+ size (Inaccessible _) = 1

6668

6769score :: Err -> Int

6870score (CantUnify _ _ m s) = s + score m

@@ -74,6 +76,7 @@ instance Show Err where

7476 show (Msg s) = s

7577 show (CantUnify l r e i) = "CantUnify " ++ show l ++ " " ++ show r ++ " "

7678 ++ show e ++ " " ++ show i

79+ show (Inaccessible n) = show n ++ " is not an accessible pattern variable"

7780 show _ = "Error"

7881

7982instance Pretty Err where

src/Idris/Delaborate.hs+1

@@ -85,5 +85,6 @@ pshow i (NoSuchVariable n) = "No such variable " ++ show n

8585pshow i (IncompleteTerm t) = "Incomplete term " ++ show (delab i t)

8686pshow i UniverseError = "Universe inconsistency"

8787pshow i ProgramLineComment = "Program line next to comment"

88+pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

8889pshow i (At f e) = show f ++ ":" ++ pshow i e

8990

src/Idris/ElabDecls.hs+2−2

@@ -260,7 +260,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

260260-- return False

261261 else return False

262262 pdef' <- applyOpts pdef

263− let tree@(CaseDef _ sc _) = simpleCase tcase pcover pdef

263+ tree@(CaseDef _ sc _) <- tclift $ simpleCase tcase pcover fc pdef

264264 ist <- get

265265-- let wf = wellFounded ist n sc

266266 let tot = if pcover || AssertTotal `elem` opts

@@ -279,7 +279,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

279279 iputStrLn $ show fc ++

280280 ":warning - Unreachable case: " ++

281281 show (delab ist x)) xs

282− let tree' = simpleCase tcase pcover pdef'

282+ tree' <- tclift $ simpleCase tcase pcover fc pdef'

283283 tclift $ sameLength pdef

284284 logLvl 3 (show tree)

285285 logLvl 3 $ "Optimised: " ++ show tree'

src/Idris/Prover.hs+1−1

@@ -45,7 +45,7 @@ prove ctxt lit n ty

4545 iputStrLn $ showProof lit n prf

4646 i <- get

4747 put (i { last_proof = Just (n, prf) })

48− let tree = simpleCase False True [([], P Ref n ty, tm)]

48+ let tree = simpleCase False True (FC "proof" 0) [([], P Ref n ty, tm)]

4949 logLvl 3 (show tree)

5050 (ptm, pty) <- recheckC (FC "proof" 0) [] tm

5151 ptm' <- applyOpts ptm

test/README+1

@@ -11,3 +11,4 @@ Tests:

1111009: ranges and list monad

1212010: total

1313011: record projection and update

14+012: various error regressions

test/test012/expectednew file+1

@@ -0,0 +1 @@

1+test012a.idr:7:x is not an accessible pattern variable

test/test012/runnew file+2

@@ -0,0 +1,2 @@

1+#!/bin/bash

2+idris test012a.idr -o test012a

test/test012/test012a.idrnew file+10

@@ -0,0 +1,10 @@

1+module main

3+f : Nat -> Nat

4+f x = x + 1

6+foo : Nat -> Nat

7+foo (f x) = x

9+main : IO ()

10+main = putStrLn (show (foo 1))