-----------------------------------------------------------------------------
--- Some operations to translate FlatCurry operations into SMT assertions.
---
--- @author  Michael Hanus
--- @version March 2024
---------------------------------------------------------------------------

module Verify.WithSMT
 where

import Control.Monad     ( unless, when )
import Data.Either       ( partitionEithers, rights )
import Data.IORef
import Data.List         ( (\\), find, init, isPrefixOf, last, maximum, nub
                         , partition, union )
import Data.Maybe        ( catMaybes, fromMaybe, isJust )
import Numeric           ( readHex )
import System.CPUTime    ( getCPUTime )
import System.Directory  ( doesFileExist )
import Debug.Trace

import Control.Monad.Trans.State
import Data.Tuple.Extra   ( both )
import FlatCurry.AddTypes
import FlatCurry.Build
import FlatCurry.Goodies
import FlatCurry.Names
import FlatCurry.Print
import FlatCurry.Simplify
import FlatCurry.Types as FC
import System.FilePath    ( (</>) )
import System.IOExts      ( evalCmd )
import Text.Pretty        ( pPrint, pretty, text )

import Verify.ESMT as SMT
import Verify.Helpers
import Verify.Options
import Verify.ProgInfo
import PackageConfig      ( getPackagePath )

------------------------------------------------------------------------------
-- Calls the SMT solver to check whether an assertion implies some
-- property (represented as FlatCurry expressions).
-- If the implication is `False`, the unsatisfiability of the assertion
-- is checked.
-- `Nothing` is returned if there is some error w.r.t. SMT solving.
checkUnsatisfiabilityWithSMT :: Options -> QName -> String -> IORef ProgInfo
          -> [(QName,ConsInfo)] -> [(Int,TypeExpr)] -> Expr -> IO (Maybe Bool)
checkUnsatisfiabilityWithSMT opts qf scripttitle pistore consinfos
                             vartypes assertionexp0 = do
  let assertionexp = wrapCaseWithId assertionexp0
      (cnames,fnames) = both nub
                             (partitionEithers (allQNamesInExp assertionexp))
      cnamesreq = filter (`notElem` [pre "False", pre "True", anonCons]) cnames
  --putStrLn $ "ASSERTION EXPRESSION: " ++ showExp assertionexp
  --putStrLn $ "NAMES IN ASSERTION: " ++ show (cnamesreq ++ fnames)
  loadModulesForQNames opts pistore (cnamesreq ++ fnames)
  pinfos <- fmap progInfos $ readIORef pistore
  let typedassertion = addTypes2VarExp pinfos vartypes assertionexp fcBool
  --putStrLn $ "TYPED ASSERTION EXPRESSION: " ++ showExp typedassertion
  let foassertexp   = replaceHigherOrderInExp (simpExpr typedassertion)
      foassertfuncs = rights (allQNamesInExp foassertexp)
  --putStrLn $ "SIMPLE TYPED ASSERTION EXPRESSION: " ++ showExp foassertexp
  maybe
    (transExpError typedassertion)
    (\ (assertion,varsorts) ->
       catch (checkUnsatWithSMT opts qf scripttitle pistore consinfos vartypes
                                varsorts assertion cnamesreq foassertfuncs)
             (\e -> print e >> return Nothing))
    (exp2SMTWithVars (maximum (0 : map fst vartypes))
                     Nothing foassertexp)
 where
  transExpError e = do putStrLn $ "Cannot translate expression:\n" ++ showExp e
                       return Nothing

  -- Wrap all case arguments with the identity operation.
  -- This is a work-around to fix a problem with pattern matching
  -- w.r.t. algebraic data types occurring in Z3 version 4.13.0
  -- (see example Z3BUG/match-error.smt).
  wrapCaseWithId =
    updCases (\ct e brs -> Case ct (Comb FuncCall (pre "id") [e]) brs)


checkUnsatWithSMT :: Options -> QName -> String -> IORef ProgInfo
                  -> [(QName,ConsInfo)]
                  -> [(Int,TypeExpr)] -> [(Int,Sort)]
                  -> Term -> [QName] -> [QName] -> IO (Maybe Bool)
