------------------------------------------------------------------------------
-- A source-level profiler for Curry
--
-- by Elvira Albert & German Vidal (UPV)
------------------------------------------------------------------------------
--
import Flat
import List
import FlatTools
import Unsafe

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

printVersion =
  do putStrLn "Curry Profiler (Version 1.1 of 23/05/2003)"
     putStrLn "(Technical University of Valencia)\n"

-- (used in getMatchedRHS to produce a safe renaming):
maxExpVars = 1000

-- special variable:
varBottom = Var (-1)

-- should some debug information be printed during profiling?
profDebug = False

-- treatment of MAIN annotations in the program to be profiled:
-- is this call a MAIN annotations?
-- the program to be profiled should incude a definition MAIN x = x 
-- and a definition like "foo = MAIN (initial goal)"

isMainAnnot (Comb ctype name args) =
  if ctype==FuncCall && length args == 1 && take 4 (reverse name) == "NIAM"
  then True  -- this is a call annotated with MAIN
  else False

-- get the annotation expression (provided that this is a MAIN annotation):
getMainAnnotExpr (Comb _ _ args) = head args

------------------------------------------------------------------------------
-- data structures used in the profiler:

data Cost = C [(Int,[Int])]

k0 = C []

-- operation to add two costs:

addCosts (C k) (C kk) = C (map (addC k) kk)

addC [] k = k
addC ((ccc1,k1):cs) (ccc2,k2) =
  if ccc1 == ccc2 then (ccc1, addCK k1 k2)
                  else addC cs (ccc2,k2)

addCK [a,b,c,d] [x,y,z,w] = [a+x,b+y,c+z,d+w]

-- operations to increment the current costs

incSteps cc (C k) = C (incStepsAux cc k)
incStepsAux cc [] = [(cc,[1,0,0,0])]
incStepsAux cc ((ccc,k):cs) = if cc==ccc then ((ccc, incS k) : cs)
                                         else (ccc,k) : incStepsAux cc cs
incS [a,b,c,d] = [a+1,b,c,d]

incCase cc (C k) = C (incCaseAux cc k)
incCaseAux cc [] = [(cc,[0,1,0,0])]
incCaseAux cc ((ccc,k):cs) = if cc==ccc then ((ccc, incC k) : cs)
                                        else (ccc,k) : incCaseAux cc cs 
incC [a,b,c,d] = [a,b+1,c,d]

incFCase cc (C k) = C (incFCaseAux cc k)
incFCaseAux cc [] = [(cc,[0,0,1,0])]
incFCaseAux cc ((ccc,k):cs) = if cc==ccc then ((ccc, incF k) : cs)
                                         else (ccc,k) : incFCaseAux cc cs 
incF [a,b,c,d] = [a,b,c+1,d]

---incFCase cc (C k) n = C (incFCaseAux cc k n)
---incFCaseAux cc [] n = [(cc,[0,0,n,0])]
---incFCaseAux cc ((ccc,k):cs) n = if cc==ccc then ((ccc, incF k n) : cs)
---                                         else (ccc,k) : incFCaseAux cc cs n
---incF [a,b,c,d] n = [a,b,c+n,d]

incApps cc (C k) e = C (incAppsAux cc k e)
incAppsAux cc [] e = [(cc,[0,0,0, size e])]
incAppsAux cc ((ccc,k):cs) e = if cc==ccc then ((ccc, incA k e) : cs)
                                          else (ccc,k) : incAppsAux cc cs e
incA [a,b,c,d] e = [a,b,c,d+(size e)]

incApps2 cc (C k) e = C (incAppsAux2 cc k e)
incAppsAux2 cc [] e = [(cc,[0,0,0,e])]
incAppsAux2 cc ((ccc,k):cs) e = if cc==ccc then ((ccc, incA2 k e) : cs)
                                           else (ccc,k) : incAppsAux2 cc cs e
incA2 [a,b,c,d] e = [a,b,c,d+e]

-- size counts the number of applications in an expression

size (Var _) = 0
size (Lit _) = 1
size (Comb _ _ es) = 1 + (length es) + sizeL es
size (Case _ e ces) = 1 + (length ces) + (size e) + (sizeBranchL ces)
size (Apply e1 e2) = 3 + (size e1) + (size e2)
size (Constr _ c) = 3 + (size c)
size (GuardedExpr _ c e) = 4 + (size e) + (size c)
size (Or e1 e2) = 3 + (size e1) + (size e2)
size (Choice e) = 2 + (size e)

sizeL [] = 0
sizeL (e:es) = (size e) + (sizeL es)

sizeBranchL [] = 0
sizeBranchL (Branch _ e : bs) = (size e) + (sizeBranchL bs)

-- data type for substitutions:
data Subst = Sub [Int] [Expr] | FSub


-- encapsulating the state during the profiling process:
-- the state contains:
-- * the list of all function declarations
-- * index for renamed variables

--data PEvalState = PEState [Expr] [FuncDecl] Int Int
data ProState = PState [FuncDecl] Int

getFuncDecls     (PState fds _) = fds
getRenamingIndex (PState _ i ) = i

-- update state with new index for renamed variables:
updateRenamingIndex :: ProState -> Int -> ProState
updateRenamingIndex (PState fds _) i = PState fds i

-- compute arity of a function symbol:
getArity :: ProState -> String -> Int
getArity pst f = getArityF (getFuncDecls pst) f

getArityF :: [FuncDecl] -> String -> Int
getArityF funs f
 | f=="+"    = 2
 | f=="-"    = 2
 | f=="*"    = 2
 | f=="<"    = 2
 | f==">"    = 2
 | f=="<="   = 2
 | f==">="   = 2
 | f=="&"    = 2
 | f=="&&"   = 2
 | f=="=:="  = 2
 | f=="=="   = 2
 | f=="if_then_else" = 3
 | f=="map"          = 2
 | f=="foldl"        = 3
 | f=="foldr"        = 3
 | f=="filter"       = 2
 | f=="iterate"      = 2
 | otherwise = findArity funs
 where
    findArity [] = error ("INTERNAL ERROR: cannot find arity of "++f)
    findArity (Func fn fa _ _ : fds) =
        if fn==f then fa else findArity fds

------------------------------------------------------------------------------
-- Main Functions..
------------------------------------------------------------------------------


-- the program starts with "profile file"; the file should contain the definitions
-- of MAIN and SCC (MAIN x = x, and SCC _ x = x), the initial goal appear in a
-- function definition like (foo = MAIN (initial goal))

profile :: String -> IO ()
profile p =
  do printVersion
     annprog <- readFlatCurry p
     let (prog,es) = getMainExprs annprog
     profile_aux p es annprog prog

-- idem, but accumulating the costs of previous branches..
profileAcc :: String -> IO ()
profileAcc p =
  do printVersion
     annprog <- readFlatCurry p
     let (prog,es) = getMainExprs annprog
     profileAcc_aux p es annprog prog

profile_aux :: String -> [Expr] -> Prog -> Prog -> IO ()
profile_aux _ [] _ _ = 
  do putStrLn "There are no calls to start profiling..."
