{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/QVTR2CASL.hs
Description :  Coding QVTR 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.QVTR2CASL
    ( QVTR2CASL (..)
    ) where

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

-- CSMOF
import qualified Comorphisms.CSMOF2CASL as CSMOF2CASL
import qualified CSMOF.Sign as CSMOF

-- QVTR
import QVTR.Logic_QVTR as QVTR
import QVTR.As as QVTRAs
import QVTR.Sign as QVTR
import QVTR.StatAna as QVTRAn

-- 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.ProofTree
import Common.Result
import Common.Id

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

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


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

instance Language QVTR2CASL -- default is ok

instance Comorphism QVTR2CASL
    QVTR.QVTR
    ()
    QVTRAs.Transformation
    QVTR.Sen
    ()
    ()
    QVTR.Sign
    QVTR.Morphism
    ()
    ()
    ()
    CASL
    CASL_Sublogics
    CASLBasicSpec
    CASLFORMULA
    SYMB_ITEMS
    SYMB_MAP_ITEMS
    CASLSign
    CASLMor
    C.Symbol
    C.RawSymbol
    ProofTree
    where
      sourceLogic :: QVTR2CASL -> QVTR
sourceLogic QVTR2CASL = QVTR
QVTR
      sourceSublogic :: QVTR2CASL -> ()
sourceSublogic QVTR2CASL = ()
      targetLogic :: QVTR2CASL -> CASL
targetLogic QVTR2CASL = CASL
CASL
      mapSublogic :: QVTR2CASL -> () -> Maybe CASL_Sublogics
mapSublogic QVTR2CASL _ = 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 :: QVTR2CASL
-> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
map_theory QVTR2CASL = (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory
      map_sentence :: QVTR2CASL -> Sign -> Sen -> Result CASLFORMULA
map_sentence QVTR2CASL 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
. Sign -> CASLSign -> Sen -> CASLFORMULA
mapSen Sign
s (Sign -> CASLSign
mapSign Sign
s)
      map_morphism :: QVTR2CASL -> Morphism -> Result CASLMor
map_morphism QVTR2CASL = Morphism -> Result CASLMor
mapMor
      -- map_symbol QVTR2CASL _ = Set.singleton . mapSym
      is_model_transportable :: QVTR2CASL -> Bool
is_model_transportable QVTR2CASL = Bool
True
      has_model_expansion :: QVTR2CASL -> Bool
has_model_expansion QVTR2CASL = Bool
True
      is_weakly_amalgamable :: QVTR2CASL -> Bool
is_weakly_amalgamable QVTR2CASL = Bool
True
      isInclusionComorphism :: QVTR2CASL -> Bool
isInclusionComorphism QVTR2CASL = Bool
True


mapTheory :: (QVTR.Sign, [Named QVTR.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
$ Sign -> CASLSign -> Sen -> CASLFORMULA
mapSen Sign
s 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 :: QVTR.Sign -> CASLSign
mapSign :: Sign -> CASLSign
mapSign s :: Sign
s =
  let
    sSign :: CASLSign
sSign = Sign -> CASLSign
CSMOF2CASL.mapSign (Sign -> Sign
sourceSign Sign
s)
    tSign :: CASLSign
tSign = Sign -> CASLSign
CSMOF2CASL.mapSign (Sign -> Sign
targetSign Sign
s)
    relsProp :: PredMap
relsProp = Map String RuleDef -> Map String RuleDef -> PredMap
getPropertiesFromRelations (Sign -> Map String RuleDef
nonTopRelations Sign
s) (Sign -> Map String RuleDef
topRelations Sign
s)
    keysProp :: PredMap
keysProp = [(String, String)] -> PredMap
getPropertiesFromKeys (Sign -> [(String, String)]
keyDefs Sign
s)
    sUnion :: CASLSign
sUnion = CASLSign -> CASLSign -> CASLSign
C.uniteCASLSign CASLSign
sSign CASLSign
tSign
    everyProp :: PredMap
everyProp = PredMap -> PredMap -> PredMap
C.addMapSet (CASLSign -> PredMap
forall f e. Sign f e -> PredMap
C.predMap CASLSign
sUnion) (PredMap -> PredMap -> PredMap
C.addMapSet PredMap
relsProp PredMap
keysProp)
    sentRels :: [Named CASLFORMULA]
sentRels = CASLSign -> [Named CASLFORMULA]
forall f e. Sign f e -> [Named (FORMULA f)]
C.sentences CASLSign
sSign [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ CASLSign -> [Named CASLFORMULA]
forall f e. Sign f e -> [Named (FORMULA f)]
C.sentences CASLSign
tSign
  in
    CASLSign -> CASLSign
addStringSignature (CASLSign -> PredMap -> CASLSign
replacePredMap (CASLSign -> [Named CASLFORMULA] -> CASLSign
replaceSentences CASLSign
sUnion [Named CASLFORMULA]
sentRels) PredMap
everyProp)


getPropertiesFromRelations :: Map.Map String RuleDef -> Map.Map String RuleDef -> PredMap
getPropertiesFromRelations :: Map String RuleDef -> Map String RuleDef -> PredMap
getPropertiesFromRelations nonTopRel :: Map String RuleDef
nonTopRel topRel :: Map String RuleDef
topRel = [(String, RuleDef)] -> PredMap
getRelDef ([(String, RuleDef)] -> PredMap) -> [(String, RuleDef)] -> PredMap
forall a b. (a -> b) -> a -> b
$ Map String RuleDef -> [(String, RuleDef)]
forall k a. Map k a -> [(k, a)]
Map.assocs Map String RuleDef
nonTopRel
                                               [(String, RuleDef)] -> [(String, RuleDef)] -> [(String, RuleDef)]
forall a. [a] -> [a] -> [a]
++ Map String RuleDef -> [(String, RuleDef)]
forall k a. Map k a -> [(k, a)]
Map.assocs Map String RuleDef
topRel


getRelDef :: [(String, RuleDef)] -> PredMap
getRelDef :: [(String, RuleDef)] -> PredMap
getRelDef [] = PredMap
forall a b. MapSet a b
MapSet.empty
getRelDef ((nam :: String
nam, rulDef :: RuleDef
rulDef) : rest :: [(String, RuleDef)]
rest) =
  let na :: Id
na = String -> Id
stringToId String
nam
      pa :: [Id]
pa = (TypeClass -> [Id] -> [Id]) -> [Id] -> [TypeClass] -> [Id]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((:) (Id -> [Id] -> [Id])
-> (TypeClass -> Id) -> TypeClass -> [Id] -> [Id]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Id
stringToId (String -> Id) -> (TypeClass -> String) -> TypeClass -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeClass -> String
CSMOF.name) [] (RuleDef -> [TypeClass]
QVTR.parameters RuleDef
rulDef)
  in Id -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
na ([Id] -> PredType
C.PredType [Id]
pa) ([(String, RuleDef)] -> PredMap
getRelDef [(String, RuleDef)]
rest)


getPropertiesFromKeys :: [(String, String)] -> PredMap
getPropertiesFromKeys :: [(String, String)] -> PredMap
getPropertiesFromKeys [] = PredMap
forall a b. MapSet a b
MapSet.empty
getPropertiesFromKeys ((met :: String
met, typ :: String
typ) : rest :: [(String, String)]
rest) =
  Id -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (String -> String -> Id
predKeyName String
met String
typ) ([Id] -> PredType
C.PredType []) ([(String, String)] -> PredMap
getPropertiesFromKeys [(String, String)]
rest)


predKeyName :: String -> String -> Id
predKeyName :: String -> String -> Id
predKeyName met :: String
met typ :: String
typ = String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ "key_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
met String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
typ


replacePredMap :: CASLSign -> PredMap -> CASLSign
replacePredMap :: CASLSign -> PredMap -> CASLSign
replacePredMap (C.Sign sR :: Rel Id
sR rSR :: Maybe (Rel Id)
rSR eSR :: Set Id
eSR oM :: OpMap
oM aO :: OpMap
aO _ vM :: Map SIMPLE_ID Id
vM s :: [Named CASLFORMULA]
s dS :: Set Symbol
dS eD :: [Diagnosis]
eD aM :: AnnoMap
aM gA :: GlobalAnnos
gA eI :: ()
eI) predM :: PredMap
predM =
  Rel Id
-> Maybe (Rel Id)
-> Set Id
-> OpMap
-> OpMap
-> PredMap
-> Map SIMPLE_ID Id
-> [Named CASLFORMULA]
-> Set Symbol
-> [Diagnosis]
-> AnnoMap
-> GlobalAnnos
-> ()
-> CASLSign
forall f e.
Rel Id
-> Maybe (Rel Id)
-> Set Id
-> OpMap
-> OpMap
-> PredMap
-> Map SIMPLE_ID Id
-> [Named (FORMULA f)]
-> Set Symbol
-> [Diagnosis]
-> AnnoMap
-> GlobalAnnos
-> e
-> Sign f e
C.Sign Rel Id
sR Maybe (Rel Id)
rSR Set Id
eSR OpMap
oM OpMap
aO PredMap
predM Map SIMPLE_ID Id
vM [Named CASLFORMULA]
s Set Symbol
dS [Diagnosis]
eD AnnoMap
aM GlobalAnnos
gA ()
eI


replaceSentences :: CASLSign -> [Named CASLFORMULA] -> CASLSign
replaceSentences :: CASLSign -> [Named CASLFORMULA] -> CASLSign
replaceSentences (C.Sign sR :: Rel Id
sR rSR :: Maybe (Rel Id)
rSR eSR :: Set Id
eSR oM :: OpMap
oM aO :: OpMap
aO pM :: PredMap
pM vM :: Map SIMPLE_ID Id
vM _ dS :: Set Symbol
dS eD :: [Diagnosis]
eD aM :: AnnoMap
aM gA :: GlobalAnnos
gA eI :: ()
eI) sent :: [Named CASLFORMULA]
sent =
  Rel Id
-> Maybe (Rel Id)
-> Set Id
-> OpMap
-> OpMap
-> PredMap
-> Map SIMPLE_ID Id
-> [Named CASLFORMULA]
-> Set Symbol
-> [Diagnosis]
-> AnnoMap
-> GlobalAnnos
-> ()
-> CASLSign
forall f e.
Rel Id
-> Maybe (Rel Id)
-> Set Id
-> OpMap
-> OpMap
-> PredMap
-> Map SIMPLE_ID Id
-> [Named (FORMULA f)]
-> Set Symbol
-> [Diagnosis]
-> AnnoMap
-> GlobalAnnos
-> e
-> Sign f e
C.Sign Rel Id
sR Maybe (Rel Id)
rSR Set Id
eSR OpMap
oM OpMap
aO PredMap
pM Map SIMPLE_ID Id
vM [Named CASLFORMULA]
sent Set Symbol
dS [Diagnosis]
eD AnnoMap
aM GlobalAnnos
gA ()
eI


-- ------ Sentences

mapSen :: QVTR.Sign -> CASLSign -> QVTR.Sen -> CASLFORMULA
mapSen :: Sign -> CASLSign -> Sen -> CASLFORMULA
mapSen qvtrSign :: Sign
qvtrSign _ (KeyConstr k :: Key
k) = Sign -> Key -> CASLFORMULA
createKeyFormula Sign
qvtrSign Key
k
mapSen qvtrSign :: Sign
qvtrSign sig :: CASLSign
sig (QVTSen r :: RelationSen
r) = Sign -> CASLSign -> RelationSen -> CASLFORMULA
createRuleFormula Sign
qvtrSign CASLSign
sig RelationSen
r


createKeyFormula :: QVTR.Sign -> Key -> CASLFORMULA
createKeyFormula :: Sign -> Key -> CASLFORMULA
createKeyFormula qvtrSign :: Sign
qvtrSign k :: Key
k =
  let
    souVars :: [SIMPLE_ID]
souVars = String -> Integer -> [SIMPLE_ID]
CSMOF2CASL.generateVars "x" 2
    tarVars :: [SIMPLE_ID]
tarVars = String -> Integer -> [SIMPLE_ID]
CSMOF2CASL.generateVars "y" (Integer -> [SIMPLE_ID]) -> Integer -> [SIMPLE_ID]
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ [PropKey] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([PropKey] -> Int) -> [PropKey] -> Int
forall a b. (a -> b) -> a -> b
$ Key -> [PropKey]
properties Key
k
    typeSouVar :: Id
typeSouVar = String -> Id
stringToId (Key -> String
typeName Key
k)
    souVarDec :: VAR_DECL
souVarDec = [SIMPLE_ID] -> Id -> Range -> VAR_DECL
Var_decl [SIMPLE_ID]
souVars Id
typeSouVar Range
nullRange
    (tarVarDec :: [VAR_DECL]
tarVarDec, props :: [Maybe PropertyT]
props) = Sign
-> [SIMPLE_ID]
-> [PropKey]
-> String
-> ([VAR_DECL], [Maybe PropertyT])
getVarFromKey Sign
qvtrSign [SIMPLE_ID]
tarVars (Key -> [PropKey]
properties Key
k) (Key -> String
typeName Key
k)
    pname :: Id
pname = String -> String -> Id
predKeyName (Key -> String
metamodel Key
k) (Key -> String
typeName Key
k)
    equal :: FORMULA f
equal = FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation (TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation (SIMPLE_ID -> Id -> Range -> TERM f
forall f. SIMPLE_ID -> Id -> Range -> TERM f
Qual_var ([SIMPLE_ID] -> SIMPLE_ID
forall a. [a] -> a
head [SIMPLE_ID]
souVars) Id
typeSouVar Range
nullRange)
                               Equality
Strong
                               (SIMPLE_ID -> Id -> Range -> TERM f
forall f. SIMPLE_ID -> Id -> Range -> TERM f
Qual_var ([SIMPLE_ID] -> SIMPLE_ID
forall a. [a] -> a
head ([SIMPLE_ID] -> SIMPLE_ID) -> [SIMPLE_ID] -> SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ [SIMPLE_ID] -> [SIMPLE_ID]
forall a. [a] -> [a]
tail [SIMPLE_ID]
souVars) Id
typeSouVar Range
nullRange)
                               Range
nullRange)
                     Range
nullRange
    sent :: CASLFORMULA
sent = CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
C.Relation CASLFORMULA
forall f. FORMULA f
equal
                      Relation
Implication
                      (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
C.Relation
                         (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con (SIMPLE_ID
-> String
-> [SIMPLE_ID]
-> [PropKey]
-> [Maybe PropertyT]
-> [CASLFORMULA]
getPredicatesInvocation (String -> SIMPLE_ID
mkSimpleId "x_1")
                           (Key -> String
typeName Key
k) [SIMPLE_ID]
tarVars (Key -> [PropKey]
properties Key
k) [Maybe PropertyT]
props) Range
nullRange)
                         Relation
Implication
                         (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
`Negation` Range
nullRange)
                                       (SIMPLE_ID
-> String
-> [SIMPLE_ID]
-> [PropKey]
-> [Maybe PropertyT]
-> [CASLFORMULA]
getPredicatesInvocation (String -> SIMPLE_ID
mkSimpleId "x_2")
                          (Key -> String
typeName Key
k) [SIMPLE_ID]
tarVars (Key -> [PropKey]
properties Key
k) [Maybe PropertyT]
props)) Range
nullRange)
                         Range
nullRange)
                      Range
nullRange
  in
    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 (Id -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name Id
pname ([Id] -> Range -> PRED_TYPE
Pred_type [] Range
nullRange) Range
nullRange)
                     []
                     Range
nullRange)
      Relation
C.Equivalence
      (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
sent Range
nullRange)
      Range
nullRange


getPredicatesInvocation :: VAR -> String -> [VAR] -> [PropKey] -> [Maybe CSMOF.PropertyT] -> [CASLFORMULA]
getPredicatesInvocation :: SIMPLE_ID
-> String
-> [SIMPLE_ID]
-> [PropKey]
-> [Maybe PropertyT]
-> [CASLFORMULA]
getPredicatesInvocation _ _ [] [] [] = []
getPredicatesInvocation x :: SIMPLE_ID
x typN :: String
typN (v :: SIMPLE_ID
v : restV :: [SIMPLE_ID]
restV) (p :: PropKey
p : restP :: [PropKey]
restP) (pT :: Maybe PropertyT
pT : restPT :: [Maybe PropertyT]
restPT) =
  let pr :: FORMULA f
pr = case Maybe PropertyT
pT of
             Nothing -> FORMULA f
forall f. FORMULA f
trueForm
             Just prop :: PropertyT
prop -> case PropKey
p of
                            SimpleProp pN :: String
pN -> let sor :: String
sor = String -> PropertyT -> String
QVTRAn.getOppositeType String
pN PropertyT
prop
                                                 sor2 :: String
sor2 = String -> PropertyT -> String
QVTRAn.getTargetType String
pN PropertyT
prop
                                             in PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                                  (Id -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name (String -> Id
stringToId String
pN)
                                                     ([Id] -> Range -> PRED_TYPE
Pred_type
                                                       [String -> Id
stringToId String
sor,
                                                        String -> Id
stringToId String
sor2]
                                                       Range
nullRange) Range
nullRange)
                                                  (SIMPLE_ID -> Id -> Range -> TERM f
forall f. SIMPLE_ID -> Id -> Range -> TERM f
Qual_var SIMPLE_ID
x (String -> Id
stringToId String
typN)
                                                    Range
nullRange TERM f -> [TERM f] -> [TERM f]
forall a. a -> [a] -> [a]
:
                                                   [SIMPLE_ID -> Id -> Range -> TERM f
forall f. SIMPLE_ID -> Id -> Range -> TERM f
Qual_var SIMPLE_ID
v (String -> Id
stringToId String
sor2)
                                                     Range
nullRange]) Range
nullRange
                            OppositeProp oPType :: String
oPType oPName :: String
oPName ->
                             let sor :: String
sor = String -> PropertyT -> String
QVTRAn.getTargetType String
oPName PropertyT
prop
                             in PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                 (Id -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name (String -> Id
stringToId String
oPName)
                                 ([Id] -> Range -> PRED_TYPE
Pred_type [String -> Id
stringToId String
oPType,
                                             String -> Id
stringToId String
sor] Range
nullRange)
                                   Range
nullRange)
                                 (SIMPLE_ID -> Id -> Range -> TERM f
forall f. SIMPLE_ID -> Id -> Range -> TERM f
Qual_var SIMPLE_ID
v (String -> Id
stringToId String
oPType) Range
nullRange TERM f -> [TERM f] -> [TERM f]
forall a. a -> [a] -> [a]
:
                                  [SIMPLE_ID -> Id -> Range -> TERM f
forall f. SIMPLE_ID -> Id -> Range -> TERM f
Qual_var SIMPLE_ID
x (String -> Id
stringToId String
typN) Range
nullRange])
                                Range
nullRange
  in CASLFORMULA
forall f. FORMULA f
pr CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: SIMPLE_ID
-> String
-> [SIMPLE_ID]
-> [PropKey]
-> [Maybe PropertyT]
-> [CASLFORMULA]
getPredicatesInvocation SIMPLE_ID
x String
typN [SIMPLE_ID]
restV [PropKey]
restP [Maybe PropertyT]
restPT
getPredicatesInvocation _ _ _ _ _ = []


getVarFromKey :: QVTR.Sign -> [VAR] -> [PropKey] -> String -> ([VAR_DECL], [Maybe CSMOF.PropertyT])
getVarFromKey :: Sign
-> [SIMPLE_ID]
-> [PropKey]
-> String
-> ([VAR_DECL], [Maybe PropertyT])
getVarFromKey _ [] [] _ = ([], [])
getVarFromKey qvtrSign :: Sign
qvtrSign (v :: SIMPLE_ID
v : restV :: [SIMPLE_ID]
restV) (p :: PropKey
p : restP :: [PropKey]
restP) typN :: String
typN =
  let
    (decl :: VAR_DECL
decl, prop :: Maybe PropertyT
prop) = case PropKey
p of
                    SimpleProp pN :: String
pN -> let (idP :: Id
idP, propT :: Maybe PropertyT
propT) = Sign -> String -> String -> (Id, Maybe PropertyT)
getSortOfProperty Sign
qvtrSign String
typN String
pN
                                     in ([SIMPLE_ID] -> Id -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
v] Id
idP Range
nullRange, Maybe PropertyT
propT)
                    OppositeProp oPType :: String
oPType oPName :: String
oPName -> let (_, propT :: Maybe PropertyT
propT) = Sign -> String -> String -> (Id, Maybe PropertyT)
getSortOfProperty Sign
qvtrSign String
oPType String
oPName
                                                  in ([SIMPLE_ID] -> Id -> Range -> VAR_DECL
Var_decl [SIMPLE_ID
v] (String -> Id
stringToId String
oPType) Range
nullRange, Maybe PropertyT
propT)
    (restD :: [VAR_DECL]
restD, restPr :: [Maybe PropertyT]
restPr) = Sign
-> [SIMPLE_ID]
-> [PropKey]
-> String
-> ([VAR_DECL], [Maybe PropertyT])
getVarFromKey Sign
qvtrSign [SIMPLE_ID]
restV [PropKey]
restP String
typN
  in
    (VAR_DECL
decl VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
restD, Maybe PropertyT
prop Maybe PropertyT -> [Maybe PropertyT] -> [Maybe PropertyT]
forall a. a -> [a] -> [a]
: [Maybe PropertyT]
restPr)
getVarFromKey _ _ _ _ = ([], [])


getSortOfProperty :: QVTR.Sign -> String -> String -> (Id, Maybe CSMOF.PropertyT)
getSortOfProperty :: Sign -> String -> String -> (Id, Maybe PropertyT)
getSortOfProperty qvtrSign :: Sign
qvtrSign typN :: String
typN pN :: String
pN =
  let sourceProp :: Maybe PropertyT
sourceProp = Rel TypeClass
-> Set PropertyT -> String -> String -> Maybe PropertyT
QVTRAn.findPropertyInHierarchy (Sign -> Rel TypeClass
CSMOF.typeRel (Sign -> Rel TypeClass) -> Sign -> Rel TypeClass
forall a b. (a -> b) -> a -> b
$ Sign -> Sign
QVTR.sourceSign Sign
qvtrSign)
                                                  (Sign -> Set PropertyT
CSMOF.properties (Sign -> Set PropertyT) -> Sign -> Set PropertyT
forall a b. (a -> b) -> a -> b
$ Sign -> Sign
QVTR.sourceSign Sign
qvtrSign) String
typN String
pN
      targetProp :: Maybe PropertyT
targetProp = Rel TypeClass
-> Set PropertyT -> String -> String -> Maybe PropertyT
QVTRAn.findPropertyInHierarchy (Sign -> Rel TypeClass
CSMOF.typeRel (Sign -> Rel TypeClass) -> Sign -> Rel TypeClass
forall a b. (a -> b) -> a -> b
$ Sign -> Sign
QVTR.targetSign Sign
qvtrSign)
                                                  (Sign -> Set PropertyT
CSMOF.properties (Sign -> Set PropertyT) -> Sign -> Set PropertyT
forall a b. (a -> b) -> a -> b
$ Sign -> Sign
QVTR.targetSign Sign
qvtrSign) String
typN String
pN
  in
    case Maybe PropertyT
sourceProp of
      Nothing -> case Maybe PropertyT
targetProp of
                   Nothing -> (String -> Id
stringToId "", Maybe PropertyT
forall a. Maybe a
Nothing)
                   Just p :: PropertyT
p -> (String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ String -> PropertyT -> String
QVTRAn.getTargetType String
pN PropertyT
p, PropertyT -> Maybe PropertyT
forall a. a -> Maybe a
Just PropertyT
p)
      Just p :: PropertyT
p -> (String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ String -> PropertyT -> String
QVTRAn.getTargetType String
pN PropertyT
p, PropertyT -> Maybe PropertyT
forall a. a -> Maybe a
Just PropertyT
p)


createRuleFormula :: QVTR.Sign -> CASLSign -> QVTR.RelationSen -> CASLFORMULA
createRuleFormula :: Sign -> CASLSign -> RelationSen -> CASLFORMULA
createRuleFormula qvtSign :: Sign
qvtSign _ (QVTR.RelationSen rDef :: RuleDef
rDef varS :: [RelVar]
varS parS :: [RelVar]
parS souPat :: Pattern
souPat tarPat :: Pattern
tarPat whenC :: Maybe WhenWhere
whenC whereC :: Maybe WhenWhere
whereC) =
  let
    rName :: String
rName = RuleDef -> String
QVTR.name RuleDef
rDef
    parTyp :: [Id]
parTyp = (RelVar -> Id) -> [RelVar] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Id
stringToId (String -> Id) -> (RelVar -> String) -> RelVar -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelVar -> String
varType) [RelVar]
parS

    whenVarSet :: [RelVar]
