{- 
 - 	Monadic Constraint Programming
 - 	http://www.cs.kuleuven.be/~toms/MCP/
 - 	Pieter Wuille
 -}

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Control.CP.FD.Decompose (
  DecompData,
  baseDecompData,
  decompose,
  decomposeEx,
  decompBoolLookup,
  decompIntLookup,
  decompColLookup,
) where

import Data.Map (Map)
import qualified Data.Map as Map

import Data.Set (Set)
import qualified Data.Set as Set

import Control.Monad.State.Lazy hiding (state)

import Control.CP.Debug
import Data.Expr.Data
import Data.Expr.Util
import Control.CP.FD.Graph
import Control.CP.FD.Model

data DecompData = DecompData {
  -- expressions currently accessible as variables
  cseMapBool :: Map ModelBool EGVarId,
  cseMapInt :: Map ModelInt EGVarId,
  cseMapCol :: Map ModelCol EGVarId,
  -- parent graph's data
  cseParent :: Maybe DecompData,
  -- expressions imported from parent graph
  cseImports :: ([ModelBool],[ModelInt],[ModelCol]),
  -- counter for unique id's
  cseNIds :: Int,
  -- locked nodes (already shown to the caller, and cannot be unified/replaced anymore)
  cseLocked :: EGTypeData (Set EGVarId),
  -- level of nesting
  cseLevel :: Int
}

decompBoolLookup :: DecompData -> ModelBool -> Maybe EGVarId
decompBoolLookup d v = Map.lookup v $ cseMapBool d

decompIntLookup :: DecompData -> ModelInt -> Maybe EGVarId
decompIntLookup d v = Map.lookup v $ cseMapInt d

decompColLookup :: DecompData -> ModelCol -> Maybe EGVarId
decompColLookup d v = Map.lookup v $ cseMapCol d

-- | base instance of DecompData
baseDecompData :: DecompData
baseDecompData = DecompData {
  cseMapBool = Map.empty,
  cseMapInt = Map.empty,
  cseMapCol = Map.empty,
  cseParent = Nothing,
  cseImports = ([],[],[]),
  cseNIds = 0,
  cseLevel = 0,
  cseLocked = baseTypeData (Set.empty)
}

-- | the state for the DCMonad
data DCState = DCState {
  dcsData :: DecompData,
  dcsModel :: EGModel
}

-- | base state for the DCMonad
baseDCState = DCState {
  dcsData = baseDecompData,
  dcsModel = baseGraph
}

-- | definition of a decomposer monad
newtype DCMonad a = DCMonad { state :: State DCState a }
  deriving (Monad, MonadState DCState)

-- | transform an expression into a graph, taking and returning an updated state
decomposeEx :: DecompData -> Int -> Model -> ([ModelBool],[ModelInt],[ModelCol]) -> Maybe EGModel -> (DecompData,EGModel,Int)
decomposeEx dat vars model (lb,li,lc) prev = 
  let prog = do
        s1 <- get
        put $ s1 { dcsData = (dcsData s1) { cseNIds = max vars (cseNIds $ dcsData s1) } }
        decomposeBoolEx (Just True) model
        mapM_ decomposeBool lb
        mapM_ decomposeInt li
        mapM_ decomposeCol lc
        s2 <- get
        put $ s2 { dcsData = (dcsData s2) { cseLocked = egTypeDataMap (\f -> Set.fromList $ Map.keys $ f $ egmLinks $ dcsModel s2) } }
      pmodel = case prev of
        Nothing -> baseGraph
        Just x -> x
      res = execState (state prog) $ DCState { dcsData = dat, dcsModel = pmodel }
      in (dcsData res,dcsModel res,cseNIds $ dcsData res)

-- | easier version of decomposeEx that does not require or return a state
decompose :: Model -> EGModel
decompose x = (\(_,x,_) -> x) $ decomposeEx baseDecompData 0 x ([],[],[]) Nothing

