git.iko.soy/Idris-dev
on master help sign in
Speed up termination checker
4c45c09Edwin Brady
lib/Prelude.idr+3
compare with master
unifiedsplit
@@ -247,6 +247,9 @@ getChar = mkForeign (FFun "getchar" [] FChar)
247abstract
247abstract
248data File = FHandle Ptr
248data File = FHandle Ptr
249
249
250+partial stdin : File
251+stdin = FHandle prim__stdin
252+
250do_fopen : String -> String -> IO Ptr
253do_fopen : String -> String -> IO Ptr
251do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
254do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
252
255
src/Idris/Coverage.hs+11−3
@@ -522,10 +522,11 @@ mkMultiPaths ist path cg
522 = concat (map extend cg)
522 = concat (map extend cg)
523 where extend (nextf, args)
523 where extend (nextf, args)
524 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
524 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]
525− | otherwise
525+ | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)
526 = case lookupCtxt Nothing nextf (idris_callgraph ist) of
526 = case lookupCtxt Nothing nextf (idris_callgraph ist) of
527 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
527 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)
528 _ -> [ reverse ((nextf, args) : path) ]
528 _ -> [ reverse ((nextf, args) : path) ]
529+ | otherwise = [ reverse ((nextf, args) : path) ]
529
530
530-- do (nextf, args) <- cg
531-- do (nextf, args) <- cg
531-- if ((nextf, args) `elem` path)
532-- if ((nextf, args) `elem` path)
@@ -571,7 +572,7 @@ checkMP ist i mp = if i > 0
571 Total []
572 Total []
572 else Partial (Mutual (map (fst . fst) path ++ [f]))
573 else Partial (Mutual (map (fst . fst) path ++ [f]))
573 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
574 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =
574− let argspos = zip nextargs [0..] in
575+ let argspos = collapseNothing (zip nextargs [0..]) in
575 collapse' Unchecked $
576 collapse' Unchecked $
576 do (a, pos) <- argspos
577 do (a, pos) <- argspos
577 case a of
578 case a of
@@ -595,10 +596,17 @@ checkMP ist i mp = if i > 0
595 _ -> trace ("Shouldn't happen " ++ show e) $
596 _ -> trace ("Shouldn't happen " ++ show e) $
596 return (Partial Itself)
597 return (Partial Itself)
597 else return Unchecked
598 else return Unchecked
598− | [Total _] <- lookupTotal f (tt_ctxt ist) = Unchecked
599+ | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
599 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
600 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
600 | otherwise = Unchecked
601 | otherwise = Unchecked
601
602
603+collapseNothing ((Nothing, _) : xs)
604+ = filter (\ (x, _) -> case x of
605+ Nothing -> False
606+ _ -> True) xs
607+collapseNothing (x : xs) = x : collapseNothing xs
608+collapseNothing [] = []
609+
602noPartial (Partial p : xs) = Partial p
610noPartial (Partial p : xs) = Partial p
603noPartial (_ : xs) = noPartial xs
611noPartial (_ : xs) = noPartial xs
604noPartial [] = Total []
612noPartial [] = Total []