whenVarSet = [RelVar] -> Maybe WhenWhere -> [RelVar]
collectWhenVarSet [RelVar]
varS Maybe WhenWhere
whenC

    souVarInOCL :: [RelVar]
souVarInOCL = ((String, String, OCL) -> [RelVar] -> [RelVar])
-> [RelVar] -> [(String, String, OCL)] -> [RelVar]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (_, _, ocl :: OCL
ocl) l :: [RelVar]
l -> [RelVar]
l [RelVar] -> [RelVar] -> [RelVar]
forall a. [a] -> [a] -> [a]
++ [RelVar] -> OCL -> [RelVar]
getVarIdsFromOCLExpre [RelVar]
varS OCL
ocl)
                   [] (Pattern -> [(String, String, OCL)]
QVTR.patPreds Pattern
souPat)
    souDomVarSet :: Set RelVar
souDomVarSet = [RelVar] -> Set RelVar
forall a. Ord a => [a] -> Set a
Set.fromList (Pattern -> [RelVar]
QVTR.patVarSet Pattern
souPat [RelVar] -> [RelVar] -> [RelVar]
forall a. [a] -> [a] -> [a]
++ [RelVar]
souVarInOCL)

    tarVarInOCL :: [RelVar]
tarVarInOCL = ((String, String, OCL) -> [RelVar] -> [RelVar])
-> [RelVar] -> [(String, String, OCL)] -> [RelVar]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (_, _, ocl :: OCL
ocl) l :: [RelVar]
l -> [RelVar]
l [RelVar] -> [RelVar] -> [RelVar]
forall a. [a] -> [a] -> [a]
++ [RelVar] -> OCL -> [RelVar]
getVarIdsFromOCLExpre [RelVar]
varS OCL
ocl)
                   [] (Pattern -> [(String, String, OCL)]
QVTR.patPreds Pattern
tarPat)
    tarDomVarSet :: Set RelVar