checkUnsatWithSMT opts qf title pistore consinfos vartypes
                  extravars      -- variables representing h.o. subexps
                  assertion      -- assertion to be checked
                  assertioncons  -- constructors occurring in the assertion
                  assertfuncs =  -- defined functions occurring in assertion
  flip catch (\e -> print e >> return Nothing) $ do
  --let allsyms = nub (catMaybes
  --                     (map (\n -> maybe Nothing Just (untransOpName n))
  --                          (map qidName (allQIdsOfTerm assertion))))
  unless (null assertfuncs) $ printWhenDetails opts $
    "Translating operations into SMT: " ++ unwords (map showQName assertfuncs)
  fdecls0 <- getAllFunctions opts pistore assertfuncs
  pinfos <- fmap progInfos $ readIORef pistore
  let fdecls1 = addTypes2FuncDecls pinfos
                 (map (completeBranchesInFunc consinfos True) fdecls0)
      -- reduce to functions reachable from assertion after eliminating h.o.:
      fdecls  = usedFunctions assertfuncs
                  (map (updFuncBody replaceHigherOrderInExp) fdecls1)
  --putStrLn $ "OPERATIONS TO BE TRANSLATED:\n" ++ unlines (map showFuncDecl fdecls)
  let smtfuncs = maybe (Comment $ "ERROR translating " ++
                                  show (map funcName fdecls))
                       (\fds -> DefineSigsRec fds)
                       (mapM fun2SMT fdecls)
      fdecltvars = nub (concatMap allTVarsInFuncDecl fdecls)
  --putStrLn $ "TRANSLATED FUNCTIONS:\n" ++ pPrint (pretty smtfuncs)
  --let title1 = title ++ "\nTRANSLATED FUNCTIONS:\n" ++ pPrint (pretty smtfuncs)
  let vartypestcons = foldr union [] (map (tconsOfTypeExpr . snd) vartypes)
      funcstcons    = foldr union [] (map (tconsOfTypeExpr . funcType) fdecls)
      asserttcons   = map (\(ConsType _ tc _) -> tc)
                          (map (snd3 . infoOfCons consinfos) assertioncons)
      (primtypes,usertypes) =
         partition ((== "Prelude") . fst)
                   (union funcstcons (union vartypestcons asserttcons))
  decls <- mapM (getTypeDeclOf pistore) usertypes
  -- collect all type parameters in order to declare them as sorts:
  let tvarsInVars = foldr union []
                          (map (typeParamsOfSort . type2sort)
                          (map snd vartypes ++ map TVar fdecltvars))
      varsorts = map (\(i,te) -> (i, type2sort te)) vartypes ++ extravars
  --putStrLn $ "Assertion: " ++ pPrint (pretty assertion)
  let smt   = concatMap preludeType2SMT (map snd primtypes) ++
              [ EmptyLine ] ++
              (if null decls
                 then []
                 else [ Comment "User-defined datatypes:" ] ++
                      map tdecl2SMT decls) ++
              (if null tvarsInVars
                 then []
                 else [ EmptyLine, Comment "Polymorphic sorts:" ] ++
                      map (\tv -> DeclareSort tv 0) tvarsInVars) ++
              [ EmptyLine, smtfuncs, EmptyLine
              , Comment "Free variables:" ] ++
              map (\(i,s) -> DeclareVar (SV i s)) varsorts ++
              [ EmptyLine
              , Comment "Boolean formula of assertion (known properties):"
              , sAssert assertion, EmptyLine
              , Comment "check satisfiability:"
              , CheckSat
              ]
  --putStrLn $ "SMT commands as Curry term:\n" ++ show smt
  let preludesmt = if all ((`elem` defaultSMTTypes) . snd) primtypes
                     then "Prelude_min.smt"
                     else "Prelude.smt"
  smtprelude <- readIncludeFile preludesmt
  let scripttitle = unlines (map ("; "++) (lines title))
  printWhenAll opts $
    "RAW SMT SCRIPT:\n" ++ scripttitle ++ "\n\n" ++ showSMTRaw smt
  let smtinput = scripttitle ++ "\n" ++ smtprelude ++ showSMT smt
  printWhenDetails opts $ "SMT SCRIPT:\n" ++ showWithLineNums smtinput
  let z3opts = ["-smt2", "-T:2"]
  when (optStoreSMT opts) (storeSMT "SMT-" z3opts smtinput >> return ())
  printWhenDetails opts $
    "CALLING Z3 (with options: " ++ unwords z3opts ++ ")..."
  (ecode,out,err) <- evalCmd "z3" ("-in" : z3opts) smtinput
  when (ecode > 0) $ do
    printWhenStatus opts $ "EXIT CODE: " ++ show ecode
    outfile <- storeSMT "smterror-" z3opts smtinput
    when (optVerb opts < 3) $ printWhenStatus opts $
      "ERROR in SMT script (saved in '" ++ outfile ++ "'):\n" ++
      out ++ "\n" ++ err
  printWhenDetails opts $ "RESULT:\n" ++ out
  unless (null err) $ printWhenDetails opts $ "ERROR:\n" ++ err
  let pcvalid = let ls = lines out in not (null ls) && head ls == "unsat"
  return (if ecode>0 then Nothing else Just pcvalid)
 where
  defaultSMTTypes = ["Int","Float","Bool", "Char", "[]"]

  storeSMT fileprefix z3opts script = do
    ctime <- getCPUTime
    let outfile = fileprefix ++ transOpName qf ++ "-" ++ show ctime ++ ".smt"
        execcmt = unwords $ ["; Run with: z3"] ++ z3opts ++ [outfile]
    writeFile outfile (execcmt ++ "\n\n" ++ script)
    return outfile

