{- |
Module      :  ./CASL/CCC/TermFormula.hs
Description :  auxiliary functions on terms and formulas
Copyright   :  (c) Mingyi Liu, Till Mossakowski, Uni Bremen 2004-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Auxiliary functions on terms and formulas
-}

module CASL.CCC.TermFormula where

import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.Overload
import CASL.Quantification
import CASL.Sign
import CASL.ToDoc
import CASL.Utils

import Common.Id
import Common.Result

import Control.Monad

import Data.Function
import Data.List
import Data.Maybe

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

-- | the sorted term is always ignored
unsortedTerm :: TERM f -> TERM f
unsortedTerm :: TERM f -> TERM f
unsortedTerm t :: TERM f
t = case TERM f
t of
  Sorted_term t' :: TERM f
t' _ _ -> TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t'
  Cast t' :: TERM f
t' _ _ -> TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t'
  _ -> TERM f
t

-- | check whether it exist a (unique)existent quantification
isExQuanti :: FORMULA f -> Bool
isExQuanti :: FORMULA f -> Bool
isExQuanti f :: FORMULA f
f = case FORMULA f
f of
  Quantification Universal _ f' :: FORMULA f
f' _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
isExQuanti FORMULA f
f'
  Quantification {} -> Bool
True
  Relation f1 :: FORMULA f
f1 _ f2 :: FORMULA f
f2 _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
isExQuanti FORMULA f
f1 Bool -> Bool -> Bool
|| FORMULA f -> Bool
forall f. FORMULA f -> Bool
isExQuanti FORMULA f
f2
  Negation f' :: FORMULA f
f' _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
isExQuanti FORMULA f
f'
  _ -> Bool
False

-- | check whether it contains a membership formula
isMembership :: FORMULA f -> Bool
isMembership :: FORMULA f -> Bool
isMembership f :: FORMULA f
f = case FORMULA f
f of
  Quantification _ _ f' :: FORMULA f
f' _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
isMembership FORMULA f
f'
  Junction _ fs :: [FORMULA f]