tarDomVarSet = [RelVar] -> Set RelVar
forall a. Ord a => [a] -> Set a
Set.fromList (Pattern -> [RelVar]
QVTR.patVarSet Pattern
tarPat [RelVar] -> [RelVar] -> [RelVar]
forall a. [a] -> [a] -> [a]
++ [RelVar]
tarVarInOCL)

    whereVarSet :: Set RelVar
whereVarSet = [RelVar] -> Set RelVar
forall a. Ord a => [a] -> Set a
Set.fromList ([RelVar] -> Set RelVar) -> [RelVar] -> Set RelVar
forall a b. (a -> b) -> a -> b
$ [RelVar] -> Maybe WhenWhere -> [RelVar]
collectWhenVarSet [RelVar]
varS Maybe WhenWhere
whereC

    varSet_2 :: Set RelVar
varSet_2 = Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set RelVar
tarDomVarSet Set RelVar
whereVarSet) ([RelVar] -> Set RelVar
forall a. Ord a => [a] -> Set a
Set.fromList [RelVar]
whenVarSet)) Set RelVar
souDomVarSet

  in
    if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
parS
    then 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 (Id -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name (String -> Id
stringToId String
rName) ([Id] -> Range -> PRED_TYPE
Pred_type [Id]
parTyp Range
nullRange) Range
nullRange)
                          []
                          Range
nullRange)
           Relation
C.Equivalence
           (if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
whenVarSet
            then Sign
-> [RelVar]
-> [RelVar]
-> Set RelVar
-> Pattern
-> Pattern
-> Maybe WhenWhere
-> CASLFORMULA
buildEmptyWhenFormula Sign
qvtSign [RelVar]
parS [RelVar]
varS Set RelVar
varSet_2 Pattern
souPat Pattern
tarPat Maybe WhenWhere
whereC
            else Sign
-> [RelVar]
-> [RelVar]
-> [RelVar]
-> Set RelVar
-> Pattern
-> Pattern
-> Maybe WhenWhere
-> Maybe WhenWhere
-> CASLFORMULA
buildNonEmptyWhenFormula Sign
qvtSign [RelVar]
whenVarSet [RelVar]
parS [RelVar]
varS Set RelVar
varSet_2 Pattern
souPat Pattern
tarPat Maybe WhenWhere
whenC Maybe WhenWhere
whereC)
           Range
nullRange
    else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
