545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh

fd9abdda70912b99b24e3bf1a38f26fde908a74cndmodule Maude.PreComorphism where

fd9abdda70912b99b24e3bf1a38f26fde908a74cnd

fd9abdda70912b99b24e3bf1a38f26fde908a74cndimport Data.Maybe

545f1a3ee91056d6de32adab10c2eab26db89f27dpejeshimport qualified Data.List as List

545f1a3ee91056d6de32adab10c2eab26db89f27dpejeshimport qualified Data.Set as Set

545f1a3ee91056d6de32adab10c2eab26db89f27dpejeshimport qualified Data.Map as Map

5a58787efeb02a1c3f06569d019ad81fd2efa06end

96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletcimport qualified Maude.Sign as MSign

7add1372edb1ee95a2c4d1314df4c7567bda7c62jimimport qualified Maude.Sentence as MSentence

7add1372edb1ee95a2c4d1314df4c7567bda7c62jimimport qualified Maude.Morphism as MMorphism

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenimport qualified Maude.AS_Maude as MAS

2e545ce2450a9953665f701bb05350f0d3f26275ndimport qualified Maude.Symbol as MSym

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenimport Maude.Meta.HasName

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

7add1372edb1ee95a2c4d1314df4c7567bda7c62jimimport qualified CASL.Sign as CSign

5a58787efeb02a1c3f06569d019ad81fd2efa06endimport qualified CASL.Morphism as CMorphism

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowenimport qualified CASL.AS_Basic_CASL as CAS

3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport CASL.StaticAna

7add1372edb1ee95a2c4d1314df4c7567bda7c62jim

7add1372edb1ee95a2c4d1314df4c7567bda7c62jimimport Common.Id

5a58787efeb02a1c3f06569d019ad81fd2efa06endimport Common.Result

3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport Common.AS_Annotation

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport qualified Common.Lib.Rel as Rel

7add1372edb1ee95a2c4d1314df4c7567bda7c62jim

7add1372edb1ee95a2c4d1314df4c7567bda7c62jimtype IdMap = Map.Map Id Id

00b49f91367894cf867206991ff1373cfeabb759gryzortype OpTransTuple = (CSign.OpMap, CSign.OpMap, [Named CAS.CASLFORMULA], Set.Set Component)

7f5b59ccc63c0c0e3e678a168f09ee6a2f51f9d0nd

e609c337f729875bc20e01096c7e610f45356f54nilgun-- | generates a CASL morphism from a Maude morphism

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungmapMorphism :: MMorphism.Morphism -> Result (CMorphism.CASLMor)

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndmapMorphism morph =

3b3b7fc78d1f5bfc2769903375050048ff41ff26nd let

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd src = MMorphism.source morph

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen tgt = MMorphism.target morph

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen mk = arrangeKinds (MSign.sorts src) (MSign.subsorts src)

