{- |
Module      :  ./CASL/CCC/FreeTypes.hs
Description :  consistency checking of free types
Copyright   :  (c) Mingyi Liu and Till Mossakowski and Uni Bremen 2004-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

Consistency checking of free types
-}

module CASL.CCC.FreeTypes (checkFreeType) where

import CASL.AlphaConvert
import CASL.AS_Basic_CASL
import CASL.MapSentence
import CASL.Morphism
import CASL.Sign
import CASL.Simplify
import CASL.SimplifySen
import CASL.CCC.TermFormula
import CASL.CCC.TerminationProof (terminationProof)
import CASL.Overload (leqP)
import CASL.Quantification
import CASL.ToDoc
import CASL.Utils

import Common.AS_Annotation
import Common.Consistency (Conservativity (..))
import Common.DocUtils
import Common.Id
import Common.Result
import Common.Utils (number)
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import Control.Monad
import qualified Control.Monad.Fail as Fail

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

import qualified Data.Set as Set

-- | check values of constructors (free types have only total ones)
inhabited :: Set.Set SORT -> [OP_SYMB] -> Set.Set SORT
inhabited :: Set SORT -> [OP_SYMB] -> Set SORT
inhabited sorts :: Set SORT
sorts cons :: [OP_SYMB]
cons = Set SORT -> Set SORT
iterateInhabited Set SORT
sorts where
  argsRes :: [([SORT], SORT)]
argsRes = (OP_SYMB -> [([SORT], SORT)] -> [([SORT], SORT)])
-> [([SORT], SORT)] -> [OP_SYMB] -> [([SORT], SORT)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ os :: OP_SYMB
os -> case OP_SYMB
os of
    Qual_op_name _ (Op_type Total args :: [SORT]
args res :: SORT
res _) _ -> (([SORT]
args, SORT
res) ([SORT], SORT) -> [([SORT], SORT)] -> [([SORT], SORT)]
forall a. a -> [a] -> [a]
:)
    _ -> [([SORT], SORT)] -> [([SORT], SORT)]
forall a. a -> a
id) [] [OP_SYMB]
cons
  iterateInhabited :: Set SORT -> Set SORT
iterateInhabited l :: Set SORT
l =
    if Bool
changed then Set SORT -> Set SORT
iterateInhabited Set SORT
newL else Set SORT
newL where
      (newL :: Set SORT
newL, changed :: Bool
changed) = (([SORT], SORT) -> (Set SORT, Bool) -> (Set SORT, Bool))
-> (Set SORT, Bool) -> [([SORT], SORT)] -> (Set SORT, Bool)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (ags :: [SORT]
ags, rs :: SORT
rs) p :: (Set SORT, Bool)
p@(l' :: Set SORT
l', _) ->
        if (SORT -> Bool) -> [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set SORT
l') [SORT]
ags Bool -> Bool -> Bool
&& Bool -> Bool
not (SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
rs Set SORT
l')
        then (SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
rs Set SORT
l', Bool
True) else (Set SORT, Bool)
p) (Set SORT
l, Bool
False) [([SORT], SORT)]
argsRes

-- | just filter out the axioms generated for free types
isGenAx :: Named (FORMULA f) -> Bool
isGenAx :: Named (FORMULA f) -> Bool
isGenAx ax :: Named (FORMULA f)
ax = case [Char] -> [Char] -> Maybe [Char]
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "ga_" ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ Named (FORMULA f) -> [Char]
forall s a. SenAttr s a -> a
senAttr Named (FORMULA f)
ax of
  Nothing -> Bool
True
  Just rname :: [Char]
rname -> ([Char] -> Bool) -> [[Char]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> ([Char] -> Bool) -> [Char] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
rname))
    ["disjoint_", "injective_", "selector_"]

getFs :: [Named (FORMULA f)] -> [FORMULA f]
getFs :: [Named (FORMULA f)] -> [FORMULA f]
getFs = (Named (FORMULA f) -> FORMULA f)
-> [Named (FORMULA f)] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence ([Named (FORMULA f)] -> [FORMULA f])
-> ([Named (FORMULA f)] -> [Named (FORMULA f)])
-> [Named (FORMULA f)]
-> [FORMULA f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named (FORMULA f) -> Bool)
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. (a -> Bool) -> [a] -> [a]
filter Named (FORMULA f) -> Bool
forall f. Named (FORMULA f) -> Bool
isGenAx

-- | get the constraints from sort generation axioms
constraintOfAxiom :: [FORMULA f] -> [[Constraint]]
constraintOfAxiom :: [FORMULA f] -> [[Constraint]]
constraintOfAxiom = (FORMULA f -> [[Constraint]] -> [[Constraint]])
-> [[Constraint]] -> [FORMULA f] -> [[Constraint]]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ f :: FORMULA f
f -> case FORMULA f
f of
  Sort_gen_ax constrs :: [Constraint]
constrs _ -> ([Constraint]
constrs [Constraint] -> [[Constraint]] -> [[Constraint]]
forall a. a -> [a] -> [a]
:)
  _ -> [[Constraint]] -> [[Constraint]]
forall a. a -> a
id) []

recoverSortsAndConstructors :: [FORMULA f] -> (Set.Set SORT, Set.Set OP_SYMB)
recoverSortsAndConstructors :: [FORMULA f] -> (Set SORT, Set OP_SYMB)
recoverSortsAndConstructors fs :: [FORMULA f]
fs = let
  (srts :: [[SORT]]
srts, cons :: [[OP_SYMB]]
cons, _) = [([SORT], [OP_SYMB], [(SORT, SORT)])]
-> ([[SORT]], [[OP_SYMB]], [[(SORT, SORT)]])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([([SORT], [OP_SYMB], [(SORT, SORT)])]
 -> ([[SORT]], [[OP_SYMB]], [[(SORT, SORT)]]))
-> ([[Constraint]] -> [([SORT], [OP_SYMB], [(SORT, SORT)])])
-> [[Constraint]]
-> ([[SORT]], [[OP_SYMB]], [[(SORT, SORT)]])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)]))
-> [[Constraint]] -> [([SORT], [OP_SYMB], [(SORT, SORT)])]
forall a b. (a -> b) -> [a] -> [b]
map [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)])
recover_Sort_gen_ax
    ([[Constraint]] -> ([[SORT]], [[OP_SYMB]], [[(SORT, SORT)]]))
-> [[Constraint]] -> ([[SORT]], [[OP_SYMB]], [[(SORT, SORT)]])
forall a b. (a -> b) -> a -> b
$ [FORMULA f] -> [[Constraint]]
forall f. [FORMULA f] -> [[Constraint]]
constraintOfAxiom [FORMULA f]
fs
  in ([Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ ([SORT] -> Set SORT) -> [[SORT]] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map [SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList [[SORT]]
srts, [Set OP_SYMB] -> Set OP_SYMB
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set OP_SYMB] -> Set OP_SYMB) -> [Set OP_SYMB] -> Set OP_SYMB
forall a b. (a -> b) -> a -> b
$ ([OP_SYMB] -> Set OP_SYMB) -> [[OP_SYMB]] -> [Set OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map [OP_SYMB] -> Set OP_SYMB
forall a. Ord a => [a] -> Set a
Set.fromList [[OP_SYMB]]
cons)

-- check that patterns do not overlap, if not, return proof obligation.
getOverlapQuery :: (FormExtension f, TermExtension f, Ord f) => Sign f e
  -> [[FORMULA f]] -> [FORMULA f]
getOverlapQuery :: Sign f e -> [[FORMULA f]] -> [FORMULA f]
getOverlapQuery sig :: Sign f e
sig = (FORMULA f -> Bool) -> [FORMULA f] -> [FORMULA f]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (FORMULA f -> Bool) -> FORMULA f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> Bool
forall f. FORMULA f -> Bool
is_True_atom)
  ([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) -> Maybe (FORMULA f))
-> [(FORMULA f, FORMULA f)] -> [FORMULA f]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Sign f e -> (FORMULA f, FORMULA f) -> Maybe (FORMULA f)
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e -> (FORMULA f, FORMULA f) -> Maybe (FORMULA f)
retrySubstForm Sign f e
sig) ([(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)])
-> [[FORMULA f]] -> [(FORMULA f, FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [FORMULA f] -> [(FORMULA f, FORMULA f)]
forall a. [a] -> [(a, a)]
pairs

convert2Forms :: (TermExtension f, FormExtension f, Ord f) => Sign f e
  -> FORMULA f -> FORMULA f
  -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
  -> (FORMULA f, FORMULA f, ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])))
convert2Forms :: Sign f e
-> FORMULA f
-> FORMULA f
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> (FORMULA f, FORMULA f,
    ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])))
convert2Forms sig :: Sign f e
sig f1 :: FORMULA f
f1 f2 :: FORMULA f
f2 (Result ds :: [Diagnosis]
ds m :: Maybe ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
m) =
  if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then let Just r :: ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
r = Maybe ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
m in (FORMULA f
f1, FORMULA f
f2, ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
r) else let
  (f3 :: FORMULA f
f3, c :: Int
c) = Int -> (f -> f) -> FORMULA f -> (FORMULA f, Int)
forall f. Int -> (f -> f) -> FORMULA f -> (FORMULA f, Int)
alphaConvert 1 f -> f
forall a. a -> a
id FORMULA f
f1
  f4 :: FORMULA f
f4 = Int -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Int -> (f -> f) -> FORMULA f -> FORMULA f
convertFormula Int
c f -> f
forall a. a -> a
id FORMULA f
f2
  Result _ (Just p :: ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
p) = 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 FORMULA f
f3 FORMULA f
f4
  in (FORMULA f
f3, FORMULA f
f4, ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
p)

retrySubstForm :: (FormExtension f, TermExtension f, Ord f) => Sign f e
  -> (FORMULA f, FORMULA f) -> Maybe (FORMULA f)
retrySubstForm :: Sign f e -> (FORMULA f, FORMULA f) -> Maybe (FORMULA f)
retrySubstForm sig :: Sign f e
sig (f1 :: FORMULA f
f1, f2 :: FORMULA f
f2) =
  let r :: Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
r@(Result ds :: [Diagnosis]
ds m :: Maybe ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
m) = 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 FORMULA f
f1 FORMULA f
f2
  in case Maybe ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
m of
       Nothing -> Maybe (FORMULA f)
forall a. Maybe a
Nothing
       Just s :: ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
s -> if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then FORMULA f -> Maybe (FORMULA f)
forall a. a -> Maybe a
Just (FORMULA f -> Maybe (FORMULA f)) -> FORMULA f -> Maybe (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Sign f e
-> ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> FORMULA f
-> FORMULA f
-> FORMULA f
forall f e.
(TermExtension f, GetRange f, Ord f) =>
Sign f e
-> ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> FORMULA f
-> FORMULA f
-> FORMULA f
mkOverlapEq Sign f e
sig ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
s FORMULA f
f1 FORMULA f
f2
         else let (f3 :: FORMULA f
f3, f4 :: FORMULA f
f4, s2 :: ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
s2) = Sign f e
-> FORMULA f
-> FORMULA f
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> (FORMULA f, FORMULA f,
    ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])))
forall f e.
(TermExtension f, FormExtension f, Ord f) =>
Sign f e
-> FORMULA f
-> FORMULA f
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> (FORMULA f, FORMULA f,
    ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])))
convert2Forms Sign f e
sig FORMULA f
f1 FORMULA f
f2 Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
r
              in FORMULA f -> Maybe (FORMULA f)
