1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs{- |

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsModule : $Header$

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsDescription : Coding CSMOF into CASL

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsCopyright : (c) Daniel Calegari Universidad de la Republica, Uruguay 2013

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsLicense : GPLv2 or higher, see LICENSE.txt

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsMaintainer : dcalegar@fing.edu.uy

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsStability : provisional

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsPortability : portable

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs-}

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsmodule Comorphisms.CSMOF2CASL

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ( CSMOF2CASL (..), mapSign, generateVars

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ) where

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport Logic.Logic

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport Logic.Comorphism

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport Common.DefaultMorphism

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs-- CSMOF

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport CSMOF.Logic_CSMOF as CSMOF

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport CSMOF.As as CSMOFAs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport CSMOF.Sign as CSMOF

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs-- CASL

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport CASL.Logic_CASL

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport CASL.AS_Basic_CASL as C

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport CASL.Sublogic

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport CASL.Sign as C

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport CASL.Morphism as C

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport Common.AS_Annotation

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport Common.GlobalAnnotations

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport Common.Id

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport Common.ProofTree

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport Common.Result

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport qualified Common.Lib.Rel as Rel

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport qualified Common.Lib.MapSet as MapSet

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport qualified Data.Set as Set

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsimport qualified Data.Map as Map

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs-- | lid of the morphism

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsdata CSMOF2CASL = CSMOF2CASL deriving Show

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsinstance Language CSMOF2CASL -- default is ok

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacsinstance Comorphism CSMOF2CASL

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CSMOF.CSMOF

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ()

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CSMOFAs.Metamodel

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CSMOF.Sen

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ()

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ()

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CSMOF.Sign

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CSMOF.Morphism

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ()

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ()

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ()

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CASL

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CASL_Sublogics

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CASLBasicSpec

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CASLFORMULA

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs SYMB_ITEMS

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs SYMB_MAP_ITEMS

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CASLSign

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs CASLMor

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs C.Symbol

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs C.RawSymbol

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ProofTree

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs where

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sourceLogic CSMOF2CASL = CSMOF

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sourceSublogic CSMOF2CASL = ()

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs targetLogic CSMOF2CASL = CASL

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs mapSublogic CSMOF2CASL _ = Just $ caslTop

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs { has_part = False

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , sub_features = LocFilSub

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , cons_features = SortGen True True }

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs map_theory CSMOF2CASL = mapTheory

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs map_sentence CSMOF2CASL s = return . mapSen (mapSign s)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs map_morphism CSMOF2CASL = mapMor

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs -- map_symbol CSMOF2CASL _ = Set.singleton . mapSym

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs is_model_transportable CSMOF2CASL = True

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs has_model_expansion CSMOF2CASL = True

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs is_weakly_amalgamable CSMOF2CASL = True

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs isInclusionComorphism CSMOF2CASL = True

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsmapTheory :: (CSMOF.Sign, [Named CSMOF.Sen]) -> Result (CASLSign, [Named CASLFORMULA])

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsmapTheory (s, ns) = let cs = mapSign s in

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs return (cs, map (mapNamed $ mapSen cs) ns ++ sentences cs)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsmapSign :: CSMOF.Sign -> CASLSign

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsmapSign s =

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs let

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sorts = getSorts (types s) (typeRel s)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ops = getOperations (instances s)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs predd = getPredicates (properties s)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sent = getSentencesRels (links s) (instances s)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sentDisEmb = getSortGen (typeRel s) (abstractClasses s) (types s) (instances s)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs noConfBetOps = getNoConfusionBetweenSets (instances s) (typeRel s)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs in

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs C.Sign

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs { sortRel = sorts

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , revSortRel = Just $ Rel.fromList (map revertOrder (Rel.toList sorts))

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , emptySortSet = Set.empty

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , opMap = ops

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , assocOps = MapSet.empty

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , predMap = fst predd

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , varMap = Map.empty

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , sentences = snd predd ++ sent ++ sentDisEmb ++ noConfBetOps

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , declaredSymbols = Set.empty

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , envDiags = []

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , annoMap = MapSet.empty

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , globAnnos = emptyGlobalAnnos

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs , extendedInfo = ()

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs }

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsgetSorts :: Set.Set TypeClass -> Rel.Rel TypeClass -> Rel.Rel SORT

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsgetSorts setC relC =

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs let relS = Set.fold (insertSort . name) Rel.empty setC

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs in foldr (insertPair) relS (Rel.toList relC)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsinsertSort :: String -> Rel.Rel SORT -> Rel.Rel SORT

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsinsertSort s relS = Rel.insertPair (stringToId s) (stringToId s) relS

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsinsertPair :: (TypeClass,TypeClass) -> Rel.Rel SORT -> Rel.Rel SORT

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsinsertPair (t1,t2) relS = Rel.insertPair (stringToId $ name t1) (stringToId $ name t2) relS

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsrevertOrder :: (SORT,SORT) -> (SORT,SORT)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsrevertOrder (a,b) = (b,a)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsgetPredicates :: Set.Set PropertyT -> (PredMap,[Named (FORMULA f)])

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsgetPredicates props = Set.fold (insertPredicate) (MapSet.empty,[]) props

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsinsertPredicate :: PropertyT -> (PredMap,[Named (FORMULA f)]) -> (PredMap,[Named (FORMULA f)])

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsinsertPredicate prop (predM,form) =

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs let

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sort1 = stringToId $ name $ sourceType prop

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sort2 = stringToId $ name $ targetType prop

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs pname1 = stringToId $ targetRole prop

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ptype1 = PredType $ sort1 : [sort2]

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs pname2 = stringToId $ sourceRole prop

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs ptype2 = PredType $ sort2 : [sort1]

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs nam = "equiv_" ++ targetRole prop ++ "_" ++ sourceRole prop

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs varsD = [Var_decl [(mkSimpleId "x")] sort2 nullRange, Var_decl [(mkSimpleId "y")] sort1 nullRange]

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sentRel = C.Relation

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs (C.Predication (C.Qual_pred_name pname2 (Pred_type [sort2,sort1] nullRange) nullRange)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs (C.Qual_var (mkSimpleId "x") sort2 nullRange : [C.Qual_var (mkSimpleId "y") sort1 nullRange])

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs nullRange)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs C.Equivalence

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs (C.Predication (C.Qual_pred_name pname1 (Pred_type [sort1,sort2] nullRange) nullRange)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs (C.Qual_var (mkSimpleId "y") sort1 nullRange : [C.Qual_var (mkSimpleId "x") sort2 nullRange])

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs nullRange)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs nullRange

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sent = Quantification Universal varsD sentRel nullRange

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs in

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs -- MapSet does not allows repeated elements, but predicate names can be repeated

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs -- (this must be corrected by creating a more complex ID)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs if sourceRole prop == "_"

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs then (MapSet.insert pname1 ptype1 predM, form)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs else if targetRole prop == "_"

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs then (MapSet.insert pname2 ptype2 predM, form)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs else (MapSet.insert pname1 ptype1 $ MapSet.insert pname2 ptype2 predM, (makeNamed nam sent) : form)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsgetOperations :: Map.Map String TypeClass -> OpMap

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsgetOperations ops = foldr (insertOperations) MapSet.empty (Map.toList ops)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsinsertOperations :: (String,TypeClass) -> OpMap -> OpMap

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsinsertOperations (na,tc) opM =

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs let

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs opName = stringToId na

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs opType = OpType Total [] (stringToId $ name tc)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs in

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs MapSet.insert opName opType opM

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsgetSentencesRels :: Set.Set LinkT -> Map.Map String TypeClass -> [Named (CASLFORMULA)]

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacsgetSentencesRels linkk ops = completenessOfRelations linkk ops

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacscompletenessOfRelations :: Set.Set LinkT -> Map.Map String TypeClass -> [Named (CASLFORMULA)]

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacscompletenessOfRelations linkk ops =

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs let ordLinks = getLinksByProperty linkk

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs in foldr ((++) . (createComplFormula ops)) [] (Map.toList ordLinks)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacscreateComplFormula :: Map.Map String TypeClass -> (String,[LinkT]) -> [Named (CASLFORMULA)]

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks MalnacscreateComplFormula ops (nam,linksL) =

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs let

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs varA = mkSimpleId "x"

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs varB = mkSimpleId "y"

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs in

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs case linksL of

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs [] -> []

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs (LinkT _ _ pr) : _ -> let

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sorA = stringToId $ name $ sourceType pr

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sorB = stringToId $ name $ targetType pr

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs varsD = [Var_decl [varA] sorA nullRange, Var_decl [varB] sorB nullRange]

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sent = C.Relation

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs (C.Predication (C.Qual_pred_name (stringToId $ targetRole pr) (Pred_type [sorA,sorB] nullRange) nullRange)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs (C.Qual_var varA sorA nullRange

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs : [C.Qual_var varB sorB nullRange])

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs nullRange)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs C.Equivalence

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs (Junction Dis (foldr ((:) . (getPropHold ops varA sorA varB sorB)) [] linksL) nullRange)

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs nullRange

