a6c36d3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Undo previous change until I work out why it was important...

a6c36d3Edwin Brady14 years ago

src/Idris/Coverage.hs+5−3

compare with master

unifiedsplit

@@ -403,7 +403,7 @@ buildSCG (_, n) = do

403 case lookupCtxt Nothing n (idris_callgraph ist) of

404 [cg] -> case lookupDef Nothing n (tt_ctxt ist) of

405 [CaseOp _ _ _ _ _ args sc _ _] ->

406− do logLvl 5 $ "Building SCG for " ++ show n ++ " from\n"

406+ do logLvl 3 $ "Building SCG for " ++ show n ++ " from\n"

407 ++ show sc

408 let newscg = buildSCG' ist sc args

409 logLvl 5 $ show newscg

@@ -498,8 +498,9 @@ checkSizeChange n = do

498 ist <- get

499 case lookupCtxt Nothing n (idris_callgraph ist) of

500 [cg] -> do let ms = mkMultiPaths ist [] (scg cg)

501− logLvl 6 ("Multipath for " ++ show n ++ ":\n" ++

501+ logLvl 5 ("Multipath for " ++ show n ++ ":\n" ++

502 "from " ++ show (scg cg) ++ "\n" ++

503+ show (length ms) ++ "\n" ++

503 showSep "\n" (map show ms))

504 showSep "\n" (map show ms))

504 logLvl 6 (show cg)

505 logLvl 6 (show cg)

505 -- every multipath must have an infinitely descending

506 -- every multipath must have an infinitely descending

@@ -507,7 +508,8 @@ checkSizeChange n = do

507 -- also need to checks functions called are all total

508 -- also need to checks functions called are all total

508 -- (Unchecked is okay as we'll spot problems here)

509 -- (Unchecked is okay as we'll spot problems here)

509 let tot = map (checkMP ist (length (argsdef cg))) ms

510 let tot = map (checkMP ist (length (argsdef cg))) ms

511+ logLvl 4 $ "Generated " ++ show (length tot) ++ " paths"

510− logLvl 3 $ "Paths for " ++ show n ++ " yield " ++ (show tot)

512+ logLvl 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)

511 return (noPartial tot)

513 return (noPartial tot)

512 [] -> do logLvl 5 $ "No paths for " ++ show n

514 [] -> do logLvl 5 $ "No paths for " ++ show n

513 return Unchecked

515 return Unchecked

src/Idris/ElabTerm.hs+5−1

@@ -343,8 +343,12 @@ elab ist info pattern tcgen fn tm

343 ns <- apply (Var f) (map isph args)

344 ptm <- get_term

345 g <- goal

346+ let (ns', eargs) = unzip $

347+ sortBy (\(_,x) (_,y) ->

348+ compare (priority x) (priority y))

349+ (zip ns args)

346 elabArgs (ina || not isinf, guarded)

350 elabArgs (ina || not isinf, guarded)

347− [] False ns (map (\x -> (lazyarg x, getTm x)) args)

351+ [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

348 mkSpecialised ist fc f (map getTm args') tm

352 mkSpecialised ist fc f (map getTm args') tm

349 solve

353 solve

350 ptm <- get_term

354 ptm <- get_term