fs _ -> (FORMULA f -> Bool) -> [FORMULA f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any FORMULA f -> Bool
forall f. FORMULA f -> Bool
isMembership [FORMULA f]
fs
  Negation f' :: FORMULA f
f' _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
isMembership FORMULA f
f'
  Relation f1 :: FORMULA f
f1 _ f2 :: FORMULA f
f2 _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
isMembership FORMULA f
f1 Bool -> Bool -> Bool
|| FORMULA f -> Bool
forall f. FORMULA f -> Bool
isMembership FORMULA f
f2
  Membership {} -> Bool
True
  _ -> Bool
False

-- | check whether it contains a definedness formula
containDef :: FORMULA f -> Bool
containDef :: FORMULA f -> Bool
containDef f :: FORMULA f
f = case FORMULA f
f of
  Quantification _ _ f' :: FORMULA f
f' _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
containDef FORMULA f
f'
  Junction _ fs :: [FORMULA f]
fs _ -> (FORMULA f -> Bool) -> [FORMULA f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any FORMULA f -> Bool
forall f. FORMULA f -> Bool
containDef [FORMULA f]
fs
  Relation f1 :: FORMULA f
f1 _ f2 :: FORMULA f
f2 _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
containDef FORMULA f
f1 Bool -> Bool -> Bool
|| FORMULA f -> Bool
forall f. FORMULA f -> Bool
containDef FORMULA f
f2
  Negation f' :: FORMULA f
f' _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
containDef FORMULA f
f'
  Definedness _ _ -> Bool
True
  _ -> Bool
False

-- | check whether it contains a negation
containNeg :: FORMULA f -> Bool
containNeg :: FORMULA f -> Bool
containNeg f :: FORMULA f
f = case FORMULA f
f of
  Quantification _ _ f' :: FORMULA f
f' _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
f'
  Relation _ c :: Relation
c f' :: FORMULA f
f' _ | Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
/= Relation
Equivalence -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
f'
  Relation f' :: FORMULA f
f' Equivalence _ _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
f'
  Negation _ _ -> Bool
True
  _ -> Bool
False

domainDef :: FORMULA f -> Maybe (TERM f, FORMULA f)
domainDef :: FORMULA f -> Maybe (TERM f, FORMULA f)
domainDef f :: FORMULA f
f = case FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripAllQuant FORMULA f
f of
  Relation (Definedness t :: TERM f
t _) Equivalence f' :: FORMULA f
f' _
    | Bool -> Bool
not (FORMULA f -> Bool
forall f. FORMULA f -> Bool
containDef FORMULA f
f') -> (TERM f, FORMULA f) -> Maybe (TERM f, FORMULA f)
forall a. a -> Maybe a
Just (TERM f
t, FORMULA f
f')
  _ -> Maybe (TERM f, FORMULA f)
forall a. Maybe a
Nothing

-- | check whether it is a Variable
isVar :: TERM t -> Bool
isVar :: TERM t -> Bool
isVar t :: TERM t
t = case TERM t -> TERM t
forall f. TERM f -> TERM f
unsortedTerm TERM t
t of
  Qual_var {} -> Bool
True
  _ -> Bool
False

-- | extract all variables of a term
varOfTerm :: Ord f => TERM f -> [TERM f]
varOfTerm :: TERM f -> [TERM f]
varOfTerm t :: TERM f
t = case TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t of
  Qual_var {} -> [TERM f
t]
  Application _ ts :: [TERM f]
ts _ -> (TERM f -> [TERM f]) -> [TERM f] -> [TERM f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TERM f -> [TERM f]
forall f. Ord f => TERM f -> [TERM f]
varOfTerm [TERM f]
ts
  _ -> []

-- | extract all arguments of a term
arguOfTerm :: TERM f -> [TERM f]
arguOfTerm :: TERM f -> [TERM f]
arguOfTerm = ((Id, Int), [TERM f]) -> [TERM f]
forall a b. (a, b) -> b
snd (((Id, Int), [TERM f]) -> [TERM f])
-> (TERM f -> ((Id, Int), [TERM f])) -> TERM f -> [TERM f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TERM f -> ((Id, Int), [TERM f])
forall f. TERM f -> ((Id, Int), [TERM f])
topIdOfTerm

nullId :: ((Id, Int), [TERM f])
nullId :: ((Id, Int), [TERM f])
nullId = ((String -> Id
stringToId "", 0), [])

topIdOfTerm :: TERM f -> ((Id, Int), [TERM f])
topIdOfTerm :: TERM f -> ((Id, Int), [TERM f])
topIdOfTerm t :: TERM f
t = case TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t of
  Application o :: OP_SYMB
o ts :: [TERM f]
ts _ -> ((OP_SYMB -> Id
opSymbName OP_SYMB
o, [TERM f] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TERM f]
ts), [TERM f]
ts)
  _ -> ((Id, Int), [TERM f])
forall f. ((Id, Int), [TERM f])
nullId

-- | get the patterns of a axiom
patternsOfAxiom :: FORMULA f -> [TERM f]
patternsOfAxiom :: FORMULA f -> [TERM f]
patternsOfAxiom = ((Id, Int), [TERM f]) -> [TERM f]
forall a b. (a, b) -> b
snd (((Id, Int), [TERM f]) -> [TERM f])
-> (FORMULA f -> ((Id, Int), [TERM f])) -> FORMULA f -> [TERM f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> ((Id, Int), [TERM f])
forall f. FORMULA f -> ((Id, Int), [TERM f])
topIdOfAxiom

topIdOfAxiom :: FORMULA f -> ((Id, Int), [TERM f])
topIdOfAxiom :: FORMULA f -> ((Id, Int), [TERM f])
topIdOfAxiom f :: FORMULA f
f = case FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripAllQuant FORMULA f
f of
    Negation f' :: FORMULA f
f' _ -> FORMULA f -> ((Id, Int), [TERM f])
forall f. FORMULA f -> ((Id, Int), [TERM f])
topIdOfAxiom FORMULA f
f'
    Relation _ c :: Relation
c f' :: FORMULA f
f' _ | Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
/= Relation
Equivalence -> FORMULA f -> ((Id, Int), [TERM f])
forall f. FORMULA f -> ((Id, Int), [TERM f])
topIdOfAxiom FORMULA f
f'
    Relation f' :: FORMULA f
f' Equivalence _ _ -> FORMULA f -> ((Id, Int), [TERM f])
forall f. FORMULA f -> ((Id, Int), [TERM f])
topIdOfAxiom FORMULA f
f'
    Predication p :: PRED_SYMB
p ts :: [TERM f]
ts _ -> ((PRED_SYMB -> Id
predSymbName PRED_SYMB
p, [TERM f] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TERM f]
ts), [TERM f]
ts)
    Equation t :: TERM f
t _ _ _ -> TERM f -> ((Id, Int), [TERM f])
forall f. TERM f -> ((Id, Int), [TERM f])
topIdOfTerm TERM f
t
    Definedness t :: TERM f
t _ -> TERM f -> ((Id, Int), [TERM f])
forall f. TERM f -> ((Id, Int), [TERM f])
topIdOfTerm TERM f
t
    _ -> ((Id, Int), [TERM f])
forall f. ((Id, Int), [TERM f])
nullId

-- | split the axiom into condition and rest axiom
splitAxiom :: FORMULA f -> ([FORMULA f], FORMULA f)
splitAxiom :: FORMULA f -> ([FORMULA f], FORMULA f)
splitAxiom f :: FORMULA f
f = case FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripAllQuant FORMULA f
f of
                     Relation f1 :: FORMULA f
f1 c :: Relation
c f2 :: FORMULA f
f2 _ | Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
/= Relation
Equivalence ->
                       let (f3 :: [FORMULA f]
f3, f4 :: FORMULA f
f4) = FORMULA f -> ([FORMULA f], FORMULA f)
forall f. FORMULA f -> ([FORMULA f], FORMULA f)
splitAxiom FORMULA f
f2 in (FORMULA f
f1 FORMULA f -> [FORMULA f] -> [FORMULA f]
forall a. a -> [a] -> [a]
: [FORMULA f]
f3, FORMULA f
f4)
                     f' :: FORMULA f
f' -> ([], FORMULA f
f')

-- | get the premise of a formula, without implication return true
conditionAxiom :: FORMULA f -> FORMULA f
conditionAxiom :: FORMULA f -> FORMULA f
conditionAxiom = [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct ([FORMULA f] -> FORMULA f)
-> (FORMULA f -> [FORMULA f]) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([FORMULA f], FORMULA f) -> [FORMULA f]
forall a b. (a, b) -> a
fst (([FORMULA f], FORMULA f) -> [FORMULA f])
-> (FORMULA f -> ([FORMULA f], FORMULA f))
-> FORMULA f
-> [FORMULA f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> ([FORMULA f], FORMULA f)
forall f. FORMULA f -> ([FORMULA f], FORMULA f)
splitAxiom

-- | get the conclusion of a formula, without implication return the formula
restAxiom :: FORMULA f -> FORMULA f
restAxiom :: FORMULA f -> FORMULA f
restAxiom = ([FORMULA f], FORMULA f) -> FORMULA f
forall a b. (a, b) -> b
snd (([FORMULA f], FORMULA f) -> FORMULA f)
-> (FORMULA f -> ([FORMULA f], FORMULA f))
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> ([FORMULA f], FORMULA f)
forall f. FORMULA f -> ([FORMULA f], FORMULA f)
splitAxiom

-- | get right hand side of an equivalence, without equivalence return true
resultAxiom :: FORMULA f -> FORMULA f
resultAxiom :: FORMULA f -> FORMULA f
resultAxiom f :: FORMULA f
f = case FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
restAxiom FORMULA f
f of
                  Relation _ Equivalence f' :: FORMULA f
f' _ -> FORMULA f
f'
                  _ -> FORMULA f
forall f. FORMULA f
trueForm

-- | get right hand side of an equation, without equation return dummy term
resultTerm :: FORMULA f -> TERM f
resultTerm :: FORMULA f -> TERM f
resultTerm f :: FORMULA f
f = case FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
restAxiom FORMULA f
f of
                 Negation (Definedness _ _) _ ->
                   Token -> TERM f
forall f. Token -> TERM f
varOrConst (String -> Token
mkSimpleId "undefined")
                 Equation _ _ t :: TERM f
t _ -> TERM f
t
                 _ -> Token -> TERM f
forall f. Token -> TERM f
varOrConst (String -> Token
mkSimpleId "unknown")

getSubstForm :: (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
-> FORMULA f
-> FORMULA f
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
getSubstForm sig :: Sign f e
sig f1 :: FORMULA f
f1 f2 :: FORMULA f
f2 = do
  let p1 :: [TERM f]
p1 = FORMULA f -> [TERM f]
forall f. FORMULA f -> [TERM f]
patternsOfAxiom FORMULA f
f1
      p2 :: [TERM f]
p2 = FORMULA f -> [TERM f]
forall f. FORMULA f -> [TERM f]
patternsOfAxiom FORMULA f
f2
      getVars :: FORMULA f -> Set Token
getVars = ((Token, Id) -> Token) -> Set (Token, Id) -> Set Token
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Token, Id) -> Token
forall a b. (a, b) -> a
fst (Set (Token, Id) -> Set Token)
-> (FORMULA f -> Set (Token, Id)) -> FORMULA f -> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> FORMULA f -> Set (Token, Id)
forall f e.
TermExtension f =>
Sign f e -> FORMULA f -> Set (Token, Id)
freeVars Sign f e
sig (FORMULA f -> Set (Token, Id))
-> (FORMULA f -> FORMULA f) -> FORMULA f -> Set (Token, Id)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripAllQuant
  Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
getSubst Sign f e
sig ([TERM f]
p1, FORMULA f -> Set Token
getVars FORMULA f
f1) ([TERM f]
p2, FORMULA f -> Set Token
getVars FORMULA f
f2)

mkCast :: SORT -> TERM f -> SORT -> (TERM f, [FORMULA f])
mkCast :: Id -> TERM f -> Id -> (TERM f, [FORMULA f])
mkCast s2 :: Id
s2 t :: TERM f
t s1 :: Id
s1 = if Id
s1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s2 then (TERM f
t, []) else
  case TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t of
    Qual_var v :: Token
v _ r :: Range
r -> (Token -> Id -> Range -> TERM f
forall f. Token -> Id -> Range -> TERM f
Qual_var Token
v Id
s1 Range
r, [])
    _ -> (TERM f -> Id -> Range -> TERM f
forall f. TERM f -> Id -> Range -> TERM f
Cast TERM f
t Id
s1 Range
nullRange, [TERM f -> Id -> Range -> FORMULA f
forall f. TERM f -> Id -> Range -> FORMULA f
Membership TERM f
t Id
s1 Range
nullRange])

mkSortedTerm :: SORT -> TERM f -> SORT -> TERM f
mkSortedTerm :: Id -> TERM f -> Id -> TERM f
mkSortedTerm s1 :: Id
s1 t :: TERM f
t s2 :: Id
s2 = if Id
s1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s2 then TERM f
t else
  case TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t of
    Qual_var v :: Token
v _ r :: Range
r -> Token -> Id -> Range -> TERM f
forall f. Token -> Id -> Range -> TERM f
Qual_var Token
v Id
s2 Range
r
    _ -> TERM f -> Id -> Range -> TERM f
forall f. TERM f -> Id -> Range -> TERM f
Sorted_term TERM f
t Id
s2 Range
nullRange

minSortTerm :: TermExtension f => TERM f -> TERM f
minSortTerm :: TERM f -> TERM f
minSortTerm t :: TERM f
t = case TERM f
t of
  Sorted_term st :: TERM f
st _ _ -> case TERM f -> Maybe Id
forall f. TermExtension f => f -> Maybe Id
optTermSort TERM f
st of
    Nothing -> TERM f
t
    Just _ -> TERM f -> TERM f
forall f. TermExtension f => TERM f -> TERM f
minSortTerm TERM f
st
  _ -> TERM f
t

mkSTerm :: TermExtension f => Sign f e -> SORT -> TERM f
  -> (TERM f, [FORMULA f])
mkSTerm :: Sign f e -> Id -> TERM f -> (TERM f, [FORMULA f])
mkSTerm sig :: Sign f e
sig s :: Id
s t :: TERM f
t =
  let s2 :: Id
s2 = Id -> Maybe Id -> Id
forall a. a -> Maybe a -> a
fromMaybe Id
s (Maybe Id -> Id) -> Maybe Id -> Id
forall a b. (a -> b) -> a -> b
$ TERM f -> Maybe Id
forall f. TermExtension f => f -> Maybe Id
optTermSort TERM f
t
      t0 :: TERM f
t0 = TERM f -> TERM f
forall f. TermExtension f => TERM f -> TERM f
minSortTerm TERM f
t
      s0 :: Id
s0 = Id -> Maybe Id -> Id
forall a. a -> Maybe a -> a
fromMaybe Id
s (Maybe Id -> Id) -> Maybe Id -> Id
forall a b. (a -> b) -> a -> b
$ TERM f -> Maybe Id
forall f. TermExtension f => f -> Maybe Id
optTermSort TERM f
t0
  in case Sign f e -> Id -> Id -> [Id]
forall f e. Sign f e -> Id -> Id -> [Id]
maximalSubs Sign f e
sig Id
s Id
s2 of
    l :: [Id]
l@(s1 :: Id
s1 : _) -> let
      s3 :: Id
s3 = if Id
s0 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s2 then Id
s1 else
           Id -> Maybe Id -> Id
forall a. a -> Maybe a -> a
fromMaybe Id
s1 (Maybe Id -> Id) -> Maybe Id -> Id
forall a b. (a -> b) -> a -> b
$ (Id -> Bool) -> [Id] -> Maybe Id
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Sign f e -> Id -> Id -> Bool
forall f e. Sign f e -> Id -> Id -> Bool
leqSort Sign f e
sig Id
s0) [Id]
l
      (s4 :: TERM f
s4, fs :: [FORMULA f]
fs) = Id -> TERM f -> Id -> (TERM f, [FORMULA f])
forall f. Id -> TERM f -> Id -> (TERM f, [FORMULA f])
mkCast Id
s2 TERM f
t Id
s3
      in (Id -> TERM f -> Id -> TERM f
forall f. Id -> TERM f -> Id -> TERM f
mkSortedTerm Id
s3 TERM f
s4 Id
s, [FORMULA f]
fs)
    _ -> String -> (TERM f, [FORMULA f])
forall a. HasCallStack => String -> a
error (String -> (TERM f, [FORMULA f]))
-> String -> (TERM f, [FORMULA f])
forall a b. (a -> b) -> a -> b
$ "CCC.mkSTerm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Id, Id, Id) -> String
forall a. Show a => a -> String
show (Id
s0, Id
s, Id
s2)

getSubst :: (FormExtension f, TermExtension f, Ord f) => Sign f e
  -> ([TERM f], Set.Set VAR) -> ([TERM f], Set.Set VAR)
  -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
getSubst :: Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
getSubst sig :: Sign f e
sig (p1 :: [TERM f]
p1, vs1 :: Set Token
vs1) (p2 :: [TERM f]
p2, vs2 :: Set Token
vs2) =
  let getVars :: TERM f -> Set Token
getVars = ((Token, Id) -> Token) -> Set (Token, Id) -> Set Token
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Token, Id) -> Token
forall a b. (a, b) -> a
fst (Set (Token, Id) -> Set Token)
-> (TERM f -> Set (Token, Id)) -> TERM f -> Set Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> TERM f -> Set (Token, Id)
forall f e.
TermExtension f =>
Sign f e -> TERM f -> Set (Token, Id)
freeTermVars Sign f e
sig
  in case ([TERM f]
p1, [TERM f]
p2) of
    ([], []) -> do
      let i :: Set Token
i = Set Token -> Set Token -> Set Token
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Token
vs1 Set Token
vs2
      Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set Token -> Bool
forall a. Set a -> Bool
Set.null Set Token
i)
        (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Set Token -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "possibly conflicting variables" Set Token
i]
      ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Subst f
forall k a. Map k a
Map.empty, []), (Subst f
forall k a. Map k a
Map.empty, []))
    (hd1 :: TERM f
hd1 : tl1 :: [TERM f]
tl1, hd2 :: TERM f
hd2 : tl2 :: [TERM f]
tl2) ->
      let r :: Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
r = Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
getSubst Sign f e
sig ([TERM f]
tl1, Set Token
vs1) ([TERM f]
tl2, Set Token
vs2)
          mkS1 :: Token
-> Id -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
mkS1 v1 :: Token
v1 s1 :: Id
s1 = do
              let (hd3 :: TERM f
hd3, fs :: [FORMULA f]
fs) = Sign f e -> Id -> TERM f -> (TERM f, [FORMULA f])
forall f e.
TermExtension f =>
Sign f e -> Id -> TERM f -> (TERM f, [FORMULA f])
mkSTerm Sign f e
sig Id
s1 TERM f
hd2
              ((m1 :: Subst f
m1, fs1 :: [FORMULA f]
fs1), m2 :: (Subst f, [FORMULA f])
m2) <- Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
getSubst Sign f e
sig
                ([TERM f]
tl1, Token -> Set Token -> Set Token
forall a. Ord a => a -> Set a -> Set a
Set.delete Token
v1 Set Token
vs1) ([TERM f]
tl2, Set Token
vs2)
              ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Token -> TERM f -> Subst f -> Subst f
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
v1 TERM f
hd3 Subst f
m1, [FORMULA f]
fs [FORMULA f] -> [FORMULA f] -> [FORMULA f]
forall a. [a] -> [a] -> [a]
++ [FORMULA f]
fs1), (Subst f, [FORMULA f])
m2)
          mkS2 :: Token
