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

src/Core/CaseTree.hs+22−9

compare with master

unifiedsplit

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

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

54 nut ps _ = []

55

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

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

57−simpleCase tc cover []

57+simpleCase tc cover fc []

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

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

59−simpleCase tc cover cs

59+simpleCase tc cover fc cs

60− = let pats = map (\ (avs, l, r) -> (toPats tc l, (l, r))) 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 ->

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

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

62− ns = take numargs args

65+ ns = take numargs args

66+ (tree, st) = runState

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

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

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

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

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

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

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

66 defaultCase True = STerm Erased

71 defaultCase True = STerm Erased

67 defaultCase False = UnmatchedCase "Error"

72 defaultCase False = UnmatchedCase "Error"

68

73

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+

69data Pat = PCon Name Int [Pat]

82data Pat = PCon Name Int [Pat]

70 | PConst Const

83 | PConst Const

71 | PV Name

84 | PV Name

src/Core/Evaluate.hs+3−3

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

679addCasedef n alwaysInline tcase covering ps psrt ty uctxt

680 = let ctxt = definitions uctxt

681 ps' = ps -- simpl ps in

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

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

683− simpleCase tcase covering psrt) of

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

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

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

685 let inl = alwaysInline in

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

687 Public, Unchecked) ctxt in

src/Core/TT.hs+3

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

50 | IncompleteTerm Term

51 | UniverseError

52 | ProgramLineComment

53+ | Inaccessible Name

53 | At FC Err

54 | At FC Err

54 deriving Eq

55 deriving Eq

55

56

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

63 size UniverseError = 1

64 size UniverseError = 1

64 size ProgramLineComment = 1

65 size ProgramLineComment = 1

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

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

67+ size (Inaccessible _) = 1

66

68

67score :: Err -> Int

69score :: Err -> Int

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

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

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

74 show (Msg s) = s

76 show (Msg s) = s

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

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

76 ++ show e ++ " " ++ show i

78 ++ show e ++ " " ++ show i

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

77 show _ = "Error"

80 show _ = "Error"

78

81

79instance Pretty Err where

82instance Pretty Err where

src/Idris/Delaborate.hs+1

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

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

86pshow i UniverseError = "Universe inconsistency"

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

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

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

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

89

90

src/Idris/ElabDecls.hs+2−2

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

260-- return False

261 else return False

262 pdef' <- applyOpts pdef

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

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

264 ist <- get

265-- let wf = wellFounded ist n sc

266 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

279 iputStrLn $ show fc ++

280 ":warning - Unreachable case: " ++

281 show (delab ist x)) xs

282− let tree' = simpleCase tcase pcover pdef'

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

283 tclift $ sameLength pdef

284 logLvl 3 (show tree)

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

src/Idris/Prover.hs+1−1

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

45 iputStrLn $ showProof lit n prf

46 i <- get

47 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)]

49 logLvl 3 (show tree)

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

51 ptm' <- applyOpts ptm

test/README+1

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

11009: ranges and list monad

12010: total

13011: 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

2+

3+f : Nat -> Nat

4+f x = x + 1

5+

6+foo : Nat -> Nat

7+foo (f x) = x

8+

9+main : IO ()

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