-- | decomposition states can be stacked, this function tests whether a property hold
-- for a state or any of its parents
stateProperty :: (DecompData -> Bool) -> DecompData -> Bool
stateProperty f s = if f s then True else case (cseParent s) of
  Just p -> stateProperty f p
  _ -> False

newVar :: EGVarType -> DCMonad EGVarId
newVar typ = do
  s <- get
  let (nv,nm) = addNode typ (dcsModel s)
  put $ s { dcsModel = nm }
  return nv

importBool :: Maybe Bool -> ModelBool -> DCMonad EGVarId
importBool val expr = do
  n <- newBoolVar val expr
  s <- get
  if cseLevel (dcsData s) == 0
    then error $ "Boolean expression (value="++(show val)++") escapes: " ++ (show expr)
    else do
      let ni = length $ (\(x,_,_)->x) $ cseImports $ dcsData s
      put $ s { dcsData = (dcsData s) { cseImports = (\(a,b,c) -> (a++[expr],b,c)) (cseImports $ dcsData s) } }
      addConstraint (EGBoolExtern ni) ([n],[],[])
      return n

importInt :: ModelInt -> DCMonad EGVarId
importInt expr = do
  n <- newIntVar expr
  s <- get
  if cseLevel (dcsData s) == 0
    then error $ "Integer expression escapes: " ++ (show expr)
    else do
      let ni = length $ (\(_,x,_)->x) $ cseImports $ dcsData s
      put $ s { dcsData = (dcsData s) { cseImports = (\(a,b,c) -> (a,b++[expr],c)) (cseImports $ dcsData s) } }
      addConstraint (EGIntExtern ni) ([],[n],[])
      return n

importCol :: ModelCol -> DCMonad EGVarId
importCol expr = do
  n <- newColVar expr
  s <- get
  if cseLevel (dcsData s) == 0
    then error $ "Collection expression escapes: " ++ (show expr)
    else do
      let ni = length $ (\(_,_,x)->x) $ cseImports $ dcsData s
      put $ s { dcsData = (dcsData s) { cseImports = (\(a,b,c) -> (a,b,c++[expr])) (cseImports $ dcsData s) } }
      addConstraint (EGColExtern ni) ([],[],[n])
      return n

unifyVars :: EGVarType -> EGVarId -> EGVarId -> DCMonad Bool
unifyVars typ v1 v2 = do
  s <- get
  let rm = egTypeGet typ $ cseLocked $ dcsData s
      i1 = Set.member v1 rm
      i2 = Set.member v2 rm
  if (i1 && i2)
    then return False  -- if both nodes are locked, unification is not possible
    else if i1
      then unifyVars typ v2 v1 -- if only i1 is locked, unify v2 with v1 instead of v1 with v2
      else do -- otherwise, really unify
        let nm = unifyNodes typ v1 v2 (dcsModel s)
        case typ of
          EGBoolType -> put $ s { dcsModel = nm, dcsData = (dcsData s) { cseMapBool = Map.map tran $ cseMapBool $ dcsData s } }
          EGIntType  -> put $ s { dcsModel = nm, dcsData = (dcsData s) { cseMapInt = Map.map tran $ cseMapInt $ dcsData s } }
          EGColType  -> put $ s { dcsModel = nm, dcsData = (dcsData s) { cseMapCol = Map.map tran $ cseMapCol $ dcsData s } }
        return True
  where tran = unifyIds v1 v2

addConstraint :: EGConstraintSpec -> ([EGVarId],[EGVarId],[EGVarId]) -> DCMonad ()
addConstraint spec (lb,li,lc) = do
  s <- get
  let nm = addEdge spec (EGTypeData { boolData=lb, intData=li, colData=lc }) (dcsModel s)
  put $ s { dcsModel = nm }

newBoolVar :: Maybe Bool -> ModelBool -> DCMonad EGVarId
newBoolVar val expr = do
  n <- case val of
    Nothing -> newVar EGBoolType
    Just x -> decomposeBool $ BoolConst x
  s <- get
  let nc = Map.insert expr n (cseMapBool $ dcsData s)
  put $ s { dcsData = (dcsData s) { cseMapBool = nc } }
  return n

