{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CSMOF2CASL.hs
Description :  Coding CSMOF into CASL
Copyright   :  (c) Daniel Calegari Universidad de la Republica, Uruguay 2013
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  dcalegar@fing.edu.uy
Stability   :  provisional
Portability :  portable
-}


module Comorphisms.CSMOF2CASL
    ( CSMOF2CASL (..), mapSign, generateVars
    ) where

import Logic.Logic
import Logic.Comorphism
import Common.DefaultMorphism

-- CSMOF
import CSMOF.Logic_CSMOF as CSMOF
import CSMOF.As as CSMOFAs
import CSMOF.Sign as CSMOF

-- CASL
import CASL.Logic_CASL
import CASL.AS_Basic_CASL as C
import CASL.Sublogic
import CASL.Sign as C
import CASL.Morphism as C

import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.Id
import Common.ProofTree
import Common.Result

import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet

import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)

-- | lid of the morphism
data CSMOF2CASL = CSMOF2CASL deriving Int -> CSMOF2CASL -> ShowS
[CSMOF2CASL] -> ShowS
CSMOF2CASL -> String
(Int -> CSMOF2CASL -> ShowS)
-> (CSMOF2CASL -> String)
-> ([CSMOF2CASL] -> ShowS)
-> Show CSMOF2CASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CSMOF2CASL] -> ShowS
$cshowList :: [CSMOF2CASL] -> ShowS
show :: CSMOF2CASL -> String
$cshow :: CSMOF2CASL -> String
showsPrec :: Int -> CSMOF2CASL -> ShowS
$cshowsPrec :: Int -> CSMOF2CASL -> ShowS
Show

instance Language CSMOF2CASL -- default is ok

instance Comorphism CSMOF2CASL
    CSMOF.CSMOF
    ()
    CSMOFAs.Metamodel
    CSMOF.Sen
    ()
    ()
    CSMOF.Sign
    CSMOF.Morphism
    ()
    ()
    ()
    CASL
    CASL_Sublogics
    CASLBasicSpec
    CASLFORMULA
    SYMB_ITEMS
    SYMB_MAP_ITEMS
    CASLSign
    CASLMor
    C.Symbol
    C.RawSymbol
    ProofTree
    where
      sourceLogic :: CSMOF2CASL -> CSMOF
sourceLogic CSMOF2CASL = CSMOF
CSMOF
      sourceSublogic :: CSMOF2CASL -> ()
sourceSublogic CSMOF2CASL = ()
      targetLogic :: CSMOF2CASL -> CASL
targetLogic CSMOF2CASL = CASL
CASL
      mapSublogic :: CSMOF2CASL -> () -> Maybe CASL_Sublogics
mapSublogic CSMOF2CASL _ = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just (CASL_Sublogics -> Maybe CASL_Sublogics)
-> CASL_Sublogics -> Maybe CASL_Sublogics
forall a b. (a -> b) -> a -> b
$ CASL_Sublogics
forall a. Lattice a => CASL_SL a
caslTop
        { has_part :: Bool
has_part = Bool
False
        , sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub
        , cons_features :: SortGenerationFeatures
cons_features = Bool -> Bool -> SortGenTotality -> SortGenerationFeatures
SortGen Bool
True Bool
True SortGenTotality
OnlyFree }
      map_theory :: CSMOF2CASL
-> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
map_theory CSMOF2CASL = (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory
      map_sentence :: CSMOF2CASL -> Sign -> Sen -> Result CASLFORMULA
map_sentence CSMOF2CASL s :: Sign
s = CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> (Sen -> CASLFORMULA) -> Sen -> Result CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLSign -> Sen -> CASLFORMULA
mapSen (Sign -> CASLSign
mapSign Sign
s)
      map_morphism :: CSMOF2CASL -> Morphism -> Result CASLMor
map_morphism CSMOF2CASL = Morphism -> Result CASLMor
mapMor
      -- map_symbol CSMOF2CASL _ = Set.singleton . mapSym
      is_model_transportable :: CSMOF2CASL -> Bool
is_model_transportable CSMOF2CASL = Bool
True
      has_model_expansion :: CSMOF2CASL -> Bool
has_model_expansion CSMOF2CASL = Bool
True
      is_weakly_amalgamable :: CSMOF2CASL -> Bool
is_weakly_amalgamable CSMOF2CASL = Bool
True
      isInclusionComorphism :: CSMOF2CASL -> Bool
isInclusionComorphism CSMOF2CASL = Bool
True


mapTheory :: (CSMOF.Sign, [Named CSMOF.Sen]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory :: (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory (s :: Sign
s, ns :: [Named Sen]
ns) = let cs :: CASLSign
cs = Sign -> CASLSign
mapSign Sign
s in
  (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
cs, (Named Sen -> Named CASLFORMULA)
-> [Named Sen] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((Sen -> CASLFORMULA) -> Named Sen -> Named CASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((Sen -> CASLFORMULA) -> Named Sen -> Named CASLFORMULA)
-> (Sen -> CASLFORMULA) -> Named Sen -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLSign -> Sen -> CASLFORMULA
mapSen CASLSign
cs) [Named Sen]
ns [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ CASLSign -> [Named CASLFORMULA]
forall f e. Sign f e -> [Named (FORMULA f)]
sentences CASLSign
cs)


mapSign :: CSMOF.Sign -> CASLSign
mapSign :: Sign -> CASLSign
mapSign s :: Sign
s =
  let
    sorts :: Rel SORT
sorts = Set TypeClass -> Rel TypeClass -> Rel SORT
getSorts (Sign -> Set TypeClass
types Sign
s) (Sign -> Rel TypeClass
typeRel Sign
s)
    ops :: OpMap
ops = Map String TypeClass -> OpMap
getOperations (Sign -> Map String TypeClass
instances Sign
s)
    predd :: (PredMap, [Named (FORMULA f)])
predd = Set PropertyT -> (PredMap, [Named (FORMULA f)])
forall f. Set PropertyT -> (PredMap, [Named (FORMULA f)])
getPredicates (Sign -> Set PropertyT
properties Sign
s)
    sent :: [Named CASLFORMULA]
sent = Set LinkT -> Map String TypeClass -> [Named CASLFORMULA]
getSentencesRels (Sign -> Set LinkT
links Sign
s) (Sign -> Map String TypeClass
instances Sign
s)
    sentDisEmb :: [Named CASLFORMULA]
sentDisEmb = Rel TypeClass
-> Set TypeClass
-> Set TypeClass
-> Map String TypeClass
-> [Named CASLFORMULA]
getSortGen (Sign -> Rel TypeClass
typeRel Sign
s) (Sign -> Set TypeClass
abstractClasses Sign
s) (Sign -> Set TypeClass
types Sign
s) (Sign -> Map String TypeClass
instances Sign
s)
    noConfBetOps :: [Named CASLFORMULA]
noConfBetOps = Map String TypeClass -> Rel TypeClass -> [Named CASLFORMULA]
getNoConfusionBetweenSets (Sign -> Map String TypeClass
instances Sign
s) (Sign -> Rel TypeClass
typeRel Sign
s)
  in
    Sign :: forall f e.
Rel SORT
-> Maybe (Rel SORT)
-> Set SORT
-> OpMap
-> OpMap
-> PredMap
-> Map SIMPLE_ID SORT
-> [Named (FORMULA f)]
-> Set Symbol
-> [Diagnosis]
-> AnnoMap
-> GlobalAnnos
-> e
-> Sign f e
C.Sign
    { sortRel :: Rel SORT
sortRel = Rel SORT
sorts
    , revSortRel :: Maybe (Rel SORT)
revSortRel = Rel SORT -> Maybe (Rel SORT)
forall a. a -> Maybe a
Just (Rel SORT -> Maybe (Rel SORT)) -> Rel SORT -> Maybe (Rel SORT)
forall a b. (a -> b) -> a -> b
$ [(SORT, SORT)] -> Rel SORT
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList (((SORT, SORT) -> (SORT, SORT)) -> [(SORT, SORT)] -> [(SORT, SORT)]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, SORT) -> (SORT, SORT)
revertOrder (Rel SORT -> [(SORT, SORT)]
forall a. Rel a -> [(a, a)]
Rel.toList Rel SORT
sorts))
    , emptySortSet :: Set SORT
emptySortSet = Set SORT
forall a. Set a
Set.empty
    , opMap :: OpMap
opMap = OpMap
ops
    , assocOps :: OpMap
assocOps = OpMap
forall a b. MapSet a b
MapSet.empty
    , predMap :: PredMap
predMap = (PredMap, [Named (FORMULA Any)]) -> PredMap
forall a b. (a, b) -> a
fst (PredMap, [Named (FORMULA Any)])
forall f. (PredMap, [Named (FORMULA f)])
predd
    , varMap :: Map SIMPLE_ID SORT
varMap = Map SIMPLE_ID SORT
forall k a. Map k a
Map.empty
    , sentences :: [Named CASLFORMULA]
sentences = (PredMap, [Named CASLFORMULA]) -> [Named CASLFORMULA]
forall a b. (a, b) -> b
snd (PredMap, [Named CASLFORMULA])
forall f. (PredMap, [Named (FORMULA f)])
predd [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
sent [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
sentDisEmb [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
noConfBetOps
    , declaredSymbols :: Set Symbol
declaredSymbols = Set Symbol
forall a. Set a
Set.empty
    , envDiags :: [Diagnosis]
envDiags = []
    , annoMap :: AnnoMap
annoMap = AnnoMap
forall a b. MapSet a b
MapSet.empty
    , globAnnos :: GlobalAnnos
globAnnos = GlobalAnnos
emptyGlobalAnnos
    , extendedInfo :: ()
extendedInfo = ()
    }

getSorts :: Set.Set TypeClass -> Rel.Rel TypeClass -> Rel.Rel SORT
getSorts :: Set TypeClass -> Rel TypeClass -> Rel SORT
getSorts setC :: Set TypeClass
setC relC :: Rel TypeClass
relC =
  let relS :: Rel SORT
relS = (TypeClass -> Rel SORT -> Rel SORT)
-> Rel SORT -> Set TypeClass -> Rel SORT
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (String -> Rel SORT -> Rel SORT
insertSort (String -> Rel SORT -> Rel SORT)
-> (TypeClass -> String) -> TypeClass -> Rel SORT -> Rel SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeClass -> String
name) Rel SORT
forall a. Rel a
Rel.empty Set TypeClass
setC
  in ((TypeClass, TypeClass) -> Rel SORT -> Rel SORT)
-> Rel SORT -> [(TypeClass, TypeClass)] -> Rel SORT
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TypeClass, TypeClass) -> Rel SORT -> Rel SORT
insertPair Rel SORT
relS (Rel TypeClass -> [(TypeClass, TypeClass)]
forall a. Rel a -> [(a, a)]
Rel.toList Rel TypeClass
relC)

insertSort :: String -> Rel.Rel SORT -> Rel.Rel SORT
insertSort :: String -> Rel SORT -> Rel SORT
insertSort s :: String
s = SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair (String -> SORT
stringToId String
s) (String -> SORT
stringToId String
s)

insertPair :: (TypeClass, TypeClass) -> Rel.Rel SORT -> Rel.Rel SORT
insertPair :: (TypeClass, TypeClass) -> Rel SORT -> Rel SORT
insertPair (t1 :: TypeClass
t1, t2 :: TypeClass
t2) = SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
t1) (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
t2)

revertOrder :: (SORT, SORT) -> (SORT, SORT)
revertOrder :: (SORT, SORT) -> (SORT, SORT)
revertOrder (a :: SORT
a, b :: SORT
b) = (SORT
b, SORT
a)

getPredicates :: Set.Set PropertyT -> (PredMap, [Named (FORMULA f)])
getPredicates :: Set PropertyT -> (PredMap, [Named (FORMULA f)])
getPredicates = (PropertyT
 -> (PredMap, [Named (FORMULA f)])
 -> (PredMap, [Named (FORMULA f)]))
-> (PredMap, [Named (FORMULA f)])
-> Set PropertyT
-> (PredMap, [Named (FORMULA f)])
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold PropertyT
-> (PredMap, [Named (FORMULA f)]) -> (PredMap, [Named (FORMULA f)])
forall f.
PropertyT
-> (PredMap, [Named (FORMULA f)]) -> (PredMap, [Named (FORMULA f)])
insertPredicate (PredMap
forall a b. MapSet a b
MapSet.empty, [])

insertPredicate :: PropertyT -> (PredMap, [Named (FORMULA f)]) -> (PredMap, [Named (FORMULA f)])
insertPredicate :: PropertyT
-> (PredMap, [Named (FORMULA f)]) -> (PredMap, [Named (FORMULA f)])
insertPredicate prop :: PropertyT
prop (predM :: PredMap
predM, form :: [Named (FORMULA f)]
form) =
  let
    sort1 :: SORT
sort1 = String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name (TypeClass -> String) -> TypeClass -> String
forall a b. (a -> b) -> a -> b
$ PropertyT -> TypeClass
sourceType PropertyT
prop
    sort2 :: SORT
sort2 = String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name (TypeClass -> String) -> TypeClass -> String
forall a b. (a -> b) -> a -> b
$ PropertyT -> TypeClass
targetType PropertyT
prop
    pname1 :: SORT
pname1 = String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ PropertyT -> String
targetRole PropertyT
prop
    ptype1 :: PredType
ptype1 = [SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ SORT
sort1 SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: [SORT
sort2]
    pname2 :: SORT
pname2 = String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ PropertyT -> String
sourceRole PropertyT
prop
    ptype2 :: PredType
ptype2 = [SORT] -> PredType
PredType ([SORT] -> PredType) -> [SORT] -> PredType
forall a b. (a -> b) -> a -> b
$ SORT
sort2 SORT -> [SORT] -> [SORT]
forall a. a -> [a] -> [a]
: [SORT
sort1]
    nam :: String
nam = "equiv_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ PropertyT -> String
targetRole PropertyT
prop String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ PropertyT -> String
sourceRole PropertyT
prop
    varsD :: [VAR_DECL]
varsD = [[SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [String -> SIMPLE_ID
mkSimpleId "x"] SORT
sort2 Range
nullRange,
             [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [String -> SIMPLE_ID
mkSimpleId "y"] SORT
sort1 Range
nullRange]
    sentRel :: FORMULA f
sentRel = FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
C.Relation
                (PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
C.Predication (SORT -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name SORT
pname2
                   ([SORT] -> Range -> PRED_TYPE
Pred_type [SORT
sort2, SORT
sort1] Range
nullRange) Range
nullRange)
                    (SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
C.Qual_var (String -> SIMPLE_ID
mkSimpleId "x") SORT
sort2 Range
nullRange TERM f -> [TERM f] -> [TERM f]
forall a. a -> [a] -> [a]
:
                       [SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
C.Qual_var (String -> SIMPLE_ID
mkSimpleId "y") SORT
sort1 Range
nullRange]) Range
nullRange)
                Relation
C.Equivalence
                 (PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
C.Predication (SORT -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name SORT
pname1
                   ([SORT] -> Range -> PRED_TYPE
Pred_type [SORT
sort1, SORT
sort2] Range
nullRange) Range
nullRange)
                   (SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
C.Qual_var (String -> SIMPLE_ID
mkSimpleId "y") SORT
sort1 Range
nullRange TERM f -> [TERM f] -> [TERM f]
forall a. a -> [a] -> [a]
:
                     [SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
C.Qual_var (String -> SIMPLE_ID
mkSimpleId "x") SORT
sort2 Range
nullRange]) Range
nullRange)
              Range
nullRange
    sent :: FORMULA f
sent = QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [VAR_DECL]
varsD FORMULA f
forall f. FORMULA f
sentRel Range
nullRange
  in
    {- MapSet does not allows repeated elements, but predicate names can be repeated
    (this must be corrected by creating a more complex ID) -}
    if PropertyT -> String
sourceRole PropertyT
prop String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "_"
    then (SORT -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
pname1 PredType
ptype1 PredMap
predM, [Named (FORMULA f)]
form)
    else if PropertyT -> String
targetRole PropertyT
prop String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "_"
         then (SORT -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
pname2 PredType
ptype2 PredMap
predM, [Named (FORMULA f)]
form)
         else (SORT -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
pname1 PredType
ptype1 (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ SORT -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
pname2 PredType
ptype2 PredMap
predM,
               String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed String
nam FORMULA f
forall f. FORMULA f
sent Named (FORMULA f) -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. a -> [a] -> [a]
: [Named (FORMULA f)]
form)


getOperations :: Map.Map String TypeClass -> OpMap
getOperations :: Map String TypeClass -> OpMap
getOperations ops :: Map String TypeClass
ops = ((String, TypeClass) -> OpMap -> OpMap)
-> OpMap -> [(String, TypeClass)] -> OpMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String, TypeClass) -> OpMap -> OpMap
insertOperations OpMap
forall a b. MapSet a b
MapSet.empty (Map String TypeClass -> [(String, TypeClass)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String TypeClass
ops)

insertOperations :: (String, TypeClass) -> OpMap -> OpMap
insertOperations :: (String, TypeClass) -> OpMap -> OpMap
insertOperations (na :: String
na, tc :: TypeClass
tc) opM :: OpMap
opM =
  let
    opName :: SORT
opName = String -> SORT
stringToId String
na
    opType :: OpType
opType = OpKind -> [SORT] -> SORT -> OpType
OpType OpKind
Total [] (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
tc)
  in
    SORT -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert SORT
opName OpType
opType OpMap
opM


getSentencesRels :: Set.Set LinkT -> Map.Map String TypeClass ->
                    [Named CASLFORMULA]
getSentencesRels :: Set LinkT -> Map String TypeClass -> [Named CASLFORMULA]
getSentencesRels = Set LinkT -> Map String TypeClass -> [Named CASLFORMULA]
completenessOfRelations


completenessOfRelations :: Set.Set LinkT -> Map.Map String TypeClass ->
                           [Named CASLFORMULA]
completenessOfRelations :: Set LinkT -> Map String TypeClass -> [Named CASLFORMULA]
completenessOfRelations linkk :: Set LinkT
linkk ops :: Map String TypeClass
ops =
  let ordLinks :: Map String [LinkT]
ordLinks = Set LinkT -> Map String [LinkT]
getLinksByProperty Set LinkT
linkk
  in ((String, [LinkT]) -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA]
-> [(String, [LinkT])]
-> [Named CASLFORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
(++) ([Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> ((String, [LinkT]) -> [Named CASLFORMULA])
-> (String, [LinkT])
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String TypeClass -> (String, [LinkT]) -> [Named CASLFORMULA]
createComplFormula Map String TypeClass
ops) [] (Map String [LinkT] -> [(String, [LinkT])]
forall k a. Map k a -> [(k, a)]
Map.toList Map String [LinkT]
ordLinks)

createComplFormula :: Map.Map String TypeClass -> (String, [LinkT]) ->
                      [Named CASLFORMULA]
createComplFormula :: Map String TypeClass -> (String, [LinkT]) -> [Named CASLFORMULA]
createComplFormula ops :: Map String TypeClass
ops (nam :: String
nam, linksL :: [LinkT]
linksL) =
  let
    varA :: SIMPLE_ID
varA = String -> SIMPLE_ID
mkSimpleId "x"
    varB :: SIMPLE_ID
varB = String -> SIMPLE_ID
mkSimpleId "y"
  in
    case [LinkT]
linksL of
      [] -> []
      LinkT _ _ pr :: PropertyT
pr : _ ->
       let sorA :: SORT
sorA = String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name (TypeClass -> String) -> TypeClass -> String
forall a b. (a -> b) -> a -> b
$ PropertyT -> TypeClass
sourceType PropertyT
pr
           sorB :: SORT
sorB = String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name (TypeClass -> String) -> TypeClass -> String
forall a b. (a -> b) -> a -> b
$ PropertyT -> TypeClass
targetType PropertyT
pr
           varsD :: [VAR_DECL]
varsD = [[SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
varA] SORT
sorA Range
nullRange,
                    [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
varB] SORT
sorB Range
nullRange]
           sent :: CASLFORMULA
sent = CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
C.Relation (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
C.Predication (SORT -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name
            (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ PropertyT -> String
targetRole PropertyT
pr) ([SORT] -> Range -> PRED_TYPE
Pred_type [SORT
sorA, SORT
sorB] Range
nullRange)
            Range
nullRange) (SIMPLE_ID -> SORT -> Range -> TERM ()
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
C.Qual_var SIMPLE_ID
varA SORT
sorA Range
nullRange TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
:
             [SIMPLE_ID -> SORT -> Range -> TERM ()
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
C.Qual_var SIMPLE_ID
varB SORT
sorB Range
nullRange]) Range
nullRange)
            Relation
C.Equivalence (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis
              ((LinkT -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> [LinkT] -> [CASLFORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA])
-> (LinkT -> CASLFORMULA)
-> LinkT
-> [CASLFORMULA]
-> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String TypeClass
-> SIMPLE_ID -> SORT -> SIMPLE_ID -> SORT -> LinkT -> CASLFORMULA
getPropHold Map String TypeClass
ops SIMPLE_ID
varA SORT
sorA SIMPLE_ID
varB SORT
sorB) [] [LinkT]
linksL)
               Range
nullRange) Range
nullRange
           sentQuan :: CASLFORMULA
sentQuan = QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [VAR_DECL]
varsD CASLFORMULA
sent Range
nullRange
       in [String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("compRel_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nam) CASLFORMULA
sentQuan]

getPropHold :: Map.Map String TypeClass -> VAR -> SORT -> VAR -> SORT -> LinkT
               -> CASLFORMULA
getPropHold :: Map String TypeClass
-> SIMPLE_ID -> SORT -> SIMPLE_ID -> SORT -> LinkT -> CASLFORMULA
getPropHold ops :: Map String TypeClass
ops varA :: SIMPLE_ID
varA sorA :: SORT
sorA varB :: SIMPLE_ID
varB sorB :: SORT
sorB lin :: LinkT
lin =
  let
    souObj :: Maybe TypeClass
souObj = String -> Map String TypeClass -> Maybe TypeClass
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LinkT -> String
sourceVar LinkT
lin) Map String TypeClass
ops
    tarObj :: Maybe TypeClass
tarObj = String -> Map String TypeClass -> Maybe TypeClass
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LinkT -> String
targetVar LinkT
lin) Map String TypeClass
ops
    typSou :: String
typSou = case Maybe TypeClass
souObj of
               Nothing -> LinkT -> String
sourceVar LinkT
lin -- if happens then is an error
               Just tSou :: TypeClass
tSou -> TypeClass -> String
name TypeClass
tSou
    typTar :: String
typTar = case Maybe TypeClass
tarObj of
               Nothing -> LinkT -> String
targetVar LinkT
lin -- if happens then is an error
               Just tTar :: TypeClass
tTar -> TypeClass -> String
name TypeClass
tTar
    eqA :: FORMULA f
eqA = TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation (SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
varA SORT
sorA Range
nullRange)
                   Equality
Strong
                     (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (String -> SORT
stringToId (LinkT -> String
sourceVar LinkT
lin))
                        (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] (String -> SORT
stringToId String
typSou) Range
nullRange)
                        Range
nullRange) [] Range
nullRange)
                   Range
nullRange
    eqB :: FORMULA f
eqB = TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation (SIMPLE_ID -> SORT -> Range -> TERM f
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
varB SORT
sorB Range
nullRange)
                   Equality
Strong
                   (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (String -> SORT
stringToId (LinkT -> String
targetVar LinkT
lin))
                        (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] (String -> SORT
stringToId String
typTar) Range
nullRange)
                        Range
nullRange) [] Range
nullRange)
                   Range
nullRange
  in
    Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con (CASLFORMULA
forall f. FORMULA f
eqA CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [CASLFORMULA
forall f. FORMULA f
eqB]) Range
nullRange


getLinksByProperty :: Set.Set LinkT -> Map.Map String [LinkT]
getLinksByProperty :: Set LinkT -> Map String [LinkT]
getLinksByProperty linkk :: Set LinkT
linkk =
  let elems :: [LinkT]
elems = Set LinkT -> [LinkT]
forall a. Set a -> [a]
Set.elems Set LinkT
linkk
  in (LinkT -> Map String [LinkT] -> Map String [LinkT])
-> Map String [LinkT] -> [LinkT] -> Map String [LinkT]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr LinkT -> Map String [LinkT] -> Map String [LinkT]
getByProperty Map String [LinkT]
forall k a. Map k a
Map.empty [LinkT]
elems

getByProperty :: LinkT -> Map.Map String [LinkT] -> Map.Map String [LinkT]
getByProperty :: LinkT -> Map String [LinkT] -> Map String [LinkT]
getByProperty lin :: LinkT
lin mapL :: Map String [LinkT]
mapL =
  let
    prope :: PropertyT
prope = LinkT -> PropertyT
CSMOF.property LinkT
lin
    nameLook :: String
nameLook = PropertyT -> String
sourceRole PropertyT
prope String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeClass -> String
name (PropertyT -> TypeClass
sourceType PropertyT
prope) String -> ShowS
forall a. [a] -> [a] -> [a]
++ PropertyT -> String
targetRole PropertyT
prope
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeClass -> String
name (PropertyT -> TypeClass
targetType PropertyT
prope)
    setProp :: Maybe [LinkT]
setProp = String -> Map String [LinkT] -> Maybe [LinkT]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
nameLook Map String [LinkT]
mapL
  in
    case Maybe [LinkT]
setProp of
      Nothing -> String -> [LinkT] -> Map String [LinkT] -> Map String [LinkT]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
nameLook [LinkT
lin] (String -> Map String [LinkT] -> Map String [LinkT]
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete String
nameLook Map String [LinkT]
mapL)
      Just s :: [LinkT]
s -> String -> [LinkT] -> Map String [LinkT] -> Map String [LinkT]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
nameLook (LinkT
lin LinkT -> [LinkT] -> [LinkT]
forall a. a -> [a] -> [a]
: [LinkT]
s) (String -> Map String [LinkT] -> Map String [LinkT]
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete String
nameLook Map String [LinkT]
mapL)


getSortGen :: Rel.Rel TypeClass -> Set.Set TypeClass -> Set.Set TypeClass ->
              Map.Map String TypeClass -> [Named CASLFORMULA]
getSortGen :: Rel TypeClass
-> Set TypeClass
-> Set TypeClass
-> Map String TypeClass
-> [Named CASLFORMULA]
getSortGen typpR :: Rel TypeClass
typpR absCl :: Set TypeClass
absCl typCl :: Set TypeClass
typCl inst :: Map String TypeClass
inst = Set TypeClass -> Rel TypeClass -> [Named CASLFORMULA]
disjointEmbedding Set TypeClass
absCl Rel TypeClass
typpR [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++
 Map String TypeClass -> [Named CASLFORMULA]
sortGeneration Map String TypeClass
inst [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++
 Rel TypeClass
-> Set TypeClass
-> Set TypeClass
-> Map String TypeClass
-> [Named CASLFORMULA]
sortGenerationNonAbstractSuperClasses Rel TypeClass
typpR Set TypeClass
typCl Set TypeClass
absCl Map String TypeClass
inst


-- Free type of non-abstract superclasses
sortGenerationNonAbstractSuperClasses :: Rel.Rel TypeClass -> Set.Set TypeClass
 -> Set.Set TypeClass -> Map.Map String TypeClass -> [Named CASLFORMULA]
sortGenerationNonAbstractSuperClasses :: Rel TypeClass
-> Set TypeClass
-> Set TypeClass
-> Map String TypeClass
-> [Named CASLFORMULA]
sortGenerationNonAbstractSuperClasses typpR :: Rel TypeClass
typpR typCl :: Set TypeClass
typCl absCl :: Set TypeClass
absCl inst :: Map String TypeClass
inst =
  let
    ordObj :: Map TypeClass [String]
ordObj = ((String, TypeClass)
 -> Map TypeClass [String] -> Map TypeClass [String])
-> Map TypeClass [String]
-> [(String, TypeClass)]
-> Map TypeClass [String]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String, TypeClass)
-> Map TypeClass [String] -> Map TypeClass [String]
orderByClass Map TypeClass [String]
forall k a. Map k a
Map.empty (Map String TypeClass -> [(String, TypeClass)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String TypeClass
inst)
    nonAbsClasses :: Set TypeClass
nonAbsClasses = Set TypeClass -> Set TypeClass -> Set TypeClass
getNonAbstractClasess Set TypeClass
absCl Set TypeClass
typCl
    nonAbsClassesWChilds :: [(TypeClass, [TypeClass])]
nonAbsClassesWChilds = ((TypeClass, [TypeClass]) -> Bool)
-> [(TypeClass, [TypeClass])] -> [(TypeClass, [TypeClass])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((TypeClass, [TypeClass]) -> Bool)
-> (TypeClass, [TypeClass])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TypeClass] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([TypeClass] -> Bool)
-> ((TypeClass, [TypeClass]) -> [TypeClass])
-> (TypeClass, [TypeClass])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeClass, [TypeClass]) -> [TypeClass]
forall a b. (a, b) -> b
snd)
     ((TypeClass
 -> [(TypeClass, [TypeClass])] -> [(TypeClass, [TypeClass])])
-> [(TypeClass, [TypeClass])]
-> Set TypeClass
-> [(TypeClass, [TypeClass])]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ((:) ((TypeClass, [TypeClass])
 -> [(TypeClass, [TypeClass])] -> [(TypeClass, [TypeClass])])
-> (TypeClass -> (TypeClass, [TypeClass]))
-> TypeClass
-> [(TypeClass, [TypeClass])]
-> [(TypeClass, [TypeClass])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel TypeClass -> TypeClass -> (TypeClass, [TypeClass])
getSubClasses Rel TypeClass
typpR) [] Set TypeClass
nonAbsClasses)
    childObjects :: [(TypeClass, [String])]
childObjects = ((TypeClass, [TypeClass])
 -> [(TypeClass, [String])] -> [(TypeClass, [String])])
-> [(TypeClass, [String])]
-> [(TypeClass, [TypeClass])]
-> [(TypeClass, [String])]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) ((TypeClass, [String])
 -> [(TypeClass, [String])] -> [(TypeClass, [String])])
-> ((TypeClass, [TypeClass]) -> (TypeClass, [String]))
-> (TypeClass, [TypeClass])
-> [(TypeClass, [String])]
-> [(TypeClass, [String])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map TypeClass [String]
-> (TypeClass, [TypeClass]) -> (TypeClass, [String])
getClassSubObjects Map TypeClass [String]
ordObj)
     [] [(TypeClass, [TypeClass])]
nonAbsClassesWChilds -- [(TypeClass,[String])]
  in
    ((TypeClass, [String])
 -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA]
-> [(TypeClass, [String])]
-> [Named CASLFORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> ((TypeClass, [String]) -> Named CASLFORMULA)
-> (TypeClass, [String])
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map String TypeClass -> (TypeClass, [String]) -> Named CASLFORMULA
toSortConstraintNonAbsClass Map String TypeClass
inst) [] [(TypeClass, [String])]
childObjects


-- Takes the objects, and a class with its child classes and returns the descendent objects of such class
getClassSubObjects :: Map.Map TypeClass [String] -> (TypeClass, [TypeClass]) ->
                      (TypeClass, [String])
getClassSubObjects :: Map TypeClass [String]
-> (TypeClass, [TypeClass]) -> (TypeClass, [String])
getClassSubObjects objs :: Map TypeClass [String]
objs (tc :: TypeClass
tc, subCl :: [TypeClass]
subCl) =
  let objTC :: [String]
objTC = Map TypeClass [String] -> TypeClass -> [String]
findObjectInMap Map TypeClass [String]
objs TypeClass
tc
  in
    (TypeClass
tc, [String]
objTC [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (TypeClass -> [String] -> [String])
-> [String] -> [TypeClass] -> [String]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
(++) ([String] -> [String] -> [String])
-> (TypeClass -> [String]) -> TypeClass -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map TypeClass [String] -> TypeClass -> [String]
findObjectInMap Map TypeClass [String]
objs) [] [TypeClass]
subCl)

findObjectInMap :: Map.Map TypeClass [String] -> TypeClass -> [String]
findObjectInMap :: Map TypeClass [String] -> TypeClass -> [String]
findObjectInMap objs :: Map TypeClass [String]
objs tc :: TypeClass
tc = [String] -> Maybe [String] -> [String]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [String] -> [String]) -> Maybe [String] -> [String]
forall a b. (a -> b) -> a -> b
$ TypeClass -> Map TypeClass [String] -> Maybe [String]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TypeClass
tc Map TypeClass [String]
objs

getNonAbstractClasess :: Set.Set TypeClass -> Set.Set TypeClass -> Set.Set TypeClass
getNonAbstractClasess :: Set TypeClass -> Set TypeClass -> Set TypeClass
getNonAbstractClasess absCl :: Set TypeClass
absCl classes :: Set TypeClass
classes = Set TypeClass -> Set TypeClass -> Set TypeClass
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set TypeClass
classes Set TypeClass
absCl

getSubClasses :: Rel.Rel TypeClass -> TypeClass -> (TypeClass, [TypeClass])
getSubClasses :: Rel TypeClass -> TypeClass -> (TypeClass, [TypeClass])
getSubClasses typpR :: Rel TypeClass
typpR tc :: TypeClass
tc =
  let subCla :: [TypeClass]
subCla = ((TypeClass, TypeClass) -> TypeClass)
-> [(TypeClass, TypeClass)] -> [TypeClass]
forall a b. (a -> b) -> [a] -> [b]
map (TypeClass, TypeClass) -> TypeClass
forall a b. (a, b) -> a
fst (((TypeClass, TypeClass) -> Bool)
-> [(TypeClass, TypeClass)] -> [(TypeClass, TypeClass)]
forall a. (a -> Bool) -> [a] -> [a]
filter (TypeClass -> (TypeClass, TypeClass) -> Bool
isParent TypeClass
tc) (Rel TypeClass -> [(TypeClass, TypeClass)]
forall a. Rel a -> [(a, a)]
Rel.toList Rel TypeClass
typpR))
      rec :: [TypeClass]
rec = (TypeClass -> [TypeClass] -> [TypeClass])
-> [TypeClass] -> [TypeClass] -> [TypeClass]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([TypeClass] -> [TypeClass] -> [TypeClass]
forall a. [a] -> [a] -> [a]
(++) ([TypeClass] -> [TypeClass] -> [TypeClass])
-> (TypeClass -> [TypeClass])
-> TypeClass
-> [TypeClass]
-> [TypeClass]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeClass, [TypeClass]) -> [TypeClass]
forall a b. (a, b) -> b
snd ((TypeClass, [TypeClass]) -> [TypeClass])
-> (TypeClass -> (TypeClass, [TypeClass]))
-> TypeClass
-> [TypeClass]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel TypeClass -> TypeClass -> (TypeClass, [TypeClass])
getSubClasses Rel TypeClass
typpR) [] [TypeClass]
subCla
  in (TypeClass
tc, [TypeClass]
subCla [TypeClass] -> [TypeClass] -> [TypeClass]
forall a. [a] -> [a] -> [a]
++ [TypeClass]
rec)

isParent :: TypeClass -> (TypeClass, TypeClass) -> Bool
isParent :: TypeClass -> (TypeClass, TypeClass) -> Bool
isParent tc :: TypeClass
tc (_, tc2 :: TypeClass
tc2) = TypeClass
tc TypeClass -> TypeClass -> Bool
forall a. Eq a => a -> a -> Bool
== TypeClass
tc2

toSortConstraintNonAbsClass :: Map.Map String TypeClass -> (TypeClass, [String])
                               -> Named CASLFORMULA
toSortConstraintNonAbsClass :: Map String TypeClass -> (TypeClass, [String]) -> Named CASLFORMULA
toSortConstraintNonAbsClass inst :: Map String TypeClass
inst (tc :: TypeClass
tc, lisObj :: [String]
lisObj) =
  let
    sor :: SORT
sor = String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
tc
    varA :: VAR_DECL
varA = [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [String -> SIMPLE_ID
mkSimpleId "x"] SORT
sor Range
nullRange
    sent :: CASLFORMULA
sent = Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis ((String -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> [String] -> [CASLFORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA])
-> (String -> CASLFORMULA)
-> String
-> [CASLFORMULA]
-> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Map String TypeClass -> String -> CASLFORMULA
getEqualityVarObject SORT
sor Map String TypeClass
inst)
      [] [String]
lisObj) Range
nullRange
    constr :: CASLFORMULA
constr = QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [VAR_DECL
varA] CASLFORMULA
sent Range
nullRange
  in
    String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("sortGenCon_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeClass -> String
name TypeClass
tc) CASLFORMULA
constr

getEqualityVarObject :: SORT -> Map.Map String TypeClass -> String -> CASLFORMULA
getEqualityVarObject :: SORT -> Map String TypeClass -> String -> CASLFORMULA
getEqualityVarObject sor :: SORT
sor inst :: Map String TypeClass
inst obj :: String
obj =
  let oTyp :: SORT
oTyp = case String -> Map String TypeClass -> Maybe TypeClass
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
obj Map String TypeClass
inst of
                Nothing -> String -> SORT
stringToId String
obj -- If happens, there is an error
                Just ob :: TypeClass
ob -> String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
ob
  in
    TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation (SIMPLE_ID -> SORT -> Range -> TERM ()
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var (String -> SIMPLE_ID
mkSimpleId "x") SORT
sor Range
nullRange)
      Equality
Strong
      (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (String -> SORT
stringToId String
obj)
        (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] SORT
oTyp Range
nullRange)
        Range
nullRange) [] Range
nullRange)
      Range
