{- |

    Module      :  ./CASL/CCC/OnePoint.hs
    Description :  Check for truth in one-point model
    Copyright   :  (c) Mingyi Liu and Till Mossakowski and Uni Bremen 2004
    License     :  GPLv2 or higher, see LICENSE.txt

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

Check for truth in one-point model
   with all predicates true, all functions total

-}

module CASL.CCC.OnePoint where

import CASL.AS_Basic_CASL
import CASL.Morphism (Morphism, imageOfMorphism)
import CASL.Sign (Sign, predMap, sortSet, supersortsOf, toPredType)

import Data.Maybe
import qualified Data.Set as Set

import qualified Common.Lib.MapSet as MapSet

{-
We use a three valued logic to evaluate a formula in a one-point expansion
of an unknown arbitrary model. This means that for new sorts and new predicates,
every equation and predicate application holds, but for the old sorts and
predicates, we do not know anything. The three valued logic is represented
with Maybe Bool. It has the following meaning:

         Nothing      * = unknown
         Just True    True
         Jast False   False

The connectives are as follows:

and t f *
t   t f *
f   f f f
*   * f *

or  t f *
t   t t t
f   t f *
*   t * *

implies t f *
t       t f *
f       t t t
*       t * *

equivalent t f *
t          t f *
f          f t *
*          * * *

not t f *
    f t *

(this is just Kleene's strong three-valued logic)
-}

evaluateOnePoint :: Morphism f e m -> [FORMULA f] -> Maybe Bool
evaluateOnePoint :: Morphism f e m -> [FORMULA f] -> Maybe Bool
evaluateOnePoint m :: Morphism f e m
m fs :: [FORMULA f]
fs =
     let p :: [Maybe Bool]
p = (FORMULA f -> Maybe Bool) -> [FORMULA f] -> [Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Sign f e -> FORMULA f -> Maybe Bool
forall f e. Sign f e -> FORMULA f -> Maybe Bool
evaluateOnePointFORMULA (Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
imageOfMorphism Morphism f e m
m)) [FORMULA f]
fs
     in if Maybe Bool -> [Maybe Bool] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False) [Maybe Bool]
p then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
        else if Maybe Bool -> [Maybe Bool] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Maybe Bool
forall a. Maybe a
Nothing [Maybe Bool]
p then Maybe Bool
forall a. Maybe a
Nothing
                               else Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True

{-
evaluateOnePoint :: Morphism f e m-> [FORMULA f] -> Maybe Bool
evaluateOnePoint m fs = do
     p <- mapM (evaluateOnePointFORMULA (imageOfMorphism m)) fs
     return (all id p)
-}


evaluateOnePointFORMULA :: Sign f e -> FORMULA f -> Maybe Bool
evaluateOnePointFORMULA :: Sign f e -> FORMULA f -> Maybe Bool
evaluateOnePointFORMULA sig :: Sign f e
sig (Quantification _ _ f :: FORMULA f
f _) =
                      Sign f e -> FORMULA f -> Maybe Bool
forall f e. Sign f e -> FORMULA f -> Maybe Bool
evaluateOnePointFORMULA Sign f e
sig FORMULA f
f

evaluateOnePointFORMULA sig :: Sign f e
sig (Junction j :: Junctor
j fs :: [FORMULA f]
fs _) =
      let p :: [Maybe Bool]
p = (FORMULA f -> Maybe Bool) -> [FORMULA f] -> [Maybe Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Sign f e -> FORMULA f -> Maybe Bool
forall f e. Sign f e -> FORMULA f -> Maybe Bool
evaluateOnePointFORMULA Sign f e
sig) [FORMULA f]
fs
          b :: Bool
b = Junctor
j Junctor -> Junctor -> Bool
forall a. Eq a => a -> a -> Bool
== Junctor
Dis
      in if Maybe Bool -> [Maybe Bool] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b) [Maybe Bool]