-> Id -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
mkS2 v2 :: Token
v2 s2 :: Id
s2 = do
              let (hd3 :: TERM f
hd3, fs :: [FORMULA f]
fs) = Sign f e -> Id -> TERM f -> (TERM f, [FORMULA f])
forall f e.
TermExtension f =>
Sign f e -> Id -> TERM f -> (TERM f, [FORMULA f])
mkSTerm Sign f e
sig Id
s2 TERM f
hd1
              (m1 :: (Subst f, [FORMULA f])
m1, (m2 :: Subst f
m2, fs2 :: [FORMULA f]
fs2)) <- Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
getSubst Sign f e
sig ([TERM f]
tl1, Set Token
vs1)
                ([TERM f]
tl2, Token -> Set Token -> Set Token
forall a. Ord a => a -> Set a -> Set a
Set.delete Token
v2 Set Token
vs2)
              ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((Subst f, [FORMULA f])
m1, (Token -> TERM f -> Subst f -> Subst f
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
v2 TERM f
hd3 Subst f
m2, [FORMULA f]
fs [FORMULA f] -> [FORMULA f] -> [FORMULA f]
forall a. [a] -> [a] -> [a]
++ [FORMULA f]
fs2))
          cond :: Token -> Set Token -> TERM f -> Bool
cond v :: Token
v vs :: Set Token
vs hd :: TERM f
hd = Token -> Set Token -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Token
v Set Token
vs Bool -> Bool -> Bool
&& Token -> Set Token -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Token
v (TERM f -> Set Token
getVars TERM f
hd)
          diag :: a -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
