content: {- |
  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 qualified Control.Monad.Fail as Fail
  
  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 :: (Fail.MonadFail 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 :: (Fail.MonadFail 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.fail $ "no support for: " ++ showDoc t ""
  
  -- | translate a list of casl terms to the patterns of a term in TRS
  termsPA :: (Fail.MonadFail 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, Fail.MonadFail 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, Fail.MonadFail 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 :: (Fail.MonadFail m, FormExtension f) => FORMULA f -> m String
  axiom2Rule f = case f of
    Negation f' _ -> case f' of
      Quantification {} ->
        Fail.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 :: (Fail.MonadFail 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.fail "no support for local quantifications"
    Membership {} -> Fail.fail "no support for membership tests"
    _ -> Fail.fail $ "no support for: " ++ showDoc f ""
  