profile_aux p (e:[]) _ prog =
  do putStrLn ("Main goal:\n")
     putStrLn (concatMap (\ex->ppExpr 0 ex ++"\n") (e:[]))
     putStrLn ("Starting profiling for program \""++p++"\"...")
     putStrLn ("\nSolutions:\n"++(ppSols expL subs kL))
     --putStrLn ("Profiling Info:\n"++(ppCostL kL))
  where
    (expL,_,kL,subs) = unzip4 (findall (\r -> (profileProg prog e) =:= r))

profileAcc_aux :: String -> [Expr] -> Prog -> Prog -> IO ()
profileAcc_aux _ [] _ _ = 
  do putStrLn "There are no calls to start profiling..."
profileAcc_aux p (e:[]) _ prog =
  do putStrLn ("Main goal:\n")
     putStrLn (concatMap (\ex->ppExpr 0 ex ++"\n") (e:[]))
     putStrLn ("Starting profiling (Acc) for program \""++p++"\"...")
     putStrLn ("\nSolutions:\n"++(ppSols expL subs kL))
     --putStrLn ("Profiling Info:\n"++(ppCostL kL))
  where
    (expL,_,kLaux,subs) = unzip4 (findall (\r -> (profileProg prog e) =:= r))
    kL = accumulateCosts k0 kLaux

accumulateCosts _ [] = []
accumulateCosts k (k1:ks) = nk : accumulateCosts nk ks
  where nk = addCosts k k1

-- Transform a list of triples into a triple of lists
unzip4              :: [(a,b,c,d)] -> ([a],[b],[c],[d])
unzip4 []           = ([],[],[],[])
unzip4 ((x,y,z,w):ts) = (x:xs,y:ys,z:zs,w:ws) where (xs,ys,zs,ws) = unzip4 ts

ppSols [] _ _ = ""
ppSols (e:es) (s:ss) (k:ks) = 
   --  if e==(Comb FuncCall "failed" [])
   --     then (ppSols es ss ks)
   --     else 
  ("\nValue:"++(ppExpr 0 e)++"\nAnswer:"
          ++(ppSubs s)++"\nProfiling Info:\n"++(ppCost k))++(ppSols es ss ks)

ppCostL [] = "\n"
ppCostL (k:ks) = ("\n"++(ppCost k))++(ppCostL ks)

ppCost (C k) = ppCostAux k
ppCostAux [] = "\n"
ppCostAux ((cc,[a,b,c,d]):ccs) = (show cc)++" --> Steps: "++(show a)++" Case: "++(show b)++" Fcase: "++(show c)++" Apps: "++(show d)++"\n"++(ppCostAux ccs)

ppSubs FSub = "FSub"
ppSubs (Sub vars exps) = ppSubsAux vars exps
ppSubsAux [] _ = "\n"
ppSubsAux (v:vs) (e:es) = (ppVar v) ++ " -> " ++ (ppExpr 0 e) ++ " " ++ (ppSubsAux vs es)

---------------------------------------------------------------------------
-- extract all expressions e embedded in a call (MAIN e) in a program
-- and replace these calls by e:

getMainExprs :: Prog -> (Prog,[Expr])
getMainExprs (Prog modname imports types oldfuns ops trans) =
  (Prog modname imports types newfuns ops trans, evalexps)
 where
   funexppairs = map getFuncMainExprs oldfuns
   newfuns = map fst funexppairs
   evalexps = concatMap snd funexppairs
   
getFuncMainExprs :: FuncDecl -> (FuncDecl,[Expr])
getFuncMainExprs (Func name arity ftype (External ename)) =
  (Func name arity ftype (External ename), [])
getFuncMainExprs (Func name arity ftype (Rule lhs rhs)) =
  (Func name arity ftype (Rule lhs newrhs), evalexps)
 where
   (newrhs,evalexps) = getMainExprsInExp rhs

getMainExprsInExp (Var i) = (Var i, [])
getMainExprsInExp (Lit l) = (Lit l, [])
getMainExprsInExp (Comb ctype name args)
  | isMainAnnot (Comb ctype name args)
              = let expr = getMainAnnotExpr (Comb ctype name args)
                 in (expr,[expr])
  | otherwise = let (newargs,pexps) = getMainExprsInExps args
                 in (Comb ctype name newargs, pexps)
getMainExprsInExp (Apply e1 e2) =
 let (ne1,pe1) = getMainExprsInExp e1
     (ne2,pe2) = getMainExprsInExp e2
  in (Apply ne1 ne2, pe1++pe2)
getMainExprsInExp (Constr vars e) =
 let (ne,pe) = getMainExprsInExp e
  in (Constr vars ne, pe)
getMainExprsInExp (Or e1 e2) =
 let (ne1,pe1) = getMainExprsInExp e1
     (ne2,pe2) = getMainExprsInExp e2
  in (Or ne1 ne2, pe1++pe2)
getMainExprsInExp (Case ctype e bs) =
 let (ne,pe1) = getMainExprsInExp e
     (nbs,pe2) = getMainExprsInBranches bs
  in (Case ctype ne nbs, pe1++pe2)
getMainExprsInExp (Choice e) =
 let (ne,pe) = getMainExprsInExp e
  in (Choice ne, pe)
getMainExprsInExp (GuardedExpr vars e1 e2) =
 let (ne1,pe1) = getMainExprsInExp e1
     (ne2,pe2) = getMainExprsInExp e2
  in (GuardedExpr vars ne1 ne2, pe1++pe2)

getMainExprsInExps [] = ([],[])
getMainExprsInExps (e:es) = let (ne,pe1) = getMainExprsInExp e
                                (nes,pe2) = getMainExprsInExps es
                             in (ne:nes, pe1++pe2)

getMainExprsInBranches [] = ([],[])
getMainExprsInBranches (Branch p e : bs) =
   let (ne,pe1) = getMainExprsInExp e
       (nbs,pe2) = getMainExprsInBranches bs
    in (Branch p ne : nbs, pe1++pe2)



--profiling of a program
profileProg :: Prog -> Expr -> (Expr,Int,Cost,Subst)
profileProg (Prog _ _ _ funs _ _) e = meta_evalc (PState funs (maxVarIndex e)) (e,0,k0,Sub [] [])


meta_evalc pst (e,cc,k,s) =
  if testC e
     then (e,cc,k,s)
     else meta_evalc pst (ne,ncc,nk,ns)
  where (ne,ncc,nk,ns) = strict (evalc pst (e,cc,k,s))

testC e =
 if profDebug
    then (trace ("\n" ++ ppExpr 0 e) bool)
    else bool
 where bool = (isConstr e || isSuspended e)

----------------------------------------------------------------------------
--evalc implements our cost-augmented metainterpreter..

evalc :: ProState -> (Expr,Int,Cost,Subst) -> (Expr,Int,Cost,Subst)

----------------------------------------------------------------------------
--RLNT calculus:
--
-- HNF, Case of Case, Case Function, Case Select, Case Guess, Function Eval
----------------------------------------------------------------------------

----------------------------------------------------------------------------
-- HNF:

