cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegariDescription : Coding CSMOF into CASL
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegariCopyright : (c) Daniel Calegari Universidad de la Republica, Uruguay 2013
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegariLicense : GPLv2 or higher, see LICENSE.txt
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegariMaintainer : dcalegar@fing.edu.uy
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegariStability : provisional
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegariPortability : portable
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari ( CSMOF2CASL (..), mapSign, generateVars
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegariimport CSMOF.As as CSMOFAs
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegariimport qualified Common.Lib.Rel as Rel
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegariimport qualified Common.Lib.MapSet as MapSet
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegariimport qualified Data.Set as Set
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegariimport qualified Data.Map as Map
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Maybe (fromMaybe)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari-- | lid of the morphism
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegaridata CSMOF2CASL = CSMOF2CASL deriving Show
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegariinstance Language CSMOF2CASL -- default is ok
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegariinstance Comorphism CSMOF2CASL
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari CASL_Sublogics
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari CASLBasicSpec
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari SYMB_MAP_ITEMS
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari sourceLogic CSMOF2CASL = CSMOF
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari sourceSublogic CSMOF2CASL = ()
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari targetLogic CSMOF2CASL = CASL
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari mapSublogic CSMOF2CASL _ = Just $ caslTop
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari { has_part = False
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari , sub_features = LocFilSub
b5c780c06889ceb5c241a6b5da7ef0663e5451caDaniel Calegari , cons_features = SortGen True True }
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari map_theory CSMOF2CASL = mapTheory
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari map_sentence CSMOF2CASL s = return . mapSen (mapSign s)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari map_morphism CSMOF2CASL = mapMor
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari -- map_symbol CSMOF2CASL _ = Set.singleton . mapSym
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari is_model_transportable CSMOF2CASL = True
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari has_model_expansion CSMOF2CASL = True
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari is_weakly_amalgamable CSMOF2CASL = True
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari isInclusionComorphism CSMOF2CASL = True
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarimapTheory :: (CSMOF.Sign, [Named CSMOF.Sen]) -> Result (CASLSign, [Named CASLFORMULA])
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarimapTheory (s, ns) = let cs = mapSign s in
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari return (cs, map (mapNamed $ mapSen cs) ns ++ sentences cs)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarimapSign :: CSMOF.Sign -> CASLSign
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari sorts = getSorts (types s) (typeRel s)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari ops = getOperations (instances s)
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari predd = getPredicates (properties s)
b767e7055b5ef62c990a111ac0524500592f8781Daniel Calegari sent = getSentencesRels (links s) (instances s)
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari sentDisEmb = getSortGen (typeRel s) (abstractClasses s) (types s) (instances s)
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari noConfBetOps = getNoConfusionBetweenSets (instances s) (typeRel s)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari { sortRel = sorts
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari , revSortRel = Just $ Rel.fromList (map revertOrder (Rel.toList sorts))
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari , emptySortSet = Set.empty
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari , opMap = ops
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari , predMap = fst predd
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari , sentences = snd predd ++ sent ++ sentDisEmb ++ noConfBetOps
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari , declaredSymbols = Set.empty
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari , envDiags = []
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari , globAnnos = emptyGlobalAnnos
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari , extendedInfo = ()
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarigetSorts :: Set.Set TypeClass -> Rel.Rel TypeClass -> Rel.Rel SORT
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSorts setC relC =
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari let relS = Set.fold (insertSort . name) Rel.empty setC
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in foldr insertPair relS (Rel.toList relC)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegariinsertSort :: String -> Rel.Rel SORT -> Rel.Rel SORT
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinsertSort s = Rel.insertPair (stringToId s) (stringToId s)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinsertPair :: (TypeClass, TypeClass) -> Rel.Rel SORT -> Rel.Rel SORT
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinsertPair (t1, t2) = Rel.insertPair (stringToId $ name t1) (stringToId $ name t2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederrevertOrder :: (SORT, SORT) -> (SORT, SORT)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederrevertOrder (a, b) = (b, a)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetPredicates :: Set.Set PropertyT -> (PredMap, [Named (FORMULA f)])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetPredicates = Set.fold insertPredicate (MapSet.empty, [])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinsertPredicate :: PropertyT -> (PredMap, [Named (FORMULA f)]) -> (PredMap, [Named (FORMULA f)])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinsertPredicate prop (predM, form) =
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari sort1 = stringToId $ name $ sourceType prop
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari sort2 = stringToId $ name $ targetType prop
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari pname1 = stringToId $ targetRole prop
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari ptype1 = PredType $ sort1 : [sort2]
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari pname2 = stringToId $ sourceRole prop
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari ptype2 = PredType $ sort2 : [sort1]
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari nam = "equiv_" ++ targetRole prop ++ "_" ++ sourceRole prop
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder varsD = [Var_decl [mkSimpleId "x"] sort2 nullRange,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Var_decl [mkSimpleId "y"] sort1 nullRange]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (C.Predication (C.Qual_pred_name pname2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Pred_type [sort2, sort1] nullRange) nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (C.Qual_var (mkSimpleId "x") sort2 nullRange :
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [C.Qual_var (mkSimpleId "y") sort1 nullRange]) nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (C.Predication (C.Qual_pred_name pname1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Pred_type [sort1, sort2] nullRange) nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (C.Qual_var (mkSimpleId "y") sort1 nullRange :
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [C.Qual_var (mkSimpleId "x") sort2 nullRange]) nullRange)
b5c780c06889ceb5c241a6b5da7ef0663e5451caDaniel Calegari sent = Quantification Universal varsD sentRel nullRange
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- MapSet does not allows repeated elements, but predicate names can be repeated
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (this must be corrected by creating a more complex ID) -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if sourceRole prop == "_"
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari then (MapSet.insert pname1 ptype1 predM, form)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else if targetRole prop == "_"
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari then (MapSet.insert pname2 ptype2 predM, form)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else (MapSet.insert pname1 ptype1 $ MapSet.insert pname2 ptype2 predM,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder makeNamed nam sent : form)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarigetOperations :: Map.Map String TypeClass -> OpMap
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetOperations ops = foldr insertOperations MapSet.empty (Map.toList ops)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinsertOperations :: (String, TypeClass) -> OpMap -> OpMap
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinsertOperations (na, tc) opM =
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari opName = stringToId na
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari opType = OpType Total [] (stringToId $ name tc)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari MapSet.insert opName opType opM
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSentencesRels :: Set.Set LinkT -> Map.Map String TypeClass ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [Named CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSentencesRels = completenessOfRelations
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercompletenessOfRelations :: Set.Set LinkT -> Map.Map String TypeClass ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [Named CASLFORMULA]
b767e7055b5ef62c990a111ac0524500592f8781Daniel CalegaricompletenessOfRelations linkk ops =
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari let ordLinks = getLinksByProperty linkk
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in foldr ((++) . createComplFormula ops) [] (Map.toList ordLinks)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercreateComplFormula :: Map.Map String TypeClass -> (String, [LinkT]) ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [Named CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercreateComplFormula ops (nam, linksL) =
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari varA = mkSimpleId "x"
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari varB = mkSimpleId "y"
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari case linksL of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder LinkT _ _ pr : _ ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let sorA = stringToId $ name $ sourceType pr
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sorB = stringToId $ name $ targetType pr
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder varsD = [Var_decl [varA] sorA nullRange,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Var_decl [varB] sorB nullRange]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sent = C.Relation (C.Predication (C.Qual_pred_name
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (stringToId $ targetRole pr) (Pred_type [sorA, sorB] nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nullRange) (C.Qual_var varA sorA nullRange :
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [C.Qual_var varB sorB nullRange]) nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (foldr ((:) . getPropHold ops varA sorA varB sorB) [] linksL)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nullRange) nullRange
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sentQuan = Quantification Universal varsD sent nullRange
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in [makeNamed ("compRel_" ++ nam) sentQuan]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetPropHold :: Map.Map String TypeClass -> VAR -> SORT -> VAR -> SORT -> LinkT
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetPropHold ops varA sorA varB sorB lin =
b767e7055b5ef62c990a111ac0524500592f8781Daniel Calegari souObj = Map.lookup (sourceVar lin) ops
b767e7055b5ef62c990a111ac0524500592f8781Daniel Calegari tarObj = Map.lookup (targetVar lin) ops
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder typSou = case souObj of
b767e7055b5ef62c990a111ac0524500592f8781Daniel Calegari Nothing -> sourceVar lin -- if happens then is an error
b767e7055b5ef62c990a111ac0524500592f8781Daniel Calegari Just tSou -> name tSou
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder typTar = case tarObj of
b767e7055b5ef62c990a111ac0524500592f8781Daniel Calegari Nothing -> targetVar lin -- if happens then is an error
b767e7055b5ef62c990a111ac0524500592f8781Daniel Calegari Just tTar -> name tTar
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder eqA = Equation (Qual_var varA sorA nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Application (Qual_op_name (stringToId (sourceVar lin))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Op_type Total [] (stringToId typSou) nullRange)
b767e7055b5ef62c990a111ac0524500592f8781Daniel Calegari nullRange) [] nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder eqB = Equation (Qual_var varB sorB nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Application (Qual_op_name (stringToId (targetVar lin))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Op_type Total [] (stringToId typTar) nullRange)
b767e7055b5ef62c990a111ac0524500592f8781Daniel Calegari nullRange) [] nullRange)
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari Junction Con (eqA : [eqB]) nullRange
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel CalegarigetLinksByProperty :: Set.Set LinkT -> Map.Map String [LinkT]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetLinksByProperty linkk =
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari let elems = Set.elems linkk
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in foldr getByProperty Map.empty elems
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel CalegarigetByProperty :: LinkT -> Map.Map String [LinkT] -> Map.Map String [LinkT]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetByProperty lin mapL =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nameLook = sourceRole prope ++ name (sourceType prope) ++ targetRole prope
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ name (targetType prope)
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari setProp = Map.lookup nameLook mapL
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari case setProp of
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari Nothing -> Map.insert nameLook [lin] (Map.delete nameLook mapL)
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari Just s -> Map.insert nameLook (lin : s) (Map.delete nameLook mapL)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSortGen :: Rel.Rel TypeClass -> Set.Set TypeClass -> Set.Set TypeClass ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.Map String TypeClass -> [Named CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSortGen typpR absCl typCl inst = disjointEmbedding absCl typpR ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sortGeneration inst ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sortGenerationNonAbstractSuperClasses typpR typCl absCl inst
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel Calegari-- Free type of non-abstract superclasses
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersortGenerationNonAbstractSuperClasses :: Rel.Rel TypeClass -> Set.Set TypeClass
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Set.Set TypeClass -> Map.Map String TypeClass -> [Named CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersortGenerationNonAbstractSuperClasses typpR typCl absCl inst =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ordObj = foldr orderByClass Map.empty (Map.toList inst)
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari nonAbsClasses = getNonAbstractClasess absCl typCl
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nonAbsClassesWChilds = filter (not . null . snd)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Set.fold ((:) . getSubClasses typpR) [] nonAbsClasses)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder childObjects = foldr ((:) . getClassSubObjects ordObj)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [] nonAbsClassesWChilds -- [(TypeClass,[String])]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder foldr ((:) . toSortConstraintNonAbsClass inst) [] childObjects
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari-- Takes the objects, and a class with its child classes and returns the descendent objects of such class
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetClassSubObjects :: Map.Map TypeClass [String] -> (TypeClass, [TypeClass]) ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (TypeClass, [String])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetClassSubObjects objs (tc, subCl) =
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari let objTC = findObjectInMap objs tc
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (tc, objTC ++ foldr ((++) . findObjectInMap objs) [] subCl)
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel CalegarifindObjectInMap :: Map.Map TypeClass [String] -> TypeClass -> [String]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfindObjectInMap objs tc = fromMaybe [] $ Map.lookup tc objs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetNonAbstractClasess :: Set.Set TypeClass -> Set.Set TypeClass -> Set.Set TypeClass
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel CalegarigetNonAbstractClasess absCl classes = Set.difference classes absCl
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSubClasses :: Rel.Rel TypeClass -> TypeClass -> (TypeClass, [TypeClass])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSubClasses typpR tc =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let subCla = map fst (filter (isParent tc) (Rel.toList typpR))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder rec = foldr ((++) . snd . getSubClasses typpR) [] subCla
bf8877d598d8afb4892e6b8f9e5abd77f3230ccaDaniel Calegari in (tc, subCla ++ rec)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederisParent :: TypeClass -> (TypeClass, TypeClass) -> Bool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederisParent tc (_, tc2) = tc == tc2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertoSortConstraintNonAbsClass :: Map.Map String TypeClass -> (TypeClass, [String])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Named CASLFORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertoSortConstraintNonAbsClass inst (tc, lisObj) =
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari sor = stringToId $ name tc
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder varA = Var_decl [mkSimpleId "x"] sor nullRange
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sent = Junction Dis (foldr ((:) . getEqualityVarObject sor inst)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [] lisObj) nullRange
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari constr = Quantification Universal [varA] sent nullRange
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari makeNamed ("sortGenCon_" ++ name tc) constr
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel CalegarigetEqualityVarObject :: SORT -> Map.Map String TypeClass -> String -> CASLFORMULA
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel CalegarigetEqualityVarObject sor inst obj =
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari let oTyp = case Map.lookup obj inst of
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari Nothing -> stringToId obj -- If happens, there is an error
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari Just ob -> stringToId $ name ob
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Equation (Qual_var (mkSimpleId "x") sor nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Application (Qual_op_name (stringToId obj)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Op_type Total [] oTyp nullRange)
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari nullRange) [] nullRange)
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari-- Sorts are generated as a free type of object functions
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersortGeneration :: Map.Map String TypeClass -> [Named CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersortGeneration inst =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ordObj = foldr orderByClass Map.empty (Map.toList inst)
7e9757ba2f41c4ac30634a4a1f1d87a042e37c45Daniel Calegari noJunk = foldr ((:) . toSortConstraint) [] (Map.toList ordObj)
7e9757ba2f41c4ac30634a4a1f1d87a042e37c45Daniel CalegarimapFilterJust :: [Maybe a] -> [a]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapFilterJust list =
7e9757ba2f41c4ac30634a4a1f1d87a042e37c45Daniel Calegari a : rest -> case a of
7e9757ba2f41c4ac30634a4a1f1d87a042e37c45Daniel Calegari Nothing -> mapFilterJust rest
7e9757ba2f41c4ac30634a4a1f1d87a042e37c45Daniel Calegari Just el -> el : mapFilterJust rest
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederorderByClass :: (String, TypeClass) -> Map.Map TypeClass [String] ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.Map TypeClass [String]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederorderByClass (ob, tc) mapTC =
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari case Map.lookup tc mapTC of
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari Nothing -> Map.insert tc [ob] mapTC
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari Just listObj -> Map.insert tc (ob : listObj) (Map.delete tc mapTC)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetNoConfusionBetweenSets :: Map.Map String TypeClass -> Rel.Rel TypeClass ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [Named CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetNoConfusionBetweenSets inst relC =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let ordObj = Map.toList $ foldr orderByClass Map.empty (Map.toList inst)
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari in mapFilterJust $ foldr ((:) . getNoConfusionBSetsAxiom ordObj relC) [] ordObj
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetNoConfusionBSetsAxiom :: [(TypeClass, [String])] -> Rel.Rel TypeClass ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (TypeClass, [String]) -> Maybe (Named CASLFORMULA)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetNoConfusionBSetsAxiom ordObj relC (tc, lisObj) =
7e9757ba2f41c4ac30634a4a1f1d87a042e37c45Daniel Calegari case lisObj of
7e9757ba2f41c4ac30634a4a1f1d87a042e37c45Daniel Calegari [] -> Nothing
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let filteredObj = removeUntilType tc ordObj
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder diffForm = foldr ((++) . diffOfRestConstants (tc, lisObj) relC)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [] filteredObj in
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari case diffForm of
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari [] -> Nothing
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari _ : _ -> let constr = Junction Con diffForm nullRange
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari in Just $ makeNamed ("noConfusion_" ++ name tc) constr
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel CalegariremoveUntilType :: TypeClass -> [(TypeClass, [String])] -> [(TypeClass, [String])]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederremoveUntilType tc lis =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (tc2, lisObj2) : rest -> if tc == tc2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then (tc2, lisObj2) : rest
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari else removeUntilType tc rest
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdiffOfRestConstants :: (TypeClass, [String]) -> Rel.Rel TypeClass ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (TypeClass, [String]) -> [CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdiffOfRestConstants (tc1, lisObj1) relC (tc2, lisObj2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | tc1 == tc2 = foldr ((++) . diffOfRestOps tc1 lisObj1) [] lisObj1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | haveCommonSort tc1 tc2 relC =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder concatMap (diffOfRestOpsDiffSort (tc1, lisObj1) tc2) lisObj2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | otherwise = []
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel CalegarihaveCommonSort :: TypeClass -> TypeClass -> Rel.Rel TypeClass -> Bool
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel CalegarihaveCommonSort t1 t2 relT =
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari let succT1 = superSorts relT t1
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari succT2 = superSorts relT t2
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari in not $ Set.null $ Set.intersection succT1 succT2
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari-- This is the non exported function reachable in Rel
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel CalegarisuperSorts :: Rel.Rel TypeClass -> TypeClass -> Set.Set TypeClass
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel CalegarisuperSorts relT tc = Set.fold reach Set.empty $ Rel.succs relT tc where
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari reach e s = if Set.member e s then s
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel Calegari else Set.fold reach (Set.insert e s) $ Rel.succs relT e
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel CalegaridiffOfRestOpsDiffSort :: (TypeClass, [String]) -> TypeClass -> String -> [CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdiffOfRestOpsDiffSort (tc1, lisObj1) tc2 objName = concatMap
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (diffOpsDiffSorts tc2 objName tc1) lisObj1
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel CalegaridiffOpsDiffSorts :: TypeClass -> String -> TypeClass -> String -> [CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdiffOpsDiffSorts tc2 objName2 tc1 objName1 =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [Negation (Equation (Application (Qual_op_name (stringToId objName1)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Op_type Total [] (stringToId $ name tc1) nullRange) nullRange) [] nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Strong (Application (Qual_op_name (stringToId objName2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Op_type Total [] (stringToId $ name tc2) nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nullRange) [] nullRange) nullRange) nullRange]
7e9757ba2f41c4ac30634a4a1f1d87a042e37c45Daniel CalegaridiffOfRestOps :: TypeClass -> [String] -> String -> [CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdiffOfRestOps tc lisObj objName =
50fe6868628ed8933eb21bcd8518a430e6a78ff7Daniel Calegari let lis = removeUntil lisObj objName
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in concatMap (diffOps tc objName) lis
50fe6868628ed8933eb21bcd8518a430e6a78ff7Daniel CalegariremoveUntil :: [String] -> String -> [String]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederremoveUntil lis str =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder a : rest -> if a == str
50fe6868628ed8933eb21bcd8518a430e6a78ff7Daniel Calegari else removeUntil rest str
7e9757ba2f41c4ac30634a4a1f1d87a042e37c45Daniel CalegaridiffOps :: TypeClass -> String -> String -> [CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdiffOps tc objName1 objName2 =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [Negation (Equation
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Application (Qual_op_name (stringToId objName1)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Op_type Total [] (stringToId $ name tc) nullRange)
7e9757ba2f41c4ac30634a4a1f1d87a042e37c45Daniel Calegari nullRange) [] nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Application (Qual_op_name (stringToId objName2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Op_type Total [] (stringToId $ name tc) nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nullRange) [] nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nullRange | objName1 /= objName2]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertoSortConstraint :: (TypeClass, [String]) -> Named CASLFORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertoSortConstraint (tc, lisObj) =
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari sor = stringToId $ name tc
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari simplCon = Constraint sor (foldr ((:) . toConstraint sor) [] lisObj) sor
eae727f2a1203f1e3c86e40667fe6dfb1173abcbcmaeder constr = mkSort_gen_ax [simplCon] True
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari makeNamed ("sortGenCon_" ++ name tc) constr
f3a838d9e2932da421939f348a2c3d31ded88989Daniel CalegaritoConstraint :: Id -> String -> (OP_SYMB, [Int])
f3a838d9e2932da421939f348a2c3d31ded88989Daniel CalegaritoConstraint sor obName =
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari let obj = stringToId obName
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Qual_op_name obj (Op_type Total [] sor nullRange) nullRange, [])
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari-- Each abstract class is the disjoint embedding of it subsorts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdisjointEmbedding :: Set.Set TypeClass -> Rel.Rel TypeClass ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [Named CASLFORMULA]
28f6f14c76163be14b8df1e532653c5aabb5bf2eDaniel CalegaridisjointEmbedding absCl rel =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder injSyms = map (\ (s, t) -> (Qual_op_name
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (mkUniqueInjName (stringToId $ name s) (stringToId $ name t))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Op_type Total [stringToId $ name s]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (stringToId $ name t) nullRange) nullRange, [])) $ Rel.toList $
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder resType _ (Op_name _, _) = False
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder resType s (Qual_op_name _ t _, _) = res_OP_TYPE t == s
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder collectOps s = Constraint (stringToId $ name s)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (filter (resType (stringToId $ name s)) injSyms) (stringToId $ name s)
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari sortList = Set.toList absCl
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari constrs = map collectOps sortList
cba1bca86fce751bb0dc758f4a7e43ff95640137Daniel Calegari [makeNamed "disjEmbedd" (Sort_gen_ax constrs True)]
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarimapSen :: CASLSign -> CSMOF.Sen -> CASLFORMULA
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarimapSen sig (Sen con car cot) = -- trueForm
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari minC = minConstraint con car (predMap sig)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari maxC = maxConstraint con car (predMap sig)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari Junction Con (minC : [maxC]) nullRange
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari LEQ -> maxConstraint con car (predMap sig)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari GEQ -> minConstraint con car (predMap sig)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegariminConstraint :: MultConstr -> Integer -> PredMap -> CASLFORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederminConstraint con int predM =
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari predTypes = MapSet.lookup (stringToId $ getRole con) predM -- Set PredType
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari souVars = generateVars "x" 1
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari tarVars = generateVars "y" int
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari correctPredType = Set.fold (getCorrectPredType con) [] predTypes
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari souVarDec = Var_decl souVars (head (predArgs (head correctPredType))) nullRange
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari tarVarDec = Var_decl tarVars (last (predArgs (head correctPredType))) nullRange
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then Quantification Universal [souVarDec] (Quantification
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Existential [tarVarDec] (Junction Con (generateVarDiff tarVarDec :
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [generateProp souVarDec tarVarDec (stringToId $ getRole con)])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nullRange) nullRange) nullRange
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Quantification Universal [souVarDec] (Quantification
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Existential [tarVarDec] (generateProp souVarDec tarVarDec
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (stringToId $ getRole con)) nullRange) nullRange
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel CalegarigetCorrectPredType :: MultConstr -> PredType -> [PredType] -> [PredType]
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel CalegarigetCorrectPredType con pt ptLis =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if stringToId (name (CSMOF.getType con)) == head (predArgs pt)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then pt : ptLis else ptLis
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarigenerateVars :: String -> Integer -> [VAR]
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarigenerateVars varRoot int =
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari 1 -> [mkSimpleId (varRoot ++ "_" ++ show int)]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder n -> mkSimpleId (varRoot ++ "_" ++ show int) : generateVars varRoot (n - 1)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarigenerateVarDiff :: VAR_DECL -> CASLFORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenerateVarDiff (Var_decl vars sor _) = Junction Con
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (foldr ((++) . diffOfRest sor vars) [] vars) nullRange
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegaridiffOfRest :: SORT -> [VAR] -> VAR -> [CASLFORMULA]
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegaridiffOfRest sor vars var = map (diffVar sor var) vars
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegaridiffVar :: SORT -> VAR -> VAR -> CASLFORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdiffVar sor var1 var2 =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if var1 /= var2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then Negation (Equation
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Qual_var var1 sor nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Qual_var var2 sor nullRange)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari else trueForm
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarigenerateProp :: VAR_DECL -> VAR_DECL -> Id -> CASLFORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenerateProp (Var_decl varD sort _) (Var_decl varD2 sort2 _) rol =
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari Junction Con (map (createPropRel (head varD) sort rol sort2) varD2) nullRange
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegaricreatePropRel :: VAR -> SORT -> Id -> SORT -> VAR -> CASLFORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercreatePropRel souVar sor rol sor2 tarVar =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Predication (C.Qual_pred_name rol (Pred_type [sor, sor2] nullRange) nullRange)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Qual_var souVar sor nullRange : [Qual_var tarVar sor2 nullRange]) nullRange
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarimaxConstraint :: MultConstr -> Integer -> PredMap -> CASLFORMULA
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermaxConstraint con int predM =
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari predTypes = MapSet.lookup (stringToId $ getRole con) predM -- Set PredType
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari souVars = generateVars "x" 1
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari tarVars = generateVars "y" (int + 1)
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari correctPredType = Set.fold (getCorrectPredType con) [] predTypes
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari souVarDec = Var_decl souVars (head (predArgs (head correctPredType))) nullRange
6d24e3b0fdf91413ff58265a93fd4fc08be8b950Daniel Calegari tarVarDec = Var_decl tarVars (last (predArgs (head correctPredType))) nullRange
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Quantification Universal (souVarDec : [tarVarDec])
f3a838d9e2932da421939f348a2c3d31ded88989Daniel Calegari (Junction Con [generateProp souVarDec tarVarDec (stringToId $ getRole con)] nullRange)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari (Junction Dis (generateExEqual tarVarDec) nullRange)
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarigenerateExEqual :: VAR_DECL -> [CASLFORMULA]
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarigenerateExEqual (Var_decl varD sor _) = generateExEqualList varD sor
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarigenerateExEqualList :: [VAR] -> SORT -> [CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenerateExEqualList vars sor =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder v : rest -> generateExEqualVar rest sor v ++ generateExEqualList rest sor
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarigenerateExEqualVar :: [VAR] -> SORT -> VAR -> [CASLFORMULA]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergenerateExEqualVar vars sor var =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder foldr ((++) . (\ el -> if el == var
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else [Equation (Qual_var var sor nullRange) Strong
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Qual_var el sor nullRange) nullRange]))
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari-- | Translation of morphisms
cebd8658147937d53195664ad8b1e37de1e6f017Daniel CalegarimapMor :: CSMOF.Morphism -> Result CASLMor
b5c780c06889ceb5c241a6b5da7ef0663e5451caDaniel CalegarimapMor m = return C.Morphism
b5c780c06889ceb5c241a6b5da7ef0663e5451caDaniel Calegari { msource = mapSign $ domOfDefaultMorphism m
b5c780c06889ceb5c241a6b5da7ef0663e5451caDaniel Calegari , mtarget = mapSign $ codOfDefaultMorphism m
cebd8658147937d53195664ad8b1e37de1e6f017Daniel Calegari , extended_map = ()