{- |
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 :: Sign f e -> [FORMULA f] -> [FORMULA f] -> IO (Maybe Bool, String)
terminationProof sig :: Sign f e
sig fs :: [FORMULA f]
fs dms :: [FORMULA f]
dms =
  if [FORMULA f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FORMULA f]
fs then (Maybe Bool, String) -> IO (Maybe Bool, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, "no formulas") else do
  let
    axhead :: [String]
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 :: [VAR]
allVars = Set VAR -> [VAR]
forall a. Set a -> [a]
Set.toList (Set VAR -> [VAR])
-> ([FORMULA f] -> Set VAR) -> [FORMULA f] -> [VAR]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((VAR, SORT) -> VAR) -> Set (VAR, SORT) -> Set VAR
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (VAR, SORT) -> VAR
forall a b. (a, b) -> a
fst (Set (VAR, SORT) -> Set VAR)
-> ([FORMULA f] -> Set (VAR, SORT)) -> [FORMULA f] -> Set VAR
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set (VAR, SORT)] -> Set (VAR, SORT)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
      ([Set (VAR, SORT)] -> Set (VAR, SORT))
-> ([FORMULA f] -> [Set (VAR, SORT)])
-> [FORMULA f]
-> Set (VAR, SORT)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f -> Set (VAR, SORT)) -> [FORMULA f] -> [Set (VAR, SORT)]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA f -> Set (VAR, SORT)
forall f. FORMULA f -> Set (VAR, SORT)
getQuantVars ([FORMULA f] -> [VAR]) -> [FORMULA f] -> [VAR]
forall a b. (a -> b) -> a -> b
$ [FORMULA f]
dms [FORMULA f] -> [FORMULA f] -> [FORMULA f]
forall a. [a] -> [a] -> [a]
++ [FORMULA f]
fs
    c_vars :: String
c_vars = "(VAR t t1 t2 "
      String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((VAR -> String) -> [VAR] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map VAR -> String
transToken [VAR]
allVars) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
    (rs :: [Result String]
rs, ls :: [Result String]
ls) = (Result String -> Bool)
-> [Result String] -> ([Result String], [Result String])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (Maybe String -> Bool)
-> (Result String -> Maybe String) -> Result String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result String -> Maybe String
forall a. Result a -> Maybe a
maybeResult) ([Result String] -> ([Result String], [Result String]))
-> [Result String] -> ([Result String], [Result String])
forall a b. (a -> b) -> a -> b
$ (FORMULA f -> Result String) -> [FORMULA f] -> [Result String]
forall a b. (a -> b) -> [a] -> [b]
map (Sign f e -> [FORMULA f] -> FORMULA f -> Result String
forall f (m :: * -> *) e.
(FormExtension f, TermExtension f, Ord f, MonadFail m) =>
Sign f e -> [FORMULA f] -> FORMULA f -> m String
axiom2TRS Sign f e
sig [FORMULA f]
dms) [FORMULA f]
fs
    c_axms :: [String]
c_axms = [String]
axhead [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Result String -> String) -> [Result String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe String -> String
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe String -> String)
-> (Result String -> Maybe String) -> Result String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result String -> Maybe String
forall a. Result a -> Maybe a
maybeResult) [Result String]
rs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [")"]
  if [Result String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Result String]
ls then do
      String
tmpFile <- String -> String -> IO String
getTempFile ([String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
c_vars String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
c_axms) "Input.trs"
      String
aprovePath <- String -> String -> IO String
getEnvDef "HETS_APROVE" "CASL/Termination/AProVE.jar"
      Maybe (ExitCode, String, String)
mr <- Int -> String -> [String] -> IO (Maybe (ExitCode, String, String))
timeoutCommand 20 "java"
        ("-ea" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: "-jar" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
aprovePath String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
words "-u cli -m wst -p plain"
         [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
tmpFile])
      String -> IO ()
removeFile String
tmpFile
      (Maybe Bool, String) -> IO (Maybe Bool, String)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Maybe Bool, String) -> IO (Maybe Bool, String))