diag v :: a
v = [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> a -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
                            "unsupported occurrence of variable" a
v] Result ()
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
r
      in case (TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
hd1, TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
hd2) of
        (Qual_var v1 :: Token
v1 s1 :: Id
s1 _, Qual_var v2 :: Token
v2 s2 :: Id
s2 _)
          | Token
v1 Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
v2 Bool -> Bool -> Bool
&& Id
s1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s2 -> Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
getSubst Sign f e
sig ([TERM f]
tl1, Token -> Set Token -> Set Token
forall a. Ord a => a -> Set a -> Set a
Set.delete Token
v1 Set Token
vs1)
               ([TERM f]
tl2, Token -> Set Token -> Set Token
forall a. Ord a => a -> Set a -> Set a
Set.delete Token
v2 Set Token
vs2)
          | Token -> Set Token -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Token
v1 Set Token
vs2 ->
            if Token -> Set Token -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Token
v2 Set Token
vs1
            then [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Token -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
                            ("unsupported mix of variables '"
                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
v1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' and") Token
v2] Result ()
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
r
            else Token
-> Id -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
mkS1 Token
v1 Id
s1
          | Bool
otherwise -> Token
-> Id -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
mkS2 Token
v2 Id
s2
        (Qual_var v1 :: Token
v1 s1 :: Id
s1 _, _) ->
            if Token -> Set Token -> TERM f -> Bool
cond Token
v1 Set Token
vs2 TERM f
hd2 then Token -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall a.
(GetRange a, Pretty a) =>
a -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
diag Token
v1
            else Token
-> Id -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
mkS1 Token
v1 Id
s1
        (_, Qual_var v2 :: Token
v2 s2 :: Id
s2 _) ->
            if Token -> Set Token -> TERM f -> Bool
cond Token
v2 Set Token
vs1 TERM f
hd1 then Token -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall a.
(GetRange a, Pretty a) =>
a -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
diag Token
v2
            else Token
-> Id -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
mkS2 Token
v2 Id
s2
        (_, _) | 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
hd1 TERM f
hd2 ->
             Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e
-> ([TERM f], Set Token)
-> ([TERM f], Set Token)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
getSubst Sign f e
sig (TERM f -> [TERM f]
forall f. TERM f -> [TERM f]
arguOfTerm TERM f
hd1 [TERM f] -> [TERM f] -> [TERM f]
forall a. [a] -> [a] -> [a]
++ [TERM f]
tl1, Set Token
vs1)
                          (TERM f -> [TERM f]
forall f. TERM f -> [TERM f]
arguOfTerm TERM f
hd2 [TERM f] -> [TERM f] -> [TERM f]
forall a. [a] -> [a] -> [a]
++ [TERM f]
tl2, Set Token
vs2)
        _ -> String
-> TERM f
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "no overlap at" TERM f
hd1
    _ -> String -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall a. HasCallStack => String -> a
error "non-matching leading terms"

-- | extract defined subsorts
isSubsortDef :: FORMULA f -> Maybe (SORT, VAR_DECL, FORMULA f)
isSubsortDef :: FORMULA f -> Maybe (Id, VAR_DECL, FORMULA f)
isSubsortDef f :: FORMULA f
f = case FORMULA f
f of
  Quantification Universal [vd :: VAR_DECL
vd@(Var_decl [v :: Token
v] super :: Id
super _)]
    (Relation (Membership (Qual_var v2 :: Token
v2 super2 :: Id
super2 _) sub :: Id
sub _) Equivalence f1 :: FORMULA f
f1 _) _
     | (Token
v, Id
super) (Token, Id) -> (Token, Id) -> Bool
forall a. Eq a => a -> a -> Bool
== (Token
v2, Id
super2) -> (Id, VAR_DECL, FORMULA f) -> Maybe (Id, VAR_DECL, FORMULA f)
forall a. a -> Maybe a
Just (Id
sub, VAR_DECL
vd, FORMULA f
f1)
  _ -> Maybe (Id, VAR_DECL, FORMULA f)
forall a. Maybe a
Nothing

-- | create the obligations for subsorts
infoSubsorts :: Set.Set SORT -> [(SORT, VAR_DECL, FORMULA f)] -> [FORMULA f]
infoSubsorts :: Set Id -> [(Id, VAR_DECL, FORMULA f)] -> [FORMULA f]
infoSubsorts emptySorts :: Set Id
emptySorts = ((Id, VAR_DECL, FORMULA f) -> FORMULA f)
-> [(Id, VAR_DECL, FORMULA f)] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, v :: VAR_DECL
v, f :: FORMULA f
f) -> [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL
v] FORMULA f
f)
  ([(Id, VAR_DECL, FORMULA f)] -> [FORMULA f])