1bbfd08d1d3f7f7ce1f775d469063cbedb6c26cdMareks Malnacs sentQuan = Quantification Universal varsD sent nullRange

in

[makeNamed ("compRel_" ++ nam) sentQuan]

getPropHold :: Map.Map String TypeClass -> VAR -> SORT -> VAR -> SORT -> LinkT -> CASLFORMULA

getPropHold ops varA sorA varB sorB lin =

let

souObj = Map.lookup (sourceVar lin) ops

tarObj = Map.lookup (targetVar lin) ops

typSou = case souObj of

Nothing -> sourceVar lin -- if happens then is an error

Just tSou -> name tSou

typTar = case tarObj of

Nothing -> targetVar lin -- if happens then is an error

Just tTar -> name tTar

eqA = Equation (Qual_var varA sorA nullRange)

Strong

(Application (Qual_op_name (stringToId (sourceVar lin))

(Op_type Total [] (stringToId typSou) nullRange)

nullRange) [] nullRange)

nullRange

eqB = Equation (Qual_var varB sorB nullRange)

Strong

(Application (Qual_op_name (stringToId (targetVar lin))

(Op_type Total [] (stringToId typTar) nullRange)

nullRange) [] nullRange)

nullRange

in

Junction Con (eqA : [eqB]) nullRange