-> (Maybe Bool, String) -> IO (Maybe Bool, String)
forall a b. (a -> b) -> a -> b
$ case Maybe (ExitCode, String, String)
mr of
        Nothing -> (Maybe Bool
forall a. Maybe a
Nothing, "timeout")
        Just (_, proof :: String
proof, _) -> (case String -> [String]
words String
proof of
          "YES" : _ -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
          "NO" : _ -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
          _ -> Maybe Bool
forall a. Maybe a
Nothing, String
proof)
    else (Maybe Bool, String) -> IO (Maybe Bool, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Bool
forall a. Maybe a
Nothing, [String] -> String
unlines ([String] -> String)
-> ([Diagnosis] -> [String]) -> [Diagnosis] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Diagnosis -> String) -> [Diagnosis] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Diagnosis -> String
diagString ([Diagnosis] -> String) -> [Diagnosis] -> String
forall a b. (a -> b) -> a -> b
$ (Result String -> [Diagnosis]) -> [Result String] -> [Diagnosis]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Result String -> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags [Result String]
ls)

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

transStringAux :: String -> String
transStringAux :: String -> String
transStringAux = (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ c :: Char
c -> String -> Char -> Map Char String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault [Char
c] Char
c Map Char String
charMap)

transString :: String -> String
transString :: String -> String
transString s :: String
s = let t :: String
t = String -> String
transStringAux String
s in
  if String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
t [String]
keywords then '_' Char -> String -> String
forall a. a -> [a] -> [a]
: String
t else String
t

transToken :: Token -> String
transToken :: VAR -> String
transToken = String -> String
transString (String -> String) -> (VAR -> String) -> VAR -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VAR -> String
tokStr

transId :: Id -> ShowS
transId :: SORT -> String -> String
transId (Id ts :: [VAR]
ts cs :: [SORT]
cs _) =
    (String -> String)
