PreComorphism.hs revision b9840e4ee6fda6e42fa4ee9f337482ccc4839a39
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
fecce42517d20490f893c4a9dee29b000e1653eaAdriá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)
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 []
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
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
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
5318901bb69bf247e0f341312c800ba4ea87e46bAdriá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
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
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
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
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
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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescomapSentence sg sen@(MSentence.Equation eq) = case any MAS.owise ats of
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco False -> return $ 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
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco in return 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
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescomapSentence sg sen@(MSentence.Membership mb) = return $ 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
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescomapSentence sg sen@(MSentence.Rule rl) = return $ 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])
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescomapTheory (sg, nsens) = return $ 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 ()
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco mk = arrangeKinds (MSign.sorts msign) (MSign.subsorts msign)
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco cs = kindsFromMap mk
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco ks = kindPredicates mk
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco rp = rewPredicates ks cs
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco rs = rewPredicatesSens cs
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco ops = deletePredefined $ MSign.ops msign
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ksyms = kinds2syms cs
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco (cops, assoc_ops, ops_forms, comps) = translateOps mk ops
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco ctor_sen = [ctorSen False (cs, Rel.empty, comps)]
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco cops' = predefinedOps cs cops $ booleanImported ops
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ops_syms = ops2symbols cops'
3f8cdebaede9921402318d525b57a9af8f9279d3Adrián Riesco (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens
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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco new_sens = concat [rs, ops_forms, no_owise_forms, owise_forms, mb_rl_forms, ctor_sen]
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescobooleanImported :: MSign.OpMap -> Bool
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescobooleanImported = Map.member (mkSimpleId "if_then_else_fi")
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescodeletePredefined om = om5
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco where om1 = Map.delete (mkSimpleId "if_then_else_fi") om
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco om2 = Map.delete (mkSimpleId "_==_") om1
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco om3 = Map.delete (mkSimpleId "_=/=_") om2
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco om4 = Map.delete (mkSimpleId "upTerm") om3
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco om5 = Map.delete (mkSimpleId "downTerm") om4
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescopredefinedOps :: Set.Set Id -> CSign.OpMap -> Bool -> CSign.OpMap
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescopredefinedOps kinds om True = Set.fold predefinedOpKind om kinds
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescopredefinedOps _ om False = om
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescopredefinedOpKind :: Id -> CSign.OpMap -> CSign.OpMap
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescopredefinedOpKind kind om = om3
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco where if_id = str2id "if_then_else_fi"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco double_eq_id = str2id "_==_"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco neg_double_eq_id = str2id "_=/=_"
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco bool_id = str2id "Bool"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco if_opt = Set.singleton $ CSign.OpType CAS.Total [bool_id, kind, kind] kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco eq_opt = Set.singleton $ CSign.OpType CAS.Total [kind, kind] bool_id
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco om1 = Map.insertWith Set.union if_id if_opt om
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco om2 = Map.insertWith Set.union double_eq_id eq_opt om1
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco om3 = Map.insertWith Set.union neg_double_eq_id eq_opt om2
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescopredefinedSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescopredefinedSens = Set.fold predefinedSensKind []
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescopredefinedSensKind :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián RiescopredefinedSensKind kind acc = concat [iss, eqs, neqs, acc]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where iss = ifSens kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco eqs = equalitySens kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neqs = nonEqualitySens kind
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco-- psen = plusSen
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoifSens :: Id -> [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoifSens kind = [form'', neg_form'']
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where v1 = newVarIndex 1 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v2 = newVarIndex 2 kind
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco bk = str2id "Bool"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco bv = newVarIndex 2 bk
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco true_type = CAS.Op_type CAS.Total [] bk nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco true_id = CAS.Qual_op_name (str2id "true") true_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco true_term = CAS.Application true_id [] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco if_type = CAS.Op_type CAS.Total [bk, kind, kind] kind nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco if_name = str2id "if_then_else_fi"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco if_id = CAS.Qual_op_name if_name if_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco if_term = CAS.Application if_id [bv, v1, v2] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco prem = CAS.Strong_equation bv true_term nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco concl = CAS.Strong_equation if_term v1 nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form = CAS.Implication prem concl True nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adriá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"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form'' = makeNamed name1 form'
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_form'' = makeNamed name2 neg_form'
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoequalitySens :: Id -> [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoequalitySens kind = [form'', comp_form'']
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where v1 = newVarIndex 1 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v2 = newVarIndex 2 kind
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco bk = str2id "Bool"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco b_type = CAS.Op_type CAS.Total [] bk nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco true_term = CAS.Application true_id [] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco false_term = CAS.Application false_id [] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco prem = CAS.Strong_equation v1 v2 nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdriá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
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco concl = CAS.Strong_equation double_eq_term true_term nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form = CAS.Implication prem concl True nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form' = quantifyUniversally form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_prem = CAS.Negation prem nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adriá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 RiescononEqualitySens :: Id -> [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescononEqualitySens kind = [form'', comp_form'']
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where v1 = newVarIndex 1 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v2 = newVarIndex 2 kind
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco bk = str2id "Bool"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco b_type = CAS.Op_type CAS.Total [] bk nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco true_term = CAS.Application true_id [] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco false_term = CAS.Application false_id [] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco prem = CAS.Strong_equation v1 v2 nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdriá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
aea9000fc94442cbfc92596f4264473c0fce51e4Adriá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
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco neg_prem = CAS.Negation prem nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco new_concl = CAS.Strong_equation double_eq_term true_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 ++ "_=/=_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 RiescoplusSen :: [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoplusSen = [form'']
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco where nat_kind = str2id "Nat"
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco v1 = newVarIndex 1 nat_kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco v2 = newVarIndex 2 nat_kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco plus_type = CAS.Op_type CAS.Total [nat_kind, nat_kind] nat_kind nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco plus_id = CAS.Qual_op_name (str2id "_+_") plus_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco succ_type = CAS.Op_type CAS.Total [nat_kind] nat_kind nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco succ_id = CAS.Qual_op_name (str2id "s_") succ_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco succ_v1 = CAS.Application succ_id [v1] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco lhs = CAS.Application plus_id [succ_v1, v2] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco add_term = CAS.Application plus_id [v1, v2] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco rhs = CAS.Application succ_id [add_term] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form = CAS.Strong_equation lhs rhs nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form' = quantifyUniversally form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name = "add_+_"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form'' = makeNamed name form'
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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescotranslateOps :: IdMap -> MSign.OpMap -> OpTransTuple
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescotranslateOps im = Map.fold (translateOpDeclSet im) (Map.empty, Map.empty, [], Set.empty)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translates an operator declaration set into a tern as described above
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescotranslateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotranslateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescotranslateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescotranslateOpDecl im (syms, ats) (ops, assoc_ops, forms, cs) = (ops', assoc_ops', forms', cs')
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where predOps = ops2pred im syms
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco sym = head $ 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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco assoc_ops' = if any MAS.assoc ats
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco then Map.insertWith (Set.union) cop_id cop_type assoc_ops
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco else assoc_ops
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco cs' = if any MAS.ctor ats
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco then Set.insert (Component cop_id ot) cs
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)
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco where f = token2id . getName
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco g = \ x -> Map.findWithDefault (errorId "Maude symbol 2 CASL symbol") (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) []
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco-- | generates the membership 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 co' = token2id s
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "op-mb to predicate") co' im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco f = \ m x -> Map.lookup (token2id $ getName x) m
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ar' = mapMaybe (f im) ar
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco op_type = CAS.Op_type CAS.Total ar' kind nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco op' = CAS.Qual_op_name (token2id op) op_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (vars, prems) = ops2predPremises im ar 0
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name co' pred_type nullRange
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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco-- | creates a conjuctive formula distinguishing the size of the list
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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco-- | generates the predicates asserting the "true" sort of the operator if all
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco-- the arguments have the correct sort
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
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "mb of op as predicate") s' im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name s' pred_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco var = newVarIndex i kind
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Predication pred_name [var] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (terms, forms) = ops2predPremises im ss (i + 1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where k' = token2id k
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "mb of op as predicate") 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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco MSentence.Equation (MAS.Eq _ _ _ ats) -> case any MAS.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-- | 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-- | 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
0f77efdcc159eee5682aabf2b9a3c178c467b466Adriá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
0f77efdcc159eee5682aabf2b9a3c178c467b466Adriá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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco (_, ts, conds) = fromJust tpl
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco ts' = qualifyExVarsTerms ts
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco conds' = qualifyExVarsForms conds
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco prems = (createEqs ts' terms) ++ conds'
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco conj_form = CAS.Conjunction prems nullRange
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco ex_form = if vars' /= []
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco then CAS.Quantification CAS.Existential vars' conj_form nullRange
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco else conj_form
0f77efdcc159eee5682aabf2b9a3c178c467b466Adriá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
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco tpl = getLeftApp inner_form
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco ok = case tpl of
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco Nothing -> False
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco Just _ -> let (op, ts, _) = fromJust tpl
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco in req_op == op && length terms == length ts
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco-- | qualifies the variables in a list of formulas with the suffix "_ex" to
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco-- distinguish them from the variables already bound
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForms :: [CAS.CASLFORMULA] -> [CAS.CASLFORMULA]
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForms = map qualifyExVarsForm
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco-- | qualifies the variables in a formula with the suffix "_ex" to distinguish them
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco-- from the variables already bound
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForm (CAS.Strong_equation t t' r) = CAS.Strong_equation qt qt' r
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco where qt = qualifyExVarsTerm t
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco qt' = qualifyExVarsTerm t'
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForm (CAS.Predication op ts r) = CAS.Predication op ts' r
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco where ts' = qualifyExVarsTerms ts
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescoqualifyExVarsForm f = f
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
0f77efdcc159eee5682aabf2b9a3c178c467b466Adriá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
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
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescogetLeftApp :: CAS.CASLFORMULA -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM], [CAS.CASLFORMULA])
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetLeftApp (CAS.Strong_equation term _ _) = case getLeftAppTerm term of
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco Nothing -> Nothing
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco Just (op, ts) -> Just (op, ts, [])
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescogetLeftApp (CAS.Implication prem concl _ _) = case getLeftApp concl of
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco Nothing -> Nothing
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco Just (op, ts, _) -> Just (op, ts, conds)
fecce42517d20490f893c4a9dee29b000e1653eaAdriá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
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco-- | extracts the formulas of the given premise, distinguishing whether it is
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián Riesco-- a conjunction or not
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescogetPremisesImplication :: CAS.CASLFORMULA -> [CAS.CASLFORMULA]
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescogetPremisesImplication (CAS.Conjunction forms _) = forms
0f77efdcc159eee5682aabf2b9a3c178c467b466Adrián RiescogetPremisesImplication form = [form]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | translate a Maude membership into a CASL formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescomb2formula im (MAS.Mb t s [] _) = quantifyUniversally form
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where ct = maudeTerm2caslTerm im t
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco s' = token2id $ getName s
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "mb to formula") s' im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name s' pred_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco 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
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco s' = token2id $ getName s
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "mb to formula") s' im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name s' pred_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco 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
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco where ty = token2id $ getName $ MAS.getTermType t
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "rl to formula") ty im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name rewID pred_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco form = CAS.Predication pred_name [ct, ct'] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescorl2formula im (MAS.Rl t t' conds@(_:_) _) = quantifyUniversally form
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco where ty = token2id $ getName $ MAS.getTermType t
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "rl to formula") ty im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name rewID pred_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ct = maudeTerm2caslTerm im t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ct' = maudeTerm2caslTerm im t'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco conds_form = conds2formula im conds
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco concl_form = CAS.Predication pred_name [ct, ct'] nullRange
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
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco s' = token2id $ getName s
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "mb cond to formula") s' im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name s' pred_type nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián 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'
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ty = token2id $ getName $ MAS.getTermType t
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "rw cond to formula") ty im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_name = CAS.Qual_pred_name rewID pred_type nullRange
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
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco where kind = Map.findWithDefault (errorId "maude term to CASL term") (token2id $ getName ty) im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescomaudeTerm2caslTerm im (MAS.Const q ty) = CAS.Application op [] nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where name = token2id q
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ty' = token2id $ getName ty
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "maude term to CASL term") ty' im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco op_type = CAS.Op_type CAS.Total [] kind nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco op = CAS.Qual_op_name name op_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescomaudeTerm2caslTerm im (MAS.Apply q ts ty) = CAS.Application op tts nullRange
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco where name = token2id q
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco tts = map (maudeTerm2caslTerm im) ts
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ty' = token2id $ getName ty
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco kind = Map.findWithDefault (errorId "maude term to CASL term") ty' im
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco types_tts = getTypes tts
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco op_type = CAS.Op_type CAS.Total types_tts kind nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco op = CAS.Qual_op_name name op_type nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetTypes :: [CAS.CASLTERM] -> [Id]
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetTypes = mapMaybe getType
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetType :: CAS.CASLTERM -> Maybe Id
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetType (CAS.Qual_var _ kind _) = Just kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetType (CAS.Application op _ _) = case op of
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco CAS.Qual_op_name _ (CAS.Op_type _ _ kind _) _ -> Just kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescogetType _ = Nothing
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescorewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescorewPredicatesSens = Set.fold rewPredicateSens []
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescorewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescorewPredicateSens kind acc = [ref, trans] ++ acc
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where ref = reflSen kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco trans = transSen kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | creates the reflexivity predicate for the given kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoreflSen :: Id -> Named CAS.CASLFORMULA
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescoreflSen kind = makeNamed name $ quantifyUniversally form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where v = newVar kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pn = CAS.Qual_pred_name rewID pred_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form = CAS.Predication pn [v, v] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name = "rew_refl_" ++ show kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | creates the transitivity predicate for the given kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotransSen :: Id -> Named CAS.CASLFORMULA
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotransSen kind = makeNamed name $ quantifyUniversally form
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco where v1 = newVarIndex 1 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v2 = newVarIndex 2 kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco v3 = newVarIndex 3 kind
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pred_type = CAS.Pred_type [kind, kind] nullRange
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco pn = CAS.Qual_pred_name rewID pred_type nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco prem1 = CAS.Predication pn [v1, v2] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco prem2 = CAS.Predication pn [v2, v3] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco concl = CAS.Predication pn [v1, v3] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco conj_form = CAS.Conjunction [prem1, prem2] nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco form = CAS.Implication conj_form concl True nullRange
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco name = "rew_trans_" ++ show kind
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | generate the predicates for the rewrites
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)
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescokindPredicate sort kind mis = case sort == (str2id "Universal") of
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco False -> let ar = Set.singleton $ CSign.PredType [kind]
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | extract the kinds from the map of id's
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescokindsFromMap :: IdMap -> Set.Set Id
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
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco-- | return the maximal elements from the sort relation
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescogetTop r tok = case succs of
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
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riescotoken2id t = mkId ts
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco where ts = maudeSymbol2validCASLSymbol t
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | build an Id from a Maude symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescosym2id :: MSym.Symbol -> Id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescosym2id = token2id . getName
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riescostr2id :: String -> Id
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riescostr2id = token2id . mkSimpleId
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco-- | build an Id from a list of sorts, taking the first from the ordered list
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescosort2id :: [MSym.Symbol] -> Id
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riescosort2id syms = mkId sym''
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco where sym = head $ List.sort syms
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco sym' = getName sym
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco sym'' = maudeSymbol2validCASLSymbol sym'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | add universal quantification of all variables in the formula
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoquantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA
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-- | 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
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescogetVarsTerm _ = Map.empty
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco-- | generates the constructor constraint
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescoctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA
fecce42517d20490f893c4a9dee29b000e1653eaAdrián RiescoctorSen isFree (sorts, _, ops) = do
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco let sortList = Set.toList sorts
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco (CSign.toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco allSyms = opSyms
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco resType _ (CAS.Op_name _) = False
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco resType s (CAS.Qual_op_name _ t _) = CAS.res_OP_TYPE t == s
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco getIndex s = maybe (-1) id $ List.findIndex (== s) sortList
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco addIndices (CAS.Op_name _) =
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco error "CASL/StaticAna: Internal error in function addIndices"
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco addIndices os@(CAS.Qual_op_name _ t _) =
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco (os,map getIndex $ CAS.args_OP_TYPE t)
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco collectOps s =
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco constrs = map collectOps sortList
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco f = CAS.Sort_gen_ax constrs isFree
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco makeNamed ("ga_generated_" ++ showSepList (showString "_") showId sortList "") f
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescomaudeSymbol2validCASLSymbol :: Token -> [Token]
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescomaudeSymbol2validCASLSymbol t = splitDoubleUnderscores str ""
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco where str = ms2vcs $ show t
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riescoms2vcs :: String -> String
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riescoms2vcs s = case Map.member s stringMap of
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco True -> Map.findWithDefault "" s stringMap
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco False -> let f = \ x y -> if Map.member x charMap
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco then (charMap Map.! x) ++ ['\''] ++ y
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco else if x == '_'
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco then "__" ++ y
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco in foldr f [] s
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco-- | map of reserved words
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescostringMap :: Map.Map String String
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco [("true", "maudeTrue"),
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco ("false", "maudeFalse")]
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco-- | splits the string into a list of tokens, separating the double
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco-- underscores from the rest of characters
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescosplitDoubleUnderscores :: String -> String -> [Token]
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescosplitDoubleUnderscores [] acc = if null acc
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco else [mkSimpleId acc]
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescosplitDoubleUnderscores ('_' : '_' : cs) acc = if null acc
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco then dut : rest
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco else acct : dut : rest
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco where acct = mkSimpleId acc
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco dut = mkSimpleId "__"
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco rest = splitDoubleUnderscores cs []
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescosplitDoubleUnderscores (c : cs) acc = splitDoubleUnderscores cs (acc ++ [c])
7474965b2e6323002c96c0b39a59843cde201870Adrián RiescoerrorId :: String -> Id
7474965b2e6323002c96c0b39a59843cde201870Adrián RiescoerrorId s = token2id $ mkSimpleId $ "ERROR: " ++ s