-- Defining CHRs in Curry:

--module CHR((<=>),(==>),(\\),(|>),(/\),(.<=.),
--           true,constraint_Int_Int,compileCHR) where

module CHR where

import Unsafe(showAnyQTerm)
import List(nub,intersperse)
import Char
import FlatCurry
import FlatCurryTools(showCurryType)
import XML
import System(system)
import Read(readNat)

----------------------------------------------------------------------------------
-- Definition for writing CHRs:

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

--- The data type of Constraint Handling Rules.
data CHRule goal = SimpRule goal goal
                 | PropRule goal goal
                 | SimpagRule goal goal goal -- first goal is kept if rule applicable

g1 <=> g2 = SimpRule g1 g2
g1 ==> g2 = PropRule g1 g2
g1 \\ (SimpRule g2 g3) = SimpagRule g1 g2 g3

data Goal a = C                String
            | C_a              String a
            | C_a_a            String a a
            | C_Int            String Int
            | C_Int_Int        String Int Int
            | C_Int_Int_Int    String Int Int Int
            | C_Bool           String Bool
            | C_Bool_Bool      String Bool Bool
            | C_Bool_Bool_Bool String Bool Bool Bool
            | Conjunction (Goal a) (Goal a)
            | GuardedGoal (Goal a) (Goal a) -- only used in right-hand sides

--- Conjunction of constraints.
c1 /\ c2 = Conjunction c1 c2

--- The trivial constraint.
true = C "true"

--- The unsatisfiable constraint.
fail = C "fail"

--- Built-in syntactic equality on arbitrary terms.
(.=.)  = C_a_a "="

--- Built-in less-or-equal on numbers.
x .<=. y = C_Int_Int "=<" x y

guard |> goal = GuardedGoal guard goal

----------------------------------------------------------------------------------
-- translate concrete CHRs into Prolog module:

compileCHR :: String -> [CHRule (Goal _)] -> IO ()
compileCHR chrmod chrules = do
  putStr ("Generating CHR constraint module '"++chrmod++".curry'...")
  writeFile (chrmod++"_prim.curry") (showCHRTermProg chrules)
  (prologstring,constraints,goaltype) <- showPrologCHR (chrmod++"_prim")
  --putStrLn prologstring
  writeFile (chrmod++"_prim.pl") prologstring
  system ("rm "++chrmod++"_prim.curry "++chrmod++"_prim.fcy "++chrmod++"_prim.fint")
  writeFile (chrmod++".curry") (showCHRModule chrmod constraints goaltype)
  writeXmlFileWithParams (chrmod++".prim_c2p")
          [DtdUrl "http://www.informatik.uni-kiel.de/~pakcs/primitives.dtd"]
          (constraints2xml chrmod constraints)
  putStrLn "done."

-- show Curry module as interface to CHR solver implemented in Prolog:
showCHRModule chrmod constraints goaltype =
  "module "++chrmod++" where\n\n"++
  unlines (map (showCurryConstraint goaltype) constraints)

showCurryConstraint goaltype (cname,carity,ctype) =
  let cargtypes = map (\t->if t=="a" then goaltype else t) (cconsname2types ctype) in
  cname ++" :: "++ concatMap (++" -> ") cargtypes ++ "Success\n" ++
  cname ++ concatMap (\i->" x"++show i) [1..carity] ++ " = " ++
           concatMap (\i->"seq x"++show i++" (") [1..carity] ++ "prim_"++cname ++
           concatMap (\i->" x"++show i) [1..carity] ++
           take carity (repeat ')') ++ "\n\n" ++
  "prim_"++cname++" :: "++ concatMap (++" -> ") cargtypes ++ "Success\n" ++
  "prim_"++cname++" external\n"

-- show specification of external operations:
constraints2xml chrmod constraints =
  xml "primitives" (map constraint2xml constraints)
 where
   constraint2xml (cname,carity,_) =
     XElem "primitive" [("name","prim_"++cname),("arity",show carity)]
           [xml "library" [xtxt (chrmod++"_prim")],
            xml "entry" [xtxt ("prim_"++cname)]]

-- show CHRs as Curry module containing a single main function:
showCHRTermProg chrules =
  let (freevarterm,numfreevars) = nameFreeVars (showAnyQTerm chrules) in
  "import CHR\n\n" ++
  "main = " ++ freevarterm ++"\n"++
  " where " ++ concat (intersperse "," (map (\i->"freeVar"++show i) [0..numfreevars]))
            ++ " free\n"

-- replace all "_<n>" in a string by "freeVar<n>" and return the modified string
-- together with the maximum <n>:
nameFreeVars :: String -> (String,Int)
nameFreeVars "" = ("",0)
nameFreeVars [c] = ([c],0)
nameFreeVars (c1:c2:cs) =
  if c1==' ' && c2=='_'
  then let freevaridx = readNat (takeWhile isDigit cs)
           (ncs,n) = nameFreeVars cs in (" freeVar" ++ ncs, max freevaridx n)
  else let (ncs,n) = nameFreeVars (c2:cs) in (c1:ncs,n)

