{-# 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 :: forall a. String -> a -> a
traceTerm String
msg a
a = a
a -- trace msg a

traceTermM :: Monad m => String -> m ()
traceTermM :: forall (m :: * -> *). Monad m => String -> m ()
traceTermM String
msg = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- traceM msg
{-
traceTerm msg a = trace msg a
traceTermM msg = traceM msg
-}


traceProg :: String -> a -> a
traceProg :: forall a. String -> a -> a
traceProg String
msg a
a =  a
a

traceProgM :: Monad m => String -> m ()
traceProgM :: forall (m :: * -> *). Monad m => String -> m ()
traceProgM String
msg = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
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 :: Int
cutoff = Int
2  -- we can trace descend of 3, ascend of 2


type Matrix a = M.Matrix Int a

empty :: Matrix a
empty :: forall a. Matrix a
empty = Size Int -> [(MIx Int, a)] -> Matrix Int a
forall i b. Size i -> [(MIx i, b)] -> Matrix i b
M.M (Int -> Int -> Size Int
forall i. i -> i -> Size i
M.Size Int
0 Int
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 (Int -> Order -> ShowS
[Order] -> ShowS
Order -> String
(Int -> Order -> ShowS)
-> (Order -> String) -> ([Order] -> ShowS) -> Show Order
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Order -> ShowS
showsPrec :: Int -> Order -> ShowS
$cshow :: Order -> String
show :: Order -> String
$cshowList :: [Order] -> ShowS
showList :: [Order] -> ShowS
Show,Order -> Order -> Bool
(Order -> Order -> Bool) -> (Order -> Order -> Bool) -> Eq Order
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Order -> Order -> Bool
== :: Order -> Order -> Bool
$c/= :: Order -> Order -> Bool
/= :: Order -> Order -> Bool
Eq,Eq Order
Eq Order =>
(Order -> Order -> Ordering)
-> (Order -> Order -> Bool)
-> (Order -> Order -> Bool)
-> (Order -> Order -> Bool)
-> (Order -> Order -> Bool)
-> (Order -> Order -> Order)
-> (Order -> Order -> Order)
-> Ord Order
Order -> Order -> Bool
Order -> Order -> Ordering
Order -> Order -> Order
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Order -> Order -> Ordering
compare :: Order -> Order -> Ordering
$c< :: Order -> Order -> Bool
< :: Order -> Order -> Bool
$c<= :: Order -> Order -> Bool
<= :: Order -> Order -> Bool
$c> :: Order -> Order -> Bool
> :: Order -> Order -> Bool
$c>= :: Order -> Order -> Bool
>= :: Order -> Order -> Bool
$cmax :: Order -> Order -> Order
max :: Order -> Order -> Order
$cmin :: Order -> Order -> Order
min :: Order -> Order -> Order
Ord)

instance HasZero Order where
  zeroElement :: Order
zeroElement = Order
Un

-- smart constructor
orderMat :: Matrix Order -> Order
orderMat :: Matrix Int Order -> Order
orderMat Matrix Int Order
m | Matrix Int Order -> Bool
forall i b. (Num i, Ix i) => Matrix i b -> Bool
M.isEmpty Matrix Int Order
m                = Int -> Order
Decr Int
0
           | Just Order
o <- Matrix Int Order -> Maybe Order
forall i b. (Num i, Ix i, HasZero b) => Matrix i b -> Maybe b
M.isSingleton Matrix Int Order
m  = Order
o
           | Bool
otherwise                  = Matrix Int Order -> Order
Mat Matrix Int Order
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 :: (?cutoff::Int) => Int -> Order
decr Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< - ?cutoff::Int
Int
?cutoff = Order
Un
       | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> ?cutoff::Int
Int
?cutoff  = Int -> Order
Decr (?cutoff::Int
Int
?cutoff Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
       | Bool
otherwise   = Int -> Order
Decr Int
i

-- present order in terms of <,<=,?
abstract :: Order -> Order
abstract :: Order -> Order
abstract (Decr Int
k) | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Int -> Order
Decr Int
1
                  | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Int -> Order
Decr Int
0
                  | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0  = Order
Un
abstract Order
Un = Order
Un
abstract (Mat Matrix Int Order
m) = Matrix Int Order -> Order
Mat (Matrix Int Order -> Order) -> Matrix Int Order -> Order
forall a b. (a -> b) -> a -> b
$ Matrix Int Order -> Matrix Int Order
absCM Matrix Int Order
m

absCM :: Matrix Order -> Matrix Order
absCM :: Matrix Int Order -> Matrix Int Order
absCM = (Order -> Order) -> Matrix Int Order -> Matrix Int Order
forall a b. (a -> b) -> Matrix Int a -> Matrix Int b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Order -> Order
abstract
-- absCM = map (map abstract)

-- the one is never needed for matrix multiplication
ordRing :: (?cutoff :: Int) => Semiring Order
ordRing :: (?cutoff::Int) => Semiring Order
ordRing = Semiring { add :: Order -> Order -> Order
add = (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
maxO , mul :: Order -> Order -> Order
mul = (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
comp , zero :: Order
zero = Order
Un } -- , one = Decr 0 }

-- composition = sequence of calls
comp :: (?cutoff :: Int) => Order -> Order -> Order
comp :: (?cutoff::Int) => Order -> Order -> Order
comp Order
_ Order
Un = Order
Un
comp Order
Un Order
_ = Order
Un
comp (Decr Int
k) (Decr Int
l) = (?cutoff::Int) => Int -> Order
Int -> Order
decr (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l)
comp (Mat Matrix Int Order
m1) (Mat Matrix Int Order
m2) = if (Matrix Int Order -> Matrix Int Order -> Bool
forall a. Matrix a -> Matrix a -> Bool
composable Matrix Int Order
m1 Matrix Int Order
m2) then
                             Matrix Int Order -> Order
Mat (Matrix Int Order -> Order) -> Matrix Int Order -> Order
forall a b. (a -> b) -> a -> b
$ Semiring Order
-> Matrix Int Order -> Matrix Int Order -> Matrix Int Order
forall i a.
(Enum i, Num i, Ix i, Eq a) =>
Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
M.mul Semiring Order
(?cutoff::Int) => Semiring Order
ordRing Matrix Int Order
m1 Matrix Int Order
m2
                         else
                             (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
comp ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m1) ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m2)
comp (Decr Int
0) (Mat Matrix Int Order
m) = Matrix Int Order -> Order
Mat Matrix Int Order
m
comp (Mat Matrix Int Order
m) (Decr Int
0) = Matrix Int Order -> Order
Mat Matrix Int Order
m
comp Order
o (Mat Matrix Int Order
m) = (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
comp Order
o ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m)
comp (Mat Matrix Int Order
m) Order
o = (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
comp ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m) Order
o

maxO :: (?cutoff :: Int) => Order -> Order -> Order
maxO :: (?cutoff::Int) => Order -> Order -> Order
maxO Order
o1 Order
o2 = case (Order
o1,Order
o2) of
               (Order
Un,Order
_) -> Order
o2
               (Order
_,Order
Un) -> Order
o1
               (Decr Int
k, Decr Int
l) -> Int -> Order
Decr (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
k Int
l) -- cutoff not needed
               (Mat Matrix Int Order
m1, Mat Matrix Int Order
m2) -> if (Matrix Int Order -> Matrix Int Order -> Bool
forall a. Matrix a -> Matrix a -> Bool
sameSize Matrix Int Order
m1 Matrix Int Order
m2) then
                                       Matrix Int Order -> Order
Mat (Matrix Int Order -> Order) -> Matrix Int Order -> Order
forall a b. (a -> b) -> a -> b
$ (Order -> Order -> Order)
-> Matrix Int Order -> Matrix Int Order -> Matrix Int Order
forall i a.
Ord i =>
(a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
M.add (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
maxO Matrix Int Order
m1 Matrix Int Order
m2
                                   else
                                       (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
maxO ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m1) ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m2)
               (Mat Matrix Int Order
m1,Order
_) -> (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
maxO ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m1) Order
o2
               (Order
_,Mat Matrix Int Order
m2) -> (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
maxO Order
o1 ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m2)

minO :: (?cutoff :: Int) => Order -> Order -> Order
minO :: (?cutoff::Int) => Order -> Order -> Order
minO Order
o1 Order
o2 = case (Order
o1,Order
o2) of
               (Order
Un,Order
_) -> Order
Un
               (Order
_,Order
Un) -> Order
Un
               (Decr Int
k, Decr Int
l) -> (?cutoff::Int) => Int -> Order
Int -> Order
decr (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
k Int
l)
               (Mat Matrix Int Order
m1, Mat Matrix Int Order
m2) -> if (Matrix Int Order -> Matrix Int Order -> Bool
forall a. Matrix a -> Matrix a -> Bool
sameSize Matrix Int Order
m1 Matrix Int Order
m2) then
                                       Matrix Int Order -> Order
Mat (Matrix Int Order -> Order) -> Matrix Int Order -> Order
forall a b. (a -> b) -> a -> b
$ (?cutoff::Int) =>
Matrix Int Order -> Matrix Int Order -> Matrix Int Order
Matrix Int Order -> Matrix Int Order -> Matrix Int Order
minM Matrix Int Order
m1 Matrix Int Order
m2
                                   else
                                       (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
minO ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m1) ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m2)
               (Mat Matrix Int Order
m1,Order
_) -> (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
minO ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m1) Order
o2
               (Order
_,Mat Matrix Int Order
m2) -> (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
minO Order
o1 ((?cutoff::Int) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
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 :: (?cutoff::Int) =>
Matrix Int Order -> Matrix Int Order -> Matrix Int Order
minM = (Order -> Order -> Order)
-> Matrix Int Order -> Matrix Int Order -> Matrix Int Order
forall i a.
Ord i =>
(a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
M.intersectWith (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
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 :: (?cutoff::Int) => [Order] -> Order
maxL = (Order -> Order -> Order) -> [Order] -> Order
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
maxO

minL :: (?cutoff :: Int) => [Order] -> Order
minL :: (?cutoff::Int) => [Order] -> Order
minL = (Order -> Order -> Order) -> [Order] -> Order
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
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 :: (?cutoff::Int) => Matrix Int Order -> Order
collapse Matrix Int Order
m = case Matrix Int Order -> [[Order]]
forall i b.
(Ord i, Integral i, Enum i, HasZero b, Show i) =>
Matrix i b -> [[b]]
M.toLists (Matrix Int Order -> Matrix Int Order
forall i b. Ord i => Matrix i b -> Matrix i b
M.transpose Matrix Int Order
m) of
--   [] -> __IMPOSSIBLE__   -- This can never happen if order matrices are generated by the smart constructor
   [[Order]]
m' -> (Order -> Order -> Order) -> [Order] -> Order
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
comp ([Order] -> Order) -> [Order] -> Order
forall a b. (a -> b) -> a -> b
$ ([Order] -> Order) -> [[Order]] -> [Order]
forall a b. (a -> b) -> [a] -> [b]
map ((Order -> Order -> Order) -> [Order] -> Order
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
maxO) [[Order]]
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 :: forall a. Semiring a -> Vector a -> a
ssum Semiring a
sem Vector a
v = (a -> a -> a) -> a -> Vector a -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Semiring a -> a -> a -> a
forall a. Semiring a -> a -> a -> a
add Semiring a
sem) (Semiring a -> a
forall a. Semiring a -> a
zero Semiring a
sem) Vector a
v

vadd :: Semiring a -> Vector a -> Vector a -> Vector a
vadd :: forall a. Semiring a -> Vector a -> Vector a -> Vector a
vadd Semiring a
sem Vector a
v1 Vector a
v2 = [ (Semiring a -> a -> a -> a
forall a. Semiring a -> a -> a -> a
add Semiring a
sem) a
x a
y | (a
x,a
y) <- Vector a -> Vector a -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip Vector a
v1 Vector a
v2]

scalarProdukt :: Semiring a -> Vector a -> Vector a -> a
scalarProdukt :: forall a. Semiring a -> Vector a -> Vector a -> a
scalarProdukt Semiring a
sem Vector a
xs Vector a
ys = Semiring a -> Vector a -> a
forall a. Semiring a -> Vector a -> a
ssum Semiring a
sem [(Semiring a -> a -> a -> a
forall a. Semiring a -> a -> a -> a
mul Semiring a
sem) a
x a
y  | (a
x,a
y) <- Vector a -> Vector a -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip Vector a
xs Vector a
ys]

madd :: Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a
madd :: forall a.
Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a
madd Semiring a
sem NaiveMatrix a
m1 NaiveMatrix a
m2 = [ Semiring a -> Vector a -> Vector a -> Vector a
forall a. Semiring a -> Vector a -> Vector a -> Vector a
vadd Semiring a
sem Vector a
x Vector a
y | (Vector a
x,Vector a
y) <- NaiveMatrix a -> NaiveMatrix a -> [(Vector a, Vector a)]
forall a b. [a] -> [b] -> [(a, b)]
zip NaiveMatrix a
m1 NaiveMatrix a
m2]

transp :: NaiveMatrix a -> NaiveMatrix a
transp :: forall a. NaiveMatrix a -> NaiveMatrix a
transp [] = []
transp [Vector a]
y = [[ Vector a
zVector a -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!!Int
j | Vector a
z<-[Vector a]
y] | Int
j<-[Int
0..Int
s]]
    where
    s :: Int
s = Vector a -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Vector a] -> Vector a
forall a. HasCallStack => [a] -> a
head [Vector a]
y)Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1

mmul :: Show a => Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a
mmul :: forall a.
Show a =>
Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a
mmul Semiring a
sem NaiveMatrix a
m1 NaiveMatrix a
m2 = let m :: NaiveMatrix a
m =
                         [[Semiring a -> [a] -> [a] -> a
forall a. Semiring a -> Vector a -> Vector a -> a
scalarProdukt Semiring a
sem [a]
r [a]
c | [a]
c <- NaiveMatrix a -> NaiveMatrix a
forall a. NaiveMatrix a -> NaiveMatrix a
transp NaiveMatrix a
m2] | [a]
r<-NaiveMatrix a
m1 ]
                 in NaiveMatrix a
m
diag :: NaiveMatrix a -> Vector a
diag :: forall a. NaiveMatrix a -> Vector a
diag [] = []
diag [Vector a]
m = [ ([Vector a]
m [Vector a] -> Int -> Vector a
forall a. HasCallStack => [a] -> Int -> a
!! Int
j) Vector a -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
j | Int
j <- [ Int
0..Int
s] ]
   where
     s :: Int
s = Vector a -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Vector a] -> Vector a
forall a. HasCallStack => [a] -> a
head [Vector a]
m) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

elems :: NaiveMatrix a -> Vector a
elems :: forall a. NaiveMatrix a -> Vector a
elems NaiveMatrix a
m = NaiveMatrix a -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat NaiveMatrix a
m

{-
ok :: Matrix a -> Matrix a -> Bool
ok m1 m2 = (length m1) == length m2
-}

sameSize :: Matrix a -> Matrix a -> Bool
sameSize :: forall a. Matrix a -> Matrix a -> Bool
sameSize Matrix a
m1 Matrix a
m2 = Matrix a -> Size Int
forall i b. Matrix i b -> Size i
M.size Matrix a
m1 Size Int -> Size Int -> Bool
forall a. Eq a => a -> a -> Bool
== Matrix a -> Size Int
forall i b. Matrix i b -> Size i
M.size Matrix a
m2

composable :: Matrix a -> Matrix a -> Bool
composable :: forall a. Matrix a -> Matrix a -> Bool
composable Matrix a
m1 Matrix a
m2 = Size Int -> Int
forall i. Size i -> i
M.rows (Matrix a -> Size Int
forall i b. Matrix i b -> Size i
M.size Matrix a
m1) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Size Int -> Int
forall i. Size i -> i
M.cols (Matrix a -> Size Int
forall i b. Matrix i b -> Size i
M.size Matrix a
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 :: (?cutoff::Int) =>
TSO Name -> [Pattern] -> [Expr] -> Arity -> Matrix Int Order
compareArgs TSO Name
tso [Pattern]
_ [] Arity
_ = Matrix Int Order
forall a. Matrix a
empty
compareArgs TSO Name
tso [] [Expr]
_ Arity
_ = Matrix Int Order
forall a. Matrix a
empty
compareArgs TSO Name
tso [Pattern]
pl [Expr]
el Arity
ar_g =
  Size Int -> [[Order]] -> Matrix Int Order
forall i b.
(Ord i, Num i, Enum i, HasZero b) =>
Size i -> [[b]] -> Matrix i b
M.fromLists (M.Size { rows :: Int
M.rows = Arity -> Int
fullArity Arity
ar_g , cols :: Int
M.cols = [Pattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern]
pl }) ([[Order]] -> Matrix Int Order) -> [[Order]] -> Matrix Int Order
forall a b. (a -> b) -> a -> b
$
    (Expr -> [Order]) -> [Expr] -> [[Order]]
forall a b. (a -> b) -> [a] -> [b]
map (\ Expr
e -> (Pattern -> Order) -> [Pattern] -> [Order]
forall a b. (a -> b) -> [a] -> [b]
map (\ Pattern
p -> --traceTerm ("comparing " ++ show e ++ " to " ++ show p) $
                                    (?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
TSO Name -> Expr -> Pattern -> Order
compareExpr TSO Name
tso Expr
e Pattern
p) [Pattern]
pl) [Expr]
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 :: (?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
compareExpr TSO Name
tso Expr
e Pattern
p =
  let ret :: a -> a
ret a
o = String -> a -> a
forall a. String -> a -> a
traceTerm (String
"comparing expression " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" to pattern " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pattern -> String
forall a. Show a => a -> String
show Pattern
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" returns " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
o) a
o in
    Order -> Order
forall {a}. Show a => a -> a
ret (Order -> Order) -> Order -> Order
forall a b. (a -> b) -> a -> b
$ (?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
TSO Name -> Expr -> Pattern -> Order
compareExpr' TSO Name
tso Expr
e Pattern
p

compareExpr' :: (?cutoff :: Int) => TSO Name -> Expr -> Pattern -> Order
compareExpr' :: (?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
compareExpr' TSO Name
tso (Ann Tagged Expr
e) Pattern
p = (?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
TSO Name -> Expr -> Pattern -> Order
compareExpr' TSO Name
tso (Tagged Expr -> Expr
forall a. Tagged a -> a
unTag Tagged Expr
e) Pattern
p
compareExpr' TSO Name
tso Expr
e Pattern
p =
   case ((Expr, [Expr]) -> (Expr, [Expr])
conView ((Expr, [Expr]) -> (Expr, [Expr]))
-> (Expr, [Expr]) -> (Expr, [Expr])
forall a b. (a -> b) -> a -> b
$ Expr -> (Expr, [Expr])
spineView Expr
e, Pattern
p) of
      ((Expr, [Expr])
_,UnusableP Pattern
_) -> Order
Un
--      (Erased e,_)    -> compareExpr' tso e p
      ((Expr, [Expr])
_,ErasedP Pattern
p)   -> (?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
TSO Name -> Expr -> Pattern -> Order
compareExpr' TSO Name
tso Expr
e Pattern
p
      ((Expr, [Expr])
_,DotP Expr
e') -> case Expr -> Maybe Pattern
exprToPattern Expr
e' of
                       Maybe Pattern
Nothing ->  if Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e' then Int -> Order
Decr Int
0 else Order
Un
                       Just Pattern
p' -> (?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
TSO Name -> Expr -> Pattern -> Order
compareExpr' TSO Name
tso Expr
e Pattern
p'
      ((Var Name
i,[Expr]
_), Pattern
p) -> -- traceTerm ("compareVar " ++ show i ++ " " ++ show p) $
                         (?cutoff::Int) => TSO Name -> Name -> Pattern -> Order
TSO Name -> Name -> Pattern -> Order
compareVar TSO Name
tso Name
i Pattern
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 ConK
_) QName
n1),[Expr]
args),ConP PatternInfo
_ QName
n2 [Pattern]
pl) | QName
n1 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
n2 Bool -> Bool -> Bool
&& [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Pattern] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern]
pl ->
          let os :: [Order]
os = (Expr -> Pattern -> Order) -> [Expr] -> [Pattern] -> [Order]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
TSO Name -> Expr -> Pattern -> Order
compareExpr' TSO Name
tso) [Expr]
args [Pattern]
pl
          in  String -> Order -> Order
forall a. String -> a -> a
trace (String
"compareExpr (con/con case): os = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Order] -> String
forall a. Show a => a -> String
show [Order]
(?cutoff::Int) => [Order]
os) (Order -> Order) -> Order -> Order
forall a b. (a -> b) -> a -> b
$
              if [Order] -> Bool
forall a. Null a => a -> Bool
null [Order]
(?cutoff::Int) => [Order]
os then Int -> Order
Decr Int
0 else (?cutoff::Int) => [Order] -> Order
[Order] -> Order
minL [Order]
(?cutoff::Int) => [Order]
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 Expr
e2,[Expr]
_),SuccP Pattern
p2) ->  (?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
TSO Name -> Expr -> Pattern -> Order
compareExpr' TSO Name
tso Expr
e2 Pattern
p2
      -- new cases for counting constructors
      ((Succ Expr
e2,[Expr]
_),Pattern
p) ->  Int -> Order
Decr (-Int
1) (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
`comp` (?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
TSO Name -> Expr -> Pattern -> Order
compareExpr' TSO Name
tso Expr
e2 Pattern
p
      ((Def (DefId (ConK ConK
Cons) QName
n1),args :: [Expr]
args@(Expr
_:[Expr]
_)), Pattern
p) ->  Int -> Order
Decr (-Int
1) (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
`comp` (?cutoff::Int) => [Order] -> Order
[Order] -> Order
minL ((Expr -> Order) -> [Expr] -> [Order]
forall a b. (a -> b) -> [a] -> [b]
map (\Expr
e -> (?cutoff::Int) => TSO Name -> Expr -> Pattern -> Order
TSO Name -> Expr -> Pattern -> Order
compareExpr' TSO Name
tso Expr
e Pattern
p) [Expr]
args)
      ((Proj PrePost
Post Name
n1,[]), ProjP Name
n2) | Name
n1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n2 -> Int -> Order
Decr Int
0
      ((Expr, [Expr]), Pattern)
_ -> Order
Un

conView :: (Expr, [Expr]) -> (Expr, [Expr])
conView :: (Expr, [Expr]) -> (Expr, [Expr])
conView (Record (NamedRec ConK
co QName
n Bool
_ Dotted
_) [(Name, Expr)]
rs, [Expr]
es) = (DefId -> Expr
Def (IdKind -> QName -> DefId
DefId (ConK -> IdKind
ConK ConK
co) QName
n), ((Name, Expr) -> Expr) -> [(Name, Expr)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Expr) -> Expr
forall a b. (a, b) -> b
snd [(Name, Expr)]
rs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
es)
conView (Expr, [Expr])
p = (Expr, [Expr])
p

compareVar :: (?cutoff :: Int) => TSO Name -> Name -> Pattern -> Order
compareVar :: (?cutoff::Int) => TSO Name -> Name -> Pattern -> Order
compareVar TSO Name
tso Name
n Pattern
p =
  let ret :: p -> p
ret p
o = p
o in -- traceTerm ("comparing variable " ++ n ++ " to " ++ show p ++ " returns " ++ show o) o in
    case Pattern
p of
      UnusableP Pattern
_ -> Order -> Order
forall {p}. p -> p
ret Order
Un
      ErasedP Pattern
p   -> (?cutoff::Int) => TSO Name -> Name -> Pattern -> Order
TSO Name -> Name -> Pattern -> Order
compareVar TSO Name
tso Name
n Pattern
p
      VarP Name
n2 -> if Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n2 then Int -> Order
Decr Int
0 else
        case Name -> Name -> TSO Name -> Maybe Int
forall a. (Ord a, Eq a) => a -> a -> TSO a -> Maybe Int
TSO.diff Name
n Name
n2 TSO Name
tso of -- if n2 is the k-th father of n, then it is a decrease by k
          Maybe Int
Nothing -> Order -> Order
forall {p}. p -> p
ret Order
Un
          Just Int
k -> Order -> Order
forall {p}. p -> p
ret (Order -> Order) -> Order -> Order
forall a b. (a -> b) -> a -> b
$ (?cutoff::Int) => Int -> Order
Int -> Order
decr Int
k
      SizeP Expr
n1 Name
n2 -> if Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n2 then Int -> Order
Decr Int
0 else
        case Name -> Name -> TSO Name -> Maybe Int
forall a. (Ord a, Eq a) => a -> a -> TSO a -> Maybe Int
TSO.diff Name
n Name
n2 TSO Name
tso of -- if n2 is the k-th father of n, then it is a decrease by k
          Maybe Int
Nothing -> Order -> Order
forall {p}. p -> p
ret Order
Un
          Just Int
k -> Order -> Order
forall {p}. p -> p
ret (Order -> Order) -> Order -> Order
forall a b. (a -> b) -> a -> b
$ (?cutoff::Int) => Int -> Order
Int -> Order
decr Int
k
      PairP Pattern
p1 Pattern
p2 -> (?cutoff::Int) => [Order] -> Order
[Order] -> Order
maxL ((Pattern -> Order) -> [Pattern] -> [Order]
forall a b. (a -> b) -> [a] -> [b]
map ((?cutoff::Int) => TSO Name -> Name -> Pattern -> Order
TSO Name -> Name -> Pattern -> Order
compareVar TSO Name
tso Name
n) [Pattern
p1,Pattern
p2])
         -- no decrease in pair:  ALT: comp (Decr 1) (...)
      ConP PatternInfo
pi QName
c (Pattern
p:[Pattern]
pl) | PatternInfo -> ConK
coPat PatternInfo
pi ConK -> ConK -> Bool
forall a. Eq a => a -> a -> Bool
== ConK
Cons ->
        (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
comp (Int -> Order
Decr Int
1) ((?cutoff::Int) => [Order] -> Order
[Order] -> Order
maxL ((Pattern -> Order) -> [Pattern] -> [Order]
forall a b. (a -> b) -> [a] -> [b]
map ((?cutoff::Int) => TSO Name -> Name -> Pattern -> Order
TSO Name -> Name -> Pattern -> Order
compareVar TSO Name
tso Name
n) (Pattern
pPattern -> [Pattern] -> [Pattern]
forall a. a -> [a] -> [a]
:[Pattern]
pl)))
      ConP{}   -> Order -> Order
forall {p}. p -> p
ret Order
Un
      ProjP{}  -> Order -> Order
forall {p}. p -> p
ret Order
Un
      SuccP Pattern
p2 -> (?cutoff::Int) => Order -> Order -> Order
Order -> Order -> Order
comp (Int -> Order
Decr Int
1) ((?cutoff::Int) => TSO Name -> Name -> Pattern -> Order
TSO Name -> Name -> Pattern -> Order
compareVar TSO Name
tso Name
n Pattern
p2)
      DotP Expr
e -> case (Expr -> Maybe Pattern
exprToPattern Expr
e) of
                    Maybe Pattern
Nothing -> Order -> Order
forall {p}. p -> p
ret (Order -> Order) -> Order -> Order
forall a b. (a -> b) -> a -> b
$ Order
Un
                    Just Pattern
p' -> (?cutoff::Int) => TSO Name -> Name -> Pattern -> Order
TSO Name -> Name -> Pattern -> Order
compareVar TSO Name
tso Name
n Pattern
p'
      Pattern
_ -> String -> Order
forall a. HasCallStack => String -> a
error (String -> Order) -> String -> Order
forall a b. (a -> b) -> a -> b
$ String
"NYI: compareVar " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Pattern -> String
forall a. Show a => a -> String
show Pattern
p -- ret $ Un

---

type Index = Name

data Call = Call { Call -> Name
source :: Index , Call -> Name
target :: Index , Call -> Matrix Int Order
matrix :: CallMatrix }
            deriving (Call -> Call -> Bool
(Call -> Call -> Bool) -> (Call -> Call -> Bool) -> Eq Call
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Call -> Call -> Bool
== :: Call -> Call -> Bool
$c/= :: Call -> Call -> Bool
/= :: Call -> Call -> Bool
Eq,Int -> Call -> ShowS
[Call] -> ShowS
Call -> String
(Int -> Call -> ShowS)
-> (Call -> String) -> ([Call] -> ShowS) -> Show Call
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Call -> ShowS
showsPrec :: Int -> Call -> ShowS
$cshow :: Call -> String
show :: Call -> String
$cshowList :: [Call] -> ShowS
showList :: [Call] -> ShowS
Show,Eq Call
Eq Call =>
(Call -> Call -> Ordering)
-> (Call -> Call -> Bool)
-> (Call -> Call -> Bool)
-> (Call -> Call -> Bool)
-> (Call -> Call -> Bool)
-> (Call -> Call -> Call)
-> (Call -> Call -> Call)
-> Ord Call
Call -> Call -> Bool
Call -> Call -> Ordering
Call -> Call -> Call
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Call -> Call -> Ordering
compare :: Call -> Call -> Ordering
$c< :: Call -> Call -> Bool
< :: Call -> Call -> Bool
$c<= :: Call -> Call -> Bool
<= :: Call -> Call -> Bool
$c> :: Call -> Call -> Bool
> :: Call -> Call -> Bool
$c>= :: Call -> Call -> Bool
>= :: Call -> Call -> Bool
$cmax :: Call -> Call -> Call
max :: Call -> Call -> Call
$cmin :: Call -> Call -> Call
min :: Call -> Call -> Call
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 :: Matrix Int Order -> Matrix Int Order -> Bool
subsumes Matrix Int Order
m Matrix Int Order
m' = ((Order, Order) -> Bool) -> Matrix Int (Order, Order) -> Bool
forall a i. (a -> Bool) -> Matrix i a -> Bool
M.all ((Order -> Order -> Bool) -> (Order, Order) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Order -> Order -> Bool
leq) Matrix Int (Order, Order)
mm'
  where mm' :: Matrix Int (Order, Order)
mm' = Matrix Int Order -> Matrix Int Order -> Matrix Int (Order, Order)
forall i a.
(Ord i, HasZero a) =>
Matrix i a -> Matrix i a -> Matrix i (a, a)
M.zip Matrix Int Order
m Matrix Int Order
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 :: Order -> Order -> Bool
leq Order
Un Order
_ = Bool
True
leq (Decr Int
k) (Decr Int
l) = Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
l
leq (Mat Matrix Int Order
m) (Mat Matrix Int Order
m') = Matrix Int Order -> Matrix Int Order -> Bool
subsumes Matrix Int Order
m Matrix Int Order
m'
leq Order
_ Order
_ = Bool
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 :: Matrix Int Order -> Matrix Int Order -> Bool
progress Matrix Int Order
m Matrix Int Order
m' = ((Order, Order) -> Bool) -> Matrix Int (Order, Order) -> Bool
forall a i. (a -> Bool) -> Matrix i a -> Bool
M.any ((Order -> Order -> Bool) -> (Order, Order) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Order -> Order -> Bool
decrToward0) Matrix Int (Order, Order)
mm'
  where mm' :: Matrix Int (Order, Order)
mm' = Matrix Int Order -> Matrix Int Order -> Matrix Int (Order, Order)
forall i a.
(Ord i, HasZero a) =>
Matrix i a -> Matrix i a -> Matrix i (a, a)
M.zip Matrix Int Order
m Matrix Int Order
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 :: Order -> Order -> Bool
decrToward0 Order
Un (Decr Int
l) = Bool
True Bool -> Bool -> Bool
&& Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0
decrToward0 (Decr Int
k) (Decr Int
l) = Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
l  Bool -> Bool -> Bool
&& Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0
decrToward0 (Mat Matrix Int Order
m) (Mat Matrix Int Order
m') = Matrix Int Order -> Matrix Int Order -> Bool
progress Matrix Int Order
m Matrix Int Order
m'
decrToward0 Order
_ Order
_ = Bool
False


{- call pathes

  are lists of names of length >=2

  [f,g,h] = f --> g --> h
-}

newtype CallPath = CallPath { CallPath -> [Name]
getCallPath :: [Name] } deriving CallPath -> CallPath -> Bool
(CallPath -> CallPath -> Bool)
-> (CallPath -> CallPath -> Bool) -> Eq CallPath
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CallPath -> CallPath -> Bool
== :: CallPath -> CallPath -> Bool
$c/= :: CallPath -> CallPath -> Bool
/= :: CallPath -> CallPath -> Bool
Eq

instance Show CallPath where
  show :: CallPath -> String
show (CallPath [Name
g]) = Name -> String
forall a. Show a => a -> String
show Name
g
  show (CallPath (Name
f:[Name]
l)) = Name -> String
forall a. Show a => a -> String
show Name
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-->" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallPath -> String
forall a. Show a => a -> String
show ([Name] -> CallPath
CallPath [Name]
l)

emptyCP :: CallPath
emptyCP :: CallPath
emptyCP = [Name] -> CallPath
CallPath []

mkCP :: Name -> Name -> CallPath
mkCP :: Name -> Name -> CallPath
mkCP Name
src Name
tgt = [Name] -> CallPath
CallPath [Name
src, Name
tgt]

mulCP :: CallPath -> CallPath -> CallPath
mulCP :: CallPath -> CallPath -> CallPath
mulCP cp1 :: CallPath
cp1@(CallPath [Name]
one) cp2 :: CallPath
cp2@(CallPath (Name
g:[Name]
two)) =
  if [Name] -> Name
forall a. HasCallStack => [a] -> a
last [Name]
one Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
g then [Name] -> CallPath
CallPath ([Name]
one [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
two)
  else String -> CallPath
forall a. HasCallStack => String -> a
error (String
"internal error: Termination.mulCP: trying to compose callpath " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallPath -> String
forall a. Show a => a -> String
show CallPath
cp1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallPath -> String
forall a. Show a => a -> String
show CallPath
cp2)

compatibleCP :: CallPath -> CallPath -> Bool
compatibleCP :: CallPath -> CallPath -> Bool
compatibleCP (CallPath [Name]
one) (CallPath [Name]
two) = [Name] -> Name
forall a. HasCallStack => [a] -> a
head [Name]
one Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== [Name] -> Name
forall a. HasCallStack => [a] -> a
head [Name]
two Bool -> Bool -> Bool
&& [Name] -> Name
forall a. HasCallStack => [a] -> a
last [Name]
one Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== [Name] -> Name
forall a. HasCallStack => [a] -> a
last [Name]
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 :: (?cutoff::Int) => CompCall -> CompCall -> CompCall
mulCC cc1 :: CompCall
cc1@(CallPath
cp1, Matrix Int Order
m1) cc2 :: CompCall
cc2@(CallPath
cp2, Matrix Int Order
m2) = (CallPath -> CallPath -> CallPath)
-> (Matrix Int Order -> Matrix Int Order -> Matrix Int Order)
-> CompCall
-> CompCall
-> CompCall
forall a b c d e f.
(a -> b -> c) -> (d -> e -> f) -> (a, d) -> (b, e) -> (c, f)
zipPair CallPath -> CallPath -> CallPath
mulCP ((Matrix Int Order -> Matrix Int Order -> Matrix Int Order)
-> Matrix Int Order -> Matrix Int Order -> Matrix Int Order
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Semiring Order
-> Matrix Int Order -> Matrix Int Order -> Matrix Int Order
forall i a.
(Enum i, Num i, Ix i, Eq a) =>
Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
M.mul Semiring Order
(?cutoff::Int) => Semiring Order
ordRing)) CompCall
cc1 CompCall
cc2

subsumesCC :: CompCall -> CompCall -> Bool
subsumesCC :: CompCall -> CompCall -> Bool
subsumesCC cc1 :: CompCall
cc1@(CallPath
cp1, Matrix Int Order
m1) cc2 :: CompCall
cc2@(CallPath
cp2, Matrix Int Order
m2) =
  if CallPath -> CallPath -> Bool
compatibleCP CallPath
cp1 CallPath
cp2 then Matrix Int Order
m1 Matrix Int Order -> Matrix Int Order -> Bool
`subsumes` Matrix Int Order
m2
   else String -> Bool
forall a. HasCallStack => String -> a
error (String
"internal error: Termination.subsumesCC: trying to compare composed call " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CompCall -> String
forall a. Show a => a -> String
show CompCall
cc2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CompCall -> String
forall a. Show a => a -> String
show CompCall
cc1)

progressCC :: CompCall -> CompCall -> Bool
progressCC :: CompCall -> CompCall -> Bool
progressCC cc1 :: CompCall
cc1@(CallPath
cp1, Matrix Int Order
m1) cc2 :: CompCall
cc2@(CallPath
cp2, Matrix Int Order
m2) = Matrix Int Order -> Matrix Int Order -> Bool
progress Matrix Int Order
m1 Matrix Int Order
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 :: (?cutoff::Int) => Semiring CMSet
cmRing = Semiring { add :: CMSet -> CMSet -> CMSet
add = CMSet -> CMSet -> CMSet
unionCMSet , mul :: CMSet -> CMSet -> CMSet
mul = (?cutoff::Int) => CMSet -> CMSet -> CMSet
CMSet -> CMSet -> CMSet
mulCMSet , zero :: CMSet
zero = [] } -- one = undefined ,

type Progress = Writer Any
type ProgressH = Writer (Any, Any)

firstHalf :: (Any, Any)
firstHalf :: (Any, Any)
firstHalf = (Bool -> Any
Any Bool
True, Bool -> Any
Any Bool
False)

secondHalf :: (Any, Any)
secondHalf :: (Any, Any)
secondHalf = (Bool -> Any
Any Bool
False, Bool -> Any
Any Bool
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 :: CompCall -> CMSet -> ProgressH CMSet
addCMh CompCall
m [] = String -> ProgressH CMSet -> ProgressH CMSet
forall a. String -> a -> a
traceProg (String
"adding new call " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CompCall -> String
forall a. Show a => a -> String
show CompCall
m) (ProgressH CMSet -> ProgressH CMSet)
-> ProgressH CMSet -> ProgressH CMSet
forall a b. (a -> b) -> a -> b
$ do
  (Any, Any) -> WriterT (Any, Any) Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Any, Any)
firstHalf
  CMSet -> ProgressH CMSet
forall a. a -> WriterT (Any, Any) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (CMSet -> ProgressH CMSet) -> CMSet -> ProgressH CMSet
forall a b. (a -> b) -> a -> b
$ [CompCall
m]
addCMh CompCall
m (CompCall
m':CMSet
ms) =
  if CompCall
m' CompCall -> CompCall -> Bool
`subsumesCC` CompCall
m then String -> ProgressH CMSet -> ProgressH CMSet
forall a. String -> a -> a
traceTerm (String
"discarding new call " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CompCall -> String
forall a. Show a => a -> String
show CompCall
m) (ProgressH CMSet -> ProgressH CMSet)
-> ProgressH CMSet -> ProgressH CMSet
forall a b. (a -> b) -> a -> b
$
     CMSet -> ProgressH CMSet
forall a. a -> WriterT (Any, Any) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (CMSet -> ProgressH CMSet) -> CMSet -> ProgressH CMSet
forall a b. (a -> b) -> a -> b
$ CompCall
m'CompCall -> CMSet -> CMSet
forall a. a -> [a] -> [a]
:CMSet
ms -- terminate early
   else do (ms', (Any h1, Any h2)) <- ProgressH CMSet -> WriterT (Any, Any) Identity (CMSet, (Any, Any))
forall a.
WriterT (Any, Any) Identity a
-> WriterT (Any, Any) Identity (a, (Any, Any))
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (ProgressH CMSet
 -> WriterT (Any, Any) Identity (CMSet, (Any, Any)))
-> ProgressH CMSet
-> WriterT (Any, Any) Identity (CMSet, (Any, Any))
forall a b. (a -> b) -> a -> b
$ CompCall -> CMSet -> ProgressH CMSet
addCMh CompCall
m CMSet
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' :: CompCall -> CMSet -> Progress CMSet
addCM' CompCall
m CMSet
ms = ((CMSet, (Any, Any)) -> (CMSet, Any))
-> ProgressH CMSet -> Progress CMSet
forall a w b w'. ((a, w) -> (b, w')) -> Writer w a -> Writer w' b
mapWriter (\(CMSet
ms, (Any Bool
h1, Any Bool
h2)) -> (CMSet
ms, Bool -> Any
Any (Bool -> Any) -> Bool -> Any
forall a b. (a -> b) -> a -> b
$ Bool
h1 Bool -> Bool -> Bool
&& Bool
h2)) (CompCall -> CMSet -> ProgressH CMSet
addCMh CompCall
m CMSet
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' :: CMSet -> CMSet -> Progress CMSet
unionCMSet' [] []  = CMSet -> Progress CMSet
forall a. a -> WriterT Any Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return []
unionCMSet' CMSet
ms []  = Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True) WriterT Any Identity () -> Progress CMSet -> Progress CMSet
forall a b.
WriterT Any Identity a
-> WriterT Any Identity b -> WriterT Any Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CMSet -> Progress CMSet
forall a. a -> WriterT Any Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CMSet
ms
unionCMSet' CMSet
ms CMSet
ms' = (CMSet -> CompCall -> Progress CMSet)
-> CMSet -> CMSet -> Progress CMSet
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((CompCall -> CMSet -> Progress CMSet)
-> CMSet -> CompCall -> Progress CMSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip CompCall -> CMSet -> Progress CMSet
addCM') CMSet
ms' CMSet
ms

-- non-monadic versions
addCM :: CompCall -> CMSet -> CMSet
addCM :: CompCall -> CMSet -> CMSet
addCM CompCall
m CMSet
ms = (CMSet, Any) -> CMSet
forall a b. (a, b) -> a
fst ((CMSet, Any) -> CMSet) -> (CMSet, Any) -> CMSet
forall a b. (a -> b) -> a -> b
$ Progress CMSet -> (CMSet, Any)
forall w a. Writer w a -> (a, w)
runWriter (CompCall -> CMSet -> Progress CMSet
addCM' CompCall
m CMSet
ms)

unionCMSet :: CMSet -> CMSet -> CMSet
unionCMSet :: CMSet -> CMSet -> CMSet
unionCMSet CMSet
ms CMSet
ms' = (CMSet, Any) -> CMSet
forall a b. (a, b) -> a
fst ((CMSet, Any) -> CMSet) -> (CMSet, Any) -> CMSet
forall a b. (a -> b) -> a -> b
$ Progress CMSet -> (CMSet, Any)
forall w a. Writer w a -> (a, w)
runWriter (CMSet -> CMSet -> Progress CMSet
unionCMSet' CMSet
ms CMSet
ms')

mulCMSet :: (?cutoff :: Int) => CMSet -> CMSet -> CMSet
mulCMSet :: (?cutoff::Int) => CMSet -> CMSet -> CMSet
mulCMSet CMSet
ms CMSet
ms' = (CMSet -> CompCall -> CMSet) -> CMSet -> CMSet -> CMSet
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((CompCall -> CMSet -> CMSet) -> CMSet -> CompCall -> CMSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip CompCall -> CMSet -> CMSet
addCM) [] (CMSet -> CMSet) -> CMSet -> CMSet
forall a b. (a -> b) -> a -> b
$ [ (?cutoff::Int) => CompCall -> CompCall -> CompCall
CompCall -> CompCall -> CompCall
mulCC CompCall
m CompCall
m' | CompCall
m <- CMSet
ms, CompCall
m' <- CMSet
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 :: (?cutoff::Int) => CallGraph -> Progress CallGraph
stepCG CallGraph
cg = do
  String -> WriterT Any Identity ()
forall (m :: * -> *). Monad m => String -> m ()
traceProgM (String
"next iteration")
  String -> WriterT Any Identity ()
forall (m :: * -> *). Monad m => String -> m ()
traceProgM (String
"old cg " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallGraph -> String
forall a. Show a => a -> String
show CallGraph
cg)
  String -> WriterT Any Identity ()
forall (m :: * -> *). Monad m => String -> m ()
traceProgM (String
"composed calls " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallGraph -> String
forall a. Show a => a -> String
show CallGraph
(?cutoff::Int) => CallGraph
cg')
  String -> WriterT Any Identity ()
forall (m :: * -> *). Monad m => String -> m ()
traceProgM (String
"adding new calls to callgraph...")
  ([CMSet] -> [CMSet] -> WriterT Any Identity [CMSet])
-> CallGraph -> CallGraph -> Progress CallGraph
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ((CMSet -> CMSet -> Progress CMSet)
-> [CMSet] -> [CMSet] -> WriterT Any Identity [CMSet]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM CMSet -> CMSet -> Progress CMSet
unionCMSet') CallGraph
(?cutoff::Int) => CallGraph
cg' CallGraph
cg
  where cg' :: CallGraph
cg' = Semiring CMSet -> CallGraph -> CallGraph -> CallGraph
forall a.
Show a =>
Semiring a -> NaiveMatrix a -> NaiveMatrix a -> NaiveMatrix a
mmul Semiring CMSet
(?cutoff::Int) => Semiring CMSet
cmRing CallGraph
cg CallGraph
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 :: (?cutoff::Int) => CallGraph -> CallGraph
complCGraph CallGraph
cg =
  let (CallGraph
cg', Any Bool
prog) = Progress CallGraph -> (CallGraph, Any)
forall w a. Writer w a -> (a, w)
runWriter (Progress CallGraph -> (CallGraph, Any))
-> Progress CallGraph -> (CallGraph, Any)
forall a b. (a -> b) -> a -> b
$ (?cutoff::Int) => CallGraph -> Progress CallGraph
CallGraph -> Progress CallGraph
stepCG CallGraph
cg
  in  if Bool
(?cutoff::Int) => Bool
prog Bool -> Bool -> Bool
&& (?cutoff::Int) => CallGraph -> Bool
CallGraph -> Bool
checkAll CallGraph
(?cutoff::Int) => CallGraph
cg' then (?cutoff::Int) => CallGraph -> CallGraph
CallGraph -> CallGraph
complCGraph CallGraph
(?cutoff::Int) => CallGraph
cg' else CallGraph
(?cutoff::Int) => CallGraph
cg'

checkAll :: (?cutoff :: Int) => CallGraph -> Bool
checkAll :: (?cutoff::Int) => CallGraph -> Bool
checkAll CallGraph
cg = (CMSet -> Bool) -> [CMSet] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((CompCall -> Bool) -> CMSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((?cutoff::Int) => Matrix Int Order -> Bool
Matrix Int Order -> Bool
checkIdem (Matrix Int Order -> Bool)
-> (CompCall -> Matrix Int Order) -> CompCall -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompCall -> Matrix Int Order
forall a b. (a, b) -> b
snd)) ([CMSet] -> Bool) -> [CMSet] -> Bool
forall a b. (a -> b) -> a -> b
$ CallGraph -> [CMSet]
forall a. NaiveMatrix a -> Vector a
diag CallGraph
cg

-- each idempotent call needs a decreasing diagonal entry
checkIdem :: (?cutoff :: Int) => CallMatrix -> Bool
checkIdem :: (?cutoff::Int) => Matrix Int Order -> Bool
checkIdem Matrix Int Order
cm =
  let cm' :: Matrix Int Order
cm'   = Semiring Order
-> Matrix Int Order -> Matrix Int Order -> Matrix Int Order
forall i a.
(Enum i, Num i, Ix i, Eq a) =>
Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
M.mul Semiring Order
(?cutoff::Int) => Semiring Order
ordRing Matrix Int Order
cm Matrix Int Order
cm
      eqAbs :: Bool
eqAbs = (Matrix Int Order -> Matrix Int Order
absCM Matrix Int Order
cm) Matrix Int Order -> Matrix Int Order -> Bool
forall a. Eq a => a -> a -> Bool
== (Matrix Int Order -> Matrix Int Order
absCM Matrix Int Order
(?cutoff::Int) => Matrix Int Order
cm')
      d :: [Order]
d     = Matrix Int Order -> [Order]
forall i b.
(Enum i, Num i, Ix i, Show i, HasZero b) =>
Matrix i b -> [b]
M.diagonal Matrix Int Order
cm
  in  String -> Bool -> Bool
forall a. String -> a -> a
traceTerm (String
"checkIdem: cm = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Matrix Int Order -> String
forall a. Show a => a -> String
show Matrix Int Order
cm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" cm' = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Matrix Int Order -> String
forall a. Show a => a -> String
show Matrix Int Order
cm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" eqAbs = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
(?cutoff::Int) => Bool
eqAbs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" d = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Order] -> String
forall a. Show a => a -> String
show [Order]
d) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      -- if cm `subsumes` cm'
      if Bool
(?cutoff::Int) => Bool
eqAbs
       then (Order -> Bool) -> [Order] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Order -> Bool
isDecr [Order]
d else Bool
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 :: [Name] -> [Call] -> CallGraph
makeCG [Name]
names [Call]
calls = (Name -> [CMSet]) -> [Name] -> CallGraph
forall a b. (a -> b) -> [a] -> [b]
map (\ Name
src -> Name -> [Call] -> [CMSet]
mkRow Name
src [ Call
c | Call
c <- [Call]
calls, Call -> Name
source Call
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
src ]) [Name]
names
  where mkRow :: Name -> [Call] -> [CMSet]
mkRow Name
src [Call]
calls = (Name -> CMSet) -> [Name] -> [CMSet]
forall a b. (a -> b) -> [a] -> [b]
map (\ Name
tgt ->  CMSet -> CMSet -> CMSet
unionCMSet [ (Name -> Name -> CallPath
mkCP Name
src Name
tgt, Call -> Matrix Int Order
matrix Call
c) | Call
c <- [Call]
calls, Call -> Name
target Call
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
tgt ] []) [Name]
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 :: Order -> Bool
isDecr Order
o = case Order
o of
             (Decr Int
k) -> Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
             (Mat Matrix Int Order
m) -> (Order -> Bool) -> [Order] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Order -> Bool
isDecr (Matrix Int Order -> [Order]
forall i b.
(Enum i, Num i, Ix i, Show i, HasZero b) =>
Matrix i b -> [b]
M.diagonal Matrix Int Order
m)
             Order
_ -> Bool
False


-------------------

-- top level function
terminationCheck :: MonadAssert m => [Fun] -> m ()
terminationCheck :: forall (m :: * -> *). MonadAssert m => [Fun] -> m ()
terminationCheck [Fun]
funs = do
       let ?cutoff = ?cutoff::Int
Int
cutoff
       String -> m ()
forall (m :: * -> *). Monad m => String -> m ()
traceTermM (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"terminationCheck " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Fun] -> String
forall a. Show a => a -> String
show [Fun]
funs
       let tl :: [(Name, Bool)]
tl = (?cutoff::Int) => [Fun] -> [(Name, Bool)]
[Fun] -> [(Name, Bool)]
terminationCheckFuns [Fun]
funs
       let nl :: [Name]
nl = ((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
forall a b. (a, b) -> a
fst [(Name, Bool)]
(?cutoff::Int) => [(Name, Bool)]
tl
       let bl :: [Bool]
bl = ((Name, Bool) -> Bool) -> [(Name, Bool)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Bool
forall a b. (a, b) -> b
snd [(Name, Bool)]
(?cutoff::Int) => [(Name, Bool)]
tl
       let nl2 :: [Name]
nl2 = [ Name
n | (Name
n,Bool
b) <- [(Name, Bool)]
(?cutoff::Int) => [(Name, Bool)]
tl , Bool
b Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
False ]
       case ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
(?cutoff::Int) => [Bool]
bl) of
            Bool
True -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Bool
False -> case [Name]
(?cutoff::Int) => [Name]
nl of
                    [Name
f] -> String -> m ()
forall (m :: * -> *). MonadAssert m => String -> m ()
recoverFail (String
"Termination check for function " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" fails ")
                    [Name]
_   -> String -> m ()
forall (m :: * -> *). MonadAssert m => String -> m ()
recoverFail (String
"Termination check for mutual block " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
(?cutoff::Int) => [Name]
nl String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" fails for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
(?cutoff::Int) => [Name]
nl2)


terminationCheckFuns :: (?cutoff :: Int) => [Fun] -> [(Name,Bool)]
terminationCheckFuns :: (?cutoff::Int) => [Fun] -> [(Name, Bool)]
terminationCheckFuns [Fun]
funs =
   let namar :: [(Name, Arity)]
namar = (Fun -> (Name, Arity)) -> [Fun] -> [(Name, Arity)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Fun (TypeSig Name
n Expr
_) Name
_ Arity
ar [Clause]
_) -> (Name
n, Arity
ar)) [Fun]
funs
               -- collectNames funs
       names :: [Name]
names = ((Name, Arity) -> Name) -> [(Name, Arity)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Arity) -> Name
forall a b. (a, b) -> a
fst [(Name, Arity)]
namar
       cg0 :: [Call]
cg0 = (?cutoff::Int) => [(Name, Arity)] -> [Fun] -> [Call]
[(Name, Arity)] -> [Fun] -> [Call]
collectCGFunDecl [(Name, Arity)]
namar [Fun]
funs
   in (?cutoff::Int) => [Name] -> [Call] -> [(Name, Bool)]
[Name] -> [Call] -> [(Name, Bool)]
sizeChangeTermination [Name]
names [Call]
(?cutoff::Int) => [Call]
cg0

sizeChangeTermination :: (?cutoff :: Int) => [Name] -> [Call] -> [(Name,Bool)]
sizeChangeTermination :: (?cutoff::Int) => [Name] -> [Call] -> [(Name, Bool)]
sizeChangeTermination [Name]
names [Call]
cg0 =
   let cg1 :: CallGraph
cg1 = [Name] -> [Call] -> CallGraph
makeCG [Name]
names [Call]
cg0
       cg :: CallGraph
cg = (?cutoff::Int) => CallGraph -> CallGraph
CallGraph -> CallGraph
complCGraph (CallGraph -> CallGraph) -> CallGraph -> CallGraph
forall a b. (a -> b) -> a -> b
$ CallGraph
cg1
       beh :: [(Name, Bool)]
beh = [Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
names ([Bool] -> [(Name, Bool)]) -> [Bool] -> [(Name, Bool)]
forall a b. (a -> b) -> a -> b
$ (CMSet -> Bool) -> [CMSet] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ((CompCall -> Bool) -> CMSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((?cutoff::Int) => Matrix Int Order -> Bool
Matrix Int Order -> Bool
checkIdem (Matrix Int Order -> Bool)
-> (CompCall -> Matrix Int Order) -> CompCall -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompCall -> Matrix Int Order
forall a b. (a, b) -> b
snd)) ([CMSet] -> [Bool]) -> [CMSet] -> [Bool]
forall a b. (a -> b) -> a -> b
$ CallGraph -> [CMSet]
forall a. NaiveMatrix a -> Vector a
diag CallGraph
(?cutoff::Int) => CallGraph
cg
   in String -> [(Name, Bool)] -> [(Name, Bool)]
forall a. String -> a -> a
traceTerm (String
"collected names: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
names) ([(Name, Bool)] -> [(Name, Bool)])
-> [(Name, Bool)] -> [(Name, Bool)]
forall a b. (a -> b) -> a -> b
$
      String -> [(Name, Bool)] -> [(Name, Bool)]
forall a. String -> a -> a
traceTerm (String
"call graph: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Call] -> String
forall a. Show a => a -> String
show [Call]
cg0) ([(Name, Bool)] -> [(Name, Bool)])
-> [(Name, Bool)] -> [(Name, Bool)]
forall a b. (a -> b) -> a -> b
$
      String -> [(Name, Bool)] -> [(Name, Bool)]
forall a. String -> a -> a
traceTerm (String
"normalized call graph: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallGraph -> String
forall a. Show a => a -> String
show CallGraph
cg1) ([(Name, Bool)] -> [(Name, Bool)])
-> [(Name, Bool)] -> [(Name, Bool)]
forall a b. (a -> b) -> a -> b
$
      String -> [(Name, Bool)] -> [(Name, Bool)]
forall a. String -> a -> a
traceTerm (String
"completed call graph: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CallGraph -> String
forall a. Show a => a -> String
show CallGraph
(?cutoff::Int) => CallGraph
cg) ([(Name, Bool)] -> [(Name, Bool)])
-> [(Name, Bool)] -> [(Name, Bool)]
forall a b. (a -> b) -> a -> b
$
      String -> [(Name, Bool)] -> [(Name, Bool)]
forall a. String -> a -> a
traceTerm (String
"recursion behaviours" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Name, Bool)] -> String
forall a. Show a => a -> String
show [(Name, Bool)]
(?cutoff::Int) => [(Name, Bool)]
beh) ([(Name, Bool)] -> [(Name, Bool)])
-> [(Name, Bool)] -> [(Name, Bool)]
forall a b. (a -> b) -> a -> b
$
      [(Name, Bool)]
(?cutoff::Int) => [(Name, Bool)]
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 :: (?cutoff::Int) => [(Name, Arity)] -> [Fun] -> [Call]
collectCGFunDecl [(Name, Arity)]
names [Fun]
funs =
      (Fun -> [Call]) -> [Fun] -> [Call]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(Name, Arity)] -> Fun -> [Call]
collectClauses [(Name, Arity)]
names) [Fun]
funs
          where
            collectClauses :: [(Name,Arity)] -> Fun -> [Call]
            collectClauses :: [(Name, Arity)] -> Fun -> [Call]
collectClauses [(Name, Arity)]
names (Fun (TypeSig Name
n Expr
_) Name
_ Arity
ar [Clause]
cll) = [(Name, Arity)] -> Name -> [Clause] -> [Call]
collectClause [(Name, Arity)]
names Name
n [Clause]
cll
            collectClause :: [(Name,Arity)] -> Name -> [Clause] -> [Call]
            collectClause :: [(Name, Arity)] -> Name -> [Clause] -> [Call]
collectClause [(Name, Arity)]
names Name
n ((Clause TeleVal
_ [Pattern]
pl Maybe Expr
Nothing):[Clause]
rest) = [(Name, Arity)] -> Name -> [Clause] -> [Call]
collectClause [(Name, Arity)]
names Name
n [Clause]
rest
            collectClause [(Name, Arity)]
names Name
n ((Clause TeleVal
_ [Pattern]
pl (Just Expr
rhs)):[Clause]
rest) =
              String -> [Call] -> [Call]
forall a. String -> a -> a
traceTerm (String
"collecting calls in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
rhs) ([Call] -> [Call]) -> [Call] -> [Call]
forall a b. (a -> b) -> a -> b
$
                ((?cutoff::Int) =>
[(Name, Arity)] -> Name -> [Pattern] -> Expr -> [Call]
[(Name, Arity)] -> Name -> [Pattern] -> Expr -> [Call]
collectCallsExpr [(Name, Arity)]
names Name
n [Pattern]
pl Expr
rhs) [Call] -> [Call] -> [Call]
forall a. [a] -> [a] -> [a]
++ ([(Name, Arity)] -> Name -> [Clause] -> [Call]
collectClause [(Name, Arity)]
names Name
n [Clause]
rest)
            collectClause [(Name, Arity)]
names Name
n [] = []

-- | harvest i > j  from  case i { $ j -> ...}
tsoCase :: TSO Name -> Expr -> [Clause] -> TSO Name
tsoCase :: TSO Name -> Expr -> [Clause] -> TSO Name
tsoCase TSO Name
tso (Var Name
x) [Clause TeleVal
_ [SuccP (VarP Name
y)] Maybe Expr
_] = Name -> (Int, Name) -> TSO Name -> TSO Name
forall a. (Ord a, Eq a) => a -> (Int, a) -> TSO a -> TSO a
TSO.insert Name
y (Int
1,Name
x) TSO Name
tso
tsoCase TSO Name
tso Expr
_ [Clause]
_ = TSO Name
tso

-- | harvest i < j  from (i < j) -> ... or (i < j) & ...
tsoBind :: TSO Name -> TBind -> TSO Name
tsoBind :: TSO Name -> TBind -> TSO Name
tsoBind TSO Name
tso (TBind Name
x (Domain (Below LtLe
ltle (Var Name
y)) Kind
_ Dec
_)) = Name -> (Int, Name) -> TSO Name -> TSO Name
forall a. (Ord a, Eq a) => a -> (Int, a) -> TSO a -> TSO a
TSO.insert Name
x (LtLe -> Int
forall {a}. Num a => LtLe -> a
n LtLe
ltle,Name
y) TSO Name
tso
  where n :: LtLe -> a
n LtLe
Lt = a
1
        n LtLe
Le = a
0
tsoBind TSO Name
tso TBind
_ = TSO Name
tso

collectCallsExpr :: (?cutoff :: Int) => [(Name,Arity)] -> Name -> [Pattern] -> Expr -> [Call]
collectCallsExpr :: (?cutoff::Int) =>
[(Name, Arity)] -> Name -> [Pattern] -> Expr -> [Call]
collectCallsExpr [(Name, Arity)]
nl Name
f [Pattern]
pl Expr
e = String -> [Call] -> [Call]
forall a. String -> a -> a
traceTerm (String
"collectCallsExpr " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e) ([Call] -> [Call]) -> [Call] -> [Call]
forall a b. (a -> b) -> a -> b
$
  (?cutoff::Int) => TSO Name -> Expr -> [Call]
TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e where
    tso :: TSO Name
tso = [Pattern] -> TSO Name
tsoFromPatterns [Pattern]
pl
    loop :: TSO Name -> Expr -> [Call]
loop TSO Name
tso (Ann Tagged Expr
e) = TSO Name -> Expr -> [Call]
loop TSO Name
tso (Tagged Expr -> Expr
forall a. Tagged a -> a
unTag Tagged Expr
e)
    loop TSO Name
tso Expr
e = [Call]
(?cutoff::Int) => [Call]
headcalls [Call] -> [Call] -> [Call]
forall a. [a] -> [a] -> [a]
++ [Call]
argcalls where
      (Expr
hd, [Expr]
args) = Expr -> (Expr, [Expr])
spineView Expr
e -- $ ignoreTopErasure e
      argcalls :: [Call]
argcalls = (Expr -> [Call]) -> [Expr] -> [Call]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TSO Name -> Expr -> [Call]
loop TSO Name
tso) [Expr]
args
      headcalls :: [Call]
headcalls = case Expr
hd of
          (Def (DefId IdKind
FunK (QName Name
g))) ->
              case Name -> [(Name, Arity)] -> Maybe Arity
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
g [(Name, Arity)]
nl of
                Maybe Arity
Nothing -> []
                Just Arity
ar_g ->
                  String -> [Call] -> [Call]
forall a. String -> a -> a
traceTerm (String
"found call from " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
g) ([Call] -> [Call]) -> [Call] -> [Call]
forall a b. (a -> b) -> a -> b
$
                             let (Just Arity
ar_f) = Name -> [(Name, Arity)] -> Maybe Arity
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
f [(Name, Arity)]
nl
                                 (Just Int
f') = (Name, Arity) -> [(Name, Arity)] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex (Name
f,Arity
ar_f) [(Name, Arity)]
nl
                                 (Just Int
g') = (Name, Arity) -> [(Name, Arity)] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
List.elemIndex (Name
g,Arity
ar_g) [(Name, Arity)]
nl
                                 m :: Matrix Int Order
m = (?cutoff::Int) =>
TSO Name -> [Pattern] -> [Expr] -> Arity -> Matrix Int Order
TSO Name -> [Pattern] -> [Expr] -> Arity -> Matrix Int Order
compareArgs TSO Name
tso [Pattern]
pl [Expr]
args Arity
ar_g
                                 cg :: Call
cg = Call { source :: Name
source = Name
f
                                           , target :: Name
target = Name
g
                                           , matrix :: Matrix Int Order
matrix = Matrix Int Order
(?cutoff::Int) => Matrix Int Order
m }
                             in
                               String -> [Call] -> [Call]
forall a. String -> a -> a
traceTerm (String
"found call " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Call -> String
forall a. Show a => a -> String
show Call
(?cutoff::Int) => Call
cg) ([Call] -> [Call]) -> [Call] -> [Call]
forall a b. (a -> b) -> a -> b
$
                                 [Call
(?cutoff::Int) => Call
cg]
          (Case Expr
e Maybe Expr
_ [Clause]
cls) -> TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e [Call] -> [Call] -> [Call]
forall a. [a] -> [a] -> [a]
++ (Expr -> [Call]) -> [Expr] -> [Call]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TSO Name -> Expr -> [Call]
loop (TSO Name -> Expr -> [Clause] -> TSO Name
tsoCase TSO Name
tso Expr
e [Clause]
cls)) ((Clause -> Expr) -> [Clause] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> (Expr -> Expr) -> Maybe Expr -> Expr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
Irr Expr -> Expr
forall {p}. p -> p
id (Maybe Expr -> Expr) -> (Clause -> Maybe Expr) -> Clause -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Expr
clExpr) [Clause]
cls)
          (Lam Dec
_ Name
_ Expr
e1) -> TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e1
          (LLet LBind
tb Telescope
tel Expr
e1 Expr
e2) | Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel->
             (TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e1) [Call] -> [Call] -> [Call]
forall a. [a] -> [a] -> [a]
++ -- type won't get evaluated
             (TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e2)
          (Quant PiSigma
_ tb :: TBind
tb@(TBind Name
x Dom Expr
dom) Expr
e2) -> (TSO Name -> Expr -> [Call]
loop TSO Name
tso (Dom Expr -> Expr
forall a. Dom a -> a
typ Dom Expr
dom)) [Call] -> [Call] -> [Call]
forall a. [a] -> [a] -> [a]
++ (TSO Name -> Expr -> [Call]
loop (TSO Name -> TBind -> TSO Name
tsoBind TSO Name
tso TBind
tb) Expr
e2)
          (Quant PiSigma
_ (TMeasure Measure Expr
mu) Expr
e2) -> (Expr -> [Call]) -> Measure Expr -> [Call]
forall m a. Monoid m => (a -> m) -> Measure a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TSO Name -> Expr -> [Call]
loop TSO Name
tso) Measure Expr
mu [Call] -> [Call] -> [Call]
forall a. [a] -> [a] -> [a]
++ (TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e2)
          (Quant PiSigma
_ (TBound Bound Expr
beta) Expr
e2) -> (Expr -> [Call]) -> Bound Expr -> [Call]
forall m a. Monoid m => (a -> m) -> Bound a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TSO Name -> Expr -> [Call]
loop TSO Name
tso) Bound Expr
beta [Call] -> [Call] -> [Call]
forall a. [a] -> [a] -> [a]
++ (TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e2)
          (Below LtLe
ltle Expr
e) -> TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e
          (Sing Expr
e1 Expr
e2) -> (TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e1) [Call] -> [Call] -> [Call]
forall a. [a] -> [a] -> [a]
++ (TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e2)
          (Pair Expr
e1 Expr
e2) -> (TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e1) [Call] -> [Call] -> [Call]
forall a. [a] -> [a] -> [a]
++ (TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e2)
          (Succ Expr
e) -> TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e
          (Max [Expr]
es) -> (Expr -> [Call]) -> [Expr] -> [Call]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TSO Name -> Expr -> [Call]
loop TSO Name
tso) [Expr]
es
          (Plus [Expr]
es) -> (Expr -> [Call]) -> [Expr] -> [Call]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TSO Name -> Expr -> [Call]
loop TSO Name
tso) [Expr]
es
          Sort (SortC{})  -> []
          Sort (Set Expr
e)    -> TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e
          Sort (CoSet Expr
e)  -> TSO Name -> Expr -> [Call]
loop TSO Name
tso Expr
e
          Var{}   -> []
          Zero{} -> []
          Infty{} -> []
          Def{}   -> []
          Irr{}   -> []
          Proj{}   -> []
          Record RecInfo
ri [(Name, Expr)]
rs -> ((Name, Expr) -> [Call]) -> [(Name, Expr)] -> [Call]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TSO Name -> Expr -> [Call]
loop TSO Name
tso (Expr -> [Call])
-> ((Name, Expr) -> Expr) -> (Name, Expr) -> [Call]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Expr) -> Expr
forall a b. (a, b) -> b
snd) [(Name, Expr)]
rs
          Ann Tagged Expr
e1 -> TSO Name -> Expr -> [Call]
loop TSO Name
tso (Tagged Expr -> Expr
forall a. Tagged a -> a
unTag Tagged Expr
e1)
--          Con{}   -> []
--          Let{}   -> []
          Meta{}  -> String -> [Call]
forall a. HasCallStack => String -> a
error (String -> [Call]) -> String -> [Call]
forall a b. (a -> b) -> a -> b
$ String
"collect calls in unresolved meta variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e
          Expr
_ -> String -> [Call]
forall a. HasCallStack => String -> a
error (String -> [Call]) -> String -> [Call]
forall a b. (a -> b) -> a -> b
$ String
"NYI: collect calls in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
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^*)^*

-}