newIntVar :: ModelInt -> DCMonad EGVarId
newIntVar expr = do
  n <- newVar EGIntType
  s <- get
  let nc = Map.insert expr n (cseMapInt $ dcsData s)
  put $ s { dcsData = (dcsData s) { cseMapInt = nc } }
  return n

newColVar :: ModelCol -> DCMonad EGVarId
newColVar expr = do
  n <- newVar EGColType
  s <- get
  let nc = Map.insert expr n (cseMapCol $ dcsData s)
  put $ s { dcsData = (dcsData s) { cseMapCol = nc } }
  return n

decomposeSubmodel :: (Int,Int,Int) -> (([ModelBool],[ModelInt],[ModelCol]) -> DCMonad ()) -> DCMonad (EGModel,([EGVarId],[EGVarId],[EGVarId]))
decomposeSubmodel (nArgsBool,nArgsInt,nArgsCol) m = do
  oArgsBool <- mapM (const $ nextId >>= (\x -> return $ BoolTerm $ ModelBoolVar $ x)) [1..nArgsBool]
  oArgsInt  <- mapM (const $ nextId >>= (\x -> return $ Term     $ ModelIntVar  $ x)) [1..nArgsInt]
  oArgsCol  <- mapM (const $ nextId >>= (\x -> return $ ColTerm  $ ModelColVar  $ x)) [1..nArgsCol]
  s <- get
  let sm = m (oArgsBool,oArgsInt,oArgsCol)
      ns = execState (state sm) $ baseDCState { dcsData = (dcsData baseDCState) { cseLevel = 1 + (cseLevel $ dcsData s), cseNIds = 0+(cseNIds $ dcsData s), cseParent = Just $ dcsData s } }
  put $ s { dcsData = (dcsData s) { cseNIds = 0+(cseNIds $ dcsData ns) } }
  argsBool <- mapM decomposeBool $ (\(x,_,_) -> x) $ cseImports $ dcsData ns
  argsInt <-  mapM decomposeInt  $ (\(_,x,_) -> x) $ cseImports $ dcsData ns
  argsCol <-  mapM decomposeCol  $ (\(_,_,x) -> x) $ cseImports $ dcsData ns
  return (dcsModel ns, (argsBool,argsInt,argsCol))

constIntTrans :: ModelIntTerm ModelFunctions -> EGParTerm
constIntTrans (ModelIntPar x) = EGPTParam x
constIntTrans x = error $ "non-constant int transform: "++(show x)
constColTrans :: ModelColTerm ModelFunctions -> EGParColTerm
constColTrans (ModelColPar x) = EGPTColParam x
constColTrans x = error $ "non-constant col transform: "++(show x)
constBoolTrans :: ModelBoolTerm ModelFunctions -> EGParBoolTerm
constBoolTrans (ModelBoolPar x) = EGPTBoolParam x
constBoolTrans x = error $ "non-constant bool transform: "++(show x)
constIntTransInv :: EGParTerm -> ModelIntTerm ModelFunctions
constIntTransInv (EGPTParam x) = ModelIntPar x
constColTransInv :: EGParColTerm -> ModelColTerm ModelFunctions
constColTransInv (EGPTColParam x) = ModelColPar x
constBoolTransInv :: EGParBoolTerm -> ModelBoolTerm ModelFunctions
constBoolTransInv (EGPTBoolParam x) = ModelBoolPar x

constTrans = (constIntTrans,constColTrans,constBoolTrans,constIntTransInv,constColTransInv,constBoolTransInv)
invConstTrans = (constIntTransInv,constColTransInv,constBoolTransInv,constIntTrans,constColTrans,constBoolTrans)