-> ([(Id, VAR_DECL, FORMULA f)] -> [(Id, VAR_DECL, FORMULA f)])
-> [(Id, VAR_DECL, FORMULA f)]
-> [FORMULA f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Id, VAR_DECL, FORMULA f) -> Bool)
-> [(Id, VAR_DECL, FORMULA f)] -> [(Id, VAR_DECL, FORMULA f)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (s :: Id
s, _, _) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
s Set Id
emptySorts)

-- | extract the leading symbol from a formula
leadingSym :: GetRange f => FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
leadingSym :: FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
leadingSym = (Either (TERM f) (FORMULA f) -> Either OP_SYMB PRED_SYMB)
-> Maybe (Either (TERM f) (FORMULA f))
-> Maybe (Either OP_SYMB PRED_SYMB)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either (TERM f) (FORMULA f) -> Either OP_SYMB PRED_SYMB
forall f. Either (TERM f) (FORMULA f) -> Either OP_SYMB PRED_SYMB
extractLeadingSymb (Maybe (Either (TERM f) (FORMULA f))
 -> Maybe (Either OP_SYMB PRED_SYMB))
-> (FORMULA f -> Maybe (Either (TERM f) (FORMULA f)))
-> FORMULA f
-> Maybe (Either OP_SYMB PRED_SYMB)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
forall f.
GetRange f =>
FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
leadingTermPredication

