{- |
Module      :  ./CASL/Freeness.hs
Description :  Computation of the constraints needed for free definition links.
Copyright   :  (c) Adrian Riesco, Facultad de Informatica UCM 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  ariesco@fdi.ucm.es
Stability   :  experimental
Portability :  portable

Computation of the constraints needed for free definition links.
-}

module CASL.Freeness (quotientTermAlgebra) where

import CASL.Sign
import CASL.Morphism
import CASL.StaticAna

import CASL.AS_Basic_CASL

import Logic.Prover ()

import Common.Id
import Common.Result
import Common.AS_Annotation
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet

import Data.Char
import Data.Maybe
import Data.List (groupBy, elemIndex)
import qualified Data.Map as Map
import qualified Data.Set as Set

-- | main function, in charge of computing the quotient term algebra
quotientTermAlgebra :: CASLMor -- sigma : Sigma -> SigmaM
                    -> [Named CASLFORMULA] -- Th(M)
                    -> Result (CASLSign, {- SigmaK
                               CASLMor, -- iota : SigmaM' -> SigmaK -}
                               [Named CASLFORMULA] -- Ax(K)
                              )
quotientTermAlgebra :: CASLMor
-> [Named CASLFORMULA] -> Result (CASLSign, [Named CASLFORMULA])
quotientTermAlgebra sigma :: CASLMor
sigma sens :: [Named CASLFORMULA]
sens =
                  let
                    sigma_0 :: CASLSign
sigma_0 = CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
msource CASLMor
sigma
                    ss_0 :: Set SORT
ss_0 = CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CASLSign
sigma_0
                    sigma_m :: CASLSign
sigma_m = CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
mtarget CASLMor
sigma
                    sigma_k :: CASLSign
sigma_k = Set SORT -> CASLSign -> CASLSign
create_sigma_k Set SORT
ss_0 CASLSign
sigma_m
                    axs :: [Named CASLFORMULA]
axs = Set SORT
-> CASLSign
-> CASLSign
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
create_axs Set SORT
ss_0 CASLSign
sigma_m CASLSign
sigma_k [Named CASLFORMULA]
sens
                  in (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
sigma_k, [Named CASLFORMULA]
axs)

-- | generates the axioms of the module K
create_axs :: Set.Set SORT -> CASLSign -> CASLSign -> [Named CASLFORMULA]
              -> [Named CASLFORMULA]
create_axs :: Set SORT
-> CASLSign
-> CASLSign
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
create_axs sg_ss :: Set SORT
sg_ss sg_m :: CASLSign
sg_m sg_k :: CASLSign
sg_k sens :: [Named CASLFORMULA]
sens = [Named CASLFORMULA]
forms
      where ss_m :: Set SORT
ss_m = CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CASLSign
sg_m
            ss :: Set SORT
ss = (SORT -> SORT) -> Set SORT -> Set SORT
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map SORT -> SORT
mkFreeName (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
ss_m Set SORT
sg_ss
            sr :: Rel SORT
sr = CASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel CASLSign
sg_k
            comps :: Set Component
comps = OpMap -> Set Component
ops2comp (OpMap -> Set Component) -> OpMap -> Set Component
forall a b. (a -> b) -> a -> b
$ CASLSign -> OpMap
forall f e. Sign f e -> OpMap
opMap CASLSign
sg_k
            ss' :: Set SORT
ss' = OpMap -> Set SORT -> Set SORT
filterNoCtorSorts (CASLSign -> OpMap
forall f e. Sign f e -> OpMap
opMap CASLSign
sg_k) Set SORT
ss
            ctor_sen :: [Named CASLFORMULA]
ctor_sen = GenAx -> [Named CASLFORMULA]
freeCons (Set SORT
ss', Rel SORT
sr, Set Component
comps)
            make_axs :: [Named CASLFORMULA]
make_axs = Set SORT -> [Named CASLFORMULA]
make_forms Set SORT
sg_ss [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ Set SORT -> [Named CASLFORMULA]
make_hom_forms Set SORT
sg_ss
            h_axs_ops :: [Named CASLFORMULA]
h_axs_ops = OpMap -> [Named CASLFORMULA]
homomorphism_axs_ops (OpMap -> [Named CASLFORMULA]) -> OpMap -> [Named CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ CASLSign -> OpMap
forall f e. Sign f e -> OpMap
opMap CASLSign
sg_m
            h_axs_preds :: [Named CASLFORMULA]
h_axs_preds = PredMap -> [Named CASLFORMULA]
homomorphism_axs_preds (PredMap -> [Named CASLFORMULA]) -> PredMap -> [Named CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ CASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap CASLSign
sg_m
            h_axs_surj :: [Named CASLFORMULA]
h_axs_surj = Set SORT -> [Named CASLFORMULA]
hom_surjectivity (Set SORT -> [Named CASLFORMULA])
-> Set SORT -> [Named CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CASLSign
sg_m
            q_axs :: [Named CASLFORMULA]
q_axs = [Named CASLFORMULA] -> [Named CASLFORMULA]
quotient_axs [Named CASLFORMULA]
sens
            symm_ax :: CASLFORMULA
symm_ax = Set SORT -> CASLFORMULA
symmetry_axs Set SORT
ss_m
            tran_ax :: CASLFORMULA
tran_ax = Set SORT -> CASLFORMULA
transitivity_axs Set SORT
ss_m
            cong_ax :: CASLFORMULA
cong_ax = OpMap -> CASLFORMULA
congruence_axs (CASLSign -> OpMap
forall f e. Sign f e -> OpMap
opMap CASLSign
sg_m)
            satThM :: CASLFORMULA
satThM = [Named CASLFORMULA] -> CASLFORMULA
sat_thm_ax [Named CASLFORMULA]
sens
            prems :: CASLFORMULA
prems = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA
symm_ax, CASLFORMULA
tran_ax, CASLFORMULA
cong_ax, CASLFORMULA
satThM]
            ltkh :: CASLFORMULA
ltkh = Set SORT -> PredMap -> CASLFORMULA
larger_than_ker_h Set SORT
ss_m (CASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap CASLSign
sg_m)
            krnl_axs :: [Named CASLFORMULA]
krnl_axs = [Set SORT
-> PredMap -> CASLFORMULA -> CASLFORMULA -> Named CASLFORMULA
mkKernelAx Set SORT
ss_m (CASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap CASLSign
sg_m) CASLFORMULA
prems CASLFORMULA
ltkh]
            forms :: [Named CASLFORMULA]
forms = [[Named CASLFORMULA]] -> [Named CASLFORMULA]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Named CASLFORMULA]
ctor_sen, [Named CASLFORMULA]
make_axs, [Named CASLFORMULA]
h_axs_ops, [Named CASLFORMULA]
h_axs_preds,
                            [Named CASLFORMULA]
h_axs_surj, [Named CASLFORMULA]
q_axs, [Named CASLFORMULA]
krnl_axs]

filterNoCtorSorts :: OpMap -> Set.Set SORT -> Set.Set SORT
filterNoCtorSorts :: OpMap -> Set SORT -> Set SORT
filterNoCtorSorts om :: OpMap
om = (SORT -> Bool) -> Set SORT -> Set SORT
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (OpMap -> SORT -> Bool
filterNoCtorSort OpMap
om)

filterNoCtorSort :: OpMap -> SORT -> Bool
filterNoCtorSort :: OpMap -> SORT -> Bool
filterNoCtorSort om :: OpMap
om s :: SORT
s = (Set OpType -> Bool) -> [Set OpType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SORT -> Set OpType -> Bool
resultTypeSet SORT
s) ([Set OpType] -> Bool)
-> (Map SORT (Set OpType) -> [Set OpType])
-> Map SORT (Set OpType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SORT (Set OpType) -> [Set OpType]
forall k a. Map k a -> [a]
Map.elems (Map SORT (Set OpType) -> Bool) -> Map SORT (Set OpType) -> Bool
forall a b. (a -> b) -> a -> b
$ OpMap -> Map SORT (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap OpMap
om

resultTypeSet :: SORT -> Set.Set OpType -> Bool
resultTypeSet :: SORT -> Set OpType -> Bool
resultTypeSet s :: SORT
s = (OpType -> Bool) -> [OpType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SORT -> OpType -> Bool
resultType SORT
s) ([OpType] -> Bool)
-> (Set OpType -> [OpType]) -> Set OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList

resultType :: SORT -> OpType -> Bool
resultType :: SORT -> OpType -> Bool
resultType s :: SORT
s = (SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
==) (SORT -> Bool) -> (OpType -> SORT) -> OpType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> SORT
opRes

{- | generates formulas of the form make(h(x)) =e= x,
for any x of sort gn_free_s -}
make_hom_forms :: Set.Set SORT -> [Named CASLFORMULA]
make_hom_forms :: Set SORT -> [Named CASLFORMULA]
make_hom_forms = (SORT -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA] -> Set SORT -> [Named CASLFORMULA]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ((:) (Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> (SORT -> Named CASLFORMULA)
-> SORT
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Named CASLFORMULA
make_hom_form) []

{- | generates a formula of the form make(h(x)) =e= x,
for gn_free_s given the SORT s -}
make_hom_form :: SORT -> Named CASLFORMULA
make_hom_form :: SORT -> Named CASLFORMULA
make_hom_form s :: SORT
s = [Char] -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_make_hom_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show SORT
s) CASLFORMULA
q_eq
      where free_s :: SORT
free_s = SORT -> SORT
mkFreeName SORT
s
            v :: CASLTERM
v = SORT -> CASLTERM
newVar SORT
free_s
            ot_hom :: OP_TYPE
ot_hom = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Partial [SORT
free_s] SORT
s Range
nullRange
            os_hom :: OP_SYMB
os_hom = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
homId OP_TYPE
ot_hom
            term_hom :: CASLTERM
term_hom = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
os_hom [CASLTERM
v]
            ot_mk :: OP_TYPE
ot_mk = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT
s] SORT
free_s Range
nullRange
            os_mk :: OP_SYMB
os_mk = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
makeId OP_TYPE
ot_mk
            term_mk :: CASLTERM
term_mk = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
os_mk [CASLTERM
term_hom]
            eq :: CASLFORMULA
eq = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkExEq CASLTERM
term_mk CASLTERM
v
            q_eq :: CASLFORMULA
q_eq = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
eq

-- | generates the formulas relating the make functions with the homomorphism
make_forms :: Set.Set SORT -> [Named CASLFORMULA]
make_forms :: Set SORT -> [Named CASLFORMULA]
make_forms = (SORT -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA] -> Set SORT -> [Named CASLFORMULA]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ((:) (Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> (SORT -> Named CASLFORMULA)
-> SORT
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Named CASLFORMULA
make_form) []

{- | generates the formulas relating the make function for this sort
with the homomorphism -}
make_form :: SORT -> Named CASLFORMULA
make_form :: SORT -> Named CASLFORMULA
make_form s :: SORT
s = [Char] -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_hom_make_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show SORT
s) CASLFORMULA
q_eq
      where free_s :: SORT
free_s = SORT -> SORT
mkFreeName SORT
s
            v :: CASLTERM
v = SORT -> CASLTERM
newVar SORT
s
            ot_mk :: OP_TYPE
ot_mk = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT
s] SORT
free_s Range
nullRange
            os_mk :: OP_SYMB
os_mk = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
makeId OP_TYPE
ot_mk
            term_mk :: CASLTERM
term_mk = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
os_mk [CASLTERM
v]
            ot_hom :: OP_TYPE
ot_hom = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Partial [SORT
free_s] SORT
s Range
nullRange
            os_hom :: OP_SYMB
os_hom = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
homId OP_TYPE
ot_hom
            term_hom :: CASLTERM
term_hom = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
os_hom [CASLTERM
term_mk]
            eq :: CASLFORMULA
eq = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq CASLTERM
term_hom CASLTERM
v
            q_eq :: CASLFORMULA
q_eq = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
eq

-- | computes the last part of the axioms to assert the kernel of h
larger_than_ker_h :: Set.Set SORT -> PredMap -> CASLFORMULA
larger_than_ker_h :: Set SORT -> PredMap -> CASLFORMULA
larger_than_ker_h ss :: Set SORT
ss mis :: PredMap
mis = CASLFORMULA
conj
     where ltkhs :: [CASLFORMULA]
ltkhs = Set SORT -> [CASLFORMULA]
ltkh_sorts Set SORT
ss
           ltkhp :: [CASLFORMULA]
ltkhp = PredMap -> [CASLFORMULA]
ltkh_preds PredMap
mis
           conj :: CASLFORMULA
conj = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([CASLFORMULA]
ltkhs [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
ltkhp)

{- | computes the second part of the conjunction of the formula "largerThanKerH"
from the kernel of H -}
ltkh_preds :: PredMap -> [CASLFORMULA]
ltkh_preds :: PredMap -> [CASLFORMULA]
ltkh_preds = (SORT -> PredType -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> PredMap -> [CASLFORMULA]
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ name :: SORT
name -> (:) (CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA])
-> (PredType -> CASLFORMULA)
-> PredType
-> [CASLFORMULA]
-> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> PredType -> CASLFORMULA
ltkh_preds_aux SORT
name) []

{- | computes the second part of the conjunction of the formula "largerThanKerH"
from the kernel of H for a concrete predicate profile -}
ltkh_preds_aux :: Id -> PredType -> CASLFORMULA
ltkh_preds_aux :: SORT -> PredType -> CASLFORMULA
ltkh_preds_aux name :: SORT
name (PredType args :: [SORT]
args) = CASLFORMULA
imp'
     where free_name :: SORT
free_name = SORT -> SORT
mkFreeName SORT
name
           free_args :: [SORT]
free_args = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args
           psi :: SORT
psi = SORT -> SORT
psiName SORT
name
           pt :: PRED_TYPE
pt = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
free_args Range
nullRange
           ps_name :: PRED_SYMB
ps_name = SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
free_name PRED_TYPE
pt
           ps_psi :: PRED_SYMB
ps_psi = SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
psi PRED_TYPE
pt
           vars :: [CASLTERM]
vars = Int -> [SORT] -> [CASLTERM]
createVars 1 [SORT]
free_args
           prem :: CASLFORMULA
prem = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps_name [CASLTERM]
vars
           concl :: CASLFORMULA
concl = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps_psi [CASLTERM]
vars
           imp :: CASLFORMULA
imp = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
prem CASLFORMULA
concl
           imp' :: CASLFORMULA
imp' = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
imp

{- | computes the first part of the conjunction of the formula "largerThanKerH"
from the kernel of H -}
ltkh_sorts :: Set.Set SORT -> [CASLFORMULA]
ltkh_sorts :: Set SORT -> [CASLFORMULA]
ltkh_sorts = (SORT -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> Set SORT -> [CASLFORMULA]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ((:) (CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA])
-> (SORT -> CASLFORMULA) -> SORT -> [CASLFORMULA] -> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> CASLFORMULA
ltkh_sort) []

{- | computes the first part of the conjunction of the formula "largerThanKerH"
from the kernel of H for a concrete sort -}
ltkh_sort :: SORT -> CASLFORMULA
ltkh_sort :: SORT -> CASLFORMULA
ltkh_sort s :: SORT
s = CASLFORMULA
imp'
     where free_s :: SORT
free_s = SORT -> SORT
mkFreeName SORT
s
           v1 :: CASLTERM
v1 = Int -> SORT -> CASLTERM
newVarIndex 1 SORT
free_s
           v2 :: CASLTERM
v2 = Int -> SORT -> CASLTERM
newVarIndex 2 SORT
free_s
           phi :: SORT
phi = SORT -> SORT
phiName SORT
s
           pt :: PRED_TYPE
pt = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT
free_s, SORT
free_s] Range
nullRange
           ps :: PRED_SYMB
ps = SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
phi PRED_TYPE
pt
           ot_hom :: OP_TYPE
ot_hom = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Partial [SORT
free_s] SORT
s Range
nullRange
           name_hom :: OP_SYMB
name_hom = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
homId OP_TYPE
ot_hom
           t1 :: CASLTERM
t1 = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
name_hom [CASLTERM
v1]
           t2 :: CASLTERM
t2 = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
name_hom [CASLTERM
v2]
           prem :: CASLFORMULA
prem = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkExEq CASLTERM
t1 CASLTERM
t2
           concl :: CASLFORMULA
concl = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
v1, CASLTERM
v2]
           imp :: CASLFORMULA
imp = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
prem CASLFORMULA
concl
           imp' :: CASLFORMULA
imp' = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
imp

-- | generates the axioms for satThM
sat_thm_ax :: [Named CASLFORMULA] -> CASLFORMULA
sat_thm_ax :: [Named CASLFORMULA] -> CASLFORMULA
sat_thm_ax forms :: [Named CASLFORMULA]
forms = CASLFORMULA
final_form
     where forms' :: [CASLFORMULA]
forms' = (Named CASLFORMULA -> CASLFORMULA)
-> [Named CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (CASLFORMULA -> CASLFORMULA
free_formula (CASLFORMULA -> CASLFORMULA)
-> (Named CASLFORMULA -> CASLFORMULA)
-> Named CASLFORMULA
-> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence)
             ([Named CASLFORMULA] -> [CASLFORMULA])
-> [Named CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ (Named CASLFORMULA -> Bool)
-> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. (a -> Bool) -> [a] -> [a]
filter (CASLFORMULA -> Bool
no_gen (CASLFORMULA -> Bool)
-> (Named CASLFORMULA -> CASLFORMULA) -> Named CASLFORMULA -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence) [Named CASLFORMULA]
forms
           final_form :: CASLFORMULA
final_form = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
forms'

-- | checks if the formula is a sort generation constraint
no_gen :: CASLFORMULA -> Bool
no_gen :: CASLFORMULA -> Bool
no_gen (Sort_gen_ax _ _) = Bool
False
no_gen _ = Bool
True

-- | computes the axiom for the congruence of the kernel of h
congruence_axs :: OpMap -> CASLFORMULA
congruence_axs :: OpMap -> CASLFORMULA
congruence_axs om :: OpMap
om = CASLFORMULA
conj
     where axs :: [CASLFORMULA]
axs = (SORT -> OpType -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> OpMap -> [CASLFORMULA]
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ name :: SORT
name -> (:) (CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA])
-> (OpType -> CASLFORMULA)
-> OpType
-> [CASLFORMULA]
-> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> OpType -> CASLFORMULA
congruence_ax_aux SORT
name)
                 [] OpMap
om
           conj :: CASLFORMULA
conj = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
axs

{- | computes the axiom for the congruence of the kernel of h
for a single type of an operator id -}
congruence_ax_aux :: Id -> OpType -> CASLFORMULA
congruence_ax_aux :: SORT -> OpType -> CASLFORMULA
congruence_ax_aux name :: SORT
name ot :: OpType
ot = CASLFORMULA
cong_form'
     where OpType _ args :: [SORT]
args res :: SORT
res = OpType
ot
           free_name :: SORT
free_name = SORT -> SORT
mkFreeName SORT
name
           free_args :: [SORT]
free_args = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args
           free_res :: SORT
free_res = SORT -> SORT
mkFreeName SORT
res
           free_ot :: OP_TYPE
free_ot = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT]
free_args SORT
free_res Range
nullRange
           free_os :: OP_SYMB
free_os = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
free_name OP_TYPE
free_ot
           lgth :: Int
lgth = [SORT] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SORT]
free_args
           xs :: [CASLTERM]