----------------------------------------------------------------------------------
-- read a Curry program containing CHRs as main function and translate it
-- to Prolog CHR:
showPrologCHR currychrmainprog = do
  (Prog modname _ _ [Func _ _ _ maintype (Rule _ (Free _ mainexp))] _)
                                                   <- readFlatCurry currychrmainprog
  let constraints = constraintsOfHandler mainexp
  return (chrHeader modname constraints ++
          unlines (showHandlerRules mainexp) ++ "\n" ++
          unlines (map showChrPrimDefinition constraints),
          constraints, showChrTypeInstance maintype)

-- show the actual type instance from type expression of all rules:
showChrTypeInstance (TCons _ [TCons _ [TCons _ [texp]]]) =
  showCurryType showTCons True texp
 where
   showTCons (mn,cn) = if mn=="prelude" then cn else mn++"."++cn

chrHeader modname constraints =
  ":- module('"++modname++"',["++ concat (intersperse "," 
    (map (\ (cname,carity,_)->"prim_"++cname++"/"++show (carity+1)) constraints))
    ++"]).\n\n" ++
  ":- use_module(library(chr)).\n\n" ++
  "handler '"++modname++"'.\n\n" ++
  "constraints " ++
   concat (intersperse "," (map (\ (cname,carity,_)->cname++"/"++show carity) constraints))
   ++ ".\n\n"

showChrPrimDefinition (cname,carity,_) =
  "prim_"++cname++"("++concatMap (\i->"X"++show i++",") [1..carity]++
  "R) :- "++
  cname++"("++concat (intersperse "," (map (\i->"X"++show i) [1..carity]))++"), "++
  "R=success.\n"

----------------------------------------------------------------------------------
-- get all the constraints of a CHR handler:
constraintsOfHandler chrules =
  nub (concatMap constraintsOfRule (flatList2list chrules))

constraintsOfRule (Comb ConsCall (_,chrtype) chrargs)
  | chrtype=="SimpRule" = constraintsOfGoal (head chrargs)
  | chrtype=="PropRule" = constraintsOfGoal (head chrargs)
  | chrtype=="SimpagRule" = constraintsOfGoal (head chrargs) ++
                            constraintsOfGoal (chrargs!!1)

constraintsOfGoal (Comb ConsCall (_,cname) args)
  | cname=="GuardedGoal" = error "Guards in CHR left-hand sides not allowed!"
  | cname=="Conjunction" = constraintsOfGoal (head args) ++ constraintsOfGoal (args!!1)
  | otherwise = [(map exp2chr (flatList2list (head args)), length args - 1, cname)]

----------------------------------------------------------------------------------
-- show the rules of a CHR handler:
showHandlerRules chrules = map showFlatRule (flatList2list chrules)

showFlatRule (Comb ConsCall (_,chrtype) chrargs)
  | chrtype=="SimpRule" = showFlatGoals False (head chrargs) ++ " <=> " ++
                          showFlatGoals False (chrargs!!1) ++"."
  | chrtype=="PropRule" = showFlatGoals False (head chrargs) ++ " ==> " ++
                          showFlatGoals False (chrargs!!1) ++"."
  | chrtype=="SimpagRule" = showFlatGoals False (head chrargs) ++ " \\ " ++
                            showFlatGoals False (chrargs!!1) ++ " <=> " ++
                            showFlatGoals False (chrargs!!2) ++"."
  | otherwise = error "showFlatRule: unknown rule"

showFlatGoals isguarded (Comb ConsCall (_,cname) args)
  | cname=="GuardedGoal"
   = if isguarded
     then error "Nested guards in CHRs not allowed!"
     else showFlatGoals True (head args) ++ " | " ++ showFlatGoals True (args!!1)
  | cname=="Conjunction"
   = showFlatGoals isguarded (head args) ++ ", " ++ showFlatGoals isguarded (args!!1)
  | null (tail args) = transId (map exp2chr (flatList2list (head args)))
  | otherwise = transId (map exp2chr (flatList2list (head args))) ++
                "("++concat (intersperse "," (map showFlatExp (tail args)))++")"

transId cs | cs=="Eq" = "="
           | otherwise = toLower (head cs) : tail cs

showFlatExp e = case e of
  Var i -> "X"++show i
  Lit (Intc i) -> show i
  Lit (Floatc x) -> show x
  Lit (Charc c) -> show (ord c)
  Comb ConsCall (m,f) [] -> showPrologAtom (if m=="prelude" then f else m++"."++f)
  _ -> error $ "CHR.showFlatExp: can't handle FlatCurry expression: "++show e

-- shows a string as a Prolog atom:
showPrologAtom s | all isAlpha s && not (null s) && isLower (head s) = s
                 | otherwise = "'"++s++"'"

----------------------------------------------------------------------------------
-- translate a list in FlatCurry representation into a list of its elements:
flatList2list :: Expr -> [Expr]
flatList2list (Comb ConsCall _ []) = []
flatList2list (Comb ConsCall _ [fhead,ftail]) = fhead : flatList2list ftail

-- translate a FlatCurry character literal into the character:
exp2chr :: Expr -> Char
exp2chr (Lit (Charc c)) = c

-- "C_Int_Int" -> ["Int","Int"]
cconsname2types =  words . map (\c->if c=='_' then ' ' else c) . drop 2