-- | extract the leading symbol with the range from a formula
leadingSymPos :: GetRange f => FORMULA f
  -> (Maybe (Either (TERM f) (FORMULA f)), Range)
leadingSymPos :: FORMULA f -> (Maybe (Either (TERM f) (FORMULA f)), Range)
leadingSymPos f :: FORMULA f
f = (FORMULA f, Bool, Bool, Bool)
-> (Maybe (Either (TERM f) (FORMULA f)), Range)
forall f.
GetRange f =>
(FORMULA f, Bool, Bool, Bool)
-> (Maybe (Either (TERM f) (FORMULA f)), Range)
leading (FORMULA f
f, Bool
False, Bool
False, Bool
False) where
  -- three booleans to indicate inside implication, equivalence or negation
  leadTerm :: TERM f -> Range -> (Maybe (Either (TERM f) b), Range)
leadTerm t :: TERM f
t q :: Range
q = case TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t of
    a :: TERM f
a@(Application _ _ p :: Range
p) -> (Either (TERM f) b -> Maybe (Either (TERM f) b)
forall a. a -> Maybe a
Just (TERM f -> Either (TERM f) b
forall a b. a -> Either a b
Left TERM f
a), Range
p)
    _ -> (Maybe (Either (TERM f) b)
forall a. Maybe a
Nothing, Range
q)
  leading :: (FORMULA f, Bool, Bool, Bool)