parS)
                        (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 (Id -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name (String -> Id
stringToId String
rName) ([Id] -> Range -> PRED_TYPE
Pred_type [Id]
parTyp Range
nullRange) Range
nullRange)
                                                   ([RelVar] -> [TERM ()]
createVarRule [RelVar]
parS)
                                                   Range
nullRange)
                                    Relation
C.Equivalence
                                    (if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
whenVarSet
                                     then Sign
-> [RelVar]
-> [RelVar]
-> Set RelVar
-> Pattern
-> Pattern
-> Maybe WhenWhere
-> CASLFORMULA
buildEmptyWhenFormula Sign
qvtSign [RelVar]
parS [RelVar]
varS Set RelVar
varSet_2 Pattern
souPat Pattern
tarPat Maybe WhenWhere
whereC
                                     else Sign
-> [RelVar]
-> [RelVar]
-> [RelVar]
-> Set RelVar
-> Pattern
-> Pattern
-> Maybe WhenWhere
-> Maybe WhenWhere
-> CASLFORMULA
buildNonEmptyWhenFormula Sign
qvtSign [RelVar]
whenVarSet [RelVar]
parS [RelVar]
varS Set RelVar
varSet_2 Pattern
souPat Pattern
tarPat Maybe WhenWhere
whenC Maybe WhenWhere
whereC)
                                    Range
nullRange)
                        Range
nullRange


createVarRule :: [RelVar] -> [C.CASLTERM]
createVarRule :: [RelVar] -> [TERM ()]
createVarRule = (RelVar -> TERM ()) -> [RelVar] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: RelVar
v -> SIMPLE_ID -> Id -> Range -> TERM ()
forall f. SIMPLE_ID -> Id -> Range -> TERM f
Qual_var (String -> SIMPLE_ID
mkSimpleId (String -> SIMPLE_ID) -> String -> SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ RelVar -> String
varName RelVar
v)
                                    (String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ RelVar -> String
varType RelVar
v) Range
nullRange)

collectWhenVarSet :: [RelVar] -> Maybe QVTRAs.WhenWhere -> [RelVar]
collectWhenVarSet :: [RelVar] -> Maybe WhenWhere -> [RelVar]
collectWhenVarSet _ Nothing = []
collectWhenVarSet varS :: [RelVar]
varS (Just (WhenWhere relInv :: [RelInvok]
relInv oclExp :: [OCL]
oclExp)) =
  let
    relVars :: [RelVar]
relVars = [Maybe RelVar] -> [RelVar]
forall a. [Maybe a] -> [a]
QVTRAn.getSomething ([Maybe RelVar] -> [RelVar]) -> [Maybe RelVar] -> [RelVar]
forall a b. (a -> b) -> a -> b
$ (String -> Maybe RelVar) -> [String] -> [Maybe RelVar]
forall a b. (a -> b) -> [a] -> [b]
map ([RelVar] -> String -> Maybe RelVar
findRelVarFromName [RelVar]
varS)
               ((RelInvok -> [String]) -> [RelInvok] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RelInvok -> [String]
QVTRAs.params [RelInvok]
relInv)
    oclExpVars :: [RelVar]
oclExpVars = (OCL -> [RelVar] -> [RelVar]) -> [RelVar] -> [OCL] -> [RelVar]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([RelVar] -> [RelVar] -> [RelVar]
forall a. [a] -> [a] -> [a]
(++) ([RelVar] -> [RelVar] -> [RelVar])
-> (OCL -> [RelVar]) -> OCL -> [RelVar] -> [RelVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RelVar] -> OCL -> [RelVar]
getVarIdsFromOCLExpre [RelVar]
varS) [] [OCL]
oclExp
  in
    [RelVar]
relVars [RelVar] -> [RelVar] -> [RelVar]
forall a. [a] -> [a] -> [a]
++ [RelVar]
oclExpVars


findRelVarFromName :: [RelVar] -> String -> Maybe RelVar
findRelVarFromName :: [RelVar] -> String -> Maybe RelVar
findRelVarFromName [] _ = Maybe RelVar
forall a. Maybe a
Nothing
findRelVarFromName (v :: RelVar
v : restV :: [RelVar]
restV) nam :: String
nam = if RelVar -> String
QVTRAs.varName RelVar
v String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nam
                                     then RelVar -> Maybe RelVar
forall a. a -> Maybe a
Just RelVar
v
                                     else [RelVar] -> String -> Maybe RelVar
findRelVarFromName [RelVar]
restV String
nam


getVarIdsFromOCLExpre :: [RelVar] -> QVTRAs.OCL -> [RelVar]
getVarIdsFromOCLExpre :: [RelVar] -> OCL -> [RelVar]
getVarIdsFromOCLExpre varS :: [RelVar]
varS (StringExp str :: STRING
str) = [RelVar] -> STRING -> [RelVar]
getVarIdsFromStrExpre [RelVar]
varS STRING
str
getVarIdsFromOCLExpre varS :: [RelVar]
varS (Paren expr :: OCL
expr) = [RelVar] -> OCL -> [RelVar]
getVarIdsFromOCLExpre [RelVar]
varS OCL
expr
getVarIdsFromOCLExpre varS :: [RelVar]
varS (NotB expr :: OCL
expr) = [RelVar] -> OCL -> [RelVar]
getVarIdsFromOCLExpre [RelVar]
varS OCL
expr
getVarIdsFromOCLExpre varS :: [RelVar]
varS (AndB exp1 :: OCL
exp1 exp2 :: OCL
exp2) = [RelVar] -> OCL -> [RelVar]
getVarIdsFromOCLExpre [RelVar]
varS OCL
exp1
 [RelVar] -> [RelVar] -> [RelVar]
forall a. [a] -> [a] -> [a]
++ [RelVar] -> OCL -> [RelVar]
getVarIdsFromOCLExpre [RelVar]
varS OCL
exp2
getVarIdsFromOCLExpre varS :: [RelVar]
varS (OrB exp1 :: OCL
exp1 exp2 :: OCL
exp2) = [RelVar] -> OCL -> [RelVar]
getVarIdsFromOCLExpre [RelVar]
varS OCL
exp1
 [RelVar] -> [RelVar] -> [RelVar]
forall a. [a] -> [a] -> [a]
++ [RelVar] -> OCL -> [RelVar]
getVarIdsFromOCLExpre [RelVar]
varS OCL
exp2
getVarIdsFromOCLExpre varS :: [RelVar]
varS (Equal str1 :: STRING
str1 str2 :: STRING
str2) = [RelVar] -> STRING -> [RelVar]
getVarIdsFromStrExpre [RelVar]
varS STRING
str1
 [RelVar] -> [RelVar] -> [RelVar]
forall a. [a] -> [a] -> [a]
++ [RelVar] -> STRING -> [RelVar]
getVarIdsFromStrExpre [RelVar]
varS STRING
str2
getVarIdsFromOCLExpre _ _ = []


getVarIdsFromStrExpre :: [RelVar] -> QVTRAs.STRING -> [RelVar]
getVarIdsFromStrExpre :: [RelVar] -> STRING -> [RelVar]
getVarIdsFromStrExpre varS :: [RelVar]
varS (ConcatExp str1 :: STRING
str1 str2 :: STRING
str2) =
 [RelVar] -> STRING -> [RelVar]
getVarIdsFromStrExpre [RelVar]
varS STRING
str1 [RelVar] -> [RelVar] -> [RelVar]
forall a. [a] -> [a] -> [a]
++ [RelVar] -> STRING -> [RelVar]
getVarIdsFromStrExpre [RelVar]
varS STRING
str2
getVarIdsFromStrExpre varS :: [RelVar]
varS (VarExp v :: String
v) = case [RelVar] -> String -> Maybe RelVar
findRelVarFromName [RelVar]
varS String
v of
                                          Nothing -> []
                                          Just r :: RelVar
r -> [RelVar
r]
getVarIdsFromStrExpre _ _ = []


{- 1. WhenVarSet = ∅
∀ x1 , ..., xn ∈ (VarSet\2_VarSet)\ParSet,
(Pattern1 → ∃ y1 , ..., ym ∈ 2_VarSet\ParSet, (Pattern2 ∧ where)) -}

buildEmptyWhenFormula :: QVTR.Sign -> [RelVar] -> [RelVar] -> Set.Set RelVar -> Pattern -> Pattern -> Maybe WhenWhere -> CASLFORMULA
buildEmptyWhenFormula :: Sign
-> [RelVar]
-> [RelVar]
-> Set RelVar
-> Pattern
-> Pattern
-> Maybe WhenWhere
-> CASLFORMULA
buildEmptyWhenFormula qvtSign :: Sign
qvtSign parS :: [RelVar]
parS varS :: [RelVar]
varS varSet_2 :: Set RelVar
varSet_2 souPat :: Pattern
souPat tarPat :: Pattern
tarPat whereC :: Maybe WhenWhere
whereC =
  let
    listPars :: Set RelVar
listPars = [RelVar] -> Set RelVar
forall a. Ord a => [a] -> Set a
Set.fromList [RelVar]
parS
    diffVarSet_1 :: [RelVar]
diffVarSet_1 = Set RelVar -> [RelVar]
forall a. Set a -> [a]
Set.toList (Set RelVar -> [RelVar]) -> Set RelVar -> [RelVar]
forall a b. (a -> b) -> a -> b
$ Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference ([RelVar] -> Set RelVar
forall a. Ord a => [a] -> Set a
Set.fromList [RelVar]
varS) Set RelVar
varSet_2) Set RelVar
listPars
    diffVarSet_2 :: [RelVar]
diffVarSet_2 = Set RelVar -> [RelVar]
forall a. Set a -> [a]
Set.toList (Set RelVar -> [RelVar]) -> Set RelVar -> [RelVar]
forall a b. (a -> b) -> a -> b
$ Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set RelVar
varSet_2 Set RelVar
listPars
    souPatF :: CASLFORMULA