nullRange


-- Sorts are generated as a free type of object functions
sortGeneration :: Map.Map String TypeClass -> [Named CASLFORMULA]
sortGeneration :: Map String TypeClass -> [Named CASLFORMULA]
sortGeneration inst :: Map String TypeClass
inst =
  let
    ordObj :: Map TypeClass [String]
ordObj = ((String, TypeClass)
 -> Map TypeClass [String] -> Map TypeClass [String])
-> Map TypeClass [String]
-> [(String, TypeClass)]
-> Map TypeClass [String]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String, TypeClass)
-> Map TypeClass [String] -> Map TypeClass [String]
orderByClass Map TypeClass [String]
forall k a. Map k a
Map.empty (Map String TypeClass -> [(String, TypeClass)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String TypeClass
inst)
    noJunk :: [Named CASLFORMULA]
noJunk = ((TypeClass, [String])
 -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA]
-> [(TypeClass, [String])]
-> [Named CASLFORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> ((TypeClass, [String]) -> Named CASLFORMULA)
-> (TypeClass, [String])
-> [Named CASLFORMULA]
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeClass, [String]) -> Named CASLFORMULA
toSortConstraint) [] (Map TypeClass [String] -> [(TypeClass, [String])]
forall k a. Map k a -> [(k, a)]
Map.toList Map TypeClass [String]
ordObj)
  in
    [Named CASLFORMULA]
