{- |
Module      :  ./CASL/Utils.hs
Description :  Utilities for CASL and its comorphisms
Copyright   :  (c) Klaus Luettich and Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt

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

Utilities for CASL and its comorphisms

-}

module CASL.Utils where

import Data.Maybe
import Data.List

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

import Common.Id

import CASL.AS_Basic_CASL
import CASL.Fold

type Subst f = Map.Map VAR (TERM f)

-- | specialized delete that deletes all shadowed variables
deleteVMap :: [VAR_DECL] -> Subst f -> Subst f
deleteVMap :: [VAR_DECL] -> Subst f -> Subst f
deleteVMap vDecls :: [VAR_DECL]
vDecls m :: Subst f
m = (VAR -> Subst f -> Subst f) -> Subst f -> [VAR] -> Subst f
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr VAR -> Subst f -> Subst f
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Subst f
m
  ([VAR] -> Subst f) -> [VAR] -> Subst f
forall a b. (a -> b) -> a -> b
$ (VAR_DECL -> [VAR]) -> [VAR_DECL] -> [VAR]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Var_decl vs :: [VAR]
vs _ _) -> [VAR]
vs) [VAR_DECL]
vDecls

replaceVarsRec :: Subst f -> (f -> f) -> Record f (FORMULA f) (TERM f)
replaceVarsRec :: Subst f -> (f -> f) -> Record f (FORMULA f) (TERM f)
replaceVarsRec m :: Subst f
m mf :: f -> f
mf = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
mf)
     { foldQual_var :: TERM f -> VAR -> SORT -> Range -> TERM f
foldQual_var = \ qv :: TERM f
qv v :: VAR
v _ _ ->
           TERM f -> Maybe (TERM f) -> TERM f
forall a. a -> Maybe a -> a
fromMaybe TERM f
qv (Maybe (TERM f) -> TERM f) -> Maybe (TERM f) -> TERM f
forall a b. (a -> b) -> a -> b
$ VAR -> Subst f -> Maybe (TERM f)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VAR
v Subst f
m
     , foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
foldQuantification = \ orig :: FORMULA f
orig _ _ _ _ ->
               let Quantification q :: QUANTIFIER
q vs :: [VAR_DECL]
vs f :: FORMULA f
f ps :: Range
ps = FORMULA f
orig
                   nm :: Subst f
nm = [VAR_DECL] -> Subst f -> Subst f
forall f. [VAR_DECL] -> Subst f -> Subst f
deleteVMap [VAR_DECL]
vs Subst f
m
               in QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vs (Subst f -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Subst f -> (f -> f) -> FORMULA f -> FORMULA f
replaceVarsF Subst f
nm f -> f
mf FORMULA f
f) Range
ps
     }

{- | replaceVars replaces all Qual_var occurences that are supposed
to be replaced according to the Subst -}
replaceVarsF :: Subst f
             -> (f -> f)
             -- ^ this function replaces Qual_var in ExtFORMULA
             -> FORMULA f -> FORMULA f
replaceVarsF :: Subst f -> (f -> f) -> FORMULA f -> FORMULA f
replaceVarsF m :: Subst f
m = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst f -> (f -> f) -> Record f (FORMULA f) (TERM f)
forall f. Subst f -> (f -> f) -> Record f (FORMULA f) (TERM f)
replaceVarsRec Subst f
m