forall a. a -> Maybe a
Just (FORMULA f -> Maybe (FORMULA f))
-> (FORMULA f -> FORMULA f) -> FORMULA f -> Maybe (FORMULA f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> FORMULA f -> FORMULA f
forall f e. TermExtension f => Sign f e -> FORMULA f -> FORMULA f
stripQuant Sign f e
sig (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Int -> (f -> f) -> FORMULA f -> FORMULA f
convertFormula 1 f -> f
forall a. a -> a
id
                     (FORMULA f -> Maybe (FORMULA f)) -> FORMULA f -> Maybe (FORMULA f)
forall a b. (a -> b) -> a -> b
$ Sign f e
-> ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> FORMULA f
-> FORMULA f
-> FORMULA f
forall f e.
(TermExtension f, GetRange f, Ord f) =>
Sign f e
-> ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> FORMULA f
-> FORMULA f
-> FORMULA f
mkOverlapEq Sign f e
sig ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
s2 FORMULA f
f3 FORMULA f
f4

quant :: TermExtension f => Sign f e -> FORMULA f -> FORMULA f
quant :: Sign f e -> FORMULA f -> FORMULA f
quant sig :: Sign f e
sig f :: FORMULA f
f = 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

mkOverlapEq :: (TermExtension f, GetRange f, Ord f) => Sign f e
  -> ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
  -> FORMULA f -> FORMULA f -> FORMULA f
mkOverlapEq :: Sign f e
-> ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> FORMULA f
-> FORMULA f
-> FORMULA f
mkOverlapEq sig :: Sign f e
sig ((s1 :: Subst f
s1, fs1 :: [FORMULA f]
fs1), (s2 :: Subst f
s2, fs2 :: [FORMULA f]
fs2)) f1 :: FORMULA f
f1 f2 :: FORMULA f
f2 = Sign f e -> FORMULA f -> FORMULA f
forall f e. TermExtension f => Sign f e -> FORMULA f -> FORMULA f
quant Sign f e
sig (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> FORMULA f -> FORMULA f
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula f -> f
forall a. a -> a
id
     (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
mkImpl ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct ([FORMULA f] -> FORMULA f) -> [FORMULA f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ (FORMULA f -> FORMULA f) -> [FORMULA f] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (Subst f -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Subst f -> (f -> f) -> FORMULA f -> FORMULA f
replaceVarsF Subst f
s1 f -> f
forall a. a -> a
id) [FORMULA f]
fs2
               [FORMULA f] -> [FORMULA f] -> [FORMULA f]
forall a. [a] -> [a] -> [a]
++ (FORMULA f -> FORMULA f) -> [FORMULA f] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (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]
fs1)
     (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. GetRange f => FORMULA f -> FORMULA f -> FORMULA f
overlapQuery (Subst f -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Subst f -> (f -> f) -> FORMULA f -> FORMULA f
replaceVarsF Subst f
s1 f -> f
forall a. a -> a
id (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripAllQuant FORMULA f
f1)
     (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripAllQuant FORMULA f
f2

{-
  check if leading symbols are new (not in the image of morphism),
        if not, return it as proof obligation
-}
getDefsForOld :: GetRange f => Sign f e -> [FORMULA f]
  -> [FORMULA f]
getDefsForOld :: Sign f e -> [FORMULA f] -> [FORMULA f]
getDefsForOld sig :: Sign f e
sig axioms :: [FORMULA f]
axioms = let
        oldOpMap :: OpMap
oldOpMap = Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
sig
        oldPredMap :: PredMap
oldPredMap = Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
sig
    in (FORMULA f -> Bool) -> [FORMULA f] -> [FORMULA f]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ f :: FORMULA f
f -> case FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
forall f.
GetRange f =>
FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
leadingSym FORMULA f
f of
         Just (Left (Qual_op_name ident :: SORT
ident ot :: OP_TYPE
ot _))
           | SORT -> OpType -> OpMap -> Bool
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> Bool
MapSet.member SORT
ident (OP_TYPE -> OpType
toOpType OP_TYPE
ot) OpMap
oldOpMap -> Bool
True
         Just (Right (Qual_pred_name ident :: SORT
ident pt :: PRED_TYPE
pt _))
           | SORT -> PredType -> PredMap -> Bool
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> Bool
MapSet.member SORT
ident (PRED_TYPE -> PredType
toPredType PRED_TYPE
pt) PredMap
oldPredMap -> Bool
True
         _ -> Bool
False) [FORMULA f]
axioms

isFreeSortGen :: FORMULA f -> Bool
isFreeSortGen :: FORMULA f -> Bool
isFreeSortGen f :: FORMULA f
f = case FORMULA f
f of
  Sort_gen_ax _ True -> Bool
True
  _ -> Bool
False

-- | non-inhabited non-empty sorts
getNefsorts :: Set.Set SORT -> Set.Set SORT -> Set.Set SORT
  -> (Set.Set SORT, [OP_SYMB]) -> Set.Set SORT
getNefsorts :: Set SORT
-> Set SORT -> Set SORT -> (Set SORT, [OP_SYMB]) -> Set SORT
getNefsorts oldSorts :: Set SORT
oldSorts nSorts :: Set SORT
nSorts esorts :: Set SORT
esorts (srts :: Set SORT
srts, cons :: [OP_SYMB]
cons) =
  Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
fsorts (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Set SORT -> [OP_SYMB] -> Set SORT
inhabited Set SORT
oldSorts [OP_SYMB]
cons where
    fsorts :: Set SORT
fsorts = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set SORT
nSorts Set SORT
srts) Set SORT
esorts

getDataStatus :: Set.Set SORT -> Set.Set SORT -> Set.Set SORT -> Conservativity
getDataStatus :: Set SORT -> Set SORT -> Set SORT -> Conservativity
getDataStatus nSorts :: Set SORT
nSorts defSubs :: Set SORT
defSubs genSorts :: Set SORT
genSorts
  | Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
nSorts = Conservativity
Def
  | Set SORT -> Bool
forall a. Set a -> Bool
Set.null (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
nSorts (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set SORT
genSorts Set SORT
defSubs = Conservativity
Mono
  | Bool
otherwise = Conservativity
Cons

getConStatus :: Conservativity -> [FORMULA f] -> Conservativity
getConStatus :: Conservativity -> [FORMULA f] -> Conservativity
getConStatus dataStatus :: Conservativity
dataStatus fs :: [FORMULA f]
fs = Conservativity -> Conservativity -> Conservativity
forall a. Ord a => a -> a -> a
min Conservativity
dataStatus (Conservativity -> Conservativity)
-> Conservativity -> Conservativity
forall a b. (a -> b) -> a -> b
$ if [FORMULA f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FORMULA f]
fs then Conservativity
Def else Conservativity
Cons

-- | check whether it is the domain of a partial function
isDomain :: FORMULA f -> Bool
isDomain :: FORMULA f -> Bool
isDomain = Maybe (TERM f, FORMULA f) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (TERM f, FORMULA f) -> Bool)
-> (FORMULA f -> Maybe (TERM f, FORMULA f)) -> FORMULA f -> Bool
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

-- | check whether it contains a definedness formula in correct form
correctDef :: FORMULA f -> Bool
correctDef :: FORMULA f -> Bool
correctDef f :: FORMULA f
f = case FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripAllQuant FORMULA f
f of
  Relation (Definedness _ _) c :: Relation
c _ _ | Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
/= Relation
Equivalence -> Bool
True
  Negation (Definedness _ _) _ -> Bool
True
  Definedness _ _ -> Bool
True
  _ -> Bool
False

showForm :: (TermExtension f, FormExtension f) => Sign f e -> FORMULA f
  -> String
showForm :: Sign f e -> FORMULA f -> [Char]
showForm s :: Sign f e
s = (FORMULA f -> [Char] -> [Char]) -> [Char] -> FORMULA f -> [Char]
forall a b c. (a -> b -> c) -> b -> a -> c
flip FORMULA f -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc "" (FORMULA f -> [Char])
-> (FORMULA f -> FORMULA f) -> FORMULA f -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e -> FORMULA f -> FORMULA f
simplifyCASLSen Sign f e
s

-- check the definitional form of the partial axioms
checkDefinitional :: (FormExtension f, TermExtension f)
  => Sign f e -> [FORMULA f] -> Maybe (Result (Conservativity, [FORMULA f]))
checkDefinitional :: Sign f e
-> [FORMULA f] -> Maybe (Result (Conservativity, [FORMULA f]))
checkDefinitional tsig :: Sign f e
tsig fs :: [FORMULA f]
fs = let
       formatAxiom :: FORMULA f -> [Char]
formatAxiom = Sign f e -> FORMULA f -> [Char]
forall f e.
(TermExtension f, FormExtension f) =>
Sign f e -> FORMULA f -> [Char]
showForm Sign f e
tsig
       (noLSyms :: [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]
noLSyms, withLSyms :: [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]
withLSyms) = ((FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range)) -> Bool)
-> [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]
-> ([(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))],
    [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe (Either (TERM f) (FORMULA f)) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (Either (TERM f) (FORMULA f)) -> Bool)
-> ((FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))
    -> Maybe (Either (TERM f) (FORMULA f)))
-> (FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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))
    -> (Maybe (Either (TERM f) (FORMULA f)), Range))
-> (FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))
-> 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))
-> (Maybe (Either (TERM f) (FORMULA f)), Range)
forall a b. (a, b) -> b
snd)
         ([(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]
 -> ([(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))],
     [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]))
-> [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]
-> ([(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))],
    [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))])
forall a b. (a -> b) -> a -> b
$ (FORMULA f
 -> (FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range)))
-> [FORMULA f]
-> [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: FORMULA f
a -> (FORMULA f
a, FORMULA f -> (Maybe (Either (TERM f) (FORMULA f)), Range)
forall f.
GetRange f =>
FORMULA f -> (Maybe (Either (TERM f) (FORMULA f)), Range)
leadingSymPos FORMULA f
a)) [FORMULA f]
fs
       partialLSyms :: [(FORMULA f, OP_SYMB)]
partialLSyms = ((FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))
 -> [(FORMULA f, OP_SYMB)] -> [(FORMULA f, OP_SYMB)])
-> [(FORMULA f, OP_SYMB)]
-> [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]
-> [(FORMULA f, OP_SYMB)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (a :: FORMULA f
a, (ma :: Maybe (Either (TERM f) (FORMULA f))
ma, _)) -> case Maybe (Either (TERM f) (FORMULA f))
ma of
         Just (Left (Application t :: OP_SYMB
t@(Qual_op_name _ (Op_type k :: OpKind
k _ _ _) _) _ _))
           | OpKind
k OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpKind
Partial -> ((FORMULA f
a, OP_SYMB
t) (FORMULA f, OP_SYMB)
-> [(FORMULA f, OP_SYMB)] -> [(FORMULA f, OP_SYMB)]
forall a. a -> [a] -> [a]
:)
         _ -> [(FORMULA f, OP_SYMB)] -> [(FORMULA f, OP_SYMB)]
forall a. a -> a
id) [] [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]
withLSyms
       (domainDefs :: [(FORMULA f, OP_SYMB)]
domainDefs, otherPartials :: [(FORMULA f, OP_SYMB)]
otherPartials) = ((FORMULA f, OP_SYMB) -> Bool)
-> [(FORMULA f, OP_SYMB)]
-> ([(FORMULA f, OP_SYMB)], [(FORMULA f, OP_SYMB)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (FORMULA f -> Bool
forall f. FORMULA f -> Bool
isDomain (FORMULA f -> Bool)
-> ((FORMULA f, OP_SYMB) -> FORMULA f)
-> (FORMULA f, OP_SYMB)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f, OP_SYMB) -> FORMULA f
forall a b. (a, b) -> a
fst) [(FORMULA f, OP_SYMB)]
partialLSyms
       (withDefs :: [(FORMULA f, OP_SYMB)]
withDefs, withOutDefs :: [(FORMULA f, OP_SYMB)]
withOutDefs) = ((FORMULA f, OP_SYMB) -> Bool)
-> [(FORMULA f, OP_SYMB)]
-> ([(FORMULA f, OP_SYMB)], [(FORMULA f, OP_SYMB)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (FORMULA f -> Bool
forall f. FORMULA f -> Bool
containDef (FORMULA f -> Bool)
-> ((FORMULA f, OP_SYMB) -> FORMULA f)
-> (FORMULA f, OP_SYMB)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f, OP_SYMB) -> FORMULA f
forall a b. (a, b) -> a
fst) [(FORMULA f, OP_SYMB)]
otherPartials
       (correctDefs :: [(FORMULA f, OP_SYMB)]
correctDefs, wrongDefs :: [(FORMULA f, OP_SYMB)]
wrongDefs) = ((FORMULA f, OP_SYMB) -> Bool)
-> [(FORMULA f, OP_SYMB)]
-> ([(FORMULA f, OP_SYMB)], [(FORMULA f, OP_SYMB)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (FORMULA f -> Bool
forall f. FORMULA f -> Bool
correctDef (FORMULA f -> Bool)
-> ((FORMULA f, OP_SYMB) -> FORMULA f)
-> (FORMULA f, OP_SYMB)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f, OP_SYMB) -> FORMULA f
forall a b. (a, b) -> a
fst) [(FORMULA f, OP_SYMB)]
withDefs
       grDomainDefs :: [[(FORMULA f, OP_SYMB)]]
grDomainDefs = ((FORMULA f, OP_SYMB) -> (FORMULA f, OP_SYMB) -> Bool)
-> [(FORMULA f, OP_SYMB)] -> [[(FORMULA f, OP_SYMB)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
Rel.partList ((OP_SYMB -> OP_SYMB -> Bool)
-> ((FORMULA f, OP_SYMB) -> OP_SYMB)
-> (FORMULA f, OP_SYMB)
-> (FORMULA f, OP_SYMB)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on (Sign f e -> OP_SYMB -> OP_SYMB -> Bool
forall f e. Sign f e -> OP_SYMB -> OP_SYMB -> Bool
sameOpSymbs Sign f e
tsig) (FORMULA f, OP_SYMB) -> OP_SYMB
forall a b. (a, b) -> b
snd) [(FORMULA f, OP_SYMB)]
domainDefs
       (multDomainDefs :: [[(FORMULA f, OP_SYMB)]]
multDomainDefs, oneDomainDefs :: [[(FORMULA f, OP_SYMB)]]
oneDomainDefs) = ([(FORMULA f, OP_SYMB)] -> Bool)
-> [[(FORMULA f, OP_SYMB)]]
-> ([[(FORMULA f, OP_SYMB)]], [[(FORMULA f, OP_SYMB)]])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\ l :: [(FORMULA f, OP_SYMB)]
l -> case [(FORMULA f, OP_SYMB)]
l of
          [_] -> Bool
False
          _ -> Bool
True) [[(FORMULA f, OP_SYMB)]]
grDomainDefs
       singleDomainDefs :: [(FORMULA f, OP_SYMB)]
singleDomainDefs = ([(FORMULA f, OP_SYMB)] -> (FORMULA f, OP_SYMB))
-> [[(FORMULA f, OP_SYMB)]] -> [(FORMULA f, OP_SYMB)]
forall a b. (a -> b) -> [a] -> [b]
map [(FORMULA f, OP_SYMB)] -> (FORMULA f, OP_SYMB)
forall a. [a] -> a
head [[(FORMULA f, OP_SYMB)]]
oneDomainDefs
       nonCompleteDomainDefs :: [(FORMULA f, OP_SYMB)]
nonCompleteDomainDefs = ((FORMULA f, OP_SYMB) -> Bool)
-> [(FORMULA f, OP_SYMB)] -> [(FORMULA f, OP_SYMB)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (da :: FORMULA f
da, _) -> case FORMULA f -> Maybe (TERM f, FORMULA f)
forall f. FORMULA f -> Maybe (TERM f, FORMULA f)
domainDef FORMULA f
da of
         Just (ta :: TERM f
ta, _) | (TERM f -> Bool) -> [TERM f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TERM f -> Bool
forall t. TERM t -> Bool
isVar ([TERM f] -> Bool) -> [TERM f] -> Bool
forall a b. (a -> b) -> a -> b
$ TERM f -> [TERM f]
forall f. TERM f -> [TERM f]
arguOfTerm TERM f
ta -> Bool
False
         _ -> Bool
True) [(FORMULA f, OP_SYMB)]
singleDomainDefs
       domainObls :: [(FORMULA f, FORMULA f)]
domainObls = ((FORMULA f, OP_SYMB) -> [(FORMULA f, FORMULA f)])
-> [(FORMULA f, OP_SYMB)] -> [(FORMULA f, FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (da :: FORMULA f
da, dt :: OP_SYMB
dt) -> ((FORMULA f, OP_SYMB) -> (FORMULA f, FORMULA f))
-> [(FORMULA f, OP_SYMB)] -> [(FORMULA f, FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (de :: FORMULA f
de, _) -> (FORMULA f
da, FORMULA f
de))
           ([(FORMULA f, OP_SYMB)] -> [(FORMULA f, FORMULA f)])
-> [(FORMULA f, OP_SYMB)] -> [(FORMULA f, FORMULA f)]
forall a b. (a -> b) -> a -> b
$ ((FORMULA f, OP_SYMB) -> Bool)
-> [(FORMULA f, OP_SYMB)] -> [(FORMULA f, OP_SYMB)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Sign f e -> OP_SYMB -> OP_SYMB -> Bool
forall f e. Sign f e -> OP_SYMB -> OP_SYMB -> Bool
sameOpSymbs Sign f e
tsig OP_SYMB
dt (OP_SYMB -> Bool)
-> ((FORMULA f, OP_SYMB) -> OP_SYMB)
-> (FORMULA f, OP_SYMB)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f, OP_SYMB) -> OP_SYMB
forall a b. (a, b) -> b
snd) [(FORMULA f, OP_SYMB)]
correctDefs) [(FORMULA f, OP_SYMB)]
singleDomainDefs
       nonEqDoms :: [(FORMULA f, FORMULA f)]
nonEqDoms = ((FORMULA f, FORMULA f) -> Bool)
-> [(FORMULA f, FORMULA f)] -> [(FORMULA f, FORMULA f)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (da :: FORMULA f
da, de :: FORMULA f
de) ->
         case (FORMULA f -> Maybe (TERM f, FORMULA f)
forall f. FORMULA f -> Maybe (TERM f, FORMULA f)
domainDef FORMULA f
da, FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripAllQuant FORMULA f
de) of
           (Just (ta :: TERM f
ta, _), Relation (Definedness te :: TERM f
te _) c :: Relation
c _ _)
             | Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
/= Relation
Equivalence Bool -> Bool -> Bool
&& Sign f e -> TERM f -> TERM f -> Bool
forall f e. Sign f e -> TERM f -> TERM f -> Bool
sameOpsApp Sign f e
tsig TERM f
ta TERM f
te ->
             case FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
forall f.
GetRange f =>
FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
leadingTermPredication FORMULA f
de of
               Just (Left t :: TERM f
t) | Sign f e -> TERM f -> TERM f -> Bool
forall f e. Sign f e -> TERM f -> TERM f -> Bool
eqPattern Sign f e
tsig TERM f
te TERM f
t -> Bool
False
               _ -> Bool
True
           _ -> Bool
True) [(FORMULA f, FORMULA f)]
domainObls
       defOpSymbs :: Set OP_SYMB
defOpSymbs = [OP_SYMB] -> Set OP_SYMB
forall a. Ord a => [a] -> Set a
Set.fromList ([OP_SYMB] -> Set OP_SYMB) -> [OP_SYMB] -> Set OP_SYMB
forall a b. (a -> b) -> a -> b
$ ([(FORMULA f, OP_SYMB)] -> OP_SYMB)
-> [[(FORMULA f, OP_SYMB)]] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f, OP_SYMB) -> OP_SYMB
forall a b. (a, b) -> b
snd ((FORMULA f, OP_SYMB) -> OP_SYMB)
-> ([(FORMULA f, OP_SYMB)] -> (FORMULA f, OP_SYMB))
-> [(FORMULA f, OP_SYMB)]
-> OP_SYMB
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(FORMULA f, OP_SYMB)] -> (FORMULA f, OP_SYMB)
forall a. [a] -> a
head) [[(FORMULA f, OP_SYMB)]]
grDomainDefs
         [OP_SYMB] -> [OP_SYMB] -> [OP_SYMB]
forall a. [a] -> [a] -> [a]
++ ((FORMULA f, OP_SYMB) -> OP_SYMB)
-> [(FORMULA f, OP_SYMB)] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA f, OP_SYMB) -> OP_SYMB
forall a b. (a, b) -> b
snd [(FORMULA f, OP_SYMB)]
correctDefs
       wrongWithoutDefs :: [(FORMULA f, OP_SYMB)]
wrongWithoutDefs = ((FORMULA f, OP_SYMB) -> Bool)
-> [(FORMULA f, OP_SYMB)] -> [(FORMULA f, OP_SYMB)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((OP_SYMB -> Set OP_SYMB -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set OP_SYMB
defOpSymbs) (OP_SYMB -> Bool)
-> ((FORMULA f, OP_SYMB) -> OP_SYMB)
-> (FORMULA f, OP_SYMB)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f, OP_SYMB) -> OP_SYMB
forall a b. (a, b) -> b
snd)
         [(FORMULA f, OP_SYMB)]
withOutDefs
       ds :: [Diagnosis]
ds = ((FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))
 -> Diagnosis)
-> [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]
-> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: FORMULA f
a, (_, pos :: Range
pos)) -> DiagKind -> [Char] -> Range -> Diagnosis
Diag
         DiagKind