noJunk

mapFilterJust :: [Maybe a] -> [a]
mapFilterJust :: [Maybe a] -> [a]
mapFilterJust list :: [Maybe a]
list =
  case [Maybe a]
list of
    [] -> []
    a :: Maybe a
a : rest :: [Maybe a]
rest -> case Maybe a
a of
                  Nothing -> [Maybe a] -> [a]
forall a. [Maybe a] -> [a]
mapFilterJust [Maybe a]
rest
                  Just el :: a
el -> a
el a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [Maybe a] -> [a]
forall a. [Maybe a] -> [a]
mapFilterJust [Maybe a]
rest

orderByClass :: (String, TypeClass) -> Map.Map TypeClass [String] ->
                Map.Map TypeClass [String]
orderByClass :: (String, TypeClass)
-> Map TypeClass [String] -> Map TypeClass [String]
orderByClass (ob :: String
ob, tc :: TypeClass
tc) mapTC :: Map TypeClass [String]
mapTC =
  case TypeClass -> Map TypeClass [String] -> Maybe [String]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TypeClass
tc Map TypeClass [String]
mapTC of
    Nothing -> TypeClass
-> [String] -> Map TypeClass [String] -> Map TypeClass [String]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TypeClass
tc [String
ob] Map TypeClass [String]
mapTC
    Just listObj :: [String]