dependenceTester d = 
  (
    \x -> if Map.member x (cseMapInt d) && not (x `elem` ((\(_,x,_) -> x) $ cseImports d)) then Just True else Nothing,
    \x -> if Map.member x (cseMapCol d) && not (x `elem` ((\(_,_,x) -> x) $ cseImports d)) then Just True else Nothing,
    \x -> case x of
      BoolTerm (ModelExtra _) -> Just True
      _ -> if Map.member x (cseMapBool d) && not (x `elem` ((\(x,_,_) -> x) $ cseImports d)) then Just True else Nothing
  )

dependentIntExpr :: DecompData -> ModelInt -> Bool
dependentIntExpr d = propertyEx $ dependenceTester d
dependentBoolExpr :: DecompData -> ModelBool -> Bool
dependentBoolExpr d = boolPropertyEx $ dependenceTester d
dependentColExpr :: DecompData -> ModelCol -> Bool
dependentColExpr d = colPropertyEx $ dependenceTester d

nextId :: DCMonad Int
nextId = do
  s <- get
  let n = cseNIds $ dcsData s
  put $ s { dcsData = (dcsData s) { cseNIds = n + 1 } }
  return n

-----------------------------------------
-- | Decomposition of special values | --
-----------------------------------------

decomposeBool :: ModelBool -> DCMonad EGVarId
decomposeBool expr = do
  (Just x) <- decomposeBoolEx Nothing expr
  return x

decomposeBoolEx :: Maybe Bool -> ModelBool -> DCMonad (Maybe EGVarId)
decomposeBoolEx val expr = do
  s <- get
  debug ("decomposeBoolEx [level "++(show $ cseLevel $ dcsData s)++"] val="++(show val)++" expr="++(show expr)) $ return ()
  let key = expr
  case Map.lookup key (cseMapBool $ dcsData s) of    -- local variable or already locally decomposed expression
    Just i -> do
      debug ("decomposeBoolEx [level "++(show $ cseLevel $ dcsData s)++"] val="++(show val)++" expr="++(show expr)++": already decomposed: "++(show i)) $ return ()
      return $ Just i
    Nothing -> if (modelVariantBool expr)
      then do
        if (stateProperty (Map.member key . cseMapBool) $ dcsData s) && not (dependentBoolExpr (dcsData s) expr) && (cseLevel $ dcsData s) > 0
          then do   -- Loop Invariant Code Motion
            debug ("decomposeBoolEx: [level "++(show $ cseLevel $ dcsData s)++"] [variant indep] "++(show expr)) $ return ()
            n <- importBool val expr
            return $ Just n
          else do
            debug ("decomposeBoolEx: [level "++(show $ cseLevel $ dcsData s)++"] [variant dep] "++(show expr)) $ return ()
            realDecomposeBoolEx val expr
        else do
          debug ("decomposeBoolEx: [level "++(show $ cseLevel $ dcsData s)++"] [invariant] "++(show expr)) $ return ()
          n <- newBoolVar val expr
          let tr = boolTransform constTrans expr
          addConstraint (EGBoolValue tr) ([n],[],[])
          return $ Just n

decomposeInt :: ModelInt -> DCMonad EGVarId
decomposeInt expr = do
  s <- get
  debug ("decomposeInt [level "++(show $ cseLevel $ dcsData s)++"] expr="++(show expr)) $ return ()
  let key = expr
  case Map.lookup key (cseMapInt $ dcsData s) of
    Just i -> return i
    Nothing -> if (modelVariantInt expr)
      then if (stateProperty (Map.member key . cseMapInt) $ dcsData s) && not (dependentIntExpr (dcsData s) expr) && (cseLevel $ dcsData s) > 0
        then do
          debug ("decomposeInt: [level "++(show $ cseLevel $ dcsData s)++"] [variant indep] "++(show expr)) $ return ()
          importInt expr
        else do
          debug ("decomposeInt: [level "++(show $ cseLevel $ dcsData s)++"] [variant dep] "++(show expr)) $ return ()
          realDecomposeInt expr
      else do
        debug ("decomposeInt: [level "++(show $ cseLevel $ dcsData s)++"] [invariant] "++(show expr)) $ return ()
        n <- newIntVar expr
        let tr = transform constTrans expr
        addConstraint (EGIntValue tr) ([],[n],[])
        return n

