PreComorphism.hs revision 5318901bb69bf247e0f341312c800ba4ea87e46b
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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates a CASL morphism from a Maude morphism
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapMorphism :: MMorphism.Morphism -> Result (CMorphism.CASLMor)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapMorphism morph =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco mk = arrangeKinds (MSign.sorts src) (MSign.subsorts src)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco cs = kindsFromMap mk
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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 []
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in Result [] $ Just $ 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeOpMap2CASLOpMap 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco g = \ x -> fromJust $ Map.lookup (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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sym_id = token2id q
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = fromJust $ Map.lookup 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeSort2caslId im sym = fromJust $ Map.lookup (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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreatePredMap 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = fromJust $ Map.lookup 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoapplySortMap2CASLSorts :: MMorphism.SortMap -> Set.Set Id -> CMorphism.Sort_map
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoapplySortMap2CASLSorts sm = Set.fold (applySortMap2CASLSort sm) Map.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | computes the morphism for a single kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoapplySortMap2CASLSort :: MMorphism.SortMap -> Id -> CMorphism.Sort_map -> CMorphism.Sort_map
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoapplySortMap2CASLSort sm sort csm = new_csm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where toks = getTokens sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco new_toks = map (rename sm) toks
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco new_sort = mkId new_toks
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco new_csm = if new_sort == sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else Map.insert sort new_sort csm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | renames the sorts in a given kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescorename :: MMorphism.SortMap -> Token -> Token
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescorename sm tok = new_tok
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where sym = MSym.Sort tok
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sym' = if Map.member sym sm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco then fromJust $ Map.lookup sym sm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco new_tok = getName sym'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates a Maude sentence into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSentence sg sen@(MSentence.Equation eq) = case owise ats of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco False -> Result [] $ Just $ sentence $ noOwiseSen2Formula mk named
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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 Result [] $ Just trans
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco MAS.Eq _ _ _ ats = eq
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco named = makeNamed "" sen
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSentence sg sen@(MSentence.Membership mb) = Result [] $ Just $ sentence form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco named = makeNamed "" sen
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = mb_rl2formula mk named
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapSentence sg sen@(MSentence.Rule rl) = Result [] $ Just $ sentence form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco named = makeNamed "" sen
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomapTheory :: (MSign.Sign, [Named MSentence.Sentence])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapTheory (sg, nsens) = Result [] $ Just $ maude2casl sg nsens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | computes new signature and sentences of CASL associated to the
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- given Maude signature and sentences
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomaude2casl :: MSign.Sign -> [Named MSentence.Sentence]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomaude2casl msign nsens = (csign { CSign.sortSet = cs,
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco CSign.declaredSymbols = syms }, new_sens)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where csign = CSign.emptySign ()
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco mk = arrangeKinds (MSign.sorts msign) (MSign.subsorts msign)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco cs = kindsFromMap mk
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco ks = kindPredicates mk
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco rp = rewPredicates ks cs
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ksyms = kinds2syms cs
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (cops, assoc_ops, ops_forms) = translateOps mk ops
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ops_syms = ops2symbols cops
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_sens = subsortSens mk (Rel.toList $ MSign.subsorts msign)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco named_sens = map (makeNamed "") pred_sens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences msign
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs (nsens ++ sg_sens)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco preds_syms = preds2syms preds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco syms = Set.union ksyms $ Set.union ops_syms preds_syms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco new_sens = ops_forms ++ named_sens ++ no_owise_forms ++ owise_forms ++ mb_rl_forms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates the Maude operator map into a tuple of CASL operators, CASL
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- associative operators and the formulas generated by the operator attributes
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- and the membership induced from each Maude operator
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOps :: IdMap -> MSign.OpMap -> (CSign.OpMap, CSign.OpMap, [Named CAS.CASLFORMULA])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOps im = Map.fold (translateOpDeclSet im) (Map.empty, Map.empty, [])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates an operator declaration set into a tern as described above
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOpDeclSet :: IdMap -> MSign.OpDeclSet
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> (CSign.OpMap, CSign.OpMap, [Named CAS.CASLFORMULA])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> (CSign.OpMap, CSign.OpMap, [Named CAS.CASLFORMULA])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOpDecl :: IdMap -> MSign.OpDecl
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> (CSign.OpMap, CSign.OpMap, [Named CAS.CASLFORMULA])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> (CSign.OpMap, CSign.OpMap, [Named CAS.CASLFORMULA])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOpDecl im (syms, ats) (ops, assoc_ops, forms) = (ops', assoc_ops', forms6)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where predOps = ops2pred im syms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (sym : _) = Set.toList syms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (cop_id, ot) = fromJust $ maudeSym2CASLOp im sym
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco forms' = forms ++ predOps
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ops' = Map.insertWith (Set.union) cop_id cop_type ops
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco assoc_ops' = if assoc ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco then Map.insertWith (Set.union) cop_id cop_type assoc_ops
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else assoc_ops
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco op_name = CAS.Op_name cop_id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco forms1 = if assoc ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else let assoc_f = associativeSen op_name (head $ CSign.opArgs ot)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in makeNamed "" assoc_f : forms'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco forms2 = if comm ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else let comm_f = commutativeSen op_name (head $ CSign.opArgs ot)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in makeNamed "" comm_f : forms1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco forms3 = if idem ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else let idem_f = idempotentSen op_name (head $ CSign.opArgs ot)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in makeNamed "" idem_f : forms2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco forms4 = if identity ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else let iden = maudeTerm2caslTerm im $ fromJust $ getIdentity ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco identity_f = identitySens op_name (head $ CSign.opArgs ot) iden
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in map (makeNamed "") identity_f ++ forms3
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco forms5 = if leftId ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else let lid = maudeTerm2caslTerm im $ fromJust $ getIdentity ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco lid_f = left_identitySen op_name (head $ CSign.opArgs ot) lid
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in makeNamed "" lid_f : forms4
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco forms6 = if rightId ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else let rid = maudeTerm2caslTerm im $ fromJust $ getIdentity ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco rid_f = right_identitySen op_name (head $ CSign.opArgs ot) rid
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in makeNamed "" rid_f : forms5
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates a Maude operator symbol into a pair with the id of the operator
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- and its CASL type
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeSym2CASLOp :: IdMap -> MSym.Symbol -> Maybe (Id, CSign.OpType)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where f = token2id . getName
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco g = \ x -> fromJust $ Map.lookup (f x) im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeSym2CASLOp _ _ = Nothing
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates the predicates associated to each operator declaration in Maude
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- due to the associated membership if the coarity is a sort and not a kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoops2pred :: IdMap -> MSym.SymbolSet -> [Named CAS.CASLFORMULA]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoops2pred im = Set.fold (op2pred im) []
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | generates the memebership predicate associated to an operator
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoop2pred :: IdMap -> MSym.Symbol -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoop2pred im (MSym.Operator op ar co) acc = case co of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco op' = CAS.Op_name $ token2id op
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco co' = token2id s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (vars, prems) = ops2predPremises im ar 0
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_name = CAS.Pred_name co'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco op_term = CAS.Application op' vars nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco op_pred = CAS.Predication pred_name [op_term] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco conj_form = createConjForm prems
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco imp_form = if null prems
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else CAS.Implication conj_form op_pred True nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco q_form = quantifyUniversally imp_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco final_form = makeNamed "" q_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in final_form : acc
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoop2pred _ _ acc = acc
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateConjForm [] = CAS.True_atom nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateConjForm [a] = a
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateConjForm fs = CAS.Conjunction fs nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = fromJust $ Map.lookup s' im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco var = newVarIndex i kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Predication pred_name [var] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (terms, forms) = ops2predPremises im ss (i + 1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where k' = token2id k
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = fromJust $ Map.lookup k' im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco var = newVarIndex i kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (terms, forms) = ops2predPremises im ss (i + 1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoops2predPremises _ _ _ = ([], [])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | traverses the Maude sentences, returning a pair of list of sentences.
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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] ->
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ([Named MSentence.Sentence], [Named MSentence.Sentence], [Named MSentence.Sentence])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosplitOwiseEqs [] = ([], [], [])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosplitOwiseEqs (s : ss) = res
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sen = sentence s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco res = case sen of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco MSentence.Equation (MAS.Eq _ _ _ ats) -> case owise ats of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco True -> (no_owise_sens, s : owise_sens, mbs_rls)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco False -> (s : no_owise_sens, owise_sens, mbs_rls)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> (no_owise_sens, owise_sens, s : mbs_rls)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | check if a list of attribute statements contains the owise attribute
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoowise :: [MAS.StmntAttr] -> Bool
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoowise [] = False
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoowise (a : as) = case a of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> owise as
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | check if a list of attributes contains the assoc attribute
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoassoc :: [MAS.Attr] -> Bool
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoassoc [] = False
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoassoc (a : as) = case a of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> assoc as
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | check if a list of attributes contains the comm attribute
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescocomm :: [MAS.Attr] -> Bool
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescocomm [] = False
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescocomm (a : as) = case a of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | check if a list of attributes contains the idem attribute
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoidem :: [MAS.Attr] -> Bool
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoidem [] = False
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoidem (a : as) = case a of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | check if a list of attributes contains the identity attribute
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoidentity :: [MAS.Attr] -> Bool
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoidentity [] = False
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoidentity (a : as) = case a of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> identity as
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | check if a list of attributes contains the left identity attribute
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoleftId :: [MAS.Attr] -> Bool
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoleftId [] = False
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoleftId (a : as) = case a of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> leftId as
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | check if a list of attributes contains the right identity attribute
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescorightId :: [MAS.Attr] -> Bool
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescorightId [] = False
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescorightId (a : as) = case a of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> rightId as
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | returns the identity term from the attribute set
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetIdentity [] = Nothing
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetIdentity (a : as) = case a of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> getIdentity as
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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' }
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates a Maude equation defined with the "owise" attribute into
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoowiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoowiseSen2Formula im owise_forms s = s'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where MSentence.Equation eq = sentence s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sen' = owiseEq2Formula im owise_forms eq
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco s' = s { sentence = sen' }
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates a Maude membership or rule into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb_rl2formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb_rl2formula im s = case sen of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco mb' = mb2formula im mb
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in s { sentence = mb' }
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco rl' = rl2formula im rl
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in s { sentence = rl' }
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> makeNamed "" $ CAS.False_atom nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where sen = sentence s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | create the CASL predicates derived from Maude subsort declarations
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosubsortSens :: IdMap -> [(MSym.Symbol, MSym.Symbol)] -> [CAS.CASLFORMULA]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosubsortSens im = map (subsortSen im)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | create a CASL predicate from a Maude subsort declaration
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosubsortSen :: IdMap -> (MSym.Symbol, MSym.Symbol) -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosubsortSen im (sub, super) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where sub' = getName sub
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco super' = getName super
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco kind = fromJust $ Map.lookup (token2id sub') im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sub_pred_name = CAS.Pred_name $ token2id sub'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco super_pred_name = CAS.Pred_name $ token2id super'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco var = newVar kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sub_form = CAS.Predication sub_pred_name [var] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco super_form = CAS.Predication super_pred_name [var] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Implication sub_form super_form True nullRange
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-- | translate a Maude equation without the "owise" attribute into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiesconoOwiseEq2Formula im (MAS.Eq t t' conds@(_ : _) _) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco conds_form = conds2formula im conds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco concl_form = CAS.Strong_equation ct ct' nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Implication conds_form concl_form True nullRange
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 (op, ts) = fromJust $ getLeftApp eq_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ex_form = existencialNegationOtherEqs op ts no_owise_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco imp_form = CAS.Implication ex_form eq_form True nullRange
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 conj_form = CAS.Conjunction (createEqs ts' terms) nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in [neg_form]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where (inner_form, vars) = noQuantification $ sentence form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco vars' = qualifyExVars vars
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (op, ts) = fromJust $ getLeftApp inner_form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ts' = qualifyExVarsTerms ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ok = req_op == op && length terms == length ts
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 variable 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Sorted_term t s r) = CAS.Sorted_term (qualifyExVarsTerm t) s r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Cast t s r) = CAS.Cast (qualifyExVarsTerm t) s r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Conditional t1 f t2 r) = CAS.Conditional t1' f t2' r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where t1' = qualifyExVarsTerm t1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t2' = qualifyExVarsTerm t2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Mixfix_term ts) = CAS.Mixfix_term ts'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts' = map qualifyExVarsTerm ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Mixfix_parenthesized ts r) = CAS.Mixfix_parenthesized ts' r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts' = map qualifyExVarsTerm ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Mixfix_bracketed ts r) = CAS.Mixfix_bracketed ts' r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts' = map qualifyExVarsTerm ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm (CAS.Mixfix_braced ts r) = CAS.Mixfix_braced ts' r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ts' = map qualifyExVarsTerm ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarsTerm t = t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | qualifies a list of variables with the suffix "_ex" to
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- distinguish them from the variables already bound
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVars :: [CAS.VAR_DECL] -> [CAS.VAR_DECL]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVars = map qualifyExVar
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | qualifies a variable with the suffix "_ex" to distinguish it from
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- the variables already bound
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVar (CAS.Var_decl vars s r) = CAS.Var_decl vars' s r
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where vars' = map qualifyExVarAux vars
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | qualifies a token with the suffix "_ex"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarAux :: Token -> Token
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoqualifyExVarAux var = mkSimpleId $ show var ++ "_ex"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates a list of strong equalities from two lists of terms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocreateEqs :: [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]
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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetLeftApp :: CAS.CASLFORMULA -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM])
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetLeftApp (CAS.Strong_equation term _ _) = getLeftAppTerm term
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-- | translate a Maude membership into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb2formula im (MAS.Mb t s [] _) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_name = CAS.Pred_name $ token2id $ getName s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Predication pred_name [ct] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb2formula im (MAS.Mb t s conds@(_ : _) _) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_name = CAS.Pred_name $ token2id $ getName s
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-- | translate a Maude rule into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescorl2formula :: IdMap -> MAS.Rule -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescorl2formula im (MAS.Rl t t' [] _) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_name = CAS.Pred_name rewID
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Predication pred_name [ct, ct'] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescorl2formula im (MAS.Rl t t' conds@(_:_) _) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_name = CAS.Pred_name rewID
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco conds_form = conds2formula im conds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco concl_form = CAS.Predication pred_name [ct, ct'] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Implication conds_form concl_form True nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a conjunction of Maude conditions to a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoconds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoconds2formula im conds = CAS.Conjunction forms nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where forms = map (cond2formula im) conds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a single Maude condition to a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescocond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescocond2formula im (MAS.EqCond 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.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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_name = CAS.Pred_name $ token2id $ getName s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescocond2formula im (MAS.RwCond t t') = CAS.Predication pred_name [ct, ct'] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pred_name = CAS.Pred_name rewID
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a Maude term into a CASL term
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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 = fromJust $ Map.lookup (token2id $ getName ty) im
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeTerm2caslTerm _ (MAS.Const q _) = CAS.Application (CAS.Op_name name) [] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where name = token2id q
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomaudeTerm2caslTerm im (MAS.Apply q ts _) = CAS.Application (CAS.Op_name name) tts nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where name = token2id q
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco tts = map (maudeTerm2caslTerm im) ts
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | generate the predicates
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescorewPredicates :: Map.Map Id (Set.Set CSign.PredType) -> Set.Set Id
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescorewPredicates m = Set.fold rewPredicate m
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescorewPredicate :: Id -> Map.Map Id (Set.Set CSign.PredType)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescorewPredicate kind m = Map.insertWith (Set.union) rewID ar m
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where ar = Set.singleton $ CSign.PredType [kind, kind]
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | create the predicates that assign sorts to each term
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescokindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescokindPredicates = Map.foldWithKey kindPredicate Map.empty
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | create the predicates that assign the current sort to the
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- corresponding terms
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescokindPredicate :: Id -> Id -> Map.Map Id (Set.Set CSign.PredType)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescokindPredicate sort kind mis = Map.insertWith (Set.union) sort ar mis
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where ar = Set.singleton $ CSign.PredType [kind]
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | extract the kinds from the map of id's
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescokindsFromMap :: IdMap -> Set.Set Id
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | return a map where each sort is mapped to its kind, both of them
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- already converted to Id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoarrangeKinds :: MSign.SortSet -> MSign.SubsortRel -> IdMap
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoarrangeKinds ss r = arrangeKindsList (Set.toList ss) r Map.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | traverse the sorts and creates a table that assigns to each sort its kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoarrangeKindsList :: [MSym.Symbol] -> MSign.SubsortRel -> IdMap -> IdMap
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoarrangeKindsList [] _ m = m
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoarrangeKindsList l@(s : _) r m = arrangeKindsList not_rel r m'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where tops = List.sort $ getTop r s
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco (rel, not_rel) = sameKindList s tc l
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco f = \ x y z -> Map.insert (sym2id y) (sort2id x) z
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco m' = foldr (f tops) m rel
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | creates two list distinguishing in the first componente the symbols
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- with the same kind than the given one and in the second one the
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- symbols with different kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | 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,
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- including only one sort for each kind.
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosortsTranslationList :: [MSym.Symbol] -> MSign.SubsortRel -> Set.Set Id
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescosortsTranslationList [] _ = Set.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescosortsTranslationList (s : ss) r = Set.insert (sort2id tops) res
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where tops@(top : _) = List.sort $ getTop r s
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco ss' = deleteRelated ss top r
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco res = sortsTranslation ss' r
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | return a maximal element from the sort relation
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetTop r tok = case succs of
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | build an Id from a token with the function mkId
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescotoken2id :: Token -> Id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescotoken2id t = mkId [t]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | build an Id from a Maude symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescosym2id :: MSym.Symbol -> Id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescosym2id = token2id . getName
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | build an Id from a list of sorts, including the "[" and "," if needed
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescosort2id :: [MSym.Symbol] -> Id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescosort2id syms = mkId tokens'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where tokens = map getName syms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco tokens' = mkSimpleId "[" : (putCommas tokens) ++ [mkSimpleId "]"]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | inserts commas between tokens
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoputCommas :: [Token] -> [Token]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoputCommas [] = []
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoputCommas [t] = [t]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoputCommas (t : ts) = t : (mkSimpleId ",") : putCommas ts
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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else CAS.Quantification CAS.Universal var_decl form nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where vars = getVars form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco var_decl = listVarDecl vars
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescolistVarDecl :: Map.Map Id (Set.Set Token) -> [CAS.VAR_DECL]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescolistVarDecl = Map.foldWithKey f []
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where f = \ sort var_set acc -> CAS.Var_decl (Set.toList var_set) sort nullRange : acc
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-- | create the sentence to state that an operator is associative
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoassociativeSen :: CAS.OP_SYMB -> Id -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoassociativeSen op sort = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = newVarIndex 1 sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = newVarIndex 2 sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v3 = newVarIndex 3 sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t1 = CAS.Application op [v2, v3] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t = CAS.Application op [v1, t1] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t2 = CAS.Application op [v1, v2] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t' = CAS.Application op [t2, v3] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Strong_equation t t' nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | create the sentence to state that an operator is commutative
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocommutativeSen :: CAS.OP_SYMB -> Id -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescocommutativeSen op sort = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = newVarIndex 1 sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = newVarIndex 2 sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t = CAS.Application op [v1, v2] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t' = CAS.Application op [v2, v1] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Strong_equation t t' nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | create the sentences to state that an operator has identity
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoidentitySens :: CAS.OP_SYMB -> Id -> CAS.CASLTERM -> [CAS.CASLFORMULA]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoidentitySens op sort t = [form1, form2]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v = newVar sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t1 = CAS.Application op [v, t] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t2 = CAS.Application op [t, v] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form1 = quantifyUniversally $ CAS.Strong_equation t1 v nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form2 = quantifyUniversally $ CAS.Strong_equation t2 v nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | create the sentences to state that an operator has left-identity
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoleft_identitySen :: CAS.OP_SYMB -> Id -> CAS.CASLTERM -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoleft_identitySen op sort t = form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v = newVar sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t' = CAS.Application op [t, v] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = quantifyUniversally $ CAS.Strong_equation t' v nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | create the sentences to state that an operator has right-identity
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoright_identitySen :: CAS.OP_SYMB -> Id -> CAS.CASLTERM -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoright_identitySen op sort t = form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v = newVar sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t' = CAS.Application op [v, t] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = quantifyUniversally $ CAS.Strong_equation t' v nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | create the sentences to state that an operator is idempotent
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoidempotentSen :: CAS.OP_SYMB -> Id -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoidempotentSen op sort = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = newVarIndex 1 sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = newVarIndex 2 sort
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco t = CAS.Application op [v1, v2] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Strong_equation t v1 nullRange
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.union set acc
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where set = Set.fold (createSym4id pn) Set.empty 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
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where sym = CSign.Symbol on $ CSign.OpAsItemType ot
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Quantification _ _ f _) = getVars f
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Conjunction fs _) = foldr (Map.unionWith (Set.union) . getVars) Map.empty fs
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Disjunction fs _) = foldr (Map.unionWith (Set.union) . getVars) Map.empty fs
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Implication f1 f2 _ _) = Map.unionWith (Set.union) v1 v2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = getVars f1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = getVars f2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Equivalence f1 f2 _) = Map.unionWith (Set.union) v1 v2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = getVars f1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = getVars f2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Negation f _) = getVars f
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Predication _ ts _) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Definedness t _) = getVarsTerm t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Existl_equation t1 t2 _) = Map.unionWith (Set.union) v1 v2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = getVarsTerm t1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = getVarsTerm t2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Strong_equation t1 t2 _) = Map.unionWith (Set.union) v1 v2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = getVarsTerm t1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = getVarsTerm t2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Membership t _ _) = getVarsTerm t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVars (CAS.Mixfix_formula t) = getVarsTerm t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | extract the variables of a CASL term
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm :: CAS.CASLTERM -> Map.Map Id (Set.Set Token)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Qual_var var sort _) = Map.insert sort (Set.singleton var) Map.empty
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Application _ ts _) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Cast t _ _) = getVarsTerm t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Conditional t1 f t2 _) = Map.unionWith (Set.union) v3 m
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where v1 = getVarsTerm t1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v2 = getVarsTerm t2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco v3 = getVars f
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Mixfix_term ts) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Mixfix_parenthesized ts _) =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Mixfix_bracketed ts _) =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm (CAS.Mixfix_braced ts _) =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetVarsTerm _ = Map.empty