listObj -> TypeClass
-> [String] -> Map TypeClass [String] -> Map TypeClass [String]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TypeClass
tc (String
ob String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
listObj) (TypeClass -> Map TypeClass [String] -> Map TypeClass [String]
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete TypeClass
tc Map TypeClass [String]
mapTC)


getNoConfusionBetweenSets :: Map.Map String TypeClass -> Rel.Rel TypeClass ->
                             [Named CASLFORMULA]
getNoConfusionBetweenSets :: Map String TypeClass -> Rel TypeClass -> [Named CASLFORMULA]
getNoConfusionBetweenSets inst :: Map String TypeClass
inst relC :: Rel TypeClass
relC =
  let ordObj :: [(TypeClass, [String])]
ordObj = Map TypeClass [String] -> [(TypeClass, [String])]
forall k a. Map k a -> [(k, a)]
Map.toList (Map TypeClass [String] -> [(TypeClass, [String])])
-> Map TypeClass [String] -> [(TypeClass, [String])]
forall a b. (a -> b) -> a -> b
$ ((String, TypeClass)
 -> Map TypeClass [String] -> Map TypeClass [String])
-> Map TypeClass [String]
-> [(String, TypeClass)]
-> Map TypeClass [String]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String, TypeClass)
-> Map TypeClass [String] -> Map TypeClass [String]
orderByClass Map TypeClass [String]
forall k a. Map k a
Map.empty (Map String TypeClass -> [(String, TypeClass)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String TypeClass
inst)
  in [Maybe (Named CASLFORMULA)] -> [Named CASLFORMULA]
forall a. [Maybe a] -> [a]
mapFilterJust ([Maybe (Named CASLFORMULA)] -> [Named CASLFORMULA])
-> [Maybe (Named CASLFORMULA)] -> [Named CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ ((TypeClass, [String])
 -> [Maybe (Named CASLFORMULA)] -> [Maybe (Named CASLFORMULA)])
-> [Maybe (Named CASLFORMULA)]
-> [(TypeClass, [String])]
-> [Maybe (Named CASLFORMULA)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (Maybe (Named CASLFORMULA)
 -> [Maybe (Named CASLFORMULA)] -> [Maybe (Named CASLFORMULA)])
-> ((TypeClass, [String]) -> Maybe (Named CASLFORMULA))
-> (TypeClass, [String])
-> [Maybe (Named CASLFORMULA)]
-> [Maybe (Named CASLFORMULA)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(TypeClass, [String])]
-> Rel TypeClass
-> (TypeClass, [String])
-> Maybe (Named CASLFORMULA)
getNoConfusionBSetsAxiom [(TypeClass, [String])]
ordObj Rel TypeClass
relC) [] [(TypeClass, [String])]
ordObj

getNoConfusionBSetsAxiom :: [(TypeClass, [String])] -> Rel.Rel TypeClass ->
                            (TypeClass, [String]) -> Maybe (Named CASLFORMULA)
getNoConfusionBSetsAxiom :: [(TypeClass, [String])]
-> Rel TypeClass
-> (TypeClass, [String])
-> Maybe (Named CASLFORMULA)
getNoConfusionBSetsAxiom ordObj :: [(TypeClass, [String])]
ordObj relC :: Rel TypeClass
relC (tc :: TypeClass
tc, lisObj :: [String]
lisObj) =
  case [String]
lisObj of
    [] -> Maybe (Named CASLFORMULA)
forall a. Maybe a
Nothing
    _ : _ ->
     let filteredObj :: [(TypeClass, [String])]
filteredObj = TypeClass -> [(TypeClass, [String])] -> [(TypeClass, [String])]
removeUntilType TypeClass
tc [(TypeClass, [String])]
ordObj
         diffForm :: [CASLFORMULA]
diffForm = ((TypeClass, [String]) -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> [(TypeClass, [String])] -> [CASLFORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
(++) ([CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA])
-> ((TypeClass, [String]) -> [CASLFORMULA])
-> (TypeClass, [String])
-> [CASLFORMULA]
-> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeClass, [String])
-> Rel TypeClass -> (TypeClass, [String]) -> [CASLFORMULA]
diffOfRestConstants (TypeClass
tc, [String]
lisObj) Rel TypeClass
relC)
                     [] [(TypeClass, [String])]
filteredObj in
                   case [CASLFORMULA]
diffForm of
                     [] -> Maybe (Named CASLFORMULA)
forall a. Maybe a
Nothing
                     _ : _ -> let constr :: CASLFORMULA
constr = Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [CASLFORMULA]
diffForm Range
nullRange
                              in Named CASLFORMULA -> Maybe (Named CASLFORMULA)
forall a. a -> Maybe a
Just (Named CASLFORMULA -> Maybe (Named CASLFORMULA))
-> Named CASLFORMULA -> Maybe (Named CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("noConfusion_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeClass -> String
name TypeClass
tc) CASLFORMULA
constr

removeUntilType :: TypeClass -> [(TypeClass, [String])] -> [(TypeClass, [String])]
removeUntilType :: TypeClass -> [(TypeClass, [String])] -> [(TypeClass, [String])]
removeUntilType tc :: TypeClass
tc lis :: [(TypeClass, [String])]
lis =
  case [(TypeClass, [String])]
lis of
    [] -> []
    (tc2 :: TypeClass
tc2, lisObj2 :: [String]
lisObj2) : rest :: [(TypeClass, [String])]
rest -> if TypeClass
tc TypeClass -> TypeClass -> Bool
forall a. Eq a => a -> a -> Bool
== TypeClass
tc2
                            then (TypeClass
tc2, [String]
lisObj2) (TypeClass, [String])
-> [(TypeClass, [String])] -> [(TypeClass, [String])]
forall a. a -> [a] -> [a]
: [(TypeClass, [String])]
rest
                            else TypeClass -> [(TypeClass, [String])] -> [(TypeClass, [String])]
removeUntilType TypeClass
tc [(TypeClass, [String])]
rest

diffOfRestConstants :: (TypeClass, [String]) -> Rel.Rel TypeClass ->
                       (TypeClass, [String]) -> [CASLFORMULA]
diffOfRestConstants :: (TypeClass, [String])
-> Rel TypeClass -> (TypeClass, [String]) -> [CASLFORMULA]
diffOfRestConstants (tc1 :: TypeClass
tc1, lisObj1 :: [String]
lisObj1) relC :: Rel TypeClass
relC (tc2 :: TypeClass
tc2, lisObj2 :: [String]
lisObj2)
  | TypeClass
tc1 TypeClass -> TypeClass -> Bool
forall a. Eq a => a -> a -> Bool
== TypeClass
tc2 = (String -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> [String] -> [CASLFORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
(++) ([CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA])
-> (String -> [CASLFORMULA])
-> String
-> [CASLFORMULA]
-> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeClass -> [String] -> String -> [CASLFORMULA]
diffOfRestOps TypeClass
tc1 [String]
lisObj1) [] [String]
lisObj1
  | TypeClass -> TypeClass -> Rel TypeClass -> Bool
haveCommonSort TypeClass
tc1 TypeClass
tc2 Rel TypeClass
relC =
     (String -> [CASLFORMULA]) -> [String] -> [CASLFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((TypeClass, [String]) -> TypeClass -> String -> [CASLFORMULA]
diffOfRestOpsDiffSort (TypeClass
tc1, [String]
lisObj1) TypeClass
tc2) [String]
lisObj2
  | Bool
otherwise = []

haveCommonSort :: TypeClass -> TypeClass -> Rel.Rel TypeClass -> Bool
haveCommonSort :: TypeClass -> TypeClass -> Rel TypeClass -> Bool
haveCommonSort t1 :: TypeClass
t1 t2 :: TypeClass
t2 relT :: Rel TypeClass
relT =
  let succT1 :: Set TypeClass
succT1 = Rel TypeClass -> TypeClass -> Set TypeClass
superSorts Rel TypeClass
relT TypeClass
t1
      succT2 :: Set TypeClass
succT2 = Rel TypeClass -> TypeClass -> Set TypeClass
superSorts Rel TypeClass
relT TypeClass
t2
  in Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set TypeClass -> Bool
forall a. Set a -> Bool
Set.null (Set TypeClass -> Bool) -> Set TypeClass -> Bool
forall a b. (a -> b) -> a -> b
$ Set TypeClass -> Set TypeClass -> Set TypeClass
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set TypeClass
succT1 Set TypeClass
succT2

-- This is the non exported function reachable in Rel
superSorts :: Rel.Rel TypeClass -> TypeClass -> Set.Set TypeClass
superSorts :: Rel TypeClass -> TypeClass -> Set TypeClass
superSorts relT :: Rel TypeClass
relT tc :: TypeClass
tc = (TypeClass -> Set TypeClass -> Set TypeClass)
-> Set TypeClass -> Set TypeClass -> Set TypeClass
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold TypeClass -> Set TypeClass -> Set TypeClass
reach Set TypeClass
forall a. Set a
Set.empty (Set TypeClass -> Set TypeClass) -> Set TypeClass -> Set TypeClass
forall a b. (a -> b) -> a -> b
$ Rel TypeClass -> TypeClass -> Set TypeClass
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel TypeClass
relT TypeClass
tc where
         reach :: TypeClass -> Set TypeClass -> Set TypeClass
reach e :: TypeClass
e s :: Set TypeClass
s = if TypeClass -> Set TypeClass -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TypeClass
e Set TypeClass
s then Set TypeClass
s
                     else (TypeClass -> Set TypeClass -> Set TypeClass)
-> Set TypeClass -> Set TypeClass -> Set TypeClass
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold TypeClass -> Set TypeClass -> Set TypeClass
reach (TypeClass -> Set TypeClass -> Set TypeClass
forall a. Ord a => a -> Set a -> Set a
Set.insert TypeClass
e Set TypeClass
s) (Set TypeClass -> Set TypeClass) -> Set TypeClass -> Set TypeClass
forall a b. (a -> b) -> a -> b
$ Rel TypeClass -> TypeClass -> Set TypeClass
forall a. Ord a => Rel a -> a -> Set a
Rel.succs Rel TypeClass
relT TypeClass
e


diffOfRestOpsDiffSort :: (TypeClass, [String]) -> TypeClass -> String -> [CASLFORMULA]
diffOfRestOpsDiffSort :: (TypeClass, [String]) -> TypeClass -> String -> [CASLFORMULA]
diffOfRestOpsDiffSort (tc1 :: TypeClass
tc1, lisObj1 :: [String]
lisObj1) tc2 :: TypeClass
tc2 objName :: String
objName = (String -> [CASLFORMULA]) -> [String] -> [CASLFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
 (TypeClass -> String -> TypeClass -> String -> [CASLFORMULA]
diffOpsDiffSorts TypeClass
tc2 String
objName TypeClass
tc1) [String]
lisObj1

diffOpsDiffSorts :: TypeClass -> String -> TypeClass -> String -> [CASLFORMULA]
diffOpsDiffSorts :: TypeClass -> String -> TypeClass -> String -> [CASLFORMULA]
diffOpsDiffSorts tc2 :: TypeClass
tc2 objName2 :: String
objName2 tc1 :: TypeClass
tc1 objName1 :: String
objName1 =
  [CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (String -> SORT
stringToId String
objName1)
    (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
tc1) Range
nullRange) Range
nullRange) [] Range
nullRange)
    Equality
Strong (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (String -> SORT
stringToId String
objName2)
            (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
tc2) Range
nullRange)
      Range
nullRange) [] Range
nullRange) Range
nullRange) Range
nullRange]