evalc _ (Var v,cc,k,s) = (Var v,cc,k,s)
evalc _ (Lit l,cc,k,s) = (Lit l,cc,k,s)
evalc pst (Comb ConsCall c es, cc, k,s) = evalc_cons pst c es [] cc k s

evalc_cons _ c [] es cc k s = (Comb ConsCall c es, cc, k, s)
evalc_cons pst c (e:es) zs cc k s = 
  if ne==e 
     then evalc_cons pst c es (zs++[e]) cc k s
     else (Comb ConsCall c (nzs++[ne]++nes), cc, nk, ns)
  where (ne,_,nk,ns) = evalc pst (e,cc,k,s)
        Sub vars exps = ns
        nzs = map (substitute vars exps) zs
        nes = map (substitute vars exps) es

--  if e==ne then (Comb ConsCall c (zs++[e]++es), cc, k, s)
--           else evalc_cons pst c nses (zs++[ne]) cc nk ns

------------------------------------------------------------------------------
-- Case Select:

evalc _ (Case _ (Comb ConsCall f es) ces, cc, k, s) = 
  --evalc pst (matchBranch ces f es, cc, incCase cc k, s)
  (matchBranch ces f es, cc, incCase cc k, s)

-- match a branch (for Case Select):
matchBranch :: [BranchExpr] -> String -> [Expr] -> Expr
matchBranch [] _ _ = (Comb FuncCall "failed" [])
matchBranch (Branch (Pattern p vars) e : ces) c es =
  if p==c then substitute vars es e else matchBranch ces c es

--this is for Case's with a constant argument:
evalc _ (Case _ (Lit l) ces, cc, k, s) = (matchBranchLit ces l, cc, incCase cc k, s)
--evalc pst (matchBranchLit ces l, cc, incCase cc k, s)

-- match a branch with Literals:
matchBranchLit :: [BranchExpr] -> Literal -> Expr
matchBranchLit [] _ = (Comb FuncCall "failed" [])
matchBranchLit (Branch (LPattern p) e : ces) c =
  if p==c then e else matchBranchLit ces c

------------------------------------------------------------------------------
-- Case Guess:

evalc pst (Case ctype (Var v) ces, cc, k, s) =
  if ctype==Flex
        then evalc_cguess pst v ces cc k s
        --then evalc pst ((propBindingOne v ces), cc, incFCase cc k)
        else (Case ctype (Var v) ces, cc, k, s)

evalc_cguess _ v ces cc k s =
  if length ces == 1
     then (propBindingOneNew2 v ces cc k s)
     else (propBindingOneNew v ces cc k s)
--     then evalc pst (propBindingOneNew2 v ces cc k s)
--     else evalc pst (propBindingOneNew v ces cc k s)

--propagate matchings to the corresponding branches:
propBindingOne :: Int -> [BranchExpr] -> Expr
propBindingOne v pes = propBinding v (mem pes)

mem (a:_) = a
mem (_:b) = mem b

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

propBindingOneNew2 v pes cc k s = (vce, cc, nk, composeSubs s ns)
  where (ce,nk) = memNew2 pes cc k
        (vce,ns) = propBinding2 v ce

memNew2 (a:_) cc k = (a, incCase cc k)
memNew2 (_:b) cc k = memNew b cc k

---old version
--memNew2 (a:_) _ cc k = (a, incCase cc k)
--memNew2 (_:b) n cc k = memNew b (n+1) cc k

---
-- composition of substitutions:

composeSubs :: Subst -> Subst -> Subst
composeSubs (Sub vars1 exps1) (Sub vars2 exps2) = 
  (Sub (vars1 ++ vars2) (newExps ++ exps2))
  where newExps = (map (substitute vars2 exps2) exps1)
composeSubs FSub (Sub _ _) = FSub
composeSubs (Sub _ _) FSub = FSub
composeSubs FSub FSub = FSub

----------------
propBindingOneNew v pes cc k s = (vce, cc, nk, composeSubs s ns)
  where (ce,nk) = memNew pes cc k
        (vce,ns) = propBinding2 v ce

memNew (a:_) cc k = (a, incFCase cc (incCase cc k))
memNew (_:b) cc k = memNew b cc k

---old version with different costs for each branch..
--memNew (a:_) n cc k = (a, incFCase cc (incCase cc k) n)
--memNew (_:b) n cc k = memNew b (n+1) cc k

propBinding2 v (Branch (Pattern c vs) e) = 
   (substitute [v] [(Comb ConsCall c (index2vars vs))] e, 
    Sub [v] [(Comb ConsCall c (index2vars vs))])
propBinding2 v (Branch (LPattern (Intc p)) e) = 
   (substitute [v] [(Lit (Intc p))] e,
    Sub [v] [(Lit (Intc p))])
propBinding2 v (Branch (LPattern (Floatc p)) e) = 
   (substitute [v] [(Lit (Floatc p))] e,
    Sub [v] [(Lit (Floatc p))])
propBinding2 v (Branch (LPattern (Charc p)) e) = 
   (substitute [v] [(Lit (Charc p))] e,
    Sub [v] [(Lit (Charc p))])



--propagate matchings to the corresponding branches:
propBinding :: Int -> BranchExpr -> Expr

propBinding v (Branch (Pattern c vs) e) = 
   substitute [v] [(Comb ConsCall c (index2vars vs))] e
propBinding v (Branch (LPattern (Intc p)) e) = 
   substitute [v] [(Lit (Intc p))] e
propBinding v (Branch (LPattern (Floatc p)) e) = 
   substitute [v] [(Lit (Floatc p))] e
propBinding v (Branch (LPattern (Charc p)) e) = 
   substitute [v] [(Lit (Charc p))] e

-- transform variable indices into variable expressions and vice versa:
index2vars :: [VarIndex] -> [Expr]
index2vars = map (\i->Var i)

vars2index :: [Expr] -> [VarIndex]
vars2index = map (\(Var i)->i)


---------------------------------------------------------------------------
--Case Eval:

evalc pst (Case ctype (Comb FuncCall f es) ces, cc, k, s) =
  if ne==(Comb FuncCall f es) 
     then (Case ctype (Comb FuncCall f es) ces, cc, k, s)
     --else evalc pst (Case ctype ne nces, cc, nk, ns)
     else (Case ctype ne nces, cc, nk, ns)
  where (ne, _, nk, ns) = evalc pst (Comb FuncCall f es, cc, k, s)
        Sub vars exps = ns
        nces = map (substituteBranch vars exps) ces

evalc pst (Case ctype (Case ctype2 e2 ces2) ces, cc, k, s) =
  if ne==(Case ctype2 e2 ces2)
     then (Case ctype (Case ctype2 e2 ces2) ces, cc, k, s)
     else (Case ctype ne nces, cc, nk, ns)
     --else evalc pst (Case ctype ne nces, cc, nk, ns)
  where (ne, _, nk, ns) = evalc pst (Case ctype2 e2 ces2, cc, k, s)
        Sub vars exps = ns
        nces = map (substituteBranch vars exps) ces

substituteBranch vars exps (Branch p e) = Branch p (substitute vars exps e)