getLinksByProperty :: Set.Set LinkT -> Map.Map String [LinkT]

getLinksByProperty linkk =

let elems = Set.elems linkk

in foldr (getByProperty) Map.empty elems

getByProperty :: LinkT -> Map.Map String [LinkT] -> Map.Map String [LinkT]

getByProperty lin mapL =

let

prope = CSMOF.property lin

nameLook = sourceRole prope ++ name (sourceType prope) ++ targetRole prope ++ name (targetType prope)

setProp = Map.lookup nameLook mapL

in

case setProp of

Nothing -> Map.insert nameLook [lin] (Map.delete nameLook mapL)

Just s -> Map.insert nameLook (lin : s) (Map.delete nameLook mapL)

getSortGen :: Rel.Rel TypeClass -> Set.Set TypeClass -> Set.Set TypeClass -> Map.Map String TypeClass -> [Named (CASLFORMULA)]

getSortGen typpR absCl typCl inst = disjointEmbedding absCl typpR ++ sortGeneration inst ++

sortGenerationNonAbstractSuperClasses typpR typCl absCl inst

-- Free type of non-abstract superclasses

sortGenerationNonAbstractSuperClasses :: Rel.Rel TypeClass -> Set.Set TypeClass -> Set.Set TypeClass -> Map.Map String TypeClass -> [Named (CASLFORMULA)]

sortGenerationNonAbstractSuperClasses typpR typCl absCl inst =

let

ordObj = foldr (orderByClass) Map.empty (Map.toList inst)

nonAbsClasses = getNonAbstractClasess absCl typCl

nonAbsClassesWChilds = filter (\x -> not (null (snd x))) (Set.fold ((:) . (getSubClasses typpR)) [] nonAbsClasses)

childObjects = foldr ((:) . (getClassSubObjects ordObj)) [] nonAbsClassesWChilds -- [(TypeClass,[String])]

in

foldr ((:) . (toSortConstraintNonAbsClass inst)) [] childObjects

-- Takes the objects, and a class with its child classes and returns the descendent objects of such class

getClassSubObjects :: Map.Map TypeClass [String] -> (TypeClass,[TypeClass]) -> (TypeClass,[String])

getClassSubObjects objs (tc, subCl) =

let objTC = findObjectInMap objs tc

in

(tc, objTC ++ (foldr ((++) . (findObjectInMap objs)) [] subCl))

findObjectInMap :: Map.Map TypeClass [String] -> TypeClass -> [String]

findObjectInMap objs tc =

case Map.lookup tc objs of

Nothing -> []

Just objsTC -> objsTC

getNonAbstractClasess :: Set.Set TypeClass -> Set.Set TypeClass -> Set.Set TypeClass

getNonAbstractClasess absCl classes = Set.difference classes absCl

