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

src/IRTS/CodegenC.hs+2−2

compare with master

unifiedsplit

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

82headers xs =

83 concatMap

84 (\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"])

86

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

88debug _ = ""

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

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

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

272bcc 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);"

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

275

276

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

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

233-- Generate a simple case tree

234-- Work Right to Left

235

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

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

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

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

239 ErasureInfo ->

240 TC CaseDef

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

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

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

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

243 case r of

244 Impossible -> False

245 _ -> True) cs)

246 where

247− sc' tc cover phase fc []

247+ sc' tc defcase phase fc []

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

249− sc' tc cover phase fc cs

249+ sc' tc defcase phase fc cs

250 = let proj = phase == RunTime

251 vnames = fstT (head cs)

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

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

258 ns = take numargs args

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

260 (tree, st) = runCaseBuilder erInfo

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

261+ (match ns' ps' defcase)

262 ([], numargs, [])

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

264 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

837-- Issue #1724 on the issue tracker.

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

839addCasedef :: Name -> ErasureInfo -> CaseInfo ->

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

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

841+ Bool -> Bool ->

841 [Type] -> -- argument types

842 [Type] -> -- argument types

842 [Int] -> -- inaccessible arguments

843 [Int] -> -- inaccessible arguments

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

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

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

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

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

884 let ps_in' = map simpl ps_in

885 let ps_in' = map simpl ps_in

885 pdef = map debind ps_in' in

886 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

887 OK (CaseDef args sc _) ->

888 OK (CaseDef args sc _) ->

888 addDef n (CaseOp ci

889 addDef n (CaseOp ci

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

890 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 =

158

159 erInfo <- getErasureInfo <$> getIState

160 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

162 cov <- coverage

163 pmissing <-

164 if cov && not (hasDefault cs)

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

205 ":warning - Unreachable case: " ++

206 show (delab ist x)) xs

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

208−

208+ let defaultcase = if knowncovering

209+ then STerm Erased

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

211+ show fc ++

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

213+ " ***\n"

214+

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

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

210 RunTime fc inacc atys pdef' erInfo

216 RunTime fc inacc atys pdef' erInfo

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

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

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

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

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

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

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

219 case lookupTy n ctxt of

225 case lookupTy n ctxt of

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

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

221− tcase knowncovering

227+ tcase defaultcase

222 reflect

228 reflect

223 (AssertTotal `elem` opts)

229 (AssertTotal `elem` opts)

224 atys

230 atys

src/Idris/Prover.hs+2−2

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

76 _ -> iputStrLn $ showProof lit n prf

77 let proofs = proof_list i

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

80 logLvl 3 (show tree)

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

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

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

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

87 ptm' <- applyOpts ptm

88 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

90 [] [] -- argtys, inaccArgs

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

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