xs = Int -> [SORT] -> [CASLTERM]
createVars 1 [SORT]
free_args
           ys :: [CASLTERM]
ys = Int -> [SORT] -> [CASLTERM]
createVars (1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
lgth) [SORT]
free_args
           fst_term :: CASLTERM
fst_term = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
free_os [CASLTERM]
xs
           snd_term :: CASLTERM
snd_term = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
free_os [CASLTERM]
ys
           phi :: SORT
phi = SORT -> SORT
phiName SORT
res
           pt :: PRED_TYPE
pt = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT
free_res, SORT
free_res] Range
nullRange
           ps :: PRED_SYMB
ps = SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
phi PRED_TYPE
pt
           fst_form :: CASLFORMULA
fst_form = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
fst_term, CASLTERM
fst_term]
           snd_form :: CASLFORMULA
snd_form = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
snd_term, CASLTERM
snd_term]
           vars_forms :: [CASLFORMULA]
vars_forms = [SORT] -> [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
congruence_ax_vars [SORT]
args [CASLTERM]
xs [CASLTERM]
ys
           conj :: CASLFORMULA
conj = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA
fst_form CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: CASLFORMULA
snd_form CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [CASLFORMULA]
vars_forms
           concl :: CASLFORMULA
concl = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
fst_term, CASLTERM
snd_term]
           cong_form :: CASLFORMULA
cong_form = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
conj CASLFORMULA
concl
           cong_form' :: CASLFORMULA
cong_form' = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
cong_form


freePredNameAndType :: SORT -> (Id, PRED_TYPE)
freePredNameAndType :: SORT -> (SORT, PRED_TYPE)
freePredNameAndType s :: SORT
s = let
    phi :: SORT
phi = SORT -> SORT
phiName SORT
s
    free_s :: SORT
free_s = SORT -> SORT
mkFreeName SORT
s
    pt :: PRED_TYPE
pt = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT
free_s, SORT
free_s] Range
nullRange
    in (SORT
phi, PRED_TYPE
pt)

freePredSymb :: SORT -> PRED_SYMB
freePredSymb :: SORT -> PRED_SYMB
freePredSymb = (SORT -> PRED_TYPE -> PRED_SYMB) -> (SORT, PRED_TYPE) -> PRED_SYMB
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred ((SORT, PRED_TYPE) -> PRED_SYMB)
-> (SORT -> (SORT, PRED_TYPE)) -> SORT -> PRED_SYMB
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> (SORT, PRED_TYPE)
freePredNameAndType

-- | computes the formulas for the relations between variables
congruence_ax_vars :: [SORT] -> [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
congruence_ax_vars :: [SORT] -> [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
congruence_ax_vars (s :: SORT
s : ss :: [SORT]
ss) (x :: CASLTERM
x : xs :: [CASLTERM]
xs) (y :: CASLTERM
y : ys :: [CASLTERM]
ys) = CASLFORMULA
form CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [CASLFORMULA]
forms
     where
           form :: CASLFORMULA
form = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication (SORT -> PRED_SYMB
freePredSymb SORT
s) [CASLTERM
x, CASLTERM
y]
           forms :: [CASLFORMULA]
forms = [SORT] -> [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
congruence_ax_vars [SORT]
ss [CASLTERM]
xs [CASLTERM]
ys
congruence_ax_vars _ _ _ = []

-- | computes the transitivity axioms for the kernel of h
transitivity_axs :: Set.Set SORT -> CASLFORMULA
transitivity_axs :: Set SORT -> CASLFORMULA
transitivity_axs ss :: Set SORT
ss = CASLFORMULA
conj
     where axs :: [CASLFORMULA]
axs = (SORT -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> Set SORT -> [CASLFORMULA]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ((:) (CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA])
-> (SORT -> CASLFORMULA) -> SORT -> [CASLFORMULA] -> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> CASLFORMULA
transitivity_ax) [] Set SORT
ss
           conj :: CASLFORMULA
conj = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
axs

twoFreeVars :: SORT -> (SORT, TERM (), TERM (), VAR, VAR, PRED_SYMB, FORMULA ())
twoFreeVars :: SORT
-> (SORT, CASLTERM, CASLTERM, VAR, VAR, PRED_SYMB, CASLFORMULA)
twoFreeVars s :: SORT
s = let
   free_sort :: SORT
free_sort = SORT -> SORT
mkFreeName SORT
s
   v1 :: CASLTERM
v1@(Qual_var n1 :: VAR
n1 _ _) = Int -> SORT -> CASLTERM
newVarIndex 1 SORT
free_sort
   v2 :: CASLTERM
v2@(Qual_var n2 :: VAR
n2 _ _) = Int -> SORT -> CASLTERM
newVarIndex 2 SORT
free_sort
   ps :: PRED_SYMB
ps = SORT -> PRED_SYMB
freePredSymb SORT
s
   fst_form :: CASLFORMULA
fst_form = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
v1, CASLTERM
v2]
   in (SORT
free_sort, CASLTERM
v1, CASLTERM
v2, VAR
n1, VAR
n2, PRED_SYMB
ps, CASLFORMULA
fst_form)

{- | computes the transitivity axiom of a concrete sort for
the kernel of h -}
transitivity_ax :: SORT -> CASLFORMULA
transitivity_ax :: SORT -> CASLFORMULA
transitivity_ax s :: SORT
s = CASLFORMULA
quant
     where (free_sort :: SORT
free_sort, v1 :: CASLTERM
v1, v2 :: CASLTERM
v2, n1 :: VAR
n1, n2 :: VAR
n2, ps :: PRED_SYMB
ps, fst_form :: CASLFORMULA
fst_form) = SORT
-> (SORT, CASLTERM, CASLTERM, VAR, VAR, PRED_SYMB, CASLFORMULA)
twoFreeVars SORT
s
           v3 :: CASLTERM
v3@(Qual_var n3 :: VAR
n3 _ _) = Int -> SORT -> CASLTERM
newVarIndex 3 SORT
free_sort
           snd_form :: CASLFORMULA
snd_form = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
v2, CASLTERM
v3]
           thr_form :: CASLFORMULA
thr_form = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
v1, CASLTERM
v3]
           conj :: CASLFORMULA