souPatF = Sign -> [RelVar] -> Pattern -> CASLFORMULA
buildPatternFormula Sign
qvtSign [RelVar]
varS Pattern
souPat
    tarPatF :: CASLFORMULA
tarPatF = Sign -> [RelVar] -> Pattern -> CASLFORMULA
buildPatternFormula Sign
qvtSign [RelVar]
varS Pattern
tarPat
    whereF :: CASLFORMULA
whereF = Maybe WhenWhere -> [RelVar] -> CASLFORMULA
buildWhenWhereFormula Maybe WhenWhere
whereC [RelVar]
varS

    fst_sen :: CASLFORMULA
fst_sen | CASLFORMULA
whereF CASLFORMULA -> CASLFORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== CASLFORMULA
forall f. FORMULA f
trueForm =
                   if CASLFORMULA
tarPatF CASLFORMULA -> CASLFORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== CASLFORMULA
forall f. FORMULA f
trueForm
                   then if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_2
                        then CASLFORMULA
forall f. FORMULA f
trueForm
                        else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Existential
                                              ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_2)
                                              CASLFORMULA
forall f. FORMULA f
trueForm
                                              Range
nullRange
                   else if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_2
                        then CASLFORMULA
tarPatF
                        else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Existential
                                              ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_2)
                                              CASLFORMULA
tarPatF
                                              Range
nullRange
            | CASLFORMULA
tarPatF CASLFORMULA -> CASLFORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== CASLFORMULA
forall f. FORMULA f
trueForm =
                        if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_2
                        then CASLFORMULA
whereF
                        else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Existential
                                              ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_2)
                                              CASLFORMULA
whereF
                                              Range
nullRange
            | [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_2 = Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con [CASLFORMULA
tarPatF, CASLFORMULA
whereF] Range
nullRange
            | Bool
otherwise = QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Existential
                                    ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_2)
                                    (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con [CASLFORMULA
tarPatF, CASLFORMULA
whereF] Range
nullRange)
                                    Range
nullRange
  in
    if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_1
    then CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
C.Relation CASLFORMULA
souPatF Relation
Implication CASLFORMULA
fst_sen Range
nullRange
    else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Universal
                          ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_1)
                          (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
C.Relation CASLFORMULA
souPatF
                                      Relation
Implication
                                      CASLFORMULA
fst_sen
                                      Range
nullRange)
                          Range
nullRange


varDeclFromRelVar :: [RelVar] -> [VAR_DECL]
varDeclFromRelVar :: [RelVar] -> [VAR_DECL]
varDeclFromRelVar = (RelVar -> VAR_DECL) -> [RelVar] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: RelVar
v -> [SIMPLE_ID] -> Id -> Range -> VAR_DECL
Var_decl [String -> SIMPLE_ID
mkSimpleId (String -> SIMPLE_ID) -> String -> SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ RelVar -> String
varName RelVar
v]
                                 (String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ RelVar -> String
varType RelVar
v) Range
nullRange)

{- 2. WhenVarSet <> ∅
∀ z1 , ..., zo ∈ WhenVarSet\ParSet, (when →
∀ x1 , ..., xn ∈ (VarSet\(WhenVarSet ∪ 2_VarSet))\ParSet, (Pattern1 →
∃ y1 , ..., ym ∈ 2_VarSet\ParSet, (Pattern2 ∧ where))) -}

buildNonEmptyWhenFormula :: QVTR.Sign -> [RelVar] -> [RelVar] -> [RelVar] -> Set.Set RelVar
                                      -> Pattern -> Pattern -> Maybe WhenWhere -> Maybe WhenWhere -> CASLFORMULA
buildNonEmptyWhenFormula :: Sign
-> [RelVar]
-> [RelVar]
-> [RelVar]
-> Set RelVar
-> Pattern
-> Pattern
-> Maybe WhenWhere
-> Maybe WhenWhere
-> CASLFORMULA
buildNonEmptyWhenFormula qvtSign :: Sign
qvtSign whenVarSet :: [RelVar]
whenVarSet parS :: [RelVar]
parS varS :: [RelVar]
varS varSet_2 :: Set RelVar
varSet_2 souPat :: Pattern
souPat tarPat :: Pattern
tarPat whenC :: Maybe WhenWhere
whenC whereC :: Maybe WhenWhere
whereC =
  let
    listWhenVars :: Set RelVar
listWhenVars = [RelVar] -> Set RelVar
forall a. Ord a => [a] -> Set a
Set.fromList [RelVar]
whenVarSet
    listPars :: Set RelVar
listPars = [RelVar] -> Set RelVar
forall a. Ord a => [a] -> Set a
Set.fromList [RelVar]
parS
    diffVarSet_1 :: [RelVar]
diffVarSet_1 = Set RelVar -> [RelVar]
forall a. Set a -> [a]
Set.toList (Set RelVar -> [RelVar]) -> Set RelVar -> [RelVar]
forall a b. (a -> b) -> a -> b
$ Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set RelVar
listWhenVars Set RelVar
listPars
    diffVarSet_2 :: [RelVar]
diffVarSet_2 = Set RelVar -> [RelVar]
forall a. Set a -> [a]
Set.toList (Set RelVar -> [RelVar]) -> Set RelVar -> [RelVar]
forall a b. (a -> b) -> a -> b
$ Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference ([RelVar] -> Set RelVar
forall a. Ord a => [a] -> Set a
Set.fromList [RelVar]
varS) (Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set RelVar
listWhenVars Set RelVar
varSet_2)) Set RelVar
listPars
    diffVarSet_3 :: [RelVar]
diffVarSet_3 = Set RelVar -> [RelVar]
forall a. Set a -> [a]
Set.toList (Set RelVar -> [RelVar]) -> Set RelVar -> [RelVar]
forall a b. (a -> b) -> a -> b
$ Set RelVar -> Set RelVar -> Set RelVar
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set RelVar
varSet_2 Set RelVar
listPars
    souPatF :: CASLFORMULA
souPatF = Sign -> [RelVar] -> Pattern -> CASLFORMULA
buildPatternFormula Sign
qvtSign [RelVar]
varS Pattern
souPat
    tarPatF :: CASLFORMULA
tarPatF = Sign -> [RelVar] -> Pattern -> CASLFORMULA
buildPatternFormula Sign
qvtSign [RelVar]
varS Pattern
tarPat
    whenF :: CASLFORMULA
whenF = Maybe WhenWhere -> [RelVar] -> CASLFORMULA
buildWhenWhereFormula Maybe WhenWhere
whenC [RelVar]
varS
    whereF :: CASLFORMULA
whereF = Maybe WhenWhere -> [RelVar] -> CASLFORMULA
buildWhenWhereFormula Maybe WhenWhere
whereC [RelVar]
varS

    snd_sen :: CASLFORMULA
snd_sen | CASLFORMULA
whereF CASLFORMULA -> CASLFORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== CASLFORMULA
forall f. FORMULA f
trueForm =
                   if CASLFORMULA
tarPatF CASLFORMULA -> CASLFORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== CASLFORMULA
forall f. FORMULA f
trueForm
                   then if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_3
                        then CASLFORMULA
forall f. FORMULA f
trueForm
                        else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Existential
                                              ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_3)
                                              CASLFORMULA
forall f. FORMULA f
trueForm
                                              Range
nullRange
                   else if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_3
                        then CASLFORMULA
tarPatF
                        else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Existential
                                              ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_3)
                                              CASLFORMULA
tarPatF
                                              Range
nullRange
            | CASLFORMULA
tarPatF CASLFORMULA -> CASLFORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== CASLFORMULA
forall f. FORMULA f
trueForm =
                        if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_3
                        then CASLFORMULA
whereF
                        else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Existential
                                              ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_3)
                                              CASLFORMULA
whereF
                                              Range
nullRange
            | [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_3 = Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con [CASLFORMULA
tarPatF, CASLFORMULA
whereF] Range
nullRange
            | Bool
otherwise = QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Existential
                                    ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_3)
                                    (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con [CASLFORMULA
tarPatF, CASLFORMULA
whereF] Range
nullRange)
                                    Range
nullRange

    fst_sen :: CASLFORMULA
fst_sen | CASLFORMULA
souPatF CASLFORMULA -> CASLFORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== CASLFORMULA
forall f. FORMULA f
trueForm =
                   if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_2
                   then CASLFORMULA
snd_sen
                   else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Universal
                                         ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_2)
                                         CASLFORMULA
snd_sen
                                         Range
nullRange
            | [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_2 = CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
C.Relation CASLFORMULA
souPatF Relation
Implication CASLFORMULA
snd_sen Range
nullRange
            | Bool
otherwise = QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Universal
                                    ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_2)
                                    (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
C.Relation CASLFORMULA
souPatF
                                                Relation
Implication
                                                CASLFORMULA
snd_sen
                                                Range
nullRange) Range
nullRange
  in
    if [RelVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RelVar]
diffVarSet_1
    then CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
C.Relation CASLFORMULA
whenF Relation
Implication CASLFORMULA
fst_sen Range
nullRange
    else QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
C.Quantification QUANTIFIER
Universal
                          ([RelVar] -> [VAR_DECL]
varDeclFromRelVar [RelVar]
diffVarSet_1)
                          (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
C.Relation CASLFORMULA
whenF
                                      Relation
Implication
                                      CASLFORMULA
fst_sen
                                      Range
nullRange)
                          Range
nullRange


{- The translation of Pattern = ⟨E, A, Pr⟩ is the formula r2 (x, y) ∧ Pr such
that r2 (x, y) is the translation of predicate p = ⟨r1 : C, r2 : D⟩ for every rel(p, x, y) ∈ A with x : C, y : D. -}

buildPatternFormula :: QVTR.Sign -> [RelVar] -> Pattern -> CASLFORMULA
buildPatternFormula :: Sign -> [RelVar] -> Pattern -> CASLFORMULA
buildPatternFormula qvtSign :: Sign
qvtSign varS :: [RelVar]
varS (Pattern _ parRel :: [(PropertyT, RelVar, RelVar)]
parRel patPred :: [(String, String, OCL)]
patPred) =
  let
    relInvF :: [CASLFORMULA]
