{- 
 - 	Monadic Constraint Programming
 - 	http://www.cs.kuleuven.be/~toms/Haskell/
 - 	Tom Schrijvers & Pieter Wuille
 -}



{-# LANGUAGE StandaloneDeriving #-}

{-# LANGUAGE TypeSynonymInstances #-}

{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE FlexibleContexts #-}



module Control.CP.FD.Model (

  Model,

  ModelIntTerm(..),

  ModelBoolTerm(..),

  ModelColTerm(..),

  ModelFunctions(..),

  ModelInt,  ToModelInt(..), ModelIntArg,

  ModelCol,  ToModelCol(..), ModelColArg,

  ModelBool, ToModelBool(..), ModelBoolArg,

  modelVariantInt, modelVariantBool, modelVariantCol,

  ModelTermType(..),

  showModel,

  cte,

) where



import Data.Expr.Data

import Data.Expr.Util

import Data.Expr.Sugar



data ModelIntTerm t = 

    ModelIntVar Int

  | ModelIntPar Int

  deriving (Show)



data ModelColTerm t = 

    ModelColVar Int

  | ModelColPar Int

  deriving (Show)



data ModelBoolTerm t = 

    ModelBoolVar Int

  | ModelBoolPar Int

  | ModelExtra t

  deriving (Show)



data ModelFunctions =

    ForNewBool (ModelBoolExpr ModelFunctions -> Model)

  | ForNewInt (ModelIntExpr ModelFunctions -> Model)

  | ForNewCol (ModelColExpr ModelFunctions -> Model)



data ModelIntros =

     NewBool Int FlatModel

   | NewInt Int FlatModel

   | NewCol Int FlatModel

   deriving (Show,Eq)



instance Ord ModelIntros where

  compare (NewBool n1 m1) (NewBool n2 m2) = compare n1 n2 <<>> compare m1 m2

  compare (NewBool _ _) _ = LT

  compare _ (NewBool _ _) = GT

  compare (NewInt n1 m1) (NewInt n2 m2) = compare n1 n2 <<>> compare m1 m2

  compare (NewInt _ _) _ = LT

  compare _ (NewInt _ _) = GT

  compare (NewCol n1 m1) (NewCol n2 m2) = compare n1 n2 <<>> compare m1 m2



instance Show ModelFunctions where

  show (ForNewBool f) = show $ explicate (-999999) $ f $ BoolTerm $ ModelBoolVar (-1000000)

  show (ForNewInt f) = show $ explicate (-1999999) $ f $ Term $ ModelIntVar (-2000000)

  show (ForNewCol f) = show $ explicate (-2999999) $ f $ ColTerm $ ModelColVar (-3000000)

  

instance Eq ModelFunctions where

  a==b = False



instance Ord ModelFunctions where

  compare _ _ = error "Unable to compare model functions"



-- instance Show Model where 

--   show x = show $ explicate 0 x



deriving instance Eq t => Eq (ModelBoolTerm t)

deriving instance Ord t => Ord (ModelBoolTerm t)

deriving instance Eq t => Eq (ModelIntTerm t)

deriving instance Ord t => Ord (ModelIntTerm t)

deriving instance Eq t => Eq (ModelColTerm t)

deriving instance Ord t => Ord (ModelColTerm t)



type ModelIntExpr t       = Expr        (ModelIntTerm  t) (ModelColTerm  t) (ModelBoolTerm  t)

type ModelBoolExpr t      = BoolExpr    (ModelIntTerm  t) (ModelColTerm  t) (ModelBoolTerm  t)

type ModelColExpr t       = ColExpr     (ModelIntTerm  t) (ModelColTerm  t) (ModelBoolTerm  t)



type ModelInt = ModelIntExpr ModelFunctions

type ModelBool = ModelBoolExpr ModelFunctions

type ModelCol = ModelColExpr ModelFunctions



type ModelIntArg = ModelIntTerm ModelFunctions

type ModelBoolArg = ModelBoolTerm ModelFunctions

type ModelColArg = ModelColTerm ModelFunctions



type FlatModelInt = ModelIntExpr ModelIntros

type FlatModelBool = ModelBoolExpr ModelIntros

type FlatModelCol = ModelColExpr ModelIntros



type Model = ModelBool

type FlatModel = FlatModelBool



explicate :: Int -> Model -> FlatModel

explicate num mod = boolTransformEx (it,ct,bt,iit,ict,ibt) mod

  where it (ModelIntVar i) = Term $ ModelIntVar i

        it (ModelIntPar i) = Term $ ModelIntPar i

        ct (ModelColVar i) = ColTerm $ ModelColVar i

        ct (ModelColPar i) = ColTerm $ ModelColPar i

        iit (ModelIntVar i) = Term $ ModelIntVar i

        iit (ModelIntPar i) = Term $ ModelIntPar i

        ict (ModelColVar i) = ColTerm $ ModelColVar i

        ict (ModelColPar i) = ColTerm $ ModelColPar i

        ibt (ModelBoolVar i) = BoolTerm $ ModelBoolVar i

        ibt (ModelBoolPar i) = BoolTerm $ ModelBoolPar i

        bt (ModelBoolVar i) = BoolTerm $ ModelBoolVar i

        bt (ModelBoolPar i) = BoolTerm $ ModelBoolPar i

        bt (ModelExtra (ForNewBool f)) = BoolTerm $ ModelExtra $ NewBool num $ explicate (num+1) $ f $ BoolTerm $ ModelBoolVar num

        bt (ModelExtra (ForNewInt f)) = BoolTerm $ ModelExtra $ NewInt num $ explicate (num+1) $ f $ Term $ ModelIntVar num

        bt (ModelExtra (ForNewCol f)) = BoolTerm $ ModelExtra $ NewCol num $ explicate (num+1) $ f $ ColTerm $ ModelColVar num



flatten :: Model -> FlatModel

flatten = explicate 0



showModel :: Model -> String

showModel = show . flatten



variantIntTerm :: ModelIntTerm a -> Bool

variantIntTerm (ModelIntVar _) = True

variantIntTerm (ModelIntPar _) = False



variantBoolTerm :: ModelBoolTerm a -> Bool

variantBoolTerm (ModelBoolVar _) = True

variantBoolTerm (ModelBoolPar _) = False

variantBoolTerm (ModelExtra _) = True



variantColTerm :: ModelColTerm a -> Bool

variantColTerm (ModelColVar _) = True

variantColTerm (ModelColPar _) = False



modelVariantInt  :: ModelIntExpr x -> Bool

modelVariantInt  =     property variantIntTerm variantColTerm variantBoolTerm

modelVariantCol  :: ModelColExpr x -> Bool

modelVariantCol  =  colProperty variantIntTerm variantColTerm variantBoolTerm

modelVariantBool :: ModelBoolExpr x -> Bool

modelVariantBool = boolProperty variantIntTerm variantColTerm variantBoolTerm



newBool :: (ModelBool -> Model) -> Model

newBool = boolSimplify . BoolTerm . ModelExtra . ForNewBool



newInt :: (ModelInt -> Model) -> Model

newInt = boolSimplify . BoolTerm . ModelExtra . ForNewInt



newCol :: (ModelCol -> Model) -> Model

newCol = boolSimplify . BoolTerm . ModelExtra . ForNewCol



class ModelTermType s where

  newModelTerm :: (s -> Model) -> Model



instance ModelTermType ModelBool where

  newModelTerm = newBool



instance ModelTermType ModelInt where

  newModelTerm = newInt



instance ModelTermType ModelCol where

  newModelTerm = newCol



cte :: Integral a => a -> ModelInt

cte = Const . toInteger



class ToModelBool t where

  asBool :: t -> ModelBool



class ToModelInt t where

  asExpr :: t -> ModelInt



class ToModelCol t where

  asCol :: t -> ModelCol



instance ToExpr (ModelIntTerm ModelFunctions) (ModelColTerm ModelFunctions) (ModelBoolTerm ModelFunctions) t => ToModelInt t where

  asExpr = toExpr



instance ToBoolExpr (ModelIntTerm ModelFunctions) (ModelColTerm ModelFunctions) (ModelBoolTerm ModelFunctions) t => ToModelBool t where

  asBool = toBoolExpr



instance ToColExpr (ModelIntTerm ModelFunctions) (ModelColTerm ModelFunctions) (ModelBoolTerm ModelFunctions) t => ToModelCol t where

  asCol = toColExpr