c68aa7f213d409d464eaa6b963afb28678548f4frbowen cs = kindsFromMap mk

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf smap = MMorphism.sortMap morph

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen omap = MMorphism.opMap morph

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen smap' = applySortMap2CASLSorts smap cs

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen omap' = maudeOpMap2CASLOpMap mk omap

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen pmap = createPredMap mk smap

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen (src', _) = maude2casl src []

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen (tgt', _) = maude2casl tgt []

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen-- | translates the Maude morphism between operators into a CASL morpshim between

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen-- operators

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenmaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenmaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd-- | translates the mapping between two symbols representing operators into

5a58787efeb02a1c3f06569d019ad81fd2efa06end-- a CASL operators map

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowentranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen -> CMorphism.Op_map

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowentranslateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm = copm'

a56ff98d3082c853f69e8de5c3e8bcab2734c0earbowen where f = token2id . getName

30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh g = \ x -> fromJust $ Map.lookup (f x) im

7add1372edb1ee95a2c4d1314df4c7567bda7c62jim ot = CSign.OpType CAS.Total (map g ar) (g co)

5a58787efeb02a1c3f06569d019ad81fd2efa06end cop = (token2id from, ot)

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen to' = (token2id to, CAS.Total)

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd copm' = Map.insert cop to' copm

c68aa7f213d409d464eaa6b963afb28678548f4frbowentranslateOpMapEntry _ _ _ _ = Map.empty

c68aa7f213d409d464eaa6b963afb28678548f4frbowen

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen-- | generates a set of CASL symbol from a Maude Symbol

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfmapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenmapSymbol sg (MSym.Sort q) = Set.singleton csym

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

4aa603e6448b99f9371397d439795c91a93637eand sym_id = token2id q

c3c006c28c5b03892ccaef6e4d2cbb15a13a2072rbowen kind = fromJust $ Map.lookup sym_id mk

c3c006c28c5b03892ccaef6e4d2cbb15a13a2072rbowen pred_data = CSign.PredType [kind]

c3c006c28c5b03892ccaef6e4d2cbb15a13a2072rbowen csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data

4aa603e6448b99f9371397d439795c91a93637eandmapSymbol sg (MSym.Operator q ar co) = Set.singleton csym

c3c006c28c5b03892ccaef6e4d2cbb15a13a2072rbowen where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd q' = token2id q

c68aa7f213d409d464eaa6b963afb28678548f4frbowen ar' = map (maudeSort2caslId mk) ar

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd co' = token2id $ getName co

20f499565e77defe9dab24dd85c02f38a1175855nd op_data = CSign.OpType CAS.Total ar' co'

c3c006c28c5b03892ccaef6e4d2cbb15a13a2072rbowen csym = CSign.Symbol q' $ CSign.OpAsItemType op_data

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4ndmapSymbol _ _ = Set.empty

4126704c4950bfd46d32ad54e3b106ac6d868a73sf

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd-- | returns the sort in CASL of the Maude sort symbol

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenmaudeSort2caslId :: IdMap -> MSym.Symbol -> Id

4126704c4950bfd46d32ad54e3b106ac6d868a73sfmaudeSort2caslId im sym = fromJust $ Map.lookup (token2id $ getName sym) im

4126704c4950bfd46d32ad54e3b106ac6d868a73sf

4126704c4950bfd46d32ad54e3b106ac6d868a73sf-- | creates the predicate map for the CASL morphism from the Maude sort map and

4126704c4950bfd46d32ad54e3b106ac6d868a73sf-- the map between sorts and kinds

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowencreatePredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4ndcreatePredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen-- | creates an entry of the predicate map for a single sort

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowencreatePredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen -> CMorphism.Pred_map

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowencreatePredMap4sort im from to m = Map.insert key id_to m

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen where id_from = token2id $ getName from

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen id_to = token2id $ getName to

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd kind = fromJust $ Map.lookup id_from im

00b49f91367894cf867206991ff1373cfeabb759gryzor key = (id_from, CSign.PredType [kind])

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen-- | computes the sort morphism of CASL from the sort morphism in Maude and the set

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd-- of kinds

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenapplySortMap2CASLSorts :: MMorphism.SortMap -> Set.Set Id -> CMorphism.Sort_map

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenapplySortMap2CASLSorts sm = Set.fold (applySortMap2CASLSort sm) Map.empty

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen-- | computes the morphism for a single kind

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenapplySortMap2CASLSort :: MMorphism.SortMap -> Id -> CMorphism.Sort_map -> CMorphism.Sort_map

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenapplySortMap2CASLSort sm sort csm = new_csm

157312a2bcbad225c12462fc6d74b1aa3f32dceehumbedooh where toks = getTokens sort

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen new_toks = map (rename sm) toks

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd new_sort = mkId new_toks

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh new_csm = if new_sort == sort

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen then csm

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen else Map.insert sort new_sort csm

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh-- | renames the sorts in a given kind

545f1a3ee91056d6de32adab10c2eab26db89f27dpejeshrename :: MMorphism.SortMap -> Token -> Token

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenrename sm tok = new_tok

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen where sym = MSym.Sort tok

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh sym' = if Map.member sym sm

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen then fromJust $ Map.lookup sym sm

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh else sym

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh new_tok = getName sym'

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen-- | translates a Maude sentence into a CASL formula

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenmapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenmapSentence sg sen@(MSentence.Equation eq) = case any MAS.owise ats of

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen False -> return $ sentence $ noOwiseSen2Formula mk named

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen True -> let

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen (no_owise_sens, _, _) = splitOwiseEqs sg_sens

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen trans = sentence $ owiseSen2Formula mk no_owise_forms named

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen in return trans

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen MAS.Eq _ _ _ ats = eq

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen named = makeNamed "" sen

00b49f91367894cf867206991ff1373cfeabb759gryzormapSentence sg sen@(MSentence.Membership mb) = return $ sentence form

00b49f91367894cf867206991ff1373cfeabb759gryzor where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh MAS.Mb _ _ _ _ = mb

7add1372edb1ee95a2c4d1314df4c7567bda7c62jim named = makeNamed "" sen

5a58787efeb02a1c3f06569d019ad81fd2efa06end form = mb_rl2formula mk named

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenmapSentence sg sen@(MSentence.Rule rl) = return $ sentence form

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen MAS.Rl _ _ _ _ = rl

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen named = makeNamed "" sen

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen form = mb_rl2formula mk named

157312a2bcbad225c12462fc6d74b1aa3f32dceehumbedooh

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen-- | applies maude2casl to compute the CASL signature and sentences from

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd-- the Maude ones, and wraps them into a Result datatype

545f1a3ee91056d6de32adab10c2eab26db89f27dpejeshmapTheory :: (MSign.Sign, [Named MSentence.Sentence])

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh -> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])

545f1a3ee91056d6de32adab10c2eab26db89f27dpejeshmapTheory (sg, nsens) = return $ maude2casl sg nsens

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh-- | computes new signature and sentences of CASL associated to the

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh-- given Maude signature and sentences

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4ndmaude2casl :: MSign.Sign -> [Named MSentence.Sentence]

4aa603e6448b99f9371397d439795c91a93637eand -> (CSign.CASLSign, [Named CAS.CASLFORMULA])

bbcc277fef0330ac4c1f937cb0dea78248225c0ahumbedoohmaude2casl msign nsens = (csign { CSign.sortSet = cs,

bbcc277fef0330ac4c1f937cb0dea78248225c0ahumbedooh CSign.emptySortSet = cs,

4aa603e6448b99f9371397d439795c91a93637eand CSign.opMap = cops',

9e213c30f8f58680f0350736a2a6221baad94131humbedooh CSign.assocOps = assoc_ops,

aaf7b7f4cc1be050310c3d7f48bce0ec67e174e4nd CSign.predMap = preds,

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh CSign.declaredSymbols = syms }, new_sens)

db99fa79ac42b9cc42b63386eb289aecb0f3cb9cnd where csign = CSign.emptySign ()

545f1a3ee91056d6de32adab10c2eab26db89f27dpejesh mk' = arrangeKinds (MSign.sorts msign) (MSign.subsorts msign)

bf082801b4063fe22a99661889cbd9a7701dae9fnd cs = kindsFromMap mk'

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen mk = Map.insert (token2id $ mkSimpleId "Universal") (token2id $ mkSimpleId "[Universal]") mk'

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen ks = kindPredicates mk

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf rp = rewPredicates ks cs

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf rs = rewPredicatesSens cs

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen ops = MSign.ops msign

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen ksyms = kinds2syms cs

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen (cops, assoc_ops, ops_forms, comps) = translateOps mk ops

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen ctor_sen = [ctorSen False (cs, Rel.empty, comps)]

a56ff98d3082c853f69e8de5c3e8bcab2734c0earbowen cops' = predefinedOps cs cops

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen ops_syms = ops2symbols cops

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen preds = Map.unionWith (Set.union) ks rp

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen preds_syms = preds2syms preds

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen syms = Set.union ksyms $ Set.union ops_syms preds_syms

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen new_sens = concat [rs, ops_forms, no_owise_forms, owise_forms, mb_rl_forms, ctor_sen]