conj = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA
fst_form, CASLFORMULA
snd_form]
           imp :: CASLFORMULA
imp = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
conj CASLFORMULA
thr_form
           vd :: [VAR_DECL]
vd = [[VAR] -> SORT -> Range -> VAR_DECL
Var_decl [VAR
n1, VAR
n2, VAR
n3] SORT
free_sort Range
nullRange]
           quant :: CASLFORMULA
quant = [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vd CASLFORMULA
imp

-- | computes the symmetry axioms for the kernel of h
symmetry_axs :: Set.Set SORT -> CASLFORMULA
symmetry_axs :: Set SORT -> CASLFORMULA
symmetry_axs ss :: Set SORT
ss = CASLFORMULA
conj
     where axs :: [CASLFORMULA]
axs = (SORT -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> Set SORT -> [CASLFORMULA]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ((:) (CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA])
-> (SORT -> CASLFORMULA) -> SORT -> [CASLFORMULA] -> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> CASLFORMULA
symmetry_ax) [] Set SORT
ss
           conj :: CASLFORMULA
conj = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
axs

-- | computes the symmetry axiom of a concrete sort for the kernel of h
symmetry_ax :: SORT -> CASLFORMULA
symmetry_ax :: SORT -> CASLFORMULA
symmetry_ax s :: SORT
s = CASLFORMULA
quant
     where (free_sort :: SORT
free_sort, v1 :: CASLTERM
v1, v2 :: CASLTERM
v2, n1 :: VAR
n1, n2 :: VAR
n2, ps :: PRED_SYMB
ps, lhs :: CASLFORMULA
lhs) = SORT
-> (SORT, CASLTERM, CASLTERM, VAR, VAR, PRED_SYMB, CASLFORMULA)
twoFreeVars SORT
s
           rhs :: CASLFORMULA
rhs = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
v2, CASLTERM
v1]
           inner_form :: CASLFORMULA
inner_form = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
lhs CASLFORMULA
rhs
           vd :: [VAR_DECL]
vd = [[VAR] -> SORT -> Range -> VAR_DECL
Var_decl [VAR
n1, VAR
n2] SORT
free_sort Range
nullRange]
           quant :: CASLFORMULA
quant = [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vd CASLFORMULA
inner_form

-- | generates the name of the phi variable of a concrete sort
phiName :: SORT -> Id
phiName :: SORT -> SORT
phiName s :: SORT
s = [VAR] -> SORT
mkId [[Char] -> VAR
mkSimpleId ([Char] -> VAR) -> [Char] -> VAR
forall a b. (a -> b) -> a -> b
$ "Phi_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show SORT
s]

-- | generates the name of the phi variable of a concrete predicate
psiName :: Id -> Id
psiName :: SORT -> SORT
psiName s :: SORT
s = [VAR] -> SORT
mkId [[Char] -> VAR
mkSimpleId ([Char] -> VAR) -> [Char] -> VAR
forall a b. (a -> b) -> a -> b
$ "Psi_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show SORT
s]

{- | creates the axiom for the kernel of h given the sorts and the predicates
in M, the premises and the conclusion -}
mkKernelAx :: Set.Set SORT -> PredMap -> CASLFORMULA
              -> CASLFORMULA -> Named CASLFORMULA
mkKernelAx :: Set SORT
-> PredMap -> CASLFORMULA -> CASLFORMULA -> Named CASLFORMULA
mkKernelAx ss :: Set SORT
ss preds :: PredMap
preds prem :: CASLFORMULA
prem conc :: CASLFORMULA
conc = [Char] -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "freeness_kernel" CASLFORMULA
q2
     where imp :: CASLFORMULA
imp = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
prem CASLFORMULA
conc
           q1 :: CASLFORMULA
q1 = Set SORT -> CASLFORMULA -> CASLFORMULA
quantifyPredsSorts Set SORT
ss CASLFORMULA
imp
           q2 :: CASLFORMULA
q2 = PredMap -> CASLFORMULA -> CASLFORMULA
quantifyPredsPreds PredMap
preds CASLFORMULA
q1

{- | applies the second order quantification to the formula for the given
set of sorts -}
quantifyPredsSorts :: Set.Set SORT -> CASLFORMULA -> CASLFORMULA
quantifyPredsSorts :: Set SORT -> CASLFORMULA -> CASLFORMULA
quantifyPredsSorts ss :: Set SORT
ss f :: CASLFORMULA
f = (SORT -> CASLFORMULA -> CASLFORMULA)
-> CASLFORMULA -> Set SORT -> CASLFORMULA
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold SORT -> CASLFORMULA -> CASLFORMULA
quantifyPredsSort CASLFORMULA
f Set SORT
ss

{- | applies the second order quantification to the formula for the given
sort -}
quantifyPredsSort :: SORT -> CASLFORMULA -> CASLFORMULA
quantifyPredsSort :: SORT -> CASLFORMULA -> CASLFORMULA
quantifyPredsSort = (SORT -> PRED_TYPE -> CASLFORMULA -> CASLFORMULA)
-> (SORT, PRED_TYPE) -> CASLFORMULA -> CASLFORMULA
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SORT -> PRED_TYPE -> CASLFORMULA -> CASLFORMULA
forall f. SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred ((SORT, PRED_TYPE) -> CASLFORMULA -> CASLFORMULA)
-> (SORT -> (SORT, PRED_TYPE))
-> SORT
-> CASLFORMULA
-> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> (SORT, PRED_TYPE)
freePredNameAndType

{- | applies the second order quantification to the formula for the given
predicates -}
quantifyPredsPreds :: PredMap -> CASLFORMULA -> CASLFORMULA
quantifyPredsPreds :: PredMap -> CASLFORMULA -> CASLFORMULA
quantifyPredsPreds = (CASLFORMULA -> PredMap -> CASLFORMULA)
-> PredMap -> CASLFORMULA -> CASLFORMULA
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((CASLFORMULA -> PredMap -> CASLFORMULA)
 -> PredMap -> CASLFORMULA -> CASLFORMULA)
-> (CASLFORMULA -> PredMap -> CASLFORMULA)
-> PredMap
-> CASLFORMULA
-> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (SORT -> PredType -> CASLFORMULA -> CASLFORMULA)
-> CASLFORMULA -> PredMap -> CASLFORMULA
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey SORT -> PredType -> CASLFORMULA -> CASLFORMULA
quantifyPredsPred

{- | applies the second order quantification to the formula for the given
predicate -}
quantifyPredsPred :: Id -> PredType -> CASLFORMULA -> CASLFORMULA
quantifyPredsPred :: SORT -> PredType -> CASLFORMULA -> CASLFORMULA
quantifyPredsPred name :: SORT
name (PredType args :: [SORT]
args) f :: CASLFORMULA
f = CASLFORMULA
q_form
     where psi :: SORT
psi = SORT -> SORT
psiName SORT
name
           free_args :: [SORT]
free_args = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args
           pt :: PRED_TYPE
pt = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
free_args Range
nullRange
           q_form :: CASLFORMULA
q_form = SORT -> PRED_TYPE -> CASLFORMULA -> CASLFORMULA
forall f. SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred SORT
psi PRED_TYPE
pt CASLFORMULA
f

{- | given the axioms in the module M, the function computes the
axioms obtained for the homomorphisms -}
quotient_axs :: [Named CASLFORMULA] -> [Named CASLFORMULA]
quotient_axs :: [Named CASLFORMULA] -> [Named CASLFORMULA]
quotient_axs = (Named CASLFORMULA -> Named CASLFORMULA)
-> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map Named CASLFORMULA -> Named CASLFORMULA
quotient_ax

{- | given an axiom in the module M, the function computes the
axioms obtained for the homomorphisms -}
quotient_ax :: Named CASLFORMULA -> Named CASLFORMULA
quotient_ax :: Named CASLFORMULA -> Named CASLFORMULA
quotient_ax nsen :: Named CASLFORMULA
nsen = Named CASLFORMULA
nsen'
      where sen :: CASLFORMULA
sen = Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence Named CASLFORMULA
nsen
            sen' :: CASLFORMULA
sen' = CASLFORMULA -> CASLFORMULA
homomorphy_form CASLFORMULA
sen
            nsen' :: Named CASLFORMULA
nsen' = Named CASLFORMULA
nsen { sentence :: CASLFORMULA
sentence = CASLFORMULA
sen' }

-- | applies the homomorphism operator to the terms of the given formula
homomorphy_form :: CASLFORMULA -> CASLFORMULA
homomorphy_form :: CASLFORMULA -> CASLFORMULA
homomorphy_form (Quantification q :: QUANTIFIER
q _ f :: CASLFORMULA
f r :: Range
r) = QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
var_decl CASLFORMULA
f' Range
r
     where f' :: CASLFORMULA
f' = CASLFORMULA -> CASLFORMULA
homomorphy_form CASLFORMULA
f
           vars :: Map SORT (Set VAR)
vars = CASLFORMULA -> Map SORT (Set VAR)
getVars CASLFORMULA
f'
           var_decl :: [VAR_DECL]
var_decl = Map SORT (Set VAR) -> [VAR_DECL]
listVarDecl Map SORT (Set VAR)
vars
homomorphy_form (Junction j :: Junctor
j fs :: [CASLFORMULA]
fs r :: Range
r) = Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j [CASLFORMULA]
fs' Range
r
     where fs' :: [CASLFORMULA]
fs' = (CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map CASLFORMULA -> CASLFORMULA
homomorphy_form [CASLFORMULA]
fs
homomorphy_form (Relation f1 :: CASLFORMULA
f1 c :: Relation
c f2 :: CASLFORMULA
f2 r :: Range
r) = CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
f1' Relation
c CASLFORMULA
f2' Range
r
     where f1' :: CASLFORMULA
f1' = CASLFORMULA -> CASLFORMULA
homomorphy_form CASLFORMULA
f1
           f2' :: CASLFORMULA
f2' = CASLFORMULA -> CASLFORMULA
homomorphy_form CASLFORMULA
f2
homomorphy_form (Negation f :: CASLFORMULA
f r :: Range
r) = CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
f' Range
r
     where f' :: CASLFORMULA
f' = CASLFORMULA -> CASLFORMULA
homomorphy_form CASLFORMULA
f
homomorphy_form (Predication ps :: PRED_SYMB
ps ts :: [CASLTERM]
ts r :: Range
r) = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
ps [CASLTERM]
ts' Range
r
     where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
homomorphy_term [CASLTERM]
ts
homomorphy_form (Definedness t :: CASLTERM
t r :: Range
r) = CASLTERM -> Range -> CASLFORMULA
forall f. TERM f -> Range -> FORMULA f
Definedness CASLTERM
t' Range
r
     where t' :: CASLTERM
t' = CASLTERM -> CASLTERM
homomorphy_term CASLTERM
t
homomorphy_form (Equation t1 :: CASLTERM
t1 e :: Equality
e t2 :: CASLTERM
t2 r :: Range
r) = CASLTERM -> Equality -> CASLTERM -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation CASLTERM
t1' Equality
e CASLTERM
t2' Range
r
     where t1' :: CASLTERM
t1' = CASLTERM -> CASLTERM
homomorphy_term CASLTERM
t1
           t2' :: CASLTERM
t2' = CASLTERM -> CASLTERM
homomorphy_term CASLTERM
t2
homomorphy_form (Membership t :: CASLTERM
t s :: SORT
s r :: Range
r) = CASLTERM -> SORT -> Range -> CASLFORMULA
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership CASLTERM
t' SORT
s Range
r
     where t' :: CASLTERM
t' = CASLTERM -> CASLTERM
homomorphy_term CASLTERM
t
homomorphy_form (Mixfix_formula t :: CASLTERM
t) = CASLTERM -> CASLFORMULA
forall f. TERM f -> FORMULA f
Mixfix_formula CASLTERM
t'
     where t' :: CASLTERM
t' = CASLTERM -> CASLTERM
homomorphy_term CASLTERM
t
homomorphy_form f :: CASLFORMULA
f = CASLFORMULA
f

-- | applies the homomorphism operator to the term when possible
homomorphy_term :: CASLTERM -> CASLTERM
homomorphy_term :: CASLTERM -> CASLTERM
homomorphy_term (Qual_var v :: VAR
v s :: SORT
s r :: Range
r) = CASLTERM
forall f. TERM f
t
      where free_s :: SORT
free_s = SORT -> SORT
mkFreeName SORT
s
            v' :: TERM f
v' = VAR -> SORT -> Range -> TERM f
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
v SORT
free_s Range
r
            ot_hom :: OP_TYPE
ot_hom = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Partial [SORT
free_s] SORT
s Range
nullRange
            name_hom :: OP_SYMB
name_hom = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
homId OP_TYPE
ot_hom
            t :: TERM f
t = OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
name_hom [TERM f
forall f. TERM f
v']
homomorphy_term (Application os :: OP_SYMB
os ts :: [CASLTERM]
ts r :: Range
r) = CASLTERM
t'
      where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
free_term [CASLTERM]
ts
            Qual_op_name op_name :: SORT
op_name ot :: OP_TYPE
ot op_r :: Range
op_r = OP_SYMB
os
            Op_type _ ar :: [SORT]
ar co :: SORT
co ot_r :: Range
ot_r = OP_TYPE
ot
            op_name' :: SORT
op_name' = SORT -> SORT
mkFreeName SORT
op_name
            ar' :: [SORT]
ar' = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
ar
            co' :: SORT
co' = SORT -> SORT
mkFreeName SORT
co
            ot' :: OP_TYPE
ot' = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT]
ar' SORT
co' Range
ot_r
            os' :: OP_SYMB
os' = SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
op_name' OP_TYPE
ot' Range
op_r
            t :: CASLTERM
t = OP_SYMB -> [CASLTERM] -> Range -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
os' [CASLTERM]
ts' Range
r
            ot_hom :: OP_TYPE
ot_hom = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Partial [SORT
co'] SORT
co Range
nullRange
            name_hom :: OP_SYMB
name_hom = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
homId OP_TYPE
ot_hom
            t' :: CASLTERM
t' = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
name_hom [CASLTERM
t]
homomorphy_term t :: CASLTERM
t = CASLTERM
t

hom_surjectivity :: Set.Set SORT -> [Named CASLFORMULA]
hom_surjectivity :: Set SORT -> [Named CASLFORMULA]
hom_surjectivity = (SORT -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA] -> Set SORT -> [Named CASLFORMULA]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold SORT -> [Named CASLFORMULA] -> [Named CASLFORMULA]
f []
      where f :: SORT -> [Named CASLFORMULA] -> [Named CASLFORMULA]
f x :: SORT
x = (SORT -> Named CASLFORMULA
sort_surj SORT
x Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. a -> [a] -> [a]
:)

-- | generates the formula to state the homomorphism is surjective
sort_surj :: SORT -> Named CASLFORMULA
sort_surj :: SORT -> Named CASLFORMULA
sort_surj s :: SORT
s = Named CASLFORMULA
form'
      where v1 :: CASLTERM
v1 = Int -> SORT -> CASLTERM
newVarIndex 0 (SORT -> CASLTERM) -> SORT -> CASLTERM
forall a b. (a -> b) -> a -> b
$ SORT -> SORT
mkFreeName SORT
s
            id_v1 :: VAR
id_v1 = [Char] -> VAR
mkSimpleId "V0"
            vd1 :: VAR_DECL
vd1 = VAR -> SORT -> VAR_DECL
mkVarDecl VAR
id_v1 (SORT -> SORT
mkFreeName SORT
s)
            v2 :: CASLTERM
v2 = Int -> SORT -> CASLTERM
newVarIndex 1 SORT
s
            id_v2 :: VAR
id_v2 = [Char] -> VAR
mkSimpleId "V1"
            vd2 :: VAR_DECL
vd2 = VAR -> SORT -> VAR_DECL
mkVarDecl VAR
id_v2 SORT
s
            ot_hom :: OP_TYPE
ot_hom = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Partial [SORT -> SORT
mkFreeName SORT
s] SORT
s Range
nullRange
            name_hom :: OP_SYMB
name_hom = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
homId OP_TYPE
ot_hom
            lhs :: CASLTERM
lhs = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
name_hom [CASLTERM
v1]
            inner_form :: CASLFORMULA
inner_form = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkExEq CASLTERM
lhs CASLTERM
v2
            inner_form' :: CASLFORMULA
inner_form' = [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL
vd1] CASLFORMULA
inner_form
            form :: CASLFORMULA
form = [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vd2] CASLFORMULA
inner_form'
            form' :: Named CASLFORMULA
form' = [Char] -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_hom_surj_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SORT -> [Char]
forall a. Show a => a -> [Char]
show SORT
s) CASLFORMULA
form

-- | generates the axioms for the homomorphisms applied to the predicates
homomorphism_axs_preds :: PredMap -> [Named CASLFORMULA]
homomorphism_axs_preds :: PredMap -> [Named CASLFORMULA]
homomorphism_axs_preds =
  (SORT -> PredType -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA] -> PredMap -> [Named CASLFORMULA]
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ p_name :: SORT
p_name -> (:) (Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> (PredType -> Named CASLFORMULA)
-> PredType
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> PredType -> Named CASLFORMULA
homomorphism_form_pred SORT
p_name) []

-- | generates the axioms for the homomorphisms applied to a predicate
homomorphism_form_pred :: Id -> PredType -> Named CASLFORMULA
homomorphism_form_pred :: SORT -> PredType -> Named CASLFORMULA
homomorphism_form_pred name :: SORT
name (PredType args :: [SORT]
args) = Named CASLFORMULA
named_form
      where free_args :: [SORT]
free_args = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args
            vars_lhs :: [CASLTERM]
vars_lhs = Int -> [SORT] -> [CASLTERM]
createVars 0 [SORT]
free_args
            lhs_pt :: PRED_TYPE
lhs_pt = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
free_args Range
nullRange
            lhs_pred_name :: PRED_SYMB
lhs_pred_name = SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred (SORT -> SORT
mkFreeName SORT
name) PRED_TYPE
lhs_pt
            lhs :: CASLFORMULA
lhs = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
lhs_pred_name [CASLTERM]
vars_lhs
            inner_rhs :: [CASLTERM]
inner_rhs = [SORT] -> [CASLTERM] -> [CASLTERM]
apply_hom_vars [SORT]
args [CASLTERM]
vars_lhs
            pt_rhs :: PRED_TYPE
pt_rhs = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
args Range
nullRange
            name_rhs :: PRED_SYMB
name_rhs = SORT -> PRED_TYPE -> PRED_SYMB
mkQualPred SORT
name PRED_TYPE
pt_rhs
            rhs :: CASLFORMULA
rhs = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
name_rhs [CASLTERM]
inner_rhs
            form :: CASLFORMULA
form = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv CASLFORMULA
lhs CASLFORMULA
rhs
            form' :: CASLFORMULA
form' = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form
            named_form :: Named CASLFORMULA
named_form = [Char] -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "" CASLFORMULA
form'

-- | generates the axioms for the homomorphisms applied to the operators
homomorphism_axs_ops :: OpMap -> [Named CASLFORMULA]
homomorphism_axs_ops :: OpMap -> [Named CASLFORMULA]
homomorphism_axs_ops =
  (SORT -> OpType -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA] -> OpMap -> [Named CASLFORMULA]
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ op_name :: SORT
op_name -> (:) (Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> (OpType -> Named CASLFORMULA)
-> OpType
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> OpType -> Named CASLFORMULA
homomorphism_form_op SORT
op_name) []

-- | generates the axiom for the homomorphism applied to a concrete op
homomorphism_form_op :: Id -> OpType -> Named CASLFORMULA
homomorphism_form_op :: SORT -> OpType -> Named CASLFORMULA
homomorphism_form_op name :: SORT
name (OpType _ args :: [SORT]
args res :: SORT
res) = Named CASLFORMULA
named_form
      where free_args :: [SORT]
free_args = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args
            vars_lhs :: [CASLTERM]
vars_lhs = Int -> [SORT] -> [CASLTERM]
createVars 0 [SORT]
free_args
            ot_lhs :: OP_TYPE
ot_lhs = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT]
free_args (SORT -> SORT
mkFreeName SORT
res) Range
nullRange
            ot_hom :: OP_TYPE
ot_hom = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Partial [SORT -> SORT
mkFreeName SORT
res] SORT
res Range
nullRange
            name_hom :: OP_SYMB
name_hom = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
homId OP_TYPE
ot_hom
            name_lhs :: OP_SYMB
name_lhs = SORT -> OP_TYPE -> OP_SYMB
mkQualOp (SORT -> SORT
mkFreeName SORT
name) OP_TYPE
ot_lhs
            inner_lhs :: CASLTERM
inner_lhs = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
name_lhs [CASLTERM]
vars_lhs
            lhs :: CASLTERM
lhs = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
name_hom [CASLTERM
inner_lhs]
            ot_rhs :: OP_TYPE
ot_rhs = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT]
args SORT
res Range
nullRange
            name_rhs :: OP_SYMB