-> (Maybe (Either (TERM f) (FORMULA f)), Range)
leading (f1 :: FORMULA f
f1, b1 :: Bool
b1, b2 :: Bool
b2, b3 :: Bool
b3) = case (FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripAllQuant FORMULA f
f1, Bool
b1, Bool
b2, Bool
b3) of
    (Negation f' :: FORMULA f
f' _, _, _, False) ->
        (FORMULA f, Bool, Bool, Bool)
-> (Maybe (Either (TERM f) (FORMULA f)), Range)
leading (FORMULA f
f', Bool
b1, Bool
b2, Bool
True)
    (Relation _ c :: Relation
c f' :: FORMULA f
f' _, _, False, False)
        | Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
/= Relation
Equivalence ->
        (FORMULA f, Bool, Bool, Bool)
-> (Maybe (Either (TERM f) (FORMULA f)), Range)
leading (FORMULA f
f', Bool
True, Bool
False, Bool
False)
    (Relation f' :: FORMULA f
f' Equivalence _ _, _, False, False) ->
        (FORMULA f, Bool, Bool, Bool)
-> (Maybe (Either (TERM f) (FORMULA f)), Range)
leading (FORMULA f
f', Bool
b1, Bool
True, Bool
False)
    (Definedness t :: TERM f
t q :: Range
q, _, _, _) -> TERM f -> Range -> (Maybe (Either (TERM f) (FORMULA f)), Range)
forall f b. TERM f -> Range -> (Maybe (Either (TERM f) b), Range)
leadTerm TERM f
t Range
q
    (pr :: FORMULA f
pr@(Predication _ _ p :: Range
p), _, _, _) ->
        (Either (TERM f) (FORMULA f) -> Maybe (Either (TERM f) (FORMULA f))
forall a. a -> Maybe a
Just (FORMULA f -> Either (TERM f) (FORMULA f)
forall a b. b -> Either a b
Right FORMULA f
pr), Range
p)
    (Equation t :: TERM f
t _ _ q :: Range
q, _, False, False) -> TERM f -> Range -> (Maybe (Either (TERM f) (FORMULA f)), Range)
forall f b. TERM f -> Range -> (Maybe (Either (TERM f) b), Range)
leadTerm TERM f
t Range
q
    _ -> (Maybe (Either (TERM f) (FORMULA f))
forall a. Maybe a
Nothing, FORMULA f -> Range
forall a. GetRange a => a -> Range
getRange FORMULA f
f1)

-- | extract the leading term or predication from a formula
leadingTermPredication :: GetRange f => FORMULA f
  -> Maybe (Either (TERM f) (FORMULA f))
leadingTermPredication :: FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
leadingTermPredication = (Maybe (Either (TERM f) (FORMULA f)), Range)
-> Maybe (Either (TERM f) (FORMULA f))
forall a b. (a, b) -> a
fst ((Maybe (Either (TERM f) (FORMULA f)), Range)
 -> Maybe (Either (TERM f) (FORMULA f)))
-> (FORMULA f -> (Maybe (Either (TERM f) (FORMULA f)), Range))
-> FORMULA f
-> Maybe (Either (TERM f) (FORMULA f))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> (Maybe (Either (TERM f) (FORMULA f)), Range)
forall f.
GetRange f =>
FORMULA f -> (Maybe (Either (TERM f) (FORMULA f)), Range)
leadingSymPos

-- | extract the leading symbol from a term or a formula
extractLeadingSymb :: Either (TERM f) (FORMULA f) -> Either OP_SYMB PRED_SYMB
extractLeadingSymb :: Either (TERM f) (FORMULA f) -> Either OP_SYMB PRED_SYMB
extractLeadingSymb lead :: Either (TERM f) (FORMULA f)
lead = case Either (TERM f) (FORMULA f)
lead of
  Left (Application os :: OP_SYMB
os _ _) -> OP_SYMB -> Either OP_SYMB PRED_SYMB
forall a b. a -> Either a b
Left OP_SYMB
os
  Right (Predication p :: PRED_SYMB
p _ _) -> PRED_SYMB -> Either OP_SYMB PRED_SYMB
forall a b. b -> Either a b
Right PRED_SYMB
p
  _ -> String -> Either OP_SYMB PRED_SYMB
forall a. HasCallStack => String -> a
error "CASL.CCC.TermFormula<extractLeadingSymb>"

-- | replaces variables by terms in a term or formula
substRec :: Eq f => [(TERM f, TERM f)] -> Record f (FORMULA f) (TERM f)
substRec :: [(TERM f, TERM f)] -> Record f (FORMULA f) (TERM f)
substRec subs :: [(TERM f, TERM f)]
subs = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
forall a. a -> a
id)
   { foldQual_var :: TERM f -> Token -> Id -> Range -> TERM f
foldQual_var = \ t :: TERM f
t _ _ _ -> [(TERM f, TERM f)] -> TERM f -> TERM f
forall t. Eq t => [(t, t)] -> t -> t
subst [(TERM f, TERM f)]
subs TERM f
t } where
  subst :: [(t, t)] -> t -> t
subst l :: [(t, t)]
l tt :: t
tt = case [(t, t)]
l of
    [] -> t
tt
    (n :: t
n, v :: t
v) : r :: [(t, t)]
r -> if t
tt t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
v then t
n else [(t, t)] -> t -> t
subst [(t, t)]
r t
tt

substitute :: Eq f => [(TERM f, TERM f)] -> TERM f -> TERM f
substitute :: [(TERM f, TERM f)] -> TERM f -> TERM f
substitute = Record f (FORMULA f) (TERM f) -> TERM f -> TERM f
forall f a b. Record f a b -> TERM f -> b
foldTerm (Record f (FORMULA f) (TERM f) -> TERM f -> TERM f)
-> ([(TERM f, TERM f)] -> Record f (FORMULA f) (TERM f))
-> [(TERM f, TERM f)]
-> TERM f
-> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TERM f, TERM f)] -> Record f (FORMULA f) (TERM f)
forall f.
Eq f =>
[(TERM f, TERM f)] -> Record f (FORMULA f) (TERM f)
substRec