p then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b
         else if Maybe Bool -> [Maybe Bool] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Maybe Bool
forall a. Maybe a
Nothing [Maybe Bool]
p then Maybe Bool
forall a. Maybe a
Nothing
                                else Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b

evaluateOnePointFORMULA sig :: Sign f e
sig (Relation f1 :: FORMULA f
f1 c :: Relation
c f2 :: FORMULA f
f2 _) =
         let p1 :: Maybe Bool
p1 = Sign f e -> FORMULA f -> Maybe Bool
forall f e. Sign f e -> FORMULA f -> Maybe Bool
evaluateOnePointFORMULA Sign f e
sig FORMULA f
f1
             p2 :: Maybe Bool
p2 = Sign f e -> FORMULA f -> Maybe Bool
forall f e. Sign f e -> FORMULA f -> Maybe Bool
evaluateOnePointFORMULA Sign f e
sig FORMULA f
f2
         in case Relation
c of
         Equivalence -> if Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Bool
p1 Bool -> Bool -> Bool
|| Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Bool
p2 then Maybe Bool
forall a. Maybe a
Nothing
              else Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Maybe Bool
p1 Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Bool
p2
         _ | Maybe Bool
p1 Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False Bool -> Bool -> Bool
|| Maybe Bool
p2 Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
           | Maybe Bool
p1 Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Bool -> Bool -> Bool
&& Maybe Bool
p2 Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
           | Bool
otherwise -> Maybe Bool
forall a. Maybe a
Nothing

evaluateOnePointFORMULA sig :: Sign f e
sig (Negation f :: FORMULA f
f _) =
      (Bool -> Bool) -> Maybe Bool -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (Maybe Bool -> Maybe Bool) -> Maybe Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Sign f e -> FORMULA f -> Maybe Bool
forall f e. Sign f e -> FORMULA f -> Maybe Bool
evaluateOnePointFORMULA Sign f e
sig FORMULA f
f

evaluateOnePointFORMULA _ (Atom b :: Bool
b _) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b

evaluateOnePointFORMULA sig :: Sign f e
sig (Predication pred_symb :: PRED_SYMB
pred_symb _ _) =
     case PRED_SYMB
pred_symb of
       Pred_name _ -> Maybe Bool
forall a. Maybe a
Nothing
       Qual_pred_name pname :: PRED_NAME
pname ptype :: PRED_TYPE
ptype _ ->
           if PRED_NAME -> PredType -> MapSet PRED_NAME PredType -> Bool
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> Bool
MapSet.member PRED_NAME
pname (PRED_TYPE -> PredType
toPredType PRED_TYPE
ptype) (Sign f e -> MapSet PRED_NAME PredType
forall f e. Sign f e -> MapSet PRED_NAME PredType
predMap Sign f e
sig)
           then Maybe Bool
forall a. Maybe a
Nothing
           else Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True

evaluateOnePointFORMULA sig :: Sign f e
sig (Definedness (Sorted_term _ sort :: PRED_NAME
sort _) _) =
      if PRED_NAME -> Set PRED_NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PRED_NAME
sort (Sign f e -> Set PRED_NAME
forall f e. Sign f e -> Set PRED_NAME
sortSet Sign f e
sig) then Maybe Bool
forall a. Maybe a
Nothing else Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True

evaluateOnePointFORMULA sig :: Sign f e
sig (Equation (Sorted_term _ sort1 :: PRED_NAME
sort1 _) _
    (Sorted_term _ sort2 :: PRED_NAME
sort2 _) _) =
        if Bool -> Bool
not (PRED_NAME -> Set PRED_NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PRED_NAME
sort1 (Sign f e -> Set PRED_NAME
forall f e. Sign f e -> Set PRED_NAME
sortSet Sign f e
sig))
             Bool -> Bool -> Bool
&& Bool -> Bool
not (PRED_NAME -> Set PRED_NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PRED_NAME
sort2 (Sign f e -> Set PRED_NAME
forall f e. Sign f e -> Set PRED_NAME
sortSet Sign f e
sig)) then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
        else Maybe Bool
