content: {-# 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 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 OnlyFree }
        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 = mkSort_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, [])
  