@@ -311,15 +311,85 @@ buildSCG (_, n) = do
311311 ist <- getIState
312312 case lookupCtxt n (idris_callgraph ist) of
313313 [cg] -> case lookupDef n (tt_ctxt ist) of
314− [CaseOp _ _ _ _ _ args sc _ _] ->
315− do logLvl 3 $ "Building SCG for " ++ show n ++ " from\n"
316− ++ show sc
317− let newscg = buildSCG' ist sc args
314+ [CaseOp _ _ _ pats _ args sc _ _] ->
315+ do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
316+ ++ show pats ++ "\n" ++ show sc
317+ let newscg = buildSCG' ist (rights pats) args
318318 logLvl 5 $ show newscg
319319 addToCG n ( cg { scg = newscg } )
320320 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
321321 x -> error $ "buildSCG: " ++ show (n, x)
322322
323+buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
324+buildSCG' ist pats args = nub $ concatMap scgPat pats where
325+ scgPat (lhs, rhs) = let (f, pargs) = unApply (dePat lhs) in
326+ findCalls (dePat rhs) (patvars lhs) pargs
327+
328+ findCalls ap@(App f a) pvs pargs
329+ | (P _ (UN "lazy") _, [_, arg]) <- unApply ap
330+ = findCalls arg pvs pargs
331+ | (P _ n _, args) <- unApply ap
332+ = mkChange n args pargs ++
333+ concatMap (\x -> findCalls x pvs pargs) args
334+ findCalls (App f a) pvs pargs
335+ = findCalls f pvs pargs ++ findCalls a pvs pargs
336+ findCalls (Bind n (Let t v) e) pvs pargs
337+ = findCalls v pvs pargs ++ findCalls e (n : pvs) pargs
338+ findCalls (Bind n _ e) pvs pargs
339+ = findCalls e (n : pvs) pargs
340+ findCalls (P _ f _ ) pvs pargs
341+ | not (f `elem` pvs) = [(f, [])]
342+ findCalls _ _ _ = []
343+
344+ mkChange n args pargs = [(n, sizes args)]
345+ where
346+ sizes [] = []
347+ sizes (a : as) = checkSize a pargs 0 : sizes as
348+
349+ -- find which argument in pargs <a> is smaller than, if any
350+ checkSize a (p : ps) i
351+ | a == p = Just (i, Same)
352+ | smaller Nothing a (p, Nothing) = Just (i, Smaller)
353+ | otherwise = checkSize a ps (i + 1)
354+ checkSize a [] i = Nothing
355+
356+ -- the smaller thing we find must be the same type as <a>, and
357+ -- not be coinductive - so carry the type of the constructor we've
358+ -- gone under.
359+
360+ smaller (Just tyn) a (t, Just tyt)
361+ | a == t = isInductive (fst (unApply (getRetTy tyn)))
362+ (fst (unApply (getRetTy tyt)))
363+ smaller ty a (ap@(App f s), _)
364+ | (P (DCon _ _) n _, args) <- unApply ap
365+ = let tyn = getType n in
366+ any (smaller (ty `mplus` Just tyn) a)
367+ (zip args (map toJust (getArgTys tyn)))
368+ -- check higher order recursive arguments
369+ smaller ty (App f s) a = smaller ty f a
370+ smaller _ _ _ = False
371+
372+ toJust (n, t) = Just t
373+
374+ getType n = case lookupTy n (tt_ctxt ist) of
375+ [ty] -> ty -- must exist
376+
377+ isInductive (P _ nty _) (P _ nty' _) =
378+ let co = case lookupCtxt nty (idris_datatypes ist) of
379+ [TI _ x _] -> x
380+ _ -> False in
381+ nty == nty' && not co
382+ isInductive _ _ = False
383+
384+-- getTypeFam t | (P _ n _, _) <- unApply t
385+
386+ dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)
387+ dePat t = t
388+
389+ patvars (Bind x (PVar _) sc) = x : patvars sc
390+ patvars _ = []
391+
392+{-
323393buildSCG' :: IState -> SC -> [Name] -> [SCGEntry]
324394buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
325395 nub $ scg sc (zip args args)
@@ -406,6 +476,7 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
406476 getArgPos i n [] = Nothing
407477 getArgPos i n (x : xs) | n == x = Just i
408478 | otherwise = getArgPos (i + 1) n xs
479+-}
409480
410481checkSizeChange :: Name -> Idris Totality
411482checkSizeChange n = do