getSubClasses :: Rel.Rel TypeClass -> TypeClass -> (TypeClass,[TypeClass])

getSubClasses typpR tc =

let subCla = map (fst) (filter (isParent tc) (Rel.toList typpR))

rec = foldr ((++) . snd . (getSubClasses typpR)) [] subCla

in (tc, subCla ++ rec)

isParent :: TypeClass -> (TypeClass,TypeClass) -> Bool

isParent tc (_,tc2) = tc == tc2

toSortConstraintNonAbsClass :: Map.Map String TypeClass -> (TypeClass, [String]) -> Named (CASLFORMULA)

toSortConstraintNonAbsClass inst (tc,lisObj) =

let

sor = stringToId $ name tc

varA = Var_decl [(mkSimpleId "x")] sor nullRange

sent = Junction Dis (foldr ((:) . (getEqualityVarObject sor inst)) [] lisObj) nullRange

constr = Quantification Universal [varA] sent nullRange

in

makeNamed ("sortGenCon_" ++ name tc) constr

getEqualityVarObject :: SORT -> Map.Map String TypeClass -> String -> CASLFORMULA

getEqualityVarObject sor inst obj =

let oTyp = case Map.lookup obj inst of

Nothing -> stringToId obj -- If happens, there is an error

Just ob -> stringToId $ name ob

in

Equation (Qual_var (mkSimpleId "x") sor nullRange)

Strong

(Application (Qual_op_name (stringToId obj)

(Op_type Total [] oTyp nullRange)

nullRange) [] nullRange)

nullRange

-- Sorts are generated as a free type of object functions

sortGeneration :: Map.Map String TypeClass -> [Named (CASLFORMULA)]

sortGeneration inst =

let

ordObj = foldr (orderByClass) Map.empty (Map.toList inst)

noJunk = foldr ((:) . toSortConstraint) [] (Map.toList ordObj)

in

noJunk

mapFilterJust :: [Maybe a] -> [a]

mapFilterJust list =

case list of

[] -> []

a : rest -> case a of

Nothing -> mapFilterJust rest

Just el -> el : mapFilterJust rest

orderByClass :: (String,TypeClass) -> Map.Map TypeClass [String] -> Map.Map TypeClass [String]

orderByClass (ob,tc) mapTC =

case Map.lookup tc mapTC of

Nothing -> Map.insert tc [ob] mapTC

Just listObj -> Map.insert tc (ob : listObj) (Map.delete tc mapTC)

getNoConfusionBetweenSets :: Map.Map String TypeClass -> Rel.Rel TypeClass -> [Named (CASLFORMULA)]

getNoConfusionBetweenSets inst relC =

let ordObj = Map.toList $ foldr (orderByClass) Map.empty (Map.toList inst)

in mapFilterJust $ foldr ((:) . getNoConfusionBSetsAxiom ordObj relC) [] ordObj

getNoConfusionBSetsAxiom :: [(TypeClass, [String])] -> Rel.Rel TypeClass -> (TypeClass, [String]) -> Maybe (Named (CASLFORMULA))

getNoConfusionBSetsAxiom ordObj relC (tc,lisObj) =

case lisObj of

[] -> Nothing

_ : _ -> let

filteredObj = removeUntilType tc ordObj

diffForm = foldr ((++) . (diffOfRestConstants (tc,lisObj) relC)) [] filteredObj

in

case diffForm of

[] -> Nothing

_ : _ -> let constr = Junction Con diffForm nullRange

in Just $ makeNamed ("noConfusion_" ++ name tc) constr

removeUntilType :: TypeClass -> [(TypeClass, [String])] -> [(TypeClass, [String])]

removeUntilType tc lis =

case lis of

[] -> []

(tc2,lisObj2) : rest -> if tc == tc2

then (tc2,lisObj2) : rest

else removeUntilType tc rest

diffOfRestConstants :: (TypeClass, [String]) -> Rel.Rel TypeClass -> (TypeClass, [String]) -> [CASLFORMULA]

diffOfRestConstants (tc1,lisObj1) relC (tc2,lisObj2) =

case tc1 == tc2 of

True -> foldr ((++) . (diffOfRestOps tc1 lisObj1)) [] lisObj1

False -> case haveCommonSort tc1 tc2 relC of

True -> concat $ map (diffOfRestOpsDiffSort (tc1,lisObj1) tc2) lisObj2

False -> []

