----------------------------------------------------------------------
--- A representation of CHR rules in Curry, an interpreter
--- for CHR rules based on the refined operational semantics of
--- Duck et al. (ICLP 2004), and a compiler into CHR(Prolog).
---
--- To use CHR(Curry), specify the CHR(Curry) rules in a Curry program,
--- load it, add module `CHR` and interpret or compile the rules
--- with `runCHR` or `compileCHR`, respectively. This can be done
--- in one shot with
---
---     > pakcs :l MyRules :add CHR :eval 'compileCHR "MyCHR" "MyRules" [rule1,rule2]' :q
---
--- @author Michael Hanus
--- @version July 2021
----------------------------------------------------------------------

{-# OPTIONS_CYMAKE -Wno-incomplete-patterns -Wno-overlapping #-}

module CHR(CHR,Goal,(/\), (<=>), (==>), (|>), (\\),
           true, false, andCHR, allCHR, chrsToGoal,
           toGoal1, toGoal2, toGoal3, toGoal4, toGoal5, toGoal6,
           (.=.), (./=.), (.<=.), (.>=.), (.>.), (.<.),
           nonvar, ground, anyPrim,
           solveCHR, runCHR, runCHRwithTrace,
           compileCHR, chr2curry
          ) where

import Prelude hiding ( empty )
import Data.Char
import Data.List
import System.IO.Unsafe -- for tracing

import Control.Findall   ( rewriteSome )
import Data.Set.RBTree   ( SetRBT, member, empty, insert )
import FlatCurry.Types
import FlatCurry.Files
import FlatCurry.Goodies
import FlatCurry.Pretty        ( defaultOptions, ppTypeExp )
import Language.Prolog.Types
import Language.Prolog.Goodies ( plList )
import Language.Prolog.Show    ( showPlClause, showPlGoals )
import Text.Pretty             ( showWidth )
import XML

-------------------------------------------------------------------------------
-- Operator definitions for writing CHRs:

infix 5 .=., ./=., .<=., .>=., .>., .<.
infixr 4 /\
infix 3 <=>
infix 3 ==>
infix 2 \\
infix 1 |>

-------------------------------------------------------------------------------
-- Data types for defining Constraint Handling Rules.

--- The basic data type of Constraint Handling Rules.
data CHR dom chr =
    SimplRule [chr] [PrimConstraint dom] (Goal dom chr)
  | PropaRule [chr] [PrimConstraint dom] (Goal dom chr)
  | SimpaRule [chr] [chr] [PrimConstraint dom] (Goal dom chr)

--- Simplification rule.
(<=>) :: Goal dom chr -> Goal dom chr -> CHR dom chr
g1 <=> g2 =
  if null (primsOfGoal g1)
    then SimplRule (uchrOfGoal g1) [] g2
    else error "Rule with primitive constraint on the left-hand side!"

--- Propagation rule.
(==>) :: Goal dom chr -> Goal dom chr -> CHR dom chr
g1 ==> g2 =
  if null (primsOfGoal g1)
    then PropaRule (uchrOfGoal g1) [] g2
    else error "Rule with primitive constraint on the left-hand side!"

--- Simpagation rule: if rule is applicable, the first constraint is kept
--- and the second constraint is deleted.
(\\) :: Goal dom chr -> CHR dom chr -> CHR dom chr
g1 \\ (SimplRule lchrs guard rcs)
  | not (null (primsOfGoal g1))
  = error "Simpagation rule with primitive kept constraints!"
  | null keptcs -- to omit trivial uses of simpagation rule
  = SimplRule lchrs guard rcs
  | null lchrs -- to omit trivial uses of simpagation rule
  = PropaRule keptcs guard rcs
  | otherwise = SimpaRule keptcs lchrs guard rcs
 where
  keptcs = uchrOfGoal g1

--- A rule with a guard.
(|>) :: CHR dom chr -> Goal dom chr -> CHR dom chr
rule |> g3 = attachGuard rule
 where
  attachGuard (SimplRule lcs guard rcs) =
    if null (uchrOfGoal rcs)
      then SimplRule lcs (guard ++ primsOfGoal rcs) g3
      else error "Rule contains a guard with non-primitive constraints!"
  attachGuard (PropaRule lcs guard rcs) =
    if null (uchrOfGoal rcs)
      then PropaRule lcs (guard ++ primsOfGoal rcs) g3
      else error "Rule contains a guard with non-primitive constraints!"
  attachGuard (SimpaRule h1 h2 guard rcs) =
    if null (uchrOfGoal rcs)
      then SimpaRule h1 h2 (guard ++ primsOfGoal rcs) g3
      else error "Rule contains a guard with non-primitive constraints!"


------------------------------------------------------------------------------
-- Data types for defining CHR goals and constraints.

--- A CHR constraint is either a primitive or a user-defined constraint.
data CHRconstr dom chr = PrimCHR (PrimConstraint dom) | UserCHR chr

--- A CHR goal is a list of CHR constraints (primitive or user-defined).
data Goal dom chr = Goal [CHRconstr dom chr]

--- Conjunction of CHR goals.
(/\) :: Goal dom chr -> Goal dom chr -> Goal dom chr
(/\) (Goal c1) (Goal c2) = Goal (c1 ++ c2)

--- The always satisfiable CHR constraint.
true :: Goal dom chr
true = Goal []

--- The always unsatisfiable constraint.
false :: Goal dom chr
false = primToGoal Fail

--- Join a list of CHR goals into a single CHR goal (by conjunction).
andCHR :: [Goal dom chr] -> Goal dom chr
andCHR = foldr (/\) true

--- Is a given constraint abstraction satisfied by all elements in a list?
allCHR :: (a -> Goal dom chr) -> [a] -> Goal dom chr
allCHR fc = andCHR . map fc

-- Extracts the list of user-defined constraints contained in a CHR goal.
uchrOfGoal :: Goal dom chr -> [chr]
uchrOfGoal (Goal cs) = concatMap uchr cs
 where uchr (PrimCHR _) = []
       uchr (UserCHR c) = [c]

-- Extracts the list of primitive constraints contained in a CHR goal.
primsOfGoal :: Goal dom chr -> [PrimConstraint dom]
primsOfGoal (Goal cs) = concatMap prim cs
 where prim (PrimCHR c) = [c]
       prim (UserCHR _) = []

--- Transforms a list of CHR constraints into a CHR goal.
chrsToGoal :: [chr] -> Goal dom chr
chrsToGoal cs = Goal (map UserCHR cs)

--- Transform unary CHR constraint into a CHR goal.
toGoal1 :: (a -> chr) -> a -> Goal dom chr
toGoal1 c x = Goal [UserCHR (c x)]

--- Transforms binary CHR constraint into a CHR goal.
toGoal2 :: (a -> b -> chr) -> a -> b -> Goal dom chr
toGoal2 c x y = Goal [UserCHR (c x y)]

--- Transforms a ternary CHR constraint into a CHR goal.
toGoal3 :: (a -> b -> c -> chr) -> a -> b -> c -> Goal dom chr
toGoal3 c x y z = Goal [UserCHR (c x y z)]

--- Transforms a CHR constraint of arity 4 into a CHR goal.
toGoal4 :: (a -> b -> c -> d -> chr)
        -> a -> b -> c -> d -> Goal dom chr
toGoal4 con a b c d = Goal [UserCHR (con a b c d)]

--- Transforms a CHR constraint of arity 5 into a CHR goal.
toGoal5 :: (a -> b -> c -> d -> e -> chr)
        -> a -> b -> c -> d -> e -> Goal dom chr
toGoal5 con a b c d e = Goal [UserCHR (con a b c d e)]

--- Transforms a CHR constraint of arity 6 into a CHR goal.
toGoal6 :: (a -> b -> c -> d -> e -> f -> chr)
        -> a -> b -> c -> d -> e -> f -> Goal dom chr
toGoal6 con a b c d e f = Goal [UserCHR (con a b c d e f)]

-----------------------------------------------------------------------------
-- Primitive constraints:
data PrimConstraint a = Eq a a -- equality
                      | Neq a a -- disequality
                      | Fail   -- always unsatisfiable
                      | Compare (a -> a -> Bool) a a -- ordering constraint
                      | Ground a -- ground value
                      | Nonvar a -- not an unbound variable
                      | AnyPrim (() -> Bool) -- user-defined primitive

--- Transforms a primitive constraint into a CHR goal.
primToGoal :: PrimConstraint dom -> Goal dom chr
primToGoal pc = Goal [PrimCHR pc]

--- Primitive syntactic equality on arbitrary terms.
(.=.) :: dom -> dom -> Goal dom chr
x .=. y = primToGoal (Eq x y)

--- Primitive syntactic disequality on ground(!) terms.
(./=.) :: dom -> dom -> Goal dom chr
x ./=. y = primToGoal (Neq x y)

--- Primitive less-or-equal constraint.
(.<=.) :: Ord dom => dom -> dom -> Goal dom chr
x .<=. y = primToGoal (Compare (<=) x y)

--- Primitive greater-or-equal constraint.
(.>=.) :: Ord dom => dom -> dom -> Goal dom chr
x .>=. y = primToGoal (Compare (>=) x y)

--- Primitive less-than constraint.
(.<.) :: Ord dom => dom -> dom -> Goal dom chr
x .<. y = primToGoal (Compare (<) x y)

--- Primitive greater-than constraint.
(.>.) :: Ord dom => dom -> dom -> Goal dom chr
x .>. y = primToGoal (Compare (>) x y)

--- Primitive groundness constraint (useful for guards).
ground :: dom -> Goal dom chr
ground x = primToGoal (Ground x)

--- Primitive nonvar constraint (useful for guards).
nonvar :: dom -> Goal dom chr
nonvar x = primToGoal (Nonvar x)

--- Embed user-defined primitive constraint.
anyPrim :: (() -> Bool) -> Goal dom chr
anyPrim cf = primToGoal (AnyPrim cf)

-- Evaluate primitive constraints.
evalPrimCHR :: (Data a, Eq a) => PrimConstraint a -> Bool
evalPrimCHR (Eq x y)          = x=:=y
evalPrimCHR (Neq x y)         = (x==y) =:= False
evalPrimCHR Fail              = failed
evalPrimCHR (Compare cmp x y) = (cmp x y) =:= True
evalPrimCHR (Nonvar x)        = System.IO.Unsafe.isVar x =:= False
evalPrimCHR (Ground x)        = System.IO.Unsafe.isGround x =:= True
evalPrimCHR (AnyPrim cf)      = cf ()


------------------------------------------------------------------------------
-- Interpreter for CHR constraints
------------------------------------------------------------------------------

--- Interpret CHR rules (parameterized over domain variables)
--- for a given CHR goal (second argument) and embed this as
--- a constraint solver in Curry. If user-defined CHR constraints remain
--- after applying all CHR rules, a warning showing the residual
--- constraints is issued.
solveCHR :: (Data dom, Data chr, Eq dom, Show chr) =>
            [[dom] -> CHR dom chr] -> Goal dom chr -> Bool
solveCHR prules goal =
  let residual = runCHR prules goal
  in if null residual
       then True
       else trace ("WARNING: residual CHR constraints: "++show residual++"\n")
                  True

------------------------------------------------------------------------
-- The structure and operations for the history of the interpreter.

-- type History = [([Int],Int)] -- entry: constraint indices and rule index
-- emptyHistory  = []
-- extendHistory = (:)
-- inHistory     = elem
type History = SetRBT ([Int],Int) -- entry: constraint indices and rule index

emptyHistory :: Ord a => SetRBT a
emptyHistory = empty (<=)

extendHistory :: Ord a => a -> SetRBT a -> SetRBT a
extendHistory = insert

inHistory :: Ord a => a -> SetRBT a -> Bool
inHistory = member

------------------------------------------------------------------------
--- Interpret CHR rules (parameterized over domain variables)
--- for a given CHR goal (second argument) and return the remaining
--- CHR constraints.
runCHR :: (Data dom, Data chr, Eq dom) =>
          [[dom] -> CHR dom chr] -> Goal dom chr -> [chr]
runCHR prules goal = evalCHR False prules goal

--- Interpret CHR rules (parameterized over domain variables)
--- for a given CHR goal (second argument) and return the remaining
--- CHR constraints. Trace also the active and passive constraints
--- as well as the applied rule number during computation.
runCHRwithTrace :: (Data dom, Data chr, Eq dom) =>
                   [[dom] -> CHR dom chr] -> Goal dom chr -> [chr]
runCHRwithTrace prules goal = evalCHR True prules goal

-- Interpreter for CHR (refined semantics):
evalCHR :: (Data dom, Data chr, Eq dom) =>
           Bool -> [[dom] -> CHR dom chr] -> Goal dom chr -> [chr]
evalCHR withtrace urules (Goal goal)
   | evalConstr gidx emptyHistory chrgoal [] result
   = map snd result
 where
  tracing s = if withtrace then trace s else id

  result free

  rules = zip [1..] urules

  (gidx,chrgoal) = numberCHR 0 goal

  solvePrims = all evalPrimCHR

  -- evaluate list of active constraints:
  evalConstr gi hist gl cstore finalcs = tracing (showAnyTerm (gl,cstore)) $
                                         evalC gl cstore finalcs
   where
    evalC [] cs rcs = cs =:= rcs -- no active constraints left to work on
    evalC (PrimCHR pc : gs) cs rcs = -- awake all passive constraints:
      tracing ("Evaluate primitive: " ++ showAnyTerm pc) $
      evalPrimCHR pc & evalConstr gi hist (map UserCHR cs ++ gs) [] rcs
    evalC (UserCHR c  : gs) cs rcs =
      (normalForm c) -- necessary to evaluate functions in c's arguments
         `seq` tryRules gi hist rules c gs cs rcs

  -- try to apply CHR rules in sequential order to first active constraint:
  tryRules gi hs [] c gs cs rcs = -- no CHR rule applicable, try solve a prim:
    maybe (tracing "Suspend constraint" $
           evalConstr gi hs gs (c:cs) rcs) -- suspend first active constraint
          (\ (pc,mgs) -> tracing ("Evaluate primitive: " ++ showAnyTerm pc) $
                         evalPrimCHR pc & -- awake all passive constraints:
                         evalConstr gi hs (map UserCHR (c:cs) ++ mgs) [] rcs)
          (extractPrim gs)
  tryRules gi hist ((ri,r) : rs) c gs cs rcs =
    maybe (tryRules gi hist rs c gs cs rcs)
          (\ (newcs,newgs,remcs,is) ->
             if (is,ri) `inHistory` hist -- rule already applied?
             then tryRules gi hist rs c gs cs rcs
             else --trace (show (is,ri)) $
                  let (gj,inewcs) = numberCHR gi newcs
                   in tracing ("Apply rule " ++ show ri) $
                      evalConstr gj
                                 (if null is then hist
                                  else extendHistory (is,ri) hist)
                                 (inewcs++newgs)
                                 remcs rcs)
          (rewriteSome (applyRule (r unknown) c gs cs))

  -- Apply a CHR rule to an active constraint and constraint store
  -- and return the new goal, remaining constraint store and indices
  -- of the CHR constraints matched for the left-hand side, if it is
  -- a propogation rule (in this case, it is stored in the history to
  -- avoid re-application of the same rule).
  applyRule (SimplRule lchrs guard (Goal rchrs)) (_,c) gs cs
    | deleteSome c lchrs =:= lhs & findDelete lhs cs =:= (delcs,remcs)
      &> solvePrims guard
    = (rchrs,gs,remcs,[])                         where lhs,delcs,remcs free
  applyRule (PropaRule lchrs guard (Goal rchrs)) (i,c) gs cs
    | deleteSome c lchrs =:= lhs & findDelete lhs cs =:= (delcs,_)
      &> solvePrims guard
    = (rchrs, UserCHR (i,c) : gs, cs, i : map fst delcs)  where lhs,delcs free
  applyRule (SimpaRule kept lchrs guard (Goal rchrs)) (_,c) gs cs
    | deleteSome c lchrs =:= lhs & findDelete (kept++lhs) cs =:= (delcs,remcs)
      &> solvePrims guard
    = (rchrs, gs, take (length kept) delcs ++ remcs, [])
   where lhs,delcs,remcs free
  applyRule (SimpaRule kept lchrs guard (Goal rchrs)) (i,c) gs cs
    | deleteSome c kept =:= kc & findDelete (kc++lchrs) cs =:= (delcs,remcs)
      &> solvePrims guard
    = (rchrs, UserCHR (i,c) : gs, take (length kc) delcs ++ remcs, [])
   where kc,delcs,remcs free

-- Auxiliary operations:

-- Find a list of elements in another list and return the remaining ones:
findDelete :: Data a => [a] -> [(Int,a)] -> ([(Int,a)],[(Int,a)])
findDelete []     cs = ([],cs)
findDelete (x:xs) cs = let (z,ds) = del x cs
                           (zs,es) = findDelete xs ds
                        in (z:zs,es)
 where
  del e (z:zs) | e=:=snd z = (z,zs)
  del e (z:zs) = let (y,ys) = del e zs in (y, z:ys)

deleteSome :: Data a => a -> [a] -> [a]
deleteSome e (z:zs) | e=:=z = zs
deleteSome e (z:zs) = z : deleteSome e zs

-- Finds and deletes the first primitive constraint in a CHR goal:
extractPrim :: [CHRconstr dom chr]
            -> Maybe (PrimConstraint dom, [CHRconstr dom chr])
extractPrim [] = Nothing
extractPrim (PrimCHR pc : cs) = Just (pc, cs)
extractPrim (UserCHR c : cs) =
  maybe Nothing
        (\ (pc,rcs) -> Just (pc, UserCHR c : rcs))
        (extractPrim cs)

-- Add a unique number to each CHR constraint.
numberCHR :: Int -> [CHRconstr dom chr] -> (Int, [CHRconstr dom (Int,chr)])
numberCHR i [] = (i,[])
numberCHR i (PrimCHR pc : cs) =
  let (j,ics) = numberCHR i cs in (j, PrimCHR pc : ics)
numberCHR i (UserCHR c : cs) =
  let (j,ics) = numberCHR (i+1) cs in (j, UserCHR (i,c) : ics)


----------------------------------------------------------------------
-- Compiler from Curry CHR rules into CHR(Prolog) rules where
-- operations from the Curry program can also be called from the
-- CHR(Prolog) code.

--- Compile a list of CHR(Curry) rules into CHR(Prolog) and store its interface
--- in a Curry program (name given as first argument).
--- The second argument is the name of the module containing the
--- CHR(Curry) rules.
compileCHR :: String -> String -> [[dom] -> CHR dom chr] -> IO ()
compileCHR currymod sourcemodname rules
  | null rids = putStrLn "No CHR rules to compile."
  | otherwise = compileRules sourcemodname currymod rids
 where
  rids = map ruleId rules

-- extract the name of a rule:
ruleId :: ([dom] -> CHR dom chr) -> String
ruleId rule =
  let rcallstring = showAnyExpression rule -- "(partcall 1 funid [])"
  in takeWhile (not . isSpace) (drop (length "(partcall 1 ") rcallstring)

-- Rename the identifiers of CHR rules (first argument) to avoid name conflicts
-- with the standard compiled rules.
rnmCHR :: String -> [QName] -> QName -> QName
rnmCHR chrmodname allchrids qn@(_,fn)
  | qn `elem` allchrids = (chrmodname, fn ++ "$CHR")
  | otherwise           = qn

-- compile all specifed CHR rules to CHR(Prolog):
compileRules :: String -> String -> [String] -> IO ()
compileRules modname chrmodname rids = do
  (Prog _ _ _ fdecls opdecls) <- readFlatCurry modname
  let getftype = getFuncType fdecls
      rdefs = filter (\ (Func fname _ _ _ _) -> snd fname `elem` rids) fdecls
      (chrs,_) = unzip (map (compileRule getftype id []) (map funcRule rdefs))
      allchrs = nub (concat chrs)
      rnmchr = rnmCHR chrmodname (map fst allchrs)
      (_,trules) = unzip (map (compileRule getftype rnmchr allchrs)
                              (map funcRule rdefs))
      allchrtypes = zip allchrs (map getftype (map fst allchrs))
      curryprog = showCHRModule modname chrmodname opdecls allchrtypes
      prologprog = unlines $
        map showPlClause
          ([PlDirective [PlLit "use_module"
                               [PlStruct "library" [PlAtom "chr"]]]] ++
           map (\ (p,a) ->
                  PlDirective
                     [PlLit "chr_constraint"
                            [PlStruct "/" [PlAtom (showPlName (rnmchr p)),
                                           PlInt a]]])
               allchrs) ++
        ["","% CHR rules:"] ++ trules ++ ["","% Curry/Prolog interface:"] ++
        map (showPlClause . chrPrologPrimDefinition chrmodname rnmchr) allchrs ++
        ["","% Auxiliary predicates:",
         "sunif(X,Y) :- user:evalToken(E), user:hnf('Prelude.constrEq'(X,Y),_,E,_).",
         "eval(X) :- user:evalToken(E), user:hnf(X,_,E,_)."]
  writeFile (chrmodname ++ ".curry") curryprog
  writeFile (chrmodname ++ ".pakcs.pl") prologprog
  --putStrLn curryprog
  --putStrLn prologprog
  putStrLn $ "Curry interface to CHR(Prolog) written to "++chrmodname++".curry"

getFuncType :: [FuncDecl] -> (String,String) -> TypeExpr
getFuncType fdecls qfname =
  maybe (error $ showQName qfname ++ " not found!")
        (stripForall . funcType)
        (find (\ (Func qf _ _ _ _) -> qf == qfname) fdecls)
 where
  stripForall te = case te of ForallType _ t -> t
                              _              -> te

chrPrologPrimDefinition :: String -> (QName -> QName) -> (QName,Int) -> PlClause
chrPrologPrimDefinition chrmodname rnmchr (qcname,carity) =
  PlClause
    (chrmodname ++ "." ++ showCName ("prim_"++snd qcname))
    (map PlVar (map (\i->"X"++show i) [1..carity] ++ ["R"]))
    [PlLit (showPlName (rnmchr qcname))
           (map (\i -> PlVar ("X" ++ show i)) [1 .. carity]),
     PlLit "=" [PlVar "R", PlAtom "Prelude.True"]]


-- show Curry module as interface to CHR solver implemented in Prolog:
showCHRModule :: String -> String -> [OpDecl] ->
                 [((QName,Int),TypeExpr)] -> String
showCHRModule orgmod chrmod opdecls constraints = unlines $
  ["module "++chrmod++exports++" where","",
  -- import original modules so that their code is available for
  -- evaluating primitive (Curry-defined) constraints
   "import qualified CHR(chr2curry)",
   "import CHRcompiled",
   "import qualified "++orgmod,""] ++
  map showOpDecl chropdecls ++ [""] ++
  map showCurryConstraint constraints
 where
  exports = "(module CHRcompiled" ++
            concatMap (',':) (map (showCName . snd) chrqnames) ++ ")"
  chrqnames = map (fst . fst) constraints
  chropdecls = filter (\ (Op qop _ _) -> qop `elem` chrqnames) opdecls

-- show operator declaration
showOpDecl :: OpDecl -> String
showOpDecl (Op op fixity prec) = unwords [showFixity fixity,show prec,showOp op]
 where
  showFixity InfixOp  = "infix"
  showFixity InfixlOp = "infixl"
  showFixity InfixrOp = "infixr"

  showOp (_,on) = if isAlpha (head on) then '`':on++"`" else on

showCurryConstraint :: ((QName,Int),TypeExpr) -> String
showCurryConstraint (((_,cname),carity),ctype) =
  let cargtypes = argTypes carity ctype in
  showCName cname ++" :: "++ concatMap (++" -> ") cargtypes
    ++"Goal "++ showCurryType (resultType carity ctype) ++"\n"++
  showCName cname ++ concatMap (\i->" x"++show i) [1..carity] ++ " = Goal " ++
    take carity (repeat '(') ++
    showCName ("prim_"++cname) ++
    concatMap (\i->" $!! x"++show i++")") [1..carity] ++ "\n\n" ++
  showCName ("prim_"++cname) ++ " :: " ++
            concatMap (++" -> ") cargtypes ++ "Bool\n" ++
  showCName ("prim_"++cname) ++ " external\n"
 where
   resultType arity tp =
     if arity==0 then let TCons _ [_,chrtype] = tp
                       in chrtype
                 else let FuncType _ rtype = tp
                       in resultType (arity-1) rtype

   argTypes arity ftype = if arity==0 then [] else
     let FuncType atype rtype = ftype
      in showCurryType atype : argTypes (arity-1) rtype

-- generate prim_c2p specification of external operations:
constraints2xml :: String -> [(QName,Int)] -> XmlExp
constraints2xml prologmod constraints =
  xml "primitives" (map constraint2xml constraints)
 where
   constraint2xml ((_,cname),carity) =
     XElem "primitive" [("name",showCName ("prim_"++cname)),
                        ("arity",show carity)]
           [xml "library" [xtxt prologmod],
            xml "entry" [xtxt (showCName ("prim_"++cname))]]

-- compile a single CHR rule:
compileRule :: (QName -> TypeExpr) -> (QName -> QName) -> [(QName,Int)] -> Rule
            -> ([(QName,Int)],String)
compileRule _ _ _ (External _) = error "CHR.compileRule: external rule"
compileRule getftype rnmchr chrs (Rule _ rhs) =
  let (_,rchrs,trule) = exp2CHR 100 (firstBranch rhs)
   in (rchrs, trule ++ ".")
 where
  exp2CHR i exp = case exp of
    Comb FuncCall qf [a1,a2]
     | qf == (chrMod,"<=>")  -> let (j, chrs1,tgoal1) = transGoal i a1
                                    (k,_,tgoal2) = transGoal j a2
                                in (k, chrs1, sg tgoal1 ++" <=> "++ sg tgoal2)
     | qf == (chrMod,"==>")  -> let (j,chrs1,tgoal1) = transGoal i a1
                                    (k,_,tgoal2) = transGoal j a2
                                in (k, chrs1, sg tgoal1 ++" ==> "++ sg tgoal2)
     | qf == (chrMod,"\\\\") -> let (j,chrs1,tgoal1) = transGoal i a1
                                    (k,chrs2,trule2) = exp2CHR j a2
                                in (k, chrs1++chrs2, sg tgoal1 ++" \\ "++ trule2)
     | qf == (chrMod,"|>")   -> let (j,chrs1,trule1) = exp2CHR i a1
                                    (k,_,tgoal2) = transGoal j a2
                                in (k, chrs1, trule1 ++" | "++ sg tgoal2)
    _ -> error ("Cannot translate CHR rule: " ++ show exp)
   where sg = showPlGoals

  transGoal i exp = case reduceApply exp of
    Comb FuncCall qf args -> if fst qf == chrMod then transCHRPred  i qf args
                                                 else transUserPred i qf args
    _ -> error ("Cannot translate CHR literal: " ++ show exp)

  transCHRPred i (_,cname) args
   | cname=="/\\" =
      let (j,chrs1,tgoal1) = transGoal i (args!!0)
          (k,chrs2,tgoal2) = transGoal j (args!!1)
       in (k, chrs1++chrs2, tgoal1 ++ tgoal2)
   | cname=="nonvar" = (i, [], [PlLit "nonvar" [transArg (args!!0)]])
   | cname=="ground" = (i, [], [PlLit "ground" [transArg (args!!0)]])
   | cname=="true"   = (i, [], [PlLit "true" []])
   | cname=="false"  = (i, [], [PlLit "fail" []])
   | otherwise = maybe (error $ "Illegal CHR constraint: CHR."++cname)
                       (\chr2pl -> (i, [], [chr2pl (map transArg args)]))
                       (lookup cname chrPrims)

  transUserPred i qf args =
    let (j,plits,plit) = flattenLiteral i (rnmchr qf) args
        fplit = if qf `elem` map fst chrs
                  then plit
                  else if isCHRType (getftype qf)
                         then let PlLit pn pargs = plit
                              in PlLit "eval" [PlStruct "CHR.chr2curry"
                                                        [PlStruct pn pargs]]
                         else error ("Operation '"++snd qf++
                                     "' is not a CHR constraint!")
     in (j, [(qf, length args)], plits ++ [fplit])

-- check whether the type is a type of a CHR constraint
isCHRType :: TypeExpr -> Bool
isCHRType texp = case texp of
  FuncType _ rt -> isCHRType rt
  TCons qtc _   -> qtc == (chrMod,"Goal")
  _             -> False

-- get the first branch of a function definition
firstBranch :: Expr -> Expr
firstBranch exp = case exp of
  Case _ _ (Branch _ bexp : brs) ->
      if null brs
      then firstBranch bexp
      else error ("CHR rule with more than one branch: "++show exp)
  Free _ fexp                   -> firstBranch fexp
  _                             -> exp

-- reduce h.o. applications to a known function:
reduceApply :: Expr -> Expr
reduceApply exp = case exp of
  Comb FuncCall ("Prelude","apply") [a1,a2] ->
    let ra1 = reduceApply a1 in
    case ra1 of
      Comb FuncCall qf fargs -> Comb FuncCall qf (fargs++[a2])
      _ -> Comb FuncCall ("Prelude","apply") [ra1,a2]
  _ -> exp

-- Translation table for primitive CHR constraints:
chrPrims :: [(String,[PlTerm] -> PlGoal)]
chrPrims =
 [(".=." , \args -> PlLit "sunif" args),
  ("./=.", \args -> PlLit "sunif" [relApply "Prelude.==" args, pfalse]),
  (".>=.", \args -> PlLit "sunif" [relApply "Prelude.>=" args, ptrue]),
  (".<=.", \args -> PlLit "sunif" [relApply "Prelude.<=" args, ptrue]),
  (".>.",  \args -> PlLit "sunif" [relApply "Prelude.>"  args, ptrue]),
  (".<.",  \args -> PlLit "sunif" [relApply "Prelude.<"  args, ptrue])]
 where
  ptrue  = PlAtom "Prelude.True"
  pfalse = PlAtom "Prelude.False"
  relApply rel args = foldl (\f x -> PlStruct "Prelude.apply" [f,x])
                            (PlStruct rel [head args])
                            (tail args)

-- Translates an argument list of a CHR constraint and try to remove
-- partial calls.
transArgs :: [Expr] -> [PlTerm]
transArgs [] = []
transArgs (e:es) = case e of
  Comb (FuncPartCall 1) qn [] -> case es of
    []     -> [transArg e]
    e1:e1s -> transArgs (Comb FuncCall qn [e1] : e1s)
  _                           -> transArg e : transArgs es

-- Translates an argument of a CHR constraint.
transArg :: Expr -> PlTerm
transArg e = case e of
  Lit (Intc i)    -> PlInt i
  Lit (Floatc f)  -> PlFloat f
  Var i           -> PlVar ('X' : show i)
  Comb ct qf args -> case ct of
    FuncCall       -> PlStruct (showPlName qf) (map transArg args)
    ConsCall       -> PlStruct (showPlName qf) (map transArg args)
    FuncPartCall m -> genPartCall m qf args
    ConsPartCall m -> genPartCall m qf args
  _                     -> error $ "Not yet translatable argument: " ++ show e
 where
  genPartCall m qf args =
    PlStruct "partcall" [PlInt m, PlStruct (showPlName qf) [],
                         plList (map transArg args)]

-- Flatten a CHR literal: if arguments contain function calls,
-- add unification constraints for these arguments.
flattenLiteral :: Int -> QName -> [Expr] -> (Int,[PlGoal],PlGoal)
flattenLiteral i qf args =
  let (j,flits,fargs) = flattenArgs i args
   in (j, flits, PlLit (showPlName qf) (map transArg fargs))

-- Replace non-variable arguments by equalities for new variables.
-- The first argument and result is a counter for indexing new variables.
-- The second result is the Prolog code for new equalities.
flattenArgs :: Int -> [Expr] -> (Int,[PlGoal],[Expr])
flattenArgs i [] = (i,[],[])
flattenArgs i (arg:args) =
  if funcArg arg
  then let (j,flits,fargs) = flattenArgs (i+1) args
        in (j, PlLit "sunif" [PlVar ("X"++show i), transArg arg] : flits,
               Var i:fargs)
  else let (j,flits,fargs) = flattenArgs i args
        in (j, flits, arg : fargs)
 where
  funcArg e = case e of
    Lit _ -> False
    Var _ -> False
    Comb ConsCall _ cargs -> any funcArg cargs
    _     -> True

-- Shows a qualified name:
showQName :: QName -> String
showQName (mname,fname) = mname++"."++fname

-- Shows a name in Curry syntax, i.e., encode special characters as alphanum.
showCName :: String -> String
showCName s
  | all (\c -> isAlphaNum c || c=='_') s = s
  | isAlpha (head s) = concatMap (\c -> if isAlphaNum c || c=='_'
                                        then [c]
                                        else 'X':show (ord c))
                                 s
  | otherwise = "("++s++")"

-- Shows a qualified name in PAKCS Prolog syntax, i.e.,
-- encode special characters.
showPlName :: QName -> String
showPlName qn@(mn,fn)
  | qn == ("Prelude","[]") = "[]"
  | qn == ("Prelude",":")  = "."
  | all (\c -> isAlphaNum c || c=='_') fn = showQName qn
  | length fn > 1 && head fn == '_' = mn ++ '.' : concatMap encodeChar fn
  | otherwise = showQName qn
 where
  encodeChar c = if isAlphaNum c || c=='_' || c=='.'
                   then [c]
                   else let oc = ord c
                         in ['\'',intToDigit (oc `div` 16),
                                  intToDigit (oc `mod` 16)]

-- The name of the Curry CHR module:
chrMod :: String
chrMod = "CHR"

----------------------------------------------------------------------
-- Auxiliaries used in the compiled CHR(Prolog) code.

--- Transforms a primitive CHR constraint into a Curry constraint.
--- Used in the generated CHR(Prolog) code to evaluated primitive
--- constraints.
chr2curry :: (Data dom, Eq dom) => CHR.Goal dom chr -> Bool
chr2curry (CHR.Goal c) = case c of
  [CHR.PrimCHR pc] -> CHR.evalPrimCHR pc
  _                -> error "CHRcompiled.chr2curry: unexpected argument!"

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

-- Use FlatCurry pretty printer to show a non-top-level type expression.
showCurryType :: TypeExpr -> String
showCurryType te = '(' : showWidth 78 (ppTypeExp defaultOptions te) ++ ")"

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