{- |
Module      :  ./CASL/CCC/TerminationProof.hs
Description :  termination proofs for equation systems, using AProVE
Copyright   :  (c) Mingyi Liu and Till Mossakowski and Uni Bremen 2004-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  xinga@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Termination proofs for equation systems, using AProVE
-}

module CASL.CCC.TerminationProof (terminationProof) where

import CASL.AS_Basic_CASL
import CASL.Quantification
import CASL.Sign
import CASL.ToDoc
import CASL.Utils
import CASL.CCC.TermFormula

import Common.DocUtils
import Common.Id
import Common.ProofUtils
import Common.Result
import Common.Utils

import Control.Monad

import System.Directory

import Data.List (intercalate, partition)
import Data.Maybe

import qualified Data.Map as Map
import qualified Data.Set as Set

{-
   Automatic termination proof
   using AProVE, see http://aprove.informatik.rwth-aachen.de/

   interface to AProVE system, using system
   translate CASL signature to AProVE Input Language,
   CASL formulas to AProVE term rewrite systems(TRS),
   see http://aprove.informatik.rwth-aachen.de/help/html/in/trs.html

   if a equation system is terminal, then it is computable.
-}

terminationProof :: (FormExtension f, TermExtension f, Ord f) => Sign f e
  -> [FORMULA f] -> [FORMULA f] -> IO (Maybe Bool, String)
terminationProof sig fs dms =
  if null fs then return (Just True, "no formulas") else do
  let
    axhead =
      [ "(RULES"
      , "eq(t,t) -> true"
      , "eq(_,_) -> false"
      , "and(true,t) -> t"
      , "and(false,t) -> false"
      , "or(true,t) -> true"
      , "or(false,t) -> t"
      , "implies(false,t) -> true"
      , "implies(true,t) -> t"
      , "equiv(t,t) -> true"
      , "equiv(_,_) -> false"
      , "not(true) -> false"
      , "not(false) -> true"
      , "when_else(t1,true,t2) -> t1"
      , "when_else(t1,false,t2) -> t2" ]
    allVars = Set.toList . Set.map fst . Set.unions
      . map getQuantVars $ dms ++ fs
    c_vars = "(VAR t t1 t2 "
      ++ unwords (map transToken allVars) ++ ")"
    (rs, ls) = partition (isJust . maybeResult) $ map (axiom2TRS sig dms) fs
    c_axms = axhead ++ map (fromJust . maybeResult) rs ++ [")"]
  if null ls then do
      tmpFile <- getTempFile (unlines $ c_vars : c_axms) "Input.trs"
      aprovePath <- getEnvDef "HETS_APROVE" "CASL/Termination/AProVE.jar"
      mr <- timeoutCommand 20 "java"
        ("-ea" : "-jar" : aprovePath : words "-u cli -m wst -p plain"
         ++ [tmpFile])
      removeFile tmpFile
      return $ case mr of
        Nothing -> (Nothing, "timeout")
        Just (_, proof, _) -> (case words proof of
          "YES" : _ -> Just True
          "NO" : _ -> Just False
          _ -> Nothing, proof)
    else return (Nothing, unlines . map diagString $ concatMap diags ls)

keywords :: [String]
keywords = ["eq", "or", "implies", "equiv", "when_else"]
  -- others are CASL keywords
  ++ ["CONTEXTSENSITIVE", "EQUATIONS", "INNERMOST", "RULES", "STRATEGY"
     , "THEORY", "VAR"]

transStringAux :: String -> String
transStringAux = concatMap (\ c -> Map.findWithDefault [c] c charMap)

transString :: String -> String
transString s = let t = transStringAux s in
  if elem t keywords then '_' : t else t

transToken :: Token -> String
transToken = transString . tokStr

transId :: Id -> ShowS
transId (Id ts cs _) =
    showSepList id (showString . transToken) ts .
    if null cs then id else
    showString "{" . showSepList (showString "-") transId cs
    . showString "}"

-- | translate id to string
idStr :: Id -> String
idStr i = transId i ""

-- | get the name of a operation symbol
opSymName :: OP_SYMB -> String
opSymName = idStr . opSymbName

-- | get the name of a predicate symbol
predSymName :: PRED_SYMB -> String
predSymName = idStr . predSymbName

-- | create a predicate application
predAppl :: (Monad m, FormExtension f) => PRED_SYMB -> [TERM f] -> m String
predAppl p = liftM (predSymName p ++) . termsPA

-- | apply function string to argument string with brackets
apply :: String -> String -> String
apply f a = f ++ "(" ++ a ++ ")"

-- | create a binary application
applyBin :: String -> String -> String -> String
applyBin o t1 t2 = apply o $ t1 ++ "," ++ t2