decomposeCol :: ModelCol -> DCMonad EGVarId
decomposeCol expr = do
  s <- get
  debug ("decomposeCol [level "++(show $ cseLevel $ dcsData s)++"] expr="++(show expr)) $ return ()
  let key = expr
  case Map.lookup key (cseMapCol $ dcsData s) of
    Just i -> return i
    Nothing -> if (modelVariantCol expr)
      then if (stateProperty (Map.member key . cseMapCol) $ dcsData s) && not (dependentColExpr (dcsData s) expr) && (cseLevel $ dcsData s) > 0
        then do
          debug ("decomposeCol: [level "++(show $ cseLevel $ dcsData s)++"] [variant indep] "++(show expr)) $ return ()
          importCol expr
        else do 
          debug ("decomposeCol: [level "++(show $ cseLevel $ dcsData s)++"] [variant dep] "++(show expr)) $ return ()
          realDecomposeCol expr
      else do
        debug ("decomposeCol: [level "++(show $ cseLevel $ dcsData s)++"] [invariant] "++(show expr)) $ return ()
        n <- newColVar expr
        let tr = colTransform constTrans expr
        addConstraint (EGColValue tr) ([],[],[n])
        return n


------------------------------------------
-- | Real decomposers for expressions | --
------------------------------------------