---------------------------------------------------------------------------
--Function Eval:

evalc pst (Comb FuncCall f es, cc, k, s) = 
  if take 3 (reverse f)=="CCS" 
        then evalc_scc pst f es cc k s
             -- evalc pst ((extractExpr es), (extractCC es), k, s)
        else if definedFunc pst f
             then evalc_fun pst f es cc k s
             else evalc_builtin pst f es cc k s

extractExpr [_,a] = a
extractCC [Lit (Intc b),_] = b
extractCC2 [cc,_] = cc
extractCC3 (Lit (Intc b)) = b

evalc_fun pst f es cc k s = (newexp, cc, nk, s)
  --evalc newpst (newexp, cc, nk, s)
  where (_,newexp,nk) = matchRHS pst f es cc k

evalc_scc pst f es cc k s 
  | isVar e        = (e, cc2, k, s)
  | isLitInt e     = (e, cc2, k, s)
  | isConstant e   = (e, cc2, k, s)
  | isSCC e        = (e, cc2, k, s)
  | isConsCall e   = mixSCC pst f e cc22 k s
  | otherwise      = (Comb FuncCall f [cc22,ne], cc, nk, ns)
  where e = extractExpr es
        cc2 = extractCC es
        cc22 = extractCC2 es
        (ne,_,nk,ns) = evalc pst (e, cc2, k, s)
        
mixSCC _ f (Comb ConsCall c es) cc k s =
  (Comb ConsCall c (map (putSCC f cc) es), extractCC3 cc, k, s)

putSCC f cc e = Comb FuncCall f [cc,e]

--check whether an expression is a variable:
isSCC :: Expr -> Bool
isSCC x = case x of
          (Comb FuncCall f _) -> take 3 (reverse f)=="CCS"
          _ -> False


---------------------------------------------------------------------------
-- CALL UNFOLDING:

-- match a right-hand side of a given function:
matchRHS pst f es cc k = getMatchedRHS pst (getFuncDecls pst) f es cc k


getMatchedRHS pst (Func fname _ _ funrule : fds) name es cc k =
   if fname==name then getMatchedRHS_aux pst funrule es cc k
                  else getMatchedRHS pst fds name es cc k


getMatchedRHS_aux pst (Rule vars rhs) es cc k =
  let curr_ri = getRenamingIndex pst
      maxindex = max (maxList vars) (maxVarIndex rhs)
  in
   (updateRenamingIndex pst (curr_ri+maxindex+1),
    substituteAll vars es curr_ri rhs,
    incSteps cc (incApps cc k rhs))
   -- here we assume that no more than maxExpVars variables occur in each
   -- unfolded expression to produce a safe renaming.

-- (substitute vars exps expr) = expr[vars/exps]
-- i.e., replace all occurrences of vars by corresponding exps in the
-- expression expr
substitute :: [Int] -> [Expr] -> Expr -> Expr
substitute vars exps expr = substituteAll vars exps 0 expr

-- (substituteAll vars exps base expr):
-- substitute all occurrences of variables by corresponding expressions:
-- * substitute all occurrences of var_i by exp_i in expr
--   (if vars=[var_1,...,var_n] and exps=[exp_1,...,exp_n])
-- * substitute all other variables (Var j) by (Var (base+j))
--
-- here we assume that the new variables in guards and case patterns
-- do not occur in the list "vars" of replaced variables!

substituteAll :: [Int] -> [Expr] -> Int -> Expr -> Expr
substituteAll vars exps b (Var i) = replaceVar vars exps i
  where replaceVar [] [] var = Var (b+var)
        replaceVar (v:vs) (e:es) var = if v==var then e
                                                 else replaceVar vs es var
substituteAll _  _  _ (Lit l) = Lit l
substituteAll vs es b (Comb combtype c exps) =
                 Comb combtype c (map (substituteAll vs es b) exps)
substituteAll vs es b (Apply e1 e2) =
                 Apply (substituteAll vs es b e1) (substituteAll vs es b e2)
substituteAll vs es b (Constr vars e) =
                 Constr (map (+b) vars) (substituteAll vs es b e)
substituteAll vs es b (Or e1 e2) =
                 Or (substituteAll vs es b e1) (substituteAll vs es b e2)
substituteAll vs es b (Case ctype e cases) =
   Case ctype (substituteAll vs es b e) (map (substituteAllCase vs es b) cases)
substituteAll vs es b (GuardedExpr vars c e) =
   GuardedExpr (map (+b) vars) (substituteAll vs es b c)
                               (substituteAll vs es b e)
substituteAll vs es b (Choice e) = Choice (substituteAll vs es b e)

substituteAllCase :: [Int] -> [Expr] -> Int -> BranchExpr -> BranchExpr
substituteAllCase vs es b (Branch (Pattern l pvs) e) =
                 Branch (Pattern l (map (+b) pvs)) (substituteAll vs es b e)
substituteAllCase vs es b (Branch (LPattern l) e) =
                 Branch (LPattern l) (substituteAll vs es b e)


----------------------------------------------------------------------------
-- is f a defined function?
definedFunc :: ProState -> String -> Bool
definedFunc pst f = any (hasName f) (getFuncDecls pst)
definedFunc2 :: [FuncDecl] -> String -> Bool
definedFunc2 funs f = any (hasName f) funs

hasName :: String -> FuncDecl -> Bool
hasName name (Func fname _ _ _) = fname==name





------------------------------------------------------------------------------
-- Pretty print 
------------------------------------------------------------------------------

-- pretty printer for expressions (first argument: indentation):
ppExpr _ (Var n) = ppVar n
ppExpr _ (Lit l) = ppLit l
ppExpr b (Comb _ cf es) =
  "(" ++ cf ++ " " ++ ppList (ppExpr b) es ++ ")"
ppExpr b (Apply e1 e2) =
  "(" ++ ppExpr b e1 ++ " " ++ ppExpr b e2 ++ ")"
ppExpr b (Constr xs e) =
  "(Constr " ++ ppFormatList ppVar xs ++ (ppExpr b) e ++ ")"
ppExpr b (Or e1 e2) =
  "(Or " ++ ppExpr b e1 ++ " " ++ ppExpr b e2 ++ ")"
ppExpr b (Case Rigid e cs) =
  "(Case " ++ ppExpr b e ++ " of\n " ++ ppList (ppCase (b+2)) cs
  ++ blanks b ++ ")"
ppExpr b (Case Flex e cs) =
  "(FCase " ++ ppExpr b e ++ " of\n " ++ ppList (ppCase (b+2)) cs
  ++ blanks b ++ ")"
ppExpr b (GuardedExpr xs e1 e2) =
  "(GuardedExpr " ++ ppFormatList ppVar xs
                  ++ ppExpr b e1 ++ " " ++ ppExpr b e2 ++ ")"
ppExpr b (Choice e) = "(Choice " ++ ppExpr b e ++ ")"

ppVar i = "v" ++ show i

ppLit (Intc   i) = show i
ppLit (Floatc f) = show f
ppLit (Charc  c) = "'" ++ show (ord c) ++ "'"

