003b68c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better path generation in termination checker

003b68cEdwin Brady10 years ago

libs/base/System/Concurrency/Raw.idr−2

@@ -1,5 +1,3 @@

1−-- WARNING: No guarantees that this works properly yet!

2−

3module System.Concurrency.Raw

1module System.Concurrency.Raw

5-- Raw (i.e. not type safe) message passing

3-- Raw (i.e. not type safe) message passing

src/Idris/Coverage.hs+12−1

@@ -779,13 +779,24 @@ mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]

779mkMultiPaths ist path [] = [reverse path]

780mkMultiPaths ist path cg = concatMap extend cg

781 where extend (nextf, args)

782− | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]

782+ | (nextf, args) `inPath` path = [ reverse ((nextf, args) : path) ]

783 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)

784 = case lookupCtxt nextf (idris_callgraph ist) of

785 [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)

786 _ -> [ reverse ((nextf, args) : path) ]

787 | otherwise = [ reverse ((nextf, args) : path) ]

788

789+ inPath :: SCGEntry -> [SCGEntry] -> Bool

790+ inPath f [] = False

791+ inPath f (g : gs) = smallerEq f g || f == g || inPath f gs

792+

793+ smallerEq :: SCGEntry -> SCGEntry -> Bool

794+ smallerEq (f, args) (g, args')

795+ = f == g && not (null (filter smallers args))

796+ && filter smallers args == filter smallers args'

797+ smallers (Just (_, Smaller)) = True

798+ smallers _ = False

799+

789-- If any route along the multipath leads to infinite descent, we're fine.

800-- If any route along the multipath leads to infinite descent, we're fine.

790-- Try a route beginning with every argument.

801-- Try a route beginning with every argument.

791-- If we reach a point we've been to before, but with a smaller value,

802-- If we reach a point we've been to before, but with a smaller value,