forall a. Maybe a
Nothing

-- todo: auch pruefen, ob Sorte von t in sortSet sig
evaluateOnePointFORMULA sig :: Sign f e
sig (Membership (Sorted_term _ sort1 :: PRED_NAME
sort1 _) sort2 :: PRED_NAME
sort2 _) =
        if Bool -> Bool
not (PRED_NAME -> Set PRED_NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PRED_NAME
sort1 (Sign f e -> Set PRED_NAME
forall f e. Sign f e -> Set PRED_NAME
sortSet Sign f e
sig))
             Bool -> Bool -> Bool
&& Bool -> Bool
not (PRED_NAME -> Set PRED_NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PRED_NAME
sort2 (Sign f e -> Set PRED_NAME
forall f e. Sign f e -> Set PRED_NAME
sortSet Sign f e
sig)) then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
        else Maybe Bool
forall a. Maybe a
Nothing

evaluateOnePointFORMULA _ (Mixfix_formula _) = [Char] -> Maybe Bool
forall a. HasCallStack => [Char] -> a
error "Fehler Mixfix_formula"

evaluateOnePointFORMULA _ (Unparsed_formula _ _) = [Char] -> Maybe Bool
forall a. HasCallStack => [Char] -> a
error
                                                  "Fehler Unparsed_formula"

{-
         compute recover_Sort_gen_ax constr, get (srts,ops,maps)
         check whether all srts are "new" (not in the image of the morphism)
         check whether for all s in srts, there is a term,
           using variables of sorts outside srts
           using operation symbols from ops
         Algorithm:
         construct a list L of "inhabited" sorts
         initially, the list L is empty
         iteration step:
           for each operation symbol in ops, such that
              all argument sorts (opArgs)
                 are either in the list L or are outside srts
              add the results sort (opRes) to the list L of inhabited sorts
         start with initial list, and iterate until iteration is stable
         check whether srts is a sublist of the list resulting from the
         iteration
-}

evaluateOnePointFORMULA sig :: Sign f e
sig (Sort_gen_ax constrs :: [Constraint]
constrs _) =
      let (srts :: [PRED_NAME]
srts, ops :: [OP_SYMB]
ops, _) = [Constraint] -> ([PRED_NAME], [OP_SYMB], [(PRED_NAME, PRED_NAME)])
recover_Sort_gen_ax [Constraint]
constrs
          sorts :: Set PRED_NAME
sorts = Sign f e -> Set PRED_NAME
forall f e. Sign f e -> Set PRED_NAME
sortSet Sign f e
sig
          argsAndres :: [([PRED_NAME], PRED_NAME)]
argsAndres = (OP_SYMB -> [([PRED_NAME], PRED_NAME)])
-> [OP_SYMB] -> [([PRED_NAME], PRED_NAME)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ os :: OP_SYMB
os -> case OP_SYMB
os of
              Op_name _ -> []
              Qual_op_name _ (Op_type _ args :: [PRED_NAME]
args res :: PRED_NAME
res _) _ -> [([PRED_NAME]
args, PRED_NAME
res)]) [OP_SYMB]
ops
          iterateInhabited :: [PRED_NAME] -> [PRED_NAME]
iterateInhabited l :: [PRED_NAME]
l =
              if [PRED_NAME]
l [PRED_NAME] -> [PRED_NAME] -> Bool
forall a. Eq a => a -> a -> Bool
== [PRED_NAME]
newL then [PRED_NAME]
newL else [PRED_NAME] -> [PRED_NAME]
iterateInhabited [PRED_NAME]
newL
                  where newL :: [PRED_NAME]