ppCase b (Branch (Pattern l xs) e) = blanks b ++ "(" ++ l ++ " "
                                     ++ ppList ppVar xs
                                     ++ " -> " ++ ppExpr b e ++ ")\n"
ppCase b (Branch (LPattern l) e) = blanks b ++ "(" ++ ppLit l ++ " "
                                   ++ " -> " ++ ppExpr b e ++ ")\n"

blanks b = take b (repeat ' ')

-- format a finite list of elements (with a format function for list elems):
ppFormatList :: (a->String) -> [a] -> String
ppFormatList format elems = " [" ++ ppElems elems ++ "] "
 where
   ppElems [] = ""
   ppElems [x] = format x
   ppElems (x1:x2:xs) = format x1 ++ "," ++ ppElems (x2:xs)

ppList format elems = ppListElems elems
  where
    ppListElems [] = ""
    ppListElems [x] = format x
    ppListElems (x1:x2:xs) = format x1 ++ " " ++ ppListElems (x2:xs)

------------------------------------------------------------------------------
-- handling variables in expressions:

-- get the maximum index of all variables in an expression:
-- (or -1 if there is no variable)
maxVarIndex :: Expr -> Int
maxVarIndex (Var v)         = v
maxVarIndex (Lit _)         = -1
maxVarIndex (Comb _ _ exps) = maxList (map maxVarIndex exps)
maxVarIndex (Apply e1 e2)   = max (maxVarIndex e1) (maxVarIndex e2)
maxVarIndex (Constr vars e) = max (maxList vars) (maxVarIndex e)
maxVarIndex (Or e1 e2)      = max (maxVarIndex e1) (maxVarIndex e2)
maxVarIndex (Case _ ce cs)   = max (maxVarIndex ce) (maxList (map maxCase cs))
  where maxCase (Branch (Pattern _ pvs) e) = max (maxList pvs) (maxVarIndex e)
        maxCase (Branch (LPattern _)   e) = maxVarIndex e
maxVarIndex (GuardedExpr vars c e) =
                   max (max (maxList vars) (maxVarIndex c)) (maxVarIndex e)
maxVarIndex (Choice e)      = maxVarIndex e

-- maximum of two numbers:
max i j = if i<=j then j else i

-- maximum of a list of naturals (-1 if list is empty):
maxList xs = foldr max (-1) xs


----------------------------------------------------------------------------
--Extension of the RLNT calculus:
--
-- partcall, apply, constr, or, guardedexpr, choice
----------------------------------------------------------------------------



----------------------------------------------------------------------------
--Partcall:

evalc _ (Comb PartCall c es, cc, k, s) = (Comb PartCall c es, cc, k, s)


----------------------------------------------------------------------------
--Or expression:

--evalc pst (Or e1 e2, cc, k, s) = evalc pst (e1, cc, k, s) 
--evalc pst (Or e1 e2, cc, k, s) = evalc pst (e2, cc, k, s)


----------------------------------------------------------------------------
--Choice:

--evalc _ _ (Choice e) = Choice e

----------------------------------------------------------------------------
--These rules complements Case-of-case, Case Select, Case Fun, and Case Guess:
--
evalc pst (Case ctype (Apply e1 e2) ces, cc, k, s) = 
  if ne==(Apply e1 e2)
     then (Case ctype (Apply e1 e2) ces, cc, k, s)
     else (Case ctype ne nces, cc, nk,ns)
     --else evalc pst (Case ctype ne nces, cc, nk,ns)
  --where (ne, _, nk,ns) = evalc pst (Apply e1 e2, cc, k,s)
  where (ne, _, nk, ns) = evalc pst (Apply e1 e2, cc, k,s)
        Sub vars exps = ns
        nces = map (substituteBranch vars exps) ces

evalc pst (Case ctype (Constr vars es) ces, cc, k, s) = 
  if ne==(Constr vars es)
     then (Case ctype (Constr vars es) ces, cc, k, s) 
     else (Case ctype ne nces, cc, nk, ns)
     --else evalc pst (Case ctype ne nces, cc, nk, ns)
  --where (ne, _, nk, ns) = evalc pst (Constr vars es, cc, k, s)
  where (ne, _, nk, ns) = evalc pst (Constr vars es, cc, k, s)
        Sub vars2 exps = ns
        nces = map (substituteBranch vars2 exps) ces

evalc pst (Case ctype (Or e1 e2) ces, cc, k, s) = 
  if ne==(Or e1 e2)
     then (Case ctype (Or e1 e2) ces, cc, k, s)
     else (Case ctype ne nces, cc, nk, ns)
     --else evalc pst (Case ctype ne nces, cc, nk, ns)
  --where (ne, _, nk, ns) = evalc pst (Or e1 e2, cc, k, s)
  where (ne, _, nk, ns) = evalc pst (Or e1 e2, cc, k, s)
        Sub vars exps = ns
        nces = map (substituteBranch vars exps) ces

evalc pst (Case ctype (GuardedExpr vars gc e) ces, cc, k, s) =
  if ne==(GuardedExpr vars gc e)
     then (Case ctype (GuardedExpr vars gc e) ces, cc, k, s)
     else (Case ctype ne nces, cc, nk, ns)
     --else evalc pst (Case ctype ne nces, cc, nk, ns)
  --where (ne, _, nk, ns) = evalc pst (GuardedExpr vars gc e, cc, k, s)
  where (ne, _, nk, ns) = evalc pst (GuardedExpr vars gc e, cc, k, s)
        Sub vars2 exps = ns
        nces = map (substituteBranch vars2 exps) ces

--evalc _ _ (Case ctype (Choice e) ces) = Case ctype (Choice e) ces


----------------------------------------------------------------------------
--Apply:

evalc pst (Apply e1 e2, cc, k, s) = 
  if (isPartCall e1) then evalc_apply pst e1 e2 cc k s
                     else evalc_applyAux pst e1 e2 cc k s

evalc_applyAux pst e e2 cc k s = 
  if ne==e 
     then (Apply e e2, cc, k, s)
     else (Apply ne ne2, cc, nk, ns)
     --else evalc pst (Apply ne ne2, cc, nk, ns)
  --where (ne,_,nk, ns) = evalc pst (e,cc,k, s)
  where (ne, _, nk, ns) = evalc pst (e,cc,k, s)
        Sub vars exps = ns
        ne2 = substitute vars exps e2

isPartCall :: Expr -> Bool
isPartCall x = case x of 
                    (Comb PartCall _ _) -> True
                    _ -> False

--evalc_apply :: ProState -> Expr -> Expr -> Int -> Cost -> (Expr,Int,Cost)
evalc_apply pst (Comb PartCall f es) e2 cc k s =
  if (getArity pst f)==(length es + 1)
  then evalc pst (Comb FuncCall f (es++[e2]), cc, k, s)
  else evalc pst (Comb PartCall f (es++[e2]), cc, k, s)

-----------------------------------------------------------------------------
--Guarded expressions:

evalc pst (GuardedExpr vars gc e, cc, k, s) =
  if gc==(Comb FuncCall "success" []) || gc==(Comb ConsCall "True" [])
     then evalc pst (e,cc,k,s)
     else evalc_guarded pst vars gc e cc k s