--- Try to read a file in the `include` directory of the package
--  or, if this does not exists, in a local `include` directory.
readIncludeFile :: String -> IO String
readIncludeFile incfile = do
  ppinclude <- fmap (</> "include" </> incfile) getPackagePath
  exppinclude <- doesFileExist ppinclude
  if exppinclude
    then readFile ppinclude
    else do
      let localinclude = "include" </> incfile
      exlocalinclude <- doesFileExist localinclude
      if exlocalinclude
        then readFile localinclude
        else do putStrLn $ "Warning: " ++ localinclude ++ " not found!\n" ++
                           "SMT script might be incomplete!"
                return ""

-- Translate a typed variable into an SMT declaration:
typedVar2SMT :: (Int,TypeExpr) -> Command
typedVar2SMT (i,te) = DeclareVar (SV i (type2sort te))

-- Gets all type constructors occurring in a type expression.
tconsOfTypeExpr :: TypeExpr -> [QName]
tconsOfTypeExpr (TVar _) = []
tconsOfTypeExpr (FuncType a b) =  union (tconsOfTypeExpr a) (tconsOfTypeExpr b)
tconsOfTypeExpr (TCons qName texps) =
  foldr union [qName] (map tconsOfTypeExpr texps)
tconsOfTypeExpr (ForallType _ te) =  tconsOfTypeExpr te

------------------------------------------------------------------------------
-- Get all qualified names occurring in an expression which are either
-- constructor or defined function names.
allQNamesInExp :: Expr -> [Either QName QName]
allQNamesInExp e =
  trExpr (const id) (const id) comb lt fr (.) cas branch const e []
 where
  comb ct qn exp = ((classifyName ct) qn:) . foldr (.) id exp
   where classifyName FuncCall         = Right
         classifyName (FuncPartCall _) = Right
         classifyName ConsCall         = Left
         classifyName (ConsPartCall _) = Left
  lt bs exp = exp . foldr (.) id (map snd bs)
  fr _ exp = exp
  cas _ exp bs = exp . foldr (.) id bs
  branch pat exp = ((args pat)++) . exp
  args (Pattern qc _) = [Left qc]
  args (LPattern _)   = []

------------------------------------------------------------------------------
--- Shows a text with line numbers prefixed:
showWithLineNums :: String -> String
showWithLineNums txt =
  let txtlines  = lines txt
      maxlog    = ilog (length txtlines + 1)
      showNum n = (take (maxlog - ilog n) (repeat ' ')) ++ show n ++ ": "
  in unlines . map (uncurry (++)) . zip (map showNum [1..]) $ txtlines