haveCommonSort :: TypeClass -> TypeClass -> Rel.Rel TypeClass -> Bool

haveCommonSort t1 t2 relT =

let succT1 = superSorts relT t1

succT2 = superSorts relT t2

in not $ Set.null $ Set.intersection succT1 succT2

-- This is the non exported function reachable in Rel

superSorts :: Rel.Rel TypeClass -> TypeClass -> Set.Set TypeClass

superSorts relT tc = Set.fold reach Set.empty $ Rel.succs relT tc where

reach e s = if Set.member e s then s

else Set.fold reach (Set.insert e s) $ Rel.succs relT e

diffOfRestOpsDiffSort :: (TypeClass, [String]) -> TypeClass -> String -> [CASLFORMULA]

diffOfRestOpsDiffSort (tc1,lisObj1) tc2 objName = concat $ map (diffOpsDiffSorts tc2 objName tc1) lisObj1

diffOpsDiffSorts :: TypeClass -> String -> TypeClass -> String -> [CASLFORMULA]

diffOpsDiffSorts tc2 objName2 tc1 objName1 = [Negation (Equation

(Application (Qual_op_name (stringToId objName1)

(Op_type Total [] (stringToId $ name tc1) nullRange)

nullRange)

[] nullRange)

Strong

(Application (Qual_op_name (stringToId objName2)

(Op_type Total [] (stringToId $ name tc2) nullRange)

nullRange)

[] nullRange)

nullRange)

nullRange]

diffOfRestOps :: TypeClass -> [String] -> String -> [CASLFORMULA]

diffOfRestOps tc lisObj objName =

let lis = removeUntil lisObj objName

in concat $ map (diffOps tc objName) lis

removeUntil :: [String] -> String -> [String]

removeUntil lis str =

case lis of

[] -> []

a : rest -> if a == str

then rest

else removeUntil rest str

diffOps :: TypeClass -> String -> String -> [CASLFORMULA]

diffOps tc objName1 objName2 =

if not (objName1 == objName2)

then [Negation (Equation

(Application (Qual_op_name (stringToId objName1)

(Op_type Total [] (stringToId $ name tc) nullRange)

nullRange) [] nullRange)

Strong

(Application (Qual_op_name (stringToId objName2)

(Op_type Total [] (stringToId $ name tc) nullRange)

nullRange) [] nullRange)

nullRange)

nullRange]

else []

toSortConstraint :: (TypeClass, [String]) -> Named (CASLFORMULA)

toSortConstraint (tc,lisObj) =

let

sor = stringToId $ name tc

simplCon = Constraint sor (foldr ((:) . toConstraint sor) [] lisObj) sor

constr = Sort_gen_ax [simplCon] True

in

makeNamed ("sortGenCon_" ++ name tc) constr

toConstraint :: Id -> String -> (OP_SYMB, [Int])

toConstraint sor obName =

let obj = stringToId obName

in

(Qual_op_name obj (Op_type Total [] sor nullRange) nullRange,[])

-- Each abstract class is the disjoint embedding of it subsorts

disjointEmbedding :: Set.Set TypeClass -> Rel.Rel TypeClass -> [Named (CASLFORMULA)]

disjointEmbedding absCl rel =

let

injSyms = map (\ (s, t) -> (Qual_op_name (mkUniqueInjName (stringToId $ name s) (stringToId $ name t))

(Op_type Total [(stringToId $ name s)] (stringToId $ name t) nullRange) nullRange,[]))

$ Rel.toList

$ Rel.irreflex rel

resType _ ((Op_name _),_) = False

resType s ((Qual_op_name _ t _),_) = res_OP_TYPE t == s

collectOps s = Constraint (stringToId $ name s) (filter (resType (stringToId $ name s)) injSyms) (stringToId $ name s)

sortList = Set.toList absCl

constrs = map collectOps sortList

in

[makeNamed "disjEmbedd" (Sort_gen_ax constrs True)]

mapSen :: CASLSign -> CSMOF.Sen -> CASLFORMULA

mapSen sig (Sen con car cot) = -- trueForm

case cot of

EQUAL -> let

minC = minConstraint con car (predMap sig)

maxC = maxConstraint con car (predMap sig)

in

Junction Con (minC : [maxC]) nullRange

LEQ -> maxConstraint con car (predMap sig)

GEQ -> minConstraint con car (predMap sig)

minConstraint :: MultConstr -> Integer -> PredMap -> CASLFORMULA