evalc_guarded pst vars gc e cc k s = 
  if ngc==gc
     then (GuardedExpr vars gc e, cc, k, s)
     else (GuardedExpr vars ngc ne, cc, nk, ns)
     --else evalc pst (GuardedExpr vars ngc ne, cc, nk, ns)
  --where (ngc, _, nk, ns) = evalc pst (gc, cc, k, s)
  where (ngc, _, nk, ns) = evalc pst (gc, cc, k, s)
        Sub vars2 exps = ns
        ne = substitute vars2 exps e

-----------------------------------------------------------------------------
--Constraints:

evalc pst (Constr vars e, cc, k, s)
  | e==(Comb FuncCall "success" [])  = (Comb FuncCall "success" [],cc,k,s)
  | e==(Comb ConsCall "True" [])     = (Comb FuncCall "success" [],cc,k,s)
  | otherwise                        = evalc_constr pst vars e cc k s

evalc_constr pst vars e cc k s = 
  if ne==e
     then (Constr vars e, cc, k, s)
     else (Constr vars ne, cc, nk, ns)
     --else evalc pst (Constr vars ne, cc, nk, ns)
  where (ne, _, nk, ns) = evalc pst (e,cc,k,s)

-----------------------------------------------------------------------------
--Built-in's:

strict x | x==x = x

evalc_builtin :: ProState -> String -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)

evalc_builtin pst f es cc k s
  | f=="=="   = evalc_builtinEQ pst f es cc k s
  | f=="=:="  = evalc_builtinEQ2 pst f es cc k s
  | f=="if_then_else" = evalc_builtinITE pst es cc (incSteps cc (incCase cc (incApps2 cc k 8))) s
  | f=="&&"   = evalc_builtinAND pst es cc k s
  | f=="&"    = evalc_builtinCAND pst es cc k s
  | f=="*"    = evalc_builtinARITH pst f es cc k s
  | f=="+"    = evalc_builtinARITH pst f es cc k s
  | f=="-"    = evalc_builtinARITH pst f es cc k s
  | f=="<"    = evalc_builtinARITH pst f es cc k s
  | f==">"    = evalc_builtinARITH pst f es cc k s
  | f=="<="   = evalc_builtinARITH pst f es cc k s
  | f==">="   = evalc_builtinARITH pst f es cc k s
  --| f=="map"  = evalc_builtinMAP pst f es cc k
  --| f=="foldl"   = evalc_builtinFOLDL pst f es cc k
  --| f=="foldr"   = evalc_builtinFOLDR pst f es cc k
  --| f=="filter"  = evalc_builtinFILTER pst f es cc k
  --| f=="iterate" = evalc_builtinITERATE pst f es cc k
  | True        = (Comb FuncCall f es, cc, k, s)
     
---------------------------------
-- STRICT EQUALITY:

evalc_builtinEQ :: ProState -> String -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinEQ pst f [e1,e2] cc k s
  | (isVar e1) || (isVar e2)            = (Comb FuncCall f [e1,e2], cc, k, s)
  | (isConsCall e1) && (isConsCall e2)  = evalc_builtinEQaux pst f [e1,e2] cc k s
  | (isLitInt e1) && (isLitInt e2)      = evalc_builtinEQlit f e1 e2 cc k s
  | (isLitInt e1) || (isConsCall e1)    = evalc_EQAux2 pst f e1 e2 cc k s
  | otherwise                           = evalc_EQAux pst f e1 e2 cc k s

evalc_EQAux pst f e1 e2 cc k s = 
  if ne1==e1 then (Comb FuncCall f [ne1,ne2], cc, nk, ns)
             else (Comb FuncCall f [ne1,ne2], cc, nk, ns)
             --else evalc pst (Comb FuncCall f [ne1,ne2], cc, nk, ns)
  --where (ne1,_,nk,ns) = evalc pst (e1,cc,k,s)
  where (ne1, _, nk, ns) = evalc pst (e1,cc,k,s)
        Sub vars exps = ns
        ne2 = substitute vars exps e2

evalc_EQAux2 pst f e1 e2 cc k s = 
  if ne2==e2
     then (Comb FuncCall f [e1,e2], cc, k, s)
     else (Comb FuncCall f [ne1,ne2], cc, nk, ns)
     --else evalc pst (Comb FuncCall f [ne1,ne2], cc, nk, ns)
  --where (ne2,_,nk,ns) = evalc pst (e2,cc,k,s)
  where (ne2, _, nk, ns) = evalc pst (e2,cc,k,s)
        Sub vars exps = ns
        ne1 = substitute vars exps e1

evalc_builtinEQaux :: ProState -> String -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinEQaux pst f [Comb _ f1 e1, Comb _ f2 e2] cc k s
  | f1==f2                                      = evalc pst (makeSeqCon f e1 e2, cc, k,s)
  | (f1=="False") && (f2=="failed") && f=="=="  = (Comb ConsCall "True" [], cc, k,s)
  | (f1=="False") && (f2=="failed") && f=="=:=" = (Comb FuncCall "success" [],cc,k,s)
  | (f1=="failed") && (f2=="False") && f=="=="  = (Comb ConsCall "True" [],cc,k,s)
  | (f1=="failed") && (f2=="False") && f=="=:=" = (Comb FuncCall "success" [],cc,k,s)
  | f=="=="                                     = (Comb ConsCall "False" [],cc,k,s)
  | otherwise                                   = (Comb FuncCall "failed" [],cc,k,s)