Warning ("missing leading symbol in:\n  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FORMULA f -> [Char]
formatAxiom FORMULA f
a) Range
pos)
           [(FORMULA f, (Maybe (Either (TERM f) (FORMULA f)), Range))]
noLSyms
         [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ ((FORMULA f, OP_SYMB) -> Diagnosis)
-> [(FORMULA f, OP_SYMB)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: FORMULA f
a, t :: OP_SYMB
t) -> DiagKind -> [Char] -> Range -> Diagnosis
Diag
         DiagKind
Warning ("definedness is not definitional:\n  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FORMULA f -> [Char]
formatAxiom FORMULA f
a)
                (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> Range
forall a. GetRange a => a -> Range
getRange OP_SYMB
t) [(FORMULA f, OP_SYMB)]
wrongDefs
         [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ ([(FORMULA f, OP_SYMB)] -> Diagnosis)
-> [[(FORMULA f, OP_SYMB)]] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ l :: [(FORMULA f, OP_SYMB)]
l@((_, t :: OP_SYMB
t) : _) -> DiagKind -> [Char] -> Range -> Diagnosis
Diag DiagKind
Warning ([[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
             ("multiple domain axioms for: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OP_SYMB -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc OP_SYMB
t "")
             [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: ((FORMULA f, OP_SYMB) -> [Char])
-> [(FORMULA f, OP_SYMB)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (("  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char])
-> ((FORMULA f, OP_SYMB) -> [Char])
-> (FORMULA f, OP_SYMB)
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> [Char]
formatAxiom (FORMULA f -> [Char])
-> ((FORMULA f, OP_SYMB) -> FORMULA f)
-> (FORMULA f, OP_SYMB)
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f, OP_SYMB) -> FORMULA f
forall a b. (a, b) -> a
fst) [(FORMULA f, OP_SYMB)]
l) (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> Range
forall a. GetRange a => a -> Range
getRange OP_SYMB
t)
           [[(FORMULA f, OP_SYMB)]]
multDomainDefs
         [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ ((FORMULA f, OP_SYMB) -> Diagnosis)
-> [(FORMULA f, OP_SYMB)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: FORMULA f
a, t :: OP_SYMB
t) -> DiagKind -> [Char] -> Range -> Diagnosis
Diag
         DiagKind
Warning ("missing definedness condition for partial '"
                      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ OP_SYMB -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc OP_SYMB
t "' in:\n  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FORMULA f -> [Char]
formatAxiom FORMULA f
a)
             (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> Range
forall a. GetRange a => a -> Range
getRange OP_SYMB
t) [(FORMULA f, OP_SYMB)]
wrongWithoutDefs
         [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ ((FORMULA f, OP_SYMB) -> Diagnosis)
-> [(FORMULA f, OP_SYMB)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ (da :: FORMULA f
da, _) -> DiagKind -> [Char] -> Range -> Diagnosis
Diag
         DiagKind
Warning ("non-complete domain axiom:\n  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FORMULA f -> [Char]
formatAxiom FORMULA f
da)
             (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Range
forall a. GetRange a => a -> Range
getRange FORMULA f
da) [(FORMULA f, OP_SYMB)]
nonCompleteDomainDefs
         [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ ((FORMULA f, FORMULA f) -> Diagnosis)
-> [(FORMULA f, FORMULA f)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ (da :: FORMULA f
da, de :: FORMULA f
de) -> DiagKind -> [Char] -> Range -> Diagnosis
Diag
         DiagKind
Warning ("unexpected definedness condition:\n  "
                  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FORMULA f -> [Char]
formatAxiom FORMULA f
de
                  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "\nin the presence of domain axiom:\n  "
                  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FORMULA f -> [Char]
formatAxiom FORMULA f
da) (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Range
forall a. GetRange a => a -> Range
getRange FORMULA f
de) [(FORMULA f, FORMULA f)]
nonEqDoms
       in if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then Maybe (Result (Conservativity, [FORMULA f]))
forall a. Maybe a
Nothing else Result (Conservativity, [FORMULA f])
-> Maybe (Result (Conservativity, [FORMULA f]))
forall a. a -> Maybe a
Just (Result (Conservativity, [FORMULA f])
 -> Maybe (Result (Conservativity, [FORMULA f])))
-> Result (Conservativity, [FORMULA f])
-> Maybe (Result (Conservativity, [FORMULA f]))
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
-> Maybe (Conservativity, [FORMULA f])
-> Result (Conservativity, [FORMULA f])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Conservativity, [FORMULA f])
forall a. Maybe a
Nothing

{-
  call the symbols in the image of the signature morphism "new"

- each new sort must be a free type,
  i.e. it must occur in a sort generation constraint that is marked as free
    (Sort_gen_ax constrs True)
    such that the sort is in srts,
        where (srts,ops,_)=recover_Sort_gen_ax constrs
    if not, output "don't know"
  and there must be one term of that sort (inhabited)
    if not, output "no"
- group the axioms according to their leading operation/predicate symbol,
  i.e. the f resp. the p in
  forall x_1:s_n .... x_n:s_n .                  f(t_1,...,t_m)=t
  forall x_1:s_n .... x_n:s_n .       phi =>      f(t_1,...,t_m)=t
                                  Implication  Application  Strong_equation
  forall x_1:s_n .... x_n:s_n .                  p(t_1,...,t_m)<=>phi
  forall x_1:s_n .... x_n:s_n .    phi1  =>      p(t_1,...,t_m)<=>phi
                                 Implication   Predication    Equivalence
  if there are axioms not being of this form, output "don't know"
-}
checkSort :: Bool -> Set.Set SORT -> Set.Set SORT -> Set.Set SORT
  -> Set.Set SORT -> Set.Set SORT -> Sign f e -> Sign f e
  -> Maybe (Result (Conservativity, [FORMULA f]))
checkSort :: Bool
-> Set SORT
-> Set SORT
-> Set SORT
-> Set SORT
-> Set SORT
-> Sign f e
-> Sign f e
-> Maybe (Result (Conservativity, [FORMULA f]))
checkSort noSentence :: Bool
noSentence nSorts :: Set SORT
nSorts defSubsorts :: Set SORT
defSubsorts gSorts :: Set SORT
gSorts fSorts :: Set SORT
fSorts nefsorts :: Set SORT
nefsorts sSig :: Sign f e
sSig tSig :: Sign f e
tSig
    | Bool
noSentence Bool -> Bool -> Bool
&& Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
nSorts =
        let cond :: Bool
cond = OpMap -> Bool
forall a b. MapSet a b -> Bool
MapSet.null (OpMap -> OpMap -> OpMap
diffOpMapSet (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
tSig) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
sSig)
              Bool -> Bool -> Bool
&& PredMap -> Bool
forall a b. MapSet a b -> Bool
MapSet.null (PredMap -> PredMap -> PredMap
diffMapSet (Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
tSig) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
sSig)
        in Result (Conservativity, [FORMULA f])
-> Maybe (Result (Conservativity, [FORMULA f]))
forall a. a -> Maybe a
Just (Result (Conservativity, [FORMULA f])
 -> Maybe (Result (Conservativity, [FORMULA f])))
-> Result (Conservativity, [FORMULA f])
-> Maybe (Result (Conservativity, [FORMULA f]))
forall a b. (a -> b) -> a -> b
$ (Conservativity, [FORMULA f])
-> [Char] -> Result (Conservativity, [FORMULA f])
forall a. a -> [Char] -> Result a
justHint (if Bool
cond then Conservativity
Def else Conservativity
Cons, [])
        ([Char] -> Result (Conservativity, [FORMULA f]))
-> [Char] -> Result (Conservativity, [FORMULA f])
forall a b. (a -> b) -> a -> b
$ (if Bool
cond then "neither symbols"
          else "neither sorts") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ " nor sentences have been added"
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
notFreeSorts =
        [Char] -> Set SORT -> Maybe (Result (Conservativity, [FORMULA f]))
forall a a.
(GetRange a, Pretty a) =>
[Char] -> a -> Maybe (Result a)
mkUnknown "some types are not freely generated" Set SORT
notFreeSorts
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
nefsorts = [Char]
-> Set SORT
-> Maybe (Conservativity, [FORMULA f])
-> Maybe (Result (Conservativity, [FORMULA f]))
forall a a.
(GetRange a, Pretty a) =>
[Char] -> a -> Maybe a -> Maybe (Result a)
mkWarn "some sorts are not inhabited"
        Set SORT
nefsorts (Maybe (Conservativity, [FORMULA f])
 -> Maybe (Result (Conservativity, [FORMULA f])))
-> Maybe (Conservativity, [FORMULA f])
-> Maybe (Result (Conservativity, [FORMULA f]))
forall a b. (a -> b) -> a -> b
$ (Conservativity, [FORMULA f])
-> Maybe (Conservativity, [FORMULA f])
forall a. a -> Maybe a
Just (Conservativity
Inconsistent, [])
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set SORT -> Bool
forall a. Set a -> Bool
Set.null Set SORT
genNotNew = [Char] -> Set SORT -> Maybe (Result (Conservativity, [FORMULA f]))
forall a a.
(GetRange a, Pretty a) =>
[Char] -> a -> Maybe (Result a)
mkUnknown "some defined sorts are not new"
        Set SORT
genNotNew
    | Bool
otherwise = Maybe (Result (Conservativity, [FORMULA f]))
forall a. Maybe a
Nothing
    where
        notFreeSorts :: Set SORT
notFreeSorts = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set SORT
nSorts
          (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set SORT
gSorts Set SORT
fSorts
        genNotNew :: Set SORT
genNotNew = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference
          ([Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set SORT
defSubsorts, Set SORT
gSorts, Set SORT
fSorts]) Set SORT
nSorts
        mkWarn :: [Char] -> a -> Maybe a -> Maybe (Result a)
mkWarn s :: [Char]
s i :: a
i r :: Maybe a
r = Result a -> Maybe (Result a)
forall a. a -> Maybe a
Just (Result a -> Maybe (Result a)) -> Result a -> Maybe (Result a)
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe a -> Result a
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> [Char] -> a -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> [Char] -> a -> Diagnosis
mkDiag DiagKind
Warning [Char]
s a
i] Maybe a
r
        mkUnknown :: [Char] -> a -> Maybe (Result a)
mkUnknown s :: [Char]
s i :: a
i = [Char] -> a -> Maybe a -> Maybe (Result a)
forall a a.
(GetRange a, Pretty a) =>
[Char] -> a -> Maybe a -> Maybe (Result a)
mkWarn [Char]
s a
i Maybe a
forall a. Maybe a
Nothing

checkLeadingTerms :: (FormExtension f, TermExtension f, Ord f)
  => Sign f e -> [FORMULA f] -> [OP_SYMB]
  -> Maybe (Result (Conservativity, [FORMULA f]))
checkLeadingTerms :: Sign f e
-> [FORMULA f]
-> [OP_SYMB]
-> Maybe (Result (Conservativity, [FORMULA f]))
checkLeadingTerms tsig :: Sign f e
tsig fsn :: [FORMULA f]
fsn constructors :: [OP_SYMB]
constructors = let
    ltp :: [Either (TERM f) (FORMULA f)]
ltp = (FORMULA f -> Maybe (Either (TERM f) (FORMULA f)))
-> [FORMULA f] -> [Either (TERM f) (FORMULA f)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
forall f.
GetRange f =>
FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
leadingTermPredication [FORMULA f]
fsn
    formatTerm :: TERM f -> [Char]
formatTerm = (TERM f -> [Char] -> [Char]) -> [Char] -> TERM f -> [Char]
forall a b c. (a -> b -> c) -> b -> a -> c
flip TERM f -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc "" (TERM f -> [Char]) -> (TERM f -> TERM f) -> TERM f -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> TERM f -> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e -> TERM f -> TERM f
simplifyCASLTerm Sign f e
tsig
    args :: [(Range, [Char], [TERM f])]
args = (Either (TERM f) (FORMULA f)
 -> [(Range, [Char], [TERM f])] -> [(Range, [Char], [TERM f])])
-> [(Range, [Char], [TERM f])]
-> [Either (TERM f) (FORMULA f)]
-> [(Range, [Char], [TERM f])]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ ei :: Either (TERM f) (FORMULA f)
ei -> case Either (TERM f) (FORMULA f)
ei of
      Left (Application os :: OP_SYMB
os ts :: [TERM f]
ts qs :: Range
qs) ->
         ((Range
qs, "term for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show (OP_SYMB -> SORT
opSymbName OP_SYMB
os), [TERM f]
ts) (Range, [Char], [TERM f])
-> [(Range, [Char], [TERM f])] -> [(Range, [Char], [TERM f])]
forall a. a -> [a] -> [a]
:)
      Right (Predication ps :: PRED_SYMB
ps ts :: [TERM f]
ts qs :: Range
qs) ->
         ((Range
qs, "predicate " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show (PRED_SYMB -> SORT
predSymbName PRED_SYMB
ps), [TERM f]
ts) (Range, [Char], [TERM f])
-> [(Range, [Char], [TERM f])] -> [(Range, [Char], [TERM f])]
forall a. a -> [a] -> [a]
:)
      _ -> [(Range, [Char], [TERM f])] -> [(Range, [Char], [TERM f])]
forall a. a -> a
id) [] [Either (TERM f) (FORMULA f)]
ltp
    ds :: [Diagnosis]
ds = ((Range, [Char], [TERM f]) -> [Diagnosis] -> [Diagnosis])
-> [Diagnosis] -> [(Range, [Char], [TERM f])] -> [Diagnosis]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (qs :: Range
qs, d :: [Char]
d, ts :: [TERM f]
ts) l :: [Diagnosis]
l ->
           let vs :: [TERM f]
vs = (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
               dupVs :: [TERM f]
dupVs = [TERM f]
vs [TERM f] -> [TERM f] -> [TERM f]
forall a. Eq a => [a] -> [a] -> [a]
\\ Set (TERM f) -> [TERM f]
forall a. Set a -> [a]
Set.toList ([TERM f] -> Set (TERM f)
forall a. Ord a => [a] -> Set a
Set.fromList [TERM f]
vs)
               nonCs :: [TERM f]
nonCs = Sign f e -> [OP_SYMB] -> [TERM f] -> [TERM f]
forall f e. Sign f e -> [OP_SYMB] -> [TERM f] -> [TERM f]
checkTerms Sign f e
tsig [OP_SYMB]
constructors [TERM f]
ts
               td :: [Char]
td = " in leading " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
d [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ": "
           in (TERM f -> Diagnosis) -> [TERM f] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: TERM f
v -> DiagKind -> [Char] -> Range -> Diagnosis
Diag DiagKind
Warning
                    ("duplicate variable" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
td [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TERM f -> [Char]
formatTerm TERM f
v) Range
qs) [TERM f]
dupVs
              [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ (TERM f -> Diagnosis) -> [TERM f] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ t :: TERM f
t -> DiagKind -> [Char] -> Range -> Diagnosis
Diag DiagKind
Warning
                     ("non-constructor" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
td [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TERM f -> [Char]
formatTerm TERM f
t)
                     Range
qs) [TERM f]
nonCs
              [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
l) [] [(Range, [Char], [TERM f])]
args
    in if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then Maybe (Result (Conservativity, [FORMULA f]))
forall a. Maybe a
Nothing else Result (Conservativity, [FORMULA f])
-> Maybe (Result (Conservativity, [FORMULA f]))
forall a. a -> Maybe a
Just (Result (Conservativity, [FORMULA f])
 -> Maybe (Result (Conservativity, [FORMULA f])))
-> Result (Conservativity, [FORMULA f])
-> Maybe (Result (Conservativity, [FORMULA f]))
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
-> Maybe (Conservativity, [FORMULA f])
-> Result (Conservativity, [FORMULA f])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Conservativity, [FORMULA f])
forall a. Maybe a
Nothing

-- check the sufficient completeness
checkIncomplete :: (FormExtension f, TermExtension f, Ord f)
  => Sign f e -> [FORMULA f] -> [OP_SYMB] -> [[FORMULA f]] -> [OP_SYMB]
  -> Maybe (Result (Conservativity, [FORMULA f]))
checkIncomplete :: Sign f e
-> [FORMULA f]
-> [OP_SYMB]
-> [[FORMULA f]]
-> [OP_SYMB]
-> Maybe (Result (Conservativity, [FORMULA f]))
checkIncomplete sig :: Sign f e
sig obligations :: [FORMULA f]
obligations doms :: [OP_SYMB]
doms fsn :: [[FORMULA f]]
fsn cons :: [OP_SYMB]
cons =
  case Sign f e
-> [OP_SYMB]
-> [[FORMULA f]]
-> [OP_SYMB]
-> [(Result [([Char], FORMULA f)], [FORMULA f])]
forall f e.
(Ord f, FormExtension f, TermExtension f) =>
Sign f e
-> [OP_SYMB]
-> [[FORMULA f]]
-> [OP_SYMB]
-> [(Result [([Char], FORMULA f)], [FORMULA f])]
getNotComplete Sign f e
sig [OP_SYMB]
doms [[FORMULA f]]
fsn [OP_SYMB]
cons of
  [] -> Maybe (Result (Conservativity, [FORMULA f]))
forall a. Maybe a
Nothing
  incomplete :: [(Result [([Char], FORMULA f)], [FORMULA f])]
incomplete -> let
    formatAxiom :: FORMULA f -> [Char]
formatAxiom = Sign f e -> FORMULA f -> [Char]
forall f e.
(TermExtension f, FormExtension f) =>
Sign f e -> FORMULA f -> [Char]
showForm Sign f e
sig
    in Result (Conservativity, [FORMULA f])
-> Maybe (Result (Conservativity, [FORMULA f]))
forall a. a -> Maybe a
Just (Result (Conservativity, [FORMULA f])
 -> Maybe (Result (Conservativity, [FORMULA f])))
-> Result (Conservativity, [FORMULA f])
-> Maybe (Result (Conservativity, [FORMULA f]))
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
-> Maybe (Conservativity, [FORMULA f])
-> Result (Conservativity, [FORMULA f])
forall a. [Diagnosis] -> Maybe a -> Result a
Result
      (((Result [([Char], FORMULA f)], [FORMULA f]) -> Diagnosis)
-> [(Result [([Char], FORMULA f)], [FORMULA f])] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Result ds :: [Diagnosis]
ds mfs :: Maybe [([Char], FORMULA f)]
mfs, fs :: [FORMULA f]
fs@(hd :: FORMULA f
hd : _)) -> let
        (lSym :: Maybe (Either (TERM f) (FORMULA f))
lSym, pos :: Range
pos) = FORMULA f -> (Maybe (Either (TERM f) (FORMULA f)), Range)
forall f.
GetRange f =>
FORMULA f -> (Maybe (Either (TERM f) (FORMULA f)), Range)
leadingSymPos FORMULA f
hd
        sname :: SORT
sname = case (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))
lSym of
                      Just (Left opS :: OP_SYMB
opS) -> OP_SYMB -> SORT
opSymbName OP_SYMB
opS
                      Just (Right pS :: PRED_SYMB
pS) -> PRED_SYMB -> SORT
predSymbName PRED_SYMB
pS
                      _ -> [Char] -> SORT
forall a. HasCallStack => [Char] -> a
error "CASL.CCC.FreeTypes.<Symb_Name>"
        in DiagKind -> [Char] -> Range -> Diagnosis
Diag DiagKind
Warning ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
             ("the definition of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show SORT
sname
              [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds then " may not be" else " is not") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ " complete")
             [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: "the defining formula group is:"
             [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: ((FORMULA f, Int) -> [Char]) -> [(FORMULA f, Int)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (\ (f :: FORMULA f
f, n :: Int
n) -> "  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char] -> [Char]
forall a. Show a => a -> [Char] -> [Char]
shows Int
n ". "
                    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FORMULA f -> [Char]
formatAxiom FORMULA f
f) ([FORMULA f] -> [(FORMULA f, Int)]
forall a. [a] -> [(a, Int)]
number [FORMULA f]
fs)
             [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ (Diagnosis -> [Char]) -> [Diagnosis] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Diagnosis -> [Char]
diagString [Diagnosis]
ds
             [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
-> ([([Char], FORMULA f)] -> [[Char]])
-> Maybe [([Char], FORMULA f)]
-> [[Char]]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe []
                 ((([Char], FORMULA f) -> [Char])
-> [([Char], FORMULA f)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: [Char]
p, f :: FORMULA f
f) -> "possibly incomplete pattern for: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
p
                   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "\n  with completeness condition: "
                   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FORMULA f -> [Char]
formatAxiom FORMULA f
f)) Maybe [([Char], FORMULA f)]
mfs
             ) Range
pos)
       [(Result [([Char], FORMULA f)], [FORMULA f])]
incomplete) (Maybe (Conservativity, [FORMULA f])
 -> Result (Conservativity, [FORMULA f]))
-> Maybe (Conservativity, [FORMULA f])
-> Result (Conservativity, [FORMULA f])
forall a b. (a -> b) -> a -> b
$ (Conservativity, [FORMULA f])
-> Maybe (Conservativity, [FORMULA f])
forall a. a -> Maybe a
Just (Conservativity
Cons, [FORMULA f]
obligations)

renameVars :: Int -> [FORMULA f] -> (Int, [FORMULA f])
renameVars :: Int -> [FORMULA f] -> (Int, [FORMULA f])
renameVars c :: Int
c = (FORMULA f -> (Int, [FORMULA f]) -> (Int, [FORMULA f]))
-> (Int, [FORMULA f]) -> [FORMULA f] -> (Int, [FORMULA f])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ f :: FORMULA f
f (c1 :: Int
c1, l :: [FORMULA f]
l) ->
   let (f2 :: FORMULA f
f2, c2 :: Int
c2) = Int -> (f -> f) -> FORMULA f -> (FORMULA f, Int)
forall f. Int -> (f -> f) -> FORMULA f -> (FORMULA f, Int)
alphaConvert Int
c1 f -> f
forall a. a -> a
id FORMULA f
f in
   (Int
c2, FORMULA f
f2 FORMULA f -> [FORMULA f] -> [FORMULA f]
forall a. a -> [a] -> [a]
: [FORMULA f]
l)) (Int
c, [])

checkTerminal :: (FormExtension f, TermExtension f, Ord f)
  => Sign f e -> Conservativity -> [FORMULA f] -> [FORMULA f] -> [FORMULA f]
  -> IO (Result (Conservativity, [FORMULA f]))
checkTerminal :: Sign f e
-> Conservativity
-> [FORMULA f]
-> [FORMULA f]
-> [FORMULA f]
-> IO (Result (Conservativity, [FORMULA f]))
checkTerminal sig :: Sign f e
sig conStatus :: Conservativity
conStatus obligations :: [FORMULA f]
obligations doms :: [FORMULA f]
doms fsn :: [FORMULA f]
fsn =
    if [FORMULA f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FORMULA f]
fsn then Result (Conservativity, [FORMULA f])
-> IO (Result (Conservativity, [FORMULA f]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Conservativity, [FORMULA f])
 -> IO (Result (Conservativity, [FORMULA f])))
-> Result (Conservativity, [FORMULA f])
-> IO (Result (Conservativity, [FORMULA f]))
forall a b. (a -> b) -> a -> b
$ (Conservativity, [FORMULA f])
-> [Char] -> Result (Conservativity, [FORMULA f])
forall a. a -> [Char] -> Result a
justHint (Conservativity
conStatus, [FORMULA f]
obligations)
      "no defining sentences"
    else do
    let (c :: Int
c, domains :: [FORMULA f]
domains) = Int -> [FORMULA f] -> (Int, [FORMULA f])
forall f. Int -> [FORMULA f] -> (Int, [FORMULA f])
renameVars 1 [FORMULA f]
doms
        fs_terminalProof :: [FORMULA f]
fs_terminalProof = (Int, [FORMULA f]) -> [FORMULA f]
forall a b. (a, b) -> b
snd ((Int, [FORMULA f]) -> [FORMULA f])
-> (Int, [FORMULA f]) -> [FORMULA f]
forall a b. (a -> b) -> a -> b
$ Int -> [FORMULA f] -> (Int, [FORMULA f])
forall f. Int -> [FORMULA f] -> (Int, [FORMULA f])
renameVars Int
c [FORMULA f]
fsn
    (proof :: Maybe Bool
proof, str :: [Char]
str) <- Sign f e -> [FORMULA f] -> [FORMULA f] -> IO (Maybe Bool, [Char])
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e -> [FORMULA f] -> [FORMULA f] -> IO (Maybe Bool, [Char])
terminationProof Sign f e
sig [FORMULA f]
fs_terminalProof [FORMULA f]
domains
    Result (Conservativity, [FORMULA f])
-> IO (Result (Conservativity, [FORMULA f]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Conservativity, [FORMULA f])
 -> IO (Result (Conservativity, [FORMULA f])))
-> Result (Conservativity, [FORMULA f])
-> IO (Result (Conservativity, [FORMULA f]))
forall a b. (a -> b) -> a -> b
$ case Maybe Bool
proof of
        Just True -> (Conservativity, [FORMULA f])
-> [Char] -> Result (Conservativity, [FORMULA f])
forall a. a -> [Char] -> Result a
justHint (Conservativity
conStatus, [FORMULA f]
obligations) "termination succeeded"
        _ -> (Conservativity, [FORMULA f])
-> [Char] -> Range -> Result (Conservativity, [FORMULA f])
forall a. a -> [Char] -> Range -> Result a
warning (Conservativity
Cons, [FORMULA f]
obligations)
             (if Maybe Bool -> Bool
forall a. Maybe a -> Bool
isJust Maybe Bool
proof then "not terminating"
              else "cannot prove termination: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
str) Range
nullRange

checkPos :: FORMULA f -> Bool
checkPos :: FORMULA f -> Bool
checkPos f :: FORMULA f
f = case FORMULA f
f of
      Quantification _ _ f' :: FORMULA f
f' _ -> FORMULA f -> Bool
forall f. FORMULA f -> Bool
checkPos FORMULA f
f'
      Junction _ cs :: [FORMULA f]
cs _ -> (FORMULA f -> Bool) -> [FORMULA f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA f -> Bool
forall f. FORMULA f -> Bool
checkPos [FORMULA f]
cs
      Relation i1 :: FORMULA f
i1 c :: Relation
c i2 :: FORMULA f
i2 _ -> let
        c1 :: Bool
c1 = FORMULA f -> Bool
forall f. FORMULA f -> Bool
checkPos FORMULA f
i1
        c2 :: Bool
c2 = FORMULA f -> Bool
forall f. FORMULA f -> Bool
checkPos FORMULA f
i2
        in if Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
== Relation
Equivalence then Bool
c1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
c2 else Bool
c1 Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
<= Bool
c2
      Negation n :: FORMULA f
n _ -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Bool
forall f. FORMULA f -> Bool
checkPos FORMULA f
n
      Atom b :: Bool
b _ -> Bool
b
      Predication {} -> Bool
True
      Membership {} -> Bool
True
      Definedness {} -> Bool
True
      Equation {} -> Bool
True
      Sort_gen_ax cs :: [Constraint]
cs _ -> case [Constraint]
cs of
        [c :: Constraint
c] -> case Constraint -> [(OP_SYMB, [Int])]
opSymbs Constraint
c of
          [_] -> Bool
True
            {- just a single constructor creates a unique value
            even for multiple one-point components -}
          _ -> Bool
False
        _ -> Bool
False
      _ -> Bool
False

partitionMaybe :: (a -> Maybe b) -> [a] -> ([b], [a])
partitionMaybe :: (a -> Maybe b) -> [a] -> ([b], [a])
partitionMaybe f :: a -> Maybe b
f = (a -> ([b], [a]) -> ([b], [a])) -> ([b], [a]) -> [a] -> ([b], [a])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ a :: a
a (bs :: [b]
bs, as :: [a]
as) ->
  ([b], [a]) -> (b -> ([b], [a])) -> Maybe b -> ([b], [a])
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([b]
bs, a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
as) (\ b :: b
b -> (b
b b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
bs, [a]
as)) (Maybe b -> ([b], [a])) -> Maybe b -> ([b], [a])
forall a b. (a -> b) -> a -> b
$ a -> Maybe b
f a
a) ([], [])


{- -----------------------------------------------------------------------
   function checkFreeType:
   - check if leading symbols are new (not in the image of morphism),
           if not, return them as obligations
   - generated datatype is free
   - if new sort is not etype or esort, it can not be empty.
   - the leading terms consist of variables and constructors only,
           if not, return Nothing
     - split function leading_Symb into
       leadingTermPredication
       and
       extractLeadingSymb
     - collect all operation symbols from recover_Sort_gen_ax fconstrs
                                                       (= constructors)
   - no variable occurs twice in a leading term, if not, return Nothing
   - check that patterns do not overlap, if not, return obligations
     This means:
       in each group of the grouped axioms:
       all patterns of leading terms/formulas are disjoint
       this means: either leading symbol is a variable,
                           and there is just one axiom
                   otherwise, group axioms according to leading symbol
                              no symbol may be a variable
                              check recursively the arguments of
                              constructor in each group
  - sufficient completeness
  - termination proof
------------------------------------------------------------------------
free datatypes and recursive equations are consistent -}
checkFreeType :: (FormExtension f, TermExtension f, Ord f)
  => (Sign f e, [Named (FORMULA f)]) -> Morphism f e m
  -> [Named (FORMULA f)] -> IO (Result (Conservativity, [FORMULA f]))
checkFreeType :: (Sign f e, [Named (FORMULA f)])
-> Morphism f e m
-> [Named (FORMULA f)]
-> IO (Result (Conservativity, [FORMULA f]))
checkFreeType (_, osens :: [Named (FORMULA f)]
osens) m :: Morphism f e m
m axs :: [Named (FORMULA f)]
axs = do
  let sig :: Sign f e
sig = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
m
      sSig :: Sign f e
sSig = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
imageOfMorphism Morphism f e m
m
      fs :: [FORMULA f]
fs = [Named (FORMULA f)] -> [FORMULA f]
forall f. [Named (FORMULA f)] -> [FORMULA f]
getFs [Named (FORMULA f)]
axs -- strip labels and generated sentences
      (exQuants :: [FORMULA f]
exQuants, fs2 :: [FORMULA f]
fs2) = (FORMULA f -> Bool) -> [FORMULA f] -> ([FORMULA f], [FORMULA f])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition FORMULA f -> Bool
forall f. FORMULA f -> Bool
isExQuanti [FORMULA f]
fs
      (memShips :: [FORMULA f]
memShips, fs3 :: [FORMULA f]
fs3) = (FORMULA f -> Bool) -> [FORMULA f] -> ([FORMULA f], [FORMULA f])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition FORMULA f -> Bool
forall f. FORMULA f -> Bool
isMembership [FORMULA f]
fs2
      (sortGens1 :: [FORMULA f]
sortGens1, axioms :: [FORMULA f]
axioms) = (FORMULA f -> Bool) -> [FORMULA f] -> ([FORMULA f], [FORMULA f])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition FORMULA f -> Bool
forall f. FORMULA f -> Bool
isSortGen [FORMULA f]
fs3
      (freeSortGens :: [FORMULA f]
freeSortGens, sortGens :: [FORMULA f]
sortGens) = (FORMULA f -> Bool) -> [FORMULA f] -> ([FORMULA f], [FORMULA f])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition FORMULA f -> Bool
forall f. FORMULA f -> Bool
isFreeSortGen [FORMULA f]
sortGens1
      (domains :: [FORMULA f]
domains, axLessDoms :: [FORMULA f]
axLessDoms) = (FORMULA f -> Bool) -> [FORMULA f] -> ([FORMULA f], [FORMULA f])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition FORMULA f -> Bool
forall f. FORMULA f -> Bool
isDomain [FORMULA f]
axioms
      (genSorts1 :: Set SORT
genSorts1, cons1 :: Set OP_SYMB
cons1) =
        [FORMULA f] -> (Set SORT, Set OP_SYMB)
forall f. [FORMULA f] -> (Set SORT, Set OP_SYMB)
recoverSortsAndConstructors ([FORMULA f] -> (Set SORT, Set OP_SYMB))
-> [FORMULA f] -> (Set SORT, Set OP_SYMB)
forall a b. (a -> b) -> a -> b
$ [Named (FORMULA f)] -> [FORMULA f]
forall f. [Named (FORMULA f)] -> [FORMULA f]
getFs [Named (FORMULA f)]
osens
      (freeSorts :: Set SORT
freeSorts, cons2 :: Set OP_SYMB
cons2) =
        [FORMULA f] -> (Set SORT, Set OP_SYMB)
forall f. [FORMULA f] -> (Set SORT, Set OP_SYMB)
recoverSortsAndConstructors [FORMULA f]
freeSortGens
      (genSorts2 :: Set SORT
genSorts2, cons3 :: Set OP_SYMB
cons3) =
        [FORMULA f] -> (Set SORT, Set OP_SYMB)
forall f. [FORMULA f] -> (Set SORT, Set OP_SYMB)
recoverSortsAndConstructors [FORMULA f]
sortGens
      sortCons :: (Set SORT, [OP_SYMB])
sortCons@(genSorts :: Set SORT
genSorts, cons :: [OP_SYMB]
cons) =
        ([Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
         [Set SORT
freeSorts, Set SORT
genSorts2, (SORT -> SORT) -> Set SORT -> Set SORT
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Sort_map -> SORT -> SORT
mapSort (Sort_map -> SORT -> SORT) -> Sort_map -> SORT -> SORT
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m) Set SORT
genSorts1]
        , Set OP_SYMB -> [OP_SYMB]
forall a. Set a -> [a]
Set.toList (Set OP_SYMB -> [OP_SYMB]) -> Set OP_SYMB -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$ [Set OP_SYMB] -> Set OP_SYMB
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set OP_SYMB
cons2, Set OP_SYMB
cons3, (OP_SYMB -> OP_SYMB) -> Set OP_SYMB -> Set OP_SYMB
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Morphism f e m -> OP_SYMB -> OP_SYMB
forall f e m. Morphism f e m -> OP_SYMB -> OP_SYMB
mapOpSymb Morphism f e m
m) Set OP_SYMB
cons1])
      oldSorts :: Set SORT
oldSorts = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
sSig
      newSorts :: Set SORT
newSorts = Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
sig) Set SORT
oldSorts
      emptySorts :: Set SORT
emptySorts = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet Sign f e
sig
      nonInhabitedSorts :: Set SORT
nonInhabitedSorts = Set SORT
-> Set SORT -> Set SORT -> (Set SORT, [OP_SYMB]) -> Set SORT
getNefsorts Set SORT
oldSorts Set SORT
newSorts Set SORT
emptySorts (Set SORT, [OP_SYMB])
sortCons
      (subsortDefns :: [(SORT, VAR_DECL, FORMULA f)]
subsortDefns, memShips2 :: [FORMULA f]
memShips2) = (FORMULA f -> Maybe (SORT, VAR_DECL, FORMULA f))
-> [FORMULA f] -> ([(SORT, VAR_DECL, FORMULA f)], [FORMULA f])
forall a b. (a -> Maybe b) -> [a] -> ([b], [a])
partitionMaybe FORMULA f -> Maybe (SORT, VAR_DECL, FORMULA f)
forall f. FORMULA f -> Maybe (SORT, VAR_DECL, FORMULA f)
isSubsortDef [FORMULA f]
memShips
      defSubsorts :: Set SORT
defSubsorts = [SORT] -> Set SORT
forall a. Ord a => [a] -> Set a
Set.fromList ([SORT] -> Set SORT) -> [SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ ((SORT, VAR_DECL, FORMULA f) -> SORT)
-> [(SORT, VAR_DECL, FORMULA f)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: SORT
s, _, _) -> SORT
s) [(SORT, VAR_DECL, FORMULA f)]
subsortDefns
      dataStatus :: Conservativity
dataStatus = Set SORT -> Set SORT -> Set SORT -> Conservativity
getDataStatus Set SORT
newSorts Set SORT
defSubsorts Set SORT
genSorts
      defsForOld :: [FORMULA f]
defsForOld = Sign f e -> [FORMULA f] -> [FORMULA f]
forall f e. GetRange f => Sign f e -> [FORMULA f] -> [FORMULA f]
getDefsForOld Sign f e
sSig [FORMULA f]
axioms
      opsPredsAndExAxioms :: [FORMULA f]
opsPredsAndExAxioms = [FORMULA f]
defsForOld [FORMULA f] -> [FORMULA f] -> [FORMULA f]
forall a. [a] -> [a] -> [a]
++ [FORMULA f]
exQuants [FORMULA f] -> [FORMULA f] -> [FORMULA f]
forall a. [a] -> [a] -> [a]
++ [FORMULA f]
memShips2
      conStatus :: Conservativity
conStatus = Conservativity -> [FORMULA f] -> Conservativity
forall f. Conservativity -> [FORMULA f] -> Conservativity
getConStatus Conservativity
dataStatus [FORMULA f]
opsPredsAndExAxioms
      memObl :: [FORMULA f]
memObl = Set SORT -> [(SORT, VAR_DECL, FORMULA f)] -> [FORMULA f]
forall f. Set SORT -> [(SORT, VAR_DECL, FORMULA f)] -> [FORMULA f]
infoSubsorts Set SORT
emptySorts [(SORT, VAR_DECL, FORMULA f)]
subsortDefns
      axGroup :: [[FORMULA f]]
axGroup = Sign f e -> [FORMULA f] -> [[FORMULA f]]
forall f e. GetRange f => Sign f e -> [FORMULA f] -> [[FORMULA f]]
groupAxioms Sign f e
sig [FORMULA f]
axLessDoms
      overLaps :: [FORMULA f]
overLaps = Sign f e -> [[FORMULA f]] -> [FORMULA f]
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e -> [[FORMULA f]] -> [FORMULA f]
getOverlapQuery Sign f e
sig [[FORMULA f]]
axGroup
      obligations :: [FORMULA f]
obligations = [FORMULA f]
opsPredsAndExAxioms [FORMULA f] -> [FORMULA f] -> [FORMULA f]
forall a. [a] -> [a] -> [a]
++ [FORMULA f]
memObl [FORMULA f] -> [FORMULA f] -> [FORMULA f]
forall a. [a] -> [a] -> [a]
++ [FORMULA f]
overLaps
      domSyms :: [OP_SYMB]
domSyms = [Either OP_SYMB PRED_SYMB] -> [OP_SYMB]
forall a b. [Either a b] -> [a]
lefts ([Either OP_SYMB PRED_SYMB] -> [OP_SYMB])
-> [Either OP_SYMB PRED_SYMB] -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$ (FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB))
-> [FORMULA f] -> [Either OP_SYMB PRED_SYMB]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
forall f.
GetRange f =>
FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
leadingSym [FORMULA f]
domains
      ms :: [Maybe (Result (Conservativity, [FORMULA f]))]
ms =
        [ Sign f e
-> [FORMULA f] -> Maybe (Result (Conservativity, [FORMULA f]))
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e
-> [FORMULA f] -> Maybe (Result (Conservativity, [FORMULA f]))
checkDefinitional Sign f e
sig [FORMULA f]
axioms
        , Bool
-> Set SORT
-> Set SORT
-> Set SORT
-> Set SORT
-> Set SORT
-> Sign f e
-> Sign f e
-> Maybe (Result (Conservativity, [FORMULA f]))
forall f e.
Bool
-> Set SORT
-> Set SORT
-> Set SORT
-> Set SORT
-> Set SORT
-> Sign f e
-> Sign f e
-> Maybe (Result (Conservativity, [FORMULA f]))
checkSort ([Named (FORMULA f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named (FORMULA f)]
axs) Set SORT
newSorts Set SORT
defSubsorts Set SORT
genSorts2 Set SORT
freeSorts
            Set SORT
nonInhabitedSorts Sign f e
sSig Sign f e
sig
        , Sign f e
-> [FORMULA f]
-> [OP_SYMB]
-> Maybe (Result (Conservativity, [FORMULA f]))
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e
-> [FORMULA f]
-> [OP_SYMB]
-> Maybe (Result (Conservativity, [FORMULA f]))
checkLeadingTerms Sign f e
sig [FORMULA f]
axioms [OP_SYMB]
cons
        , Sign f e
-> [FORMULA f]
-> [OP_SYMB]
-> [[FORMULA f]]
-> [OP_SYMB]
-> Maybe (Result (Conservativity, [FORMULA f]))
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e
-> [FORMULA f]
-> [OP_SYMB]
-> [[FORMULA f]]
-> [OP_SYMB]
-> Maybe (Result (Conservativity, [FORMULA f]))
checkIncomplete Sign f e
sig [FORMULA f]
obligations [OP_SYMB]
domSyms [[FORMULA f]]
axGroup [OP_SYMB]
cons ]
  Result (Conservativity, [FORMULA f])
r <- case [Maybe (Result (Conservativity, [FORMULA f]))]
-> [Result (Conservativity, [FORMULA f])]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Result (Conservativity, [FORMULA f]))]
ms of
    [] -> Sign f e
-> Conservativity
-> [FORMULA f]
-> [FORMULA f]
-> [FORMULA f]
-> IO (Result (Conservativity, [FORMULA f]))
forall f e.
(FormExtension f, TermExtension f, Ord f) =>
Sign f e
-> Conservativity
-> [FORMULA f]
-> [FORMULA f]
-> [FORMULA f]
-> IO (Result (Conservativity, [FORMULA f]))
checkTerminal Sign f e
sig Conservativity
conStatus [FORMULA f]
obligations [FORMULA f]
domains [FORMULA f]
axLessDoms
    a :: Result (Conservativity, [FORMULA f])
a : _ -> Result (Conservativity, [FORMULA f])
-> IO (Result (Conservativity, [FORMULA f]))
forall (m :: * -> *) a. Monad m => a -> m a
return Result (Conservativity, [FORMULA f])
a
  Result (Conservativity, [FORMULA f])
-> IO (Result (Conservativity, [FORMULA f]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Conservativity, [FORMULA f])
 -> IO (Result (Conservativity, [FORMULA f])))
-> Result (Conservativity, [FORMULA f])
-> IO (Result (Conservativity, [FORMULA f]))
forall a b. (a -> b) -> a -> b
$ case Result (Conservativity, [FORMULA f])
r of
    Result ds :: [Diagnosis]
ds Nothing ->
      case (Named (FORMULA f) -> Bool)
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Named (FORMULA f) -> Bool) -> Named (FORMULA f) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> Bool
forall f. FORMULA f -> Bool
checkPos (FORMULA f -> Bool)
-> (Named (FORMULA f) -> FORMULA f) -> Named (FORMULA f) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence) ([Named (FORMULA f)] -> [Named (FORMULA f)])
-> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a b. (a -> b) -> a -> b
$ [Named (FORMULA f)]
axs [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ [Named (FORMULA f)]
osens of
        [] -> (Conservativity, [FORMULA f])
-> [Char] -> Result (Conservativity, [FORMULA f])
forall a. a -> [Char] -> Result a
justHint (Conservativity
Cons, []) "theory is positive!"
        l :: [Named (FORMULA f)]
l -> let
          ps :: [Diagnosis]
ps = (Named (FORMULA f) -> Diagnosis)
-> [Named (FORMULA f)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (\ f :: Named (FORMULA f)
f -> DiagKind -> [Char] -> Range -> Diagnosis
Diag DiagKind
Hint ("formula is not positive:\n  "
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show (Named (FORMULA f) -> Doc
forall f. FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula (Named (FORMULA f) -> Doc) -> Named (FORMULA f) -> Doc
forall a b. (a -> b) -> a -> b
$ (FORMULA f -> FORMULA f) -> Named (FORMULA f) -> Named (FORMULA f)
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed (Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e -> FORMULA f -> FORMULA f
simplifyCASLSen Sign f e
sig) Named (FORMULA f)
f))
            (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ Named (FORMULA f) -> Range
forall a. GetRange a => a -> Range
getRange Named (FORMULA f)
f) ([Named (FORMULA f)] -> [Diagnosis])
-> [Named (FORMULA f)] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ Int -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. Int -> [a] -> [a]
take 2 [Named (FORMULA f)]
l
          in [Diagnosis]
-> Maybe (Conservativity, [FORMULA f])
-> Result (Conservativity, [FORMULA f])
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([Diagnosis]
ps [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
ds) Maybe (Conservativity, [FORMULA f])
forall a. Maybe a
Nothing
    _ -> Result (Conservativity, [FORMULA f])
r

{- | group the axioms according to their leading symbol,
output Nothing if there is some axiom in incorrect form -}
groupAxioms :: GetRange f => Sign f e -> [FORMULA f] -> [[FORMULA f]]
groupAxioms :: Sign f e -> [FORMULA f] -> [[FORMULA f]]
groupAxioms sig :: Sign f e
sig phis :: [FORMULA f]
phis = ([(Either OP_SYMB PRED_SYMB, FORMULA f)] -> [FORMULA f])
-> [[(Either OP_SYMB PRED_SYMB, FORMULA f)]] -> [[FORMULA f]]
forall a b. (a -> b) -> [a] -> [b]
map (((Either OP_SYMB PRED_SYMB, FORMULA f) -> FORMULA f)
-> [(Either OP_SYMB PRED_SYMB, FORMULA f)] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (Either OP_SYMB PRED_SYMB, FORMULA f) -> FORMULA f
forall a b. (a, b) -> b
snd)
   ([[(Either OP_SYMB PRED_SYMB, FORMULA f)]] -> [[FORMULA f]])
-> [[(Either OP_SYMB PRED_SYMB, FORMULA f)]] -> [[FORMULA f]]
forall a b. (a -> b) -> a -> b
$ ((Either OP_SYMB PRED_SYMB, FORMULA f)
 -> (Either OP_SYMB PRED_SYMB, FORMULA f) -> Bool)
-> [(Either OP_SYMB PRED_SYMB, FORMULA f)]
-> [[(Either OP_SYMB PRED_SYMB, FORMULA f)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
Rel.partList (\ (e1 :: Either OP_SYMB PRED_SYMB
e1, _) (e2 :: Either OP_SYMB PRED_SYMB
e2, _) -> case (Either OP_SYMB PRED_SYMB
e1, Either OP_SYMB PRED_SYMB
e2) of
       (Left o1 :: OP_SYMB
o1, Left 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
       (Right (Qual_pred_name p1 :: SORT
p1 t1 :: PRED_TYPE
t1 _), Right (Qual_pred_name p2 :: SORT
p2 t2 :: PRED_TYPE
t2 _)) ->
           SORT
p1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
p2 Bool -> Bool -> Bool
&& (PredType -> PredType -> Bool)
-> (PRED_TYPE -> PredType) -> PRED_TYPE -> PRED_TYPE -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on (Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP Sign f e
sig) PRED_TYPE -> PredType
toPredType PRED_TYPE
t1 PRED_TYPE
t2
       _ -> Bool
False)
   ([(Either OP_SYMB PRED_SYMB, FORMULA f)]
 -> [[(Either OP_SYMB PRED_SYMB, FORMULA f)]])
-> [(Either OP_SYMB PRED_SYMB, FORMULA f)]
-> [[(Either OP_SYMB PRED_SYMB, FORMULA f)]]
forall a b. (a -> b) -> a -> b
$ (FORMULA f
 -> [(Either OP_SYMB PRED_SYMB, FORMULA f)]
 -> [(Either OP_SYMB PRED_SYMB, FORMULA f)])
-> [(Either OP_SYMB PRED_SYMB, FORMULA f)]
-> [FORMULA f]
-> [(Either OP_SYMB PRED_SYMB, FORMULA f)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ f :: FORMULA f
f -> case FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
forall f.
GetRange f =>
FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
leadingSym FORMULA f
f of
    Just ei :: Either OP_SYMB PRED_SYMB
ei -> ((Either OP_SYMB PRED_SYMB
ei, FORMULA f
f) (Either OP_SYMB PRED_SYMB, FORMULA f)
-> [(Either OP_SYMB PRED_SYMB, FORMULA f)]
-> [(Either OP_SYMB PRED_SYMB, FORMULA f)]
forall a. a -> [a] -> [a]
:)
    Nothing -> [(Either OP_SYMB PRED_SYMB, FORMULA f)]
-> [(Either OP_SYMB PRED_SYMB, FORMULA f)]
forall a. a -> a
id) [] [FORMULA f]
phis

-- | return the non-constructor terms of arguments of a leading term
checkTerms :: Sign f e -> [OP_SYMB] -> [TERM f] -> [TERM f]
checkTerms :: Sign f e -> [OP_SYMB] -> [TERM f] -> [TERM f]
checkTerms sig :: Sign f e
sig cons :: [OP_SYMB]
cons = (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. TERM f -> [TERM f]
checkT
  where checkT :: TERM f -> [TERM f]
checkT t :: TERM f
t = case TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t of
          Qual_var {} -> []
          Application subop :: OP_SYMB
subop subts :: [TERM f]
subts _ ->
            if Sign f e -> [OP_SYMB] -> OP_SYMB -> Bool
forall f e. Sign f e -> [OP_SYMB] -> OP_SYMB -> Bool
isCons Sign f e
sig [OP_SYMB]
cons OP_SYMB
subop then (TERM f -> [TERM f]) -> [TERM f] -> [TERM f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TERM f -> [TERM f]
checkT [TERM f]
subts else [TERM f
t]
          _ -> [TERM f
t]

{- | check whether the operation symbol is a constructor
(or a related overloaded variant). -}
isCons :: Sign f e -> [OP_SYMB] -> OP_SYMB -> Bool
isCons :: Sign f e -> [OP_SYMB] -> OP_SYMB -> Bool
isCons sig :: Sign f e
sig cons :: [OP_SYMB]
cons os :: OP_SYMB
os = (OP_SYMB -> Bool) -> [OP_SYMB] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (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
os) [OP_SYMB]
cons

-- | create all possible pairs from a list
pairs :: [a] -> [(a, a)]
pairs :: [a] -> [(a, a)]
pairs ps :: [a]
ps = case [a]
ps of
  hd :: a
hd : tl :: [a]
tl@(_ : _) -> (a -> (a, a)) -> [a] -> [(a, a)]
forall a b. (a -> b) -> [a] -> [b]
map (\ x :: a
x -> (a
hd, a
x)) [a]
tl [(a, a)] -> [(a, a)] -> [(a, a)]
forall a. [a] -> [a] -> [a]
++ [a] -> [(a, a)]
forall a. [a] -> [(a, a)]
pairs [a]
tl
  _ -> []

-- | create the proof obligation for a pair of overlapped formulas
overlapQuery :: GetRange f => FORMULA f -> FORMULA f -> FORMULA f
overlapQuery :: FORMULA f -> FORMULA f -> FORMULA f
overlapQuery a1 :: FORMULA f
a1 a2 :: FORMULA f
a2 =
        case FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
forall f.
GetRange f =>
FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
leadingSym FORMULA f
a1 of
          Just (Left _)
            | FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a1 Bool -> Bool -> Bool
&& Bool -> Bool
not (FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a2) ->
                FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f
con1, FORMULA f
con2])
                            (FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
mkNeg (TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness TERM f
resT2 Range
nullRange))
            | FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a2 Bool -> Bool -> Bool
&& Bool -> Bool
not (FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a1) ->
                FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f
con1, FORMULA f
con2])
                            (FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
mkNeg (TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness TERM f
resT1 Range
nullRange))
            | FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a1 Bool -> Bool -> Bool
&& FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a2 -> FORMULA f
forall f. FORMULA f
trueForm
            | Bool
otherwise ->
                FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f
con1, FORMULA f
con2])
                            (TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM f
resT1 TERM f
resT2)
          Just (Right _)
            | FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a1 Bool -> Bool -> Bool
&& Bool -> Bool
not (FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a2) ->
                FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f
con1, FORMULA f
con2])
                            (FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
mkNeg FORMULA f
resA2)
            | FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a2 Bool -> Bool -> Bool
&& Bool -> Bool
not (FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a1) ->
                FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f
con1, FORMULA f
con2])
                            (FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
mkNeg FORMULA f
resA1)
            | FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a1 Bool -> Bool -> Bool
&& FORMULA f -> Bool
forall f. FORMULA f -> Bool
containNeg FORMULA f
a2 -> FORMULA f
forall f. FORMULA f
trueForm
            | Bool
otherwise ->
                FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f
con1, FORMULA f
con2])
                            ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f