--- The value of `ilog n` is the floor of the logarithm
--- in the base 10 of `n`.
--- Fails if `n &lt;= 0`.
--- For positive integers, the returned value is
--- 1 less the number of digits in the decimal representation of `n`.
---
--- @param n - The argument.
--- @return the floor of the logarithm in the base 10 of `n`.
ilog :: Int -> Int
ilog n | n>0 = if n<10 then 0 else 1 + ilog (n `div` 10)

---------------------------------------------------------------------------
--- Translates a type declaration into an SMT datatype declaration.
tdecl2SMT :: TypeDecl -> Command
tdecl2SMT (TypeSyn tc _ _ _) =
  error $ "Cannot translate type synonym '" ++ showQName tc ++ "' into SMT!"
tdecl2SMT (TypeNew tc _ _ _) =
  error $ "Cannot translate newtype '" ++ showQName tc ++ "' into SMT!"
tdecl2SMT (Type tc _ tvars consdecls) =
  DeclareDatatypes
   [(tcons2SMT tc, length tvars,
     DT (map (\ (v,_) -> 'T' : show v) tvars) (map tconsdecl consdecls))]
 where
  tconsdecl (Cons qn _ _ texps) =
    let cname = transOpName qn
    in DCons cname (map (texp2sel qn) (zip [1..] texps))

  texp2sel cname (i,texp) = (genSelName cname i, type2sortD True texp)

--- Generates the name of the i-th selector for a given constructor.
genSelName :: QName -> Int -> String
genSelName qc@(mn,fn) i
 | mn == "Prelude" && take 3 fn == "(,,"
 = transOpName qc ++ "_" ++ show i
 | otherwise
 = "sel" ++ show i ++ '-' : transOpName qc

--- Translates a prelude type into an SMT datatype declaration,
--- if necessary.
preludeType2SMT :: String -> [Command]
preludeType2SMT tn
 | take 3 tn == "(,,"
 = let arity = length tn -1
   in [ Comment "Declaration of tuple type:"
      , DeclareDatatypes
        [(tcons2SMT (pre tn), arity,
          DT (map (\v -> 'T' : show v) [1 .. arity])
             [DCons (transOpName (pre tn)) (map texp2sel [1 .. arity])])]]
 | otherwise
 = []
 where
  texp2sel i = (genSelName (pre tn) i, SComb ('T' : show i) [])

---------------------------------------------------------------------------
-- Translates a function declaration into a (possibly polymorphic)
-- SMT function declaration.
fun2SMT :: FuncDecl -> Maybe ([Ident],FunSig,Term)
fun2SMT (Func qn _ _ texp rule) = do
  let fsig = FunSig (transOpName qn)
                    (map type2sort (argTypes texp))
                    (type2sort (resultType texp))
  srule <- rule2SMT rule
  let tpars = union (typeParamsOfFunSig fsig) (typeParamsOfTerm srule)
  return (tpars, fsig, srule)
 where
  rule2SMT (External s) = return $
    tEqu (tComb (transOpName qn) []) (tComb ("External:" ++ s) [])
  rule2SMT (Rule vs exp) = do
    let isnd = ndExpr exp
        lhs  = tComb (transOpName qn) (map TSVar vs)
    (rhs,varsorts) <- exp2SMTWithVars (maximum (0:vs))
                                      (if isnd then Just lhs else Nothing)
                                      (simpExpr exp)
    return $
      Forall (map (\ (v,t) -> SV v (type2sort t))
                  (funcType2TypedVars vs texp))
             (Exists (map (\ (v,s) -> SV v s) varsorts)
                     (if isnd then rhs else tEqu lhs rhs))

--- Returns `True` if the expression is non-deterministic,
--- i.e., if `Or` or `Free` occurs in the expression.
ndExpr :: Expr -> Bool
ndExpr = trExpr (\_ -> False)
                (\_ -> False)
                (\_ _ nds -> or nds)
                (\bs nd -> nd || any snd bs)
                (\_ _ -> True)
                (\_ _ -> True)
                (\_ nd bs -> nd || or bs)
                (\_ -> id)
                (\nd _ -> nd)