relInvF = ((PropertyT, RelVar, RelVar) -> CASLFORMULA)
-> [(PropertyT, RelVar, RelVar)] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (PropertyT, RelVar, RelVar) -> CASLFORMULA
buildPatRelFormula [(PropertyT, RelVar, RelVar)]
parRel
    oclExpF :: [CASLFORMULA]
oclExpF = ((String, String, OCL) -> CASLFORMULA)
-> [(String, String, OCL)] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> [RelVar] -> (String, String, OCL) -> CASLFORMULA
buildOCLFormulaWRel Sign
qvtSign [RelVar]
varS) [(String, String, OCL)]
patPred
  in
    if [CASLFORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CASLFORMULA]
oclExpF
    then if [CASLFORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CASLFORMULA]
relInvF
         then CASLFORMULA
forall f. FORMULA f
trueForm
         else Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con [CASLFORMULA]
relInvF Range
nullRange
    else if [CASLFORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CASLFORMULA]
relInvF
         then Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con [CASLFORMULA]
oclExpF Range
nullRange
         else Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con ([CASLFORMULA]
relInvF [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
oclExpF) Range
nullRange


buildPatRelFormula :: (CSMOF.PropertyT, RelVar, RelVar) -> CASLFORMULA
buildPatRelFormula :: (PropertyT, RelVar, RelVar) -> CASLFORMULA
buildPatRelFormula (p :: PropertyT
p, souV :: RelVar
souV, tarV :: RelVar
tarV) =
  let
    rName :: String
rName = PropertyT -> String
CSMOF.targetRole PropertyT
p
    predTyp :: [Id]
predTyp = [String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
CSMOF.name (TypeClass -> String) -> TypeClass -> String
forall a b. (a -> b) -> a -> b
$ PropertyT -> TypeClass
CSMOF.sourceType PropertyT
p, String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$
               TypeClass -> String
CSMOF.name (TypeClass -> String) -> TypeClass -> String
forall a b. (a -> b) -> a -> b
$ PropertyT -> TypeClass
CSMOF.targetType PropertyT
p]
    varsInv :: [TERM ()]
varsInv = [RelVar] -> [TERM ()]
createVarRule [RelVar
souV, RelVar
tarV]
  in
    PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name (String -> Id
stringToId String
rName) ([Id] -> Range -> PRED_TYPE
Pred_type [Id]
predTyp Range
nullRange) Range
nullRange)
                [TERM ()]
varsInv
                Range
nullRange


{- The translation of when = ⟨whenc , whenr⟩ is the formula Rule(v) ∧ whenc such that
Rule(v) is the translation of (Rulew , v) ∈ whenr. The translation of where is defined in a similar way. -}

buildWhenWhereFormula :: Maybe WhenWhere -> [RelVar] -> CASLFORMULA
buildWhenWhereFormula :: Maybe WhenWhere -> [RelVar] -> CASLFORMULA
buildWhenWhereFormula Nothing _ = CASLFORMULA
forall f. FORMULA f
trueForm -- ERROR, this cannot happens
buildWhenWhereFormula (Just (WhenWhere relInv :: [RelInvok]
relInv oclExp :: [OCL]
oclExp)) varS :: [RelVar]
varS =
  let
    relInvF :: [CASLFORMULA]
relInvF = (RelInvok -> CASLFORMULA) -> [RelInvok] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([RelVar] -> RelInvok -> CASLFORMULA
buildRelInvocFormula [RelVar]
varS) [RelInvok]
relInv
    oclExpF :: [CASLFORMULA]
oclExpF = (OCL -> CASLFORMULA) -> [OCL] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([RelVar] -> OCL -> CASLFORMULA
buildOCLFormula [RelVar]
varS) [OCL]
oclExp
  in
    if [CASLFORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CASLFORMULA]
oclExpF
    then if [CASLFORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CASLFORMULA]
relInvF
         then CASLFORMULA
forall f. FORMULA f
trueForm
         else Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con [CASLFORMULA]
relInvF Range
nullRange
    else if [CASLFORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CASLFORMULA]
relInvF
         then Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con [CASLFORMULA]
oclExpF Range
nullRange
         else Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con ([CASLFORMULA]
relInvF [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
oclExpF) Range
nullRange


buildRelInvocFormula :: [RelVar] -> RelInvok -> CASLFORMULA
buildRelInvocFormula :: [RelVar] -> RelInvok -> CASLFORMULA
buildRelInvocFormula varS :: [RelVar]
varS rel :: RelInvok
rel =
  let
    vars :: [RelVar]
vars = [Maybe RelVar] -> [RelVar]
forall a. [Maybe a] -> [a]
QVTRAn.getSomething ([Maybe RelVar] -> [RelVar]) -> [Maybe RelVar] -> [RelVar]
forall a b. (a -> b) -> a -> b
$ (String -> Maybe RelVar) -> [String] -> [Maybe RelVar]
forall a b. (a -> b) -> [a] -> [b]
map ([RelVar] -> String -> Maybe RelVar
findRelVarFromName [RelVar]
varS) (RelInvok -> [String]
QVTRAs.params RelInvok
rel)
    varsInv :: [TERM ()]
varsInv = [RelVar] -> [TERM ()]
createVarRule [RelVar]
vars
    predTyp :: [Id]
predTyp = (RelVar -> Id) -> [RelVar] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Id
stringToId (String -> Id) -> (RelVar -> String) -> RelVar -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelVar -> String
varType) [RelVar]
vars
  in
    PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
C.Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name (String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ RelInvok -> String
QVTRAs.name RelInvok
rel)
      ([Id] -> Range -> PRED_TYPE
Pred_type [Id]
predTyp Range
nullRange) Range
nullRange) [TERM ()]
varsInv Range
nullRange


buildOCLFormulaWRel :: QVTR.Sign -> [RelVar] -> (String, String, OCL) -> CASLFORMULA
buildOCLFormulaWRel :: Sign -> [RelVar] -> (String, String, OCL) -> CASLFORMULA
buildOCLFormulaWRel qvtSign :: Sign
qvtSign varS :: [RelVar]
varS (prN :: String
prN, varN :: String
varN, StringExp str :: STRING
str) =
  let oclT :: TERM ()
oclT = STRING -> [RelVar] -> TERM ()
buildSTRINGTerm STRING
str [RelVar]
varS
      typ :: String
typ = case [RelVar] -> String -> Maybe RelVar
findRelVarFromName [RelVar]
varS String
varN of
              Nothing -> ""
              Just v :: RelVar
v -> RelVar -> String
varType RelVar
v

      (_, p :: Maybe PropertyT
p) = Sign -> String -> String -> (Id, Maybe PropertyT)
getSortOfProperty Sign
qvtSign String
typ String
prN
      (sor :: Id
sor, sor2 :: Id
sor2) = case Maybe PropertyT
p of
                     Nothing -> (String -> Id
stringToId "", String -> Id
stringToId "")
                     Just pp :: PropertyT
pp -> if PropertyT -> String
CSMOF.targetRole PropertyT
pp String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
prN
                      then (String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
CSMOF.name (TypeClass -> String) -> TypeClass -> String
forall a b. (a -> b) -> a -> b
$ PropertyT -> TypeClass
CSMOF.sourceType PropertyT
pp,
                            String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
CSMOF.name (TypeClass -> String) -> TypeClass -> String
forall a b. (a -> b) -> a -> b
$ PropertyT -> TypeClass
CSMOF.targetType PropertyT
pp)
                      else (String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
CSMOF.name (TypeClass -> String) -> TypeClass -> String
forall a b. (a -> b) -> a -> b
$ PropertyT -> TypeClass
CSMOF.targetType PropertyT
pp,
                            String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ TypeClass -> String
CSMOF.name (TypeClass -> String) -> TypeClass -> String
forall a b. (a -> b) -> a -> b
$ PropertyT -> TypeClass
CSMOF.sourceType PropertyT
pp)
  in
    PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
C.Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
C.Qual_pred_name (String -> Id
stringToId String
prN) ([Id] -> Range -> PRED_TYPE
Pred_type [Id
sor, Id
sor2]
      Range
nullRange) Range
nullRange)
     (SIMPLE_ID -> Id -> Range -> TERM ()
forall f. SIMPLE_ID -> Id -> Range -> TERM f
Qual_var (String -> SIMPLE_ID
mkSimpleId String
varN) (String -> Id
stringToId String
typ) Range
nullRange TERM () -> [TERM ()] -> [TERM ()]
forall a. a -> [a] -> [a]
: [TERM ()
oclT]) Range
nullRange
buildOCLFormulaWRel _ _ _ = CASLFORMULA
forall f. FORMULA f
trueForm


buildOCLFormula :: [RelVar] -> OCL -> CASLFORMULA
buildOCLFormula :: [RelVar] -> OCL -> CASLFORMULA
buildOCLFormula varS :: [RelVar]
varS (Paren e :: OCL
e) = [RelVar] -> OCL -> CASLFORMULA
buildOCLFormula [RelVar]
varS OCL
e
buildOCLFormula _ (BExp b :: Bool
b) = if Bool
b then CASLFORMULA
forall f. FORMULA f
trueForm else CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
C.Negation CASLFORMULA
forall f. FORMULA f
trueForm Range
nullRange
buildOCLFormula varS :: [RelVar]
varS (NotB e :: OCL
e) = CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
C.Negation ([RelVar] -> OCL -> CASLFORMULA
buildOCLFormula [RelVar]
varS OCL
e) Range
nullRange
buildOCLFormula varS :: [RelVar]
varS (AndB lE :: OCL
lE rE :: OCL
rE) = Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Con [[RelVar] -> OCL -> CASLFORMULA
buildOCLFormula [RelVar]
varS OCL
lE,
                                     [RelVar] -> OCL -> CASLFORMULA
buildOCLFormula [RelVar]
varS OCL
rE] Range
nullRange
buildOCLFormula varS :: [RelVar]
varS (OrB lE :: OCL
lE rE :: OCL
rE) = Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
C.Junction Junctor
Dis [[RelVar] -> OCL -> CASLFORMULA
buildOCLFormula [RelVar]
varS OCL
lE,
                                     [RelVar] -> OCL -> CASLFORMULA
buildOCLFormula [RelVar]
varS OCL
rE] Range
nullRange
buildOCLFormula varS :: [RelVar]
varS (Equal lE :: STRING
lE rE :: STRING
rE) = TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
C.Equation (STRING -> [RelVar] -> TERM ()
buildSTRINGTerm STRING
lE [RelVar]
varS)
                                      Equality