resA1, FORMULA f
resA2])
          _ -> [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "CASL.CCC.FreeTypes.<overlapQuery>"
      where [con1 :: FORMULA f
con1, con2 :: FORMULA f
con2] = (FORMULA f -> FORMULA f) -> [FORMULA f] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
conditionAxiom [FORMULA f
a1, FORMULA f
a2]
            [resT1 :: TERM f
resT1, resT2 :: TERM f
resT2] = (FORMULA f -> TERM f) -> [FORMULA f] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA f -> TERM f
forall f. FORMULA f -> TERM f
resultTerm [FORMULA f
a1, FORMULA f
a2]
            [resA1 :: FORMULA f
resA1, resA2 :: FORMULA f
resA2] = (FORMULA f -> FORMULA f) -> [FORMULA f] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
resultAxiom [FORMULA f
a1, FORMULA f
a2]

getNotComplete :: (Ord f, FormExtension f, TermExtension f)
  => Sign f e -> [OP_SYMB] -> [[FORMULA f]] -> [OP_SYMB]
  -> [(Result [(String, FORMULA f)], [FORMULA f])]
getNotComplete :: Sign f e
-> [OP_SYMB]
-> [[FORMULA f]]
-> [OP_SYMB]
-> [(Result [([Char], FORMULA f)], [FORMULA f])]
getNotComplete sig :: Sign f e
sig doms :: [OP_SYMB]
doms fsn :: [[FORMULA f]]
fsn constructors :: [OP_SYMB]
constructors =
  let consMap :: MapSet SORT (SORT, OP_TYPE)
consMap = (OP_SYMB
 -> MapSet SORT (SORT, OP_TYPE) -> MapSet SORT (SORT, OP_TYPE))
-> MapSet SORT (SORT, OP_TYPE)
-> [OP_SYMB]
-> MapSet SORT (SORT, OP_TYPE)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (Qual_op_name o :: SORT
o ot :: OP_TYPE
ot _) ->
        SORT
-> (SORT, OP_TYPE)
-> MapSet SORT (SORT, OP_TYPE)
-> MapSet SORT (SORT, OP_TYPE)
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (OP_TYPE -> SORT
res_OP_TYPE OP_TYPE
ot) (SORT
o, OP_TYPE
ot)) MapSet SORT (SORT, OP_TYPE)
forall a b. MapSet a b
MapSet.empty [OP_SYMB]
constructors
      consMap2 :: MapSet SORT OP_TYPE