name_rhs = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
name OP_TYPE
ot_rhs
            inner_rhs :: [CASLTERM]
inner_rhs = [SORT] -> [CASLTERM] -> [CASLTERM]
apply_hom_vars [SORT]
args [CASLTERM]
vars_lhs
            rhs :: CASLTERM
rhs = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
name_rhs [CASLTERM]
inner_rhs
            form :: CASLFORMULA
form = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq CASLTERM
lhs CASLTERM
rhs
            form' :: CASLFORMULA
form' = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form
            named_form :: Named CASLFORMULA
named_form = [Char] -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "" CASLFORMULA
form'

-- | generates the variables for the homomorphisms
apply_hom_vars :: [SORT] -> [CASLTERM] -> [CASLTERM]
apply_hom_vars :: [SORT] -> [CASLTERM] -> [CASLTERM]
apply_hom_vars (s :: SORT
s : ss :: [SORT]
ss) (t :: CASLTERM
t : ts :: [CASLTERM]
ts) = CASLTERM
t' CASLTERM -> [CASLTERM] -> [CASLTERM]
forall a. a -> [a] -> [a]
: [CASLTERM]
ts'
      where ot_hom :: OP_TYPE
ot_hom = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Partial [SORT -> SORT
mkFreeName SORT
s] SORT
s Range
nullRange
            name_hom :: OP_SYMB
name_hom = SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
homId OP_TYPE
ot_hom
            t' :: CASLTERM
t' = OP_SYMB -> [CASLTERM] -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
name_hom [CASLTERM
t]
            ts' :: [CASLTERM]
ts' = [SORT] -> [CASLTERM] -> [CASLTERM]
apply_hom_vars [SORT]
ss [CASLTERM]
ts
apply_hom_vars _ _ = []

-- | generates a list of differents variables of the given sorts
createVars :: Int -> [SORT] -> [CASLTERM]
createVars :: Int -> [SORT] -> [CASLTERM]
createVars _ [] = []
createVars i :: Int
i (s :: SORT
s : ss :: [SORT]
ss) = CASLTERM
var CASLTERM -> [CASLTERM] -> [CASLTERM]
forall a. a -> [a] -> [a]
: [CASLTERM]
ts
      where var :: CASLTERM
var = Int -> SORT -> CASLTERM
newVarIndex Int
i SORT
s
            ts :: [CASLTERM]
ts = Int -> [SORT] -> [CASLTERM]
createVars (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [SORT]
ss

-- | computes the set of components from the map of operators
ops2comp :: OpMap -> Set.Set Component
ops2comp :: OpMap -> Set Component
ops2comp = (SORT -> OpType -> Set Component -> Set Component)
-> Set Component -> OpMap -> Set Component
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey (\ n :: SORT
n -> Component -> Set Component -> Set Component
forall a. Ord a => a -> Set a -> Set a
Set.insert (Component -> Set Component -> Set Component)
-> (OpType -> Component)
-> OpType
-> Set Component
-> Set Component
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> OpType -> Component
Component SORT
n) Set Component
forall a. Set a
Set.empty

-- | computes the sentence for the constructors
freeCons :: GenAx -> [Named CASLFORMULA]
freeCons :: GenAx -> [Named CASLFORMULA]
freeCons (sorts :: Set SORT
sorts, rel :: Rel SORT
rel, ops :: Set Component
ops) =
    let sortList :: [SORT]
sortList = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList Set SORT
sorts
        opSyms :: [OP_SYMB]
opSyms = (Component -> OP_SYMB) -> [Component] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map ( \ c :: Component
c -> let iden :: SORT
iden = Component -> SORT
compId Component
c in SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
iden
                      (OpType -> OP_TYPE
toOP_TYPE (OpType -> OP_TYPE) -> OpType -> OP_TYPE
forall a b. (a -> b) -> a -> b
$ Component -> OpType
compType Component
c) (Range -> OP_SYMB) -> Range -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ SORT -> Range
posOfId SORT
iden) ([Component] -> [OP_SYMB]) -> [Component] -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$ Set Component -> [Component]
forall a. Set a -> [a]
Set.toList Set Component
ops
        injSyms :: [OP_SYMB]
injSyms = ((SORT, SORT) -> OP_SYMB) -> [(SORT, SORT)] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (s :: SORT
s, t :: SORT
t) -> let p :: Range
p = SORT -> Range
posOfId SORT
s in
                        SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (SORT -> SORT -> SORT
mkUniqueInjName SORT
s SORT
t)
                         (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT
s] SORT
t Range
p) Range
p)
                  ([(SORT, SORT)] -> [OP_SYMB]) -> [(SORT, SORT)] -> [OP_SYMB]