e9425c93ba098a7844e138a61e1be5f46d2aa2ddnd

4aa603e6448b99f9371397d439795c91a93637eandpredefinedOps :: Set.Set Id -> CSign.OpMap -> CSign.OpMap

9e213c30f8f58680f0350736a2a6221baad94131humbedoohpredefinedOps kinds om = Set.fold predefinedOpKind om'' kinds

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen where if_id = token2id $ mkSimpleId "if_then_else_fi"

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen double_eq_id = token2id $ mkSimpleId "_==_"

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen neg_double_eq_id = token2id $ mkSimpleId "_=/=_"

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen om' = Map.delete double_eq_id $ Map.delete if_id om

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen om'' = Map.delete neg_double_eq_id om'

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenpredefinedOpKind :: Id -> CSign.OpMap -> CSign.OpMap

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowenpredefinedOpKind kind om = om3

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen where if_id = token2id $ mkSimpleId "if_then_else_fi"

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen double_eq_id = token2id $ mkSimpleId "_==_"

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen neg_double_eq_id = token2id $ mkSimpleId "_=/=_"

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen bool_id = token2id $ mkSimpleId "[Bool]"

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen if_opt = Set.singleton $ CSign.OpType CAS.Total [bool_id, kind, kind] kind

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen eq_opt = Set.singleton $ CSign.OpType CAS.Total [kind, kind] bool_id

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf om1 = Map.insertWith Set.union if_id if_opt om

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen om2 = Map.insertWith Set.union double_eq_id eq_opt om1

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen om3 = Map.insertWith Set.union neg_double_eq_id eq_opt om2

c35acdcbd4d173d3c536cf0be1295fa6c510cf8drbowen

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndpredefinedSens :: Set.Set Id -> [Named CAS.CASLFORMULA]

7add1372edb1ee95a2c4d1314df4c7567bda7c62jimpredefinedSens = Set.fold predefinedSensKind []

7add1372edb1ee95a2c4d1314df4c7567bda7c62jim

00b49f91367894cf867206991ff1373cfeabb759gryzorpredefinedSensKind :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

7f5b59ccc63c0c0e3e678a168f09ee6a2f51f9d0ndpredefinedSensKind kind acc = concat [iss, eqs, neqs, psen, acc]

e609c337f729875bc20e01096c7e610f45356f54nilgun where iss = ifSens kind

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung eqs = equalitySens kind

727872d18412fc021f03969b8641810d8896820bhumbedooh neqs = nonEqualitySens kind

0d0ba3a410038e179b695446bb149cce6264e0abnd psen = plusSen

727872d18412fc021f03969b8641810d8896820bhumbedooh

cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedoohifSens :: Id -> [Named CAS.CASLFORMULA]

0d0ba3a410038e179b695446bb149cce6264e0abndifSens kind = [form'', neg_form'']

cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh where v1 = newVarIndex 1 kind

727872d18412fc021f03969b8641810d8896820bhumbedooh v2 = newVarIndex 2 kind

0d0ba3a410038e179b695446bb149cce6264e0abnd bv = newVarIndex 2 $ token2id $ mkSimpleId "[Bool]"

0d0ba3a410038e179b695446bb149cce6264e0abnd true_id = CAS.Op_name $ token2id $ mkSimpleId "true"

0d0ba3a410038e179b695446bb149cce6264e0abnd true_term = CAS.Application true_id [] nullRange

ac082aefa89416cbdc9a1836eaf3bed9698201c8humbedooh if_id = CAS.Op_name $ token2id $ mkSimpleId "if_then_else_fi"

0d0ba3a410038e179b695446bb149cce6264e0abnd if_term = CAS.Application if_id [bv, v1, v2] nullRange

0d0ba3a410038e179b695446bb149cce6264e0abnd prem = CAS.Strong_equation bv true_term nullRange

0d0ba3a410038e179b695446bb149cce6264e0abnd concl = CAS.Strong_equation if_term v1 nullRange

727872d18412fc021f03969b8641810d8896820bhumbedooh form = CAS.Implication prem concl True nullRange

0d0ba3a410038e179b695446bb149cce6264e0abnd form' = quantifyUniversally form

0d0ba3a410038e179b695446bb149cce6264e0abnd neg_prem = CAS.Negation prem nullRange

30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh neg_concl = CAS.Strong_equation if_term v2 nullRange

205f749042ed530040a4f0080dbcb47ceae8a374rjung neg_form = CAS.Implication neg_prem neg_concl True nullRange

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen neg_form' = quantifyUniversally neg_form

0d0ba3a410038e179b695446bb149cce6264e0abnd name1 = show kind ++ "_if_true"

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd name2 = show kind ++ "_if_false"

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd form'' = makeNamed name1 form'

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd neg_form'' = makeNamed name2 neg_form'

5a58787efeb02a1c3f06569d019ad81fd2efa06end

equalitySens :: Id -> [Named CAS.CASLFORMULA]

equalitySens kind = [form'', comp_form'']

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

true_id = CAS.Op_name $ token2id $ mkSimpleId "true"

true_term = CAS.Application true_id [] nullRange

false_id = CAS.Op_name $ token2id $ mkSimpleId "false"

false_term = CAS.Application false_id [] nullRange

prem = CAS.Strong_equation v1 v2 nullRange

double_eq_id = CAS.Op_name $ token2id $ mkSimpleId "_==_"

double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange

concl = CAS.Strong_equation double_eq_term true_term nullRange

form = CAS.Implication prem concl True nullRange

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

new_concl = CAS.Strong_equation double_eq_term false_term nullRange

comp_form = CAS.Implication neg_prem new_concl True nullRange

comp_form' = quantifyUniversally comp_form

name1 = show kind ++ "_==_true"

name2 = show kind ++ "_==_false"

form'' = makeNamed name1 form'