-> (VAR -> String -> String) -> [VAR] -> String -> String
forall a.
(String -> String)
-> (a -> String -> String) -> [a] -> String -> String
showSepList String -> String
forall a. a -> a
id (String -> String -> String
showString (String -> String -> String)
-> (VAR -> String) -> VAR -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VAR -> String
transToken) [VAR]
ts (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    if [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
cs then String -> String
forall a. a -> a
id else
    String -> String -> String
showString "{" (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String)
-> (SORT -> String -> String) -> [SORT] -> String -> String
forall a.
(String -> String)
-> (a -> String -> String) -> [a] -> String -> String
showSepList (String -> String -> String
showString "-") SORT -> String -> String
transId [SORT]
cs
    (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString "}"

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

-- | get the name of a operation symbol
opSymName :: OP_SYMB -> String
opSymName :: OP_SYMB -> String
opSymName = SORT -> String
idStr (SORT -> String) -> (OP_SYMB -> SORT) -> OP_SYMB -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_SYMB -> SORT
opSymbName

-- | get the name of a predicate symbol
predSymName :: PRED_SYMB -> String
predSymName :: PRED_SYMB -> String
predSymName = SORT -> String
idStr (SORT -> String) -> (PRED_SYMB -> SORT) -> PRED_SYMB -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRED_SYMB -> SORT
predSymbName

-- | create a predicate application
predAppl :: (Fail.MonadFail m, FormExtension f) => PRED_SYMB -> [TERM f] -> m String
predAppl :: PRED_SYMB -> [TERM f] -> m String
predAppl p :: PRED_SYMB
p = (String -> String) -> m String -> m String
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (PRED_SYMB -> String
predSymName PRED_SYMB
p String -> String -> String
forall a. [a] -> [a] -> [a]
++) (m String -> m String)
-> ([TERM f] -> m String) -> [TERM f] -> m String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TERM f] -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
[TERM f] -> m String
termsPA

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

-- | create a binary application
applyBin :: String -> String -> String -> String
applyBin :: String -> String -> String -> String
applyBin o :: String
o t1 :: String
t1 t2 :: String
t2 = String -> String -> String
apply String
o (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
t1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t2

-- | translate a casl term to a term of TRS(Terme Rewrite Systems)
term2TRS :: (Fail.MonadFail m, FormExtension f) => TERM f -> m String
term2TRS :: TERM f -> m String
term2TRS t :: TERM f
t = case TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t of
  Qual_var var :: VAR
var _ _ -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ VAR -> String
tokStr VAR
var
  Application o :: OP_SYMB
o ts :: [TERM f]
ts _ -> (String -> String) -> m String -> m String
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (OP_SYMB -> String
opSymName OP_SYMB
o String -> String -> String
forall a. [a] -> [a] -> [a]
++) (m String -> m String) -> m String -> m String
forall a b. (a -> b) -> a -> b
$ [TERM f] -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
[TERM f] -> m String
termsPA [TERM f]
ts
  Conditional t1 :: TERM f
t1 f :: FORMULA f
f t2 :: TERM f
t2 _ -> do
    String
b1 <- TERM f -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
TERM f -> m String
term2TRS TERM f
t1
    String
c <- FORMULA f -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
FORMULA f -> m String
axiomSub FORMULA f
f
    String
b2 <- TERM f -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
TERM f -> m String
term2TRS TERM f
t2
    String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ String -> String -> String
apply "when_else" (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
b1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
b2
  _ -> String -> m String
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ "no support for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TERM f -> String -> String
forall a. Pretty a => a -> String -> String
showDoc TERM f
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 :: [TERM f] -> m String
termsPA ts :: [TERM f]
ts = if [TERM f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM f]
ts then String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return "" else
    ([String] -> String) -> m [String] -> m String
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (String -> String -> String
apply "" (String -> String) -> ([String] -> String) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ",") (m [String] -> m String) -> m [String] -> m String
forall a b. (a -> b) -> a -> b
$ (TERM f -> m String) -> [TERM f] -> m [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TERM f -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
TERM f -> m String
term2TRS [TERM f]
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 :: Sign f e -> [FORMULA f] -> FORMULA f -> m String
axiom2TRS sig :: Sign f e
sig doms :: [FORMULA f]
doms f :: FORMULA f
f = case FORMULA f -> ([FORMULA f], FORMULA f)
forall f. FORMULA f -> ([FORMULA f], FORMULA f)
splitAxiom FORMULA f
f of
  (cs :: [FORMULA f]
cs, f' :: FORMULA f
f') -> do
    String
r <- FORMULA f -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
FORMULA f -> m String
axiom2Rule FORMULA f
f'
    [String]
s <- (FORMULA f -> m String) -> [FORMULA f] -> m [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign f e -> [FORMULA f] -> FORMULA f -> m String
forall f (m :: * -> *) e.
(FormExtension f, TermExtension f, Ord f, MonadFail m) =>
Sign f e -> [FORMULA f] -> FORMULA f -> m String
axiom2Cond Sign f e
sig [FORMULA f]
doms) [FORMULA f]
cs
    let a :: String -> String
a c :: String
c = case [String]
s of
          [] -> ""
          _ -> String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
s
        t :: m String
t = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ String
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
a " | "
        g :: String
g = String -> String
a ", "
    case FORMULA f
f' of
      Equation t1 :: TERM f
t1 Strong t2 :: TERM f
t2 _ -> case TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t2 of
        Conditional tt1 :: TERM f
tt1 ff :: FORMULA f
ff tt2 :: TERM f
tt2 _ -> do
          String
e1 <- TERM f -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
TERM f -> m String
term2TRS TERM f
t1
          String
c <- FORMULA f -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
FORMULA f -> m String
axiomSub FORMULA f
ff
          String
b1 <- TERM f -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
TERM f -> m String
term2TRS TERM f
tt1
          String
b2 <- TERM f -> m String
forall (m :: * -> *) f.
(MonadFail m, FormExtension f) =>
TERM f -> m String
term2TRS TERM f
tt2
          String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ String
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
b1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " | "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -> true" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
g String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
b2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " | "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -> false" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
g
        _ -> m String
t
      _ -> m String
t

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

-- | check whether it is an application term only applied to variables
isApp :: TERM t -> Bool
isApp :: TERM t -> Bool
isApp t :: TERM t
t = case TERM t -> TERM t
forall f. TERM f -> TERM f
unsortedTerm TERM t
t of
  Application _ ts :: [TERM t]
ts _ -> (TERM t -> Bool) -> [TERM t] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TERM t -> Bool
forall t. TERM t -> Bool
isVar [TERM t]
ts
  _ -> Bool
False

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

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