content: {-# LANGUAGE ImplicitParams, PatternGuards #-}
  
  module Termination where
  
  import Prelude hiding (null)
  
  import Control.Monad
  import Control.Monad.Writer (Writer, runWriter, mapWriter, tell, listen)
  
  import qualified Data.List as List
  import Data.Monoid
  #if !MIN_VERSION_base(4,8,0)
  import Data.Foldable (foldMap)
  #endif
  import Debug.Trace
  
  --import System
  
  import Abstract
  import TraceError
  import Util
  
  import Semiring
  import qualified SparseMatrix as M
  
  import TreeShapedOrder (TSO)
  import qualified TreeShapedOrder as TSO
  
  traceTerm :: String -> a -> a
  traceTerm msg a = a -- trace msg a
  
  traceTermM :: Monad m => String -> m ()
  traceTermM msg = return () -- traceM msg
  {-
  traceTerm msg a = trace msg a
  traceTermM msg = traceM msg
  -}
  
  
  traceProg :: String -> a -> a
  traceProg msg a =  a
  
  traceProgM :: Monad m => String -> m ()
  traceProgM msg = return ()
  {-
  traceProg msg a = trace msg a
  traceProgM msg = traceM msg
  -}
  
  -- cutoff:  How far can we count?
  -- cutoff = 0 : decrease of -infty,0,1 (original SCT)
  -- cutoff = 1 : "           -infty,-1,0,1,2
  -- etc.
  -- this is a parameter to the termination checker
  
  cutoff :: Int
  cutoff = 2  -- we can trace descend of 3, ascend of 2
  
  
  type Matrix a = M.Matrix Int a
  
  empty :: Matrix a
  empty = M.M (M.Size 0 0) []
  
  -- greater numbers shall mean more information for the term.checker.
  data Order = Decr Int -- positive numbers: decrease, neg. numbers: increase
             | Un       -- infinite increase (- infty)
             | Mat (Matrix Order) -- square matrices only (rows = call arguments, cols = parameters of caller)
             deriving (Show,Eq,Ord)
  
  instance HasZero Order where
    zeroElement = Un
  
  -- smart constructor
  orderMat :: Matrix Order -> Order
  orderMat m | M.isEmpty m                = Decr 0
             | Just o <- M.isSingleton m  = o
             | otherwise                  = Mat m
  {-
  orderMat []    = Decr 0   -- 0x0 Matrix = neutral element
  orderMat [[o]] = o        -- 1x1 Matrix
  orderMat oss   = Mat oss  -- nxn Matrix
  -}
  
  -- smart constructor
  decr :: (?cutoff :: Int) => Int -> Order
  decr i | i < - ?cutoff = Un
         | i > ?cutoff  = Decr (?cutoff + 1)
         | otherwise   = Decr i
  
  -- present order in terms of <,<=,?
  abstract :: Order -> Order
  abstract (Decr k) | k > 0 = Decr 1
                    | k == 0 = Decr 0
                    | k < 0  = Un
  abstract Un = Un
  abstract (Mat m) = Mat $ absCM m
  
  absCM :: Matrix Order -> Matrix Order
  absCM = fmap abstract
  -- absCM = map (map abstract)
  
  -- the one is never needed for matrix multiplication
  ordRing :: (?cutoff :: Int) => Semiring Order
  ordRing = Semiring { add = maxO , mul = comp , zero = Un } -- , one = Decr 0 }
  
  -- composition = sequence of calls
  comp :: (?cutoff :: Int) => Order -> Order -> Order
  comp _ Un = Un
  comp Un _ = Un
  comp (Decr k) (Decr l) = decr (k + l)
  comp (Mat m1) (Mat m2) = if (composable m1 m2) then
                               Mat $ M.mul ordRing m1 m2
                           else
                               comp (collapse m1) (collapse m2)
  comp (Decr 0) (Mat m) = Mat m
  comp (Mat m) (Decr 0) = Mat m
  comp o (Mat m) = comp o (collapse m)
  comp (Mat m) o = comp (collapse m) o
  
  maxO :: (?cutoff :: Int) => Order -> Order -> Order
  maxO o1 o2 = case (o1,o2) of
                 (Un,_) -> o2
                 (_,Un) -> o1
                 (Decr k, Decr l) -> Decr (max k l) -- cutoff not needed
                 (Mat m1, Mat m2) -> if (sameSize m1 m2) then
                                         Mat $ M.add maxO m1 m2
                                     else
                                         maxO (collapse m1) (collapse m2)
                 (Mat m1,_) -> maxO (collapse m1) o2
                 (_,Mat m2) -> maxO o1 (collapse m2)
  
  minO :: (?cutoff :: Int) => Order -> Order -> Order
  minO o1 o2 = case (o1,o2) of
                 (Un,_) -> Un
                 (_,Un) -> Un
                 (Decr k, Decr l) -> decr (min k l)
                 (Mat m1, Mat m2) -> if (sameSize m1 m2) then
                                         Mat $ minM m1 m2
                                     else
                                         minO (collapse m1) (collapse m2)
                 (Mat m1,_) -> minO (collapse m1) o2
                 (_,Mat m2) -> minO o1 (collapse m2)
  
  {-
  -- for non empty lists:
  minimumO :: (?cutoff :: Int) => [Order] -> Order
  minimumO = foldl1 minO
  -}
  
  -- | pointwise minimum
  minM :: (?cutoff :: Int) => Matrix Order -> Matrix Order -> Matrix Order
  minM = M.intersectWith minO
  {-
  minM m1 m2 = [ minV x y | (x,y) <- zip m1 m2]
   where
     minV :: Vector Order -> Vector Order -> Vector Order
     minV v1 v2 = [ minO x y | (x,y) <- zip v1 v2]
  -}
  
  maxL :: (?cutoff :: Int) => [Order] -> Order
  maxL = foldl1 maxO
  
  minL :: (?cutoff :: Int) => [Order] -> Order
  minL = foldl1 minO
  
  {- collapse m
  
  We assume that m codes a permutation:  each row has at most one column
  that is not Un.
  
  To collapse a matrix into a single value, we take the best value of
  each column and multiply them.  That means if one column is all Un,
  i.e., no argument relates to that parameter, than the collapsed value
  is also Un.
  
  This makes order multiplication associative.
  
  
  collapse :: (?cutoff :: Int) => Matrix Order -> Order
  collapse m = foldl1 comp (map maxL (M.transpose m))
  
  -}
  
  
  {- collapse m
  
  We assume that m codes a permutation:  each row has at most one column
  that is not Un.
  
  To collapse a matrix into a single value, we take the best value of
  each column and multiply them.  That means if one column is all Un,
  i.e., no argument relates to that parameter, than the collapsed value
  is also Un.
  
  This makes order multiplication associative.
  
  -}
  collapse :: (?cutoff :: Int) => Matrix Order -> Order
  collapse m = case M.toLists (M.transpose m) of
  --   [] -> __IMPOSSIBLE__   -- This can never happen if order matrices are generated by the smart constructor
     m' -> foldl1 comp $ map (foldl1 maxO) m'
  
  
  
  type Vector a = [a]
  type NaiveMatrix a = [Vector a]
  
  ---
  -- matrix stuff
  
  {-
  data Semiring a = Semiring { add :: (a -> a -> a) , mul :: (a -> a -> a) , one :: a , zero :: a }
  -}
  
  ssum :: Semiring a -> Vector a -> a
  ssum sem v = foldl (add sem) (zero sem) v
  
  vadd :: Semiring a -> Vector a -> Vector a -> Vector a
  vadd sem v1 v2 = [ (add sem) x y | (x,y) <- zip v1 v2]
  
  scalarProdukt :: Semiring a -> Vector a -> Vector a -> a
  scalarProdukt sem xs ys = ssum sem [(mul sem) x y  | (x,y) <- zip xs ys]
  
  madd :: Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a
  madd sem m1 m2 = [ vadd sem x y | (x,y) <- zip m1 m2]
  
  transp :: NaiveMatrix a -> NaiveMatrix a
  transp [] = []
  transp y = [[ z!!j | z<-y] | j<-[0..s]]
      where
      s = length (head y)-1
  
  mmul :: Show a => Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a
  mmul sem m1 m2 = let m =
                           [[scalarProdukt sem r c | c <- transp m2] | r<-m1 ]
                   in m
  diag :: NaiveMatrix a -> Vector a
  diag [] = []
  diag m = [ (m !! j) !! j | j <- [ 0..s] ]
     where
       s = length (head m) - 1
  
  elems :: NaiveMatrix a -> Vector a
  elems m = concat m
  
  {-
  ok :: Matrix a -> Matrix a -> Bool
  ok m1 m2 = (length m1) == length m2
  -}
  
  sameSize :: Matrix a -> Matrix a -> Bool
  sameSize m1 m2 = M.size m1 == M.size m2
  
  composable :: Matrix a -> Matrix a -> Bool
  composable m1 m2 = M.rows (M.size m1) == M.cols (M.size m2)
  
  ---
  
  -- create a call matrix
  -- each row is for one argument  of the callee
  -- each column for one parameter of the caller
  compareArgs :: (?cutoff :: Int) => TSO Name -> [Pattern] -> [Expr] -> Arity -> Matrix Order
  compareArgs tso _ [] _ = empty
  compareArgs tso [] _ _ = empty
  compareArgs tso pl el ar_g =
    M.fromLists (M.Size { M.rows = fullArity ar_g , M.cols = length pl }) $
      map (\ e -> map (\ p -> --traceTerm ("comparing " ++ show e ++ " to " ++ show p) $
                                      compareExpr tso e p) pl) el
  {-
  compareArgs tso pl el ar_g =
          let
              diff = ar_g - length el
              fill = if diff > 0 then
                         replicate diff (replicate (length pl) Un)
                     else []
              cmp = map (\ e -> (map (\ p -> --traceTerm ("comparing " ++ show e ++ " to " ++ show p) $
                                      compareExpr tso e p) pl)) el
          in
            cmp ++ fill
  -}
  
  {-
  compareExpr :: (?cutoff :: Int) => Expr -> Pattern -> Order
  compareExpr e p =
     case (e,p) of
        (_,UnusableP _) -> Un
        (_,DotP e') -> case exprToPattern e' of
                         Nothing -> if e == e' then Decr 0 else Un
                         Just p' -> compareExpr e p'
        (Var i,p) -> traceTerm ("compareVar " ++ show i ++ " " ++ show p) $ compareVar i p
        (App (Var i) _,p) -> compareVar i p
        (Con _ n1,ConP _ n2 [])  | n1 == n2 -> Decr 0
        (App (Con _ n1) [e1],ConP _ n2 [p1]) | n1 == n2 -> compareExpr e1 p1
        (App (Con _ n1) args,ConP _ n2 pl) | n1 == n2 && length args == length pl ->
                Mat (map (\ e -> (map (compareExpr e) pl)) args)
                -- without extended order :  minL $ zipWith compareExpr args pl
        (Succ e2,SuccP p2) -> compareExpr e2 p2
        -- new cases for counting constructors
        (Succ e2,p) -> Decr (-1) `comp` compareExpr e2 p
        (App (Con _ n1) args@(_:_), p) -> Decr (-1) `comp` minL (map (\e -> compareExpr e p) args)
        _ -> Un
  -}
  
  
  
  compareExpr :: (?cutoff :: Int) => TSO Name -> Expr -> Pattern -> Order
  compareExpr tso e p =
    let ret o = traceTerm ("comparing expression " ++ show e ++ " to pattern " ++ show p ++ " returns " ++ show o) o in
      ret $ compareExpr' tso e p
  
  compareExpr' :: (?cutoff :: Int) => TSO Name -> Expr -> Pattern -> Order
  compareExpr' tso (Ann e) p = compareExpr' tso (unTag e) p
  compareExpr' tso e p =
     case (conView $ spineView e, p) of
        (_,UnusableP _) -> Un
  --      (Erased e,_)    -> compareExpr' tso e p
        (_,ErasedP p)   -> compareExpr' tso e p
        (_,DotP e') -> case exprToPattern e' of
                         Nothing ->  if e == e' then Decr 0 else Un
                         Just p' -> compareExpr' tso e p'
        ((Var i,_), p) -> -- traceTerm ("compareVar " ++ show i ++ " " ++ show p) $
                           compareVar tso i p
  --      (Con _ n1,ConP _ n2 [])  | n1 == n2 -> Decr 0
  --      (App (Con _ n1) [e1],ConP _ n2 [p1]) | n1 == n2 -> compareExpr' tso e1 p1
        ((Def (DefId (ConK _) n1),args),ConP _ n2 pl) | n1 == n2 && length args == length pl ->
            let os = zipWith (compareExpr' tso) args pl
            in  trace ("compareExpr (con/con case): os = " ++ show os) $
                if null os then Decr 0 else minL os
  {- 2011-12-16 deactivate structured (matrix) orders
            orderMat $
              M.fromLists (M.Size { M.rows = length args, M.cols = length pl }) $
                 map (\ e -> map (compareExpr' tso e) pl) args
                -- without extended order :  minL $ zipWith compareExpr' tso args pl
  -}
        ((Succ e2,_),SuccP p2) ->  compareExpr' tso e2 p2
        -- new cases for counting constructors
        ((Succ e2,_),p) ->  Decr (-1) `comp` compareExpr' tso e2 p
        ((Def (DefId (ConK Cons) n1),args@(_:_)), p) ->  Decr (-1) `comp` minL (map (\e -> compareExpr' tso e p) args)
        ((Proj Post n1,[]), ProjP n2) | n1 == n2 -> Decr 0
        _ -> Un
  
  conView :: (Expr, [Expr]) -> (Expr, [Expr])
  conView (Record (NamedRec co n _ _) rs, es) = (Def (DefId (ConK co) n), map snd rs ++ es)
  conView p = p
  
  compareVar :: (?cutoff :: Int) => TSO Name -> Name -> Pattern -> Order
  compareVar tso n p =
    let ret o = o in -- traceTerm ("comparing variable " ++ n ++ " to " ++ show p ++ " returns " ++ show o) o in
      case p of
        UnusableP _ -> ret Un
        ErasedP p   -> compareVar tso n p
        VarP n2 -> if n == n2 then Decr 0 else
          case TSO.diff n n2 tso of -- if n2 is the k-th father of n, then it is a decrease by k
            Nothing -> ret Un
            Just k -> ret $ decr k
        SizeP n1 n2 -> if n == n2 then Decr 0 else
          case TSO.diff n n2 tso of -- if n2 is the k-th father of n, then it is a decrease by k
            Nothing -> ret Un
            Just k -> ret $ decr k
        PairP p1 p2 -> maxL (map (compareVar tso n) [p1,p2])
           -- no decrease in pair:  ALT: comp (Decr 1) (...)
        ConP pi c (p:pl) | coPat pi == Cons ->
          comp (Decr 1) (maxL (map (compareVar tso n) (p:pl)))
        ConP{}   -> ret Un
        ProjP{}  -> ret Un
        SuccP p2 -> comp (Decr 1) (compareVar tso n p2)
        DotP e -> case (exprToPattern e) of
                      Nothing -> ret $ Un
                      Just p' -> compareVar tso n p'
        _ -> error $ "NYI: compareVar " ++ show n ++ " to " ++ show p -- ret $ Un
  
  ---
  
  type Index = Name
  
  data Call = Call { source :: Index , target :: Index , matrix :: CallMatrix }
              deriving (Eq,Show,Ord)
  
  -- call matrix:
  -- each row is for one argument  of the callee (target)
  -- each column for one parameter of the caller (source)
  
  type CallMatrix = Matrix Order
  
  -- for two matrices m m' of the same dimensions,
  -- m `subsumes` m'  if  pointwise the entries of m are smaller than of m'
  subsumes :: Matrix Order -> Matrix Order -> Bool
  subsumes m m' = M.all (uncurry leq) mm'
    where mm' = M.zip m m' -- create one matrix of pairs
  {-
  subsumes m m' = all (all (uncurry leq)) mm'
    where mm' = zipWith zip m m' -- create one matrix of pairs
  -}
  
  -- Order forms itself a partial order
  leq :: Order -> Order -> Bool
  leq Un _ = True
  leq (Decr k) (Decr l) = k <= l
  leq (Mat m) (Mat m') = subsumes m m'
  leq _ _ = False
  
  -- for two matrices m m' such that m `subsumes` m'
  -- m `progress` m'  any positive entry in m' is smaller in m
  progress :: Matrix Order -> Matrix Order -> Bool
  progress m m' = M.any (uncurry decrToward0) mm'
    where mm' = M.zip m m' -- create one matrix of pairs
  {-
  progress m m' = any (any (uncurry decrToward0)) mm'
    where mm' = zipWith zip m m' -- create one matrix of pairs
  -}
  
  decrToward0 :: Order -> Order -> Bool
  decrToward0 Un (Decr l) = True && l >= 0
  decrToward0 (Decr k) (Decr l) = k < l  && l >= 0
  decrToward0 (Mat m) (Mat m') = progress m m'
  decrToward0 _ _ = False
  
  
  {- call pathes
  
    are lists of names of length >=2
  
    [f,g,h] = f --> g --> h
  -}
  
  newtype CallPath = CallPath { getCallPath :: [Name] } deriving Eq
  
  instance Show CallPath where
    show (CallPath [g]) = show g
    show (CallPath (f:l)) = show f ++ "-->" ++ show (CallPath l)
  
  emptyCP :: CallPath
  emptyCP = CallPath []
  
  mkCP :: Name -> Name -> CallPath
  mkCP src tgt = CallPath [src, tgt]
  
  mulCP :: CallPath -> CallPath -> CallPath
  mulCP cp1@(CallPath one) cp2@(CallPath (g:two)) =
    if last one == g then CallPath (one ++ two)
    else error ("internal error: Termination.mulCP: trying to compose callpath " ++ show cp1 ++ " with " ++ show cp2)
  
  compatibleCP :: CallPath -> CallPath -> Bool
  compatibleCP (CallPath one) (CallPath two) = head one == head two && last one == last two
  
  {-
  addCP :: CallPath -> CallPath -> CallPath
  addCP (CallPath []) cp = cp
  addCP cp (CallPath []) = cp
  addCP cp1 cp2 = if cp1 == cp2 then cp1 else error ("internal error: Termination.addCP: trying to blend non-equal callpathes " ++ show cp1 ++ " and " ++ show cp2)
  
  cpRing :: Semiring CallPath
  cpRing = Semiring { add = addCP , mul = mulCP , one = undefined , zero = emptyCP }
  -}
  
  -- composed calls
  
  type CompCall = (CallPath, CallMatrix)
  
  mulCC :: (?cutoff :: Int) => CompCall -> CompCall -> CompCall
  mulCC cc1@(cp1, m1) cc2@(cp2, m2) = zipPair mulCP (flip (M.mul ordRing)) cc1 cc2
  
  subsumesCC :: CompCall -> CompCall -> Bool
  subsumesCC cc1@(cp1, m1) cc2@(cp2, m2) =
    if compatibleCP cp1 cp2 then m1 `subsumes` m2
     else error ("internal error: Termination.subsumesCC: trying to compare composed call " ++ show cc2 ++ " with " ++ show cc1)
  
  progressCC :: CompCall -> CompCall -> Bool
  progressCC cc1@(cp1, m1) cc2@(cp2, m2) = progress m1 m2
  
  
  {- call graph completion
  
  organize call graph as a square matrix
  
    Name * Name -> Set CallMatrix
  
  the completion process finds new calls by composing old calls.
  There are two qualities of new calls.
  
    1) a completely new call or a call matrix in which one cell
       progressed from (Decr k | k > 0) towards -infty, i.e. a positive
       entry got smaller
  
    2) a negative entry got smaller
  
  As long as 1-calls are found, continue completion.
  [ I think 2-calls can be ignored when deciding whether to cont. ]
  
   -}
  
  -- sets of call matrices
  
  type CMSet    = [CompCall]  -- normal form: no CM subsumes another
  
  cmRing :: (?cutoff :: Int) => Semiring CMSet
  cmRing = Semiring { add = unionCMSet , mul = mulCMSet , zero = [] } -- one = undefined ,
  
  type Progress = Writer Any
  type ProgressH = Writer (Any, Any)
  
  firstHalf :: (Any, Any)
  firstHalf = (Any True, Any False)
  
  secondHalf :: (Any, Any)
  secondHalf = (Any False, Any True)
  
  -- we keep CMSets always in normal form
  -- progress reported if m is "better" than one of ms
  -- progress can only be reported if m is being added, i.e., not subsumed
  addCMh :: CompCall -> CMSet -> ProgressH CMSet
  addCMh m [] = traceProg ("adding new call " ++ show m) $ do
    tell firstHalf
    return $ [m]
  addCMh m (m':ms) =
    if m' `subsumesCC` m then traceTerm ("discarding new call " ++ show m) $
       return $ m':ms -- terminate early
     else do (ms', (Any h1, Any h2)) <- listen $ addCMh m ms
             when (h1 && not h2 && m `progressCC` m') $ do
               traceProgM ("progress made by " ++ show m ++ " over " ++ show m')
               tell secondHalf -- $ Any True
             if m `subsumesCC` m' then traceTerm ("discarding old call " ++ show m') $
                   return ms'
              else return $ m' : ms'
  
  addCM' :: CompCall -> CMSet -> Progress CMSet
  addCM' m ms = mapWriter (\(ms, (Any h1, Any h2)) -> (ms, Any $ h1 && h2)) (addCMh m ms)
  
  -- progress is reported if one of ms is "better" than ms'
  -- or if the oldset was empty and is no longer
  -- unionCMSet' addition oldset
  unionCMSet' :: CMSet -> CMSet -> Progress CMSet
  unionCMSet' [] []  = return []
  unionCMSet' ms []  = tell (Any True) >> return ms
  unionCMSet' ms ms' = foldM (flip addCM') ms' ms
  
  -- non-monadic versions
  addCM :: CompCall -> CMSet -> CMSet
  addCM m ms = fst $ runWriter (addCM' m ms)
  
  unionCMSet :: CMSet -> CMSet -> CMSet
  unionCMSet ms ms' = fst $ runWriter (unionCMSet' ms ms')
  
  mulCMSet :: (?cutoff :: Int) => CMSet -> CMSet -> CMSet
  mulCMSet ms ms' = foldl (flip addCM) [] $ [ mulCC m m' | m <- ms, m' <- ms' ]
  
  {- call graph entries
  
  type CGEntry = (CallPath, CMSet)
  
  cgeRing :: Semiring CGEntry
  cgeRing = Semiring { add = zipPair addCP unionCMSet,
                       mul = zipPair mulCP mulCMSet,
                       one = undefined,
                       zero = (emptyCP, []) }
  
  addCGEntry' :: CGEntry -> CGEntry -> Progress CGEntry
  addCGEntry' (cp1, ms1) (cp2, ms2) = do
    let cp = addCP cp1 cp2
    traceTermM ("call")
    ms <- unionCMSet' ms1 ms2
    return $ (cp, ms)
  -}
  
  -- call graphs
  
  type CallGraph = NaiveMatrix CMSet -- CGEntry
  
  stepCG :: (?cutoff :: Int) => CallGraph -> Progress CallGraph
  stepCG cg = do
    traceProgM ("next iteration")
    traceProgM ("old cg " ++ show cg)
    traceProgM ("composed calls " ++ show cg')
    traceProgM ("adding new calls to callgraph...")
    zipWithM (zipWithM unionCMSet') cg' cg
    where cg' = mmul cmRing cg cg
  
  {- "each idempotent call f->f has a decreasing arg" is an invariant
     of good call graphs.  Thus, we can stop call graph completion
     as soon as we see it violated.
  
     "idempotent" is defined on abstracted call matrices, i.e.,
     those that only have <, <=, ? and are not counting.
   -}
  complCGraph :: (?cutoff :: Int) => CallGraph -> CallGraph
  complCGraph cg =
    let (cg', Any prog) = runWriter $ stepCG cg
    in  if prog && checkAll cg' then complCGraph cg' else cg'
  
  checkAll :: (?cutoff :: Int) => CallGraph -> Bool
  checkAll cg = all (all (checkIdem . snd)) $ diag cg
  
  -- each idempotent call needs a decreasing diagonal entry
  checkIdem :: (?cutoff :: Int) => CallMatrix -> Bool
  checkIdem cm =
    let cm'   = M.mul ordRing cm cm
        eqAbs = (absCM cm) == (absCM cm')
        d     = M.diagonal cm
    in  traceTerm ("checkIdem: cm = " ++ show cm ++ " cm' = " ++ show cm ++ " eqAbs = " ++ show eqAbs ++ " d = " ++ show d) $
        -- if cm `subsumes` cm'
        if eqAbs
         then any isDecr d else True
  
  {- generate a call graph from a list of names and list of calls
  1. group calls by source, obtaining a list of row
  -}
  
  {- THIS IS WRONG:
  makeCG :: [Name] -> [Call] -> CallGraph
  makeCG names calls = map (\ tgt -> mkRow tgt [ c | c <- calls, target c == tgt ]) names
    where mkRow tgt calls = map (\ src ->  unionCMSet [ (mkCP src tgt, matrix c) | c <- calls, source c == src ] []) names
  -}
  
  makeCG :: [Name] -> [Call] -> CallGraph
  makeCG names calls = map (\ src -> mkRow src [ c | c <- calls, source c == src ]) names
    where mkRow src calls = map (\ tgt ->  unionCMSet [ (mkCP src tgt, matrix c) | c <- calls, target c == tgt ] []) names
  
  {-
  callComb :: Call -> Call -> Call
  callComb (Call s1 t1 m1) (Call s2 t2 m2) = Call s2 t1 (mmul ordRing m1 m2)
  
  cgComb :: [Call] -> [Call] -> [Call]
  cgComb cg1 cg2 = [ callComb c1 c2 | c1 <- cg1 , c2 <- cg2 , (source c1 == target c2)]
  
  complete :: [Call] -> [Call]
  complete cg = traceTerm ("call graph: " ++ show cg) $
    let cg' = complete' cg -- $ Set.fromList cg
    in -- traceTerm ("complete " ++ show cg')
         cg' -- Set.toList cg'
  
  complete' :: [Call] -> [Call]  -- Set Call -> Set Call
  complete' cg =
                let cgs = Set.fromList cg
                    cgs' = Set.union cgs (Set.fromList $ cgComb cg cg )
                    cg' = Set.toList cgs'
                in
                  if (cgs == cgs') then cg else complete' cg'
  
  checkAll :: [Call] -> Bool
  checkAll x = all checkIdem x
  
  -- each idempotent call needs a decreasing diagonal entry
  checkIdem :: Call -> Bool
  checkIdem c = let cc = callComb c c
                    d = diag (matrix cc)
                    containsDecr = any isDecr d
                in (not (c == cc)) || containsDecr
  -}
  isDecr :: Order -> Bool
  isDecr o = case o of
               (Decr k) -> k > 0
               (Mat m) -> any isDecr (M.diagonal m)
               _ -> False
  
  
  -------------------
  
  -- top level function
  terminationCheck :: MonadAssert m => [Fun] -> m ()
  terminationCheck funs = do
         let ?cutoff = cutoff
         traceTermM $ "terminationCheck " ++ show funs
         let tl = terminationCheckFuns funs
         let nl = map fst tl
         let bl = map snd tl
         let nl2 = [ n | (n,b) <- tl , b == False ]
         case (and bl) of
              True -> return ()
              False -> case nl of
                      [f] -> recoverFail ("Termination check for function " ++ show f ++ " fails ")
                      _   -> recoverFail ("Termination check for mutual block " ++ show nl ++ " fails for " ++ show nl2)
  
  
  terminationCheckFuns :: (?cutoff :: Int) => [Fun] -> [(Name,Bool)]
  terminationCheckFuns funs =
     let namar = map (\ (Fun (TypeSig n _) _ ar _) -> (n, ar)) funs
                 -- collectNames funs
         names = map fst namar
         cg0 = collectCGFunDecl namar funs
     in sizeChangeTermination names cg0
  
  sizeChangeTermination :: (?cutoff :: Int) => [Name] -> [Call] -> [(Name,Bool)]
  sizeChangeTermination names cg0 =
     let cg1 = makeCG names cg0
         cg = complCGraph $ cg1
         beh = zip names $ map (all (checkIdem . snd)) $ diag cg
     in traceTerm ("collected names: " ++ show names) $
        traceTerm ("call graph: " ++ show cg0) $
        traceTerm ("normalized call graph: " ++ show cg1) $
        traceTerm ("completed call graph: " ++ show cg) $
        traceTerm ("recursion behaviours" ++ show beh) $
        beh
  
  
  {-
  terminationCheckFuns :: [ (TypeSig,[Clause]) ] -> [(Name,Bool)]
  terminationCheckFuns funs =
      let beh = recBehaviours funs
      in
        traceTerm ("recursion behaviours" ++ show beh) $
          zip (map fst beh) (map (checkAll . snd ) beh )
  
  -- This is the main driver.
  recBehaviours :: [ (TypeSig,[Clause]) ] -> [(Name,[Call])]
  recBehaviours funs = let names = map fst $ collectNames funs
                           cg0 = collectCGFunDecl funs
                           cg = complete cg0
                       in traceTerm ("collected names: " ++ show names) $
                          traceTerm ("call graph: " ++ show cg0) $
                          groupCalls names [ c | c <- cg , (target c == source c) ]
  
  
  groupCalls :: [Name] -> [Call] -> [(Name,[Call])]
  groupCalls [] _ = []
  groupCalls (n:nl) cl = (n, [ c | c <- cl , (source c == n) ]) : groupCalls nl cl
  -}
  
  collectCGFunDecl :: (?cutoff :: Int) => [(Name,Arity)] -> [Fun] -> [Call]
  collectCGFunDecl names funs =
        concatMap (collectClauses names) funs
            where
              collectClauses :: [(Name,Arity)] -> Fun -> [Call]
              collectClauses names (Fun (TypeSig n _) _ ar cll) = collectClause names n cll
              collectClause :: [(Name,Arity)] -> Name -> [Clause] -> [Call]
              collectClause names n ((Clause _ pl Nothing):rest) = collectClause names n rest
              collectClause names n ((Clause _ pl (Just rhs)):rest) =
                traceTerm ("collecting calls in " ++ show rhs) $
                  (collectCallsExpr names n pl rhs) ++ (collectClause names n rest)
              collectClause names n [] = []
  
  -- | harvest i > j  from  case i { $ j -> ...}
  tsoCase :: TSO Name -> Expr -> [Clause] -> TSO Name
  tsoCase tso (Var x) [Clause _ [SuccP (VarP y)] _] = TSO.insert y (1,x) tso
  tsoCase tso _ _ = tso
  
  -- | harvest i < j  from (i < j) -> ... or (i < j) & ...
  tsoBind :: TSO Name -> TBind -> TSO Name
  tsoBind tso (TBind x (Domain (Below ltle (Var y)) _ _)) = TSO.insert x (n ltle,y) tso
    where n Lt = 1
          n Le = 0
  tsoBind tso _ = tso
  
  collectCallsExpr :: (?cutoff :: Int) => [(Name,Arity)] -> Name -> [Pattern] -> Expr -> [Call]
  collectCallsExpr nl f pl e = traceTerm ("collectCallsExpr " ++ show e) $
    loop tso e where
      tso = tsoFromPatterns pl
      loop tso (Ann e) = loop tso (unTag e)
      loop tso e = headcalls ++ argcalls where
        (hd, args) = spineView e -- $ ignoreTopErasure e
        argcalls = concatMap (loop tso) args
        headcalls = case hd of
            (Def (DefId FunK (QName g))) ->
                case lookup g nl of
                  Nothing -> []
                  Just ar_g ->
                    traceTerm ("found call from " ++ show f ++ " to " ++ show g) $
                               let (Just ar_f) = lookup f nl
                                   (Just f') = List.elemIndex (f,ar_f) nl
                                   (Just g') = List.elemIndex (g,ar_g) nl
                                   m = compareArgs tso pl args ar_g
                                   cg = Call { source = f
                                             , target = g
                                             , matrix = m }
                               in
                                 traceTerm ("found call " ++ show cg) $
                                   [cg]
            (Case e _ cls) -> loop tso e ++ concatMap (loop (tsoCase tso e cls)) (map (maybe Irr id . clExpr) cls)
            (Lam _ _ e1) -> loop tso e1
            (LLet tb tel e1 e2) | null tel->
               (loop tso e1) ++ -- type won't get evaluated
               (loop tso e2)
            (Quant _ tb@(TBind x dom) e2) -> (loop tso (typ dom)) ++ (loop (tsoBind tso tb) e2)
            (Quant _ (TMeasure mu) e2) -> foldMap (loop tso) mu ++ (loop tso e2)
            (Quant _ (TBound beta) e2) -> foldMap (loop tso) beta ++ (loop tso e2)
            (Below ltle e) -> loop tso e
            (Sing e1 e2) -> (loop tso e1) ++ (loop tso e2)
            (Pair e1 e2) -> (loop tso e1) ++ (loop tso e2)
            (Succ e) -> loop tso e
            (Max es) -> concatMap (loop tso) es
            (Plus es) -> concatMap (loop tso) es
            Sort (SortC{})  -> []
            Sort (Set e)    -> loop tso e
            Sort (CoSet e)  -> loop tso e
            Var{}   -> []
            Zero{} -> []
            Infty{} -> []
            Def{}   -> []
            Irr{}   -> []
            Proj{}   -> []
            Record ri rs -> foldMap (loop tso . snd) rs
            Ann e1 -> loop tso (unTag e1)
  --          Con{}   -> []
  --          Let{}   -> []
            Meta{}  -> error $ "collect calls in unresolved meta variable " ++ show e
            _ -> error $ "NYI: collect calls in " ++ show e
  
  {-
  collectCallsExpr :: (?cutoff :: Int) => [(Name,Int)] -> Name -> [Pattern] -> Expr -> [Call]
  collectCallsExpr nl f pl e =
    traceTerm ("collectCallsExpr " ++ show e) $
      case e of
        (App (Def g) args) ->
          let calls = concatMap (collectCallsExpr nl f pl) args
              gIn = lookup g nl
          in
           traceTerm ("found call from " ++ f ++ " to " ++ g) $
            case gIn of
              Nothing -> calls
              Just ar_g -> let (Just ar_f) = lookup f nl
                               (Just f') = List.elemIndex (f,ar_f) nl
                               (Just g') = List.elemIndex (g,ar_g) nl
                               m = compareArgs pl args ar_g
                               cg = Call { source = f
                                         , target = g
                                         , matrix = m }
                           in
                             traceTerm ("found call " ++ show cg) $
                               cg:calls
        (Def g) ->  collectCallsExpr nl f pl (App (Def g) [])
        (App e args) -> concatMap (collectCallsExpr nl f pl) (e:args)
        (Case e cls) -> concatMap (collectCallsExpr nl f pl) (e:map clExpr cls)
        (Lam _ _ e1) -> collectCallsExpr nl f pl e1
        (LLet _ e1 t1 e2) ->  (collectCallsExpr nl f pl e1) ++ -- type won't get evaluated
                              (collectCallsExpr nl f pl e2)
        (Pi _ _ e1 e2) -> (collectCallsExpr nl f pl e1) ++
                                (collectCallsExpr nl f pl e2)
        (Sing e1 e2) -> (collectCallsExpr nl f pl e1) ++
                                (collectCallsExpr nl f pl e2)
        (Succ e1) -> collectCallsExpr nl f pl e1
        Sort{}  -> []
        Var{}   -> []
        Infty{} -> []
        Con{}   -> []
        Let{}   -> []
        Meta{}  -> error $ "collect calls in unresolved meta variable " ++ show e
        _ -> error $ "NYI: collect calls in " ++ show e
  -}
  
  ----------------------------------------------------------------------
  {- Foetus II - Counting Lexicographic Termination (delta-Foetus)
  
  delta-SCT [Ben-Amram 2006] is too inefficient, at least with the bound
  given in the paper.
  
    B(G) = (k + 1)2^k · m^2 · 2^(2k+1) (m∆)^(3k+1) (k + 1)^(3k^2+3k+1)
  
  is an upper bound on the length of the longest path to be looked at to
  exclude non-termination.
  
  I guess that both argument permutation and counting is not very
  common.  So an approach would be
  
  - try to show termination with SCT
  - try to show termination with delta-Foetus
  
  Call graph completion in delta-Foetus
  
  1. Iterate as long new simple cycles show up (i.e. cycles with no subcycles)
  
  2. Find the possible lexicographic termination orders to for each function
  
  3. Continue iterating while any of the arguments involved in any of the termination orders gets worse.  Some termination order hypotheses might collapse.
  
  4. Stop when all hypotheses have collapsed (FAIL) or when no standing hypotheses gets any worse (SUCCESS).
  
  Implementation:
  
  After 1. save for each function and each of its arguments the worst
  recursive behavior in any of the calls.  This map will be used to
  monitor progress.
  
  
  Careful:
  
    f x = f (x-1) | g (x - 100)
    g x = g (x+1) | f (x - 100)
  
  Bad call f->f only found after 201 iterations of g!
  
  Idea:  regular expressions over call matrices!
  
    (m1 + m2^*)^*
  
  -}
  