comp_form'' = makeNamed name2 comp_form'

nonEqualitySens :: Id -> [Named CAS.CASLFORMULA]

nonEqualitySens kind = [form'', comp_form'']

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

true_id = CAS.Op_name $ token2id $ mkSimpleId "true"

true_term = CAS.Application true_id [] nullRange

false_id = CAS.Op_name $ token2id $ mkSimpleId "false"

false_term = CAS.Application false_id [] nullRange

prem = CAS.Strong_equation v1 v2 nullRange

double_eq_id = CAS.Op_name $ token2id $ mkSimpleId "_=/=_"

double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange

concl = CAS.Strong_equation double_eq_term false_term nullRange

form = CAS.Implication prem concl True nullRange

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

new_concl = CAS.Strong_equation double_eq_term true_term nullRange

comp_form = CAS.Implication neg_prem new_concl True nullRange

comp_form' = quantifyUniversally comp_form

name1 = show kind ++ "_=/=_false"

name2 = show kind ++ "_=/=_true"

form'' = makeNamed name1 form'

comp_form'' = makeNamed name2 comp_form'

plusSen :: [Named CAS.CASLFORMULA]

plusSen = [form'']

where v1 = newVarIndex 1 $ token2id $ mkSimpleId "[Nat]"

v2 = newVarIndex 2 $ token2id $ mkSimpleId "[Nat]"

plus_id = CAS.Op_name $ token2id $ mkSimpleId "_+_"

succ_id = CAS.Op_name $ token2id $ mkSimpleId "s_"

succ_v1 = CAS.Application succ_id [v1] nullRange

lhs = CAS.Application plus_id [succ_v1, v2] nullRange

add_term = CAS.Application plus_id [v1, v2] nullRange

rhs = CAS.Application succ_id [add_term] nullRange

form = CAS.Strong_equation lhs rhs nullRange

form' = quantifyUniversally form

name = "add_+_"

form'' = makeNamed name form'

-- | translates the Maude operator map into a tuple of CASL operators, CASL

-- associative operators and the formulas generated by the operator attributes

-- and the membership induced from each Maude operator

translateOps :: IdMap -> MSign.OpMap -> OpTransTuple

translateOps im = Map.fold (translateOpDeclSet im) (Map.empty, Map.empty, [], Set.empty)

-- | translates an operator declaration set into a tern as described above

translateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple

translateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods

translateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple

translateOpDecl im (syms, ats) (ops, assoc_ops, forms, cs) = (ops', assoc_ops', forms', cs')

where predOps = ops2pred im syms

sym = head $ Set.toList syms

(cop_id, ot) = fromJust $ maudeSym2CASLOp im sym

cop_type = Set.singleton ot

forms' = forms ++ predOps

ops' = Map.insertWith (Set.union) cop_id cop_type ops

assoc_ops' = if any MAS.assoc ats

then Map.insertWith (Set.union) cop_id cop_type assoc_ops

else assoc_ops

cs' = if any MAS.ctor ats

then Set.insert (Component cop_id ot) cs

else cs

-- | translates a Maude operator symbol into a pair with the id of the operator

-- and its CASL type

maudeSym2CASLOp :: IdMap -> MSym.Symbol -> Maybe (Id, CSign.OpType)

maudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot)

where f = token2id . getName

g = \ x -> fromJust $ Map.lookup (f x) im

ot = CSign.OpType CAS.Total (map g ar) (g co)

maudeSym2CASLOp _ _ = Nothing

-- | generates the predicates associated to each operator declaration in Maude

-- due to the associated membership if the coarity is a sort and not a kind

ops2pred :: IdMap -> MSym.SymbolSet -> [Named CAS.CASLFORMULA]

ops2pred im = Set.fold (op2pred im) []

-- | generates the memebership predicate associated to an operator

op2pred :: IdMap -> MSym.Symbol -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

op2pred im (MSym.Operator op ar co) acc = case co of

MSym.Sort s -> let

op' = CAS.Op_name $ token2id op

co' = token2id s

(vars, prems) = ops2predPremises im ar 0

pred_name = CAS.Pred_name co'

op_term = CAS.Application op' vars nullRange

op_pred = CAS.Predication pred_name [op_term] nullRange

conj_form = createConjForm prems

imp_form = if null prems

then op_pred

else CAS.Implication conj_form op_pred True nullRange

q_form = quantifyUniversally imp_form

final_form = makeNamed "" q_form

in final_form : acc

_ -> acc

op2pred _ _ acc = acc

-- | creates a conjuctive formula distinguishing the size of the list

createConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA

createConjForm [] = CAS.True_atom nullRange

createConjForm [a] = a

createConjForm fs = CAS.Conjunction fs nullRange

-- | generates the predicates asserting the "true" sort of the operator if all

-- the arguments have the correct sort

ops2predPremises :: IdMap -> [MSym.Symbol] -> Int -> ([CAS.CASLTERM], [CAS.CASLFORMULA])

ops2predPremises im (MSym.Sort s : ss) i = (var : terms, form : forms)

where s' = token2id s

kind = fromJust $ Map.lookup s' im

pred_name = CAS.Pred_name s'

var = newVarIndex i kind

form = CAS.Predication pred_name [var] nullRange

(terms, forms) = ops2predPremises im ss (i + 1)

ops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)

where k' = token2id k

kind = fromJust $ Map.lookup k' im

var = newVarIndex i kind

(terms, forms) = ops2predPremises im ss (i + 1)

ops2predPremises _ _ _ = ([], [])

-- | traverses the Maude sentences, returning a pair of list of sentences.

-- The first list in the pair are the equations without the attribute "owise",

-- while the second one are the equations with this attribute

splitOwiseEqs :: [Named MSentence.Sentence] ->

([Named MSentence.Sentence], [Named MSentence.Sentence], [Named MSentence.Sentence])

splitOwiseEqs [] = ([], [], [])

splitOwiseEqs (s : ss) = res