realDecomposeBoolEx :: Maybe Bool -> ModelBool -> DCMonad (Maybe EGVarId)
realDecomposeBoolEx val expr = case expr of
  BoolTerm (ModelExtra (ForNewBool f)) -> do
    n <- nextId
    let v = BoolTerm $ ModelBoolVar n
    newBoolVar Nothing v
    decomposeBoolEx val $ f v
  BoolTerm (ModelExtra (ForNewInt f)) -> do
    n <- nextId
    let v = Term $ ModelIntVar n
    newIntVar v
    decomposeBoolEx val $ f v
  BoolTerm (ModelExtra (ForNewCol f)) -> do
    n <- nextId
    let v = ColTerm $ ModelColVar n
    newColVar v
    decomposeBoolEx val $ f v
  BoolTerm (ModelBoolVar i) -> do
    n <- newBoolVar val expr
    return $ Just n
  BoolCond c t f -> case val of
    Just True -> do
      dc <- decomposeBool c
      di <- decomposeBool $ boolSimplify $ BoolNot c
      ct <- decomposeBool (BoolConst True)
      if (t /= BoolConst True) 
        then do
          dt <- decomposeBool t
          addConstraint EGCondEqual ([dc,dt,ct],[],[])
        else return ()
      if (f /= BoolConst True)
        then do
          df <- decomposeBool f
          addConstraint EGCondEqual ([di,df,ct],[],[])
        else return ()
      return Nothing
    _ -> error "No reified boolean conditional exists"
  BoolAnd a b -> case val of
    Just True -> do
      decomposeBoolEx val a
      decomposeBoolEx val b
      return Nothing
    _ -> do
      n <- newBoolVar val expr
      ad <- decomposeBool a
      bd <- decomposeBool b
      addConstraint EGAnd ([n,ad,bd],[],[])
      return $ Just n
  BoolOr a b -> case val of
    Just False -> do
      decomposeBoolEx val a
      decomposeBoolEx val b
      return Nothing
    _ -> do
      n <- newBoolVar val expr
      ad <- decomposeBool a
      bd <- decomposeBool b
      addConstraint EGOr ([n,ad,bd],[],[])
      return $ Just n
  BoolNot a -> case val of
    Just True -> do
      decomposeBoolEx (Just False) a
      return Nothing
    Just False -> do
      decomposeBoolEx (Just True) a
      return Nothing
    _ -> do
      n <- newBoolVar val expr
      ad <- decomposeBool a
      addConstraint EGNot ([n,ad],[],[])
      return $ Just n
  Rel a r b -> case (r,val) of
    (EREqual,Just True) -> do
      ad <- decomposeInt a
      bd <- decomposeInt b
      res <- unifyVars EGIntType ad bd
      if res
        then return Nothing
        else do
          n <- decomposeBool (BoolConst True)
          addConstraint EGEqual ([n],[ad,bd],[])
          return Nothing
    (ERDiff,Just False) -> do
      ad <- decomposeInt a 
      bd <- decomposeInt b
      res <- unifyVars EGIntType ad bd
      if res
        then return Nothing
        else do
          n <- decomposeBool (BoolConst True)
          addConstraint EGEqual ([n],[ad,bd],[])
          return Nothing
    _ -> do
      n <- newBoolVar val expr
      ad <- decomposeInt a
      bd <- decomposeInt b
      addConstraint (case r of
          EREqual -> EGEqual
          ERDiff -> EGDiff
          ERLess -> EGLess True
        ) ([n],[ad,bd],[])
      return $ Just n
  ColEqual a b -> case val of
    Just True -> do
      ad <- decomposeCol a
      bd <- decomposeCol b
      res <- unifyVars EGColType ad bd
      if not res
        then error "unification of collections failed"
        else return Nothing
    _ -> error "No negated or reified version of ColEqual exists"
  AllDiff b c -> case val of
    Just True -> do
      ac <- decomposeCol c
      addConstraint (EGAllDiff b) ([],[],[ac])
      return Nothing
    _ -> error "No negated or reified version of AllDiff exists"
  Sorted b c -> case val of
    Just True -> do
      ac <- decomposeCol c
      addConstraint (EGSorted b) ([],[],[ac])
      return Nothing
    _ -> error "No negated or reified version of Sorted exists"
  Dom i c -> case val of
    Just True -> do
      ac <- decomposeCol c
      ai <- decomposeInt i
      addConstraint EGDom ([],[ai],[ac])
      return Nothing
    _ -> error "No negated or reified version of Dom exists"
  BoolEqual a b -> case val of
    Just True -> do
      ad <- decomposeBool a
      bd <- decomposeBool b
      res <- unifyVars EGBoolType ad bd
      if res
        then return Nothing
        else do
          n <- decomposeBool (BoolConst True)
          addConstraint EGEquiv ([n,ad,bd],[],[])
          return Nothing
    _ -> do
      n <- newBoolVar val expr
      ad <- decomposeBool a
      bd <- decomposeBool b
      addConstraint EGEquiv ([n,ad,bd],[],[])
      return $ Just n