forall a b. (a -> b) -> a -> b
$ Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel SORT -> [(SORT, SORT)]) -> Rel SORT -> [(SORT, SORT)]
forall a b. (a -> b) -> a -> b
$ Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.irreflex Rel SORT
rel
        allSyms :: [OP_SYMB]
allSyms = [OP_SYMB]
opSyms [OP_SYMB] -> [OP_SYMB] -> [OP_SYMB]
forall a. [a] -> [a] -> [a]
++ [OP_SYMB]
injSyms
        resType :: SORT -> OP_SYMB -> Bool
resType _ (Op_name _) = Bool
False
        resType s :: SORT
s (Qual_op_name _ t :: OP_TYPE
t _) = OP_TYPE -> SORT
res_OP_TYPE OP_TYPE
t SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s
        getIndex :: SORT -> Int
getIndex s :: SORT
s = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (-1) (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ SORT -> [SORT] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex SORT
s [SORT]
sortList
        addIndices :: OP_SYMB -> (OP_SYMB, [Int])
addIndices (Op_name _) =
          [Char] -> (OP_SYMB, [Int])
forall a. HasCallStack => [Char] -> a
error "CASL/StaticAna: Internal error in function addIndices"
        addIndices os :: OP_SYMB
os@(Qual_op_name _ t :: OP_TYPE
t _) =
            (OP_SYMB
os, (SORT -> Int) -> [SORT] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Int
getIndex ([SORT] -> [Int]) -> [SORT] -> [Int]
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> [SORT]
args_OP_TYPE OP_TYPE
t)
        collectOps :: SORT -> Constraint
collectOps s :: SORT
s =
          SORT -> [(OP_SYMB, [Int])] -> SORT -> Constraint
Constraint SORT
s ((OP_SYMB -> (OP_SYMB, [Int])) -> [OP_SYMB] -> [(OP_SYMB, [Int])]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> (OP_SYMB, [Int])
addIndices ([OP_SYMB] -> [(OP_SYMB, [Int])])
-> [OP_SYMB] -> [(OP_SYMB, [Int])]
forall a b. (a -> b) -> a -> b
$ (OP_SYMB -> Bool) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> Bool) -> [a] -> [a]
filter (SORT -> OP_SYMB -> Bool
resType SORT
s) [OP_SYMB]
allSyms) SORT
s
        constrs :: [Constraint]
constrs = (SORT -> Constraint) -> [SORT] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Constraint
collectOps [SORT]
sortList
        f :: FORMULA f
f = [Constraint] -> Bool -> FORMULA f
forall f. [Constraint] -> Bool -> FORMULA f
mkSort_gen_ax [Constraint]
constrs Bool
True
 -- added by me:
        nonSub :: OP_SYMB -> Bool
nonSub (Qual_op_name n :: SORT
n _ _) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SORT -> Bool
isInjName SORT
n
        nonSub _ = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error "use qualified names"
        consSymbs :: [[OP_SYMB]]
consSymbs = (Constraint -> [OP_SYMB]) -> [Constraint] -> [[OP_SYMB]]
forall a b. (a -> b) -> [a] -> [b]
map ((OP_SYMB -> Bool) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> Bool) -> [a] -> [a]
filter OP_SYMB -> Bool
nonSub ([OP_SYMB] -> [OP_SYMB])
-> (Constraint -> [OP_SYMB]) -> Constraint -> [OP_SYMB]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((OP_SYMB, [Int]) -> OP_SYMB) -> [(OP_SYMB, [Int])] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map (OP_SYMB, [Int]) -> OP_SYMB
forall a b. (a, b) -> a
fst ([(OP_SYMB, [Int])] -> [OP_SYMB])
-> (Constraint -> [(OP_SYMB, [Int])]) -> Constraint -> [OP_SYMB]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> [(OP_SYMB, [Int])]
opSymbs) [Constraint]
constrs
        toTuple :: OP_SYMB -> (SORT, OpType, [COMPONENTS])
toTuple (Qual_op_name n :: SORT
n ot :: OP_TYPE
ot@(Op_type _ args :: [SORT]
args _ _) _) =
                  (SORT
n, OP_TYPE -> OpType
toOpType OP_TYPE
ot, (SORT -> COMPONENTS) -> [SORT] -> [COMPONENTS]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> COMPONENTS
Sort [SORT]
args)
        toTuple _ = [Char] -> (SORT, OpType, [COMPONENTS])
forall a. HasCallStack => [Char] -> a
error "use qualified names"
        consSymbs' :: [[(SORT, OpType, [COMPONENTS])]]
consSymbs' = ([OP_SYMB] -> [(SORT, OpType, [COMPONENTS])])
-> [[OP_SYMB]] -> [[(SORT, OpType, [COMPONENTS])]]
forall a b. (a -> b) -> [a] -> [b]
map ((OP_SYMB -> (SORT, OpType, [COMPONENTS]))
-> [OP_SYMB] -> [(SORT, OpType, [COMPONENTS])]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> (SORT, OpType, [COMPONENTS])
toTuple) [[OP_SYMB]]
consSymbs
        sortSymbs :: [[OP_SYMB]]
sortSymbs = (Constraint -> [OP_SYMB]) -> [Constraint] -> [[OP_SYMB]]
forall a b. (a -> b) -> [a] -> [b]
map ((OP_SYMB -> Bool) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (OP_SYMB -> Bool) -> OP_SYMB -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_SYMB -> Bool
nonSub) ([OP_SYMB] -> [OP_SYMB])
-> (Constraint -> [OP_SYMB]) -> Constraint -> [OP_SYMB]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((OP_SYMB, [Int]) -> OP_SYMB) -> [(OP_SYMB, [Int])] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map (OP_SYMB, [Int]) -> OP_SYMB
forall a b. (a, b) -> a
fst ([(OP_SYMB, [Int])] -> [OP_SYMB])
-> (Constraint -> [(OP_SYMB, [Int])]) -> Constraint -> [OP_SYMB]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> [(OP_SYMB, [Int])]
opSymbs) [Constraint]
constrs
        getSubsorts :: OP_SYMB -> SORT
getSubsorts (Qual_op_name _ (Op_type _ [ss :: SORT
ss] _ _) _) = SORT
ss
        getSubsorts _ = [Char] -> SORT
forall a. HasCallStack => [Char] -> a
error "error in injSyms"
        sortSymbs' :: [(SORT, [SORT])]
sortSymbs' = ([OP_SYMB] -> (SORT, [SORT])) -> [[OP_SYMB]] -> [(SORT, [SORT])]
forall a b. (a -> b) -> [a] -> [b]
map (\ l :: [OP_SYMB]
l ->
                       case [OP_SYMB]
l of
                        Qual_op_name _ (Op_type _ _ rs :: SORT
rs _) _ : _ ->
                          (SORT
rs, (OP_SYMB -> SORT) -> [OP_SYMB] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> SORT
getSubsorts [OP_SYMB]
l)
                        _ -> [Char] -> (SORT, [SORT])
forall a. HasCallStack => [Char] -> a
error "empty list filtered")
                     ([[OP_SYMB]] -> [(SORT, [SORT])])
-> [[OP_SYMB]] -> [(SORT, [SORT])]
forall a b. (a -> b) -> a -> b
$ ([OP_SYMB] -> Bool) -> [[OP_SYMB]] -> [[OP_SYMB]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([OP_SYMB] -> Bool) -> [OP_SYMB] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OP_SYMB] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [[OP_SYMB]]
sortSymbs
        sortAx :: [Named (FORMULA f)]
