{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : $Header$

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 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

sourceSublogic QVTR2CASL = ()

targetLogic QVTR2CASL = CASL

mapSublogic QVTR2CASL _ = Just $ caslTop

{ has_part = False

, sub_features = LocFilSub

, cons_features = SortGen True True }

map_theory QVTR2CASL = mapTheory

map_sentence QVTR2CASL s = return . mapSen s (mapSign s)

map_morphism QVTR2CASL = mapMor

-- map_symbol QVTR2CASL _ = Set.singleton . mapSym

is_model_transportable QVTR2CASL = True

has_model_expansion QVTR2CASL = True

is_weakly_amalgamable QVTR2CASL = True

isInclusionComorphism QVTR2CASL = True

mapTheory :: (QVTR.Sign, [Named QVTR.Sen]) -> Result (CASLSign, [Named CASLFORMULA])

mapTheory (s, ns) = let cs = mapSign s in

return (cs, map (mapNamed $ mapSen s cs) ns ++ sentences cs )

mapSign :: QVTR.Sign -> CASLSign

mapSign s =

let

sSign = CSMOF2CASL.mapSign (sourceSign s)

tSign = CSMOF2CASL.mapSign (targetSign s)

relsProp = getPropertiesFromRelations (nonTopRelations s) (topRelations s)

keysProp = getPropertiesFromKeys (keyDefs s)

sUnion = C.uniteCASLSign sSign tSign

everyProp = C.addMapSet (C.predMap sUnion) (C.addMapSet relsProp keysProp)

sentRels = C.sentences sSign ++ C.sentences tSign

in

addStringSignature (replacePredMap (replaceSentences sUnion sentRels) everyProp)

getPropertiesFromRelations :: Map.Map String RuleDef -> Map.Map String RuleDef -> PredMap

getPropertiesFromRelations nonTopRel topRel = getRelDef $ Map.assocs nonTopRel

++ Map.assocs topRel

getRelDef :: [(String, RuleDef)] -> PredMap

getRelDef [] = MapSet.empty

getRelDef ((nam, rulDef) : rest) =

let na = stringToId nam

pa = foldr ((:) . stringToId . CSMOF.name) [] (QVTR.parameters rulDef)

in MapSet.insert na (C.PredType pa) (getRelDef rest)

getPropertiesFromKeys :: [(String, String)] -> PredMap

getPropertiesFromKeys [] = MapSet.empty

getPropertiesFromKeys ((met, typ) : rest) =

MapSet.insert (predKeyName met typ) (C.PredType []) (getPropertiesFromKeys rest)

predKeyName :: String -> String -> Id

predKeyName met typ = stringToId $ "key_" ++ met ++ "_" ++ typ

replacePredMap :: CASLSign -> PredMap -> CASLSign

replacePredMap (C.Sign sR rSR eSR oM aO _ vM s dS eD aM gA eI) predM =

C.Sign sR rSR eSR oM aO predM vM s dS eD aM gA eI

replaceSentences :: CASLSign -> [Named CASLFORMULA] -> CASLSign

replaceSentences (C.Sign sR rSR eSR oM aO pM vM _ dS eD aM gA eI) sent =

C.Sign sR rSR eSR oM aO pM vM sent dS eD aM gA eI

-- ------ Sentences

mapSen :: QVTR.Sign -> CASLSign -> QVTR.Sen -> CASLFORMULA

mapSen qvtrSign _ (KeyConstr k) = createKeyFormula qvtrSign k

mapSen qvtrSign sig (QVTSen r) = createRuleFormula qvtrSign sig r

createKeyFormula :: QVTR.Sign -> Key -> CASLFORMULA

createKeyFormula qvtrSign k =

let

souVars = CSMOF2CASL.generateVars "x" 2

tarVars = CSMOF2CASL.generateVars "y" $ toInteger $ length $ properties k

typeSouVar = stringToId (typeName k)

souVarDec = Var_decl souVars typeSouVar nullRange

(tarVarDec, props) = getVarFromKey qvtrSign tarVars (properties k) (typeName k)

pname = predKeyName (metamodel k) (typeName k)

equal = Negation (Equation (Qual_var (head souVars) typeSouVar nullRange)

Strong

(Qual_var (head $ tail souVars) typeSouVar nullRange)

nullRange)

nullRange

sent = C.Relation equal

Implication

(C.Relation

(Junction Con (getPredicatesInvocation (mkSimpleId "x_1")

(typeName k) tarVars (properties k) props) nullRange)

Implication

(Junction Dis (map (`Negation` nullRange)

(getPredicatesInvocation (mkSimpleId "x_2")

(typeName k) tarVars (properties k) props)) nullRange)

nullRange)

nullRange

in

C.Relation

(C.Predication (C.Qual_pred_name pname (Pred_type [] nullRange) nullRange)

[]

nullRange)

C.Equivalence

(Quantification Universal (souVarDec : tarVarDec) sent nullRange)

nullRange

getPredicatesInvocation :: VAR -> String -> [VAR] -> [PropKey] -> [Maybe CSMOF.PropertyT] -> [CASLFORMULA]

getPredicatesInvocation _ _ [] [] [] = []

getPredicatesInvocation x typN (v : restV) (p : restP) (pT : restPT) =

let pr = case pT of

Nothing -> trueForm

Just prop -> case p of

SimpleProp pN -> let sor = QVTRAn.getOppositeType pN prop

sor2 = QVTRAn.getTargetType pN prop

in Predication

(C.Qual_pred_name (stringToId pN)

(Pred_type

[stringToId sor,

stringToId sor2]

nullRange) nullRange)

(Qual_var x (stringToId typN)

nullRange :

[Qual_var v (stringToId sor2)

nullRange]) nullRange

OppositeProp oPType oPName ->

let sor = QVTRAn.getTargetType oPName prop

in Predication

(C.Qual_pred_name (stringToId oPName)

(Pred_type [stringToId oPType,

stringToId sor] nullRange)

nullRange)

(Qual_var v (stringToId oPType) nullRange :

[Qual_var x (stringToId typN) nullRange])

nullRange

in pr : getPredicatesInvocation x typN restV restP restPT

getPredicatesInvocation _ _ _ _ _ = []

getVarFromKey :: QVTR.Sign -> [VAR] -> [PropKey] -> String -> ([VAR_DECL], [Maybe CSMOF.PropertyT])

getVarFromKey _ [] [] _ = ([], [])

getVarFromKey qvtrSign (v : restV) (p : restP) typN =

let

(decl, prop) = case p of

SimpleProp pN -> let (idP, propT) = getSortOfProperty qvtrSign typN pN

in (Var_decl [v] idP nullRange, propT)

OppositeProp oPType oPName -> let (_, propT) = getSortOfProperty qvtrSign oPType oPName

in (Var_decl [v] (stringToId oPType) nullRange, propT)

(restD, restPr) = getVarFromKey qvtrSign restV restP typN

in

(decl : restD, prop : restPr)

getVarFromKey _ _ _ _ = ([], [])

getSortOfProperty :: QVTR.Sign -> String -> String -> (Id, Maybe CSMOF.PropertyT)

getSortOfProperty qvtrSign typN pN =

let sourceProp = QVTRAn.findPropertyInHierarchy (CSMOF.typeRel $ QVTR.sourceSign qvtrSign)

(CSMOF.properties $ QVTR.sourceSign qvtrSign) typN pN

targetProp = QVTRAn.findPropertyInHierarchy (CSMOF.typeRel $ QVTR.targetSign qvtrSign)

(CSMOF.properties $ QVTR.targetSign qvtrSign) typN pN

in

case sourceProp of

Nothing -> case targetProp of

Nothing -> (stringToId "", Nothing)

Just p -> (stringToId $ QVTRAn.getTargetType pN p, Just p)

Just p -> (stringToId $ QVTRAn.getTargetType pN p, Just p)

createRuleFormula :: QVTR.Sign -> CASLSign -> QVTR.RelationSen -> CASLFORMULA

createRuleFormula qvtSign _ (QVTR.RelationSen rDef varS parS souPat tarPat whenC whereC) =

let

rName = QVTR.name rDef

parTyp = map (stringToId . varType) parS

whenVarSet = collectWhenVarSet varS whenC

souVarInOCL = foldr (\ (_, _, ocl) l -> l ++ getVarIdsFromOCLExpre varS ocl)

[] (QVTR.patPreds souPat)

souDomVarSet = Set.fromList (QVTR.patVarSet souPat ++ souVarInOCL)

tarVarInOCL = foldr (\ (_, _, ocl) l -> l ++ getVarIdsFromOCLExpre varS ocl)

[] (QVTR.patPreds tarPat)

tarDomVarSet = Set.fromList (QVTR.patVarSet tarPat ++ tarVarInOCL)

whereVarSet = Set.fromList $ collectWhenVarSet varS whereC

varSet_2 = Set.difference (Set.difference (Set.union tarDomVarSet whereVarSet) (Set.fromList whenVarSet)) souDomVarSet

in

if null parS

then C.Relation

(C.Predication (C.Qual_pred_name (stringToId rName) (Pred_type parTyp nullRange) nullRange)

[]

nullRange)

C.Equivalence

(if null whenVarSet

then buildEmptyWhenFormula qvtSign parS varS varSet_2 souPat tarPat whereC

else buildNonEmptyWhenFormula qvtSign whenVarSet parS varS varSet_2 souPat tarPat whenC whereC)

nullRange

else Quantification Universal (varDeclFromRelVar parS)

(C.Relation (C.Predication (C.Qual_pred_name (stringToId rName) (Pred_type parTyp nullRange) nullRange)

(createVarRule parS)

nullRange)

C.Equivalence

(if null whenVarSet

then buildEmptyWhenFormula qvtSign parS varS varSet_2 souPat tarPat whereC

else buildNonEmptyWhenFormula qvtSign whenVarSet parS varS varSet_2 souPat tarPat whenC whereC)

nullRange)

nullRange

createVarRule :: [RelVar] -> [C.CASLTERM]

createVarRule = map (\ v -> Qual_var (mkSimpleId $ varName v)

(stringToId $ varType v) nullRange)

collectWhenVarSet :: [RelVar] -> Maybe QVTRAs.WhenWhere -> [RelVar]

collectWhenVarSet _ Nothing = []

collectWhenVarSet varS (Just (WhenWhere relInv oclExp)) =

let

relVars = QVTRAn.getSomething $ map (findRelVarFromName varS)

(concatMap QVTRAs.params relInv)

oclExpVars = foldr ((++) . getVarIdsFromOCLExpre varS) [] oclExp

in

relVars ++ oclExpVars

findRelVarFromName :: [RelVar] -> String -> Maybe RelVar

findRelVarFromName [] _ = Nothing

findRelVarFromName (v : restV) nam = if QVTRAs.varName v == nam

then Just v

else findRelVarFromName restV nam

getVarIdsFromOCLExpre :: [RelVar] -> QVTRAs.OCL -> [RelVar]

getVarIdsFromOCLExpre varS (StringExp str) = getVarIdsFromStrExpre varS str

getVarIdsFromOCLExpre varS (Paren expr) = getVarIdsFromOCLExpre varS expr

getVarIdsFromOCLExpre varS (NotB expr) = getVarIdsFromOCLExpre varS expr

getVarIdsFromOCLExpre varS (AndB exp1 exp2) = getVarIdsFromOCLExpre varS exp1

++ getVarIdsFromOCLExpre varS exp2

getVarIdsFromOCLExpre varS (OrB exp1 exp2) = getVarIdsFromOCLExpre varS exp1

++ getVarIdsFromOCLExpre varS exp2

getVarIdsFromOCLExpre varS (Equal str1 str2) = getVarIdsFromStrExpre varS str1

++ getVarIdsFromStrExpre varS str2

getVarIdsFromOCLExpre _ _ = []

getVarIdsFromStrExpre :: [RelVar] -> QVTRAs.STRING -> [RelVar]

getVarIdsFromStrExpre varS (ConcatExp str1 str2) =

getVarIdsFromStrExpre varS str1 ++ getVarIdsFromStrExpre varS str2

getVarIdsFromStrExpre varS (VarExp v) = case findRelVarFromName varS v of

Nothing -> []

Just r -> [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 qvtSign parS varS varSet_2 souPat tarPat whereC =

let

listPars = Set.fromList parS

diffVarSet_1 = Set.toList $ Set.difference (Set.difference (Set.fromList varS) varSet_2) listPars

diffVarSet_2 = Set.toList $ Set.difference varSet_2 listPars

souPatF = buildPatternFormula qvtSign varS souPat

tarPatF = buildPatternFormula qvtSign varS tarPat

whereF = buildWhenWhereFormula whereC varS

fst_sen | whereF == trueForm =

if tarPatF == trueForm

then if null diffVarSet_2

then trueForm

else C.Quantification Existential

(varDeclFromRelVar diffVarSet_2)

trueForm

nullRange

else if null diffVarSet_2

then tarPatF

else C.Quantification Existential

(varDeclFromRelVar diffVarSet_2)

tarPatF

nullRange

| tarPatF == trueForm =

if null diffVarSet_2

then whereF

else C.Quantification Existential

(varDeclFromRelVar diffVarSet_2)

whereF

nullRange

| null diffVarSet_2 = C.Junction Con [tarPatF, whereF] nullRange

| otherwise = C.Quantification Existential

(varDeclFromRelVar diffVarSet_2)

(C.Junction Con [tarPatF, whereF] nullRange)

nullRange

in

if null diffVarSet_1

then C.Relation souPatF Implication fst_sen nullRange

else C.Quantification Universal

(varDeclFromRelVar diffVarSet_1)

(C.Relation souPatF

Implication

fst_sen

nullRange)

nullRange

varDeclFromRelVar :: [RelVar] -> [VAR_DECL]

varDeclFromRelVar = map (\ v -> Var_decl [mkSimpleId $ varName v]

(stringToId $ varType v) 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 qvtSign whenVarSet parS varS varSet_2 souPat tarPat whenC whereC =

let

listWhenVars = Set.fromList whenVarSet

listPars = Set.fromList parS

diffVarSet_1 = Set.toList $ Set.difference listWhenVars listPars

diffVarSet_2 = Set.toList $ Set.difference (Set.difference (Set.fromList varS) (Set.union listWhenVars varSet_2)) listPars

diffVarSet_3 = Set.toList $ Set.difference varSet_2 listPars

souPatF = buildPatternFormula qvtSign varS souPat

tarPatF = buildPatternFormula qvtSign varS tarPat

whenF = buildWhenWhereFormula whenC varS

whereF = buildWhenWhereFormula whereC varS

snd_sen | whereF == trueForm =

if tarPatF == trueForm

then if null diffVarSet_3

then trueForm

else C.Quantification Existential

(varDeclFromRelVar diffVarSet_3)

trueForm

nullRange

else if null diffVarSet_3

then tarPatF

else C.Quantification Existential

(varDeclFromRelVar diffVarSet_3)

tarPatF

nullRange

| tarPatF == trueForm =

if null diffVarSet_3

then whereF

else C.Quantification Existential

(varDeclFromRelVar diffVarSet_3)

whereF

nullRange

| null diffVarSet_3 = C.Junction Con [tarPatF, whereF] nullRange

| otherwise = C.Quantification Existential

(varDeclFromRelVar diffVarSet_3)

(C.Junction Con [tarPatF, whereF] nullRange)

nullRange

fst_sen | souPatF == trueForm =

if null diffVarSet_2

then snd_sen

else C.Quantification Universal

(varDeclFromRelVar diffVarSet_2)

snd_sen

nullRange

| null diffVarSet_2 = C.Relation souPatF Implication snd_sen nullRange

| otherwise = C.Quantification Universal

(varDeclFromRelVar diffVarSet_2)

(C.Relation souPatF

Implication

snd_sen

nullRange) nullRange

in

if null diffVarSet_1

then C.Relation whenF Implication fst_sen nullRange

else C.Quantification Universal

(varDeclFromRelVar diffVarSet_1)

(C.Relation whenF

Implication

fst_sen

nullRange)

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 qvtSign varS (Pattern _ parRel patPred) =

let

relInvF = map buildPatRelFormula parRel

oclExpF = map (buildOCLFormulaWRel qvtSign varS) patPred

in

if null oclExpF

then if null relInvF

then trueForm

else C.Junction Con relInvF nullRange

else if null relInvF

then C.Junction Con oclExpF nullRange

else C.Junction Con (relInvF ++ oclExpF) nullRange

buildPatRelFormula :: (CSMOF.PropertyT, RelVar, RelVar) -> CASLFORMULA

buildPatRelFormula (p, souV, tarV) =

let

rName = CSMOF.targetRole p

predTyp = [stringToId $ CSMOF.name $ CSMOF.sourceType p, stringToId $

CSMOF.name $ CSMOF.targetType p]

varsInv = createVarRule [souV, tarV]

in

Predication (C.Qual_pred_name (stringToId rName) (Pred_type predTyp nullRange) nullRange)

varsInv

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 Nothing _ = trueForm -- ERROR, this cannot happens

buildWhenWhereFormula (Just (WhenWhere relInv oclExp)) varS =

let

relInvF = map (buildRelInvocFormula varS) relInv

oclExpF = map (buildOCLFormula varS) oclExp

in

if null oclExpF

then if null relInvF

then trueForm

else C.Junction Con relInvF nullRange

else if null relInvF

then C.Junction Con oclExpF nullRange

else C.Junction Con (relInvF ++ oclExpF) nullRange

buildRelInvocFormula :: [RelVar] -> RelInvok -> CASLFORMULA

buildRelInvocFormula varS rel =

let

vars = QVTRAn.getSomething $ map (findRelVarFromName varS) (QVTRAs.params rel)

varsInv = createVarRule vars

predTyp = map (stringToId . varType) vars

in

C.Predication (C.Qual_pred_name (stringToId $ QVTRAs.name rel)

(Pred_type predTyp nullRange) nullRange) varsInv nullRange

buildOCLFormulaWRel :: QVTR.Sign -> [RelVar] -> (String, String, OCL) -> CASLFORMULA

buildOCLFormulaWRel qvtSign varS (prN, varN, StringExp str) =

let oclT = buildSTRINGTerm str varS

typ = case findRelVarFromName varS varN of

Nothing -> ""

Just v -> varType v

(_, p) = getSortOfProperty qvtSign typ prN

(sor, sor2) = case p of

Nothing -> (stringToId "", stringToId "")

Just pp -> if CSMOF.targetRole pp == prN

then (stringToId $ CSMOF.name $ CSMOF.sourceType pp,

stringToId $ CSMOF.name $ CSMOF.targetType pp)

else (stringToId $ CSMOF.name $ CSMOF.targetType pp,

stringToId $ CSMOF.name $ CSMOF.sourceType pp)

in

C.Predication (C.Qual_pred_name (stringToId prN) (Pred_type [sor, sor2]

nullRange) nullRange)

(Qual_var (mkSimpleId varN) (stringToId typ) nullRange : [oclT]) nullRange

buildOCLFormulaWRel _ _ _ = trueForm

buildOCLFormula :: [RelVar] -> OCL -> CASLFORMULA

buildOCLFormula varS (Paren e) = buildOCLFormula varS e

buildOCLFormula _ (BExp b) = if b then trueForm else C.Negation trueForm nullRange

buildOCLFormula varS (NotB e) = C.Negation (buildOCLFormula varS e) nullRange

buildOCLFormula varS (AndB lE rE) = C.Junction Con [buildOCLFormula varS lE,

buildOCLFormula varS rE] nullRange

buildOCLFormula varS (OrB lE rE) = C.Junction Dis [buildOCLFormula varS lE,

buildOCLFormula varS rE] nullRange

buildOCLFormula varS (Equal lE rE) = C.Equation (buildSTRINGTerm lE varS)

Strong (buildSTRINGTerm rE varS) nullRange

buildOCLFormula _ (StringExp _) = trueForm -- This is not a formula, but a term used within an equality

buildSTRINGTerm :: STRING -> [RelVar] -> CASLTERM

buildSTRINGTerm (Str str) _ = C.Application (Qual_op_name (stringToId str)

(Op_type Total [] (stringToId "String") nullRange) nullRange) [] nullRange

buildSTRINGTerm (ConcatExp lS rS) varS =

let

lSTerm = buildSTRINGTerm lS varS

rSTerm = buildSTRINGTerm rS varS

stringSort = stringToId "String"

in

C.Application (Qual_op_name (stringToId "++")

(Op_type Total [stringSort, stringSort] stringSort nullRange)

nullRange)

[lSTerm, rSTerm]

nullRange

buildSTRINGTerm (VarExp vE) varS =

let

var = case findRelVarFromName varS vE of

Nothing -> stringToId ""

Just v -> stringToId $ varType v

in

Qual_var (mkSimpleId vE) var 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 m = return C.Morphism

{ msource = mapSign $ domOfDefaultMorphism m

, mtarget = mapSign $ codOfDefaultMorphism m

, sort_map = Map.empty

, op_map = Map.empty

, pred_map = Map.empty

, 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 s =

let

stringSort = stringToId "String"

(strObj, othObj) = separateStringConstraintFromOthers $ sentences s

{- strObjTr = getStringObjFromTransformation ns

strObjOps = foldr (\(idd,opT) se -> MapSet.insert idd opT se) MapSet.empty (getStringOperations strObjTr) -}

everyString = Set.toList (getStringObjects strObj) -- Set.toList (Set.union strObjTr (getStringObjects strObj))

concatOp = mkTotOpType [stringSort, stringSort] stringSort

in

C.Sign { sortRel = Rel.insertPair stringSort stringSort (C.sortRel s)

, revSortRel = C.revSortRel s

, emptySortSet = C.emptySortSet s

, opMap = MapSet.insert (stringToId "++") concatOp (C.opMap s) -- MapSet.union strObjOps (C.opMap s)

, assocOps = C.assocOps s

, predMap = C.predMap s

, varMap = C.varMap s

, sentences = getNoConfusionStrings everyString :

(toStringConstraint (stringSort, everyString) :

deleteNoConfusionString othObj)

, declaredSymbols = C.declaredSymbols s

, envDiags = C.envDiags s

, annoMap = C.annoMap s

, globAnnos = C.globAnnos s

, extendedInfo = C.extendedInfo 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 [] = []

deleteNoConfusionString (nf : restNF) =

let rest = deleteNoConfusionString restNF

in if startswith (senAttr nf) "noConfusion_String"

then rest

else nf : rest

startswith :: String -> String -> Bool

startswith [] [] = True

startswith (a : restA) (b : restB) = a == b && startswith restA restB

startswith _ _ = False

getNoConfusionStrings :: [Id] -> Named CASLFORMULA

getNoConfusionStrings ordObj =

let diffForm = foldr ((++) . diffOfRestStringOps ordObj) [] ordObj

in makeNamed "noConfusion_String" (Junction Con diffForm nullRange)

diffOfRestStringOps :: [Id] -> Id -> [CASLFORMULA]

diffOfRestStringOps lisObj objName =

let lis = removeUntilId lisObj objName

in concatMap (diffOpsStr objName) lis

removeUntilId :: [Id] -> Id -> [Id]

removeUntilId lis str =

case lis of

[] -> []

a : rest -> if a == str

then rest

else removeUntilId rest str

diffOpsStr :: Id -> Id -> [CASLFORMULA]

diffOpsStr objName1 objName2 =

[Negation (Equation

(Application (Qual_op_name objName1

(Op_type Total [] (stringToId "String") nullRange)

nullRange) [] nullRange)

Strong

(Application (Qual_op_name objName2

(Op_type Total [] (stringToId "String") nullRange)

nullRange) [] nullRange)

nullRange)

nullRange | objName1 /= 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 [] = ([], [])

separateStringConstraintFromOthers (f : restF) =

let (restString, restOther) = separateStringConstraintFromOthers restF

in case sentence f of

Sort_gen_ax [Constraint sor _ _] _ -> if sor == stringToId "String"

then (f : restString, restOther)

else (restString, f : restOther)

_ -> (restString, f : restOther)

-- Get String names from Qual_op_name

getStringObjects :: [Named CASLFORMULA] -> Set.Set Id

getStringObjects [] = Set.empty

getStringObjects (f : restF) =

case sentence f of

Sort_gen_ax [Constraint _ listObj _] _ -> Set.union

(getObjNamesFromOp listObj) (getStringObjects restF)

_ -> getStringObjects restF

getObjNamesFromOp :: [(OP_SYMB, [Int])] -> Set.Set Id

getObjNamesFromOp [] = Set.empty

getObjNamesFromOp ((op, _) : restOp) =

case op of

Qual_op_name obj _ _ -> Set.insert obj (getObjNamesFromOp restOp)

_ -> getObjNamesFromOp restOp

{- Generate free type

String ::= EMPTY | ... (string instances) ...

__ ++ __ (first: String; rest: String) -}

toStringConstraint :: (Id, [Id]) -> Named CASLFORMULA

toStringConstraint (sor, lisObj) =

let

stringSort = stringToId "String"

concatOp = (Qual_op_name (stringToId "++") (Op_type Total

[stringSort, stringSort] stringSort nullRange) nullRange, [])

simplCon = Constraint sor (concatOp : foldr ((:) . toConstraintFromId sor)

[] lisObj) sor

constr = Sort_gen_ax [simplCon] True

in

makeNamed "sortGenCon_String" constr

toConstraintFromId :: Id -> Id -> (OP_SYMB, [Int])

toConstraintFromId sor obj = (Qual_op_name obj (Op_type Total [] sor nullRange)

nullRange, [])