5faaba9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

More information runtime error for missing case

Now gives line number and function, returning an error code, without the ugly assertion failure.

commit5faaba901cba14cd2e94eb2570a3fc5151233034 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 21 Dec 2014, 22:57 (12 years ago) parente95c877

5 files changed+23−16

compare with master

unifiedsplit

src/IRTS/CodegenC.hs+2−2 src/Idris/Core/CaseTree.hs+6−6 src/Idris/Core/Evaluate.hs+3−2 src/Idris/Elab/Clause.hs+10−4 src/Idris/Prover.hs+2−2

src/IRTS/CodegenC.hs+2−2

@@ -82,7 +82,7 @@ codegenC' defs out exec incs objs libs flags dbg

8282headers xs =

8383 concatMap

8484 (\h -> "#include <" ++ h ++ ">\n")

85− (xs ++ ["idris_rts.h", "idris_bitstring.h", "idris_stdfgn.h", "assert.h"])

85+ (xs ++ ["idris_rts.h", "idris_bitstring.h", "idris_stdfgn.h"])

8686

8787debug TRACE = "#define IDRIS_TRACE\n\n"

8888debug _ = ""

@@ -270,7 +270,7 @@ bcc i (FOREIGNCALL l LANG_C rty fn args)

270270 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"

271271 where fcall (t, arg) = irts_c t (creg arg)

272272bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed

273−bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); assert(0); exit(-1);"

273+bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); exit(-1); exit(-1);"

274274-- bcc i _ = indent i ++ "// not done yet\n"

275275

276276

src/Idris/Core/CaseTree.hs+6−6

@@ -233,20 +233,20 @@ data Phase = CompileTime | RunTime

233233-- Generate a simple case tree

234234-- Work Right to Left

235235

236−simpleCase :: Bool -> Bool -> Bool ->

236+simpleCase :: Bool -> SC -> Bool ->

237237 Phase -> FC -> [Int] -> [Type] ->

238238 [([Name], Term, Term)] ->

239239 ErasureInfo ->

240240 TC CaseDef

241−simpleCase tc cover reflect phase fc inacc argtys cs erInfo

242− = sc' tc cover phase fc (filter (\(_, _, r) ->

241+simpleCase tc defcase reflect phase fc inacc argtys cs erInfo

242+ = sc' tc defcase phase fc (filter (\(_, _, r) ->

243243 case r of

244244 Impossible -> False

245245 _ -> True) cs)

246246 where

247− sc' tc cover phase fc []

247+ sc' tc defcase phase fc []

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

249− sc' tc cover phase fc cs

249+ sc' tc defcase phase fc cs

250250 = let proj = phase == RunTime

251251 vnames = fstT (head cs)

252252 pats = map (\ (avs, l, r) ->

@@ -258,7 +258,7 @@ simpleCase tc cover reflect phase fc inacc argtys cs erInfo

258258 ns = take numargs args

259259 (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats

260260 (tree, st) = runCaseBuilder erInfo

261− (match ns' ps' (defaultCase cover))

261+ (match ns' ps' defcase)

262262 ([], numargs, [])

263263 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in

264264 if proj then return (stripLambdas t)

src/Idris/Core/Evaluate.hs+3−2

@@ -837,7 +837,8 @@ addDatatype (Data n tag ty unique cons) uctxt

837837-- Issue #1724 on the issue tracker.

838838-- https://github.com/idris-lang/Idris-dev/issues/1724

839839addCasedef :: Name -> ErasureInfo -> CaseInfo ->

840− Bool -> Bool -> Bool -> Bool ->

840+ Bool -> SC -> -- default case

841+ Bool -> Bool ->

841842 [Type] -> -- argument types

842843 [Int] -> -- inaccessible arguments

843844 [Either Term (Term, Term)] ->

@@ -883,7 +884,7 @@ simplifyCasedef n ei uctxt

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

884885 let ps_in' = map simpl ps_in

885886 pdef = map debind ps_in' in

886− case simpleCase False True False CompileTime emptyFC [] atys pdef ei of

887+ case simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei of

887888 OK (CaseDef args sc _) ->

888889 addDef n (CaseOp ci

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

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

@@ -158,7 +158,7 @@ elabClauses info' fc opts n_in cs =

158158

159159 erInfo <- getErasureInfo <$> getIState

160160 tree@(CaseDef scargs sc _) <- tclift $

161− simpleCase tcase False reflect CompileTime fc inacc atys pdef erInfo

161+ simpleCase tcase (UnmatchedCase "Error") reflect CompileTime fc inacc atys pdef erInfo

162162 cov <- coverage

163163 pmissing <-

164164 if cov && not (hasDefault cs)

@@ -205,8 +205,14 @@ elabClauses info' fc opts n_in cs =

205205 ":warning - Unreachable case: " ++

206206 show (delab ist x)) xs

207207 let knowncovering = (pcover && cov) || AssertTotal `elem` opts

208−

209− tree' <- tclift $ simpleCase tcase knowncovering reflect

208+ let defaultcase = if knowncovering

209+ then STerm Erased

210+ else UnmatchedCase $ "*** " ++

211+ show fc ++

212+ ":unmatched case in " ++ show n ++

213+ " ***\n"

214+

215+ tree' <- tclift $ simpleCase tcase defaultcase reflect

210216 RunTime fc inacc atys pdef' erInfo

211217 logLvl 3 $ "Unoptimised " ++ show n ++ ": " ++ show tree

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

@@ -218,7 +224,7 @@ elabClauses info' fc opts n_in cs =

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

219225 case lookupTy n ctxt of

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

221− tcase knowncovering

227+ tcase defaultcase

222228 reflect

223229 (AssertTotal `elem` opts)

224230 atys

src/Idris/Prover.hs+2−2

@@ -76,7 +76,7 @@ prove opt ctxt lit n ty

7676 _ -> iputStrLn $ showProof lit n prf

7777 let proofs = proof_list i

7878 putIState (i { proof_list = (n, prf) : proofs })

79− let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

79+ let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

8080 logLvl 3 (show tree)

8181 (ptm, pty) <- recheckC (fileFC "proof") [] tm

8282 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

@@ -86,7 +86,7 @@ prove opt ctxt lit n ty

8686 Error e -> ierror (CantUnify False ty pty e [] 0)

8787 ptm' <- applyOpts ptm

8888 ei <- getErasureInfo `fmap` getIState

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

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

9090 [] [] -- argtys, inaccArgs

9191 [Right (P Ref n ty, ptm)]

9292 [([], P Ref n ty, ptm)]