-- Replace higher-order features, like occurrences of `Prelude.apply` and
-- partial applications, by `Prelude.failed` in an expression since they
-- cannot be handled by SMT. Later, occurrences of `Prelude.failed` in
-- SMT terms are replaced by fresh variables so that they are unspecified
-- values.
replaceHigherOrderInExp :: Expr -> Expr
replaceHigherOrderInExp =
  trExpr Var Lit updComb FC.Let Free Or Case Branch Typed
 where
  updComb ct qn args = case ct of
    FuncPartCall _ -> fcFailed
    ConsPartCall _ -> fcFailed
    FuncCall | qn == pre "apply" -> fcFailed
    _              -> Comb ct qn args

-- Translates a (Boolean) FlatCurry expression into an SMT expression.
-- If the second argument is an SMT expression, an equation between
-- this expression and the translated result expression is generated.
-- This is useful to axiomatize non-deterministic operations.
-- If successful, the translated SMT expression together with new variables
-- (which are replacements for higher-order applications) are returned.
-- The first argument is the maximum index of already used variables.
exp2SMTWithVars :: Int -> Maybe Term -> Expr -> Maybe (Term, [(Int,Sort)])
exp2SMTWithVars maxusedvar lhs exp =
  maybe Nothing
        (\t -> Just $ elimFailed maxusedvar t)
        (exp2SMT lhs (replaceHigherOrderInExp exp))

-- Translates a (Boolean) FlatCurry expression into an SMT expression.
-- If the first argument is an SMT expression, an equation between
-- this expression and the translated result expression is generated.
-- This is useful to axiomatize non-deterministic operations.
exp2SMT :: Maybe Term -> Expr -> Maybe Term
exp2SMT lhs exp = case exp of
  Var i          -> Just $ makeRHS (TSVar i)
  Lit l          -> Just $ makeRHS (lit2SMT l)
  Comb _ qf args -> mapM (exp2SMT Nothing) args >>= comb2SMT qf
  Case _ e bs -> do t <- exp2SMT Nothing e
                    bts <- mapM branch2SMT bs
                    return $ makeRHS (Match t bts)
  FC.Let bs e -> do tbs <- mapM (\(v,be) -> do t <- exp2SMT Nothing be
                                               return (v,t))
                                bs
                    t <- exp2SMT lhs e
                    return $ tLet tbs t
  Free _ _    -> Nothing --error "exp2SMT: Free"
  Typed e te  -> case e of
    Comb _ qf args | all isTyped args
       -> mapM (exp2SMT Nothing) args >>=
          return . makeRHS .
            TComb (As (transOpName qf)
                      (type2sort (foldr FuncType te (map exprType args))))
    _  -> exp2SMT lhs e
  Or    e1 e2 -> do t1 <- exp2SMT lhs e1
                    t2 <- exp2SMT lhs e2
                    return $ tDisj [t1,t2]
 where
  comb2SMT qf targs
    | qf `elem` map pre ["chr", "ord"] && length targs == 1
    = return $ makeRHS (head targs) -- chars are integers --> no conversion
    | otherwise
    = return $ makeRHS (tComb (transOpName qf) targs)

  makeRHS rhs = maybe rhs (\l -> tEqu l rhs) lhs

  branch2SMT (Branch (LPattern _) _) = Nothing -- literal patterns not supported
  branch2SMT (Branch (Pattern qf vs) e) = do
    t <- exp2SMT lhs e
    return (PComb (Id (transOpName qf)) vs, t)

--- Is a expression typed? (should go into FlatCurry.Goodies)
isTyped :: Expr -> Bool
isTyped e = case e of
  Typed _ _ -> True
  _         -> False

--- Gets the type of a typed expression. (should go into FlatCurry.Goodies)
exprType :: Expr -> TypeExpr
exprType e = case e of
  Typed _ te -> te
  _          -> error "FlatCurry.Goodies.exprType: not a typed expression"