consMap2 = (OP_SYMB -> MapSet SORT OP_TYPE -> MapSet SORT OP_TYPE)
-> MapSet SORT OP_TYPE -> [OP_SYMB] -> MapSet SORT OP_TYPE
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (Qual_op_name o :: SORT
o ot :: OP_TYPE
ot _) ->
        SORT -> OP_TYPE -> MapSet SORT OP_TYPE -> MapSet SORT OP_TYPE
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
o OP_TYPE
ot) MapSet SORT OP_TYPE
forall a b. MapSet a b
MapSet.empty [OP_SYMB]
constructors
  in
  ((Result [([Char], FORMULA f)], [FORMULA f]) -> Bool)
-> [(Result [([Char], FORMULA f)], [FORMULA f])]
-> [(Result [([Char], FORMULA f)], [FORMULA f])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Result ds :: [Diagnosis]
ds mfs :: Maybe [([Char], FORMULA f)]
mfs, _) -> Bool -> Bool
not ([Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds)
      Bool -> Bool -> Bool
|| Bool
-> ([([Char], FORMULA f)] -> Bool)
-> Maybe [([Char], FORMULA f)]
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Bool -> Bool
not (Bool -> Bool)
-> ([([Char], FORMULA f)] -> Bool) -> [([Char], FORMULA f)] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [([Char], FORMULA f)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) Maybe [([Char], FORMULA f)]
mfs)
  ([(Result [([Char], FORMULA f)], [FORMULA f])]
 -> [(Result [([Char], FORMULA f)], [FORMULA f])])
