4dabdba · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Propagate errors originating from case trees

4dabdbaDavid Raymond Christiansen11 years ago

src/Idris/Core/CaseTree.hs+2

compare with master

unifiedsplit

@@ -269,6 +269,8 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo

269 fstT (x, _, _) = x

270 lstT (_, _, x) = x

271

272+ -- Check that all pattern variables are reachable by a case split

273+ -- Otherwise, they won't make sense on the RHS.

272 chkAccessible (avs, l, c)

274 chkAccessible (avs, l, c)

273 | phase == RunTime || reflect = return (l, c)

275 | phase == RunTime || reflect = return (l, c)

274 | otherwise = do mapM_ (acc l) avs

276 | otherwise = do mapM_ (acc l) avs

src/Idris/Core/Evaluate.hs+36−32

@@ -1,5 +1,6 @@

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

2 PatternGuards #-}

3+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

4module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

5module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

5 rt_simplify, simplify, specialise, hnf, convEq, convEq',

6 rt_simplify, simplify, specialise, hnf, convEq, convEq',

@@ -157,6 +158,7 @@ bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)

157unbindEnv :: EnvTT n -> TT n -> TT n

158unbindEnv :: EnvTT n -> TT n -> TT n

158unbindEnv [] tm = tm

159unbindEnv [] tm = tm

159unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

160unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

161+unbindEnv env tm = error $ "Impossible case occurred: couldn't unbind env."

160

162

161usable :: Bool -- specialising

163usable :: Bool -- specialising

162 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])

164 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])

@@ -764,6 +766,7 @@ instance Show Totality where

764 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

766 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

765 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++

767 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++

766 showSep " --> " (map show ns)

768 showSep " --> " (map show ns)

769+ show (Partial (UseUndef n)) = "possibly not total because it uses the undefined name " ++ show n

767

770