Strong (STRING -> [RelVar] -> TERM ()
buildSTRINGTerm STRING
rE [RelVar]
varS) Range
nullRange
buildOCLFormula _ (StringExp _) = CASLFORMULA
forall f. FORMULA f
trueForm -- This is not a formula, but a term used within an equality


buildSTRINGTerm :: STRING -> [RelVar] -> CASLTERM
buildSTRINGTerm :: STRING -> [RelVar] -> TERM ()
buildSTRINGTerm (Str str :: String
str) _ = OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
C.Application (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (String -> Id
stringToId String
str)
  (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Total [] (String -> Id
stringToId "String") Range
nullRange) Range
nullRange) [] Range
nullRange
buildSTRINGTerm (ConcatExp lS :: STRING
lS rS :: STRING
rS) varS :: [RelVar]
varS =
  let
    lSTerm :: TERM ()
lSTerm = STRING -> [RelVar] -> TERM ()
buildSTRINGTerm STRING
lS [RelVar]
varS
    rSTerm :: TERM ()
rSTerm = STRING -> [RelVar] -> TERM ()
buildSTRINGTerm STRING
rS [RelVar]
varS
    stringSort :: Id
stringSort = String -> Id
stringToId "String"
  in
    OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
C.Application (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (String -> Id
stringToId "++")
                                (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Total [Id
stringSort, Id
stringSort] Id
stringSort Range
nullRange)
                                Range
nullRange)
                  [TERM ()
lSTerm, TERM ()
rSTerm]
                  Range
nullRange
buildSTRINGTerm (VarExp vE :: String
vE) varS :: [RelVar]
varS =
  let
    var :: Id
var = case [RelVar] -> String -> Maybe RelVar
findRelVarFromName [RelVar]
varS String
vE of
            Nothing -> String -> Id
stringToId ""
            Just v :: RelVar
v -> String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ RelVar -> String
varType RelVar
v
  in
    SIMPLE_ID -> Id -> Range -> TERM ()
forall f. SIMPLE_ID -> Id -> Range -> TERM f
Qual_var (String -> SIMPLE_ID
mkSimpleId String
vE) Id
var Range
nullRange


{- getSTRINGType :: STRING -> [RelVar] -> SORT
getSTRINGType (VarExp vE) varS =
case findRelVarFromName varS vE of
Nothing -> stringToId ""
Just v -> stringToId $ varType v
getSTRINGType _ _ = stringToId "" -}


-- | Translation of morphisms
mapMor :: QVTR.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 :: QVTR.Symbol -> C.Symbol


{- 1) Adds the String primitive type within a CASL Signature
2) Generates the strings concatenation operation ++ -}

addStringSignature :: CASLSign -> CASLSign
addStringSignature :: CASLSign -> CASLSign
addStringSignature s :: CASLSign
s =
  let
    stringSort :: Id
stringSort = String -> Id
stringToId "String"
    (strObj :: [Named CASLFORMULA]
strObj, othObj :: [Named CASLFORMULA]
othObj) = [Named CASLFORMULA] -> ([Named CASLFORMULA], [Named CASLFORMULA])
separateStringConstraintFromOthers ([Named CASLFORMULA] -> ([Named CASLFORMULA], [Named CASLFORMULA]))
-> [Named CASLFORMULA]
-> ([Named CASLFORMULA], [Named CASLFORMULA])
forall a b. (a -> b) -> a -> b
$ CASLSign -> [Named CASLFORMULA]
forall f e. Sign f e -> [Named (FORMULA f)]
sentences CASLSign
s
{- strObjTr = getStringObjFromTransformation ns
strObjOps = foldr (\(idd,opT) se -> MapSet.insert idd opT se) MapSet.empty (getStringOperations strObjTr) -}
    everyString :: [Id]
everyString = Set Id -> [Id]
forall a. Set a -> [a]
Set.toList ([Named CASLFORMULA] -> Set Id
getStringObjects [Named CASLFORMULA]
strObj) -- Set.toList (Set.union strObjTr (getStringObjects strObj))
    concatOp :: OpType
concatOp = [Id] -> Id -> OpType
mkTotOpType [Id
stringSort, Id
stringSort] Id
stringSort
  in
    Sign :: forall f e.
Rel Id
-> Maybe (Rel Id)
-> Set Id
-> OpMap
-> OpMap
-> PredMap
-> Map SIMPLE_ID Id
-> [Named (FORMULA f)]
-> Set Symbol
-> [Diagnosis]
-> AnnoMap
-> GlobalAnnos
-> e
-> Sign f e
C.Sign { sortRel :: Rel Id
sortRel = Id -> Id -> Rel Id -> Rel Id
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair Id
stringSort Id
stringSort (CASLSign -> Rel Id
forall f e. Sign f e -> Rel Id
C.sortRel CASLSign
s)
           , revSortRel :: Maybe (Rel Id)
revSortRel = CASLSign -> Maybe (Rel Id)
forall f e. Sign f e -> Maybe (Rel Id)
C.revSortRel CASLSign
s
           , emptySortSet :: Set Id
emptySortSet = CASLSign -> Set Id
forall f e. Sign f e -> Set Id
C.emptySortSet CASLSign
s
           , opMap :: OpMap
opMap = Id -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (String -> Id
stringToId "++") OpType
concatOp (CASLSign -> OpMap
forall f e. Sign f e -> OpMap
C.opMap CASLSign
s) -- MapSet.union strObjOps (C.opMap s)
           , assocOps :: OpMap
assocOps = CASLSign -> OpMap
forall f e. Sign f e -> OpMap
C.assocOps CASLSign
s
           , predMap :: PredMap
predMap = CASLSign -> PredMap
forall f e. Sign f e -> PredMap
C.predMap CASLSign
s
           , varMap :: Map SIMPLE_ID Id
varMap = CASLSign -> Map SIMPLE_ID Id
forall f e. Sign f e -> Map SIMPLE_ID Id
C.varMap CASLSign
s
           , sentences :: [Named CASLFORMULA]
sentences = [Id] -> Named CASLFORMULA
getNoConfusionStrings [Id]
everyString Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. a -> [a] -> [a]
:
                           ((Id, [Id]) -> Named CASLFORMULA
toStringConstraint (Id
stringSort, [Id]
everyString) Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. a -> [a] -> [a]
:
                             [Named CASLFORMULA] -> [Named CASLFORMULA]
deleteNoConfusionString [Named CASLFORMULA]
othObj)
           , declaredSymbols :: Set Symbol
declaredSymbols = CASLSign -> Set Symbol
forall f e. Sign f e -> Set Symbol
C.declaredSymbols CASLSign
s
           , envDiags :: [Diagnosis]
envDiags = CASLSign -> [Diagnosis]
forall f e. Sign f e -> [Diagnosis]
C.envDiags CASLSign
s
           , annoMap :: AnnoMap
annoMap = CASLSign -> AnnoMap
forall f e. Sign f e -> AnnoMap
C.annoMap CASLSign
s
           , globAnnos :: GlobalAnnos
globAnnos = CASLSign -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
C.globAnnos CASLSign
s
           , extendedInfo :: ()
extendedInfo = CASLSign -> ()
forall f e. Sign f e -> e
C.extendedInfo CASLSign
s
           }


{- splitStringByUnderscore :: String -> [String]
splitStringByUnderscore [] = []
splitStringByUnderscore str =
let
strAux = getUntilUnderscore str
rest = splitStringByUnderscore (drop (length strAux + 1) str)
in
strAux : rest -}


{- getUntilUnderscore :: String -> String
getUntilUnderscore [] = []
getUntilUnderscore (s : restS) = if s == '_'
then []
else s : getUntilUnderscore restS -}


{- getStringOperations :: Set.Set Id -> [(Id,OpType)]
getStringOperations ids = Set.fold (\idd lis -> (idd, (mkTotOpType [] (stringToId "String"))) : lis ) [] ids -}


deleteNoConfusionString :: [Named CASLFORMULA] -> [Named CASLFORMULA]
deleteNoConfusionString :: [Named CASLFORMULA] -> [Named CASLFORMULA]
deleteNoConfusionString [] = []
deleteNoConfusionString (nf :: Named CASLFORMULA
nf : restNF :: [Named CASLFORMULA]
restNF) =
  let rest :: [Named CASLFORMULA]
rest = [Named CASLFORMULA] -> [Named CASLFORMULA]
deleteNoConfusionString [Named CASLFORMULA]
restNF
  in if String -> String -> Bool
startswith (Named CASLFORMULA -> String
forall s a. SenAttr s a -> a
senAttr Named CASLFORMULA
nf) "noConfusion_String"
     then [Named CASLFORMULA]
rest
     else Named CASLFORMULA
nf Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. a -> [a] -> [a]
: [Named CASLFORMULA]
rest


startswith :: String -> String -> Bool
startswith :: String -> String -> Bool
startswith [] [] = Bool
True
startswith (a :: Char
a : restA :: String
restA) (b :: Char
b : restB :: String
restB) = Char
a Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
b Bool -> Bool -> Bool
&& String -> String -> Bool
startswith String
restA String
restB
startswith _ _ = Bool
False