--- Translates a literal into an SMT expression.
--- We represent character as ints.
lit2SMT :: Literal -> Term
lit2SMT (Intc i)   = TConst (TInt i)
lit2SMT (Floatc f) = TConst (TFloat f)
lit2SMT (Charc c)  = TConst (TInt (ord c))

----------------------------------------------------------------------------
-- Implementation of a transformation which replaces occurrences of
-- `Prelude_apply` by new fresh variables.

-- The state for this transformation.
data TransApplyState = TransApplyState
  { tsFreshVarIndex :: Int           -- fresh variable index
  , tsNewVars       :: [(Int,Sort)]  -- new typed variables
  }

type TAState a = State TransApplyState a

-- Transforms a term by replacing occurrences of
-- `Prelude_failed` with new fresh variables.
-- The first argument is the maximum index of already used variables.
elimFailed :: Int -> Term -> (Term, [(Int,Sort)])
elimFailed maxusedvar trm =
  let st0 = TransApplyState (maximum (maxusedvar : allVarsInTerm trm) + 1) []
      (ntrm,st1) = runState (elimFailedInTerm trm) st0
  in (ntrm, reverse (tsNewVars st1))

elimFailedInTerm :: Term -> TAState Term
elimFailedInTerm t = case t of
  TConst _      -> return t
  TSVar _       -> return t
  TComb (As n srt) [] | n == "Prelude_failed"
    -> do st <- get
          let fv = tsFreshVarIndex st
              fvt = (fv, srt) -- sort is type of `failed`
          put st { tsFreshVarIndex = tsFreshVarIndex st + 1
                 , tsNewVars = fvt : tsNewVars st }
          return (TSVar fv)
  TComb qid ts  -> mapM elimFailedInTerm ts >>= return . TComb qid
  SMT.Let bs bt -> do trbs <- mapM (elimFailedInTerm . snd) bs
                      trbt <- elimFailedInTerm bt
                      return $ SMT.Let (zip (map fst bs) trbs) trbt
  Forall vs te  -> elimFailedInTerm te >>= return . Forall vs
  Exists vs te  -> elimFailedInTerm te >>= return . Exists vs
  Match mt brs  -> do trmt <- elimFailedInTerm mt
                      trbs <- mapM (elimFailedInTerm . snd) brs
                      return $ Match trmt (zip (map fst brs) trbs)

-- All variables occurring in a SMT term.
allVarsInTerm :: Term -> [SVar]
allVarsInTerm (TConst _)      = []
allVarsInTerm (TSVar v)       = [v]
allVarsInTerm (TComb _ args)  = foldr union [] (map allVarsInTerm args)
allVarsInTerm (Forall vs arg) = union (map varOfSV vs) (allVarsInTerm arg)
allVarsInTerm (Exists vs arg) = union (map varOfSV vs) (allVarsInTerm arg)
allVarsInTerm (SMT.Let bs e)  =
  foldr union (map fst bs) (map allVarsInTerm (e : map snd bs))
allVarsInTerm (Match e ps)    =
  foldr union [] (map allVarsInTerm (e : map snd ps) ++ map (patVars . fst) ps)
 where
  patVars (PComb _ vs) = vs

varOfSV :: SortedVar -> SVar
varOfSV (SV v _) = v

----------------------------------------------------------------------------
--- Translates a FlatCurry type expression into a corresponding SMT sort.
--- Type variables are translated into the sort `TVar` where a
--- type variable index is appended (`TVari`) in order to generate
--- a polymorphic sort (which will later be translated by the
--- SMT translator).
--- The types `TVar` and `Func` are defined in the SMT prelude
--- which is always loaded.
type2sort :: TypeExpr -> Sort
type2sort  = type2sortD False

--- Similarly as 'type2sort' but type variables are shown as `Ti`
--- if the first argument is true, which is used when generating
--- algebraic data tyep declarations.
type2sortD :: Bool -> TypeExpr -> Sort
type2sortD dt = t2s
 where
  t2s texp = case texp of
    TVar i           -> SComb ((if dt then "T" else "TVar") ++ show i) []
    TCons qc targs   -> SComb (tcons2SMT qc) (map t2s targs)
    FuncType dom ran -> SComb "Func" (map t2s [dom,ran])
    ForallType _ te  -> t2s te
     --error "Veriy.WithSMT.type2SMT: cannot translate ForallType"