sortAx = ((SORT, [SORT]) -> [Named (FORMULA f)])
-> [(SORT, [SORT])] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((SORT -> [SORT] -> [Named (FORMULA f)])
-> (SORT, [SORT]) -> [Named (FORMULA f)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SORT -> [SORT] -> [Named (FORMULA f)]
forall f. SORT -> [SORT] -> [Named (FORMULA f)]
makeDisjSubsorts) [(SORT, [SORT])]
sortSymbs'
        freeAx :: [Named (FORMULA f)]
freeAx = ([(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)])
-> [[(SORT, OpType, [COMPONENTS])]] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ l :: [(SORT, OpType, [COMPONENTS])]
l -> [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
forall f. [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
makeDisjoint [(SORT, OpType, [COMPONENTS])]
l [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++
                              ((SORT, OpType, [COMPONENTS]) -> Named (FORMULA f))
-> [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, OpType, [COMPONENTS]) -> Named (FORMULA f)
forall f. (SORT, OpType, [COMPONENTS]) -> Named (FORMULA f)
makeInjective (
                                  ((SORT, OpType, [COMPONENTS]) -> Bool)
-> [(SORT, OpType, [COMPONENTS])] -> [(SORT, OpType, [COMPONENTS])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, _, x :: [COMPONENTS]
x) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [COMPONENTS] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [COMPONENTS]
x) [(SORT, OpType, [COMPONENTS])]
l))
                   [[(SORT, OpType, [COMPONENTS])]]
consSymbs'
        sameSort :: Constraint -> Constraint -> Bool
sameSort (Constraint s :: SORT
s _ _) (Constraint s' :: SORT
s' _ _) = SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s'
        disjToSortAx :: [Named (FORMULA f)]
disjToSortAx = ([Constraint] -> [Named (FORMULA f)])
-> [[Constraint]] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ ctors :: [Constraint]
ctors -> let
                         cs :: [[OP_SYMB]]
cs = (Constraint -> [OP_SYMB]) -> [Constraint] -> [[OP_SYMB]]
forall a b. (a -> b) -> [a] -> [b]
map (((OP_SYMB, [Int]) -> OP_SYMB) -> [(OP_SYMB, [Int])] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map (OP_SYMB, [Int]) -> OP_SYMB
forall a b. (a, b) -> a
fst ([(OP_SYMB, [Int])] -> [OP_SYMB])
-> (Constraint -> [(OP_SYMB, [Int])]) -> Constraint -> [OP_SYMB]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> [(OP_SYMB, [Int])]
opSymbs) [Constraint]
ctors
                         cSymbs :: [(SORT, OpType, [COMPONENTS])]
cSymbs = ([OP_SYMB] -> [(SORT, OpType, [COMPONENTS])])
-> [[OP_SYMB]] -> [(SORT, OpType, [COMPONENTS])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((OP_SYMB -> (SORT, OpType, [COMPONENTS]))
-> [OP_SYMB] -> [(SORT, OpType, [COMPONENTS])]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> (SORT, OpType, [COMPONENTS])
toTuple
                                             ([OP_SYMB] -> [(SORT, OpType, [COMPONENTS])])
-> ([OP_SYMB] -> [OP_SYMB])
-> [OP_SYMB]
-> [(SORT, OpType, [COMPONENTS])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OP_SYMB -> Bool) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> Bool) -> [a] -> [a]
filter OP_SYMB -> Bool
nonSub) [[OP_SYMB]]
cs
                         sSymbs :: [SORT]
sSymbs = ([OP_SYMB] -> [SORT]) -> [[OP_SYMB]] -> [SORT]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((OP_SYMB -> SORT) -> [OP_SYMB] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> SORT
getSubsorts
                                      ([OP_SYMB] -> [SORT])
-> ([OP_SYMB] -> [OP_SYMB]) -> [OP_SYMB] -> [SORT]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OP_SYMB -> Bool) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (OP_SYMB -> Bool) -> OP_SYMB -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OP_SYMB -> Bool
nonSub)) [[OP_SYMB]]
cs
                         in
                         ((SORT, OpType, [COMPONENTS]) -> [Named (FORMULA f)])
-> [(SORT, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ c :: (SORT, OpType, [COMPONENTS])
c -> (SORT -> Named (FORMULA f)) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map ((SORT, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)
forall f. (SORT, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)
makeDisjToSort (SORT, OpType, [COMPONENTS])
c) [SORT]
sSymbs)
                                   [(SORT, OpType, [COMPONENTS])]
cSymbs) ([[Constraint]] -> [Named (FORMULA f)])
-> [[Constraint]] -> [Named (FORMULA f)]
forall a b. (a -> b) -> a -> b
$ (Constraint -> Constraint -> Bool)
-> [Constraint] -> [[Constraint]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy Constraint -> Constraint -> Bool
sameSort [Constraint]
constrs
    in case [Constraint]
constrs of
     [] -> []
     _ -> [CASLFORMULA -> [SORT] -> Named CASLFORMULA
forall f. FORMULA f -> [SORT] -> Named (FORMULA f)
toSortGenNamed CASLFORMULA
forall f. FORMULA f
f [SORT]
sortList]
           [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
forall f. [Named (FORMULA f)]
freeAx [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
forall f. [Named (FORMULA f)]
sortAx [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
forall f. [Named (FORMULA f)]
disjToSortAx

-- | given the signature in M the function computes the signature K
create_sigma_k :: Set.Set SORT -> CASLSign -> CASLSign
create_sigma_k :: Set SORT -> CASLSign -> CASLSign
create_sigma_k ss :: Set SORT
ss sg_m :: CASLSign
sg_m = CASLSign
usg'
      where iota_sg :: CASLSign
iota_sg = CASLSign -> CASLSign
totalSignCopy CASLSign
sg_m
            usg :: CASLSign
usg = (() -> () -> ()) -> CASLSign -> CASLSign -> CASLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig () -> () -> ()
forall a b. a -> b -> a
const CASLSign
sg_m CASLSign
iota_sg
            om' :: OpMap
om' = Set SORT -> OpMap -> OpMap
homomorphism_ops (CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet CASLSign
sg_m) (CASLSign -> OpMap
forall f e. Sign f e -> OpMap
opMap CASLSign
usg)
            om'' :: OpMap
om'' = Set SORT -> OpMap -> OpMap
make_ops Set SORT
ss OpMap
om'
            usg' :: CASLSign
usg' = CASLSign
usg { opMap :: OpMap
opMap = OpMap
om'' }

{- | adds the make functions for the sorts in the initial module to the
operator map -}
make_ops :: Set.Set SORT -> OpMap -> OpMap
make_ops :: Set SORT -> OpMap -> OpMap
make_ops ss :: Set SORT
ss om :: OpMap
om = (SORT -> OpMap -> OpMap) -> OpMap -> Set SORT -> OpMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold SORT -> OpMap -> OpMap
make_op OpMap
om Set SORT
ss

-- | adds the make functions for the sort to the operator map
make_op :: SORT -> OpMap -> OpMap
make_op :: SORT -> OpMap -> OpMap
make_op s :: SORT
s = SORT -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
makeId (OpType -> OpMap -> OpMap) -> OpType -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ [SORT] -> SORT -> OpType
mkTotOpType [SORT
s] (SORT -> OpType) -> SORT -> OpType
forall a b. (a -> b) -> a -> b
$ SORT -> SORT
mkFreeName SORT
s

-- | identifier of the make function
makeId :: Id
makeId :: SORT
makeId = [VAR] -> SORT
mkId [[Char] -> VAR
mkSimpleId "make"]

-- | identifier of the homomorphism function
homId :: Id
homId :: SORT
homId = [VAR] -> SORT
mkId [[Char] -> VAR
mkSimpleId "hom"]

-- | creates the homomorphism operators and adds it to the given operator map
homomorphism_ops :: Set.Set SORT -> OpMap -> OpMap
homomorphism_ops :: Set SORT -> OpMap -> OpMap
homomorphism_ops ss :: Set SORT
ss om :: OpMap
om = (SORT -> OpMap -> OpMap) -> OpMap -> Set SORT -> OpMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold SORT -> OpMap -> OpMap
f OpMap
om Set SORT
ss
    where ot :: SORT -> OpType
ot sort :: SORT
sort = OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Partial [SORT -> SORT
mkFreeName SORT
sort] SORT
sort
          f :: SORT -> OpMap -> OpMap
f = SORT -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
homId (OpType -> OpMap -> OpMap)
-> (SORT -> OpType) -> SORT -> OpMap -> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> OpType
ot

-- | applies the iota renaming to a signature
totalSignCopy :: CASLSign -> CASLSign
totalSignCopy :: CASLSign -> CASLSign
totalSignCopy sg :: CASLSign
sg = CASLSign
sg {
                    emptySortSet :: Set SORT
emptySortSet = Set SORT
ess,
                    sortRel :: Rel SORT
sortRel = Rel SORT
sr,
                    opMap :: OpMap
opMap = OpMap
om,
                    assocOps :: OpMap
assocOps = OpMap
aom,
                    predMap :: PredMap
predMap = PredMap
pm,
                    varMap :: Map VAR SORT
varMap = Map VAR SORT
vm,
                    sentences :: [Named CASLFORMULA]
sentences = [],
                    declaredSymbols :: Set Symbol
declaredSymbols = Set Symbol
sms,
                    annoMap :: AnnoMap
annoMap = AnnoMap
am
                      }
     where ess :: Set SORT
ess = Set SORT -> Set SORT
iota_sort_set (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ CASLSign -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet CASLSign
sg
           sr :: Rel SORT
sr = Rel SORT -> Rel SORT
iota_sort_rel (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ CASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel CASLSign
sg
           om :: OpMap
om = OpMap -> OpMap
iota_op_map (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ CASLSign -> OpMap
forall f e. Sign f e -> OpMap
opMap CASLSign
sg
           aom :: OpMap
aom = OpMap -> OpMap
iota_op_map (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ CASLSign -> OpMap
forall f e. Sign f e -> OpMap
assocOps CASLSign
sg
           pm :: PredMap
pm = PredMap -> PredMap
iota_pred_map (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ CASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap CASLSign
sg
           vm :: Map VAR SORT
vm = Map VAR SORT -> Map VAR SORT
iota_var_map (Map VAR SORT -> Map VAR SORT) -> Map VAR SORT -> Map VAR SORT
forall a b. (a -> b) -> a -> b
$ CASLSign -> Map VAR SORT
forall f e. Sign f e -> Map VAR SORT
varMap CASLSign
sg
           sms :: Set Symbol
sms = Set Symbol -> Set Symbol
iota_syms (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ CASLSign -> Set Symbol
forall f e. Sign f e -> Set Symbol
declaredSymbols CASLSign
sg
           am :: AnnoMap
am = AnnoMap -> AnnoMap
iota_anno_map (AnnoMap -> AnnoMap) -> AnnoMap -> AnnoMap
forall a b. (a -> b) -> a -> b
$ CASLSign -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap CASLSign
sg

-- | applies the iota renaming to a set of sorts
iota_sort_set :: Set.Set SORT -> Set.Set SORT
iota_sort_set :: Set SORT -> Set SORT
iota_sort_set = (SORT -> SORT) -> Set SORT -> Set SORT
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map SORT -> SORT
mkFreeName

-- | applies the iota renaming to a sort relation
iota_sort_rel :: Rel.Rel SORT -> Rel.Rel SORT
iota_sort_rel :: Rel SORT -> Rel SORT
iota_sort_rel = (SORT -> SORT) -> Rel SORT -> Rel SORT
forall a b. (Ord a, Ord b) => (a -> b) -> Rel a -> Rel b
Rel.map SORT -> SORT
mkFreeName

-- | applies the iota renaming to an operator map
iota_op_map :: OpMap -> OpMap
iota_op_map :: OpMap -> OpMap
iota_op_map = (SORT -> OpType -> OpMap -> OpMap) -> OpMap -> OpMap -> OpMap
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
  (\ op :: SORT
op (OpType _ args :: [SORT]
args res :: SORT
res) -> SORT -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (SORT -> SORT
mkFreeName SORT
op)
       (OpType -> OpMap -> OpMap) -> OpType -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ [SORT] -> SORT -> OpType
mkTotOpType ((SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args) (SORT -> SORT
mkFreeName SORT
res)) OpMap
forall a b. MapSet a b
MapSet.empty

-- | applies the iota renaming to a predicate map
iota_pred_map :: PredMap -> PredMap
iota_pred_map :: PredMap -> PredMap
iota_pred_map = (SORT -> PredType -> PredMap -> PredMap)
-> PredMap -> PredMap -> PredMap
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
  (\ p :: SORT
p (PredType args :: [SORT]
args) -> SORT -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (SORT -> SORT
mkFreeName SORT
p)
       (PredType -> PredMap -> PredMap) -> PredType -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ [SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args) PredMap
forall a b. MapSet a b
MapSet.empty

-- | applies the iota renaming to a variable map
iota_var_map :: Map.Map SIMPLE_ID SORT -> Map.Map SIMPLE_ID SORT
iota_var_map :: Map VAR SORT -> Map VAR SORT
iota_var_map = (SORT -> SORT) -> Map VAR SORT -> Map VAR SORT
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map SORT -> SORT
mkFreeName

-- | applies the iota renaming to symbols
iota_syms :: Set.Set Symbol -> Set.Set Symbol
iota_syms :: Set Symbol -> Set Symbol
iota_syms = (Symbol -> Symbol) -> Set Symbol -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Symbol -> Symbol
iota_symbol

-- | applies the iota renaming to a symbol
iota_symbol :: Symbol -> Symbol
iota_symbol :: Symbol -> Symbol
iota_symbol (Symbol name :: SORT
name ty :: SymbType
ty) = SORT -> SymbType -> Symbol
Symbol (SORT -> SORT
mkFreeName SORT
name) (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ case SymbType
ty of
  SortAsItemType -> SymbType
SortAsItemType
  SubsortAsItemType s :: SORT
s -> SORT -> SymbType
SubsortAsItemType (SORT -> SymbType) -> SORT -> SymbType
forall a b. (a -> b) -> a -> b
$ SORT -> SORT
mkFreeName SORT
s
  OpAsItemType (OpType _ args :: [SORT]
args res :: SORT
res) -> OpType -> SymbType
OpAsItemType
    (OpType -> SymbType) -> OpType -> SymbType
forall a b. (a -> b) -> a -> b
$ [SORT] -> SORT -> OpType
mkTotOpType ((SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args) (SORT -> SORT
mkFreeName SORT
res)
  PredAsItemType (PredType args :: [SORT]
args) -> PredType -> SymbType
PredAsItemType
    (PredType -> SymbType) -> PredType -> SymbType
forall a b. (a -> b) -> a -> b
$ [SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args

-- | applies the iota renaming to the annotations
iota_anno_map :: MapSet.MapSet Symbol Annotation
  -> MapSet.MapSet Symbol Annotation
iota_anno_map :: AnnoMap -> AnnoMap
iota_anno_map = Map Symbol (Set Annotation) -> AnnoMap
forall a b. Ord a => Map a (Set b) -> MapSet a b
MapSet.fromMap (Map Symbol (Set Annotation) -> AnnoMap)
-> (AnnoMap -> Map Symbol (Set Annotation)) -> AnnoMap -> AnnoMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Symbol)
-> Map Symbol (Set Annotation) -> Map Symbol (Set Annotation)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Symbol -> Symbol
iota_symbol (Map Symbol (Set Annotation) -> Map Symbol (Set Annotation))
-> (AnnoMap -> Map Symbol (Set Annotation))
-> AnnoMap
-> Map Symbol (Set Annotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnoMap -> Map Symbol (Set Annotation)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap

-- Some auxiliary functions

-- | create a new name for the iota morphism
mkFreeName :: Id -> Id
mkFreeName :: SORT -> SORT
mkFreeName i :: SORT
i@(Id ts :: [VAR]
ts cs :: [SORT]
cs r :: Range
r) = case [VAR]
ts of
  t :: VAR
t : s :: [VAR]
s -> let st :: [Char]
st = VAR -> [Char]
tokStr VAR
t in case [Char]
st of
    c :: Char
c : _ | Char -> Bool
isAlphaNum Char
c -> [VAR] -> [SORT] -> Range -> SORT
Id ([Char] -> VAR
freeToken [Char]
st VAR -> [VAR] -> [VAR]
forall a. a -> [a] -> [a]
: [VAR]
s) [SORT]
cs Range
r
          | Bool
otherwise -> [VAR] -> [SORT] -> Range -> SORT
Id [[Char] -> VAR
mkSimpleId "gn_free"] [SORT
i] Range
r
    _ -> [VAR] -> [SORT] -> Range -> SORT
Id ([Char] -> VAR
mkSimpleId "gn_free_f" VAR -> [VAR] -> [VAR]
forall a. a -> [a] -> [a]
: [VAR]
ts) [SORT]
cs Range
r
  _ -> SORT
i

-- | a prefix for free names
freeNamePrefix :: String
freeNamePrefix :: [Char]
freeNamePrefix = "gn_free_"

-- | create a generated simple identifier
freeToken :: String -> Token
freeToken :: [Char] -> VAR
freeToken str :: [Char]
str = [Char] -> VAR
mkSimpleId ([Char] -> VAR) -> [Char] -> VAR
forall a b. (a -> b) -> a -> b
$ [Char]
freeNamePrefix [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
str

-- | obtains the sorts of the given list of term
getSorts :: [CASLTERM] -> [SORT]
getSorts :: [CASLTERM] -> [SORT]
getSorts = (CASLTERM -> Maybe SORT) -> [CASLTERM] -> [SORT]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe CASLTERM -> Maybe SORT
getSort

-- | compute the sort of the term, if possible
getSort :: CASLTERM -> Maybe SORT
getSort :: CASLTERM -> Maybe SORT
getSort (Qual_var _ kind :: SORT
kind _) = SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
kind
getSort (Application op :: OP_SYMB
op _ _) = case OP_SYMB
op of
            Qual_op_name _ (Op_type _ _ kind :: SORT
kind _) _ -> SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
kind
            _ -> Maybe SORT
forall a. Maybe a
Nothing
getSort _ = Maybe SORT
forall a. Maybe a
Nothing

-- | extracts the predicate name from the predicate symbol
pred_symb_name :: PRED_SYMB -> PRED_NAME
pred_symb_name :: PRED_SYMB -> SORT
pred_symb_name (Pred_name pn :: SORT
pn) = SORT
pn
pred_symb_name (Qual_pred_name pn :: SORT
pn _ _) = SORT
pn

{- | extract the variables from a CASL formula and put them in a map
with keys the sort of the variables and value the set of variables
in this sort -}
getVars :: CASLFORMULA -> Map.Map Id (Set.Set Token)
getVars :: CASLFORMULA -> Map SORT (Set VAR)
getVars (Quantification _ _ f :: CASLFORMULA
f _) = CASLFORMULA -> Map SORT (Set VAR)
getVars CASLFORMULA
f
getVars (QuantOp _ _ f :: CASLFORMULA
f) = CASLFORMULA -> Map SORT (Set VAR)
getVars CASLFORMULA
f
getVars (QuantPred _ _ f :: CASLFORMULA
f) = CASLFORMULA -> Map SORT (Set VAR)
getVars CASLFORMULA
f
getVars (Junction _ fs :: [CASLFORMULA]
fs _) =
    (CASLFORMULA -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> Map SORT (Set VAR) -> [CASLFORMULA] -> Map SORT (Set VAR)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> (CASLFORMULA -> Map SORT (Set VAR))
-> CASLFORMULA
-> Map SORT (Set VAR)
-> Map SORT (Set VAR)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> Map SORT (Set VAR)
getVars) Map SORT (Set VAR)
forall k a. Map k a
Map.empty [CASLFORMULA]
fs
getVars (Relation f1 :: CASLFORMULA
f1 _ f2 :: CASLFORMULA
f2 _) = (Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union Map SORT (Set VAR)
v1 Map SORT (Set VAR)
v2
     where v1 :: Map SORT (Set VAR)
v1 = CASLFORMULA -> Map SORT (Set VAR)
getVars CASLFORMULA
f1
           v2 :: Map SORT (Set VAR)
v2 = CASLFORMULA -> Map SORT (Set VAR)
getVars CASLFORMULA
f2
getVars (Negation f :: CASLFORMULA
f _) = CASLFORMULA -> Map SORT (Set VAR)
getVars CASLFORMULA
f
getVars (Predication _ ts :: [CASLTERM]
ts _) =
    (CASLTERM -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> Map SORT (Set VAR) -> [CASLTERM] -> Map SORT (Set VAR)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> (CASLTERM -> Map SORT (Set VAR))
-> CASLTERM
-> Map SORT (Set VAR)
-> Map SORT (Set VAR)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLTERM -> Map SORT (Set VAR)
getVarsTerm) Map SORT (Set VAR)
forall k a. Map k a
Map.empty [CASLTERM]
ts
getVars (Definedness t :: CASLTERM
t _) = CASLTERM -> Map SORT (Set VAR)
getVarsTerm CASLTERM
t
getVars (Equation t1 :: CASLTERM
t1 _ t2 :: CASLTERM
t2 _) = (Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union Map SORT (Set VAR)
v1 Map SORT (Set VAR)
v2
     where v1 :: Map SORT (Set VAR)
v1 = CASLTERM -> Map SORT (Set VAR)
getVarsTerm CASLTERM
t1
           v2 :: Map SORT (Set VAR)
v2 = CASLTERM -> Map SORT (Set VAR)
getVarsTerm CASLTERM
t2
getVars (Membership t :: CASLTERM
t _ _) = CASLTERM -> Map SORT (Set VAR)
getVarsTerm CASLTERM
t
getVars (Mixfix_formula t :: CASLTERM
t) = CASLTERM -> Map SORT (Set VAR)
getVarsTerm CASLTERM
t
getVars _ = Map SORT (Set VAR)
forall k a. Map k a
Map.empty

-- | extract the variables of a CASL term
getVarsTerm :: CASLTERM -> Map.Map Id (Set.Set Token)
getVarsTerm :: CASLTERM -> Map SORT (Set VAR)
getVarsTerm (Qual_var var :: VAR
var sort :: SORT
sort _) =
    SORT -> Set VAR -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SORT
sort (VAR -> Set VAR
forall a. a -> Set a
Set.singleton VAR
var) Map SORT (Set VAR)
forall k a. Map k a
Map.empty
getVarsTerm (Application _ ts :: [CASLTERM]
ts _) =
    (CASLTERM -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> Map SORT (Set VAR) -> [CASLTERM] -> Map SORT (Set VAR)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> (CASLTERM -> Map SORT (Set VAR))
-> CASLTERM
-> Map SORT (Set VAR)
-> Map SORT (Set VAR)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLTERM -> Map SORT (Set VAR)
getVarsTerm) Map SORT (Set VAR)
forall k a. Map k a
Map.empty [CASLTERM]
ts
getVarsTerm (Sorted_term t :: CASLTERM
t _ _) = CASLTERM -> Map SORT (Set VAR)
getVarsTerm CASLTERM
t
getVarsTerm (Cast t :: CASLTERM
t _ _) = CASLTERM -> Map SORT (Set VAR)
getVarsTerm CASLTERM
t
getVarsTerm (Conditional t1 :: CASLTERM
t1 f :: CASLFORMULA
f t2 :: CASLTERM
t2 _) = (Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union Map SORT (Set VAR)
v3 Map SORT (Set VAR)
m
     where v1 :: Map SORT (Set VAR)
v1 = CASLTERM -> Map SORT (Set VAR)
getVarsTerm CASLTERM
t1
           v2 :: Map SORT (Set VAR)
v2 = CASLTERM -> Map SORT (Set VAR)
getVarsTerm CASLTERM
t2
           v3 :: Map SORT (Set VAR)
v3 = CASLFORMULA -> Map SORT (Set VAR)
getVars CASLFORMULA
f
           m :: Map SORT (Set VAR)
m = (Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union Map SORT (Set VAR)
v1 Map SORT (Set VAR)
v2
getVarsTerm (Mixfix_term ts :: [CASLTERM]
ts) =
    (CASLTERM -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> Map SORT (Set VAR) -> [CASLTERM] -> Map SORT (Set VAR)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> (CASLTERM -> Map SORT (Set VAR))
-> CASLTERM
-> Map SORT (Set VAR)
-> Map SORT (Set VAR)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLTERM -> Map SORT (Set VAR)
getVarsTerm) Map SORT (Set VAR)
forall k a. Map k a
Map.empty [CASLTERM]
ts
getVarsTerm (Mixfix_parenthesized ts :: [CASLTERM]
ts _) =
    (CASLTERM -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> Map SORT (Set VAR) -> [CASLTERM] -> Map SORT (Set VAR)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> (CASLTERM -> Map SORT (Set VAR))
-> CASLTERM
-> Map SORT (Set VAR)
-> Map SORT (Set VAR)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLTERM -> Map SORT (Set VAR)
getVarsTerm) Map SORT (Set VAR)
forall k a. Map k a
Map.empty [CASLTERM]
ts
getVarsTerm (Mixfix_bracketed ts :: [CASLTERM]
ts _) =
    (CASLTERM -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> Map SORT (Set VAR) -> [CASLTERM] -> Map SORT (Set VAR)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> (CASLTERM -> Map SORT (Set VAR))
-> CASLTERM
-> Map SORT (Set VAR)
-> Map SORT (Set VAR)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLTERM -> Map SORT (Set VAR)
getVarsTerm) Map SORT (Set VAR)
forall k a. Map k a
Map.empty [CASLTERM]
ts
getVarsTerm (Mixfix_braced ts :: [CASLTERM]
ts _) =
    (CASLTERM -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> Map SORT (Set VAR) -> [CASLTERM] -> Map SORT (Set VAR)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set VAR -> Set VAR -> Set VAR)
-> Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set VAR -> Set VAR -> Set VAR
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map SORT (Set VAR) -> Map SORT (Set VAR) -> Map SORT (Set VAR))
-> (CASLTERM -> Map SORT (Set VAR))
-> CASLTERM
-> Map SORT (Set VAR)
-> Map SORT (Set VAR)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLTERM -> Map SORT (Set VAR)
getVarsTerm) Map SORT (Set VAR)
forall k a. Map k a
Map.empty [CASLTERM]
ts
getVarsTerm _ = Map SORT (Set VAR)
forall k a. Map k a
Map.empty

-- | add universal quantification of all variables in the formula
quantifyUniversally :: CASLFORMULA -> CASLFORMULA
quantifyUniversally :: CASLFORMULA -> CASLFORMULA
quantifyUniversally form :: CASLFORMULA
form = if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
var_decl
                           then CASLFORMULA
form
                           else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [VAR_DECL]
var_decl CASLFORMULA
form Range
nullRange
      where vars :: Map SORT (Set VAR)
vars = CASLFORMULA -> Map SORT (Set VAR)
getVars CASLFORMULA
form
            var_decl :: [VAR_DECL]
var_decl = Map SORT (Set VAR) -> [VAR_DECL]
listVarDecl Map SORT (Set VAR)
vars

{- | traverses a map with sorts as keys and sets of variables as value
and creates a list of variable declarations -}
listVarDecl :: Map.Map Id (Set.Set Token) -> [VAR_DECL]
listVarDecl :: Map SORT (Set VAR) -> [VAR_DECL]
listVarDecl = (SORT -> Set VAR -> [VAR_DECL] -> [VAR_DECL])
-> [VAR_DECL] -> Map SORT (Set VAR) -> [VAR_DECL]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey SORT -> Set VAR -> [VAR_DECL] -> [VAR_DECL]
f []
      where f :: SORT -> Set VAR -> [VAR_DECL] -> [VAR_DECL]
f sort :: SORT
sort var_set :: Set VAR
var_set = ([VAR] -> SORT -> Range -> VAR_DECL
Var_decl (Set VAR -> [VAR]
forall a. Set a -> [a]
Set.toList Set VAR
var_set) SORT
sort Range
nullRange VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
:)

-- | generates a new variable qualified with the given number
newVarIndex :: Int -> SORT -> CASLTERM
newVarIndex :: Int -> SORT -> CASLTERM
newVarIndex i :: Int
i sort :: SORT
sort = VAR -> SORT -> Range -> CASLTERM
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
var SORT
sort Range
nullRange
    where var :: VAR
var = [Char] -> VAR
mkSimpleId ([Char] -> VAR) -> [Char] -> VAR
forall a b. (a -> b) -> a -> b
$ 'V' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i

-- | generates a new variable
newVar :: SORT -> CASLTERM
newVar :: SORT -> CASLTERM
newVar sort :: SORT
sort = VAR -> SORT -> Range -> CASLTERM
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
var SORT
sort Range
nullRange
    where var :: VAR
var = [Char] -> VAR
mkSimpleId "V"

-- | generates the free representation of an OP_SYMB
free_op_sym :: OP_SYMB -> OP_SYMB
free_op_sym :: OP_SYMB -> OP_SYMB
free_op_sym (Op_name on :: SORT
on) = SORT -> OP_SYMB
Op_name (SORT -> OP_SYMB) -> SORT -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ SORT -> SORT
mkFreeName SORT
on
free_op_sym (Qual_op_name on :: SORT
on ot :: OP_TYPE
ot r :: Range
r) = SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
on' OP_TYPE
ot' Range
r
     where on' :: SORT
on' = SORT -> SORT
mkFreeName SORT
on
           ot' :: OP_TYPE
ot' = OP_TYPE -> OP_TYPE
free_op_type OP_TYPE
ot

-- | generates the free representation of an OP_TYPE
free_op_type :: OP_TYPE -> OP_TYPE
free_op_type :: OP_TYPE -> OP_TYPE
free_op_type (Op_type _ args :: [SORT]
args res :: SORT
res r :: Range
r) = OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [SORT]
args' SORT
res' Range
r
     where args' :: [SORT]
args' = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args
           res' :: SORT
res' = SORT -> SORT
mkFreeName SORT
res

-- | generates the free representation of a PRED_SYMB
free_pred_sym :: PRED_SYMB -> PRED_SYMB
free_pred_sym :: PRED_SYMB -> PRED_SYMB
free_pred_sym (Pred_name pn :: SORT
pn) = SORT -> PRED_SYMB
Pred_name (SORT -> PRED_SYMB) -> SORT -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ SORT -> SORT
mkFreeName SORT
pn
free_pred_sym (Qual_pred_name pn :: SORT
pn pt :: PRED_TYPE
pt r :: Range
r) = SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
pn' PRED_TYPE
pt' Range
r
     where pn' :: SORT
pn' = SORT -> SORT
mkFreeName SORT
pn
           pt' :: PRED_TYPE
pt' = PRED_TYPE -> PRED_TYPE
free_pred_type PRED_TYPE
pt

-- | generates the free representation of a PRED_TYPE
free_pred_type :: PRED_TYPE -> PRED_TYPE
free_pred_type :: PRED_TYPE -> PRED_TYPE
free_pred_type (Pred_type args :: [SORT]
args r :: Range
r) = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
args' Range
r
     where args' :: [SORT]
args' = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
args

-- | generates the free representation of a CASLTERM
free_term :: CASLTERM -> CASLTERM
free_term :: CASLTERM -> CASLTERM
free_term (Qual_var v :: VAR
v s :: SORT
s r :: Range
r) = VAR -> SORT -> Range -> CASLTERM
forall f. VAR -> SORT -> Range -> TERM f
Qual_var VAR
v (SORT -> SORT
mkFreeName SORT
s) Range
r
free_term (Application os :: OP_SYMB
os ts :: [CASLTERM]
ts r :: Range
r) = OP_SYMB -> [CASLTERM] -> Range -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
os' [CASLTERM]
ts' Range
r
     where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
free_term [CASLTERM]
ts
           os' :: OP_SYMB
os' = OP_SYMB -> OP_SYMB
free_op_sym OP_SYMB
os
free_term (Sorted_term t :: CASLTERM
t s :: SORT
s r :: Range
r) = CASLTERM -> SORT -> Range -> CASLTERM
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term CASLTERM
t' SORT
s' Range
r
     where t' :: CASLTERM
t' = CASLTERM -> CASLTERM
free_term CASLTERM
t
           s' :: SORT
s' = SORT -> SORT
mkFreeName SORT
s
free_term (Cast t :: CASLTERM
t s :: SORT
s r :: Range
r) = CASLTERM -> SORT -> Range -> CASLTERM
forall f. TERM f -> SORT -> Range -> TERM f
Cast CASLTERM
t' SORT
s' Range
r
     where t' :: CASLTERM
t' = CASLTERM -> CASLTERM
free_term CASLTERM
t
           s' :: SORT
s' = SORT -> SORT
mkFreeName SORT
s
free_term (Conditional t1 :: CASLTERM
t1 f :: CASLFORMULA
f t2 :: CASLTERM
t2 r :: Range
r) = CASLTERM -> CASLFORMULA -> CASLTERM -> Range -> CASLTERM
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional CASLTERM
t1' CASLFORMULA
f' CASLTERM
t2' Range
r
     where t1' :: CASLTERM
t1' = CASLTERM -> CASLTERM
free_term CASLTERM
t1
           t2' :: CASLTERM
t2' = CASLTERM -> CASLTERM
free_term CASLTERM
t2
           f' :: CASLFORMULA
f' = CASLFORMULA -> CASLFORMULA
free_formula CASLFORMULA
f
free_term (Mixfix_qual_pred ps :: PRED_SYMB
ps) = PRED_SYMB -> CASLTERM
forall f. PRED_SYMB -> TERM f
Mixfix_qual_pred PRED_SYMB
ps'
     where ps' :: PRED_SYMB
ps' = PRED_SYMB -> PRED_SYMB
free_pred_sym PRED_SYMB
ps
free_term (Mixfix_term ts :: [CASLTERM]
ts) = [CASLTERM] -> CASLTERM
forall f. [TERM f] -> TERM f
Mixfix_term [CASLTERM]
ts'
     where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
free_term [CASLTERM]
ts
free_term (Mixfix_sorted_term s :: SORT
s r :: Range
r) = SORT -> Range -> CASLTERM
forall f. SORT -> Range -> TERM f
Mixfix_sorted_term SORT
s' Range
r
     where s' :: SORT
s' = SORT -> SORT
mkFreeName SORT
s
free_term (Mixfix_cast s :: SORT
s r :: Range
r) = SORT -> Range -> CASLTERM
forall f. SORT -> Range -> TERM f
Mixfix_cast SORT
s' Range
r
     where s' :: SORT
s' = SORT -> SORT
mkFreeName SORT
s
free_term (Mixfix_parenthesized ts :: [CASLTERM]
ts r :: Range
r) = [CASLTERM] -> Range -> CASLTERM
forall f. [TERM f] -> Range -> TERM f
Mixfix_parenthesized [CASLTERM]
ts' Range
r
     where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
free_term [CASLTERM]
ts
free_term (Mixfix_bracketed ts :: [CASLTERM]
ts r :: Range
r) = [CASLTERM] -> Range -> CASLTERM
forall f. [TERM f] -> Range -> TERM f
Mixfix_bracketed [CASLTERM]
ts' Range
r
     where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
free_term [CASLTERM]
ts
free_term (Mixfix_braced ts :: [CASLTERM]
ts r :: Range
r) = [CASLTERM] -> Range -> CASLTERM
forall f. [TERM f] -> Range -> TERM f
Mixfix_braced [CASLTERM]
ts' Range
r
     where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
free_term [CASLTERM]
ts
free_term t :: CASLTERM
t = CASLTERM
t

-- | generates the free representation of a list of variable declarations
free_var_decls :: [VAR_DECL] -> [VAR_DECL]
free_var_decls :: [VAR_DECL] -> [VAR_DECL]
free_var_decls = (VAR_DECL -> VAR_DECL) -> [VAR_DECL] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> VAR_DECL
free_var_decl

-- | generates the free representation of a variable declaration
free_var_decl :: VAR_DECL -> VAR_DECL
free_var_decl :: VAR_DECL -> VAR_DECL
free_var_decl (Var_decl vs :: [VAR]
vs s :: SORT
s r :: Range
r) = [VAR] -> SORT -> Range -> VAR_DECL
Var_decl [VAR]
vs SORT
s' Range
r
     where s' :: SORT
s' = SORT -> SORT
mkFreeName SORT
s

{- | computes the substitution needed for the kernel of h to the
sentences of the theory of M -}
free_formula :: CASLFORMULA -> CASLFORMULA
free_formula :: CASLFORMULA -> CASLFORMULA
free_formula (Quantification q :: QUANTIFIER
q vs :: [VAR_DECL]
vs f :: CASLFORMULA
f r :: Range
r) = QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vs' CASLFORMULA
f' Range
r
     where vs' :: [VAR_DECL]
vs' = [VAR_DECL] -> [VAR_DECL]
free_var_decls [VAR_DECL]
vs
           f' :: CASLFORMULA
f' = CASLFORMULA -> CASLFORMULA
free_formula CASLFORMULA
f
free_formula (Junction j :: Junctor
j fs :: [CASLFORMULA]
fs r :: Range
r) = Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j [CASLFORMULA]
fs' Range
r
     where fs' :: [CASLFORMULA]
fs' = (CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map CASLFORMULA -> CASLFORMULA
free_formula [CASLFORMULA]
fs
free_formula (Relation f1 :: CASLFORMULA
f1 c :: Relation
c f2 :: CASLFORMULA
f2 r :: Range
r) = CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
f1' Relation
c CASLFORMULA
f2' Range
r
     where f1' :: CASLFORMULA
f1' = CASLFORMULA -> CASLFORMULA
free_formula CASLFORMULA
f1
           f2' :: CASLFORMULA
f2' = CASLFORMULA -> CASLFORMULA
free_formula CASLFORMULA
f2
free_formula (Negation f :: CASLFORMULA
f r :: Range
r) = CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
f' Range
r
     where f' :: CASLFORMULA
f' = CASLFORMULA -> CASLFORMULA
free_formula CASLFORMULA
f
free_formula (Predication ps :: PRED_SYMB
ps ts :: [CASLTERM]
ts r :: Range
r) = CASLFORMULA
pr
     where ss :: [SORT]
ss = [CASLTERM] -> [SORT]
getSorts [CASLTERM]
ts
           free_ss :: [SORT]
free_ss = (SORT -> SORT) -> [SORT] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> SORT
mkFreeName [SORT]
ss
           ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
free_term [CASLTERM]
ts
           psi :: SORT
psi = SORT -> SORT
psiName (SORT -> SORT) -> SORT -> SORT
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> SORT
pred_symb_name PRED_SYMB
ps
           pt :: PRED_TYPE
pt = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT]
free_ss Range
nullRange
           ps' :: PRED_SYMB
ps' = SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
psi PRED_TYPE
pt Range
nullRange
           pr :: CASLFORMULA
pr = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
ps' [CASLTERM]
ts' Range
r
free_formula (Definedness t :: CASLTERM
t r :: Range
r) = case Maybe SORT
sort of
        Nothing -> CASLTERM -> Range -> CASLFORMULA
forall f. TERM f -> Range -> FORMULA f
Definedness CASLTERM
t' Range
r
        Just s :: SORT
s -> PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication (SORT -> PRED_SYMB
freePredSymb SORT
s) [CASLTERM
t', CASLTERM
t']
     where t' :: CASLTERM
t' = CASLTERM -> CASLTERM
free_term CASLTERM
t
           sort :: Maybe SORT
sort = CASLTERM -> Maybe SORT
getSort CASLTERM
t
free_formula (Equation t1 :: CASLTERM
t1 e :: Equality
e t2 :: CASLTERM
t2 r :: Range
r) = let
     t1' :: CASLTERM
t1' = CASLTERM -> CASLTERM
free_term CASLTERM
t1
     t2' :: CASLTERM
t2' = CASLTERM -> CASLTERM
free_term CASLTERM
t2
     sort :: Maybe SORT
sort = CASLTERM -> Maybe SORT
getSort CASLTERM
t1
     in case Maybe SORT
sort of
        Nothing -> CASLTERM -> Equality -> CASLTERM -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation CASLTERM
t1' Equality
e CASLTERM
t2' Range
r
        Just s :: SORT
s -> let
            ps :: PRED_SYMB
ps = SORT -> PRED_SYMB
freePredSymb SORT
s
            pred1 :: CASLFORMULA
pred1 = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
t1', CASLTERM
t2']
            pred2 :: CASLFORMULA
pred2 = CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
t1', CASLTERM
t1']
            pred3 :: CASLFORMULA
pred3 = CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
ps [CASLTERM
t2', CASLTERM
t2']
            pred4 :: CASLFORMULA
pred4 = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA
pred2, CASLFORMULA
pred3]
            pred5 :: CASLFORMULA
pred5 = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct [CASLFORMULA
pred1, CASLFORMULA
pred4]
            in if Equality
e Equality -> Equality -> Bool
forall a. Eq a => a -> a -> Bool
== Equality
Existl then CASLFORMULA
pred1 else CASLFORMULA
pred5
free_formula (Membership t :: CASLTERM
t s :: SORT
s r :: Range
r) = CASLTERM -> SORT -> Range -> CASLFORMULA
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership CASLTERM
t' SORT
s' Range
r
     where t' :: CASLTERM
t' = CASLTERM -> CASLTERM
free_term CASLTERM
t
           s' :: SORT
s' = SORT -> SORT
mkFreeName SORT
s
free_formula (Mixfix_formula t :: CASLTERM
t) = CASLTERM -> CASLFORMULA
forall f. TERM f -> FORMULA f
Mixfix_formula CASLTERM
t'
     where t' :: CASLTERM
t' = CASLTERM -> CASLTERM
free_term CASLTERM
t
free_formula (QuantOp on :: SORT
on ot :: OP_TYPE
ot f :: CASLFORMULA
f) = SORT -> OP_TYPE -> CASLFORMULA -> CASLFORMULA
forall f. SORT -> OP_TYPE -> FORMULA f -> FORMULA f
QuantOp SORT
on' OP_TYPE
ot' CASLFORMULA
f'
     where on' :: SORT
on' = SORT -> SORT
mkFreeName SORT
on
           ot' :: OP_TYPE
ot' = OP_TYPE -> OP_TYPE
free_op_type OP_TYPE
ot
           f' :: CASLFORMULA
f' = CASLFORMULA -> CASLFORMULA
free_formula CASLFORMULA
f
free_formula (QuantPred pn :: SORT
pn pt :: PRED_TYPE
pt f :: CASLFORMULA
f) = SORT -> PRED_TYPE -> CASLFORMULA -> CASLFORMULA
forall f. SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred SORT
pn' PRED_TYPE
pt' CASLFORMULA
f'
     where pn' :: SORT
pn' = SORT -> SORT
mkFreeName SORT
pn
           pt' :: PRED_TYPE
pt' = PRED_TYPE -> PRED_TYPE
free_pred_type PRED_TYPE
pt
           f' :: CASLFORMULA
f' = CASLFORMULA -> CASLFORMULA
free_formula CASLFORMULA
f
free_formula f :: CASLFORMULA
f = CASLFORMULA
f