-> [(Result [([Char], FORMULA f)], [FORMULA f])]
-> [(Result [([Char], FORMULA f)], [FORMULA f])]
forall a b. (a -> b) -> a -> b
$ ([FORMULA f] -> (Result [([Char], FORMULA f)], [FORMULA f]))
-> [[FORMULA f]] -> [(Result [([Char], FORMULA f)], [FORMULA f])]
forall a b. (a -> b) -> [a] -> [b]
map (\ g :: [FORMULA f]
g ->
         (let l :: [((SORT, Int), [TERM f])]
l = (FORMULA f -> ((SORT, Int), [TERM f]))
-> [FORMULA f] -> [((SORT, Int), [TERM f])]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA f -> ((SORT, Int), [TERM f])
forall f. FORMULA f -> ((SORT, Int), [TERM f])
topIdOfAxiom [FORMULA f]
g in
                  case Set (SORT, Int) -> [(SORT, Int)]
forall a. Set a -> [a]
Set.toList (Set (SORT, Int) -> [(SORT, Int)])
-> ([(SORT, Int)] -> Set (SORT, Int))
-> [(SORT, Int)]
-> [(SORT, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(SORT, Int)] -> Set (SORT, Int)
forall a. Ord a => [a] -> Set a
Set.fromList ([(SORT, Int)] -> [(SORT, Int)]) -> [(SORT, Int)] -> [(SORT, Int)]
forall a b. (a -> b) -> a -> b
$ (((SORT, Int), [TERM f]) -> (SORT, Int))
-> [((SORT, Int), [TERM f])] -> [(SORT, Int)]
forall a b. (a -> b) -> [a] -> [b]
map ((SORT, Int), [TERM f]) -> (SORT, Int)
forall a b. (a, b) -> a
fst [((SORT, Int), [TERM f])]
l of
                    [(p :: SORT
p, i :: Int
i)] -> Sign f e
-> [OP_SYMB]
-> MapSet SORT (SORT, OP_TYPE)
-> MapSet SORT OP_TYPE
-> (LeadArgs, [(FORMULA f, [TERM f])])
-> Result [([Char], FORMULA f)]
forall f e.
(Ord f, FormExtension f, TermExtension f) =>
Sign f e
-> [OP_SYMB]
-> MapSet SORT (SORT, OP_TYPE)
-> MapSet SORT OP_TYPE
-> (LeadArgs, [(FORMULA f, [TERM f])])
-> Result [([Char], FORMULA f)]
completePatterns Sign f e
sig [OP_SYMB]
doms MapSet SORT (SORT, OP_TYPE)
consMap MapSet SORT OP_TYPE
consMap2
                      ([(SORT -> [Char] -> [Char]
showId SORT
p "", Int
i)]
                      , [FORMULA f] -> [[TERM f]] -> [(FORMULA f, [TERM f])]
forall a b. [a] -> [b] -> [(a, b)]
zip [FORMULA f]
g ([[TERM f]] -> [(FORMULA f, [TERM f])])
-> [[TERM f]] -> [(FORMULA f, [TERM f])]
forall a b. (a -> b) -> a -> b
$ (((SORT, Int), [TERM f]) -> [TERM f])
-> [((SORT, Int), [TERM f])] -> [[TERM f]]
forall a b. (a -> b) -> [a] -> [b]
map ((SORT, Int), [TERM f]) -> [TERM f]
forall a b. (a, b) -> b
snd [((SORT, Int), [TERM f])]
l)
                    l2 :: [(SORT, Int)]
l2 -> [Char] -> Result [([Char], FORMULA f)]
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> Result [([Char], FORMULA f)])
-> [Char] -> Result [([Char], FORMULA f)]
forall a b. (a -> b) -> a -> b
$ "wrongly grouped leading terms "
                      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(SORT, Int)] -> [Char]
forall a. Show a => a -> [Char]
show [(SORT, Int)]
l2
         , [FORMULA f]
g)) [[FORMULA f]]
fsn

