-- Example program based on one generated by our fusion/clustering algorithm
--
-- sum1 = fold   (+) 0    xs
-- nor1 = map    (/ sum1) xs
-- ys   = filter (>  0)   xs
-- sum2 = fold   (+) 0    ys
-- nor2 = map    (/ sum2) xs
--

module Clustering (clustering) where

import Base
import Numeric.Limp.Rep
import Numeric.Limp.Program

import qualified Numeric.Limp.Canon as C
import qualified Numeric.Limp.Canon.Pretty as C

-- | One for each combinator
data Node
 = Sum1 | Nor1 | Ys | Sum2 | Nor2
 deriving (Ord, Eq, Show)

-- | The integer variables:
-- forall a b. 0 <= F a b <= 1 :: Z
--                  F a b == 0 iff a and b are fused
data VZ
 = F Node Node
 deriving (Ord, Eq, Show)

-- | The real variables:
-- forall a b. F a b == 0 ==> O a == O b
--                            O a >  O b if edge from a to b
data VR
 = O Node
 deriving (Ord, Eq, Show)


problem1 :: Direction -> Program VZ VR IntDouble
problem1 dir
 = program dir
           objective
           constraints
           bounds

--Minimise	5f(sum1, ys)		+	1f(sum1, sum2)
--		+	5f(sum1, nor2)	+	5f(ys, sum2)
--		+	5f(ys, nor1)		+	5f(sum2, nor1)
--		+	5f(nor1, nor2)
objective
 =    f100 Sum1 Ys     .+. f1   Sum1 Sum2
 .+.  f100 Sum1 Nor2   .+. f100 Ys   Sum2
 .+.  f100 Ys   Nor1   .+. f1   Sum2 Nor1
 .+.  f100 Nor1 Nor2

--Subject to	
--	   f(sum1, ys) 					≤ 				f(sum1, sum2)
--	   f(sum2, ys)					≤ 				f(sum1, sum2)
--	-5f(sum1, ys)		≤ o(ys)	- o(sum1)	≤ 5f(sum1, ys)
--	-5f(sum1, sum2)	≤ o(sum2)	- o(sum1)	≤ 5f(sum1, sum2)
--	1f(ys, sum2)		≤ o(sum2)	- o(ys)		≤ 5f(ys, sum2)
--	-5f(nor1, nor2)	≤ o(nor2)	- o(nor1)	≤ 5f(nor1, nor2)
--						    o(sum1)	< o(nor1)
--						    o(sum2)	< o(nor2)
--
constraints
 =    filt Sum1 Sum2 Ys
 :&&  filt Sum2 Nor1 Ys
 :&&  odiff (-5) Sum1 Ys    5
 :&&  odiff (-5) Sum1 Sum2  5
 :&&  odiff   1  Ys   Sum2  5
 :&&  odiff (-5) Ys   Nor1  5
 :&&  odiff (-5) Nor1 Nor2  5
 :&&  odiff (-5) Sum1 Nor2  5
 :&&  odiff (-5) Sum2 Nor1  5
 :&&  o Sum1 `lt` o Nor1
 :&&  o Sum2 `lt` o Nor2
 where

  o  = r1 . O

  lt a b = a .+. c1 :<= b

  filt a b c
   =   f1 a c      :<= f1 a b
   :&& f1 b c      :<= f1 a b

  odiff p a b q
   = Between (p *. f1 a b) (o b .-. o a) (q *. f1 a b)

bounds
 = [ binary $ F Sum1 Sum2
   , binary $ F Sum1 Ys
   , binary $ F Sum1 Nor2
   , binary $ F Ys   Sum2
   , binary $ F Nor1 Ys
   , binary $ F Nor1 Sum2
   , binary $ F Nor1 Nor2
   ]

f100 :: Node -> Node -> Linear VZ VR IntDouble KZ
f100 a b
 = 100 *. f1 a b

f1 :: Node -> Node -> Linear VZ VR IntDouble KZ
f1 a b
 = z1 $ F (min a b) (max a b)


clustering :: IO ()
clustering
 = do   solve_problem problem1
        putStr (show $ C.program $ problem1 Minimise)