768{-!

771{-!

769deriving instance Binary Accessibility

772deriving instance Binary Accessibility

@@ -866,22 +869,23 @@ addCasedef :: Name -> ErasureInfo -> CaseInfo ->

866 [([Name], Term, Term)] -> -- compile time

869 [([Name], Term, Term)] -> -- compile time

867 [([Name], Term, Term)] -> -- inlined

870 [([Name], Term, Term)] -> -- inlined

868 [([Name], Term, Term)] -> -- run time

871 [([Name], Term, Term)] -> -- run time

869− Type -> Context -> Context

872+ Type -> Context -> TC Context

870addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

873addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

871 tcase covering reflect asserted argtys inacc

874 tcase covering reflect asserted argtys inacc

872 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

875 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt

873− = let ctxt = definitions uctxt

876+ = do let ctxt = definitions uctxt

874− access = case lookupDefAcc n False uctxt of

877+ access = case lookupDefAcc n False uctxt of

875− [(_, acc)] -> acc

878+ [(_, acc)] -> acc

876− _ -> Public

879+ _ -> Public

877− ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot ei,

880+ totalityTime <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot ei

878− simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct ei,

881+ compileTime <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct ei

879− simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl ei,

882+ inlined <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl ei

880− simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt ei) of

883+ runtime <- simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt ei

884+ ctxt' <- case (totalityTime, compileTime, inlined, runtime) of

881− (OK (CaseDef args_tot sc_tot _),

885+ (CaseDef args_tot sc_tot _,

882− OK (CaseDef args_ct sc_ct _),

886+ CaseDef args_ct sc_ct _,

883− OK (CaseDef args_inl sc_inl _),

887+ CaseDef args_inl sc_inl _,

884− OK (CaseDef args_rt sc_rt _)) ->

888+ CaseDef args_rt sc_rt _) ->

885 let inl = alwaysInline -- tcdict

889 let inl = alwaysInline -- tcdict

886 inlc = (inl || small n args_ct sc_ct) && (not asserted)

890 inlc = (inl || small n args_ct sc_ct) && (not asserted)

887 inlr = inl || small n args_rt sc_rt

891 inlr = inl || small n args_rt sc_rt

@@ -892,28 +896,27 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

892 op = (CaseOp (ci { case_inlinable = inlc })

896 op = (CaseOp (ci { case_inlinable = inlc })

893 ty argtys ps_in ps_tot cdef,

897 ty argtys ps_in ps_tot cdef,

894 access, Unchecked, EmptyMI)

898 access, Unchecked, EmptyMI)

895− in addDef n op ctxt

899+ in return $ addDef n op ctxt

896− other -> error ("Error adding case def: " ++ show other)

900+-- other -> tfail (Msg $ "Error adding case def: " ++ show other)

897− in uctxt { definitions = ctxt' }

901+ return uctxt { definitions = ctxt' }

898

902

899-- simplify a definition for totality checking

903-- simplify a definition for totality checking

900−simplifyCasedef :: Name -> ErasureInfo -> Context -> Context

904+simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context

901simplifyCasedef n ei uctxt

905simplifyCasedef n ei uctxt

902− = let ctxt = definitions uctxt

906+ = do let ctxt = definitions uctxt

903− ctxt' = case lookupCtxt n ctxt of

907+ ctxt' <- case lookupCtxt n ctxt of

904− [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->

908+ [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->

905− ctxt -- nothing to simplify (or already done...)

909+ return ctxt -- nothing to simplify (or already done...)

906− [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->

910+ [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->

907− let ps_in' = map simpl ps_in

911+ do let ps_in' = map simpl ps_in

908− pdef = map debind ps_in' in

912+ pdef = map debind ps_in'

909− case simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei of

913+ CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei

910− OK (CaseDef args sc _) ->

911− addDef n (CaseOp ci

914+ return $ addDef n (CaseOp ci

912− ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

915+ ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),

913− acc, tot, metainf) ctxt

916+ acc, tot, metainf) ctxt

914− Error err -> error (show err)

917+

915− _ -> ctxt in

918+ _ -> return ctxt

916− uctxt { definitions = ctxt' }

919+ return uctxt { definitions = ctxt' }

917 where

920 where

918 depat acc (Bind n (PVar t) sc)

921 depat acc (Bind n (PVar t) sc)

919 = depat (n : acc) (instantiate (P Bound n t) sc)

922 = depat (n : acc) (instantiate (P Bound n t) sc)

@@ -1068,6 +1071,7 @@ lookupVal n ctxt

1068 case tfst def of

1071 case tfst def of

1069 (Function _ htm) -> return (veval ctxt [] htm)

1072 (Function _ htm) -> return (veval ctxt [] htm)

1070 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

1073 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

1074+ _ -> []

1071

1075

1072lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

1076lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

1073lookupTyEnv n env = li n 0 env where

1077lookupTyEnv n env = li n 0 env where

src/Idris/Coverage.hs+3−1

@@ -423,7 +423,9 @@ checkTotality path fc n

423 | otherwise = do

424 t <- getTotality n

425 i <- getIState

426+ ctxt' <- do ctxt <- getContext

426− updateContext (simplifyCasedef n $ getErasureInfo i)

427+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt

428+ setContext ctxt'

427 ctxt <- getContext

429 ctxt <- getContext

428 i <- getIState

430 i <- getIState

429 let opts = case lookupCtxt n (idris_flags i) of

431 let opts = case lookupCtxt n (idris_flags i) of

src/Idris/Elab/Clause.hs+8−4

@@ -224,17 +224,21 @@ elabClauses info' fc opts n_in cs =

224 (idris_patdefs ist) })

225 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)

226 case lookupTy n ctxt of

227+ [ty] -> do ctxt' <- do ctxt <- getContext

228+ tclift $

227− [ty] -> do updateContext (addCasedef n erInfo caseInfo

229+ addCasedef n erInfo caseInfo

228 tcase defaultcase

230 tcase defaultcase

229 reflect

231 reflect

230 (AssertTotal `elem` opts)

232 (AssertTotal `elem` opts)

231 atys

233 atys

232 inacc

234 inacc

233 pats_pe

235 pats_pe

234− pdef

236+ pdef

235− pdef -- compile time

237+ pdef -- compile time

236 pdef_inl -- inlined

238 pdef_inl -- inlined

237− pdef' ty)

239+ pdef' ty

240+ ctxt

241+ setContext ctxt'

238 addIBC (IBCDef n)

242 addIBC (IBCDef n)

239 setTotality n tot

243 setTotality n tot

240 when (not reflect) $ do totcheck (fc, n)

244 when (not reflect) $ do totcheck (fc, n)

src/Idris/Elab/Term.hs+13−12

@@ -1730,18 +1730,19 @@ runTactical ist fc env tm = do tm' <- eval tm

1730 Left lhs -> let (ns, lhs') = patvars [] lhs'

1731 in (ns, lhs', Impossible))

1732 clauses'

1733− set_context $

1733+ ctxt'<- lift $

1734− addCasedef n (const [])

1734+ addCasedef n (const [])

1735− info False (STerm Erased)

1735+ info False (STerm Erased)

1736− True False -- TODO what are these?

1736+ True False -- TODO what are these?

1737− (map snd $ getArgTys ty) [] -- TODO inaccessible types

1737+ (map snd $ getArgTys ty) [] -- TODO inaccessible types

1738− clauses'

1738+ clauses'

1739− clauses''

1739+ clauses''

1740− clauses''

1740+ clauses''

1741− clauses''

1741+ clauses''

1742− clauses''

1742+ clauses''

1743− ty

1743+ ty

1744+ ctxt

1744− ctxt

1745+ set_context ctxt'

1745 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}

1746 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}

1746 return ()

1747 return ()

1747

1748

src/Idris/ElabDecls.hs+3−1

@@ -195,7 +195,9 @@ elabDecl' what info (PMutual f ps)

195 -- Do totality checking after entire mutual block

196 i <- get

197 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

198+ ctxt' <- do ctxt <- getContext

198− updateContext (simplifyCasedef n $ getErasureInfo i))

199+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt

200+ setContext ctxt')

199 (map snd (idris_totcheck i))

201 (map snd (idris_totcheck i))

200 mapM_ buildSCG (idris_totcheck i)

202 mapM_ buildSCG (idris_totcheck i)

201 mapM_ checkDeclTotality (idris_totcheck i)

203 mapM_ checkDeclTotality (idris_totcheck i)

src/Idris/Parser.hs+4−1

@@ -1474,7 +1474,10 @@ loadSource lidr f toline

1474 -- simplify every definition do give the totality checker

1475 -- a better chance

1476 mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

1477+ ctxt' <-

1478+ do ctxt <- getContext

1477− updateContext (simplifyCasedef n $ getErasureInfo i))

1479+ tclift $ simplifyCasedef n (getErasureInfo i) ctxt

1480+ setContext ctxt')

1478 (map snd (idris_totcheck i))

1481 (map snd (idris_totcheck i))

1479 -- build size change graph from simplified definitions

1482 -- build size change graph from simplified definitions

1480 iLOG "Totality checking"

1483 iLOG "Totality checking"

src/Idris/Prover.hs+10−7

@@ -86,13 +86,16 @@ prove opt ctxt lit n ty

86 Error e -> ierror (CantUnify False (ty, Nothing) (pty, Nothing) e [] 0)

87 ptm' <- applyOpts ptm

88 ei <- getErasureInfo `fmap` getIState

89+ ctxt' <- do ctxt <- getContext

89− updateContext (addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False

90+ tclift $ addCasedef n ei (CaseInfo True True False) False (STerm Erased) True False

90− [] [] -- argtys, inaccArgs

91+ [] [] -- argtys, inaccArgs

91− [Right (P Ref n ty, ptm)]

92+ [Right (P Ref n ty, ptm)]

92− [([], P Ref n ty, ptm)]

93+ [([], P Ref n ty, ptm)]

93− [([], P Ref n ty, ptm)]

94+ [([], P Ref n ty, ptm)]

94− [([], P Ref n ty, ptm)]

95+ [([], P Ref n ty, ptm)]

95− [([], P Ref n ty, ptm')] ty)

96+ [([], P Ref n ty, ptm')] ty

97+ ctxt

98+ setContext ctxt'

96 solveDeferred n

99 solveDeferred n

97 case idris_outputmode i of

100 case idris_outputmode i of

98 IdeMode n h ->

101 IdeMode n h ->