-- | translate a casl term to a term of TRS(Terme Rewrite Systems)
term2TRS :: (Monad m, FormExtension f) => TERM f -> m String
term2TRS t = case unsortedTerm t of
  Qual_var var _ _ -> return $ tokStr var
  Application o ts _ -> liftM (opSymName o ++) $ termsPA ts
  Conditional t1 f t2 _ -> do
    b1 <- term2TRS t1
    c <- axiomSub f
    b2 <- term2TRS t2
    return $ apply "when_else" $ b1 ++ "," ++ c ++ "," ++ b2
  _ -> fail $ "no support for: " ++ showDoc t ""

-- | translate a list of casl terms to the patterns of a term in TRS
termsPA :: (Monad m, FormExtension f) => [TERM f] -> m String
termsPA ts = if null ts then return "" else
    liftM (apply "" . intercalate ",") $ mapM term2TRS ts

{- | translate a casl axiom to TRS-rule:
a rule without condition is represented by "A -> B" in
Term Rewrite Systems; if there are some conditions, then
follow the conditions after the symbol "|".
For example : "A -> B | C -> D, E -> F, ..." -}
axiom2TRS :: (FormExtension f, TermExtension f, Ord f, Monad m) => Sign f e
  -> [FORMULA f] -> FORMULA f -> m String
axiom2TRS sig doms f = case splitAxiom f of
  (cs, f') -> do
    r <- axiom2Rule f'
    s <- mapM (axiom2Cond sig doms) cs
    let a c = case s of
          [] -> ""
          _ -> c ++ intercalate ", " s
        t = return $ r ++ a " | "
        g = a ", "
    case f' of
      Equation t1 Strong t2 _ -> case unsortedTerm t2 of
        Conditional tt1 ff tt2 _ -> do
          e1 <- term2TRS t1
          c <- axiomSub ff
          b1 <- term2TRS tt1
          b2 <- term2TRS tt2
          return $ e1 ++ " -> " ++ b1 ++ " | "
            ++ c ++ " -> true" ++ g ++ "\n"
            ++ e1 ++ " -> " ++ b2 ++ " | "
            ++ c ++ " -> false" ++ g
        _ -> t
      _ -> t

axiom2Cond :: (FormExtension f, TermExtension f, Ord f, Monad m) => Sign f e
  -> [FORMULA f] -> FORMULA f -> m String
axiom2Cond sig doms f = let s = liftM (++ " -> true") $ axiomSub f in
  case f of
  Definedness t _ | isApp t ->
    case filter (sameOpsApp sig t . fst . fromJust . domainDef) doms of
      phi : _ ->
        let Result _ st = getSubstForm sig (quantFreeVars sig f nullRange) phi
        in case st of
             Just ((_, _), (s2, _)) ->
               let Just (_, c) = domainDef phi
               in axiom2Cond sig doms $ replaceVarsF s2 id c
             Nothing -> s
      [] -> s
  _ -> s

-- | check whether it is an application term only applied to variables
isApp :: TERM t -> Bool
isApp t = case unsortedTerm t of
  Application _ ts _ -> all isVar ts
  _ -> False

axiom2Rule :: (Monad m, FormExtension f) => FORMULA f -> m String
axiom2Rule f = case f of
  Negation f' _ -> case f' of
    Quantification {} ->
      fail "no support for negated quantification"
    Definedness t _ -> liftM (++ " -> undefined") $ term2TRS t
    _ -> liftM (++ " -> false") $ axiomSub f'
  Definedness {} -> liftM (++ " -> open") $ axiomSub f
  Equation t1 Strong t2 _ -> do
    e1 <- term2TRS t1
    e2 <- term2TRS t2
    return $ e1 ++ " -> " ++ e2
  Relation f1 Equivalence f2 _ -> do
    f3 <- axiomSub f1
    f4 <- axiomSub f2
    return $ f3 ++ " -> " ++ f4
  _ -> liftM (++ " -> true") $ axiomSub f

-- | translate a casl axiom (without conditions) to a term of TRS,
axiomSub :: (Monad m, FormExtension f) => FORMULA f -> m String
axiomSub f = case f of
  Junction j fs@(_ : _) _ -> do
    as <- mapM axiomSub fs
    return $ foldr1 (applyBin $ if j == Con then "and" else "or") as
  Negation f' _ -> liftM (apply "not") $ axiomSub f'
  Atom b _ -> return $ if b then "true" else "false"
  Predication p_s ts _ -> predAppl p_s ts
  Definedness t _ -> liftM (apply "def") $ term2TRS t
  Equation t1 _ t2 _ -> do -- support any equation
    e1 <- term2TRS t1
    e2 <- term2TRS t2
    return $ applyBin "eq" e1 e2
  Relation f1 c f2 _ -> do
    s1 <- axiomSub f1
    s2 <- axiomSub f2
    return $ applyBin (if c == Equivalence then "equiv" else "implies") s1 s2
  Quantification {} -> fail "no support for local quantifications"
  Membership {} -> fail "no support for membership tests"
  _ -> fail $ "no support for: " ++ showDoc f ""