getNoConfusionStrings :: [Id] -> Named CASLFORMULA
getNoConfusionStrings :: [Id] -> Named CASLFORMULA
getNoConfusionStrings ordObj :: [Id]
ordObj =
  let diffForm :: [CASLFORMULA]
diffForm = (Id -> [CASLFORMULA] -> [CASLFORMULA])
-> [CASLFORMULA] -> [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])
-> (Id -> [CASLFORMULA]) -> Id -> [CASLFORMULA] -> [CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Id] -> Id -> [CASLFORMULA]
diffOfRestStringOps [Id]
ordObj) [] [Id]
ordObj
  in String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "noConfusion_String" (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [CASLFORMULA]
diffForm Range
nullRange)


diffOfRestStringOps :: [Id] -> Id -> [CASLFORMULA]
diffOfRestStringOps :: [Id] -> Id -> [CASLFORMULA]
diffOfRestStringOps lisObj :: [Id]
lisObj objName :: Id
objName =
  let lis :: [Id]
lis = [Id] -> Id -> [Id]
removeUntilId [Id]
lisObj Id
objName
  in (Id -> [CASLFORMULA]) -> [Id] -> [CASLFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Id -> Id -> [CASLFORMULA]
diffOpsStr Id
objName) [Id]
lis


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


diffOpsStr :: Id -> Id -> [CASLFORMULA]
diffOpsStr :: Id -> Id -> [CASLFORMULA]
diffOpsStr objName1 :: Id
objName1 objName2 :: Id
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 (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
objName1
                        (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Total [] (String -> Id
stringToId "String") Range
nullRange)
                        Range
nullRange) [] Range
nullRange)
                 Equality
Strong
                 (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
objName2
                        (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Total [] (String -> Id
stringToId "String") Range
nullRange)
                        Range
nullRange) [] Range
nullRange)
                 Range
nullRange)
       Range
nullRange | Id
objName1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
/= Id
objName2]

{- Get String instances within transformation rules
getStringObjFromTransformation :: [Named QVTR.Sen] -> Set.Set Id
getStringObjFromTransformation [] = Set.empty
getStringObjFromTransformation (ns : restNS) =
let
restId = getStringObjFromTransformation restNS
idSen = case sentence ns of
QVTSen rel -> getStringIdsFromRelation rel
_ -> Set.empty
in
Set.union idSen restId -}


{- getStringIdsFromRelation :: RelationSen -> Set.Set Id
getStringIdsFromRelation (RelationSen _ _ _ souP tarP whenCl whereCl) =
let
souPId = getStringIdsFromPattern souP
tarPId = getStringIdsFromPattern tarP
whenId = getStringIdsFromWhenWhere whenCl
whereId = getStringIdsFromWhenWhere whereCl
in
Set.unions [souPId,tarPId,whenId,whereId] -}


{- getStringIdsFromPattern :: Pattern -> Set.Set Id
getStringIdsFromPattern (Pattern _ _ p) = getStringIdsFromOclPred p -}


{- getStringIdsFromOclPred :: [(String,String,OCL)] -> Set.Set Id
getStringIdsFromOclPred [] = Set.empty
getStringIdsFromOclPred ((_,_,ocl) : restPr) = Set.union (getStringIdsFromOCL ocl) (getStringIdsFromOclPred restPr) -}


{- getStringIdsFromWhenWhere :: Maybe WhenWhere -> Set.Set Id
getStringIdsFromWhenWhere Nothing = Set.empty
getStringIdsFromWhenWhere (Just (WhenWhere _ ocl)) = Set.unions (map (getStringIdsFromOCL) ocl) -}


{- getStringIdsFromOCL :: OCL -> Set.Set Id
getStringIdsFromOCL (Paren e) = getStringIdsFromOCL e
getStringIdsFromOCL (StringExp str) = getStringIdsFromString str
getStringIdsFromOCL (BExp _) = Set.empty
getStringIdsFromOCL (NotB no) = getStringIdsFromOCL no
getStringIdsFromOCL (AndB lE rE) = Set.union (getStringIdsFromOCL lE) (getStringIdsFromOCL rE)
getStringIdsFromOCL (OrB lE rE) = Set.union (getStringIdsFromOCL lE) (getStringIdsFromOCL rE)
getStringIdsFromOCL (Equal lE rE) = Set.union (getStringIdsFromString lE) (getStringIdsFromString rE) -}


{- getStringIdsFromString :: STRING -> Set.Set Id
getStringIdsFromString (Str s) = if s == ""
then Set.insert (stringToId "EMPTY") Set.empty
else Set.insert (stringToId s) Set.empty
getStringIdsFromString (ConcatExp lS rS) = Set.union (getStringIdsFromString lS) (getStringIdsFromString rS)
getStringIdsFromString (VarExp _) = Set.empty -}


-- Separate string free type contraints (derived from each metamodel) from the others
separateStringConstraintFromOthers :: [Named CASLFORMULA] -> ([Named CASLFORMULA],
                                      [Named CASLFORMULA])
separateStringConstraintFromOthers :: [Named CASLFORMULA] -> ([Named CASLFORMULA], [Named CASLFORMULA])
separateStringConstraintFromOthers [] = ([], [])
separateStringConstraintFromOthers (f :: Named CASLFORMULA
f : restF :: [Named CASLFORMULA]
restF) =
  let (restString :: [Named CASLFORMULA]
restString, restOther :: [Named CASLFORMULA]
restOther) = [Named CASLFORMULA] -> ([Named CASLFORMULA], [Named CASLFORMULA])
separateStringConstraintFromOthers [Named CASLFORMULA]
restF
  in case Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence Named CASLFORMULA
f of
       Sort_gen_ax [Constraint sor :: Id
sor _ _] _ -> if Id
sor Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Id
stringToId "String"
                                             then (Named CASLFORMULA
f Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. a -> [a] -> [a]
: [Named CASLFORMULA]
restString, [Named CASLFORMULA]
restOther)
                                             else ([Named CASLFORMULA]
restString, Named CASLFORMULA
f Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. a -> [a] -> [a]
: [Named CASLFORMULA]
restOther)
       _ -> ([Named CASLFORMULA]
restString, Named CASLFORMULA
f Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. a -> [a] -> [a]
: [Named CASLFORMULA]
restOther)


-- Get String names from Qual_op_name
getStringObjects :: [Named CASLFORMULA] -> Set.Set Id
getStringObjects :: [Named CASLFORMULA] -> Set Id
getStringObjects [] = Set Id
forall a. Set a
Set.empty
getStringObjects (f :: Named CASLFORMULA
f : restF :: [Named CASLFORMULA]
restF) =
  case Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence Named CASLFORMULA
f of
    Sort_gen_ax [Constraint _ listObj :: [(OP_SYMB, [Int])]
listObj _] _ -> Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union
     ([(OP_SYMB, [Int])] -> Set Id
getObjNamesFromOp [(OP_SYMB, [Int])]
listObj) ([Named CASLFORMULA] -> Set Id
getStringObjects [Named CASLFORMULA]
restF)
    _ -> [Named CASLFORMULA] -> Set Id
getStringObjects [Named CASLFORMULA]
restF


getObjNamesFromOp :: [(OP_SYMB, [Int])] -> Set.Set Id
getObjNamesFromOp :: [(OP_SYMB, [Int])] -> Set Id
getObjNamesFromOp [] = Set Id
forall a. Set a
Set.empty
getObjNamesFromOp ((op :: OP_SYMB
op, _) : restOp :: [(OP_SYMB, [Int])]
restOp) =
  case OP_SYMB
op of
    Qual_op_name obj :: Id
obj _ _ -> Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
obj ([(OP_SYMB, [Int])] -> Set Id
getObjNamesFromOp [(OP_SYMB, [Int])]
restOp)
    _ -> [(OP_SYMB, [Int])] -> Set Id
getObjNamesFromOp [(OP_SYMB, [Int])]
restOp


{- Generate free type
String ::= EMPTY | ... (string instances) ...
__ ++ __ (first: String; rest: String) -}

toStringConstraint :: (Id, [Id]) -> Named CASLFORMULA
toStringConstraint :: (Id, [Id]) -> Named CASLFORMULA
toStringConstraint (sor :: Id
sor, lisObj :: [Id]
lisObj) =
  let
    stringSort :: Id
stringSort = String -> Id
stringToId "String"
    concatOp :: (OP_SYMB, [a])
concatOp = (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (String -> Id
stringToId "++") (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Total
      [Id
stringSort, Id
stringSort] Id
stringSort Range
nullRange) Range
nullRange, [])
    simplCon :: Constraint
simplCon = Id -> [(OP_SYMB, [Int])] -> Id -> Constraint
Constraint Id
sor ((OP_SYMB, [Int])
forall a. (OP_SYMB, [a])
concatOp (OP_SYMB, [Int]) -> [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])]
forall a. a -> [a] -> [a]
: (Id -> [(OP_SYMB, [Int])] -> [(OP_SYMB, [Int])])
-> [(OP_SYMB, [Int])] -> [Id] -> [(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])])
-> (Id -> (OP_SYMB, [Int]))
-> Id
-> [(OP_SYMB, [Int])]
-> [(OP_SYMB, [Int])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Id -> (OP_SYMB, [Int])
toConstraintFromId Id
sor)
      [] [Id]
lisObj) Id
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" CASLFORMULA
forall f. FORMULA f
constr

toConstraintFromId :: Id -> Id -> (OP_SYMB, [Int])
toConstraintFromId :: Id -> Id -> (OP_SYMB, [Int])
toConstraintFromId sor :: Id
sor obj :: Id
obj = (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
obj (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
Total [] Id
sor Range
nullRange)
  Range
nullRange, [])