--- Translates a FlatCurry type constructor name into SMT.
tcons2SMT :: QName -> String
tcons2SMT (mn,tc)
 | "_Dict#" `isPrefixOf` tc
 = "Dict" -- since we do not yet consider class dictionaries...
 | mn == "Prelude" && take 3 tc == "(,,"
 = "Tuple" ++ show (length tc - 1)
 | mn == "Prelude"
 = maybe (encodeSpecialChars tc) id (lookup tc transPrimTCons)
 | otherwise
 = mn ++ "_" ++ encodeSpecialChars tc

--- Primitive type constructors from the prelude and their SMT names.
transPrimTCons :: [(String,String)]
transPrimTCons =
  [("Int","Int")
  ,("Float","Real")
  ,("Char","Int")  -- Char is represented as Int
  ,("[]","List")
  ,("()","Unit")
  ,("(,)","Pair")
  ,("Maybe","Maybe")
  ,("Either","Either")
  ,("Ordering","Ordering")
  ]

--- Encode special characters in strings  
encodeSpecialChars :: String -> String
encodeSpecialChars = concatMap encChar
 where
  encChar c | c `elem` "#$%[]()!,"
            = let oc = ord c
              in ['%', int2hex (oc `div` 16), int2hex(oc `mod` 16)]
            | otherwise = [c]

  int2hex i = if i<10 then chr (ord '0' + i)
                      else chr (ord 'A' + i - 10)

--- Translates urlencoded string into equivalent ASCII string.
decodeSpecialChars :: String -> String
decodeSpecialChars [] = []
decodeSpecialChars (c:cs)
  | c == '%'  = let n = case readHex (take 2 cs) of
                          [(h,"")] -> h
                          _        -> 0
                in chr n : decodeSpecialChars (drop 2 cs)
  | otherwise = c : decodeSpecialChars cs

--- Translates a qualified FlatCurry name into an SMT string.
transOpName :: QName -> String
transOpName (mn,fn)
 | mn=="Prelude" = fromMaybe tname (lookup fn primNames)
 | otherwise     = tname
 where
  tname = mn ++ "_" ++ encodeSpecialChars fn

--- Translates a (translated) SMT string back into qualified FlatCurry name.
--- Returns Nothing if it was not a qualified name.
untransOpName :: String -> Maybe QName
untransOpName s =
  let (mn,ufn) = break (=='_') s
  in if null ufn
       then Nothing
       else Just (mn, decodeSpecialChars (tail ufn))

----------------------------------------------------------------------------
--- Some primitive names of the prelude and their SMT names.
primNames :: [(String,String)]
primNames =
  [ -- Operations
  ("&&","and")
  ,("||","or")
  ,("not","not")
  ,("==","=")
  ,("/=","/=")
  ,("===","=")
  ,("/==","/=")
  ,("=","=")
  ,("<","<")
  ,("<=","<=")
  ,(">",">")
  ,(">=",">=")
  ,("+","+")
  ,("-","-")
  ,("*","*")
  -- Constructors:
  ,("True","true")
  ,("False","false")
  ,("[]","nil")
  ,(":","insert")
  ,("()","unit")
  ,("(,)","mk-pair")
  ,("LT","LT")
  ,("EQ","EQ")
  ,("GT","GT")
  ,("Nothing","Nothing")
  ,("Just","Just")
  ,("Left","Left")
  ,("Right","Right")
  ,("_","_") -- for anonymous patterns in case expressions
  ] ++
  map (\i -> ('(' : take (i-1) (repeat ',') ++ ")", "Tuple" ++ show i)) [3..15]