type LeadArgs = [(String, Int)]

getNextArg :: Bool -> String -> LeadArgs -> (Bool, String, LeadArgs)
getNextArg :: Bool -> [Char] -> LeadArgs -> (Bool, [Char], LeadArgs)
getNextArg b :: Bool
b p :: [Char]
p l :: LeadArgs
l = case LeadArgs
l of
  [] -> (Bool
False, if Bool
b then [Char]
p else "_", [])
  h :: ([Char], Int)
h : r :: LeadArgs
r -> case ([Char], Int)
h of
    (i :: [Char]
i, c :: Int
c) -> if Int
c Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then (Bool
b, [Char]
i, LeadArgs
r) else
      let (b1 :: Bool
b1, sl :: [[Char]]
sl, r2 :: LeadArgs
r2) = Int -> Bool -> [Char] -> LeadArgs -> (Bool, [[Char]], LeadArgs)
getNextN Int
c Bool
b [Char]
p LeadArgs
r
      in (Bool
b1, [Char]
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate ", " [[Char]]
sl [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ")", LeadArgs
r2)

getNextN :: Int -> Bool -> String -> LeadArgs -> (Bool, [String], LeadArgs)
getNextN :: Int -> Bool -> [Char] -> LeadArgs -> (Bool, [[Char]], LeadArgs)
getNextN c :: Int
c b :: Bool
b p :: [Char]
p l :: LeadArgs
l = if Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 then (Bool
b, [], LeadArgs
l) else
  let (b1 :: Bool
b1, s :: [Char]
s, r :: LeadArgs
r) = Bool -> [Char] -> LeadArgs -> (Bool, [Char], LeadArgs)
getNextArg Bool
b [Char]
p LeadArgs
l
      (b2 :: Bool
b2, sl :: [[Char]]
sl, r2 :: LeadArgs
r2) = Int -> Bool -> [Char] -> LeadArgs -> (Bool, [[Char]], LeadArgs)
getNextN (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Bool
b1 [Char]
p LeadArgs
r
  in (Bool
b2, [Char]
s [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [[Char]]
sl, LeadArgs
r2)

showLeadingArgs :: String -> LeadArgs -> String
showLeadingArgs :: [Char] -> LeadArgs -> [Char]
showLeadingArgs p :: [Char]
p l :: LeadArgs
l = let (_, r :: [Char]
r, _) = Bool -> [Char] -> LeadArgs -> (Bool, [Char], LeadArgs)
getNextArg Bool
True [Char]
p (LeadArgs -> (Bool, [Char], LeadArgs))
-> LeadArgs -> (Bool, [Char], LeadArgs)
forall a b. (a -> b) -> a -> b
$ LeadArgs -> LeadArgs
forall a. [a] -> [a]
reverse LeadArgs
l in [Char]
r

-- | check whether the patterns of a function or predicate are complete
completePatterns :: (Ord f, FormExtension f, TermExtension f) => Sign f e
  -> [OP_SYMB] -> MapSet.MapSet SORT (OP_NAME, OP_TYPE)
  -> MapSet.MapSet OP_NAME OP_TYPE
  -> (LeadArgs, [(FORMULA f, [TERM f])])
  -> Result [(String, FORMULA f)]
completePatterns :: Sign f e
-> [OP_SYMB]
-> MapSet SORT (SORT, OP_TYPE)
-> MapSet SORT OP_TYPE
-> (LeadArgs, [(FORMULA f, [TERM f])])
-> Result [([Char], FORMULA f)]
completePatterns tsig :: Sign f e
tsig doms :: [OP_SYMB]
doms consMap :: MapSet SORT (SORT, OP_TYPE)
consMap consMap2 :: MapSet SORT OP_TYPE
consMap2 (leadingArgs :: LeadArgs
leadingArgs, pas :: [(FORMULA f, [TERM f])]
pas)
    | ((FORMULA f, [TERM f]) -> Bool) -> [(FORMULA f, [TERM f])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([TERM f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TERM f] -> Bool)
-> ((FORMULA f, [TERM f]) -> [TERM f])
-> (FORMULA f, [TERM f])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f, [TERM f]) -> [TERM f]
forall a b. (a, b) -> b
snd) [(FORMULA f, [TERM f])]
pas =
       let fs :: [FORMULA f]
fs = Sign f e -> [OP_SYMB] -> [FORMULA f] -> [FORMULA f]
forall f e.
(Ord f, FormExtension f, TermExtension f) =>
Sign f e -> [OP_SYMB] -> [FORMULA f] -> [FORMULA f]
checkExhaustive Sign f e
tsig [OP_SYMB]
doms ([FORMULA f] -> [FORMULA f]) -> [FORMULA f] -> [FORMULA f]
forall a b. (a -> b) -> a -> b
$ ((FORMULA f, [TERM f]) -> FORMULA f)
-> [(FORMULA f, [TERM f])] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA f, [TERM f]) -> FORMULA f
forall a b. (a, b) -> a
fst [(FORMULA f, [TERM f])]
pas
       in [([Char], FORMULA f)] -> Result [([Char], FORMULA f)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([([Char], FORMULA f)] -> Result [([Char], FORMULA f)])
-> [([Char], FORMULA f)] -> Result [([Char], FORMULA f)]
forall a b. (a -> b) -> a -> b
$ (FORMULA f -> ([Char], FORMULA f))
-> [FORMULA f] -> [([Char], FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (\ f :: FORMULA f
f -> ([Char] -> LeadArgs -> [Char]
showLeadingArgs "" LeadArgs
leadingArgs, FORMULA f
f)) [FORMULA f]
fs
    | ((FORMULA f, [TERM f]) -> Bool) -> [(FORMULA f, [TERM f])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([TERM f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TERM f] -> Bool)
-> ((FORMULA f, [TERM f]) -> [TERM f])
-> (FORMULA f, [TERM f])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f, [TERM f]) -> [TERM f]
forall a b. (a, b) -> b
snd) [(FORMULA f, [TERM f])]
pas = [Char] -> Result [([Char], FORMULA f)]
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail "wrongly grouped leading terms"
    | Bool
otherwise = let hds :: [(FORMULA f, TERM f)]
hds = ((FORMULA f, [TERM f]) -> (FORMULA f, TERM f))
-> [(FORMULA f, [TERM f])] -> [(FORMULA f, TERM f)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (f :: FORMULA f
f, hd :: TERM f
hd : _) -> (FORMULA f
f, TERM f
hd)) [(FORMULA f, [TERM f])]
pas in
            if ((FORMULA f, TERM f) -> Bool) -> [(FORMULA f, TERM f)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TERM f -> Bool
forall t. TERM t -> Bool
isVar (TERM f -> Bool)
-> ((FORMULA f, TERM f) -> TERM f) -> (FORMULA f, TERM f) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA f, TERM f) -> TERM f
forall a b. (a, b) -> b
snd) [(FORMULA f, TERM f)]
hds
            then let
              tls :: [(FORMULA f, [TERM f])]
tls = ((FORMULA f, [TERM f]) -> (FORMULA f, [TERM f]))
-> [(FORMULA f, [TERM f])] -> [(FORMULA f, [TERM f])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (f :: FORMULA f
f, _ : tl :: [TERM f]
tl) -> (FORMULA f
f, [TERM f]
tl)) [(FORMULA f, [TERM f])]
pas
              in Sign f e
-> [OP_SYMB]
-> MapSet SORT (SORT, OP_TYPE)
-> MapSet SORT OP_TYPE
-> (LeadArgs, [(FORMULA f, [TERM f])])
-> Result [([Char], FORMULA f)]
forall f e.
(Ord f, FormExtension f, TermExtension f) =>
Sign f e
-> [OP_SYMB]
-> MapSet SORT (SORT, OP_TYPE)
-> MapSet SORT OP_TYPE
-> (LeadArgs, [(FORMULA f, [TERM f])])
-> Result [([Char], FORMULA f)]
completePatterns Sign f e
tsig [OP_SYMB]
doms MapSet SORT (SORT, OP_TYPE)
consMap MapSet SORT OP_TYPE
consMap2
                      (("_", 0) ([Char], Int) -> LeadArgs -> LeadArgs
forall a. a -> [a] -> [a]
: LeadArgs
leadingArgs, [(FORMULA f, [TERM f])]
tls)
            else let
              consAppls :: [(FORMULA f, SORT, Set OP_TYPE)]
consAppls@(_ : _) = ((FORMULA f, TERM f) -> Maybe (FORMULA f, SORT, Set OP_TYPE))
-> [(FORMULA f, TERM f)] -> [(FORMULA f, SORT, Set OP_TYPE)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\ (f :: FORMULA f
f, t :: TERM f
t) -> case TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
t of
                Application (Qual_op_name o :: SORT
o ot :: OP_TYPE
ot _) _ _ ->
                  (FORMULA f, SORT, Set OP_TYPE)
-> Maybe (FORMULA f, SORT, Set OP_TYPE)
forall a. a -> Maybe a
Just (FORMULA f
f, SORT
o, (OP_TYPE -> Bool) -> Set OP_TYPE -> Set OP_TYPE
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Sign f e -> OP_TYPE -> OP_TYPE -> Bool
forall f e. Sign f e -> OP_TYPE -> OP_TYPE -> Bool
sameOpTypes Sign f e
tsig OP_TYPE
ot)
                    (Set OP_TYPE -> Set OP_TYPE) -> Set OP_TYPE -> Set OP_TYPE
forall a b. (a -> b) -> a -> b
$ SORT -> MapSet SORT OP_TYPE -> Set OP_TYPE
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
o MapSet SORT OP_TYPE
consMap2)
                _ -> Maybe (FORMULA f, SORT, Set OP_TYPE)
forall a. Maybe a
Nothing) [(FORMULA f, TERM f)]
hds
              consSrt :: Set SORT
consSrt = (Set SORT -> Set SORT -> Set SORT) -> [Set SORT] -> Set SORT
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Set SORT -> Set SORT -> Set SORT
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ ((FORMULA f, SORT, Set OP_TYPE) -> Set SORT)
-> [(FORMULA f, SORT, Set OP_TYPE)] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, _, os :: Set OP_TYPE
os) -> (OP_TYPE -> SORT) -> Set OP_TYPE -> Set SORT
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map OP_TYPE -> SORT
res_OP_TYPE Set OP_TYPE
os) [(FORMULA f, SORT, Set OP_TYPE)]
consAppls
              in case (SORT -> Bool) -> [SORT] -> [SORT]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (SORT -> Bool) -> SORT -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (SORT, OP_TYPE) -> Bool
forall a. Set a -> Bool
Set.null (Set (SORT, OP_TYPE) -> Bool)
-> (SORT -> Set (SORT, OP_TYPE)) -> SORT -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT -> MapSet SORT (SORT, OP_TYPE) -> Set (SORT, OP_TYPE)
forall a b. Ord a => a -> MapSet a b -> Set b
`MapSet.lookup` MapSet SORT (SORT, OP_TYPE)
consMap))
                     ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
consSrt of
                  [] -> [Char] -> Result [([Char], FORMULA f)]
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> Result [([Char], FORMULA f)])
-> [Char] -> Result [([Char], FORMULA f)]
forall a b. (a -> b) -> a -> b
$
                    "no common result type for constructors found: "
                       [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [TERM f] -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc (((FORMULA f, TERM f) -> TERM f)
-> [(FORMULA f, TERM f)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA f, TERM f) -> TERM f
forall a b. (a, b) -> b
snd [(FORMULA f, TERM f)]
hds) ""
                  cSrt :: SORT
cSrt : _ -> do
                    let allCons :: Set (SORT, OP_TYPE)
allCons = SORT -> MapSet SORT (SORT, OP_TYPE) -> Set (SORT, OP_TYPE)
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
cSrt MapSet SORT (SORT, OP_TYPE)
consMap
                    Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Set (SORT, OP_TYPE) -> Bool
forall a. Set a -> Bool
Set.null Set (SORT, OP_TYPE)
allCons) (Result () -> Result ())
-> ([Char] -> Result ()) -> [Char] -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Result ()
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail
                      ([Char] -> Result ()) -> [Char] -> Result ()
forall a b. (a -> b) -> a -> b
$ "no constructors for result type found: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show SORT
cSrt
                    let cons_group :: [(SORT, OP_TYPE, [(FORMULA f, [TERM f])])]
cons_group = ((SORT, OP_TYPE) -> (SORT, OP_TYPE, [(FORMULA f, [TERM f])]))
-> [(SORT, OP_TYPE)] -> [(SORT, OP_TYPE, [(FORMULA f, [TERM f])])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (c :: SORT
c, ct :: OP_TYPE
ct) -> (SORT
c, OP_TYPE
ct,
                          ((FORMULA f, [TERM f]) -> Bool)
-> [(FORMULA f, [TERM f])] -> [(FORMULA f, [TERM f])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, h :: TERM f
h : _) -> case TERM f -> TERM f
forall f. TERM f -> TERM f
unsortedTerm TERM f
h of
                            Application (Qual_op_name o :: SORT
o ot :: OP_TYPE
ot _) _ _ ->
                              SORT
c SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
o Bool -> Bool -> Bool
&& Sign f e -> OP_TYPE -> OP_TYPE -> Bool
forall f e. Sign f e -> OP_TYPE -> OP_TYPE -> Bool
sameOpTypes Sign f e
tsig OP_TYPE
ct OP_TYPE
ot
                            _ -> Bool
False) [(FORMULA f, [TERM f])]
pas)) ([(SORT, OP_TYPE)] -> [(SORT, OP_TYPE, [(FORMULA f, [TERM f])])])
-> [(SORT, OP_TYPE)] -> [(SORT, OP_TYPE, [(FORMULA f, [TERM f])])]
forall a b. (a -> b) -> a -> b
$ Set (SORT, OP_TYPE) -> [(SORT, OP_TYPE)]
forall a. Set a -> [a]
Set.toList Set (SORT, OP_TYPE)
allCons
                        vars :: [(FORMULA f, [TERM f])]