diffOfRestOps :: TypeClass -> [String] -> String -> [CASLFORMULA]
diffOfRestOps :: TypeClass -> [String] -> String -> [CASLFORMULA]
diffOfRestOps tc :: TypeClass
tc lisObj :: [String]
lisObj objName :: String
objName =
  let lis :: [String]
lis = [String] -> String -> [String]
removeUntil [String]
lisObj String
objName
  in (String -> [CASLFORMULA]) -> [String] -> [CASLFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TypeClass -> String -> String -> [CASLFORMULA]
diffOps TypeClass
tc String
objName) [String]
lis

removeUntil :: [String] -> String -> [String]
removeUntil :: [String] -> String -> [String]
removeUntil lis :: [String]
lis str :: String
str =
  case [String]
lis of
    [] -> []
    a :: String
a : rest :: [String]
rest -> if String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
str
                then [String]
rest
                else [String] -> String -> [String]
removeUntil [String]
rest String
str

diffOps :: TypeClass -> String -> String -> [CASLFORMULA]
diffOps :: TypeClass -> String -> String -> [CASLFORMULA]
diffOps tc :: TypeClass
tc objName1 :: String
objName1 objName2 :: String
objName2 =
      [CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
                 (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (String -> SORT
stringToId String
objName1)
                        (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
tc) Range
nullRange)
                        Range
nullRange) [] Range
nullRange)
                 Equality
Strong
                 (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (String -> SORT
stringToId String
objName2)
                        (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
tc) Range
nullRange)
                        Range
nullRange) [] Range
nullRange)
                 Range
nullRange)
       Range
nullRange | String
objName1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
objName2]

toSortConstraint :: (TypeClass, [String]) -> Named CASLFORMULA
toSortConstraint :: (TypeClass, [String]) -> Named CASLFORMULA
toSortConstraint (tc :: TypeClass
tc, lisObj :: [String]
lisObj) =
  let
    sor :: SORT
sor = String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
tc
    simplCon :: Constraint
simplCon = SORT -> [(OP_SYMB, [Int])] -> SORT -> Constraint
Constraint SORT
sor ((String -> [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])])
-> [(OP_SYMB, [Int])] -> [String] -> [(OP_SYMB, [Int])]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) ((OP_SYMB, [Int]) -> [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])])
-> (String -> (OP_SYMB, [Int]))
-> String
-> [(OP_SYMB, [Int])]
-> [(OP_SYMB, [Int])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> String -> (OP_SYMB, [Int])
toConstraint SORT
sor) [] [String]
lisObj) SORT
sor
    constr :: FORMULA f