--  BoolAll f (ColRange l h) -> do
--    ld <- decomposeInt l
--    hd <- decomposeInt h
--    n <- newBoolVar val expr
--    (smod,(argsBool,argsInt,argsCol)) <- decomposeSubmodel (0,1,0) $ \([],[oarg],[]) -> do
--      let sexpr = f oarg
--      arg <- newIntVar oarg
--      debug ("BoolAllC: arg="++(show arg)++" oarg="++(show oarg)) $ return ()
--      addConstraint (EGIntExtern $ -1) ([],[arg],[])
--      case val of
--        Just True -> do
--          decomposeBoolEx (Just True) sexpr
--          return ()
--        _ -> do
--          res <- decomposeBool sexpr
--          addConstraint (EGBoolExtern $ -1) ([res],[],[])
--    let force = case val of
--                Just True -> True
--                _ -> False
--    addConstraint (EGAllC smod (length argsBool,length argsInt,length argsCol) force) ([n]++argsBool,[ld,hd]++argsInt,argsCol)
--    return $ Just n
--  BoolAny f (ColRange l h) -> do
--    ld <- decomposeInt l
--    hd <- decomposeInt h
--    n <- newBoolVar val expr
--    (smod,(argsBool,argsInt,argsCol)) <- decomposeSubmodel (0,1,0) $ \([],[oarg],[]) -> do
--      let sexpr = f oarg
--      arg <- newIntVar oarg
--      addConstraint (EGIntExtern $ -1) ([],[arg],[])
--      case val of
--        Just False -> do
--          decomposeBoolEx (Just False) sexpr
--          return ()
--        _ -> do
--          res <- decomposeBool sexpr
--          addConstraint (EGBoolExtern $ -1) ([res],[],[])
--    let force = case val of
--                Just False -> True
--                _ -> False
--    addConstraint (EGAnyC smod (length argsBool,length argsInt,length argsCol) force) ([n]++argsBool,[ld,hd]++argsInt,argsCol)
--    return $ Just n
  BoolAll f c -> do
    cd <- decomposeCol c
    n <- newBoolVar val expr
    (smod,(argsBool,argsInt,argsCol)) <- decomposeSubmodel (0,1,0) $ \([],[oarg],[]) -> do
      let sexpr = f oarg
      arg <- newIntVar oarg
      addConstraint (EGIntExtern $ -1) ([],[arg],[])
      case val of
        Just True -> do   {- in case a BoolAll itself must hold, each submodel must hold too -}
          decomposeBoolEx (Just True) sexpr
          return ()
        _ -> do
          res <- decomposeBool sexpr
          addConstraint (EGBoolExtern $ -1) ([res],[],[])
    let force = 
          case val of
            Just True -> True
            _ -> False
    addConstraint (EGAll smod (length argsBool,length argsInt,length argsCol) force) ([n] ++ argsBool,argsInt,[cd] ++ argsCol)
    return $ Just n
  BoolAny f c -> do
    cd <- decomposeCol c
    n <- newBoolVar val expr
    (smod,(argsBool,argsInt,argsCol)) <- decomposeSubmodel (0,1,0) $ \([],[oarg],[]) -> do
      let sexpr = f oarg
      arg <- newIntVar oarg
      addConstraint (EGIntExtern $ -1) ([],[arg],[])
      case val of
        Just False -> do   {- in case a BoolAny itself may not hold, each submodel may not hold either -}
          decomposeBoolEx (Just False) sexpr
          return ()
        _ -> do
          res <- decomposeBool sexpr
          addConstraint (EGBoolExtern $ -1) ([res],[],[])
    let force = 
          case val of
            Just False -> True
            _ -> False
    addConstraint ((if force then EGAll else EGAny) smod (length argsBool,length argsInt,length argsCol) force) ([n] ++ argsBool,argsInt,[cd] ++ argsCol)
    return $ Just n
  _ -> error $ "Unable to decompose boolean expression: " ++ (show expr) ++ "(== " ++ (show val) ++ ")"

realDecomposeInt :: ModelInt -> DCMonad EGVarId
realDecomposeInt expr = do
  let pIntOp a x b = do
        n <- newIntVar expr
        ad <- decomposeInt a
        bd <- decomposeInt b
        addConstraint x ([],[n,ad,bd],[])
        return n
  case expr of
    Term (ModelIntVar i) -> newIntVar expr
    Plus a b -> pIntOp a EGPlus b
    Minus a b -> pIntOp a EGMinus b
    Mult a b -> pIntOp a EGMult b
    Div a b -> pIntOp a EGDiv b
    Mod a b -> pIntOp a EGMod b
    Abs a -> do
      n <- newIntVar expr
      ad <- decomposeInt a
      addConstraint EGAbs ([],[n,ad],[])
      return n
    At a b -> do
      n <- newIntVar expr
      ad <- decomposeCol a
      bd <- decomposeInt b
      addConstraint EGAt ([],[n,bd],[ad])
      return n
    ColSize a -> do
      n <- newIntVar expr
      ad <- decomposeCol a
      addConstraint EGSize ([],[n],[ad])
      return n
    Channel a -> do
      n <- newIntVar expr
      ad <- decomposeBool a
      addConstraint EGChannel ([ad],[n],[])
      return n
    Cond c t f -> do
      n <- newIntVar expr
      cd <- decomposeBool c
      td <- decomposeInt t
      fd <- decomposeInt f
      addConstraint EGCondInt ([cd],[n,td,fd],[])
      return n
    Fold f i c -> do
      cd <- decomposeCol c
      id <- decomposeInt i
      n <- newIntVar expr
      (smod,(argsBool,argsInt,argsCol)) <- decomposeSubmodel (0,2,0) $ \([],[oacc,oarg],[]) -> do
        let sexpr = f oacc oarg
        acc <- newIntVar oacc
        addConstraint (EGIntExtern $ -2) ([],[acc],[])
        arg <- newIntVar oarg
        addConstraint (EGIntExtern $ -3) ([],[arg],[])
        res <- decomposeInt sexpr
        addConstraint (EGIntExtern $ -1) ([],[res],[])
      addConstraint (EGFold smod (length argsBool,length argsInt,length argsCol)) (argsBool,[n,id]++argsInt,[cd]++argsCol)
      return n
    _ -> error $ "Unable to decompose expression: " ++ (show expr)