vars = ((FORMULA f, [TERM f]) -> Bool)
-> [(FORMULA f, [TERM f])] -> [(FORMULA f, [TERM f])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, h :: TERM f
h : _) -> TERM f -> Bool
forall t. TERM t -> Bool
isVar TERM f
h) [(FORMULA f, [TERM f])]
pas
                    [[([Char], FORMULA f)]]
ffs <- ((SORT, OP_TYPE, [(FORMULA f, [TERM f])])
 -> Result [([Char], FORMULA f)])
-> [(SORT, OP_TYPE, [(FORMULA f, [TERM f])])]
-> Result [[([Char], FORMULA f)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ f :: (SORT, OP_TYPE, [(FORMULA f, [TERM f])])
f -> LeadArgs
-> [(FORMULA f, [TERM f])]
-> (SORT, OP_TYPE, [(FORMULA f, [TERM f])])
-> Result (LeadArgs, [(FORMULA f, [TERM f])])
forall f.
(Ord f, FormExtension f, TermExtension f) =>
LeadArgs
-> [(FORMULA f, [TERM f])]
-> (SORT, OP_TYPE, [(FORMULA f, [TERM f])])
-> Result (LeadArgs, [(FORMULA f, [TERM f])])
checkConstructor LeadArgs
leadingArgs [(FORMULA f, [TERM f])]
vars (SORT, OP_TYPE, [(FORMULA f, [TERM f])])
f
                        Result (LeadArgs, [(FORMULA f, [TERM f])])
-> ((LeadArgs, [(FORMULA f, [TERM f])])
    -> Result [([Char], FORMULA f)])
-> Result [([Char], FORMULA f)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Sign f e
-> [OP_SYMB]
-> MapSet SORT (SORT, OP_TYPE)
-> MapSet SORT OP_TYPE
-> (LeadArgs, [(FORMULA f, [TERM f])])
-> Result [([Char], FORMULA f)]
forall f e.
(Ord f, FormExtension f, TermExtension f) =>
Sign f e
-> [OP_SYMB]
-> MapSet SORT (SORT, OP_TYPE)
-> MapSet SORT OP_TYPE
-> (LeadArgs, [(FORMULA f, [TERM f])])
-> Result [([Char], FORMULA f)]
completePatterns Sign f e
tsig [OP_SYMB]
doms MapSet SORT (SORT, OP_TYPE)
consMap MapSet SORT OP_TYPE
consMap2)
                      [(SORT, OP_TYPE, [(FORMULA f, [TERM f])])]
cons_group
                    [([Char], FORMULA f)] -> Result [([Char], FORMULA f)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([([Char], FORMULA f)] -> Result [([Char], FORMULA f)])
-> [([Char], FORMULA f)] -> Result [([Char], FORMULA f)]
forall a b. (a -> b) -> a -> b
$ [[([Char], FORMULA f)]] -> [([Char], FORMULA f)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[([Char], FORMULA f)]]
ffs

mkVars :: [SORT] -> [TERM f]
mkVars :: [SORT] -> [TERM f]
mkVars = (Int -> SORT -> TERM f) -> [Int] -> [SORT] -> [TERM f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ i :: Int
i -> VAR -> SORT -> TERM f
forall f. VAR -> SORT -> TERM f
mkVarTerm ([Char] -> VAR
mkSimpleId ([Char] -> VAR) -> [Char] -> VAR
forall a b. (a -> b) -> a -> b
$ 'c' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)) [1 :: Int ..]

checkConstructor :: (Ord f, FormExtension f, TermExtension f)
  => LeadArgs -> [(FORMULA f, [TERM f])]
  -> (Id, OP_TYPE, [(FORMULA f, [TERM f])])
  -> Result (LeadArgs, [(FORMULA f, [TERM f])])
checkConstructor :: LeadArgs
-> [(FORMULA f, [TERM f])]
-> (SORT, OP_TYPE, [(FORMULA f, [TERM f])])
-> Result (LeadArgs, [(FORMULA f, [TERM f])])
checkConstructor leadingArgs :: LeadArgs
leadingArgs vars :: [(FORMULA f, [TERM f])]
vars (c :: SORT
c, ct :: OP_TYPE
ct, es :: [(FORMULA f, [TERM f])]
es) = do
  let args :: [SORT]
args = OP_TYPE -> [SORT]
args_OP_TYPE OP_TYPE
ct
      nL :: LeadArgs
nL = (SORT -> [Char] -> [Char]
showId SORT
c "", [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SORT]
args) ([Char], Int) -> LeadArgs -> LeadArgs
forall a. a -> [a] -> [a]
: LeadArgs
leadingArgs
      varEqs :: [(FORMULA f, [TERM f])]
varEqs = ((FORMULA f, [TERM f]) -> (FORMULA f, [TERM f]))
-> [(FORMULA f, [TERM f])] -> [(FORMULA f, [TERM f])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (f :: FORMULA f
f, _ : t :: [TERM f]
t) -> (FORMULA f
f, [SORT] -> [TERM f]
forall f. [SORT] -> [TERM f]
mkVars [SORT]
args [TERM f] -> [TERM f] -> [TERM f]
forall a. [a] -> [a] -> [a]
++ [TERM f]
t)) [(FORMULA f, [TERM f])]
vars
      pat :: [Char]
pat = [Char] -> LeadArgs -> [Char]
showLeadingArgs
           (SORT -> [Char] -> [Char]
showId SORT
c "" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ case [SORT]
args of
             [] -> ""
             l :: [SORT]
l -> "(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate "," ((SORT -> [Char]) -> [SORT] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> SORT -> [Char]
forall a b. a -> b -> a
const "_") [SORT]
l) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ")")
           LeadArgs
leadingArgs
  case [(FORMULA f, [TERM f])]
es of
    [] -> do
      Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(FORMULA f, [TERM f])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(FORMULA f, [TERM f])]
vars) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> [Char] -> Result ()
forall a. a -> [Char] -> Result a
justWarn ()
         ([Char] -> Result ()) -> [Char] -> Result ()
forall a b. (a -> b) -> a -> b
$ "missing pattern for: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
pat
      (LeadArgs, [(FORMULA f, [TERM f])])
-> Result (LeadArgs, [(FORMULA f, [TERM f])])
forall (m :: * -> *) a. Monad m => a -> m a
return (LeadArgs
nL, [(FORMULA f, [TERM f])]
varEqs)
    _ ->
      (LeadArgs, [(FORMULA f, [TERM f])])
-> Result (LeadArgs, [(FORMULA f, [TERM f])])
forall (m :: * -> *) a. Monad m => a -> m a
return (LeadArgs
nL, [(FORMULA f, [TERM f])]
varEqs [(FORMULA f, [TERM f])]
-> [(FORMULA f, [TERM f])] -> [(FORMULA f, [TERM f])]
forall a. [a] -> [a] -> [a]
++ ((FORMULA f, [TERM f]) -> (FORMULA f, [TERM f]))
-> [(FORMULA f, [TERM f])] -> [(FORMULA f, [TERM f])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (f :: FORMULA f
f, h :: TERM f
h : t :: [TERM f]
t) -> (FORMULA f
f, TERM f -> [TERM f]
forall f. TERM f -> [TERM f]
arguOfTerm TERM f
h [TERM f] -> [TERM f] -> [TERM f]
forall a. [a] -> [a] -> [a]
++ [TERM f]
t)) [(FORMULA f, [TERM f])]
es)

-- | get condition axiom without matching definedness condition
getCond :: (GetRange f, Eq f) => Sign f e -> [OP_SYMB] -> FORMULA f -> FORMULA f
getCond :: Sign f e -> [OP_SYMB] -> FORMULA f -> FORMULA f
getCond sig :: Sign f e
sig doms :: [OP_SYMB]
doms f :: FORMULA f
f =
  let (cs :: [FORMULA f]
cs, e :: FORMULA f
e) = FORMULA f -> ([FORMULA f], FORMULA f)
forall f. FORMULA f -> ([FORMULA f], FORMULA f)
splitAxiom FORMULA f
f
  in [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct ([FORMULA f] -> FORMULA f) -> [FORMULA f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ (FORMULA f -> Bool) -> [FORMULA f] -> [FORMULA f]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ c :: FORMULA f
c -> case FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
forall f.
GetRange f =>
FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
leadingTermPredication FORMULA f
e of
       l :: Maybe (Either (TERM f) (FORMULA f))
l@(Just (Left (Application os :: OP_SYMB
os _ _)))
         | (OP_SYMB -> Bool) -> [OP_SYMB] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (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
os) [OP_SYMB]
doms
         -> case FORMULA f
c of  -- pattern term must be identical
              Definedness {} | FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
forall f.
GetRange f =>
FORMULA f -> Maybe (Either (TERM f) (FORMULA f))
leadingTermPredication FORMULA f
c Maybe (Either (TERM f) (FORMULA f))
-> Maybe (Either (TERM f) (FORMULA f)) -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe (Either (TERM f) (FORMULA f))
l -> Bool
False
              _ -> Bool
True
       _ -> Bool
True) [FORMULA f]
cs

checkExhaustive :: (Ord f, FormExtension f, TermExtension f)
  => Sign f e -> [OP_SYMB] -> [FORMULA f] -> [FORMULA f]
checkExhaustive :: Sign f e -> [OP_SYMB] -> [FORMULA f] -> [FORMULA f]
checkExhaustive sig :: Sign f e
sig doms :: [OP_SYMB]
doms es :: [FORMULA f]
es = case [FORMULA f]
es of
  f1 :: FORMULA f
f1 : rs :: [FORMULA f]
rs ->
    let sfs :: [(Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
  FORMULA f)]
sfs = (FORMULA f
 -> (Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
     FORMULA f))
-> [FORMULA f]
-> [(Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
     FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (\ f :: FORMULA f
f -> (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 FORMULA f
f1 FORMULA f
f, FORMULA f
f)) [FORMULA f]
rs
        overlap :: [(Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
  FORMULA f)]
overlap = ((Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
  FORMULA f)
 -> Bool)
-> [(Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
     FORMULA f)]
-> [(Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
     FORMULA f)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])) -> Bool)
-> ((Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
     FORMULA f)
    -> Maybe ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])))
-> (Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
    FORMULA f)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> Maybe ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall a. Result a -> Maybe a
maybeResult (Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
 -> Maybe ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])))
-> ((Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
     FORMULA f)
    -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])))
-> (Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
    FORMULA f)
-> Maybe ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
 FORMULA f)
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
forall a b. (a, b) -> a
fst) [(Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
  FORMULA f)]
sfs
        simpAndQuant :: FORMULA f -> FORMULA f
simpAndQuant = Sign f e -> FORMULA f -> FORMULA f
forall f e. TermExtension f => Sign f e -> FORMULA f -> FORMULA f
quant Sign f e
sig (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> FORMULA f -> FORMULA f
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula f -> f
forall a. a -> a
id
    in case [(Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
  FORMULA f)]
overlap of
       [] -> (FORMULA f -> Bool) -> [FORMULA f] -> [FORMULA f]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (FORMULA f -> Bool) -> FORMULA f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> Bool
forall f. FORMULA f -> Bool
is_True_atom)
          ((FORMULA f -> FORMULA f) -> [FORMULA f] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA f -> FORMULA f
simpAndQuant (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> [OP_SYMB] -> FORMULA f -> FORMULA f
forall f e.
(GetRange f, Eq f) =>
Sign f e -> [OP_SYMB] -> FORMULA f -> FORMULA f
getCond Sign f e
sig [OP_SYMB]
doms) [FORMULA f
f1])
          [FORMULA f] -> [FORMULA f] -> [FORMULA f]
forall a. [a] -> [a] -> [a]
++ Sign f e -> [OP_SYMB] -> [FORMULA f] -> [FORMULA f]
forall f e.
(Ord f, FormExtension f, TermExtension f) =>
Sign f e -> [OP_SYMB] -> [FORMULA f] -> [FORMULA f]
checkExhaustive Sign f e
sig [OP_SYMB]
doms [FORMULA f]
rs
       (r :: Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
r, f2 :: FORMULA f
f2) : rrs :: [(Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
  FORMULA f)]
rrs -> let
          (f3 :: FORMULA f
f3, f4 :: FORMULA f
f4, ((s3 :: Subst f
s3, _), (s4 :: Subst f
s4, _))) = Sign f e
-> FORMULA f
-> FORMULA f
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> (FORMULA f, FORMULA f,
    ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])))
forall f e.
(TermExtension f, FormExtension f, Ord f) =>
Sign f e
-> FORMULA f
-> FORMULA f
-> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
-> (FORMULA f, FORMULA f,
    ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])))
convert2Forms Sign f e
sig FORMULA f
f1 FORMULA f
f2 Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
r
          in Sign f e -> [OP_SYMB] -> [FORMULA f] -> [FORMULA f]
forall f e.
(Ord f, FormExtension f, TermExtension f) =>
Sign f e -> [OP_SYMB] -> [FORMULA f] -> [FORMULA f]
checkExhaustive Sign f e
sig [OP_SYMB]
doms
         ([FORMULA f] -> [FORMULA f]) -> [FORMULA f] -> [FORMULA f]
forall a b. (a -> b) -> a -> b
$ (FORMULA f -> FORMULA f
simpAndQuant
         (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
mkImpl ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
disjunct [ Subst f -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Subst f -> (f -> f) -> FORMULA f -> FORMULA f
replaceVarsF Subst f
s3 f -> f
forall a. a -> a
id (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Sign f e -> [OP_SYMB] -> FORMULA f -> FORMULA f
forall f e.
(GetRange f, Eq f) =>
Sign f e -> [OP_SYMB] -> FORMULA f -> FORMULA f
getCond Sign f e
sig [OP_SYMB]
doms FORMULA f
f3
                            , Subst f -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Subst f -> (f -> f) -> FORMULA f -> FORMULA f
replaceVarsF Subst f
s4 f -> f
forall a. a -> a
id (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Sign f e -> [OP_SYMB] -> FORMULA f -> FORMULA f
forall f e.
(GetRange f, Eq f) =>
Sign f e -> [OP_SYMB] -> FORMULA f -> FORMULA f
getCond Sign f e
sig [OP_SYMB]
doms FORMULA f
f4 ])
           (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst f -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Subst f -> (f -> f) -> FORMULA f -> FORMULA f
replaceVarsF Subst f
s3 f -> f
forall a. a -> a
id (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
restAxiom FORMULA f
f3) FORMULA f -> [FORMULA f] -> [FORMULA f]
forall a. a -> [a] -> [a]
: ((Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
  FORMULA f)
 -> FORMULA f)
-> [(Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
     FORMULA f)]
-> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
 FORMULA f)
-> FORMULA f
forall a b. (a, b) -> b
snd [(Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])),
  FORMULA f)]
rrs
  [] -> []