where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss

sen = sentence s

res = case sen of

MSentence.Equation (MAS.Eq _ _ _ ats) -> case any MAS.owise ats of

True -> (no_owise_sens, s : owise_sens, mbs_rls)

False -> (s : no_owise_sens, owise_sens, mbs_rls)

_ -> (no_owise_sens, owise_sens, s : mbs_rls)

-- | translates a Maude equation defined without the "owise" attribute into

-- a CASL formula

noOwiseSen2Formula :: IdMap -> Named MSentence.Sentence

-> Named CAS.CASLFORMULA

noOwiseSen2Formula im s = s'

where MSentence.Equation eq = sentence s

sen' = noOwiseEq2Formula im eq

s' = s { sentence = sen' }

-- | translates a Maude equation defined with the "owise" attribute into

-- a CASL formula

owiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]

-> Named MSentence.Sentence -> Named CAS.CASLFORMULA

owiseSen2Formula im owise_forms s = s'

where MSentence.Equation eq = sentence s

sen' = owiseEq2Formula im owise_forms eq

s' = s { sentence = sen' }

-- | translates a Maude membership or rule into a CASL formula

mb_rl2formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA

mb_rl2formula im s = case sen of

MSentence.Membership mb -> let

mb' = mb2formula im mb

in s { sentence = mb' }

MSentence.Rule rl -> let

rl' = rl2formula im rl

in s { sentence = rl' }

_ -> makeNamed "" $ CAS.False_atom nullRange

where sen = sentence s

-- | create the CASL predicates derived from Maude subsort declarations

subsortSens :: IdMap -> [(MSym.Symbol, MSym.Symbol)] -> [CAS.CASLFORMULA]

subsortSens im = map (subsortSen im)

-- | create a CASL predicate from a Maude subsort declaration

subsortSen :: IdMap -> (MSym.Symbol, MSym.Symbol) -> CAS.CASLFORMULA

subsortSen im (sub, super) = quantifyUniversally form

where sub' = getName sub

super' = getName super

kind = fromJust $ Map.lookup (token2id sub') im

sub_pred_name = CAS.Pred_name $ token2id sub'

super_pred_name = CAS.Pred_name $ token2id super'

var = newVar kind

sub_form = CAS.Predication sub_pred_name [var] nullRange

super_form = CAS.Predication super_pred_name [var] nullRange

form = CAS.Implication sub_form super_form True nullRange

-- | generates a new variable qualified with the given number

newVarIndex :: Int -> Id -> CAS.CASLTERM

newVarIndex i sort = CAS.Qual_var var sort nullRange

where var = mkSimpleId $ "V" ++ show i

-- | generates a new variable

newVar :: Id -> CAS.CASLTERM

newVar sort = CAS.Qual_var var sort nullRange

where var = mkSimpleId "V"

-- | Id for the rew predicate

rewID :: Id

rewID = token2id $ mkSimpleId "rew"

-- | translate a Maude equation without the "owise" attribute into a CASL formula

noOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA

noOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

form = CAS.Strong_equation ct ct' nullRange

noOwiseEq2Formula im (MAS.Eq t t' conds@(_:_) _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

conds_form = conds2formula im conds

concl_form = CAS.Strong_equation ct ct' nullRange

form = CAS.Implication conds_form concl_form True nullRange

-- | transforms a Maude equation defined with the otherwise attribute into

-- a CASL formula

owiseEq2Formula :: IdMap -> [Named CAS.CASLFORMULA] -> MAS.Equation

-> CAS.CASLFORMULA

owiseEq2Formula im no_owise_form eq = form

where (eq_form, vars) = noQuantification $ noOwiseEq2Formula im eq

(op, ts, _) = fromJust $ getLeftApp eq_form

ex_form = existencialNegationOtherEqs op ts no_owise_form

imp_form = CAS.Implication ex_form eq_form True nullRange

form = CAS.Quantification CAS.Universal vars imp_form nullRange

-- | generates a conjunction of negation of existencial quantifiers

existencialNegationOtherEqs :: CAS.OP_SYMB -> [CAS.CASLTERM] ->

[Named CAS.CASLFORMULA] -> CAS.CASLFORMULA

existencialNegationOtherEqs op ts forms = form

where ex_forms = foldr ((++) . existencialNegationOtherEq op ts) [] forms

form = if length ex_forms > 1

then CAS.Conjunction ex_forms nullRange

else head ex_forms

-- | given a formula, if it refers to the same operator indicated by the parameters

-- the predicate creates a list with the negation of the existence of variables that

-- match the pattern described in the formula. In other case it returns an empty list

existencialNegationOtherEq :: CAS.OP_SYMB -> [CAS.CASLTERM] ->

Named CAS.CASLFORMULA -> [CAS.CASLFORMULA]

existencialNegationOtherEq req_op terms form = case ok of

False -> []

True -> let

(_, ts, conds) = fromJust tpl

ts' = qualifyExVarsTerms ts

conds' = qualifyExVarsForms conds

prems = (createEqs ts' terms) ++ conds'

conj_form = CAS.Conjunction prems nullRange

ex_form = if vars' /= []

then CAS.Quantification CAS.Existential vars' conj_form nullRange

else conj_form

neg_form = CAS.Negation ex_form nullRange

in [neg_form]

where (inner_form, vars) = noQuantification $ sentence form

vars' = qualifyExVars vars

tpl = getLeftApp inner_form

ok = case tpl of

Nothing -> False

Just _ -> let (op, ts, _) = fromJust tpl

in req_op == op && length terms == length ts

-- | qualifies the variables in a list of formulas with the suffix "_ex" to

-- distinguish them from the variables already bound

qualifyExVarsForms :: [CAS.CASLFORMULA] -> [CAS.CASLFORMULA]

qualifyExVarsForms = map qualifyExVarsForm

-- | qualifies the variables in a formula with the suffix "_ex" to distinguish them

-- from the variables already bound

qualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA

qualifyExVarsForm (CAS.Strong_equation t t' r) = CAS.Strong_equation qt qt' r

where qt = qualifyExVarsTerm t

qt' = qualifyExVarsTerm t'

qualifyExVarsForm (CAS.Predication op ts r) = CAS.Predication op ts' r

where ts' = qualifyExVarsTerms ts

qualifyExVarsForm f = f

-- | qualifies the variables in a list of terms with the suffix "_ex" to

-- distinguish them from the variables already bound

qualifyExVarsTerms :: [CAS.CASLTERM] -> [CAS.CASLTERM]

qualifyExVarsTerms = map qualifyExVarsTerm

-- | qualifies the variables in a term with the suffix "_ex" to distinguish them

-- from the variables already bound

qualifyExVarsTerm :: CAS.CASLTERM -> CAS.CASLTERM

qualifyExVarsTerm (CAS.Qual_var var sort r) = CAS.Qual_var (qualifyExVarAux var) sort r

qualifyExVarsTerm (CAS.Application op ts r) = CAS.Application op ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Sorted_term t s r) = CAS.Sorted_term (qualifyExVarsTerm t) s r

qualifyExVarsTerm (CAS.Cast t s r) = CAS.Cast (qualifyExVarsTerm t) s r

qualifyExVarsTerm (CAS.Conditional t1 f t2 r) = CAS.Conditional t1' f t2' r

where t1' = qualifyExVarsTerm t1

t2' = qualifyExVarsTerm t2

qualifyExVarsTerm (CAS.Mixfix_term ts) = CAS.Mixfix_term ts'

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Mixfix_parenthesized ts r) = CAS.Mixfix_parenthesized ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Mixfix_bracketed ts r) = CAS.Mixfix_bracketed ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Mixfix_braced ts r) = CAS.Mixfix_braced ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm t = t

-- | qualifies a list of variables with the suffix "_ex" to

-- distinguish them from the variables already bound

qualifyExVars :: [CAS.VAR_DECL] -> [CAS.VAR_DECL]

qualifyExVars = map qualifyExVar

-- | qualifies a variable with the suffix "_ex" to distinguish it from

-- the variables already bound

qualifyExVar :: CAS.VAR_DECL -> CAS.VAR_DECL

qualifyExVar (CAS.Var_decl vars s r) = CAS.Var_decl vars' s r

where vars' = map qualifyExVarAux vars

-- | qualifies a token with the suffix "_ex"

qualifyExVarAux :: Token -> Token

qualifyExVarAux var = mkSimpleId $ show var ++ "_ex"

-- | creates a list of strong equalities from two lists of terms

createEqs :: [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]

createEqs (t1 : ts1) (t2 : ts2) = CAS.Strong_equation t1 t2 nullRange : ls

where ls = createEqs ts1 ts2

createEqs _ _ = []

-- | extracts the operator at the top and the arguments of the lefthand side

-- in a strong equation

getLeftApp :: CAS.CASLFORMULA -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM], [CAS.CASLFORMULA])