{- | buildVMap constructs a mapping between a list of old variables and
corresponding fresh variables based on two lists of VAR_DECL -}
buildVMap :: [VAR_DECL] -> [VAR_DECL] -> Subst f
buildVMap :: [VAR_DECL] -> [VAR_DECL] -> Subst f
buildVMap vDecls :: [VAR_DECL]
vDecls fVDecls :: [VAR_DECL]
fVDecls =
    [(VAR, TERM f)] -> Subst f
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([[(VAR, TERM f)]] -> [(VAR, TERM f)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((VAR_DECL -> VAR_DECL -> [(VAR, TERM f)])
-> [VAR_DECL] -> [VAR_DECL] -> [[(VAR, TERM f)]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VAR_DECL -> VAR_DECL -> [(VAR, TERM f)]
forall f. VAR_DECL -> VAR_DECL -> [(VAR, TERM f)]
toTups [VAR_DECL]
vDecls [VAR_DECL]
fVDecls))
    where toTups :: VAR_DECL -> VAR_DECL -> [(VAR, TERM f)]
toTups (Var_decl vars1 :: [VAR]
vars1 sor1 :: SORT
sor1 _) (Var_decl vars2 :: [VAR]
vars2 sor2 :: SORT
sor2 _) =
            if SORT
sor1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
sor2 then (VAR -> VAR -> (VAR, TERM f)) -> [VAR] -> [VAR] -> [(VAR, TERM f)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SORT -> VAR -> VAR -> (VAR, TERM f)
forall a f. SORT -> a -> VAR -> (a, TERM f)
toTup SORT
sor1) [VAR]
vars1 [VAR]
vars2
            else [Char] -> [(VAR, TERM f)]
forall a. HasCallStack => [Char] -> a
error "CASL.Utils.buildVMap"
          toTup :: SORT -> a -> VAR -> (a, TERM f)
toTup s :: SORT
s v1 :: a
v1 v2 :: VAR
v2 = (a
v1, VAR -> SORT -> TERM f
forall f. VAR -> SORT -> TERM f
mkVarTerm VAR
v2 SORT
s)

codeOutUniqueRecord :: (f -> f) -> (f -> f) -> Record f (FORMULA f) (TERM f)
codeOutUniqueRecord :: (f -> f) -> (f -> f) -> Record f (FORMULA f) (TERM f)
codeOutUniqueRecord rf :: f -> f
rf mf :: f -> f
mf = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
mf)
    { foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
foldQuantification = \ _ q :: QUANTIFIER
q vDecl :: [VAR_DECL]
vDecl f' :: FORMULA f
f' ps :: Range
ps ->
         case QUANTIFIER
q of
         Unique_existential -> let
            eqForms :: VAR_DECL -> VAR_DECL -> [FORMULA f]
eqForms (Var_decl vars1 :: [VAR]
vars1 sor1 :: SORT
sor1 _) (Var_decl vars2 :: [VAR]
vars2 sor2 :: SORT
sor2 _) =
              if SORT
sor1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
sor2 then (VAR -> VAR -> FORMULA f) -> [VAR] -> [VAR] -> [FORMULA f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SORT -> VAR -> VAR -> FORMULA f
forall f. SORT -> VAR -> VAR -> FORMULA f
eqFor SORT
sor1) [VAR]
vars1 [VAR]
vars2
              else [Char] -> [FORMULA f]
forall a. HasCallStack => [Char] -> a
error "codeOutUniqueRecord1"
            eqFor :: SORT -> VAR -> VAR -> FORMULA f
eqFor s :: SORT
s v1 :: VAR
v1 v2 :: VAR
v2 = TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (VAR -> SORT -> TERM f
forall f. VAR -> SORT -> TERM f
mkVarTerm VAR
v1 SORT
s) (VAR -> SORT -> TERM f
forall f. VAR -> SORT -> TERM f
mkVarTerm VAR
v2 SORT
s)
            {- freshVars produces new variables based on a list
            of defined variables
            args: (1) set of already used variable names
            (2) list of variables -}
            freshVars :: Set VAR -> [VAR_DECL] -> (Set VAR, [VAR_DECL])
freshVars = (Set VAR -> VAR_DECL -> (Set VAR, VAR_DECL))
-> Set VAR -> [VAR_DECL] -> (Set VAR, [VAR_DECL])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL Set VAR -> VAR_DECL -> (Set VAR, VAR_DECL)
freshVar
            freshVar :: Set VAR -> VAR_DECL -> (Set VAR, VAR_DECL)
freshVar accSet :: Set VAR
accSet (Var_decl vars :: [VAR]
vars sor :: SORT
sor _) =
              let accSet' :: Set VAR
accSet' = Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union ([VAR] -> Set VAR
forall a. Ord a => [a] -> Set a
Set.fromList [VAR]
vars) Set VAR
accSet
                  (accSet'' :: Set VAR
accSet'', vars' :: [VAR]
vars') = (Set VAR -> VAR -> (Set VAR, VAR))
-> Set VAR -> [VAR] -> (Set VAR, [VAR])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL Set VAR -> VAR -> (Set VAR, VAR)
nVar Set VAR
accSet' [VAR]
vars
              in (Set VAR
accSet'', [VAR] -> SORT -> Range -> VAR_DECL
Var_decl [VAR]
vars' SORT
sor Range
nullRange)
            genVar :: VAR -> a -> VAR
genVar t :: VAR
t i :: a
i = [Char] -> VAR
mkSimpleId ([Char] -> VAR) -> [Char] -> VAR
forall a b. (a -> b) -> a -> b
$ VAR -> [Char]
tokStr VAR
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ '_' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: a -> [Char]
forall a. Show a => a -> [Char]
show a
i
            nVar :: Set VAR -> VAR -> (Set VAR, VAR)
nVar aSet :: Set VAR
aSet v :: VAR
v =
              let v' :: VAR
v' = Maybe VAR -> VAR
forall a. HasCallStack => Maybe a -> a
fromJust ((VAR -> Bool) -> [VAR] -> Maybe VAR
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Bool -> Bool
not (Bool -> Bool) -> (VAR -> Bool) -> VAR -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VAR -> Set VAR -> Bool) -> Set VAR -> VAR -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip VAR -> Set VAR -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set VAR
aSet)
                                 [VAR -> Int -> VAR
forall a. Show a => VAR -> a -> VAR
genVar VAR
v (Int
i :: Int) | Int
i <- [1 ..]])
              in (VAR -> Set VAR -> Set VAR
forall a. Ord a => a -> Set a -> Set a
Set.insert VAR
v' Set VAR
aSet, VAR
v')
            (vSet' :: Set VAR
vSet', vDecl' :: [VAR_DECL]
vDecl') = Set VAR -> [VAR_DECL] -> (Set VAR, [VAR_DECL])
freshVars Set VAR
forall a. Set a
Set.empty [VAR_DECL]
vDecl
            (_vSet'' :: Set VAR
_vSet'', vDecl'' :: [VAR_DECL]
vDecl'') = Set VAR -> [VAR_DECL] -> (Set VAR, [VAR_DECL])
freshVars Set VAR
vSet' [VAR_DECL]
vDecl
            f'_rep_x :: FORMULA f
f'_rep_x = Subst f -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Subst f -> (f -> f) -> FORMULA f -> FORMULA f
replaceVarsF ([VAR_DECL] -> [VAR_DECL] -> Subst f
forall f. [VAR_DECL] -> [VAR_DECL] -> Subst f
buildVMap [VAR_DECL]
vDecl [VAR_DECL]
vDecl') f -> f
rf FORMULA f
f'
            f'_rep_y :: FORMULA f
f'_rep_y = Subst f -> (f -> f) -> FORMULA f -> FORMULA f
forall f. Subst f -> (f -> f) -> FORMULA f -> FORMULA f
replaceVarsF ([VAR_DECL] -> [VAR_DECL] -> Subst f
forall f. [VAR_DECL] -> [VAR_DECL] -> Subst f
buildVMap [VAR_DECL]
vDecl [VAR_DECL]
vDecl'') f -> f
rf FORMULA f
f'
            allForm :: FORMULA f
allForm = [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange ([VAR_DECL]
vDecl' [VAR_DECL] -> [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a] -> [a]
++ [VAR_DECL]
vDecl'')
                        (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
f'_rep_x, FORMULA f
f'_rep_y])
                              FORMULA f
forall f. FORMULA f
implForm) Range
ps
            implForm :: FORMULA f
implForm = [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]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((VAR_DECL -> VAR_DECL -> [FORMULA f])
-> [VAR_DECL] -> [VAR_DECL] -> [[FORMULA f]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VAR_DECL -> VAR_DECL -> [FORMULA f]
forall f. VAR_DECL -> VAR_DECL -> [FORMULA f]
eqForms [VAR_DECL]
vDecl' [VAR_DECL]
vDecl'')
            in Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con
                   [QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Existential [VAR_DECL]
vDecl FORMULA f
f' Range
ps,
                    FORMULA f
allForm] Range
ps
         _ -> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vDecl FORMULA f
f' Range
ps
    }

{- | codeOutUniqueExtF compiles every unique_existential quantification
to simple quantifications. It works recursively through the whole
formula and only touches Unique_existential quantifications:
exists! x . phi(x) ==>
(exists x. phi(x)) /\ (forall x,y . phi(x) /\ phi(y) => x=y) -}
codeOutUniqueExtF :: (f -> f)
                  -- ^ this function replaces Qual_var in ExtFORMULA
                  -> (f -> f)
                  -- ^ codes out Unique_existential in ExtFORMULA
                  -> FORMULA f -> FORMULA f
codeOutUniqueExtF :: (f -> f) -> (f -> f) -> FORMULA f -> FORMULA f
codeOutUniqueExtF rf :: f -> f
rf = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> (f -> f) -> Record f (FORMULA f) (TERM f)
forall f. (f -> f) -> (f -> f) -> Record f (FORMULA f) (TERM f)
codeOutUniqueRecord f -> f
rf

codeOutCondRecord :: (Eq f) => (f -> f)
                  -> Record f (FORMULA f) (TERM f)
codeOutCondRecord :: (f -> f) -> Record f (FORMULA f) (TERM f)
codeOutCondRecord fun :: f -> f
fun =
    ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
fun)
          { foldPredication :: FORMULA f -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
foldPredication = \ phi :: FORMULA f
phi _ _ _ ->
                    (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f)
-> Either (FORMULA f) (FORMULA f)
-> FORMULA f
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((f -> f) -> FORMULA f -> FORMULA f
forall f. Eq f => (f -> f) -> FORMULA f -> FORMULA f
codeOutConditionalF f -> f
fun) FORMULA f -> FORMULA f
forall a. a -> a
id
                               (FORMULA f -> Either (FORMULA f) (FORMULA f)
forall f. Eq f => FORMULA f -> Either (FORMULA f) (FORMULA f)
codeOutCondPredication FORMULA f
phi)
          , foldEquation :: FORMULA f -> TERM f -> Equality -> TERM f -> Range -> FORMULA f
foldEquation = \ o :: FORMULA f
o _ _ _ _ ->
                let Equation t1 :: TERM f
t1 e :: Equality
e t2 :: TERM f
t2 ps :: Range
ps = FORMULA f
o in
                  (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f)
-> Either (FORMULA f) (FORMULA f)
-> FORMULA f
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((f -> f) -> FORMULA f -> FORMULA f
forall f. Eq f => (f -> f) -> FORMULA f -> FORMULA f
codeOutConditionalF f -> f
fun) FORMULA f -> FORMULA f
forall a. a -> a
id
                    ((TERM f -> TERM f -> Range -> FORMULA f)
-> TERM f -> TERM f -> Range -> Either (FORMULA f) (FORMULA f)
forall f.
Eq f =>
(TERM f -> TERM f -> Range -> FORMULA f)
-> TERM f -> TERM f -> Range -> Either (FORMULA f) (FORMULA f)
mkEquationAtom (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
`Equation` Equality
e) TERM f
t1 TERM f
t2 Range
ps)
          , foldMembership :: FORMULA f -> TERM f -> SORT -> Range -> FORMULA f
foldMembership = \ o :: FORMULA f
o _ _ _ ->
                let Membership t :: TERM f
t s :: SORT
s ps :: Range
ps = FORMULA f
o in
                  (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f)
-> Either (FORMULA f) (FORMULA f)
-> FORMULA f
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((f -> f) -> FORMULA f -> FORMULA f
forall f. Eq f => (f -> f) -> FORMULA f -> FORMULA f
codeOutConditionalF f -> f
fun) FORMULA f -> FORMULA f
forall a. a -> a
id
                    ((TERM f -> Range -> FORMULA f)
-> TERM f -> Range -> Either (FORMULA f) (FORMULA f)
forall f.
Eq f =>
(TERM f -> Range -> FORMULA f)
-> TERM f -> Range -> Either (FORMULA f) (FORMULA f)
mkSingleTermF (TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
`Membership` SORT
s) TERM f
t Range
ps)
          , foldDefinedness :: FORMULA f -> TERM f -> Range -> FORMULA f
foldDefinedness = \ o :: FORMULA f
o _ _ ->
                let Definedness t :: TERM f
t ps :: Range
ps = FORMULA f
o in
                  (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f)
-> Either (FORMULA f) (FORMULA f)
-> FORMULA f
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((f -> f) -> FORMULA f -> FORMULA f
forall f. Eq f => (f -> f) -> FORMULA f -> FORMULA f
codeOutConditionalF f -> f
fun) FORMULA f -> FORMULA f
forall a. a -> a
id
                    ((TERM f -> Range -> FORMULA f)
-> TERM f -> Range -> Either (FORMULA f) (FORMULA f)
forall f.
Eq f =>
(TERM f -> Range -> FORMULA f)
-> TERM f -> Range -> Either (FORMULA f) (FORMULA f)
mkSingleTermF TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness TERM f
t Range
ps)
          }

codeOutCondPredication :: (Eq f) => FORMULA f
                   -> Either (FORMULA f) (FORMULA f)
                   {- ^ Left means check again for Conditional,
                   Right means no Conditional left -}
codeOutCondPredication :: FORMULA f -> Either (FORMULA f) (FORMULA f)
codeOutCondPredication phi :: FORMULA f
phi@(Predication _ ts :: [TERM f]
ts _) =
    Either (FORMULA f) (FORMULA f)
-> (TERM f -> Either (FORMULA f) (FORMULA f))
-> Maybe (TERM f)
-> Either (FORMULA f) (FORMULA f)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (FORMULA f -> Either (FORMULA f) (FORMULA f)
forall a b. b -> Either a b
Right FORMULA f
phi) (FORMULA f -> Either (FORMULA f) (FORMULA f)
forall a b. a -> Either a b
Left (FORMULA f -> Either (FORMULA f) (FORMULA f))
-> (TERM f -> FORMULA f)
-> TERM f
-> Either (FORMULA f) (FORMULA f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> TERM f -> FORMULA f
forall f. Eq f => FORMULA f -> TERM f -> FORMULA f
constructExpansion FORMULA f
phi)
          (Maybe (TERM f) -> Either (FORMULA f) (FORMULA f))
-> Maybe (TERM f) -> Either (FORMULA f) (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [TERM f] -> Maybe (TERM f)
forall a. [a] -> Maybe a
listToMaybe ([TERM f] -> Maybe (TERM f)) -> [TERM f] -> Maybe (TERM f)
forall a b. (a -> b) -> a -> b
$ (TERM f -> Maybe (TERM f)) -> [TERM f] -> [TERM f]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TERM f -> Maybe (TERM f)
forall f. TERM f -> Maybe (TERM f)
findConditionalT [TERM f]
ts
codeOutCondPredication _ = [Char] -> Either (FORMULA f) (FORMULA f)
forall a. HasCallStack => [Char] -> a
error "CASL.Utils: Predication expected"

constructExpansion :: (Eq f) => FORMULA f
                   -> TERM f
                   -> FORMULA f
constructExpansion :: FORMULA f -> TERM f -> FORMULA f
constructExpansion atom :: FORMULA f
atom c :: TERM f
c@(Conditional t1 :: TERM f
t1 phi :: FORMULA f
phi t2 :: TERM f
t2 ps :: Range
ps) =
    Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [ FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation FORMULA f
phi Relation
Implication (TERM f -> TERM f -> FORMULA f -> FORMULA f
forall f. Eq f => TERM f -> TERM f -> FORMULA f -> FORMULA f
substConditionalF TERM f
c TERM f
t1 FORMULA f
atom) Range
ps
                 , FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation FORMULA f
phi Range
ps) Relation
Implication
                              (TERM f -> TERM f -> FORMULA f -> FORMULA f
forall f. Eq f => TERM f -> TERM f -> FORMULA f -> FORMULA f
substConditionalF TERM f
c TERM f
t2 FORMULA f
atom) Range
ps] Range
ps
constructExpansion _ _ = [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "CASL.Utils: Conditional expected"

mkEquationAtom :: (Eq f) => (TERM f -> TERM f -> Range -> FORMULA f)
               -- ^ equational constructor
               -> TERM f -> TERM f -> Range
               -> Either (FORMULA f) (FORMULA f)
               {- ^ Left means check again for Conditional,
               Right means no Conditional left -}
mkEquationAtom :: (TERM f -> TERM f -> Range -> FORMULA f)
-> TERM f -> TERM f -> Range -> Either (FORMULA f) (FORMULA f)
mkEquationAtom cons :: TERM f -> TERM f -> Range -> FORMULA f
cons t1 :: TERM f
t1 t2 :: TERM f
t2 ps :: Range
ps =
    Either (FORMULA f) (FORMULA f)
-> (TERM f -> Either (FORMULA f) (FORMULA f))
-> Maybe (TERM f)
-> Either (FORMULA f) (FORMULA f)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (FORMULA f -> Either (FORMULA f) (FORMULA f)
forall a b. b -> Either a b
Right FORMULA f
phi) (FORMULA f -> Either (FORMULA f) (FORMULA f)
forall a b. a -> Either a b
Left (FORMULA f -> Either (FORMULA f) (FORMULA f))
-> (TERM f -> FORMULA f)
-> TERM f
-> Either (FORMULA f) (FORMULA f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> TERM f -> FORMULA f
forall f. Eq f => FORMULA f -> TERM f -> FORMULA f
constructExpansion FORMULA f
phi)
          (Maybe (TERM f) -> Either (FORMULA f) (FORMULA f))
-> Maybe (TERM f) -> Either (FORMULA f) (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [TERM f] -> Maybe (TERM f)
forall a. [a] -> Maybe a
listToMaybe ([TERM f] -> Maybe (TERM f)) -> [TERM f] -> Maybe (TERM f)
forall a b. (a -> b) -> a -> b
$ (TERM f -> Maybe (TERM f)) -> [TERM f] -> [TERM f]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TERM f -> Maybe (TERM f)
forall f. TERM f -> Maybe (TERM f)
findConditionalT [TERM f
t1, TERM f
t2]
    where phi :: FORMULA f
phi = TERM f -> TERM f -> Range -> FORMULA f
cons TERM f
t1 TERM f
t2 Range
ps

mkSingleTermF :: (Eq f) => (TERM f -> Range -> FORMULA f)
              -- ^ single term atom constructor
               -> TERM f -> Range
               -> Either (FORMULA f) (FORMULA f)
               {- ^ Left means check again for Conditional,
               Right means no Conditional left -}
mkSingleTermF :: (TERM f -> Range -> FORMULA f)
-> TERM f -> Range -> Either (FORMULA f) (FORMULA f)
mkSingleTermF cons :: TERM f -> Range -> FORMULA f
cons t :: TERM f
t ps :: Range
ps =
    Either (FORMULA f) (FORMULA f)
-> (TERM f -> Either (FORMULA f) (FORMULA f))
-> Maybe (TERM f)
-> Either (FORMULA f) (FORMULA f)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (FORMULA f -> Either (FORMULA f) (FORMULA f)
forall a b. b -> Either a b
Right FORMULA f
phi) (FORMULA f -> Either (FORMULA f) (FORMULA f)
forall a b. a -> Either a b
Left (FORMULA f -> Either (FORMULA f) (FORMULA f))
-> (TERM f -> FORMULA f)
-> TERM f
-> Either (FORMULA f) (FORMULA f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA f -> TERM f -> FORMULA f
forall f. Eq f => FORMULA f -> TERM f -> FORMULA f
constructExpansion FORMULA f
phi)
          (TERM f -> Maybe (TERM f)
forall f. TERM f -> Maybe (TERM f)
findConditionalT TERM f
t)
    where phi :: FORMULA f
phi = TERM f -> Range -> FORMULA f
cons TERM f
t Range
ps

{- |
'codeOutConditionalF' implemented via 'CASL.Fold.foldFormula'

at each atom with a term find first (most left,no recursion into
   terms within it) Conditional term and report it (findConditionalT)

substitute the original atom with the conjunction of the already
   encoded atoms and already encoded formula

encoded atoms are the result of the substition (substConditionalF)
   of the Conditional term with each result term of the Conditional
   term plus recusion of codingOutConditionalF

encoded formulas are the result of codingOutConditionalF

expansion of conditionals according to CASL-Ref-Manual:
\'@A[T1 when F else T2]@\' expands to
\'@(A[T1] if F) /\\ (A[T2] if not F)@\'
-}
codeOutConditionalF :: (Eq f) =>
                       (f -> f)
                    -> FORMULA f -> FORMULA f
codeOutConditionalF :: (f -> f) -> FORMULA f -> FORMULA f
codeOutConditionalF = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> Record f (FORMULA f) (TERM f)
forall f. Eq f => (f -> f) -> Record f (FORMULA f) (TERM f)
codeOutCondRecord

findConditionalRecord :: Record f (Maybe (TERM f)) (Maybe (TERM f))
findConditionalRecord :: Record f (Maybe (TERM f)) (Maybe (TERM f))
findConditionalRecord =
    ((f -> Maybe (TERM f))
-> ([Maybe (TERM f)] -> Maybe (TERM f))
-> Maybe (TERM f)
-> Record f (Maybe (TERM f)) (Maybe (TERM f))
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord ([Char] -> f -> Maybe (TERM f)
forall a. HasCallStack => [Char] -> a
error "findConditionalRecord")
     ([TERM f] -> Maybe (TERM f)
forall a. [a] -> Maybe a
listToMaybe ([TERM f] -> Maybe (TERM f))
-> ([Maybe (TERM f)] -> [TERM f])
-> [Maybe (TERM f)]
-> Maybe (TERM f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (TERM f)] -> [TERM f]
forall a. [Maybe a] -> [a]
catMaybes) Maybe (TERM f)
forall a. Maybe a
Nothing)
    { foldConditional :: TERM f
-> Maybe (TERM f)
-> Maybe (TERM f)
-> Maybe (TERM f)
-> Range
-> Maybe (TERM f)
foldConditional = \ cond :: TERM f
cond _ _ _ _ -> TERM f -> Maybe (TERM f)
forall a. a -> Maybe a
Just TERM f
cond }

findConditionalT :: TERM f -> Maybe (TERM f)
findConditionalT :: TERM f -> Maybe (TERM f)
findConditionalT =
    (FORMULA f -> Maybe (TERM f))
-> Record f (Maybe (TERM f)) (Maybe (TERM f))
-> TERM f
-> Maybe (TERM f)
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm ([Char] -> FORMULA f -> Maybe (TERM f)
forall a. HasCallStack => [Char] -> a
error "findConditionalT") Record f (Maybe (TERM f)) (Maybe (TERM f))
forall f. Record f (Maybe (TERM f)) (Maybe (TERM f))
findConditionalRecord

substConditionalRecord :: (Eq f)
                       => TERM f -- ^ Conditional to search for
                       -> TERM f -- ^ newly inserted term
                       -> Record f (FORMULA f) (TERM f)
substConditionalRecord :: TERM f -> TERM f -> Record f (FORMULA f) (TERM f)
substConditionalRecord c :: TERM f
c t :: TERM f
t = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
forall a. a -> a
id)
     { foldConditional :: TERM f -> TERM f -> FORMULA f -> TERM f -> Range -> TERM f
foldConditional = \ c1 :: TERM f
c1 _ _ _ _ ->
       {- FIXME: correct implementation would use an equality
       which checks for correct positions also! -}
             if TERM f
c1 TERM f -> TERM f -> Bool
forall a. Eq a => a -> a -> Bool
== TERM f
c then TERM f
t else TERM f
c1
     }

substConditionalF :: (Eq f)
                  => TERM f -- ^ Conditional to search for
                  -> TERM f -- ^ newly inserted term
                  -> FORMULA f -> FORMULA f
substConditionalF :: TERM f -> TERM f -> FORMULA f -> FORMULA f
substConditionalF c :: TERM f
c = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> (TERM f -> Record f (FORMULA f) (TERM f))
-> TERM f
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TERM f -> TERM f -> Record f (FORMULA f) (TERM f)
forall f. Eq f => TERM f -> TERM f -> Record f (FORMULA f) (TERM f)
substConditionalRecord TERM f
c

{- |
  Subsitute predications with strong equation if it is equivalent to.
-}
eqSubstRecord :: Set.Set PRED_SYMB -- ^ equivalent predicates
              -> (f -> f) -> Record f (FORMULA f) (TERM f)
eqSubstRecord :: Set PRED_SYMB -> (f -> f) -> Record f (FORMULA f) (TERM f)
eqSubstRecord eqPredSet :: Set PRED_SYMB
eqPredSet extFun :: f -> f
extFun =
      ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
extFun) {foldPredication :: FORMULA f -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
foldPredication = FORMULA f -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall p f. p -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
foldPred}
    where foldPred :: p -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
foldPred _ psymb :: PRED_SYMB
psymb tList :: [TERM f]
tList rng :: Range
rng =
            if PRED_SYMB -> Set PRED_SYMB -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PRED_SYMB
psymb Set PRED_SYMB
eqPredSet
              then let [f :: TERM f
f, s :: TERM f
s] = [TERM f]
tList in TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM f
f Equality
Strong TERM f
s Range
rng
              else PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
psymb [TERM f]
tList Range
rng

substEqPreds :: Set.Set PRED_SYMB -> (f -> f) -> FORMULA f -> FORMULA f
substEqPreds :: Set PRED_SYMB -> (f -> f) -> FORMULA f -> FORMULA f
substEqPreds eqPredSet :: Set PRED_SYMB
eqPredSet = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set PRED_SYMB -> (f -> f) -> Record f (FORMULA f) (TERM f)
forall f.
Set PRED_SYMB -> (f -> f) -> Record f (FORMULA f) (TERM f)
eqSubstRecord Set PRED_SYMB
eqPredSet