newL = (([PRED_NAME], PRED_NAME) -> [PRED_NAME] -> [PRED_NAME])
-> [PRED_NAME] -> [([PRED_NAME], PRED_NAME)] -> [PRED_NAME]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (as :: [PRED_NAME]
as, rs :: PRED_NAME
rs) l' :: [PRED_NAME]
l' ->
                                          if (PRED_NAME -> Bool) -> [PRED_NAME] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (PRED_NAME -> [PRED_NAME] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PRED_NAME]
l') [PRED_NAME]
as
                                                 Bool -> Bool -> Bool
&& PRED_NAME -> [PRED_NAME] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem PRED_NAME
rs [PRED_NAME]
l'
                                          then PRED_NAME
rs PRED_NAME -> [PRED_NAME] -> [PRED_NAME]
forall a. a -> [a] -> [a]
: [PRED_NAME]
l'
                                          else [PRED_NAME]
l') [PRED_NAME]
l [([PRED_NAME], PRED_NAME)]
argsAndres
    -- inhabited = iterateInhabited []
          inhabited :: [PRED_NAME]
inhabited = [PRED_NAME] -> [PRED_NAME]
iterateInhabited ([PRED_NAME] -> [PRED_NAME]) -> [PRED_NAME] -> [PRED_NAME]
forall a b. (a -> b) -> a -> b
$ Set PRED_NAME -> [PRED_NAME]
forall a. Set a -> [a]
Set.toList Set PRED_NAME
sorts
      in if (PRED_NAME -> Bool) -> [PRED_NAME] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PRED_NAME -> Set PRED_NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set PRED_NAME
sorts) [PRED_NAME]
srts then Maybe Bool
forall a. Maybe a
Nothing
         else if (PRED_NAME -> Bool) -> [PRED_NAME] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (PRED_NAME -> [PRED_NAME] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PRED_NAME]
inhabited) [PRED_NAME]
srts then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
              else Maybe Bool
forall a. Maybe a
Nothing

evaluateOnePointFORMULA _ (ExtFORMULA _) = [Char] -> Maybe Bool
forall a. HasCallStack => [Char] -> a
error "Fehler ExtFORMULA"

evaluateOnePointFORMULA _ _ = [Char] -> Maybe Bool
forall a. HasCallStack => [Char] -> a
error "Fehler" -- or Just False

-- | Test whether a signature morphism adds new supersorts
addsNewSupersorts :: Morphism f e m -> Bool
addsNewSupersorts :: Morphism f e m -> Bool
addsNewSupersorts m :: Morphism f e m
m =
    (PRED_NAME -> Bool) -> [PRED_NAME] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ s :: PRED_NAME
s -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set PRED_NAME -> Set PRED_NAME -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (PRED_NAME -> Set PRED_NAME -> Set PRED_NAME
forall a. Ord a => a -> Set a -> Set a
Set.insert PRED_NAME
s (Set PRED_NAME -> Set PRED_NAME) -> Set PRED_NAME -> Set PRED_NAME
forall a b. (a -> b) -> a -> b
$ PRED_NAME -> Sign f e -> Set PRED_NAME
forall f e. PRED_NAME -> Sign f e -> Set PRED_NAME
supersortsOf PRED_NAME
s Sign f e
sig) Set PRED_NAME
sorts)
       ([PRED_NAME] -> Bool) -> [PRED_NAME] -> Bool
forall a b. (a -> b) -> a -> b
$ Set PRED_NAME -> [PRED_NAME]
forall a. Set a -> [a]
Set.toList Set PRED_NAME
sorts
       where sig :: Sign f e
sig = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
imageOfMorphism Morphism f e m
m
             sorts :: Set PRED_NAME
sorts = Sign f e -> Set PRED_NAME
forall f e. Sign f e -> Set PRED_NAME
sortSet Sign f e
sig
{-
check: is there a sort not in the image of the morphism, that is
simultaneously s supersort of a sort that  is in the image.

e.g.
go through all sorts in the image
for each such sort s, comupte supersortsOf s
test whether a supersort is not in the image
if there is such a sort (i.e. supersort not in the image), then return True
otherwise, return False
-}