getLeftApp (CAS.Strong_equation term _ _) = case getLeftAppTerm term of

Nothing -> Nothing

Just (op, ts) -> Just (op, ts, [])

getLeftApp (CAS.Implication prem concl _ _) = case getLeftApp concl of

Nothing -> Nothing

Just (op, ts, _) -> Just (op, ts, conds)

where conds = getPremisesImplication prem

getLeftApp _ = Nothing

-- | extracts the operator at the top and the arguments of the lefthand side

-- in an application term

getLeftAppTerm :: CAS.CASLTERM -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM])

getLeftAppTerm (CAS.Application op ts _) = Just (op, ts)

getLeftAppTerm _ = Nothing

-- | extracts the formulas of the given premise, distinguishing whether it is

-- a conjunction or not

getPremisesImplication :: CAS.CASLFORMULA -> [CAS.CASLFORMULA]

getPremisesImplication (CAS.Conjunction forms _) = forms

getPremisesImplication form = [form]

-- | translate a Maude membership into a CASL formula

mb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA

mb2formula im (MAS.Mb t s [] _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

pred_name = CAS.Pred_name $ token2id $ getName s

form = CAS.Predication pred_name [ct] nullRange

mb2formula im (MAS.Mb t s conds@(_ : _) _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

pred_name = CAS.Pred_name $ token2id $ getName s

conds_form = conds2formula im conds

concl_form = CAS.Predication pred_name [ct] nullRange

form = CAS.Implication conds_form concl_form True nullRange

-- | translate a Maude rule into a CASL formula

rl2formula :: IdMap -> MAS.Rule -> CAS.CASLFORMULA

rl2formula im (MAS.Rl t t' [] _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

pred_name = CAS.Pred_name rewID

form = CAS.Predication pred_name [ct, ct'] nullRange

rl2formula im (MAS.Rl t t' conds@(_:_) _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

pred_name = CAS.Pred_name rewID

conds_form = conds2formula im conds

concl_form = CAS.Predication pred_name [ct, ct'] nullRange

form = CAS.Implication conds_form concl_form True nullRange

-- | translate a conjunction of Maude conditions to a CASL formula

conds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA

conds2formula im conds = CAS.Conjunction forms nullRange

where forms = map (cond2formula im) conds

-- | translate a single Maude condition to a CASL formula

cond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA

cond2formula im (MAS.EqCond t t') = CAS.Strong_equation ct ct' nullRange

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

cond2formula im (MAS.MatchCond t t') = CAS.Strong_equation ct ct' nullRange

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

cond2formula im (MAS.MbCond t s) = CAS.Predication pred_name [ct] nullRange

where ct = maudeTerm2caslTerm im t

pred_name = CAS.Pred_name $ token2id $ getName s

cond2formula im (MAS.RwCond t t') = CAS.Predication pred_name [ct, ct'] nullRange

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

pred_name = CAS.Pred_name rewID

-- | translate a Maude term into a CASL term

maudeTerm2caslTerm :: IdMap -> MAS.Term -> CAS.CASLTERM

maudeTerm2caslTerm im (MAS.Var q ty) = CAS.Qual_var q kind nullRange

where kind = fromJust $ Map.lookup (token2id $ getName ty) im

maudeTerm2caslTerm _ (MAS.Const q _) = CAS.Application (CAS.Op_name name) [] nullRange

where name = token2id q

maudeTerm2caslTerm im (MAS.Apply q ts _) = CAS.Application (CAS.Op_name name) tts nullRange

where name = token2id q

tts = map (maudeTerm2caslTerm im) ts

rewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]

rewPredicatesSens = Set.fold rewPredicateSens []

rewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

rewPredicateSens kind acc = [ref, trans] ++ acc

where ref = reflSen kind

trans = transSen kind

-- | creates the reflexivity predicate for the given kind

reflSen :: Id -> Named CAS.CASLFORMULA

reflSen kind = makeNamed name $ quantifyUniversally form

where v = newVar kind

pn = CAS.Pred_name rewID

form = CAS.Predication pn [v, v] nullRange

name = "rew_refl_" ++ show kind

-- | creates the transitivity predicate for the given kind

transSen :: Id -> Named CAS.CASLFORMULA

transSen kind = makeNamed name $ quantifyUniversally form

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

v3 = newVarIndex 3 kind

pn = CAS.Pred_name rewID

prem1 = CAS.Predication pn [v1, v2] nullRange

prem2 = CAS.Predication pn [v2, v3] nullRange

concl = CAS.Predication pn [v1, v3] nullRange

conj_form = CAS.Conjunction [prem1, prem2] nullRange

form = CAS.Implication conj_form concl True nullRange

name = "rew_trans_" ++ show kind

-- | generate the predicates for the rewrites

rewPredicates :: Map.Map Id (Set.Set CSign.PredType) -> Set.Set Id

-> Map.Map Id (Set.Set CSign.PredType)

rewPredicates m = Set.fold rewPredicate m

rewPredicate :: Id -> Map.Map Id (Set.Set CSign.PredType)

-> Map.Map Id (Set.Set CSign.PredType)

rewPredicate kind m = Map.insertWith (Set.union) rewID ar m

where ar = Set.singleton $ CSign.PredType [kind, kind]

-- | create the predicates that assign sorts to each term

kindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)

kindPredicates = Map.foldWithKey kindPredicate Map.empty

-- | create the predicates that assign the current sort to the

-- corresponding terms

kindPredicate :: Id -> Id -> Map.Map Id (Set.Set CSign.PredType)

-> Map.Map Id (Set.Set CSign.PredType)

kindPredicate sort kind mis = case sort == (token2id $ mkSimpleId "Universal") of

True -> mis

False -> let ar = Set.singleton $ CSign.PredType [kind]

in Map.insertWith (Set.union) sort ar mis

-- | extract the kinds from the map of id's

kindsFromMap :: IdMap -> Set.Set Id

kindsFromMap = Map.fold Set.insert Set.empty

-- | return a map where each sort is mapped to its kind, both of them

-- already converted to Id

arrangeKinds :: MSign.SortSet -> MSign.SubsortRel -> IdMap

arrangeKinds ss r = arrangeKindsList (Set.toList ss) r Map.empty

-- | traverse the sorts and creates a table that assigns to each sort its kind

arrangeKindsList :: [MSym.Symbol] -> MSign.SubsortRel -> IdMap -> IdMap

arrangeKindsList [] _ m = m

arrangeKindsList l@(s : _) r m = arrangeKindsList not_rel r m'

where tops = List.sort $ getTop r s

tc = Rel.transClosure r

(rel, not_rel) = sameKindList s tc l

f = \ x y z -> Map.insert (sym2id y) (sort2id x) z

m' = foldr (f tops) m rel

-- | creates two list distinguishing in the first componente the symbols

-- with the same kind than the given one and in the second one the

-- symbols with different kind

sameKindList :: MSym.Symbol -> MSign.SubsortRel -> [MSym.Symbol]

-> ([MSym.Symbol], [MSym.Symbol])

sameKindList _ _ [] = ([], [])

sameKindList t r (t' : ts) = if MSym.sameKind r t t'

then (t' : hold, not_hold)

else (hold, t' : not_hold)

where (hold, not_hold) = sameKindList t r ts

-- | transform the set of Maude sorts in a set of CASL sorts, including

-- only one sort for each kind.

sortsTranslation :: MSign.SortSet -> MSign.SubsortRel -> Set.Set Id

sortsTranslation ss r = sortsTranslationList (Set.toList ss) r

-- | transform a list representing the Maude sorts in a set of CASL sorts,

-- including only one sort for each kind.

sortsTranslationList :: [MSym.Symbol] -> MSign.SubsortRel -> Set.Set Id

sortsTranslationList [] _ = Set.empty

sortsTranslationList (s : ss) r = Set.insert (sort2id tops) res

where tops@(top : _) = List.sort $ getTop r s

ss' = deleteRelated ss top r

res = sortsTranslation ss' r

-- | return a maximal element from the sort relation

getTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]

getTop r tok = case succs of

[] -> [tok]

toks@(_:_) -> foldr ((++) . (getTop r)) [] toks

where succs = Set.toList $ Rel.succs r tok

-- | delete from the list of sorts those in the same kind that the parameter

deleteRelated :: [MSym.Symbol] -> MSym.Symbol -> MSign.SubsortRel -> MSign.SortSet

deleteRelated ss sym r = foldr (f sym tc) Set.empty ss

where tc = Rel.transClosure r

f = \ sort trC x y -> if MSym.sameKind trC sort x

then y

else Set.insert x y

-- | build an Id from a token with the function mkId

token2id :: Token -> Id

token2id t = mkId [t]

-- | build an Id from a Maude symbol

sym2id :: MSym.Symbol -> Id

sym2id = token2id . getName

-- | build an Id from a list of sorts, including the "[" and "," if needed

sort2id :: [MSym.Symbol] -> Id

sort2id syms = mkId tokens'

where tokens = map getName syms

tokens' = mkSimpleId "[" : (putCommas tokens) ++ [mkSimpleId "]"]

-- | inserts commas between tokens

putCommas :: [Token] -> [Token]

putCommas [] = []

putCommas [t] = [t]

putCommas (t : ts) = t : (mkSimpleId ",") : putCommas ts

-- | add universal quantification of all variables in the formula

quantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA

quantifyUniversally form = if null var_decl

then form

else CAS.Quantification CAS.Universal var_decl form nullRange

where vars = getVars form

var_decl = listVarDecl vars

-- | traverses a map with sorts as keys and sets of variables as value and creates

-- a list of variable declarations

listVarDecl :: Map.Map Id (Set.Set Token) -> [CAS.VAR_DECL]

listVarDecl = Map.foldWithKey f []

where f = \ sort var_set acc -> CAS.Var_decl (Set.toList var_set) sort nullRange : acc

-- | removes a quantification from a formula

noQuantification :: CAS.CASLFORMULA -> (CAS.CASLFORMULA, [CAS.VAR_DECL])

noQuantification (CAS.Quantification _ vars form _) = (form, vars)

noQuantification form = (form, [])

-- | translate the CASL sorts to symbols

kinds2syms :: Set.Set Id -> Set.Set CSign.Symbol

kinds2syms = Set.map kind2sym

-- | translate a CASL sort to a CASL symbol

kind2sym :: Id -> CSign.Symbol

kind2sym k = CSign.Symbol k CSign.SortAsItemType

-- | translates the CASL predicates into CASL symbols

preds2syms :: Map.Map Id (Set.Set CSign.PredType) -> Set.Set CSign.Symbol

preds2syms = Map.foldWithKey pred2sym Set.empty

-- | translates a CASL predicate into a CASL symbol

pred2sym :: Id -> Set.Set CSign.PredType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol

pred2sym pn spt acc = Set.union set acc

where set = Set.fold (createSym4id pn) Set.empty spt

-- | creates a CASL symbol for a predicate

createSym4id :: Id -> CSign.PredType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol

createSym4id pn pt acc = Set.insert sym acc

where sym = CSign.Symbol pn $ CSign.PredAsItemType pt

-- | translates the CASL operators into CASL symbols

ops2symbols :: CSign.OpMap -> Set.Set CSign.Symbol

ops2symbols = Map.foldWithKey op2sym Set.empty

-- | translates a CASL operator into a CASL symbol

op2sym :: Id -> Set.Set CSign.OpType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol

op2sym on sot acc = Set.union set acc

where set = Set.fold (createSymOp4id on) Set.empty sot

-- | creates a CASL symbol for an operator

createSymOp4id :: Id -> CSign.OpType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol

createSymOp4id on ot acc = Set.insert sym acc

where sym = CSign.Symbol on $ CSign.OpAsItemType ot

-- | extract the variables from a CASL formula and put them in a map

-- with keys the sort of the variables and value the set of variables

-- in this sort

getVars :: CAS.CASLFORMULA -> Map.Map Id (Set.Set Token)

getVars (CAS.Quantification _ _ f _) = getVars f

getVars (CAS.Conjunction fs _) = foldr (Map.unionWith (Set.union) . getVars) Map.empty fs

getVars (CAS.Disjunction fs _) = foldr (Map.unionWith (Set.union) . getVars) Map.empty fs

getVars (CAS.Implication f1 f2 _ _) = Map.unionWith (Set.union) v1 v2

where v1 = getVars f1

v2 = getVars f2

getVars (CAS.Equivalence f1 f2 _) = Map.unionWith (Set.union) v1 v2

where v1 = getVars f1

v2 = getVars f2

getVars (CAS.Negation f _) = getVars f

getVars (CAS.Predication _ ts _) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVars (CAS.Definedness t _) = getVarsTerm t

getVars (CAS.Existl_equation t1 t2 _) = Map.unionWith (Set.union) v1 v2

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

getVars (CAS.Strong_equation t1 t2 _) = Map.unionWith (Set.union) v1 v2

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

getVars (CAS.Membership t _ _) = getVarsTerm t

getVars (CAS.Mixfix_formula t) = getVarsTerm t

getVars _ = Map.empty

-- | extract the variables of a CASL term

getVarsTerm :: CAS.CASLTERM -> Map.Map Id (Set.Set Token)

getVarsTerm (CAS.Qual_var var sort _) = Map.insert sort (Set.singleton var) Map.empty

getVarsTerm (CAS.Application _ ts _) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t

getVarsTerm (CAS.Cast t _ _) = getVarsTerm t

getVarsTerm (CAS.Conditional t1 f t2 _) = Map.unionWith (Set.union) v3 m

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

v3 = getVars f

m = Map.unionWith (Set.union) v1 v2

getVarsTerm (CAS.Mixfix_term ts) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Mixfix_parenthesized ts _) =

foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Mixfix_bracketed ts _) =

foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Mixfix_braced ts _) =

foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVarsTerm _ = Map.empty

-- | generates the constructor constraint

ctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA

ctorSen isFree (sorts, _, ops) = do

let sortList = Set.toList sorts

opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide

(CSign.toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops

allSyms = opSyms

resType _ (CAS.Op_name _) = False

resType s (CAS.Qual_op_name _ t _) = CAS.res_OP_TYPE t == s

getIndex s = maybe (-1) id $ List.findIndex (== s) sortList

addIndices (CAS.Op_name _) =

error "CASL/StaticAna: Internal error in function addIndices"

addIndices os@(CAS.Qual_op_name _ t _) =

(os,map getIndex $ CAS.args_OP_TYPE t)

collectOps s =

CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s

constrs = map collectOps sortList

f = CAS.Sort_gen_ax constrs isFree

makeNamed ("ga_generated_" ++ showSepList (showString "_") showId sortList "") f