------------------------------------------------------------------------------
--- Extract all user-defined FlatCurry functions that might be called
--- by a given list of function names provided as the last argument.
--- The second argument is an `IORef` to the currently loaded modules.
--- Its contents will be extended when necessary.
getAllFunctions :: Options -> IORef ProgInfo -> [QName] -> IO [FuncDecl]
getAllFunctions opts pistore newfuns = do
  mods <- fmap (map (miProg . snd) . progInfos) $ readIORef pistore
  getAllFuncs mods preloadedFuncDecls newfuns
 where
  getAllFuncs _       currfuncs [] = return (reverse currfuncs)
  getAllFuncs allmods currfuncs (newfun:newfuncs)
    | newfun `elem` excludedCurryOperations ||
      newfun `elem` map (pre . fst) primNames ||
      newfun `elem` map funcName currfuncs || isPrimOp newfun
    = getAllFuncs allmods currfuncs newfuncs
    | fst newfun `elem` map progName allmods -- module already loaded:
    = maybe (error $ "getAllFunctions: " ++ show newfun ++ " not found!")
            (\fdecl -> --print fdecl >>
                       getAllFuncs allmods (fdecl : currfuncs)
                         (newfuncs ++
                          filter (`notElem` excludedCurryOperations)
                                 (funcsOfFuncDecl fdecl)))
            (find (\fd -> funcName fd == newfun)
                  (maybe []
                         progFuncs
                         (find (\m -> progName m == fst newfun) allmods)))
    | otherwise -- we must load a new module
    = do let mname = fst newfun
         printWhenStatus opts $
           "Loading module '" ++ mname ++ "' for '"++ snd newfun ++"'"
         addModInfoFor pistore mname
         newmod <- fmap miProg $ getModInfoFor pistore mname
         getAllFuncs (newmod : allmods) currfuncs (newfun:newfuncs)

--- Removes from a list of function declarations the functions not used
--- by an initial list of function names.
--- It is assumed that the list of functions is already sorted by
--- dependencies (ealier functions might call later ones).
usedFunctions :: [QName] -> [FuncDecl] -> [FuncDecl]
usedFunctions _ [] = []
usedFunctions usedfns (fdecl : fdecls)
  | funcName fdecl `elem` usedfns
  = fdecl : usedFunctions (union (funcsOfFuncDecl fdecl) usedfns) fdecls
  | otherwise
  = usedFunctions usedfns fdecls

--- Extract all user-defined FlatCurry functions that might be called
--- by a given list of function names provided as the last argument.
--- The second argument is an `IORef` to the currently loaded modules.
--- Its contents will be extended when necessary.
loadModulesForQNames :: Options -> IORef ProgInfo -> [QName] -> IO ()
loadModulesForQNames opts pistore qns = mapM_ loadMod (nub (map fst qns))
 where
  loadMod m = do
    mloaded <- hasModInfoFor pistore m
    unless mloaded $ do -- we must load a new module
      printWhenStatus opts $ "Loading module '" ++ m ++ "'..."
      addModInfoFor pistore m

-- Pre-loaded operations from the prelude to avoid reading the prelude
-- for simple operations.
preloadedFuncDecls :: [FuncDecl]
preloadedFuncDecls =
  [Func (pre "id") 1 Public
     (FuncType (TVar 0) (TVar 0))
     (Rule [1] (Var 1)),
   Func (pre  "not") 1  Public
     (FuncType fcBool fcBool)
     (Rule  [1] (Case Flex (Var 1)
                  [Branch (Pattern (pre "True") [] ) fcFalse,
                   Branch (Pattern (pre "False") []) fcTrue])),
   Func (pre "null") 1 Public
     (FuncType (fcList (TVar 0)) fcBool)
     (Rule [1] (Case Flex (Var 1)
                  [Branch (Pattern (pre "[]") [])   fcTrue,
                   Branch (Pattern (pre ":") [2,3]) fcFalse]))
  ]

--- Exclude character-related operations since characters are treated as
--- integers so that these operations are not required.
excludedCurryOperations :: [QName]
excludedCurryOperations =
  map pre ["apply", "failed", "chr", "ord"]

--- Returns the names of all functions occurring in the
--- body of a function declaration.
funcsOfFuncDecl :: FuncDecl -> [QName]
funcsOfFuncDecl fd =
  nub (trRule (\_ e -> funcsInExpr e) (\_ -> []) (funcRule fd))

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