listAll :: [a] -> (a -> Maybe b) -> Maybe [b]
listAll [] _ = Just []
listAll (a:b) f = case f a of
  Nothing -> Nothing
  Just r -> case listAll b f of
    Nothing -> Nothing
    Just x -> Just (r:x)

realDecomposeCol :: ModelCol -> DCMonad EGVarId
realDecomposeCol expr = case expr of
  ColList l -> do
    n <- newColVar expr
    ld <- mapM decomposeInt l
    addConstraint (EGList (length l)) ([],ld,[n])
    return n
  ColTerm (ModelColVar i) -> newColVar expr
  ColRange a b -> do
    n <- newColVar expr
    ad <- decomposeInt a
    bd <- decomposeInt b
    addConstraint EGRange ([],[ad,bd],[n])
    return n
  ColCat a b -> do
    n <- newColVar expr
    ad <- decomposeCol a
    bd <- decomposeCol b
    addConstraint EGCat ([],[],[n,ad,bd])
    return n
{-  ColSlice f n c -> do
    nn <- newColVar expr
    cd <- decomposeCol c
    let fd x = debug ("ColSlice: f("++(show x)++")="++(show $ f $ transform invConstTrans x)) $ transform constTrans $ f $ transform invConstTrans x
    let nd = transform constTrans n
    addConstraint (EGSlice fd nd) ([],[],[nn,cd])
    return nn -}
  ColSlice f nn c -> do
    cd <- decomposeCol c
    nd <- decomposeInt nn
    n <- newColVar expr
    (smod,(argsBool,argsInt,argsCol)) <- decomposeSubmodel (0,1,0) $ \([],[oarg],[]) -> do
      let sexpr = f oarg
      arg <- newIntVar oarg
      addConstraint (EGIntExtern $ -2) ([],[arg],[])
      res <- decomposeInt sexpr
      addConstraint (EGIntExtern $ -1) ([],[res],[])
    addConstraint (EGSlice smod (length argsBool,length argsInt,length argsCol)) (argsBool,[nd]++argsInt,[n,cd]++argsCol)
    return n
  ColMap f c -> do
    cd <- decomposeCol c
    n <- newColVar expr
    (smod,(argsBool,argsInt,argsCol)) <- decomposeSubmodel (0,1,0) $ \([],[oarg],[]) -> do
      let sexpr = f oarg
      arg <- newIntVar oarg
      addConstraint (EGIntExtern $ -2) ([],[arg],[])
      res <- decomposeInt sexpr
      addConstraint (EGIntExtern $ -1) ([],[res],[])
    addConstraint (EGMap smod (length argsBool,length argsInt,length argsCol)) (argsBool,argsInt,[n,cd]++argsCol)
    return n
  _ -> error $ "Unable to decompose collection: " ++ (show expr)