--the strange cases above are needed due to the current definition of Case Select
--(in particular, the case when the argument doesn't match any branch..)

evalc_builtinEQlit :: String -> Expr -> Expr -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinEQlit f (Lit (Intc x)) (Lit (Intc y)) cc k s
  | x==y && f=="=="   = (Comb ConsCall "True" [],cc,k,s)
  | x==y && f=="=:="  = (Comb FuncCall "success" [],cc,k,s)
  | x/=y && f=="=="   = (Comb ConsCall "False" [],cc,k,s)
  | otherwise         = (Comb FuncCall "failed" [],cc,k,s)


evalc_builtinEQ2 :: ProState -> String -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinEQ2 pst f [e1,e2] cc k s
  | (isConsCall e1) && (isConsCall e2)  = evalc_builtinEQaux pst f [e1,e2] cc k s
  | (isLitInt e1) && (isLitInt e2)      = evalc_builtinEQlit f e1 e2 cc k s
  | isVar e1                            = evalc_builtinEQvar1 pst f [e1,e2] cc k s
  | isVar e2                            = evalc_builtinEQvar2 pst f [e2,e1] cc k s
  | (isLitInt e1) || (isConsCall e1)    = evalc_EQAux2 pst f e1 e2 cc k s
  | otherwise                           = evalc_EQAux pst f e1 e2 cc k s


evalc_builtinEQvar1 :: ProState -> String -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinEQvar1 pst f [Var x, e] cc k s =
  if dataExp e && f=="=:="
     then evalc_builtinEQvarAux pst f x e cc k s
     else evalcEQvar1_aux pst f (Var x) e cc k s

evalcEQvar1_aux pst f v e cc k s = 
  if ne==e 
     then (Comb FuncCall f [v,e], cc, k,s)
     else (Comb FuncCall f [nv,ne], cc, nk,ns)
     --else evalc pst (Comb FuncCall f [nv,ne], cc, nk,ns)
  --where (ne,_,nk,ns) = evalc pst (e,cc,k,s)
  where (ne, _, nk, ns) = evalc pst (e,cc,k,s)
        Sub vars exps = ns
        nv = substitute vars exps v

evalc_builtinEQvar2 :: ProState -> String -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinEQvar2 pst f [Var x, e] cc k s =
  if dataExp e && f=="=:="
     then evalc_builtinEQvarAux pst f x e cc k s
     else evalcEQvar2_aux pst f (Var x) e cc k s

evalcEQvar2_aux pst f v e cc k s = 
  if ne==e
     then (Comb FuncCall f [e,v], cc, k,s)
     else (Comb FuncCall f [ne,nv], cc, nk,ns)
     --else evalc pst (Comb FuncCall f [ne,nv], cc, nk,ns)
  --where (ne,_,nk,ns) = evalc pst (e,cc,k,s)
  where (ne, _, nk, ns) = evalc pst (e,cc,k,s)
        Sub vars exps = ns
        nv = substitute vars exps v

evalc_builtinEQvarAux :: ProState -> String -> Int -> Expr -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinEQvarAux pst f x e cc k s =
  evalc pst (Case Flex (Var x) (subs2branches e f), cc, k, s)


subs2branches :: Expr -> String -> [BranchExpr]
subs2branches (Lit c) f = 
  if f=="==" 
     then [Branch (LPattern c) (Comb ConsCall "True" [])]
     else [Branch (LPattern c) (Comb FuncCall "success" [])]
subs2branches (Comb ConsCall c []) f =
  if f=="==" 
     then [Branch (Pattern c []) (Comb ConsCall "True" [])]
     else [Branch (Pattern c []) (Comb FuncCall "success" [])]
--PENDING: extend function above to cover arbitrary data terms...

--currently we only consider literals and constants.. TO DO..
dataExp :: Expr -> Bool
dataExp (Var _) = False
dataExp (Lit _) = True
dataExp (Comb ftype f args) = 
  args==[] && 
          (ftype==ConsCall || f=="success" || f=="failed")
-- if ftype==ConsCall then andL (map dataExp args) else False
dataExp (Apply _ _) = False
dataExp (Constr _ _) = False
dataExp (Or _ _) = False
dataExp (Case _ _ _) = False
dataExp (GuardedExpr _ _ _) = False
dataExp (Choice _) = False


isConsCall :: Expr -> Bool
isConsCall x = case x of 
                    (Comb ConsCall _ _) -> True
                    (Comb _ "success" _) -> True
                    (Comb _ "failed" _) -> True
                    _ -> False

isConstant :: Expr -> Bool
isConstant x = case x of 
                    (Comb ConsCall _ []) -> True
                    (Comb _ "success" _) -> True
                    (Comb _ "failed" _) -> True
                    _ -> False

makeSeqCon :: String -> [Expr] -> [Expr] -> Expr
makeSeqCon f [] [] = 
  if f=="==" then Comb ConsCall "True" []
             else Comb FuncCall "success" []
makeSeqCon f [e1] [e2] = Comb FuncCall f [e1,e2]
makeSeqCon f (e1:(e1b:es1)) (e2:(e2b:es2)) =
  if f=="==" 
     then (Comb FuncCall "&&" [(Comb FuncCall f [e1,e2]), (makeSeqCon f (e1b:es1) (e2b:es2))])
     else (Comb FuncCall "&" [(Comb FuncCall f [e1,e2]), (makeSeqCon f (e1b:es1) (e2b:es2))])

-------------------------------------------------------------------
-- IF THEN ELSE:

evalc_builtinITE :: ProState -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinITE pst [c,e1,e2] cc k s
  | c==(Comb ConsCall "True" [])   = evalc pst (e1,cc,k,s)
  | c==(Comb ConsCall "False" [])  = evalc pst (e2,cc,k,s)
  --| isStrictEQ c                   = evalc_builtinITE_aux pst [c,e1,e2] cc k s
  | otherwise                      = evalc_ITEAux pst "if_then_else" [c,e1,e2] cc k s

evalc_ITEAux pst _ [c,e1,e2] cc k s = 
  if nc==c
     then (Comb FuncCall "if_then_else" [c,e1,e2], cc, k, s)
     else (Comb FuncCall "if_then_else" [nc,ne1,ne2], cc, nk, ns)
     --else evalc pst (Comb FuncCall "if_then_else" [nc,ne1,ne2], cc, nk, ns)
  --where (nc, _, nk,ns) = evalc pst (c,cc,k,s)
  where (nc, _, nk, ns) = evalc pst (c,cc,k,s)
        Sub vars exps = ns
        ne1 = substitute vars exps e1
        ne2 = substitute vars exps e2

--evalc_builtinITE_aux pst [Comb FuncCall "==" [c1,c2], e1, e2] cc k
--  | (isLitInt c1) && (isLitInt c2) = if c1==c2 then evalc pst (e1,cc,k)
--                                               else evalc pst (e2,cc,k)
--  | otherwise = evalc_ITEAux pst "if_then_else" [Comb FuncCall "==" [c1,c2],e1,e2] cc k


--  | isVar c1 && isConstr c2 = (Comb FuncCall "if_then_else" 
--                              [Comb FuncCall "==" [c1,c2],
--                               substitute (vars2index [c1]) [c2] e1, 
--                               e2], cc, k)
--  | isVar c2 && isConstr c1 = (Comb FuncCall "if_then_else" 
--                              [Comb FuncCall "==" [c1,c2],
--                               substitute (vars2index [c2]) [c1] e1, 
--                               e2],cc,k)
--  | otherwise               = (Comb FuncCall "if_then_else" 
--                              [Comb FuncCall "==" [c1,c2], e1, e2], cc, k)

-------------------------------------------------------------------
-- SEQUENTIAL CONJUNCTION:

evalc_builtinAND :: ProState -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinAND pst [e1,e2] cc k s
  | e1==(Comb ConsCall "True" [])    =  evalc pst (e2,cc,k,s)
  | e1==(Comb FuncCall "success" []) =  evalc pst (e2,cc,k,s)
  | e2==(Comb ConsCall "True" [])    =  evalc pst (e1,cc,k,s)
  | e2==(Comb FuncCall "success" []) =  evalc pst (e1,cc,k,s)
  | e1==(Comb ConsCall "False" [])   =  (Comb ConsCall "False" [], cc,k,s)
  | e1==(Comb FuncCall "failed" [])  =  (Comb FuncCall "failed" [],cc,k,s)
  | e2==(Comb ConsCall "False" [])   =  (Comb ConsCall "False" [],cc,k,s)
  | e2==(Comb FuncCall "failed" [])  =  (Comb FuncCall "failed" [],cc,k,s)
  | otherwise                        =  evalc_ANDAux pst e1 e2 cc k s

evalc_ANDAux pst e1 e2 cc k s = 
  if ne1==e1
     then (Comb FuncCall "&&" [e1,e2], cc, k, s)
     else (Comb FuncCall "&&" [ne1,ne2], cc, nk, ns)
     --else evalc pst (Comb FuncCall "&&" [ne1,ne2], cc, nk, ns)
  where (ne1,_,nk,ns) = evalc pst (e1,cc,k,s)
        Sub vars exps = ns
        ne2 = substitute vars exps e2

 
--------------------------------------------------------------------
-- CONCURRENT CONJUNCTION:

evalc_builtinCAND :: ProState -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinCAND pst [e1,e2] cc k s
  | e1==(Comb FuncCall "success" [])  = evalc pst (e2,cc,k,s)
  | e2==(Comb FuncCall "success" [])  = evalc pst (e1,cc,k,s)
  | e1==(Comb FuncCall "failed" [])   = (Comb FuncCall "failed" [],cc,k,s)
  | e2==(Comb FuncCall "failed" [])   = (Comb FuncCall "failed" [],cc,k,s)
  | otherwise                         = evalc_CANDAux pst e1 e2 cc k s


evalc_CANDAux pst e1 e2 cc k s = 
  if isSuspended e1 
    then evalc_CANDAux1 pst e1 e2 cc k s
    else evalc_CANDAux2 pst e1 e2 cc k s

evalc_CANDAux1 pst e1 e2 cc k s = 
  if ne2==e2
     then (Comb FuncCall "&" [e1,e2], cc, k, s)
     else (Comb FuncCall "&" [ne1,ne2], cc, nk, ns)
     --else evalc pst (Comb FuncCall "&" [ne1,ne2], cc, nk, ns)
  where (ne2,_,nk,ns) = evalc pst (e2,cc,k,s)
        Sub vars exps = ns
        ne1 = substitute vars exps e1
        
evalc_CANDAux2 pst e1 e2 cc k s = 
  if ne1==e1
     then (Comb FuncCall "&" [e1 ,e2], cc, k, s)
     else (Comb FuncCall "&" [ne1 ,ne2], cc, nk, ns)
     --else evalc pst (Comb FuncCall "&" [ne1 ,ne2], cc, nk, ns)
  --where (ne1,_,nk, ns) = evalc pst (e1,cc,k,s)
  where (ne1,_,nk,ns) = evalc pst (e1 ,cc,k,s)
        Sub vars exps = ns
        ne2 = substitute vars exps e2
        
isSuspended :: Expr -> Bool
isSuspended e = case e of 
                     (Case Rigid (Var _) _) -> True
                     (Comb FuncCall "&" es) -> andL (map isSuspended es)
                     (Comb FuncCall "==" [e1,e2]) -> (isVar e1) || (isVar e2)
                     (Comb FuncCall "=:=" [e1,e2]) -> (isSuspended e1) || (isSuspended e2)
                     _ -> False

-- mejora esta para que acepte suspensions! (solo va el colormap "simple"..)
--evalc_CANDAux pst e1 e2 cc k s = evalc pst (Comb FuncCall "&" [ne1,ne2], cc, nk, ns)
--  --where (ne1,_,nk, ns) = evalc pst (e1,cc,k,s)
--  where (ne1,_,nk,ns) = evalc pst (e1,cc,k,s)
--        Sub vars exps = ns
--        ne2 = substitute vars exps e2


-----------------------------------------------------------------------
-- ARITHMETIC AND RELATIONAL OPERATORS:

evalc_builtinARITH :: ProState -> String -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinARITH pst f [e1,e2] cc k s =
  if (isLitInt e1) && (isLitInt e2)
     then evalc_builtinARITHaux f [e1,e2] cc k s
     else if (isLitInt e2) then evalc_ARITHAux pst f e1 e2 cc k s
             else evalc_ARITHAux2 pst f e1 e2 cc k s

evalc_ARITHAux pst f e1 e2 cc k s = 
  if ne1==e1
     then (Comb FuncCall f [e1,e2], cc, k, s)
     else (Comb FuncCall f [ne1,e2], cc, nk, ns)
     --else evalc pst (Comb FuncCall f [ne1,e2], cc, nk, ns)
  where (ne1,_,nk,ns) = evalc pst (e1,cc,k,s)
evalc_ARITHAux2 pst f e1 e2 cc k s = 
  if ne2==e2
     then (Comb FuncCall f [e1,e2], cc, k, s)
     else (Comb FuncCall f [e1,ne2], cc, nk, ns)
     --else evalc pst (Comb FuncCall f [e1,ne2], cc, nk, ns)
  where (ne2,_,nk,ns) = evalc pst (e2,cc,k,s)


--PENDING: extend to floats and to more operators..


evalc_builtinARITHaux :: String -> [Expr] -> Int -> Cost -> Subst -> (Expr,Int,Cost,Subst)
evalc_builtinARITHaux f [(Lit (Intc e1)),(Lit (Intc e2))] cc k s
  | (f=="*")   = (Lit (Intc (e1*e2)),cc,k,s)
  | (f=="+")   = (Lit (Intc (e1+e2)),cc,k,s)
  | (f=="-")   = (Lit (Intc (e1-e2)),cc,k,s)
  | (f=="<")   = if e1<e2 then (Comb ConsCall "True" [],cc,k,s) else (Comb ConsCall "False" [],cc,k,s)
  | (f==">")   = if e1>e2 then (Comb ConsCall "True" [],cc,k,s) else (Comb ConsCall "False" [],cc,k,s)
  | (f=="<=")  = if e1<=e2 then (Comb ConsCall "True" [],cc,k,s) else (Comb ConsCall "False" [],cc,k,s)
  | (f==">=")  = if e1>=e2 then (Comb ConsCall "True" [],cc,k,s) else (Comb ConsCall "False" [],cc,k,s)

isLitInt :: Expr -> Bool
isLitInt e = case e of 
                 (Lit (Intc _)) -> True
                 _ -> False

--check whether an expression is a variable:
isVar :: Expr -> Bool
isVar x = case x of 
               (Var _) -> True
               _ -> False

--check whether an expression is a strict equality
isStrictEQ :: Expr -> Bool
isStrictEQ x = case x of
                   (Comb FuncCall "==" _) -> True
                   _ -> False

--check whether an expression is a literal:
isLit :: Expr -> Bool
isLit x = case x of 
               (Lit _) -> True
               _ -> False


isConstr :: Expr -> Bool
isConstr e = case e of 
                  (Var _) -> True
                  (Lit _) -> True
                  (Comb ConsCall _ es) -> andL (map isConstr es)
                  (Comb _ "success" _) -> True
                  (Comb _ "failed" _) -> True
                  _ -> False

isGroundConstr :: Expr -> Bool
isGroundConstr e = case e of
                        (Var _) -> False
                        (Lit _) -> True
                        (Comb ConsCall _ es) -> andL (map isGroundConstr es)
                        _ -> False

--conjunction of a list of boolean terms

andL:: [Bool] -> Bool
andL es = foldr (&&) True es