substiF :: Eq f => [(TERM f, TERM f)] -> FORMULA f -> FORMULA f
substiF :: [(TERM f, TERM f)] -> FORMULA f -> FORMULA f
substiF = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> ([(TERM f, TERM f)] -> Record f (FORMULA f) (TERM f))
-> [(TERM f, TERM f)]
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TERM f, TERM f)] -> Record f (FORMULA f) (TERM f)
forall f.
Eq f =>
[(TERM f, TERM f)] -> Record f (FORMULA f) (TERM f)
substRec

sameOpTypes :: Sign f e -> OP_TYPE -> OP_TYPE -> Bool
sameOpTypes :: Sign f e -> OP_TYPE -> OP_TYPE -> Bool
sameOpTypes sig :: Sign f e
sig = (OpType -> OpType -> Bool)
-> (OP_TYPE -> OpType) -> OP_TYPE -> OP_TYPE -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on (Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF Sign f e
sig) OP_TYPE -> OpType
toOpType

sameOpSymbs :: Sign f e -> OP_SYMB -> OP_SYMB -> Bool
sameOpSymbs :: Sign f e -> OP_SYMB -> OP_SYMB -> Bool
sameOpSymbs sig :: Sign f e
sig o1 :: OP_SYMB
o1 o2 :: OP_SYMB
o2 = (Id -> Id -> Bool) -> (OP_SYMB -> Id) -> OP_SYMB -> OP_SYMB -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
(==) OP_SYMB -> Id
opSymbName OP_SYMB
o1 OP_SYMB
o2 Bool -> Bool -> Bool
&& case (OP_SYMB
o1, OP_SYMB
o2) of
  (Qual_op_name _ t1 :: OP_TYPE
t1 _, Qual_op_name _ t2 :: OP_TYPE
t2 _) -> Sign f e -> OP_TYPE -> OP_TYPE -> Bool
forall f e. Sign f e -> OP_TYPE -> OP_TYPE -> Bool
sameOpTypes Sign f e
sig OP_TYPE
t1 OP_TYPE
t2
  _ -> Bool
False

-- | check whether two terms are the terms of same application symbol
sameOpsApp :: Sign f e -> TERM f -> TERM f -> Bool
sameOpsApp :: Sign f e -> TERM f -> TERM f -> Bool
sameOpsApp sig :: Sign f e
sig app1 :: TERM f
app1 app2 :: TERM f
app2 = case (TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
app1, TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
app2) of
  (Application o1 :: OP_SYMB
o1 _ _, Application o2 :: OP_SYMB
o2 _ _) -> Sign f e -> OP_SYMB -> OP_SYMB -> Bool
forall f e. Sign f e -> OP_SYMB -> OP_SYMB -> Bool
sameOpSymbs Sign f e
sig OP_SYMB
o1 OP_SYMB
o2
  _ -> Bool
False

eqPattern :: Sign f e -> TERM f -> TERM f -> Bool
eqPattern :: Sign f e -> TERM f -> TERM f -> Bool
eqPattern sig :: Sign f e
sig t1 :: TERM f
t1 t2 :: TERM f
t2 = case (TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t1, TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t2) of
  (Qual_var v1 :: Token
v1 _ _, Qual_var v2 :: Token
v2 _ _) -> Token
v1 Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
v2
  _ | 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
t1 TERM f
t2 ->
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ ([TERM f] -> [TERM f] -> [Bool])
-> (TERM f -> [TERM f]) -> TERM f -> TERM f -> [Bool]
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on ((TERM f -> TERM f -> Bool) -> [TERM f] -> [TERM f] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith ((TERM f -> TERM f -> Bool) -> [TERM f] -> [TERM f] -> [Bool])
-> (TERM f -> TERM f -> Bool) -> [TERM f] -> [TERM f] -> [Bool]
forall a b. (a -> b) -> a -> b
$ Sign f e -> TERM f -> TERM f -> Bool
forall f e. Sign f e -> TERM f -> TERM f -> Bool
eqPattern Sign f e
sig) TERM f -> [TERM f]
forall f. TERM f -> [TERM f]
arguOfTerm TERM f
t1 TERM f
t2
  _ -> Bool
False