constr = [Constraint] -> Bool -> FORMULA f
forall f. [Constraint] -> Bool -> FORMULA f
mkSort_gen_ax [Constraint
simplCon] Bool
True
  in
    String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("sortGenCon_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeClass -> String
name TypeClass
tc) CASLFORMULA
forall f. FORMULA f
constr


toConstraint :: Id -> String -> (OP_SYMB, [Int])
toConstraint :: SORT -> String -> (OP_SYMB, [Int])
toConstraint sor :: SORT
sor obName :: String
obName =
  let obj :: SORT
obj = String -> SORT
stringToId String
obName
  in
    (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name SORT
obj (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [] SORT
sor Range
nullRange) Range
nullRange, [])


-- Each abstract class is the disjoint embedding of it subsorts
disjointEmbedding :: Set.Set TypeClass -> Rel.Rel TypeClass ->
                     [Named CASLFORMULA]
disjointEmbedding :: Set TypeClass -> Rel TypeClass -> [Named CASLFORMULA]
disjointEmbedding absCl :: Set TypeClass
absCl rel :: Rel TypeClass
rel =
  let
      injSyms :: [(OP_SYMB, [a])]
injSyms = ((TypeClass, TypeClass) -> (OP_SYMB, [a]))
-> [(TypeClass, TypeClass)] -> [(OP_SYMB, [a])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: TypeClass
s, t :: TypeClass
t) -> (SORT -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name
        (SORT -> SORT -> SORT
mkUniqueInjName (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
s) (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
t))
       (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
Op_type OpKind
Total [String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
s]
        (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
t) Range
nullRange) Range
nullRange, [])) ([(TypeClass, TypeClass)] -> [(OP_SYMB, [a])])
-> [(TypeClass, TypeClass)] -> [(OP_SYMB, [a])]
forall a b. (a -> b) -> a -> b
$ Rel TypeClass -> [(TypeClass, TypeClass)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel TypeClass -> [(TypeClass, TypeClass)])
-> Rel TypeClass -> [(TypeClass, TypeClass)]
forall a b. (a -> b) -> a -> b
$
       Rel TypeClass -> Rel TypeClass
forall a. Ord a => Rel a -> Rel a
Rel.irreflex Rel TypeClass
rel
      resType :: SORT -> (OP_SYMB, b) -> 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
      collectOps :: TypeClass -> Constraint
collectOps s :: TypeClass
s = SORT -> [(OP_SYMB, [Int])] -> SORT -> Constraint
Constraint (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
s)
       (((OP_SYMB, [Int]) -> Bool)
-> [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])]
forall a. (a -> Bool) -> [a] -> [a]
filter (SORT -> (OP_SYMB, [Int]) -> Bool
forall b. SORT -> (OP_SYMB, b) -> Bool
resType (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
s)) [(OP_SYMB, [Int])]
forall a. [(OP_SYMB, [a])]
injSyms) (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
name TypeClass
s)
      sortList :: [TypeClass]
sortList = Set TypeClass -> [TypeClass]
forall a. Set a -> [a]
Set.toList Set TypeClass
absCl
      constrs :: [Constraint]
constrs = (TypeClass -> Constraint) -> [TypeClass] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map TypeClass -> Constraint
collectOps [TypeClass]
sortList
  in
      [String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "disjEmbedd" ([Constraint] -> Bool -> CASLFORMULA
forall f. [Constraint] -> Bool -> FORMULA f
Sort_gen_ax [Constraint]
constrs Bool
True)]


mapSen :: CASLSign -> CSMOF.Sen -> CASLFORMULA
mapSen :: CASLSign -> Sen -> CASLFORMULA
mapSen sig :: CASLSign
sig (Sen con :: MultConstr
con car :: Integer
car cot :: ConstraintType
cot) = -- trueForm
   case ConstraintType
cot of
     EQUAL -> let
                minC :: CASLFORMULA
minC = MultConstr -> Integer -> PredMap -> CASLFORMULA
minConstraint MultConstr
con Integer
car (CASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap CASLSign
sig)
                maxC :: CASLFORMULA
maxC = MultConstr -> Integer -> PredMap -> CASLFORMULA
maxConstraint MultConstr
con Integer
car (CASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap CASLSign
sig)
              in
                Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con (CASLFORMULA
minC CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [CASLFORMULA
maxC]) Range
nullRange
     LEQ -> MultConstr -> Integer -> PredMap -> CASLFORMULA
maxConstraint MultConstr
con Integer
car (CASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap CASLSign
sig)
     GEQ -> MultConstr -> Integer -> PredMap -> CASLFORMULA
minConstraint MultConstr
con Integer
car (CASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap CASLSign
sig)


minConstraint :: MultConstr -> Integer -> PredMap -> CASLFORMULA
minConstraint :: MultConstr -> Integer -> PredMap -> CASLFORMULA
minConstraint con :: MultConstr
con int :: Integer
int predM :: PredMap
predM =
  let
    predTypes :: Set PredType
predTypes = SORT -> PredMap -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ MultConstr -> String
getRole MultConstr
con) PredMap
predM -- Set PredType
    souVars :: [SIMPLE_ID]
souVars = String -> Integer -> [SIMPLE_ID]
generateVars "x" 1
    tarVars :: [SIMPLE_ID]
tarVars = String -> Integer -> [SIMPLE_ID]
generateVars "y" Integer
int
    correctPredType :: [PredType]
correctPredType = (PredType -> [PredType] -> [PredType])
-> [PredType] -> Set PredType -> [PredType]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (MultConstr -> PredType -> [PredType] -> [PredType]
getCorrectPredType MultConstr
con) [] Set PredType
predTypes
    souVarDec :: VAR_DECL
souVarDec = [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID]
souVars ([SORT] -> SORT
forall a. [a] -> a
head (PredType -> [SORT]
predArgs ([PredType] -> PredType
forall a. [a] -> a
head [PredType]
correctPredType))) Range
nullRange
    tarVarDec :: VAR_DECL
tarVarDec = [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID]
tarVars ([SORT] -> SORT
forall a. [a] -> a
last (PredType -> [SORT]
predArgs ([PredType] -> PredType
forall a. [a] -> a
head [PredType]
correctPredType))) Range
nullRange
  in
    if Integer
int Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 1
    then QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [VAR_DECL
souVarDec] (QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification
          QUANTIFIER
Existential [VAR_DECL
tarVarDec] (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con (VAR_DECL -> CASLFORMULA
generateVarDiff VAR_DECL
tarVarDec CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
:
            [VAR_DECL -> VAR_DECL -> SORT -> CASLFORMULA
generateProp VAR_DECL
souVarDec VAR_DECL
tarVarDec (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ MultConstr -> String
getRole MultConstr
con)])
             Range
nullRange) Range
nullRange) Range
nullRange
    else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [VAR_DECL
souVarDec] (QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification
          QUANTIFIER
Existential [VAR_DECL
tarVarDec] (VAR_DECL -> VAR_DECL -> SORT -> CASLFORMULA
generateProp VAR_DECL
souVarDec VAR_DECL
tarVarDec
            (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ MultConstr -> String
getRole MultConstr
con)) Range
nullRange) Range
nullRange

getCorrectPredType :: MultConstr -> PredType -> [PredType] -> [PredType]
getCorrectPredType :: MultConstr -> PredType -> [PredType] -> [PredType]
getCorrectPredType con :: MultConstr
con pt :: PredType
pt ptLis :: [PredType]
ptLis =
   if String -> SORT
stringToId (TypeClass -> String
name (MultConstr -> TypeClass
CSMOF.getType MultConstr
con)) SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== [SORT] -> SORT
forall a. [a] -> a
head (PredType -> [SORT]
predArgs PredType
pt)
   then PredType
pt PredType -> [PredType] -> [PredType]
forall a. a -> [a] -> [a]
: [PredType]
ptLis else [PredType]
ptLis

generateVars :: String -> Integer -> [VAR]
generateVars :: String -> Integer -> [SIMPLE_ID]
generateVars varRoot :: String
varRoot int :: Integer
int =
  case Integer
int of
    1 -> [String -> SIMPLE_ID
mkSimpleId (String
varRoot String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
int)]
    n :: Integer
n -> String -> SIMPLE_ID
mkSimpleId (String
varRoot String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
int) SIMPLE_ID -> [SIMPLE_ID] -> [SIMPLE_ID]
forall a. a -> [a] -> [a]
: String -> Integer -> [SIMPLE_ID]
generateVars String
varRoot (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1)

