PreComorphism.hs revision fe5611d78ea0648e8719cb004a6a26e9a033429a
a530dde7009b0a808300c420def741354a4d13d2Martin KühlModule : $Header$
a530dde7009b0a808300c420def741354a4d13d2Martin KühlDescription : Maude Comorphisms
a530dde7009b0a808300c420def741354a4d13d2Martin KühlCopyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescotype IdMap = Map.Map Id Id
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riescotype OpTransTuple = (CSign.OpMap, CSign.OpMap, [Named CAS.CASLFORMULA], Set.Set Component)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates a CASL morphism from a Maude morphism
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapMorphism :: MMorphism.Morphism -> Result (CMorphism.CASLMor)
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescomapMorphism morph =
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco mk = arrangeKinds (MSign.sorts src) (MSign.subsorts src)
6e121321775373fe11161d23c541437456df19b4Adrián Riesco cs = kindsFromMap mk
6e121321775373fe11161d23c541437456df19b4Adrián Riesco smap' = applySortMap2CASLSorts smap cs
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 ()
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates the Maude morphism between operators into a CASL morpshim between
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map
a74f814d3b445eadad6f68737a98a7a303698affChristian MaedermaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates the mapping between two symbols representing operators into
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- a CASL operators map
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm = copm'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where f = token2id . getName
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco g = \ x -> Map.findWithDefault (errorId "translate op map entry") (f x) im
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 = arrangeKinds (MSign.sorts sg) (MSign.subsorts 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 = arrangeKinds (MSign.sorts sg) (MSign.subsorts 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
7474965b2e6323002c96c0b39a59843cde201870Adrián RiescomaudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id") (token2id $ getName sym) im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates the predicate map for the CASL morphism from the Maude sort map and
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- the 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreatePredMap4sort im from to m = Map.insert key id_to m
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where id_from = token2id $ getName from
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco id_to = token2id $ getName to
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "predicate for sort") id_from im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco key = (id_from, CSign.PredType [kind])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | computes the sort morphism of CASL from the sort morphism in Maude and the set
6e121321775373fe11161d23c541437456df19b4Adrián RiescoapplySortMap2CASLSorts :: MMorphism.SortMap -> Set.Set Id -> CMorphism.Sort_map
6e121321775373fe11161d23c541437456df19b4Adrián RiescoapplySortMap2CASLSorts sm = Set.fold (applySortMap2CASLSort sm) Map.empty
6e121321775373fe11161d23c541437456df19b4Adrián Riesco-- | computes the morphism for a single kind
6e121321775373fe11161d23c541437456df19b4Adrián RiescoapplySortMap2CASLSort :: MMorphism.SortMap -> Id -> CMorphism.Sort_map -> CMorphism.Sort_map
6e121321775373fe11161d23c541437456df19b4Adrián RiescoapplySortMap2CASLSort sm sort csm = new_csm
6e121321775373fe11161d23c541437456df19b4Adrián Riesco where toks = getTokens sort
6e121321775373fe11161d23c541437456df19b4Adrián Riesco new_toks = map (rename sm) toks
6e121321775373fe11161d23c541437456df19b4Adrián Riesco new_sort = mkId new_toks
6e121321775373fe11161d23c541437456df19b4Adrián Riesco new_csm = if new_sort == sort
6e121321775373fe11161d23c541437456df19b4Adrián Riesco else Map.insert sort new_sort csm
6e121321775373fe11161d23c541437456df19b4Adrián Riesco-- | renames the sorts in a given kind
6e121321775373fe11161d23c541437456df19b4Adriá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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSentence sg sen@(MSentence.Equation eq) = case any MAS.owise ats of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco False -> return $ sentence $ noOwiseSen2Formula mk named
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco (no_owise_sens, _, _) = splitOwiseEqs sg_sens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco trans = sentence $ owiseSen2Formula mk no_owise_forms named
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in return trans
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco MAS.Eq _ _ _ ats = eq
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco named = makeNamed "" sen
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescomapSentence sg sen@(MSentence.Membership mb) = return $ sentence form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco named = makeNamed "" sen
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco form = mb_rl2formula mk named
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSentence sg sen@(MSentence.Rule rl) = return $ sentence form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco named = makeNamed "" sen
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco form = mb_rl2formula mk named
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | applies maude2casl to compute the CASL signature and sentences from
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- the Maude ones, and wraps them into a Result datatype
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapTheory :: (MSign.Sign, [Named MSentence.Sentence])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapTheory (sg, nsens) = return $ maude2casl sg nsens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | computes new signature and sentences of CASL associated to the
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- given Maude signature and sentences
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescomaude2casl :: MSign.Sign -> [Named MSentence.Sentence]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomaude2casl msign nsens = (csign { CSign.sortSet = cs,
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco CSign.declaredSymbols = syms }, new_sens)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where csign = CSign.emptySign ()
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco mk = arrangeKinds (MSign.sorts msign) (MSign.subsorts msign)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco cs = kindsFromMap mk
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ks = kindPredicates mk
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco rp = rewPredicates ks cs
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco rs = rewPredicatesSens cs
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco ops = deleteUniversal $ MSign.ops msign
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco ksyms = kinds2syms cs
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco (cops, assoc_ops, ops_forms, comps) = translateOps mk ops
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco ctor_sen = [ctorSen False (cs, Rel.empty, comps)]
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco cops' = universalOps cs cops $ booleanImported ops
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco rs' = rewPredicatesCongSens cops'
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco pred_forms = loadLibraries (MSign.sorts msign) ops
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco ops_syms = ops2symbols cops'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens
ab9c6be005cb2af851307b7968c2baa16a76d6b1Adrián Riesco no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens
5eb747ed1f9cb3d902d4277badfc2a42f9f98b0cAdrián Riesco mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco preds_syms = preds2syms preds
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco syms = Set.union ksyms $ Set.union ops_syms preds_syms
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco new_sens = concat [rs, rs', ops_forms, no_owise_forms, owise_forms,
3f8cdebaede9921402318d525b57a9af8f9279d3Adrián Riesco mb_rl_forms, ctor_sen, pred_forms]
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco-- | generates the sentences to state that the rew predicates are a congruence
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescorewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescorewPredicatesCongSens = Map.foldWithKey rewPredCongSet []
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco-- | generates the sentences to state that the rew predicates are a congruence
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco-- for the operator types in the set
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescorewPredCongSet :: Id -> Set.Set CSign.OpType -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescorewPredCongSet idn ots fs = fs ++ fs'
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco where fs' = Set.fold (rewPredCong idn) [] ots
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco-- | generates the sentences to state that the rew predicates are a congruence
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco-- for a single operator
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescorewPredCong :: Id -> CSign.OpType -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescorewPredCong op ot fs = case args of
0f593bb6e3f0bc82abf3d6d3c76ef222a43d0476Adrián Riesco _ -> nq_form : fs
0f593bb6e3f0bc82abf3d6d3c76ef222a43d0476Adrián Riesco where args = CSign.opArgs ot
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco vars1 = rewPredCongPremise 0 args
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco vars2 = rewPredCongPremise (length args) args
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco res_pred_type = CAS.Pred_type [res, res] nullRange
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco pn = CAS.Qual_pred_name rewID res_pred_type nullRange
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco name = "rew_cong_" ++ show op
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco prems = rewPredsCong args vars1 vars2
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco prems_conj = createConjForm prems
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco os = CAS.Qual_op_name op (CSign.toOP_TYPE ot) nullRange
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco conc_term1 = CAS.Application os vars1 nullRange
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco conc_term2 = CAS.Application os vars2 nullRange
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco conc_form = CAS.Predication pn [conc_term1, conc_term2] nullRange
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco form = createImpForm prems_conj conc_form
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco nq_form = makeNamed name $ quantifyUniversally form
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco-- | generates a list of variables of the given sorts
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescorewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescorewPredCongPremise n (s : ss) = newVarIndex n s : rewPredCongPremise (n + 1) ss
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescorewPredCongPremise _ [] = []
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder-- | generates a list of rew predicates with the given variables
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescorewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]
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 _ _ _ = []
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- | load the CASL libraries for the Maude built-in operators
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescoloadLibraries :: MSign.SortSet -> MSign.OpMap -> [Named CAS.CASLFORMULA]
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescoloadLibraries ss om = case natImported ss om of
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco True -> loadNaturalNatSens
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- | loads the sentences associated to the natural numbers
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescoloadNaturalNatSens :: [Named CAS.CASLFORMULA]
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescoloadNaturalNatSens =
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco let lib = head $ unsafePerformIO $ readLib "Maude/MaudeNumbers.casl"
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco in case lib of
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco G_theory lid _ _ thSens _ -> let sens = toNamedList thSens
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco sens' <- coerceSens lid CASL "" sens
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco filter (not . ctorCons) sens'
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- | checks if a sentence is an constructor sentence
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescoctorCons :: Named CAS.CASLFORMULA -> Bool
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescoctorCons f = case sentence f of
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- | checks if the boolean values are imported
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescobooleanImported :: MSign.OpMap -> Bool
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescobooleanImported = Map.member (mkSimpleId "if_then_else_fi")
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- | checks if the natural numbers are imported
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiesconatImported :: MSign.SortSet -> MSign.OpMap -> Bool
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiesconatImported ss om = b1 && b2 && b3
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco where b1 = Set.member (MSym.Sort $ mkSimpleId "Nat") ss
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco b2 = Map.member (mkSimpleId "0") om
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco b3 = case b2 of
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco False -> True
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco True -> specialZeroSet $ om Map.! (mkSimpleId "0")
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescospecialZeroSet :: MSign.OpDeclSet -> Bool
223be434693e8c97e2522ac19155a284b3536035Adrián RiescospecialZeroSet = Set.fold specialZero False
223be434693e8c97e2522ac19155a284b3536035Adrián RiescospecialZero :: MSign.OpDecl -> Bool -> Bool
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescospecialZero (_, ats) b = b' || b
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco where b' = isSpecial ats
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoisSpecial :: [MAS.Attr] -> Bool
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescoisSpecial [] = False
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoisSpecial ((MAS.Special _) : _) = True
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoisSpecial (_ : ats) = isSpecial ats
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | delete the universal operators from Maude specifications, that will be
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- substituted for one operator for each sort in the specification
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescodeleteUniversal om = om5
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco where om1 = Map.delete (mkSimpleId "if_then_else_fi") om
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco om2 = Map.delete (mkSimpleId "_==_") om1
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco om3 = Map.delete (mkSimpleId "_=/=_") om2
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco om4 = Map.delete (mkSimpleId "upTerm") om3
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco om5 = Map.delete (mkSimpleId "downTerm") om4
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates the universal operators for all the sorts in the module
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescouniversalOps :: Set.Set Id -> CSign.OpMap -> Bool -> CSign.OpMap
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescouniversalOps kinds om True = Set.fold universalOpKind om kinds
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescouniversalOps _ om False = om
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco-- | generates the universal operators for a concrete module
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescouniversalOpKind :: Id -> CSign.OpMap -> CSign.OpMap
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescouniversalOpKind kind om = om3
0be63c5d4b5e66cc600a0003081ae2bf85be9615Adrián Riesco where if_id = str2id "if_then_else_fi"
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco double_eq_id = str2id "_==_"
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco neg_double_eq_id = str2id "_=/=_"
0be63c5d4b5e66cc600a0003081ae2bf85be9615Adrián Riesco bool_id = str2id "Bool"
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco if_opt = Set.singleton $ CSign.OpType CAS.Total [bool_id, kind, kind] kind
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco eq_opt = Set.singleton $ CSign.OpType CAS.Total [kind, kind] bool_id
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco om1 = Map.insertWith Set.union if_id if_opt om
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco om2 = Map.insertWith Set.union double_eq_id eq_opt om1
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco om3 = Map.insertWith Set.union neg_double_eq_id eq_opt om2
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco-- | generates the formulas for the universal operators
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescouniversalSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescouniversalSens = Set.fold universalSensKind []
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco-- | generates the formulas for the universal operators for the given sort
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescouniversalSensKind :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
223be434693e8c97e2522ac19155a284b3536035Adrián RiescouniversalSensKind kind acc = concat [iss, eqs, neqs, acc]
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco where iss = ifSens kind
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco eqs = equalitySens kind
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco neqs = nonEqualitySens kind
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco-- | generates the formulas for the if statement
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián RiescoifSens :: Id -> [Named CAS.CASLFORMULA]
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián RiescoifSens kind = [form'', neg_form'']
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco where v1 = newVarIndex 1 kind
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco v2 = newVarIndex 2 kind
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco bk = str2id "Bool"
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco bv = newVarIndex 2 bk
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco true_type = CAS.Op_type CAS.Total [] bk nullRange
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco true_id = CAS.Qual_op_name (str2id "true") true_type nullRange
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco true_term = CAS.Application true_id [] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco if_type = CAS.Op_type CAS.Total [bk, kind, kind] kind nullRange
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco if_name = str2id "if_then_else_fi"
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco if_id = CAS.Qual_op_name if_name if_type nullRange
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco if_term = CAS.Application if_id [bv, v1, v2] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco prem = CAS.Strong_equation bv true_term nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco concl = CAS.Strong_equation if_term v1 nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco form = CAS.Implication prem concl True nullRange
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco form' = quantifyUniversally form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_prem = CAS.Negation prem nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_concl = CAS.Strong_equation if_term v2 nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_form = CAS.Implication neg_prem neg_concl True nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_form' = quantifyUniversally neg_form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name1 = show kind ++ "_if_true"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name2 = show kind ++ "_if_false"
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco form'' = makeNamed name1 form'
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco neg_form'' = makeNamed name2 neg_form'
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | generates the formulas for the equality
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoequalitySens :: Id -> [Named CAS.CASLFORMULA]
223be434693e8c97e2522ac19155a284b3536035Adrián RiescoequalitySens kind = [form'', comp_form'']
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco where v1 = newVarIndex 1 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v2 = newVarIndex 2 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco bk = str2id "Bool"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco b_type = CAS.Op_type CAS.Total [] bk nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco true_term = CAS.Application true_id [] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco false_term = CAS.Application false_id [] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco prem = CAS.Strong_equation v1 v2 nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind nullRange
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco double_eq_name = str2id "_==_"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco concl = CAS.Strong_equation double_eq_term true_term nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form = CAS.Implication prem concl True nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco form' = quantifyUniversally form
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco neg_prem = CAS.Negation prem nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco new_concl = CAS.Strong_equation double_eq_term false_term nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco comp_form = CAS.Implication neg_prem new_concl True nullRange
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'
aea9000fc94442cbfc92596f4264473c0fce51e4Adriá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
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco bk = str2id "Bool"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco b_type = CAS.Op_type CAS.Total [] bk nullRange
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco true_term = CAS.Application true_id [] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco false_term = CAS.Application false_id [] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco prem = CAS.Strong_equation v1 v2 nullRange
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco double_eq_name = str2id "_==_"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco concl = CAS.Strong_equation double_eq_term false_term nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form = CAS.Implication prem concl True nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form' = quantifyUniversally form
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco neg_prem = CAS.Negation prem nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco new_concl = CAS.Strong_equation double_eq_term true_term nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco comp_form = CAS.Implication neg_prem new_concl True nullRange
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'
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | translates the Maude operator map into a tuple of CASL operators, CASL
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- associative operators, membership induced from each Maude operator,
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- and the set of sorts with the ctor attribute
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotranslateOps :: IdMap -> MSign.OpMap -> OpTransTuple
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotranslateOps im = Map.fold (translateOpDeclSet im) (Map.empty, Map.empty, [], Set.empty)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | translates an operator declaration set into a tern as described above
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescotranslateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotranslateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | given an operator declaration updates the accumulator with the translation
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- to CASL operator, checking if the operator has the assoc attribute to insert
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco-- it in the map of associative operators, generating the membership predicate
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco-- induced by the operator declaration, and checking if it has the ctor attribute
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco-- to introduce the operator in the generators sentence
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotranslateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescotranslateOpDecl im (syms, ats) (ops, assoc_ops, forms, cs) = (ops', assoc_ops', forms', cs')
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where predOps = ops2pred im syms
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco sym = head $ Set.toList syms
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco (cop_id, ot) = fromJust $ maudeSym2CASLOp im sym
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco forms' = forms ++ predOps
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco ops' = Map.insertWith (Set.union) cop_id cop_type ops
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco assoc_ops' = if any MAS.assoc ats
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco then Map.insertWith (Set.union) cop_id cop_type assoc_ops
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco else assoc_ops
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco cs' = if any MAS.ctor ats
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco then Set.insert (Component cop_id ot) cs
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | translates a Maude operator symbol into a pair with the id of the operator
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- and its CASL type
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescomaudeSym2CASLOp :: IdMap -> MSym.Symbol -> Maybe (Id, CSign.OpType)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescomaudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where f = token2id . getName
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco g = \ x -> Map.findWithDefault (errorId "Maude_sym2CASL_sym") (f x) im
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescomaudeSym2CASLOp _ _ = Nothing
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco-- | generates the predicates associated to each operator declaration in Maude
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco-- due to the associated membership if the coarity is a sort and not a kind
357381f0a999099cd2d4c268006df56b47847d68Adrián Riescoops2pred :: IdMap -> MSym.SymbolSet -> [Named CAS.CASLFORMULA]
357381f0a999099cd2d4c268006df56b47847d68Adrián Riescoops2pred im = Set.fold (op2pred im) []
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco-- | generates the membership predicate associated to an operator
357381f0a999099cd2d4c268006df56b47847d68Adrián Riescoop2pred :: IdMap -> MSym.Symbol -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
357381f0a999099cd2d4c268006df56b47847d68Adrián Riescoop2pred im (MSym.Operator op ar co) acc = case co of
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco co' = token2id s
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco kind = Map.findWithDefault (errorId "op-mb to predicate") co' im
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco f = \ m x -> Map.lookup (token2id $ getName x) m
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco ar' = mapMaybe (f im) ar
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco op_type = CAS.Op_type CAS.Total ar' kind nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco op' = CAS.Qual_op_name (token2id op) op_type nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco (vars, prems) = ops2predPremises im ar 0
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco pred_type = CAS.Pred_type [kind] nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco pred_name = CAS.Qual_pred_name co' pred_type nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco op_term = CAS.Application op' vars nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco op_pred = CAS.Predication pred_name [op_term] nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco conj_form = createConjForm prems
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco imp_form = if null prems
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco else CAS.Implication conj_form op_pred True nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco q_form = quantifyUniversally imp_form
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco final_form = makeNamed "" q_form
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco in final_form : acc
357381f0a999099cd2d4c268006df56b47847d68Adrián Riescoop2pred _ _ acc = acc
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco-- | creates a conjuctive formula distinguishing the size of the list
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescocreateConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescocreateConjForm [] = CAS.True_atom nullRange
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescocreateConjForm [a] = a
357381f0a999099cd2d4c268006df56b47847d68Adrián RiescocreateConjForm fs = CAS.Conjunction fs nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates a implication formula distinguishing the size of the premises
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescocreateImpForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA -> CAS.CASLFORMULA
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescocreateImpForm (CAS.True_atom _) form = form
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescocreateImpForm form1 form2 = CAS.Implication form1 form2 True nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates the predicates asserting the "true" sort of the operator if all
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- the arguments have the correct sort
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riescoops2predPremises :: IdMap -> [MSym.Symbol] -> Int -> ([CAS.CASLTERM], [CAS.CASLFORMULA])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoops2predPremises im (MSym.Sort s : ss) i = (var : terms, form : forms)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where s' = token2id s
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco kind = Map.findWithDefault (errorId "mb of op as predicate") s' im
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco pred_type = CAS.Pred_type [kind] nullRange
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco pred_name = CAS.Qual_pred_name s' pred_type nullRange
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco var = newVarIndex i kind
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco form = CAS.Predication pred_name [var] nullRange
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco (terms, forms) = ops2predPremises im ss (i + 1)
71410be62420b321abb02ef1ac2b7f2141b3bc7fAdrián Riescoops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)
71410be62420b321abb02ef1ac2b7f2141b3bc7fAdrián Riesco where k' = token2id k
71410be62420b321abb02ef1ac2b7f2141b3bc7fAdrián Riesco kind = Map.findWithDefault (errorId "mb of op as predicate") k' im
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco var = newVarIndex i kind
71410be62420b321abb02ef1ac2b7f2141b3bc7fAdrián Riesco (terms, forms) = ops2predPremises im ss (i + 1)
71410be62420b321abb02ef1ac2b7f2141b3bc7fAdrián Riescoops2predPremises _ _ _ = ([], [])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | traverses the Maude sentences, returning a pair of list of sentences.
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco-- The first list in the pair are the equations without the attribute "owise",
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- while the second one are the equations with this attribute
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosplitOwiseEqs :: [Named MSentence.Sentence] ->
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco ([Named MSentence.Sentence], [Named MSentence.Sentence], [Named MSentence.Sentence])
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescosplitOwiseEqs [] = ([], [], [])
fecce42517d20490f893c4a9dee29b000e1653eaAdriá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
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco MSentence.Equation (MAS.Eq _ _ _ ats) -> case any MAS.owise ats of
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco True -> (no_owise_sens, s : owise_sens, mbs_rls)
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco False -> (s : no_owise_sens, owise_sens, mbs_rls)
357381f0a999099cd2d4c268006df56b47847d68Adrián Riesco _ -> (no_owise_sens, owise_sens, s : mbs_rls)
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco-- | translates a Maude equation defined without the "owise" attribute into
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoOwiseSen2Formula :: 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' }
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- | translates a Maude equation defined with the "owise" attribute into
172f4dfb4b858440fab545bac00d3ec4abd0cbe4Adrián Riesco-- a CASL formula
172f4dfb4b858440fab545bac00d3ec4abd0cbe4Adrián RiescoowiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]
172f4dfb4b858440fab545bac00d3ec4abd0cbe4Adrián Riesco -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
172f4dfb4b858440fab545bac00d3ec4abd0cbe4Adrián RiescoowiseSen2Formula im owise_forms s = s'
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco where MSentence.Equation eq = sentence s
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdriá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
7474965b2e6323002c96c0b39a59843cde201870Adrián Riescomb_rl2formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdriá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' }
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco _ -> makeNamed "" $ CAS.False_atom nullRange
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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco 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"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates a Maude equation without the "owise" attribute into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoOwiseEq2Formula im eq@(MAS.Eq t t' [] _) = quantifyUniversally vars_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Strong_equation ct ct' nullRange
c2b9205d94467085f8b07c294c86493d55427074Adrián Riesco vars_form = varsImp (MSentence.Equation eq) im form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoOwiseEq2Formula im eq@(MAS.Eq t t' conds@(_:_) _) = quantifyUniversally vars_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where 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.Strong_equation ct ct' nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = createImpForm conds_form concl_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco vars_form = varsImp (MSentence.Equation eq) im form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | transforms a Maude equation defined with the otherwise attribute into
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- a 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco vars_form = varsImp (MSentence.Equation eq) im eq_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (op, ts, _) = fromJust $ getLeftApp eq_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ex_form = existencialNegationOtherEqs op ts no_owise_form
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco imp_form = createImpForm ex_form vars_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Quantification CAS.Universal vars imp_form nullRange
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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ex_forms = foldr ((++) . existencialNegationOtherEq op ts) [] forms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = if length ex_forms > 1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco then CAS.Conjunction ex_forms nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else head ex_forms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | given a formula, if it refers to the same operator indicated by the parameters
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- the predicate creates a list with the negation of the existence of variables that
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- match the pattern described in the formula. In other case it returns an empty list
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoexistencialNegationOtherEq :: CAS.OP_SYMB -> [CAS.CASLTERM] ->
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoexistencialNegationOtherEq req_op terms form = case ok of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (_, ts, conds) = fromJust tpl
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ts' = qualifyExVarsTerms ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco conds' = qualifyExVarsForms conds
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco prems = (createEqs ts' terms) ++ conds'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco conj_form = CAS.Conjunction prems nullRange
6f6549c13f912de12345850e4eb248ec358c1b43Adrián Riesco ex_form = if vars' /= []
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco then CAS.Quantification CAS.Existential vars' conj_form nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else conj_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco neg_form = CAS.Negation ex_form nullRange
6f6549c13f912de12345850e4eb248ec358c1b43Adrián Riesco in [neg_form]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where (inner_form, vars) = noQuantification $ sentence form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco vars' = qualifyExVars vars
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco tpl = getLeftApp inner_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ok = case tpl of
172f4dfb4b858440fab545bac00d3ec4abd0cbe4Adrián Riesco Nothing -> False
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco Just _ -> let (op, ts, _) = fromJust tpl
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in req_op == op && length terms == length ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | qualifies the variables in a list of formulas with the suffix "_ex" to
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- distinguish them from the variables already bound
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsForms :: [CAS.CASLFORMULA] -> [CAS.CASLFORMULA]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsForms = map qualifyExVarsForm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | qualifies the variables in a formula with the suffix "_ex" to distinguish them
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco-- from the variables already bound
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsForm (CAS.Strong_equation t t' r) = CAS.Strong_equation qt qt' r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where qt = qualifyExVarsTerm t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco qt' = qualifyExVarsTerm t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsForm (CAS.Predication op ts r) = CAS.Predication op ts' r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts' = qualifyExVarsTerms ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsForm f = f
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | qualifies the variables in a list of terms with the suffix "_ex" to
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- distinguish them from the variables already bound
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerms :: [CAS.CASLTERM] -> [CAS.CASLTERM]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerms = map qualifyExVarsTerm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | qualifies the variables in a term with the suffix "_ex" to distinguish them
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- from the variables already bound
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm :: CAS.CASLTERM -> CAS.CASLTERM
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Qual_var var sort r) = 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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescoqualifyExVarsTerm (CAS.Sorted_term t s r) = CAS.Sorted_term (qualifyExVarsTerm t) s r
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescoqualifyExVarsTerm (CAS.Cast t s r) = CAS.Cast (qualifyExVarsTerm t) s r
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescoqualifyExVarsTerm (CAS.Conditional t1 f t2 r) = CAS.Conditional t1' f t2' r
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco where t1' = qualifyExVarsTerm t1
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco t2' = qualifyExVarsTerm t2
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsTerm (CAS.Mixfix_term ts) = CAS.Mixfix_term ts'
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco where ts' = map qualifyExVarsTerm ts
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsTerm (CAS.Mixfix_parenthesized ts r) = CAS.Mixfix_parenthesized ts' r
0f77efdcc159eee5682aabf2b9a3c178c467b466Adriá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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco where ts' = map qualifyExVarsTerm ts
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescoqualifyExVarsTerm t = t
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco-- | qualifies a list of variables with the suffix "_ex" to
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco-- distinguish them from the variables already bound
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVars :: [CAS.VAR_DECL] -> [CAS.VAR_DECL]
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVars = map qualifyExVar
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco-- | qualifies a variable with the suffix "_ex" to distinguish it from
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco-- the variables already bound
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVar (CAS.Var_decl vars s r) = CAS.Var_decl vars' s r
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco where vars' = map qualifyExVarAux vars
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco-- | qualifies a token with the suffix "_ex"
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarAux :: Token -> Token
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarAux var = mkSimpleId $ show var ++ "_ex"
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco-- | creates a list of strong equalities from two lists of terms
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescocreateEqs :: [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateEqs (t1 : ts1) (t2 : ts2) = CAS.Strong_equation t1 t2 nullRange : ls
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ls = createEqs ts1 ts2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateEqs _ _ = []
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | extracts the operator at the top and the arguments of the lefthand side
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- in a strong equation
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescogetLeftApp :: CAS.CASLFORMULA -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM], [CAS.CASLFORMULA])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetLeftApp (CAS.Strong_equation term _ _) = case getLeftAppTerm term of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Nothing -> Nothing
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Just (op, ts) -> Just (op, ts, [])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetLeftApp (CAS.Implication prem concl _ _) = case getLeftApp concl of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Nothing -> Nothing
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Just (op, ts, _) -> Just (op, ts, conds)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where conds = getPremisesImplication prem
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetLeftApp _ = Nothing
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | extracts the operator at the top and the arguments of the lefthand side
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- in 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | extracts the formulas of the given premise, distinguishing whether it is
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- a conjunction or not
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetPremisesImplication :: CAS.CASLFORMULA -> [CAS.CASLFORMULA]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetPremisesImplication (CAS.Conjunction forms _) = forms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetPremisesImplication form = [form]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a Maude membership into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb2formula im mb@(MAS.Mb t s [] _) = quantifyUniversally vars_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco s' = token2id $ getName s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = Map.findWithDefault (errorId "mb to formula") s' im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_type = CAS.Pred_type [kind] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_name = CAS.Qual_pred_name s' pred_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Predication pred_name [ct] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco vars_form = varsImp (MSentence.Membership mb) im form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb2formula im mb@(MAS.Mb t s conds@(_ : _) _) = quantifyUniversally vars_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco s' = token2id $ getName s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = Map.findWithDefault (errorId "mb to formula") s' im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_type = CAS.Pred_type [kind] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_name = CAS.Qual_pred_name s' pred_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco conds_form = conds2formula im conds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco concl_form = CAS.Predication pred_name [ct] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Implication conds_form concl_form True nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco vars_form = varsImp (MSentence.Membership mb) im form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a Maude rule into a CASL formula
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riescorl2formula :: IdMap -> MAS.Rule -> CAS.CASLFORMULA
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riescorl2formula im rl@(MAS.Rl t t' [] _) = quantifyUniversally vars_form
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco where ty = token2id $ getName $ MAS.getTermType t
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco kind = Map.findWithDefault (errorId "rl to formula") ty im
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco pred_name = CAS.Qual_pred_name rewID pred_type nullRange
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco ct = maudeTerm2caslTerm im t
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Predication pred_name [ct, ct'] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco vars_form = varsImp (MSentence.Rule rl) im form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescorl2formula im rl@(MAS.Rl t t' conds@(_:_) _) = quantifyUniversally vars_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ty = token2id $ getName $ MAS.getTermType t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = Map.findWithDefault (errorId "rl to formula") ty im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_name = CAS.Qual_pred_name rewID pred_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct = maudeTerm2caslTerm im t
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco ct' = maudeTerm2caslTerm im t'
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco conds_form = conds2formula im conds
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco concl_form = CAS.Predication pred_name [ct, ct'] nullRange
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco form = CAS.Implication conds_form concl_form True nullRange
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco vars_form = varsImp (MSentence.Rule rl) im form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a conjunction of Maude conditions to a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoconds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riescoconds2formula im conds = CAS.Conjunction forms nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where forms = map (cond2formula im) conds
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco-- | translate a single Maude condition to a CASL formula
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riescocond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescocond2formula im (MAS.EqCond t t') = CAS.Strong_equation ct ct' nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riescocond2formula im (MAS.MatchCond t t') = CAS.Strong_equation ct ct' nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescocond2formula im (MAS.MbCond t s) = CAS.Predication pred_name [ct] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco s' = token2id $ getName s
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco kind = Map.findWithDefault (errorId "mb cond to formula") s' im
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco pred_type = CAS.Pred_type [kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name s' pred_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riescocond2formula im (MAS.RwCond t t') = CAS.Predication pred_name [ct, ct'] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ty = token2id $ getName $ MAS.getTermType t
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco kind = Map.findWithDefault (errorId "rw cond to formula") ty im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco pred_name = CAS.Qual_pred_name rewID pred_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco-- | translates a Maude term into a CASL term
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescomaudeTerm2caslTerm :: IdMap -> MAS.Term -> CAS.CASLTERM
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeTerm2caslTerm im (MAS.Var q ty) = CAS.Qual_var q kind nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where kind = Map.findWithDefault (errorId "maude_term2CASL_term") (token2id $ getName ty) im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeTerm2caslTerm im (MAS.Const q ty) = CAS.Application op [] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where name = token2id q
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ty' = token2id $ getName ty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = Map.findWithDefault (errorId "maude_term2CASL_term") ty' im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco op_type = CAS.Op_type CAS.Total [] kind nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco op = CAS.Qual_op_name name op_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ty' = token2id $ getName ty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = Map.findWithDefault (errorId "maude_term2CASL_term") ty' im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco types_tts = getTypes tts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco op_type = CAS.Op_type CAS.Total types_tts kind nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco op = CAS.Qual_op_name name op_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | obtains the types of the given terms
6f6549c13f912de12345850e4eb248ec358c1b43Adrián RiescogetTypes :: [CAS.CASLTERM] -> [Id]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetTypes = mapMaybe getType
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | extracts the type of the temr
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetType :: CAS.CASLTERM -> Maybe Id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetType (CAS.Qual_var _ kind _) = Just kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetType (CAS.Application op _ _) = case op of
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco CAS.Qual_op_name _ (CAS.Op_type _ _ kind _) _ -> Just kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetType _ = Nothing
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generates the formulas for the rewrite predicates
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescorewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescorewPredicatesSens = Set.fold rewPredicateSens []
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco-- | generates the formulas for the rewrite predicate of the given sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescorewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescorewPredicateSens kind acc = ref : trans : acc
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco where ref = reflSen kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco trans = transSen kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates the reflexivity predicate for the given kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoreflSen :: Id -> Named CAS.CASLFORMULA
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescoreflSen kind = makeNamed name $ quantifyUniversally form
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco where v = newVar kind
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pn = CAS.Qual_pred_name rewID pred_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco form = CAS.Predication pn [v, v] nullRange
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco name = "rew_refl_" ++ show kind
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco-- | creates the transitivity predicate for the given kind
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescotransSen :: Id -> Named CAS.CASLFORMULA
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián RiescotransSen kind = makeNamed name $ quantifyUniversally form
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco where v1 = newVarIndex 1 kind
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco v2 = newVarIndex 2 kind
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco v3 = newVarIndex 3 kind
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco pn = CAS.Qual_pred_name rewID pred_type nullRange
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco prem1 = CAS.Predication pn [v1, v2] nullRange
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco prem2 = CAS.Predication pn [v2, v3] nullRange
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco concl = CAS.Predication pn [v1, v3] nullRange
6e121321775373fe11161d23c541437456df19b4Adrián Riesco conj_form = CAS.Conjunction [prem1, prem2] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco form = CAS.Implication conj_form concl True nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco name = "rew_trans_" ++ show kind
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- | generate the predicates for the rewrites
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescorewPredicates :: Map.Map Id (Set.Set CSign.PredType) -> Set.Set Id
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescorewPredicates m = Set.fold rewPredicate m
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco-- | generate the predicates for the rewrites of the given sort
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescorewPredicate :: Id -> Map.Map Id (Set.Set CSign.PredType)
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián RiescorewPredicate kind m = Map.insertWith (Set.union) rewID ar m
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where ar = Set.singleton $ CSign.PredType [kind, kind]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | create the predicates that assign sorts to each term
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescokindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescokindPredicates = Map.foldWithKey kindPredicate Map.empty
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | create the predicates that assign the current sort to the
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- corresponding terms
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescokindPredicate :: Id -> Id -> Map.Map Id (Set.Set CSign.PredType)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescokindPredicate sort kind mis = case sort == (str2id "Universal") of
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco False -> let ar = Set.singleton $ CSign.PredType [kind]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | extract the kinds from the map of id's
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescokindsFromMap :: IdMap -> Set.Set Id
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | return a map where each sort is mapped to its kind, both of them
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- already converted to Id
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoarrangeKinds :: MSign.SortSet -> MSign.SubsortRel -> IdMap
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoarrangeKinds ss r = arrangeKindsList (Set.toList ss) r Map.empty
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco-- | traverse the sorts and creates a table that assigns to each sort its kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescoarrangeKindsList :: [MSym.Symbol] -> MSign.SubsortRel -> IdMap -> IdMap
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoarrangeKindsList [] _ m = m
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoarrangeKindsList l@(s : _) r m = arrangeKindsList not_rel r m'
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where tops = List.sort $ getTop r s
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco (rel, not_rel) = sameKindList s tc l
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco f = \ x y z -> Map.insert (sym2id y) (sort2id x) z
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco m' = foldr (f tops) m rel
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco-- | creates two list distinguishing in the first componente the symbols
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco-- with the same kind than the given one and in the second one the
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- symbols with different kind
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescosameKindList :: MSym.Symbol -> MSign.SubsortRel -> [MSym.Symbol]
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescosameKindList _ _ [] = ([], [])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosameKindList t r (t' : ts) = if MSym.sameKind r t t'
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco then (t' : hold, not_hold)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco else (hold, t' : not_hold)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where (hold, not_hold) = sameKindList t r ts
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder-- | transform the set of Maude sorts in a set of CASL sorts, including
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- only one sort for each kind.
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescosortsTranslation :: MSign.SortSet -> MSign.SubsortRel -> Set.Set Id
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescosortsTranslation ss r = sortsTranslationList (Set.toList ss) r
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | transform a list representing the Maude sorts in a set of CASL sorts,
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco-- including only one sort for each kind.
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescosortsTranslationList :: [MSym.Symbol] -> MSign.SubsortRel -> Set.Set Id
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescosortsTranslationList [] _ = Set.empty
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescosortsTranslationList (s : ss) r = Set.insert (sort2id tops) res
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where tops@(top : _) = List.sort $ getTop r s
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco ss' = deleteRelated ss top r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco res = sortsTranslation ss' r
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | return the maximal elements from the sort relation
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescogetTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescogetTop r tok = case succs of
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco toks@(_:_) -> foldr ((++) . (getTop r)) [] toks
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | delete from the list of sorts those in the same kind that the parameter
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescodeleteRelated :: [MSym.Symbol] -> MSym.Symbol -> MSign.SubsortRel -> MSign.SortSet
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescodeleteRelated ss sym r = foldr (f sym tc) Set.empty ss
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco f = \ sort trC x y -> if MSym.sameKind trC sort x
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco-- | build an Id from a token with the function mkId
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescotoken2id :: Token -> Id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescotoken2id t = mkId ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts = maudeSymbol2validCASLSymbol t
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | build an Id from a Maude symbol
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescosym2id :: MSym.Symbol -> Id
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescosym2id = token2id . getName
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates an Id from a string
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescostr2id :: String -> Id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescostr2id = token2id . mkSimpleId
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | build an Id from a list of sorts, taking the first from the ordered list
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescosort2id :: [MSym.Symbol] -> Id
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescosort2id syms = mkId sym''
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where sym = head $ List.sort syms
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adriá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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoquantifyUniversally form = if null var_decl
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco else CAS.Quantification CAS.Universal var_decl form nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco where vars = getVars form
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco var_decl = listVarDecl vars
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco-- | traverses a map with sorts as keys and sets of variables as value and creates
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- a list of variable declarations
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescolistVarDecl :: Map.Map Id (Set.Set Token) -> [CAS.VAR_DECL]
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián RiescolistVarDecl = Map.foldWithKey f []
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco where f = \ sort var_set acc -> CAS.Var_decl (Set.toList var_set) sort nullRange : acc
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImp :: MSentence.Sentence -> IdMap -> CAS.CASLFORMULA -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImp sen im form = createImpForm imp_form form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where imp_form = varsImplication sen im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates the implication obtained from the implicit information given
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- in Maude variables
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImplication :: MSentence.Sentence -> IdMap -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImplication (MSentence.Membership mb) im = createConjForm forms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where MAS.Mb t _ conds _ = mb
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco formsTerm = varsImpTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco formsCond = varsImpConds im conds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco forms = Set.toList $ Set.union formsTerm formsCond
a74f814d3b445eadad6f68737a98a7a303698affChristian MaedervarsImplication (MSentence.Equation eq) im = createConjForm forms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where MAS.Eq t _ conds _ = eq
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco formsTerm = varsImpTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco formsCond = varsImpConds im conds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco forms = Set.toList $ Set.union formsTerm formsCond
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImplication (MSentence.Rule rl) im = createConjForm forms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where MAS.Rl t _ conds _ = rl
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco formsTerm = varsImpTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco formsCond = varsImpConds im conds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco forms = Set.toList $ Set.union formsTerm formsCond
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | computes the predicates with the information associated to the variables in
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- matching conditions
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImpConds :: IdMap -> [MAS.Condition] -> Set.Set CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImpConds im = foldr (Set.union . (varsImpCond im)) Set.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | auxiliary function that computes the predicates with the information associated
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- to the variables in matching conditions
a74f814d3b445eadad6f68737a98a7a303698affChristian MaedervarsImpCond :: IdMap -> MAS.Condition -> Set.Set CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImpCond im (MAS.MatchCond t _) = varsImpTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImpCond im (MAS.RwCond _ t) = varsImpTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImpCond _ _ = Set.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | computes the predicates with the information associated to the variables in
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImpTerms :: IdMap -> [MAS.Term] -> Set.Set CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImpTerms im = foldr (Set.union . (varsImpTerm im)) Set.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | computes the predicates with the information associated to the variables in
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImpTerm :: IdMap -> MAS.Term -> Set.Set CAS.CASLFORMULA
a74f814d3b445eadad6f68737a98a7a303698affChristian MaedervarsImpTerm im (MAS.Var q (MAS.TypeSort s)) =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Set.singleton $ CAS.Predication ps [term] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where sort = token2id $ getName s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = im Map.! sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pt = CAS.Pred_type [kind] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ps = CAS.Qual_pred_name sort pt nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco term = CAS.Qual_var q kind nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- The variable is declared on the kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImpTerm im (MAS.Apply _ terms _) = varsImpTerms im terms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescovarsImpTerm _ _ = Set.empty
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
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescopreds2syms :: Map.Map Id (Set.Set CSign.PredType) -> Set.Set CSign.Symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescopreds2syms = Map.foldWithKey pred2sym Set.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates a CASL predicate into a CASL symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescopred2sym :: Id -> Set.Set CSign.PredType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescopred2sym pn spt acc = Set.fold (createSym4id pn) acc spt
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates a CASL symbol for a predicate
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateSym4id :: Id -> CSign.PredType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateSym4id pn pt acc = Set.insert sym acc
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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates a CASL operator into a CASL symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoop2sym :: Id -> Set.Set CSign.OpType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoop2sym on sot acc = Set.union set acc
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where set = Set.fold (createSymOp4id on) Set.empty sot
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates a CASL symbol for an operator
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateSymOp4id :: Id -> CSign.OpType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateSymOp4id on ot acc = Set.insert sym acc
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco where sym = CSign.Symbol on $ CSign.OpAsItemType ot
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco-- | extract the variables from a CASL formula and put them in a map
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- with keys the sort of the variables and value the set of variables
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- in this sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars :: CAS.CASLFORMULA -> Map.Map Id (Set.Set Token)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescogetVars (CAS.Quantification _ _ f _) = getVars f
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescogetVars (CAS.Conjunction fs _) = foldr (Map.unionWith (Set.union) . getVars) Map.empty fs
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetVars (CAS.Disjunction fs _) = foldr (Map.unionWith (Set.union) . getVars) Map.empty fs
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetVars (CAS.Implication f1 f2 _ _) = Map.unionWith (Set.union) v1 v2
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco where v1 = getVars f1
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco v2 = getVars f2
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetVars (CAS.Equivalence f1 f2 _) = Map.unionWith (Set.union) v1 v2
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco where v1 = getVars f1
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco v2 = getVars f2
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetVars (CAS.Negation f _) = getVars f
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetVars (CAS.Predication _ ts _) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetVars (CAS.Definedness t _) = getVarsTerm t
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetVars (CAS.Existl_equation t1 t2 _) = Map.unionWith (Set.union) v1 v2
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco where v1 = getVarsTerm t1
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco v2 = getVarsTerm t2
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetVars (CAS.Strong_equation t1 t2 _) = Map.unionWith (Set.union) v1 v2
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco where v1 = getVarsTerm t1
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco v2 = getVarsTerm t2
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetVars (CAS.Membership t _ _) = getVarsTerm t
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetVars (CAS.Mixfix_formula t) = getVarsTerm t
6e121321775373fe11161d23c541437456df19b4Adrián Riesco-- | extract the variables of a CASL term
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescogetVarsTerm :: CAS.CASLTERM -> Map.Map Id (Set.Set Token)
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescogetVarsTerm (CAS.Qual_var var sort _) = Map.insert sort (Set.singleton var) Map.empty
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescogetVarsTerm (CAS.Application _ ts _) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescogetVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescogetVarsTerm (CAS.Cast t _ _) = getVarsTerm t
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescogetVarsTerm (CAS.Conditional t1 f t2 _) = Map.unionWith (Set.union) v3 m
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco where v1 = getVarsTerm t1
ebdb7b09e2ad2bb780d84c127d72c30dfcfb87b2Adrián Riesco v2 = getVarsTerm t2
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco v3 = getVars f
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescogetVarsTerm (CAS.Mixfix_term ts) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescogetVarsTerm (CAS.Mixfix_parenthesized ts _) =
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescogetVarsTerm (CAS.Mixfix_bracketed ts _) =
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescogetVarsTerm (CAS.Mixfix_braced ts _) =
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescogetVarsTerm _ = Map.empty
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco-- | generates the constructor constraint
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescoctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA
223be434693e8c97e2522ac19155a284b3536035Adrián RiescoctorSen isFree (sorts, _, ops) = do
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco let sortList = Set.toList sorts
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco (CSign.toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco allSyms = opSyms
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco resType _ (CAS.Op_name _) = False
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco resType s (CAS.Qual_op_name _ t _) = CAS.res_OP_TYPE t == s
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco getIndex s = maybe (-1) id $ List.findIndex (== s) sortList
b3a8ae62887130fd41b91bf2ea1fd66360bd3c29Adrián Riesco addIndices (CAS.Op_name _) =
b3a8ae62887130fd41b91bf2ea1fd66360bd3c29Adrián Riesco error "CASL/StaticAna: Internal error in function addIndices"
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco addIndices os@(CAS.Qual_op_name _ t _) =
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco (os,map getIndex $ CAS.args_OP_TYPE t)
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco collectOps s =
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco constrs = map collectOps sortList
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco f = CAS.Sort_gen_ax constrs isFree
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco makeNamed ("ga_generated_" ++ showSepList (showString "_") showId sortList "") f
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adriá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
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco-- | transforms a string coding a Maude identifier into another string
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riesco-- representing a CASL identifier
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riescoms2vcs :: String -> String
7474965b2e6323002c96c0b39a59843cde201870Adrián Riescoms2vcs s = case Map.member s stringMap of
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco True -> Map.findWithDefault "" s stringMap
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco False -> let f = \ x y -> if Map.member x charMap
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco then (charMap Map.! x) ++ ['\''] ++ y
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco else if x == '_'
8b389272b3312c6d3e3c0aee2e94bca6dbdade50Adrián Riesco then "__" ++ y
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco in foldr f [] s
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco-- | map of reserved words
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián RiescostringMap :: Map.Map String String
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco [("true", "maudeTrue"),
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco ("false", "maudeFalse"),
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco ("not_", "neg__"),
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco ("s_", "suc"),
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco ("_+_", "__+__"),
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco ("_*_", "__*__"),
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco ("_<_", "__<__"),
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco ("_<=_", "__<=__"),
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco ("_>_", "__>__"),
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco ("_>=_", "__>=__"),
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco ("_and_", "__maudeAnd__")]
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco-- | splits the string into a list of tokens, separating the double
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco-- underscores from the rest of characters
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescosplitDoubleUnderscores :: String -> String -> [Token]
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescosplitDoubleUnderscores [] acc = if null acc
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco else [mkSimpleId acc]
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescosplitDoubleUnderscores ('_' : '_' : cs) acc = if null acc
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco then dut : rest
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco else acct : dut : rest
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco where acct = mkSimpleId acc
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco dut = mkSimpleId "__"
c6a4f949f2a9da476c80399fb061020937255f87Adrián Riesco rest = splitDoubleUnderscores cs []
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescosplitDoubleUnderscores (c : cs) acc = splitDoubleUnderscores cs (acc ++ [c])
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoerrorId :: String -> Id
c6a4f949f2a9da476c80399fb061020937255f87Adrián RiescoerrorId s = token2id $ mkSimpleId $ "ERROR: " ++ s