a530dde7009b0a808300c420def741354a4d13d2Martin KühlDescription : Maude Comorphisms
a530dde7009b0a808300c420def741354a4d13d2Martin KühlCopyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
a530dde7009b0a808300c420def741354a4d13d2Martin KühlMaintainer : ariesco@fdi.ucm.es
a530dde7009b0a808300c420def741354a4d13d2Martin KühlStability : experimental
a530dde7009b0a808300c420def741354a4d13d2Martin KühlPortability : portable
a530dde7009b0a808300c420def741354a4d13d2Martin KühlComorphism from Maude to CASL.
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoimport qualified Data.List as List
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Data.Set as Set
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Data.Map as Map
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Maude.Sign as MSign
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Maude.Sentence as MSentence
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Maude.Morphism as MMorphism
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoimport qualified Maude.AS_Maude as MAS
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoimport qualified Maude.Symbol as MSym
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified CASL.Sign as CSign
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified CASL.Morphism as CMorphism
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoimport qualified CASL.AS_Basic_CASL as CAS
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Common.Lib.Rel as Rel
8ecdb62fa2cef068eb4dbce59f3219a8e3adc0baChristian Maederimport qualified Common.Lib.MapSet as MapSet
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescotype IdMap = Map.Map Id Id
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riescotype OpTransTuple = (CSign.OpMap, CSign.OpMap, Set.Set Component)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates a CASL morphism from a Maude morphism
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermapMorphism :: MMorphism.Morphism -> Result CMorphism.CASLMor
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescomapMorphism morph =
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco mk = kindMapId $ MSign.kindRel src
6e121321775373fe11161d23c541437456df19b4Adrián Riesco mk' = kindMapId $ MSign.kindRel tgt
6e121321775373fe11161d23c541437456df19b4Adrián Riesco smap' = applySortMap2CASLSorts smap mk mk'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco omap' = maudeOpMap2CASLOpMap mk omap
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pmap = createPredMap mk smap
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (src', _) = maude2casl src []
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (tgt', _) = maude2casl tgt []
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | translates the Maude morphism between operators into a CASL morpshim
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederbetween operators -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map
a74f814d3b445eadad6f68737a98a7a303698affChristian MaedermaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | translates the mapping between two symbols representing operators into
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedera CASL operators map -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedertranslateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where f = token2id . getName
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder g x = Map.findWithDefault (errorId "translate op map entry")
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco cop = (token2id from, ot)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco to' = (token2id to, CAS.Total)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco copm' = Map.insert cop to' copm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOpMapEntry _ _ _ _ = Map.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates a set of CASL symbol from a Maude Symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSymbol sg (MSym.Sort q) = Set.singleton csym
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco where mk = kindMapId $ MSign.kindRel sg
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sym_id = token2id q
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "map symbol") sym_id mk
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_data = CSign.PredType [kind]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSymbol sg (MSym.Operator q ar co) = Set.singleton csym
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco where mk = kindMapId $ MSign.kindRel sg
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco q' = token2id q
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ar' = map (maudeSort2caslId mk) ar
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco co' = token2id $ getName co
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco csym = CSign.Symbol q' $ CSign.OpAsItemType op_data
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSymbol _ _ = Set.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | returns the sort in CASL of the Maude sort symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeSort2caslId :: IdMap -> MSym.Symbol -> Id
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermaudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id")
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (token2id $ getName sym) im
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | creates the predicate map for the CASL morphism from the Maude sort map and
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederthe map between sorts and kinds -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreatePredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map
a74f814d3b445eadad6f68737a98a7a303698affChristian MaedercreatePredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates an entry of the predicate map for a single sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreatePredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercreatePredMap4sort im from to = Map.insert key id_to
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where id_from = token2id $ getName from
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco id_to = token2id $ getName to
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder kind = Map.findWithDefault (errorId "predicate for sort")
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco key = (id_from, CSign.PredType [kind])
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | computes the sort morphism of CASL from the sort morphism in Maude
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederand the set of kinds -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederapplySortMap2CASLSorts :: MMorphism.SortMap -> IdMap -> IdMap
6e121321775373fe11161d23c541437456df19b4Adrián RiescoapplySortMap2CASLSorts sm im im' = Map.fromList sml'
6e121321775373fe11161d23c541437456df19b4Adrián Riesco where sml = Map.toList sm
6e121321775373fe11161d23c541437456df19b4Adrián Riesco sml' = foldr (applySortMap2CASLSort im im') [] sml
6e121321775373fe11161d23c541437456df19b4Adrián Riesco-- | computes the morphism for a single sort pair
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederapplySortMap2CASLSort :: IdMap -> IdMap -> (MSym.Symbol, MSym.Symbol)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -> [(Id, Id)] -> [(Id, Id)]
6e121321775373fe11161d23c541437456df19b4Adrián RiescoapplySortMap2CASLSort im im' (s1, s2) l = l'
6e121321775373fe11161d23c541437456df19b4Adrián Riesco where p1 = (mSym2caslId s1, mSym2caslId s2)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (errorId $ "err" ++ show (mSym2caslId x)) (mSym2caslId x)
6e121321775373fe11161d23c541437456df19b4Adrián Riesco p2 = (f s1 im, f s2 im')
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder l' = p1 : if s1 == s2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then l else p2 : l
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | renames the sorts in a given kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescorename :: MMorphism.SortMap -> Token -> Token
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescorename sm tok = new_tok
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where sym = MSym.Sort tok
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sym' = if Map.member sym sm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco then fromJust $ Map.lookup sym sm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco new_tok = getName sym'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates a Maude sentence into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA
9e0e436980397412aa6c10b9aebde527ca2474bfChristian MaedermapSentence sg sen = let
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder mk = kindMapId $ MSign.kindRel sg
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder named = makeNamed "" sen
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder form = mb_rl2formula mk named
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder in return $ sentence $ case sen of
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder MSentence.Equation (MAS.Eq _ _ _ ats) -> if any MAS.owise ats then let
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder (no_owise_sens, _, _) = splitOwiseEqs sg_sens
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder in owiseSen2Formula mk no_owise_forms named
9e0e436980397412aa6c10b9aebde527ca2474bfChristian Maeder else noOwiseSen2Formula mk named
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | applies maude2casl to compute the CASL signature and sentences from
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederthe Maude ones, and wraps them into a Result datatype -}
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescomapTheory :: (MSign.Sign, [Named MSentence.Sentence])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescomapTheory (sg, nsens) = return $ maude2casl sg nsens
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | computes new signature and sentences of CASL associated to the
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedergiven Maude signature and sentences -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomaude2casl :: MSign.Sign -> [Named MSentence.Sentence]
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maedermaude2casl msign nsens = (csign {
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco CSign.declaredSymbols = syms }, new_sens)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where csign = CSign.emptySign ()
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco ss' = Set.map sym2id ss
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco mk = kindMapId $ MSign.kindRel msign
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco sbs' = maudeSbs2caslSbs sbs mk
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco cs = Set.union ss' $ kindsFromMap mk
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco preds = rewPredicates cs
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco rs = rewPredicatesSens cs
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco ops = deleteUniversal $ MSign.ops msign
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ksyms = kinds2syms cs
ab9c6be005cb2af851307b7968c2baa16a76d6b1Adrián Riesco (cops, assoc_ops, _) = translateOps mk ops -- (cops, assoc_ops, comps)
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco axSens = axiomsSens mk ops
5eb747ed1f9cb3d902d4277badfc2a42f9f98b0cAdrián Riesco ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco cops' = universalOps cs cops $ booleanImported ops
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco rs' = rewPredicatesCongSens cops'
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco pred_forms = loadLibraries (MSign.sorts msign) ops
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ops_syms = ops2symbols cops'
3f8cdebaede9921402318d525b57a9af8f9279d3Adrián Riesco (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco preds_syms = preds2syms preds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco syms = Set.union ksyms $ Set.union ops_syms preds_syms
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco new_sens = concat [rs, rs', no_owise_forms, owise_forms,
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco mb_rl_forms, ctor_sen, pred_forms, axSens]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | translates the Maude subsorts into CASL subsorts, and adds the subsorts
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederfor the kinds -}
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescomaudeSbs2caslSbs :: MSign.SubsortRel -> IdMap -> Rel.Rel CAS.SORT
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian MaedermaudeSbs2caslSbs sbs im = Rel.fromMap m4
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco l1 = [] -- map maudeSb2caslSb l
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco l2 = idList2Subsorts $ Map.toList im
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco l3 = map subsorts2Ids l
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco m4 = Map.unionWith Set.union m1 $ Map.unionWith Set.union m2 m3
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescoidList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescoidList2Subsorts [] = []
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián RiescoidList2Subsorts ((id1, id2) : il) = t1 : idList2Subsorts il
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco where t1 = (id1, Set.singleton id2)
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescomaudeSb2caslSb :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescomaudeSb2caslSb (sym, st) = (sortSym2id sym, Set.map (kindId . sortSym2id) st)
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riescosubsorts2Ids :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riescosubsorts2Ids (sym, st) = (sortSym2id sym, Set.map sortSym2id st)
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescosortSym2id :: MSym.Symbol -> Id
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescosortSym2id (MSym.Sort q) = token2id q
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedersortSym2id _ = token2id $ mkSimpleId "error_translation"
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- | generates the sentences to state that the rew predicates are a congruence
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescorewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrewPredicatesCongSens = MapSet.foldWithKey rewPredCong []
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | generates the sentences to state that the rew predicates are a congruence
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederfor a single operator -}
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrewPredCong :: Id -> CSign.OpType -> [Named CAS.CASLFORMULA]
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescorewPredCong op ot fs = case args of
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco _ -> nq_form : fs
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco where args = CSign.opArgs ot
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco vars1 = rewPredCongPremise 0 args
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco vars2 = rewPredCongPremise (length args) args
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco res_pred_type = CAS.Pred_type [res, res] nullRange
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco pn = CAS.Qual_pred_name rewID res_pred_type nullRange
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco name = "rew_cong_" ++ show op
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco prems = rewPredsCong args vars1 vars2
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco prems_conj = createConjForm prems
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco os = CAS.Qual_op_name op (CSign.toOP_TYPE ot) nullRange
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco conc_term1 = CAS.Application os vars1 nullRange
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco conc_term2 = CAS.Application os vars2 nullRange
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco conc_form = CAS.Predication pn [conc_term1, conc_term2] nullRange
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco form = createImpForm prems_conj conc_form
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco nq_form = makeNamed name $ quantifyUniversally form
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- | generates a list of variables of the given sorts
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescorewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescorewPredCongPremise n (s : ss) = newVarIndex n s : rewPredCongPremise (n + 1) ss
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescorewPredCongPremise _ [] = []
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- | generates a list of rew predicates with the given variables
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederrewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM]
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescorewPredsCong (s : ss) (t : ts) (t' : ts') = form : forms
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco where pred_type = CAS.Pred_type [s, s] nullRange
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco pn = CAS.Qual_pred_name rewID pred_type nullRange
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco form = CAS.Predication pn [t, t'] nullRange
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco forms = rewPredsCong ss ts ts'
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescorewPredsCong _ _ _ = []
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | load the CASL libraries for the Maude built-in operators
223be434693e8c97e2522ac19155a284b3536035Adrián RiescoloadLibraries :: MSign.SortSet -> MSign.OpMap -> [Named CAS.CASLFORMULA]
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederloadLibraries ss om = if natImported ss om then loadNaturalNatSens else []
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | loads the sentences associated to the natural numbers
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoloadNaturalNatSens :: [Named CAS.CASLFORMULA]
cffa214f1ca524a65075ab26339df7040fe36032Christian MaederloadNaturalNatSens = [] -- retrieve code from Rev 17944 if needed again!
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | checks if a sentence is an constructor sentence
223be434693e8c97e2522ac19155a284b3536035Adrián RiescoctorCons :: Named CAS.CASLFORMULA -> Bool
223be434693e8c97e2522ac19155a284b3536035Adrián RiescoctorCons f = case sentence f of
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | checks if the boolean values are imported
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescobooleanImported :: MSign.OpMap -> Bool
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescobooleanImported = Map.member (mkSimpleId "if_then_else_fi")
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | checks if the natural numbers are imported
223be434693e8c97e2522ac19155a284b3536035Adrián RiesconatImported :: MSign.SortSet -> MSign.OpMap -> Bool
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiesconatImported ss om = b1 && b2 && b3
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco where b1 = Set.member (MSym.Sort $ mkSimpleId "Nat") ss
0be63c5d4b5e66cc600a0003081ae2bf85be9615Adrián Riesco b2 = Map.member (mkSimpleId "s_") om
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder b3 = not b2 || specialZeroSet (om Map.! mkSimpleId "s_")
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescospecialZeroSet :: MSign.OpDeclSet -> Bool
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescospecialZeroSet = Set.fold specialZero False
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescospecialZero :: MSign.OpDecl -> Bool -> Bool
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescospecialZero (_, ats) b = b' || b
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco where b' = isSpecial ats
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescoisSpecial :: [MAS.Attr] -> Bool
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescoisSpecial [] = False
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederisSpecial (MAS.Special _ : _) = True
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescoisSpecial (_ : ats) = isSpecial ats
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | delete the universal operators from Maude specifications, that will be
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedersubstituted for one operator for each sort in the specification -}
223be434693e8c97e2522ac19155a284b3536035Adrián RiescodeleteUniversal om = om5
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco where om1 = Map.delete (mkSimpleId "if_then_else_fi") om
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco om2 = Map.delete (mkSimpleId "_==_") om1
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco om3 = Map.delete (mkSimpleId "_=/=_") om2
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco om4 = Map.delete (mkSimpleId "upTerm") om3
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco om5 = Map.delete (mkSimpleId "downTerm") om4
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates the universal operators for all the sorts in the module
223be434693e8c97e2522ac19155a284b3536035Adrián RiescouniversalOps :: Set.Set Id -> CSign.OpMap -> Bool -> CSign.OpMap
223be434693e8c97e2522ac19155a284b3536035Adrián RiescouniversalOps kinds om True = Set.fold universalOpKind om kinds
223be434693e8c97e2522ac19155a284b3536035Adrián RiescouniversalOps _ om False = om
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates the universal operators for a concrete module
223be434693e8c97e2522ac19155a284b3536035Adrián RiescouniversalOpKind :: Id -> CSign.OpMap -> CSign.OpMap
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederuniversalOpKind kind = MapSet.union $ MapSet.fromList
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder [ (if_id, [if_opt]), (double_eq_id, [eq_opt]), (neg_double_eq_id, [eq_opt]) ]
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco where if_id = str2id "if_then_else_fi"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco double_eq_id = str2id "_==_"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco neg_double_eq_id = str2id "_=/=_"
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco bool_id = str2id "Bool"
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder if_opt = CSign.OpType CAS.Total [bool_id, kind, kind] kind
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder eq_opt = CSign.OpType CAS.Total [kind, kind] bool_id
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates the formulas for the universal operators
223be434693e8c97e2522ac19155a284b3536035Adrián RiescouniversalSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
223be434693e8c97e2522ac19155a284b3536035Adrián RiescouniversalSens = Set.fold universalSensKind []
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates the formulas for the universal operators for the given sort
223be434693e8c97e2522ac19155a284b3536035Adrián RiescouniversalSensKind :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
223be434693e8c97e2522ac19155a284b3536035Adrián RiescouniversalSensKind kind acc = concat [iss, eqs, neqs, acc]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where iss = ifSens kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco eqs = equalitySens kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neqs = nonEqualitySens kind
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates the formulas for the if statement
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoifSens :: Id -> [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoifSens kind = [form'', neg_form'']
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where v1 = newVarIndex 1 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v2 = newVarIndex 2 kind
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco bk = str2id "Bool"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco bv = newVarIndex 2 bk
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco true_type = CAS.Op_type CAS.Total [] bk nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco true_id = CAS.Qual_op_name (str2id "true") true_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco true_term = CAS.Application true_id [] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco if_type = CAS.Op_type CAS.Total [bk, kind, kind] kind nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco if_name = str2id "if_then_else_fi"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco if_id = CAS.Qual_op_name if_name if_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco if_term = CAS.Application if_id [bv, v1, v2] nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder prem = CAS.mkStEq bv true_term
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder concl = CAS.mkStEq if_term v1
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder form = CAS.mkImpl prem concl
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form' = quantifyUniversally form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_prem = CAS.Negation prem nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder neg_concl = CAS.mkStEq if_term v2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder neg_form = CAS.mkImpl neg_prem neg_concl
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_form' = quantifyUniversally neg_form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name1 = show kind ++ "_if_true"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name2 = show kind ++ "_if_false"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form'' = makeNamed name1 form'
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_form'' = makeNamed name2 neg_form'
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates the formulas for the equality
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoequalitySens :: Id -> [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoequalitySens kind = [form'', comp_form'']
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where v1 = newVarIndex 1 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v2 = newVarIndex 2 kind
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco bk = str2id "Bool"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco b_type = CAS.Op_type CAS.Total [] bk nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco true_term = CAS.Application true_id [] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco false_term = CAS.Application false_id [] nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco double_eq_name = str2id "_==_"
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder double_eq_id = CAS.mkQualOp double_eq_name double_eq_type
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder concl = CAS.mkStEq double_eq_term true_term
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder form = CAS.mkImpl prem concl
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form' = quantifyUniversally form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_prem = CAS.Negation prem nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder new_concl = CAS.mkStEq double_eq_term false_term
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder comp_form = CAS.mkImpl neg_prem new_concl
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco comp_form' = quantifyUniversally comp_form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name1 = show kind ++ "_==_true"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name2 = show kind ++ "_==_false"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form'' = makeNamed name1 form'
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco comp_form'' = makeNamed name2 comp_form'
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates the formulas for the inequality
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescononEqualitySens :: Id -> [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescononEqualitySens kind = [form'', comp_form'']
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where v1 = newVarIndex 1 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v2 = newVarIndex 2 kind
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco bk = str2id "Bool"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco b_type = CAS.Op_type CAS.Total [] bk nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco true_term = CAS.Application true_id [] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco false_term = CAS.Application false_id [] nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco double_eq_name = str2id "_==_"
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder double_eq_id = CAS.mkQualOp double_eq_name double_eq_type
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder concl = CAS.mkStEq double_eq_term false_term
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder form = CAS.mkImpl prem concl
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form' = quantifyUniversally form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_prem = CAS.Negation prem nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder new_concl = CAS.mkStEq double_eq_term true_term
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder comp_form = CAS.mkImpl neg_prem new_concl
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco comp_form' = quantifyUniversally comp_form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name1 = show kind ++ "_=/=_false"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name2 = show kind ++ "_=/=_true"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form'' = makeNamed name1 form'
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco comp_form'' = makeNamed name2 comp_form'
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco-- | generates the sentences for the operator attributes
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescoaxiomsSens :: IdMap -> MSign.OpMap -> [Named CAS.CASLFORMULA]
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederaxiomsSens im = Map.fold (axiomsSensODS im) []
8ecdb62fa2cef068eb4dbce59f3219a8e3adc0baChristian MaederaxiomsSensODS :: IdMap -> MSign.OpDeclSet -> [Named CAS.CASLFORMULA]
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescoaxiomsSensODS im ods l = Set.fold (axiomsSensOD im) l ods
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederaxiomsSensOD :: IdMap -> MSign.OpDecl -> [Named CAS.CASLFORMULA]
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescoaxiomsSensOD im (ss, ats) l = Set.fold (axiomsSensSS im ats) l ss
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescoaxiomsSensSS :: IdMap -> [MAS.Attr] -> MSym.Symbol -> [Named CAS.CASLFORMULA]
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederaxiomsSensSS im ats (MSym.Operator q ar co) l = l ++ l1
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco where l1 = if elem MAS.Comm ats
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco then commSen im q ar co
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescoaxiomsSensSS _ _ _ l = l
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercommSen :: IdMap -> MAS.Qid -> MSym.Symbols -> MSym.Symbol
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescocommSen im q ar@[ar1, ar2] co = [form']
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco where q' = token2id q
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder f = (`maudeSymbol2caslSort` im)
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco ot = CAS.Op_type CAS.Total (map f ar) (f co) nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco os = CAS.Qual_op_name q' ot nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco v1 = newVarIndex 1 ar1'
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco v2 = newVarIndex 2 ar2'
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco t1 = CAS.Application os [v1, v2] nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco t2 = CAS.Application os [v2, v1] nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder name = "comm_" ++ ms2vcs (show q') ++ "_" ++ show ar1'
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco form' = makeNamed name $ quantifyUniversally form
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescocommSen _ _ _ _ = []
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco-- (newVarIndex 1 (hd ar))
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder-- maudeSymbol2caslSort x im
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | translates the Maude operator map into a tuple of CASL operators, CASL
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederassociative operators, membership induced from each Maude operator,
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederand the set of sorts with the ctor attribute -}
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescotranslateOps :: IdMap -> MSign.OpMap -> OpTransTuple
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedertranslateOps im = Map.fold (translateOpDeclSet im)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates an operator declaration set into a tern as described above
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescotranslateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | given an operator declaration updates the accumulator with the translation
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederto CASL operator, checking if the operator has the assoc attribute to insert
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederit in the map of associative operators, generating the membership predicate
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederinduced by the operator declaration, and checking if it has the ctor
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederattribute to introduce the operator in the generators sentence -}
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescotranslateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
71410be62420b321abb02ef1ac2b7f2141b3bc7fAdrián RiescotranslateOpDecl im (syms, ats) (ops, assoc_ops, cs) = case tl of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [] -> (ops', assoc_ops', cs')
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder _ -> translateOpDecl im (syms', ats) (ops', assoc_ops', cs')
d021fa76efedeeb63529a82dd1cfd81911f4d03eChristian Maeder where sym : tl = Set.toList syms
71410be62420b321abb02ef1ac2b7f2141b3bc7fAdrián Riesco (cop_id, ot, _) = fromJust $ maudeSym2CASLOp im sym
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ops' = MapSet.insert cop_id ot ops
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco assoc_ops' = if any MAS.assoc ats
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder then MapSet.insert cop_id ot assoc_ops
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else assoc_ops
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco cs' = if any MAS.ctor ats
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco then Set.insert (Component cop_id ot) cs
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | translates a Maude operator symbol into a pair with the id of the operator
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederand its CASL type -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermaudeSym2CASLOp :: IdMap -> MSym.Symbol
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescomaudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot, ot')
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco where f = token2id . getName
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder g = (`maudeSymbol2caslSort` im)
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco ot' = CSign.OpType CAS.Total (map f ar) (f co)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeSym2CASLOp _ _ = Nothing
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco-- | creates a conjuctive formula distinguishing the size of the list
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercreateConjForm = CAS.conjunct
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- | creates a implication formula distinguishing the size of the premises
172f4dfb4b858440fab545bac00d3ec4abd0cbe4Adrián RiescocreateImpForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA -> CAS.CASLFORMULA
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercreateImpForm (CAS.Atom True _) form = form
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercreateImpForm form1 form2 = CAS.mkImpl form1 form2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | generates the predicates asserting the "true" sort of the operator if all
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederthe arguments have the correct sort -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederops2predPremises :: IdMap -> [MSym.Symbol] -> Int
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoops2predPremises im (MSym.Sort s : ss) i = (var : terms, form : forms)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where s' = token2id s
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder kind = Map.findWithDefault (errorId "mb of op as predicate")
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name s' pred_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco var = newVarIndex i kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Predication pred_name [var] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (terms, forms) = ops2predPremises im ss (i + 1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where k' = token2id k
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder kind = Map.findWithDefault (errorId "mb of op as predicate")
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco var = newVarIndex i kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (terms, forms) = ops2predPremises im ss (i + 1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoops2predPremises _ _ _ = ([], [])
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | traverses the Maude sentences, returning a pair of list of sentences.
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederThe first list in the pair are the equations without the attribute "owise",
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederwhile the second one are the equations with this attribute -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedersplitOwiseEqs :: [Named MSentence.Sentence] -> ([Named MSentence.Sentence]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , [Named MSentence.Sentence], [Named MSentence.Sentence])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosplitOwiseEqs [] = ([], [], [])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosplitOwiseEqs (s : ss) = res
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sen = sentence s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco res = case sen of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder then (no_owise_sens, s : owise_sens, mbs_rls)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder else (s : no_owise_sens, owise_sens, mbs_rls)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> (no_owise_sens, owise_sens, s : mbs_rls)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | translates a Maude equation defined without the "owise" attribute into
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedera CASL formula -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedernoOwiseSen2Formula :: IdMap -> Named MSentence.Sentence
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoOwiseSen2Formula im s = s'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where MSentence.Equation eq = sentence s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sen' = noOwiseEq2Formula im eq
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco s' = s { sentence = sen' }
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | translates a Maude equation defined with the "owise" attribute into
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedera CASL formula -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederowiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoowiseSen2Formula im owise_forms s = s'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where MSentence.Equation eq = sentence s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sen' = owiseEq2Formula im owise_forms eq
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco s' = s { sentence = sen' }
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates a Maude membership or rule into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb_rl2formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb_rl2formula im s = case sen of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco mb' = mb2formula im mb
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in s { sentence = mb' }
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco rl' = rl2formula im rl
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in s { sentence = rl' }
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder _ -> makeNamed "" CAS.falseForm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where sen = sentence s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates a new variable qualified with the given number
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconewVarIndex :: Int -> Id -> CAS.CASLTERM
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconewVarIndex i sort = CAS.Qual_var var sort nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder where var = mkSimpleId $ 'V' : show i
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates a new variable
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconewVar sort = CAS.Qual_var var sort nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where var = mkSimpleId "V"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | Id for the rew predicate
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescorewID = token2id $ mkSimpleId "rew"
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | translates a Maude equation without the "owise" attribute into a CASL
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA
6f6549c13f912de12345850e4eb248ec358c1b43Adrián RiesconoOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedernoOwiseEq2Formula im (MAS.Eq t t' conds@(_ : _) _) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco conds_form = conds2formula im conds
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder concl_form = CAS.mkStEq ct ct'
172f4dfb4b858440fab545bac00d3ec4abd0cbe4Adrián Riesco form = createImpForm conds_form concl_form
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | transforms a Maude equation defined with the otherwise attribute into
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedera CASL formula -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoowiseEq2Formula :: IdMap -> [Named CAS.CASLFORMULA] -> MAS.Equation
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoowiseEq2Formula im no_owise_form eq = form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where (eq_form, vars) = noQuantification $ noOwiseEq2Formula im eq
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco (op, ts, _) = fromJust $ getLeftApp eq_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ex_form = existencialNegationOtherEqs op ts no_owise_form
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco imp_form = createImpForm ex_form eq_form
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder form = CAS.mkForall vars imp_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates a conjunction of negation of existencial quantifiers
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoexistencialNegationOtherEqs :: CAS.OP_SYMB -> [CAS.CASLTERM] ->
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoexistencialNegationOtherEqs op ts forms = form
d021fa76efedeeb63529a82dd1cfd81911f4d03eChristian Maeder where ex_forms = concatMap (existencialNegationOtherEq op ts) forms
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder form = CAS.conjunct ex_forms
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | given a formula, if it refers to the same operator indicated by the
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederparameters the predicate creates a list with the negation of the existence of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedervariables that match the pattern described in the formula. In other case it
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederreturns an empty list -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederexistencialNegationOtherEq :: CAS.OP_SYMB -> [CAS.CASLTERM]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -> Named CAS.CASLFORMULA -> [CAS.CASLFORMULA]
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederexistencialNegationOtherEq req_op terms form = if ok then let
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco (_, ts, conds) = fromJust tpl
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco ts' = qualifyExVarsTerms ts
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco conds' = qualifyExVarsForms conds
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder prems = createEqs ts' terms ++ conds'
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder conj_form = CAS.conjunct prems
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder ex_form = if null vars' then conj_form else
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder CAS.mkExist vars' conj_form
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder neg_form = CAS.mkNeg ex_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in [neg_form]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where (inner_form, vars) = noQuantification $ sentence form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco vars' = qualifyExVars vars
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco tpl = getLeftApp inner_form
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco ok = case tpl of
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco Nothing -> False
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco Just _ -> let (op, ts, _) = fromJust tpl
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco in req_op == op && length terms == length ts
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | qualifies the variables in a list of formulas with the suffix "_ex" to
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederdistinguish them from the variables already bound -}
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForms :: [CAS.CASLFORMULA] -> [CAS.CASLFORMULA]
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForms = map qualifyExVarsForm
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | qualifies the variables in a formula with the suffix "_ex" to distinguish
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederthem from the variables already bound -}
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederqualifyExVarsForm (CAS.Equation t CAS.Strong t' r) =
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco where qt = qualifyExVarsTerm t
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco qt' = qualifyExVarsTerm t'
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForm (CAS.Predication op ts r) = CAS.Predication op ts' r
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco where ts' = qualifyExVarsTerms ts
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForm f = f
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | qualifies the variables in a list of terms with the suffix "_ex" to
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederdistinguish them from the variables already bound -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerms :: [CAS.CASLTERM] -> [CAS.CASLTERM]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerms = map qualifyExVarsTerm
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | qualifies the variables in a term with the suffix "_ex" to distinguish them
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederfrom the variables already bound -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm :: CAS.CASLTERM -> CAS.CASLTERM
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederqualifyExVarsTerm (CAS.Qual_var var sort r) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder CAS.Qual_var (qualifyExVarAux var) sort r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Application op ts r) = CAS.Application op ts' r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts' = map qualifyExVarsTerm ts
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederqualifyExVarsTerm (CAS.Sorted_term t s r) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder CAS.Sorted_term (qualifyExVarsTerm t) s r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Cast t s r) = CAS.Cast (qualifyExVarsTerm t) s r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Conditional t1 f t2 r) = CAS.Conditional t1' f t2' r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where t1' = qualifyExVarsTerm t1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t2' = qualifyExVarsTerm t2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Mixfix_term ts) = CAS.Mixfix_term ts'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts' = map qualifyExVarsTerm ts
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederqualifyExVarsTerm (CAS.Mixfix_parenthesized ts r) =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts' = map qualifyExVarsTerm ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Mixfix_bracketed ts r) = CAS.Mixfix_bracketed ts' r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts' = map qualifyExVarsTerm ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Mixfix_braced ts r) = CAS.Mixfix_braced ts' r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts' = map qualifyExVarsTerm ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm t = t
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | qualifies a list of variables with the suffix "_ex" to
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederdistinguish them from the variables already bound -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVars :: [CAS.VAR_DECL] -> [CAS.VAR_DECL]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVars = map qualifyExVar
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | qualifies a variable with the suffix "_ex" to distinguish it from
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederthe variables already bound -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVar (CAS.Var_decl vars s r) = CAS.Var_decl vars' s r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where vars' = map qualifyExVarAux vars
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | qualifies a token with the suffix "_ex"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarAux :: Token -> Token
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarAux var = mkSimpleId $ show var ++ "_ex"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates a list of strong equalities from two lists of terms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateEqs :: [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercreateEqs (t1 : ts1) (t2 : ts2) = CAS.mkStEq t1 t2 : ls
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ls = createEqs ts1 ts2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateEqs _ _ = []
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | extracts the operator at the top and the arguments of the lefthand side
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederin a strong equation -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM], [CAS.CASLFORMULA])
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetLeftApp (CAS.Equation term CAS.Strong _ _) = case getLeftAppTerm term of
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco Nothing -> Nothing
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco Just (op, ts) -> Just (op, ts, [])
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetLeftApp (CAS.Relation prem c concl _) = case getLeftApp concl of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Just (op, ts, _) | c /= CAS.Equivalence -> Just (op, ts, conds)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder where conds = getPremisesImplication prem
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetLeftApp _ = Nothing
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | extracts the operator at the top and the arguments of the lefthand side
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederin an application term -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetLeftAppTerm :: CAS.CASLTERM -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetLeftAppTerm (CAS.Application op ts _) = Just (op, ts)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetLeftAppTerm _ = Nothing
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | extracts the formulas of the given premise, distinguishing whether it is
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedera conjunction or not -}
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescogetPremisesImplication :: CAS.CASLFORMULA -> [CAS.CASLFORMULA]
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetPremisesImplication (CAS.Junction CAS.Con forms _) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder concatMap getPremisesImplication forms
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescogetPremisesImplication form = [form]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a Maude membership into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riescomb2formula im (MAS.Mb t s [] _) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco s' = token2id $ getName s
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco form = CAS.Membership ct s' nullRange
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riescomb2formula im (MAS.Mb t s conds@(_ : _) _) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco s' = token2id $ getName s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco conds_form = conds2formula im conds
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco concl_form = CAS.Membership ct s' nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder form = CAS.mkImpl conds_form concl_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a Maude rule into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescorl2formula :: IdMap -> MAS.Rule -> CAS.CASLFORMULA
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riescorl2formula im (MAS.Rl t t' [] _) = quantifyUniversally form
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco where ty = token2id $ getName $ MAS.getTermType t
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "rl to formula") ty im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name rewID pred_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Predication pred_name [ct, ct'] nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederrl2formula im (MAS.Rl t t' conds@(_ : _) _) = quantifyUniversally form
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco where ty = token2id $ getName $ MAS.getTermType t
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "rl to formula") ty im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name rewID pred_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco conds_form = conds2formula im conds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco concl_form = CAS.Predication pred_name [ct, ct'] nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder form = CAS.mkImpl conds_form concl_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a conjunction of Maude conditions to a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoconds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederconds2formula im conds = CAS.conjunct forms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where forms = map (cond2formula im) conds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a single Maude condition to a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescocond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedercond2formula im (MAS.EqCond t t') = CAS.mkStEq ct ct'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedercond2formula im (MAS.MatchCond t t') = CAS.mkStEq ct ct'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
6f6549c13f912de12345850e4eb248ec358c1b43Adrián Riescocond2formula im (MAS.MbCond t s) = CAS.Membership ct s' nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco s' = token2id $ getName s
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedercond2formula im (MAS.RwCond t t') = CAS.mkPredication pred_name [ct, ct']
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ty = token2id $ getName $ MAS.getTermType t
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "rw cond to formula") ty im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name rewID pred_type nullRange
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | translates a Maude term into a CASL term
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeTerm2caslTerm :: IdMap -> MAS.Term -> CAS.CASLTERM
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescomaudeTerm2caslTerm im (MAS.Var q ty) = CAS.Qual_var q ty' nullRange
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco where ty' = maudeType2caslSort ty im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescomaudeTerm2caslTerm im (MAS.Const q ty) = CAS.Application op [] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where name = token2id q
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco ty' = maudeType2caslSort ty im
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco op_type = CAS.Op_type CAS.Total [] ty' nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco op = CAS.Qual_op_name name op_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescomaudeTerm2caslTerm im (MAS.Apply q ts ty) = CAS.Application op tts nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where name = token2id q
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco tts = map (maudeTerm2caslTerm im) ts
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco ty' = maudeType2caslSort ty im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco types_tts = getTypes tts
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco op_type = CAS.Op_type CAS.Total types_tts ty' nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco op = CAS.Qual_op_name name op_type nullRange
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescomaudeSymbol2caslSort :: MSym.Symbol -> IdMap -> CAS.SORT
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescomaudeSymbol2caslSort (MSym.Sort q) _ = token2id q
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescomaudeSymbol2caslSort (MSym.Kind q) im = Map.findWithDefault err q' im
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco where q' = token2id q
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco err = errorId "error translate symbol"
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescomaudeSymbol2caslSort _ _ = errorId "error translate symbol"
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescomaudeType2caslSort :: MAS.Type -> IdMap -> CAS.SORT
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescomaudeType2caslSort (MAS.TypeSort q) _ = token2id $ getName q
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescomaudeType2caslSort (MAS.TypeKind q) im = Map.findWithDefault err q' im
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco where q' = token2id $ getName q
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco err = errorId "error translate type"
6e121321775373fe11161d23c541437456df19b4Adrián Riesco-- | obtains the types of the given terms
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetTypes :: [CAS.CASLTERM] -> [Id]
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetTypes = mapMaybe getType
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | extracts the type of the temr
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetType :: CAS.CASLTERM -> Maybe Id
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetType (CAS.Qual_var _ kind _) = Just kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetType (CAS.Application op _ _) = case op of
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco CAS.Qual_op_name _ (CAS.Op_type _ _ kind _) _ -> Just kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetType _ = Nothing
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco-- | generates the formulas for the rewrite predicates
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescorewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescorewPredicatesSens = Set.fold rewPredicateSens []
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates the formulas for the rewrite predicate of the given sort
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescorewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescorewPredicateSens kind acc = ref : trans : acc
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where ref = reflSen kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco trans = transSen kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | creates the reflexivity predicate for the given kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoreflSen :: Id -> Named CAS.CASLFORMULA
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoreflSen kind = makeNamed name $ quantifyUniversally form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where v = newVar kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pn = CAS.Qual_pred_name rewID pred_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form = CAS.Predication pn [v, v] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name = "rew_refl_" ++ show kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | creates the transitivity predicate for the given kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotransSen :: Id -> Named CAS.CASLFORMULA
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotransSen kind = makeNamed name $ quantifyUniversally form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where v1 = newVarIndex 1 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v2 = newVarIndex 2 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v3 = newVarIndex 3 kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pn = CAS.Qual_pred_name rewID pred_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco prem1 = CAS.Predication pn [v1, v2] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco prem2 = CAS.Predication pn [v2, v3] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco concl = CAS.Predication pn [v1, v3] nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder conj_form = CAS.conjunct [prem1, prem2]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder form = CAS.mkImpl conj_form concl
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name = "rew_trans_" ++ show kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | generate the predicates for the rewrites
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrewPredicates :: Set.Set Id -> CSign.PredMap
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrewPredicates = Set.fold rewPredicate MapSet.empty
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generate the predicates for the rewrites of the given sort
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrewPredicate :: Id -> CSign.PredMap -> CSign.PredMap
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrewPredicate kind = MapSet.insert rewID $ CSign.PredType [kind, kind]
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | create the predicates that assign sorts to each term
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescokindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)
a74f814d3b445eadad6f68737a98a7a303698affChristian MaederkindPredicates = Map.foldWithKey kindPredicate Map.empty
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | create the predicates that assign the current sort to the
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedercorresponding terms -}
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescokindPredicate :: Id -> Id -> Map.Map Id (Set.Set CSign.PredType)
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederkindPredicate sort kind mis = if sort == str2id "Universal" then mis else
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let ar = Set.singleton $ CSign.PredType [kind]
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | extract the kinds from the map of id's
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescokindsFromMap :: IdMap -> Set.Set Id
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | transform the set of Maude sorts in a set of CASL sorts, including
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederonly one sort for each kind. -}
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescosortsTranslation :: MSign.SortSet -> MSign.SubsortRel -> Set.Set Id
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedersortsTranslation = sortsTranslationList . Set.toList
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | transform a list representing the Maude sorts in a set of CASL sorts,
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederincluding only one sort for each kind. -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosortsTranslationList :: [MSym.Symbol] -> MSign.SubsortRel -> Set.Set Id
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescosortsTranslationList [] _ = Set.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosortsTranslationList (s : ss) r = Set.insert (sort2id tops) res
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where tops@(top : _) = List.sort $ getTop r s
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco ss' = deleteRelated ss top r
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco res = sortsTranslation ss' r
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco-- | return the maximal elements from the sort relation
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetTop r tok = case succs of
d021fa76efedeeb63529a82dd1cfd81911f4d03eChristian Maeder toks@(_ : _) -> concatMap (getTop r) toks
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | delete from the list of sorts those in the same kind that the parameter
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederdeleteRelated :: [MSym.Symbol] -> MSym.Symbol -> MSign.SubsortRel
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescodeleteRelated ss sym r = foldr (f sym tc) Set.empty ss
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder f sort trC x y = if MSym.sameKind trC sort x
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | build an Id from a token with the function mkId
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescotoken2id :: Token -> Id
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riescotoken2id t = mkId ts
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco where ts = maudeSymbol2validCASLSymbol t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | build an Id from a Maude symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescosym2id :: MSym.Symbol -> Id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescosym2id = token2id . getName
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates an Id from a string
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riescostr2id :: String -> Id
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riescostr2id = token2id . mkSimpleId
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco-- | build an Id from a list of sorts, taking the first from the ordered list
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescosort2id :: [MSym.Symbol] -> Id
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riescosort2id syms = mkId sym''
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder where sym : _ = List.sort syms
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco sym' = getName sym
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco sym'' = maudeSymbol2validCASLSymbol sym'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | add universal quantification of all variables in the formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoquantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederquantifyUniversally form = CAS.mkForall var_decl form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where vars = getVars form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco var_decl = listVarDecl vars
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | traverses a map with sorts as keys and sets of variables as value and
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedercreates a list of variable declarations -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescolistVarDecl :: Map.Map Id (Set.Set Token) -> [CAS.VAR_DECL]
a74f814d3b445eadad6f68737a98a7a303698affChristian MaederlistVarDecl = Map.foldWithKey f []
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder where f sort var_set =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (CAS.Var_decl (Set.toList var_set) sort nullRange :)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | removes a quantification from a formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoQuantification :: CAS.CASLFORMULA -> (CAS.CASLFORMULA, [CAS.VAR_DECL])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoQuantification (CAS.Quantification _ vars form _) = (form, vars)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoQuantification form = (form, [])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate the CASL sorts to symbols
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescokinds2syms :: Set.Set Id -> Set.Set CSign.Symbol
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riescokinds2syms = Set.map kind2sym
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a CASL sort to a CASL symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescokind2sym :: Id -> CSign.Symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescokind2sym k = CSign.Symbol k CSign.SortAsItemType
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates the CASL predicates into CASL symbols
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederpreds2syms :: CSign.PredMap -> Set.Set CSign.Symbol
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederpreds2syms = MapSet.foldWithKey createSym4id Set.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates a CASL symbol for a predicate
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercreateSym4id :: Id -> CSign.PredType -> Set.Set CSign.Symbol
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercreateSym4id pn pt = Set.insert sym
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where sym = CSign.Symbol pn $ CSign.PredAsItemType pt
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates the CASL operators into CASL symbols
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoops2symbols :: CSign.OpMap -> Set.Set CSign.Symbol
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederops2symbols = MapSet.foldWithKey createSymOp4id Set.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates a CASL symbol for an operator
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercreateSymOp4id :: Id -> CSign.OpType -> Set.Set CSign.Symbol
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedercreateSymOp4id on ot = Set.insert sym
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where sym = CSign.Symbol on $ CSign.OpAsItemType ot
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | extract the variables from a CASL formula and put them in a map
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederwith keys the sort of the variables and value the set of variables
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederin this sort -}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars :: CAS.CASLFORMULA -> Map.Map Id (Set.Set Token)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Quantification _ _ f _) = getVars f
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetVars (CAS.Junction _ fs _) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder foldr (Map.unionWith Set.union . getVars) Map.empty fs
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetVars (CAS.Relation f1 _ f2 _) = Map.unionWith Set.union v1 v2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = getVars f1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = getVars f2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Negation f _) = getVars f
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetVars (CAS.Predication _ ts _) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Definedness t _) = getVarsTerm t
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetVars (CAS.Equation t1 _ t2 _) = Map.unionWith Set.union v1 v2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = getVarsTerm t1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = getVarsTerm t2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Membership t _ _) = getVarsTerm t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Mixfix_formula t) = getVarsTerm t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | extract the variables of a CASL term
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm :: CAS.CASLTERM -> Map.Map Id (Set.Set Token)
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetVarsTerm (CAS.Qual_var var sort _) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Map.insert sort (Set.singleton var) Map.empty
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetVarsTerm (CAS.Application _ ts _) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Cast t _ _) = getVarsTerm t
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetVarsTerm (CAS.Conditional t1 f t2 _) = Map.unionWith Set.union v3 m
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = getVarsTerm t1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = getVarsTerm t2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v3 = getVars f
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetVarsTerm (CAS.Mixfix_term ts) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescogetVarsTerm (CAS.Mixfix_parenthesized ts _) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescogetVarsTerm (CAS.Mixfix_bracketed ts _) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Mixfix_braced ts _) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescogetVarsTerm _ = Map.empty
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco-- | generates the constructor constraint
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescoctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederctorSen isFree (sorts, _, ops) =
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco let sortList = Set.toList sorts
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (CSign.toOP_TYPE $ compType c) $ posOfId ide)
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco allSyms = opSyms
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco resType _ (CAS.Op_name _) = False
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco resType s (CAS.Qual_op_name _ t _) = CAS.res_OP_TYPE t == s
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder getIndex s = fromMaybe (-1) $ List.elemIndex s sortList
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco addIndices (CAS.Op_name _) =
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco error "CASL/StaticAna: Internal error in function addIndices"
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco addIndices os@(CAS.Qual_op_name _ t _) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (os, map getIndex $ CAS.args_OP_TYPE t)
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco collectOps s =
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco constrs = map collectOps sortList
eae727f2a1203f1e3c86e40667fe6dfb1173abcbcmaeder f = CAS.mkSort_gen_ax constrs isFree
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder ("ga_generated_" ++ showSepList (showString "_") showId sortList "") f
6e121321775373fe11161d23c541437456df19b4Adrián Riesco-- | transforms a maude identifier into a valid CASL identifier
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescomaudeSymbol2validCASLSymbol :: Token -> [Token]
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescomaudeSymbol2validCASLSymbol t = splitDoubleUnderscores str ""
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco where str = ms2vcs $ show t
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | transforms a string coding a Maude identifier into another string
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederrepresenting a CASL identifier -}
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riescoms2vcs :: String -> String
ebdb7b09e2ad2bb780d84c127d72c30dfcfb87b2Adrián Riescoms2vcs s@('k' : 'i' : 'n' : 'd' : '_' : _) = s
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederms2vcs s = if Map.member s stringMap
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder then stringMap Map.! s
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder else let f x y
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder | Map.member x charMap = (charMap Map.! x) ++ "'" ++ y
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder | x == '_' = "__" ++ y
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder | otherwise = x : y
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder in foldr f [] s
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco-- | map of reserved words
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescostringMap :: Map.Map String String
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco [("true", "maudeTrue"),
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco ("false", "maudeFalse"),
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco ("not_", "neg__"),
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco ("s_", "suc"),
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco ("_+_", "__+__"),
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco ("_*_", "__*__"),
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco ("_<_", "__<__"),
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco ("_<=_", "__<=__"),
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco ("_>_", "__>__"),
b3a8ae62887130fd41b91bf2ea1fd66360bd3c29Adrián Riesco ("_>=_", "__>=__"),
b3a8ae62887130fd41b91bf2ea1fd66360bd3c29Adrián Riesco ("_and_", "__maudeAnd__")]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | splits the string into a list of tokens, separating the double
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederunderscores from the rest of characters -}
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescosplitDoubleUnderscores :: String -> String -> [Token]
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescosplitDoubleUnderscores [] acc = if null acc
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco else [mkSimpleId acc]
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescosplitDoubleUnderscores ('_' : '_' : cs) acc = if null acc
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco then dut : rest
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco else acct : dut : rest
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco where acct = mkSimpleId acc
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco dut = mkSimpleId "__"
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco rest = splitDoubleUnderscores cs []
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescosplitDoubleUnderscores (c : cs) acc = splitDoubleUnderscores cs (acc ++ [c])
7474965b2e6323002c96c0b39a59843cde201870Adrián RiescoerrorId :: String -> Id
7474965b2e6323002c96c0b39a59843cde201870Adrián RiescoerrorId s = token2id $ mkSimpleId $ "ERROR: " ++ s
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescokindId :: Id -> Id
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián RiescokindId i = token2id $ mkSimpleId $ "kind_" ++ show i
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescokindMapId :: MSign.KindRel -> IdMap
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescokindMapId kr = Map.fromList krl'
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco where krl = Map.toList kr
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco krl' = map (\ (x, y) -> (mSym2caslId x, mSym2caslId y)) krl
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescomSym2caslId :: MSym.Symbol -> Id
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescomSym2caslId (MSym.Sort q) = token2id q
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescomSym2caslId (MSym.Kind q) = kindId q'
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco where q' = token2id q
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescomSym2caslId _ = errorId "error translate symbol"
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco-- | checks the profile has at least one sort
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoatLeastOneSort om = Map.fromList lom'
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco where lom = Map.toList om
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco lom' = filterAtLeastOneSort lom
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederfilterAtLeastOneSort :: [(MAS.Qid, MSign.OpDeclSet)]
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescofilterAtLeastOneSort [] = []
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescofilterAtLeastOneSort ((q, ods) : ls) = hd ++ filterAtLeastOneSort ls
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco where ods' = atLeastOneSortODS ods
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco else [(q, ods')]
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoatLeastOneSortODS :: MSign.OpDeclSet -> MSign.OpDeclSet
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoatLeastOneSortODS ods = Set.fromList lods'
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco where lods = Set.toList ods
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco lods' = atLeastOneSortLODS lods
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoatLeastOneSortLODS :: [MSign.OpDecl] -> [MSign.OpDecl]
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoatLeastOneSortLODS [] = []
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoatLeastOneSortLODS ((ss, ats) : ls) = res ++ atLeastOneSortLODS ls
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco where ss' = atLeastOneSortSS ss
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco else [(ss', ats)]
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoatLeastOneSortSS :: Set.Set MSym.Symbol -> Set.Set MSym.Symbol
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoatLeastOneSortSS = Set.filter hasOneSort
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescohasOneSort :: MSym.Symbol -> Bool
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescohasOneSort (MSym.Operator _ ar co) = any isSymSort (co : ar)
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescohasOneSort _ = False
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoisSymSort :: MSym.Symbol -> Bool
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoisSymSort (MSym.Sort _) = True
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescoisSymSort _ = False
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | translates the Maude operator map into a tuple of CASL operators, CASL
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederassociative operators, membership induced from each Maude operator,
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederand the set of sorts with the ctor attribute -}
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescotranslateOps' :: IdMap -> MSign.OpMap -> OpTransTuple
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedertranslateOps' im = Map.fold (translateOpDeclSet' im)
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco-- | translates an operator declaration set into a tern as described above
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescotranslateOpDeclSet' :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescotranslateOpDeclSet' im ods tpl = Set.fold (translateOpDecl' im) tpl ods
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | given an operator declaration updates the accumulator with the translation
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederto CASL operator, checking if the operator has the assoc attribute to insert
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederit in the map of associative operators, generating the membership predicate
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederinduced by the operator declaration, and checking if it has the ctor
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederattribute to introduce the operator in the generators sentence -}
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescotranslateOpDecl' :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
d021fa76efedeeb63529a82dd1cfd81911f4d03eChristian MaedertranslateOpDecl' im (syms, ats) (ops, assoc_ops, cs) =
d021fa76efedeeb63529a82dd1cfd81911f4d03eChristian Maeder then (ops', assoc_ops', cs')
d021fa76efedeeb63529a82dd1cfd81911f4d03eChristian Maeder else translateOpDecl' im (syms', ats) (ops', assoc_ops', cs')
d021fa76efedeeb63529a82dd1cfd81911f4d03eChristian Maeder where (sym, syms') = Set.deleteFindMin syms
d021fa76efedeeb63529a82dd1cfd81911f4d03eChristian Maeder Just (cop_id, ot, _) = maudeSym2CASLOp' im sym
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ops' = MapSet.insert cop_id ot ops
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco assoc_ops' = if any MAS.assoc ats
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder then MapSet.insert cop_id ot assoc_ops
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco else assoc_ops
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco cs' = if any MAS.ctor ats
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco then Set.insert (Component cop_id ot) cs
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder{- | translates a Maude operator symbol into a pair with the id of the operator
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederand its CASL type -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermaudeSym2CASLOp' :: IdMap -> MSym.Symbol
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescomaudeSym2CASLOp' im (MSym.Operator op ar co) = Just (token2id op, ot, ot')
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco where f = token2id . getName
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder g = (`maudeSymbol2caslSort'` im)
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco ot' = CSign.OpType CAS.Total (map f ar) (f co)
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescomaudeSym2CASLOp' _ _ = Nothing
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescomaudeSymbol2caslSort' :: MSym.Symbol -> IdMap -> CAS.SORT
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermaudeSymbol2caslSort' (MSym.Sort q) _ =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder token2id $ mkSimpleId $ "kind_" ++ show q
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescomaudeSymbol2caslSort' (MSym.Kind q) im = Map.findWithDefault err q' im
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco where q' = token2id q
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco err = errorId "error translate symbol"
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescomaudeSymbol2caslSort' _ _ = errorId "error translate symbol"