generateVarDiff :: VAR_DECL -> CASLFORMULA
generateVarDiff :: VAR_DECL -> CASLFORMULA
generateVarDiff (Var_decl vars :: [SIMPLE_ID]
vars sor :: SORT
sor _) = Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con
 ((SIMPLE_ID -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> [SIMPLE_ID] -> [CASLFORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
(++) ([CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA])
-> (SIMPLE_ID -> [CASLFORMULA])
-> SIMPLE_ID
-> [CASLFORMULA]
-> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> [SIMPLE_ID] -> SIMPLE_ID -> [CASLFORMULA]
diffOfRest SORT
sor [SIMPLE_ID]
vars) [] [SIMPLE_ID]
vars) Range
nullRange

diffOfRest :: SORT -> [VAR] -> VAR -> [CASLFORMULA]
diffOfRest :: SORT -> [SIMPLE_ID] -> SIMPLE_ID -> [CASLFORMULA]
diffOfRest sor :: SORT
sor vars :: [SIMPLE_ID]
vars var :: SIMPLE_ID
var = (SIMPLE_ID -> CASLFORMULA) -> [SIMPLE_ID] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (SORT -> SIMPLE_ID -> SIMPLE_ID -> CASLFORMULA
diffVar SORT
sor SIMPLE_ID
var) [SIMPLE_ID]
vars

diffVar :: SORT -> VAR -> VAR -> CASLFORMULA
diffVar :: SORT -> SIMPLE_ID -> SIMPLE_ID -> CASLFORMULA
diffVar sor :: SORT
sor var1 :: SIMPLE_ID
var1 var2 :: SIMPLE_ID
var2 =
  if SIMPLE_ID
var1 SIMPLE_ID -> SIMPLE_ID -> Bool
forall a. Eq a => a -> a -> Bool
/= SIMPLE_ID
var2
  then CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
                 (SIMPLE_ID -> SORT -> Range -> TERM ()
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
var1 SORT
sor Range
nullRange)
                 Equality
Strong
                 (SIMPLE_ID -> SORT -> Range -> TERM ()
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
var2 SORT
sor Range
nullRange)
                 Range
nullRange)
       Range
nullRange
  else CASLFORMULA
forall f. FORMULA f
trueForm

generateProp :: VAR_DECL -> VAR_DECL -> Id -> CASLFORMULA
generateProp :: VAR_DECL -> VAR_DECL -> SORT -> CASLFORMULA
generateProp (Var_decl varD :: [SIMPLE_ID]
varD sort :: SORT
sort _) (Var_decl varD2 :: [SIMPLE_ID]
varD2 sort2 :: SORT
sort2 _) rol :: SORT
rol =
  Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con ((SIMPLE_ID -> CASLFORMULA) -> [SIMPLE_ID] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (SIMPLE_ID -> SORT -> SORT -> SORT -> SIMPLE_ID -> CASLFORMULA
createPropRel ([SIMPLE_ID] -> SIMPLE_ID
forall a. [a] -> a
head [SIMPLE_ID]
varD) SORT
sort SORT
rol SORT
sort2) [SIMPLE_ID]
varD2) Range
nullRange

createPropRel :: VAR -> SORT -> Id -> SORT -> VAR -> CASLFORMULA
createPropRel :: SIMPLE_ID -> SORT -> SORT -> SORT -> SIMPLE_ID -> CASLFORMULA
createPropRel souVar :: SIMPLE_ID
souVar sor :: SORT
sor rol :: SORT
rol sor2 :: SORT
sor2 tarVar :: SIMPLE_ID
tarVar =
  PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (SORT -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name SORT
rol ([SORT] -> Range -> PRED_TYPE
Pred_type [SORT
sor, SORT
sor2] Range
nullRange) Range
nullRange)
    (SIMPLE_ID -> SORT -> Range -> TERM ()
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
souVar SORT
sor Range
nullRange TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: [SIMPLE_ID -> SORT -> Range -> TERM ()
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
tarVar SORT
sor2 Range
nullRange]) Range
nullRange


maxConstraint :: MultConstr -> Integer -> PredMap -> CASLFORMULA
maxConstraint :: MultConstr -> Integer -> PredMap -> CASLFORMULA
maxConstraint con :: MultConstr
con int :: Integer
int predM :: PredMap
predM =
  let
    predTypes :: Set PredType
predTypes = SORT -> PredMap -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ MultConstr -> String
getRole MultConstr
con) PredMap
predM -- Set PredType
    souVars :: [SIMPLE_ID]
souVars = String -> Integer -> [SIMPLE_ID]
generateVars "x" 1
    tarVars :: [SIMPLE_ID]
tarVars = String -> Integer -> [SIMPLE_ID]
generateVars "y" (Integer
int Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1)
    correctPredType :: [PredType]
correctPredType = (PredType -> [PredType] -> [PredType])
-> [PredType] -> Set PredType -> [PredType]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (MultConstr -> PredType -> [PredType] -> [PredType]
getCorrectPredType MultConstr
con) [] Set PredType
predTypes
    souVarDec :: VAR_DECL
souVarDec = [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID]
souVars ([SORT] -> SORT
forall a. [a] -> a
head (PredType -> [SORT]
predArgs ([PredType] -> PredType
forall a. [a] -> a
head [PredType]
correctPredType))) Range
nullRange
    tarVarDec :: VAR_DECL
tarVarDec = [SIMPLE_ID] -> SORT -> Range -> VAR_DECL
Var_decl [SIMPLE_ID]
tarVars ([SORT] -> SORT
forall a. [a] -> a
last (PredType -> [SORT]
predArgs ([PredType] -> PredType
forall a. [a] -> a
head [PredType]
correctPredType))) Range
nullRange
  in
    QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal (VAR_DECL
souVarDec VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL
tarVarDec])
                   (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation
                      (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [VAR_DECL -> VAR_DECL -> SORT -> CASLFORMULA
generateProp VAR_DECL
souVarDec VAR_DECL
tarVarDec (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ MultConstr -> String
getRole MultConstr
con)] Range
nullRange)
                      Relation
Implication
                      (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis (VAR_DECL -> [CASLFORMULA]
generateExEqual VAR_DECL
tarVarDec) Range
nullRange)
                      Range
nullRange)
                   Range
nullRange

generateExEqual :: VAR_DECL -> [CASLFORMULA]
generateExEqual :: VAR_DECL -> [CASLFORMULA]
generateExEqual (Var_decl varD :: [SIMPLE_ID]
varD sor :: SORT
sor _) = [SIMPLE_ID] -> SORT -> [CASLFORMULA]
generateExEqualList [SIMPLE_ID]
varD SORT
sor

generateExEqualList :: [VAR] -> SORT -> [CASLFORMULA]
generateExEqualList :: [SIMPLE_ID] -> SORT -> [CASLFORMULA]
generateExEqualList vars :: [SIMPLE_ID]
vars sor :: SORT
sor =
  case [SIMPLE_ID]
vars of
    [] -> []
    v :: SIMPLE_ID
v : rest :: [SIMPLE_ID]
rest -> [SIMPLE_ID] -> SORT -> SIMPLE_ID -> [CASLFORMULA]
generateExEqualVar [SIMPLE_ID]
rest SORT
sor SIMPLE_ID
v [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [SIMPLE_ID] -> SORT -> [CASLFORMULA]
generateExEqualList [SIMPLE_ID]
rest SORT
sor

generateExEqualVar :: [VAR] -> SORT -> VAR -> [CASLFORMULA]
generateExEqualVar :: [SIMPLE_ID] -> SORT -> SIMPLE_ID -> [CASLFORMULA]
generateExEqualVar vars :: [SIMPLE_ID]
vars sor :: SORT
sor var :: SIMPLE_ID
var =
  (SIMPLE_ID -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> [SIMPLE_ID] -> [CASLFORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
(++) ([CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA])
-> (SIMPLE_ID -> [CASLFORMULA])
-> SIMPLE_ID
-> [CASLFORMULA]
-> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ el :: SIMPLE_ID
el -> if SIMPLE_ID
el SIMPLE_ID -> SIMPLE_ID -> Bool
forall a. Eq a => a -> a -> Bool
== SIMPLE_ID
var
                then []
                else [TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation (SIMPLE_ID -> SORT -> Range -> TERM ()
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
var SORT
sor Range
nullRange) Equality
Strong
                       (SIMPLE_ID -> SORT -> Range -> TERM ()
forall f. SIMPLE_ID -> SORT -> Range -> TERM f
Qual_var SIMPLE_ID
el SORT
sor Range
nullRange) Range
nullRange]))
        [] [SIMPLE_ID]
vars


-- | Translation of morphisms
mapMor :: CSMOF.Morphism -> Result CASLMor
mapMor :: Morphism -> Result CASLMor
mapMor m :: Morphism
m = CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism :: forall f e m.
Sign f e
-> Sign f e
-> Sort_map
-> Op_map
-> Pred_map
-> m
-> Morphism f e m
C.Morphism
  { msource :: CASLSign
msource = Sign -> CASLSign
mapSign (Sign -> CASLSign) -> Sign -> CASLSign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
forall sign. DefaultMorphism sign -> sign
domOfDefaultMorphism Morphism
m
  , mtarget :: CASLSign
mtarget = Sign -> CASLSign
mapSign (Sign -> CASLSign) -> Sign -> CASLSign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
forall sign. DefaultMorphism sign -> sign
codOfDefaultMorphism Morphism
m
  , sort_map :: Sort_map
sort_map = Sort_map
forall k a. Map k a
Map.empty
  , op_map :: Op_map
op_map = Op_map
forall k a. Map k a
Map.empty
  , pred_map :: Pred_map
pred_map = Pred_map
forall k a. Map k a
Map.empty
  , extended_map :: ()
extended_map = ()
  }


-- mapSym :: CSMOF.Symbol -> C.Symbol