minConstraint con int predM =

let

predTypes = MapSet.lookup (stringToId $ getRole con) predM -- Set PredType

souVars = generateVars "x" 1

tarVars = generateVars "y" int

correctPredType = Set.fold (getCorrectPredType con) [] predTypes

souVarDec = Var_decl souVars (head (predArgs (head correctPredType))) nullRange

tarVarDec = Var_decl tarVars (last (predArgs (head correctPredType))) nullRange

in

if int > 1

then Quantification Universal [souVarDec] (Quantification

Existential

[tarVarDec]

(Junction Con ((generateVarDiff tarVarDec) :

[(generateProp souVarDec tarVarDec (stringToId $ getRole con))]) nullRange)

nullRange)

nullRange

else Quantification Universal [souVarDec] (Quantification

Existential

[tarVarDec]

(generateProp souVarDec tarVarDec (stringToId $ getRole con))

nullRange

) nullRange

getCorrectPredType :: MultConstr -> PredType -> [PredType] -> [PredType]

getCorrectPredType con pt ptLis =

case (stringToId $ name (CSMOF.getType con)) == head (predArgs pt) of

True -> pt : ptLis

False -> ptLis

generateVars :: String -> Integer -> [VAR]

generateVars varRoot int =

case int of

1 -> [mkSimpleId (varRoot ++ "_" ++ show int)]

n -> mkSimpleId (varRoot ++ "_" ++ show int) : generateVars varRoot (n-1)

generateVarDiff :: VAR_DECL -> CASLFORMULA

generateVarDiff (Var_decl vars sor _) = Junction Con (foldr ((++) . diffOfRest sor vars) [] vars) nullRange

diffOfRest :: SORT -> [VAR] -> VAR -> [CASLFORMULA]

diffOfRest sor vars var = map (diffVar sor var) vars

diffVar :: SORT -> VAR -> VAR -> CASLFORMULA

diffVar sor var1 var2 =

if not (var1 == var2)

then Negation (Equation

(Qual_var var1 sor nullRange)

Strong

(Qual_var var2 sor nullRange)

nullRange)

nullRange

else trueForm

generateProp :: VAR_DECL -> VAR_DECL -> Id -> CASLFORMULA

generateProp (Var_decl varD sort _) (Var_decl varD2 sort2 _) rol =

Junction Con (map (createPropRel (head varD) sort rol sort2) varD2) nullRange

createPropRel :: VAR -> SORT -> Id -> SORT -> VAR -> CASLFORMULA

createPropRel souVar sor rol sor2 tarVar =

Predication (C.Qual_pred_name rol (Pred_type [sor,sor2] nullRange) nullRange)

((Qual_var souVar sor nullRange):[Qual_var tarVar sor2 nullRange]) nullRange

maxConstraint :: MultConstr -> Integer -> PredMap -> CASLFORMULA

maxConstraint con int predM =

let

predTypes = MapSet.lookup (stringToId $ getRole con) predM -- Set PredType

souVars = generateVars "x" 1

tarVars = generateVars "y" (int + 1)

correctPredType = Set.fold (getCorrectPredType con) [] predTypes

souVarDec = Var_decl souVars (head (predArgs (head correctPredType))) nullRange

tarVarDec = Var_decl tarVars (last (predArgs (head correctPredType))) nullRange

in

Quantification Universal (souVarDec : [tarVarDec])

(Relation

(Junction Con [generateProp souVarDec tarVarDec (stringToId $ getRole con)] nullRange)

Implication

(Junction Dis (generateExEqual tarVarDec) nullRange)

nullRange)

nullRange

generateExEqual :: VAR_DECL -> [CASLFORMULA]

generateExEqual (Var_decl varD sor _) = generateExEqualList varD sor

generateExEqualList :: [VAR] -> SORT -> [CASLFORMULA]

generateExEqualList vars sor =

case vars of

[] -> []

v : rest -> (generateExEqualVar rest sor v) ++ (generateExEqualList rest sor)

generateExEqualVar :: [VAR] -> SORT -> VAR -> [CASLFORMULA]

generateExEqualVar vars sor var =

foldr ((++) . (\el -> if el == var

then []

else [Equation (Qual_var var sor nullRange) Strong (Qual_var el sor nullRange) nullRange]))

[] vars

-- | Translation of morphisms

mapMor :: CSMOF.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 :: CSMOF.Symbol -> C.Symbol