PreComorphism.hs revision 6d498b6f56ed9f71cced898b6c42fb48f6e60583
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesModule : $Header$
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesDescription : Maude Comorphisms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesCopyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesMaintainer : ariesco@fdi.ucm.es
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesStability : experimental
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesPortability : portable
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesComorphism from Maude to CASL.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Data.List as List
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Data.Set as Set
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Data.Map as Map
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Maude.Sign as MSign
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Maude.Sentence as MSentence
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Maude.Morphism as MMorphism
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Maude.AS_Maude as MAS
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Maude.Symbol as MSym
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified CASL.Sign as CSign
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified CASL.Morphism as CMorphism
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified CASL.AS_Basic_CASL as CAS
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Common.ProofUtils (charMap)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport qualified Common.Lib.Rel as Rel
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestype IdMap = Map.Map Id Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestype OpTransTuple = (CSign.OpMap, CSign.OpMap, Set.Set Component)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates a CASL morphism from a Maude morphism
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapMorphism :: MMorphism.Morphism -> Result (CMorphism.CASLMor)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapMorphism morph =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes mk = kindMapId $ MSign.kindRel src
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes cs = kindsFromMap mk
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes smap' = applySortMap2CASLSorts smap cs
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes omap' = maudeOpMap2CASLOpMap mk omap
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pmap = createPredMap mk smap
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (src', _) = maude2casl src []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (tgt', _) = maude2casl tgt []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates the Maude morphism between operators into a CASL morpshim between
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates the mapping between two symbols representing operators into
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- a CASL operators map
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestranslateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm = copm'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where f = token2id . getName
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes g = \ x -> Map.findWithDefault (errorId "translate op map entry") (f x) im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes cop = (token2id from, ot)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes to' = (token2id to, CAS.Total)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes copm' = Map.insert cop to' copm
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestranslateOpMapEntry _ _ _ _ = Map.empty
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates a set of CASL symbol from a Maude Symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where mk = kindMapId $ MSign.kindRel sg
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes sym_id = token2id q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes kind = Map.findWithDefault (errorId "map symbol") sym_id mk
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_data = CSign.PredType [kind]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapSymbol sg (MSym.Operator q ar co) = Set.singleton csym
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where mk = kindMapId $ MSign.kindRel sg
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes q' = token2id q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ar' = map (maudeSort2caslId mk) ar
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes co' = token2id $ getName co
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes csym = CSign.Symbol q' $ CSign.OpAsItemType op_data
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapSymbol _ _ = Set.empty
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | returns the sort in CASL of the Maude sort symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSort2caslId :: IdMap -> MSym.Symbol -> Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id") (token2id $ getName sym) im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | creates the predicate map for the CASL morphism from the Maude sort map and
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- the map between sorts and kinds
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreatePredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreatePredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | creates an entry of the predicate map for a single sort
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreatePredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreatePredMap4sort im from to m = Map.insert key id_to m
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where id_from = token2id $ getName from
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes id_to = token2id $ getName to
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes kind = Map.findWithDefault (errorId "predicate for sort") id_from im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes key = (id_from, CSign.PredType [kind])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | computes the sort morphism of CASL from the sort morphism in Maude and the set
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesapplySortMap2CASLSorts :: MMorphism.SortMap -> Set.Set Id -> CMorphism.Sort_map
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesapplySortMap2CASLSorts sm = Set.fold (applySortMap2CASLSort sm) Map.empty
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | computes the morphism for a single kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesapplySortMap2CASLSort :: MMorphism.SortMap -> Id -> CMorphism.Sort_map -> CMorphism.Sort_map
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesapplySortMap2CASLSort sm sort csm = new_csm
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where toks = getTokens sort
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes new_toks = map (rename sm) toks
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes new_sort = mkId new_toks
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes new_csm = if new_sort == sort
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else Map.insert sort new_sort csm
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | renames the sorts in a given kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrename :: MMorphism.SortMap -> Token -> Token
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrename sm tok = new_tok
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where sym = MSym.Sort tok
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes sym' = if Map.member sym sm
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes then fromJust $ Map.lookup sym sm
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes new_tok = getName sym'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates a Maude sentence into a CASL formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapSentence sg sen@(MSentence.Equation eq) = case any MAS.owise ats of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes False -> return $ sentence $ noOwiseSen2Formula mk named
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (no_owise_sens, _, _) = splitOwiseEqs sg_sens
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes trans = sentence $ owiseSen2Formula mk no_owise_forms named
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in return trans
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where mk = kindMapId $ MSign.kindRel sg
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes MAS.Eq _ _ _ ats = eq
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes named = makeNamed "" sen
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapSentence sg sen@(MSentence.Membership mb) = return $ sentence form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where mk = kindMapId $ MSign.kindRel sg
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes MAS.Mb _ _ _ _ = mb
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes named = makeNamed "" sen
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = mb_rl2formula mk named
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapSentence sg sen@(MSentence.Rule rl) = return $ sentence form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where mk = kindMapId $ MSign.kindRel sg
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes MAS.Rl _ _ _ _ = rl
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes named = makeNamed "" sen
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = mb_rl2formula mk named
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | applies maude2casl to compute the CASL signature and sentences from
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- the Maude ones, and wraps them into a Result datatype
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapTheory :: (MSign.Sign, [Named MSentence.Sentence])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmapTheory (sg, nsens) = return $ maude2casl sg nsens
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | computes new signature and sentences of CASL associated to the
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- given Maude signature and sentences
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaude2casl :: MSign.Sign -> [Named MSentence.Sentence]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaude2casl msign nsens = (csign { CSign.sortSet = cs,
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes CSign.declaredSymbols = syms }, new_sens)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where csign = CSign.emptySign ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ss' = Set.map sym2id ss
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes mk = kindMapId $ MSign.kindRel msign
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes sbs' = maudeSbs2caslSbs sbs mk
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes cs = Set.union ss' $ kindsFromMap mk
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes preds = rewPredicates cs
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes rs = rewPredicatesSens cs
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ops = deleteUniversal $ MSign.ops msign
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ksyms = kinds2syms cs
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (cops, assoc_ops, _) = translateOps mk ops -- (cops, assoc_ops, comps)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes cops' = universalOps cs cops $ booleanImported ops
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes rs' = rewPredicatesCongSens cops'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_forms = loadLibraries (MSign.sorts msign) ops
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ops_syms = ops2symbols cops'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes preds_syms = preds2syms preds
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes syms = Set.union ksyms $ Set.union ops_syms preds_syms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes new_sens = concat [rs, rs', no_owise_forms, owise_forms,
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes mb_rl_forms, ctor_sen, pred_forms]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates the Maude subsorts into CASL subsorts, and adds the subsorts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- for the kinds
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSbs2caslSbs :: MSign.SubsortRel -> IdMap -> Rel.Rel CAS.SORT
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSbs2caslSbs sbs im = Rel.fromDistinctMap m4
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes l1 = [] -- map maudeSb2caslSb l
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes l2 = idList2Subsorts $ Map.toList im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes l3 = map subsorts2Ids l
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes m4 = Map.unionWith Set.union m1 $ Map.unionWith Set.union m2 m3
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesidList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesidList2Subsorts [] = []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesidList2Subsorts ((id1, id2) : il) = t1 : idList2Subsorts il
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where t1 = (id1, Set.singleton id2)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSb2caslSb :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSb2caslSb (sym, st) = (sortSym2id sym, Set.map (kindId . sortSym2id) st)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessubsorts2Ids :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessubsorts2Ids (sym, st) = (sortSym2id sym, Set.map sortSym2id st)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessortSym2id :: MSym.Symbol -> Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessortSym2id (MSym.Sort q) = token2id q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessortSym2id _ = token2id $ mkSimpleId $ "error_translation"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the sentences to state that the rew predicates are a congruence
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredicatesCongSens = Map.foldWithKey rewPredCongSet []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the sentences to state that the rew predicates are a congruence
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- for the operator types in the set
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredCongSet :: Id -> Set.Set CSign.OpType -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredCongSet idn ots fs = fs ++ fs'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where fs' = Set.fold (rewPredCong idn) [] ots
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the sentences to state that the rew predicates are a congruence
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- for a single operator
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredCong :: Id -> CSign.OpType -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredCong op ot fs = case args of
e18ba90a1e610b43062e90cfa8bf0c1edcad7a49bnicholes _ -> nq_form : fs
e18ba90a1e610b43062e90cfa8bf0c1edcad7a49bnicholes where args = CSign.opArgs ot
e18ba90a1e610b43062e90cfa8bf0c1edcad7a49bnicholes vars1 = rewPredCongPremise 0 args
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes vars2 = rewPredCongPremise (length args) args
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes res_pred_type = CAS.Pred_type [res, res] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pn = CAS.Qual_pred_name rewID res_pred_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes name = "rew_cong_" ++ show op
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes prems = rewPredsCong args vars1 vars2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes prems_conj = createConjForm prems
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes os = CAS.Qual_op_name op (CSign.toOP_TYPE ot) nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes conc_term1 = CAS.Application os vars1 nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes conc_term2 = CAS.Application os vars2 nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes conc_form = CAS.Predication pn [conc_term1, conc_term2] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = createImpForm prems_conj conc_form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes nq_form = makeNamed name $ quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates a list of variables of the given sorts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredCongPremise n (s : ss) = newVarIndex n s : rewPredCongPremise (n + 1) ss
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredCongPremise _ [] = []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates a list of rew predicates with the given variables
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredsCong (s : ss) (t : ts) (t' : ts') = form : forms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where pred_type = CAS.Pred_type [s, s] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pn = CAS.Qual_pred_name rewID pred_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Predication pn [t, t'] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes forms = rewPredsCong ss ts ts'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredsCong _ _ _ = []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | load the CASL libraries for the Maude built-in operators
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesloadLibraries :: MSign.SortSet -> MSign.OpMap -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesloadLibraries ss om = case natImported ss om of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes True -> loadNaturalNatSens
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | loads the sentences associated to the natural numbers
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesloadNaturalNatSens :: [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesloadNaturalNatSens =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let lib = head $ unsafePerformIO $ readLib "Maude/MaudeNumbers.casl"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in case lib of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes G_theory lid _ _ thSens _ -> let sens = toNamedList thSens
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes sens' <- coerceSens lid CASL "" sens
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes filter (not . ctorCons) sens'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | checks if a sentence is an constructor sentence
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesctorCons :: Named CAS.CASLFORMULA -> Bool
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesctorCons f = case sentence f of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | checks if the boolean values are imported
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesbooleanImported :: MSign.OpMap -> Bool
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesbooleanImported = Map.member (mkSimpleId "if_then_else_fi")
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | checks if the natural numbers are imported
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnatImported :: MSign.SortSet -> MSign.OpMap -> Bool
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnatImported ss om = b1 && b2 && b3
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where b1 = Set.member (MSym.Sort $ mkSimpleId "Nat") ss
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes b2 = Map.member (mkSimpleId "s_") om
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes b3 = case b2 of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes False -> True
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes True -> specialZeroSet $ om Map.! (mkSimpleId "s_")
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesspecialZeroSet :: MSign.OpDeclSet -> Bool
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesspecialZeroSet = Set.fold specialZero False
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesspecialZero :: MSign.OpDecl -> Bool -> Bool
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesspecialZero (_, ats) b = b' || b
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where b' = isSpecial ats
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesisSpecial :: [MAS.Attr] -> Bool
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesisSpecial [] = False
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesisSpecial ((MAS.Special _) : _) = True
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesisSpecial (_ : ats) = isSpecial ats
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | delete the universal operators from Maude specifications, that will be
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- substituted for one operator for each sort in the specification
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdeleteUniversal om = om5
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where om1 = Map.delete (mkSimpleId "if_then_else_fi") om
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes om2 = Map.delete (mkSimpleId "_==_") om1
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes om3 = Map.delete (mkSimpleId "_=/=_") om2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes om4 = Map.delete (mkSimpleId "upTerm") om3
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes om5 = Map.delete (mkSimpleId "downTerm") om4
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the universal operators for all the sorts in the module
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesuniversalOps :: Set.Set Id -> CSign.OpMap -> Bool -> CSign.OpMap
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesuniversalOps kinds om True = Set.fold universalOpKind om kinds
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesuniversalOps _ om False = om
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the universal operators for a concrete module
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesuniversalOpKind :: Id -> CSign.OpMap -> CSign.OpMap
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesuniversalOpKind kind om = om3
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where if_id = str2id "if_then_else_fi"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes double_eq_id = str2id "_==_"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes neg_double_eq_id = str2id "_=/=_"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes bool_id = str2id "Bool"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes if_opt = Set.singleton $ CSign.OpType CAS.Total [bool_id, kind, kind] kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes eq_opt = Set.singleton $ CSign.OpType CAS.Total [kind, kind] bool_id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes om2 = Map.insertWith Set.union double_eq_id eq_opt om1
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes om3 = Map.insertWith Set.union neg_double_eq_id eq_opt om2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the formulas for the universal operators
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesuniversalSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesuniversalSens = Set.fold universalSensKind []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the formulas for the universal operators for the given sort
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesuniversalSensKind :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesuniversalSensKind kind acc = concat [iss, eqs, neqs, acc]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where iss = ifSens kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes eqs = equalitySens kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes neqs = nonEqualitySens kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the formulas for the if statement
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesifSens :: Id -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesifSens kind = [form'', neg_form'']
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where v1 = newVarIndex 1 kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v2 = newVarIndex 2 kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes bk = str2id "Bool"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes bv = newVarIndex 2 bk
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes true_id = CAS.Qual_op_name (str2id "true") true_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes true_term = CAS.Application true_id [] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes if_type = CAS.Op_type CAS.Total [bk, kind, kind] kind nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes if_name = str2id "if_then_else_fi"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes if_id = CAS.Qual_op_name if_name if_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes if_term = CAS.Application if_id [bv, v1, v2] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes prem = CAS.Strong_equation bv true_term nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes concl = CAS.Strong_equation if_term v1 nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Implication prem concl True nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form' = quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes neg_prem = CAS.Negation prem nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes neg_concl = CAS.Strong_equation if_term v2 nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes neg_form = CAS.Implication neg_prem neg_concl True nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes neg_form' = quantifyUniversally neg_form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes name1 = show kind ++ "_if_true"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes name2 = show kind ++ "_if_false"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form'' = makeNamed name1 form'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes neg_form'' = makeNamed name2 neg_form'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the formulas for the equality
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesequalitySens :: Id -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesequalitySens kind = [form'', comp_form'']
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where v1 = newVarIndex 1 kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v2 = newVarIndex 2 kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes bk = str2id "Bool"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes true_term = CAS.Application true_id [] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes false_term = CAS.Application false_id [] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes prem = CAS.Strong_equation v1 v2 nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes double_eq_name = str2id "_==_"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes concl = CAS.Strong_equation double_eq_term true_term nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Implication prem concl True nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form' = quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes neg_prem = CAS.Negation prem nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes new_concl = CAS.Strong_equation double_eq_term false_term nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes comp_form = CAS.Implication neg_prem new_concl True nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes comp_form' = quantifyUniversally comp_form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes name1 = show kind ++ "_==_true"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes name2 = show kind ++ "_==_false"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form'' = makeNamed name1 form'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes comp_form'' = makeNamed name2 comp_form'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the formulas for the inequality
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnonEqualitySens :: Id -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnonEqualitySens kind = [form'', comp_form'']
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where v1 = newVarIndex 1 kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v2 = newVarIndex 2 kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes bk = str2id "Bool"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes true_term = CAS.Application true_id [] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes false_term = CAS.Application false_id [] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes prem = CAS.Strong_equation v1 v2 nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes double_eq_name = str2id "_==_"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes concl = CAS.Strong_equation double_eq_term false_term nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Implication prem concl True nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form' = quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes neg_prem = CAS.Negation prem nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes new_concl = CAS.Strong_equation double_eq_term true_term nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes comp_form = CAS.Implication neg_prem new_concl True nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes comp_form' = quantifyUniversally comp_form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes name1 = show kind ++ "_=/=_false"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes name2 = show kind ++ "_=/=_true"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form'' = makeNamed name1 form'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes comp_form'' = makeNamed name2 comp_form'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates the Maude operator map into a tuple of CASL operators, CASL
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- associative operators, membership induced from each Maude operator,
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- and the set of sorts with the ctor attribute
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestranslateOps :: IdMap -> MSign.OpMap -> OpTransTuple
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestranslateOps im = Map.fold (translateOpDeclSet im) (Map.empty, Map.empty, Set.empty)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates an operator declaration set into a tern as described above
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestranslateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestranslateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | given an operator declaration updates the accumulator with the translation
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- to CASL operator, checking if the operator has the assoc attribute to insert
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- it in the map of associative operators, generating the membership predicate
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- induced by the operator declaration, and checking if it has the ctor attribute
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- to introduce the operator in the generators sentence
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestranslateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestranslateOpDecl im (syms, ats) (ops, assoc_ops, cs) = case tl of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes [] -> (ops', assoc_ops', cs')
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes _ -> translateOpDecl im (syms', ats) (ops', assoc_ops', cs')
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where sym = head $ Set.toList syms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes tl = tail $ Set.toList syms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (cop_id, ot, _) = fromJust $ maudeSym2CASLOp im sym
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes cop_type = Set.singleton ot -- Set.union (Set.singleton ot) (Set.singleton ot')
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ops' = Map.insertWith (Set.union) cop_id cop_type ops
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes assoc_ops' = if any MAS.assoc ats
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes then Map.insertWith (Set.union) cop_id cop_type assoc_ops
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else assoc_ops
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes cs' = if any MAS.ctor ats
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes then Set.insert (Component cop_id ot) cs
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates a Maude operator symbol into a pair with the id of the operator
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- and its CASL type
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSym2CASLOp :: IdMap -> MSym.Symbol -> Maybe (Id, CSign.OpType, CSign.OpType)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot, ot')
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where f = token2id . getName
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes g = \ x -> maudeSymbol2caslSort x im -- \ x -> Map.findWithDefault (errorId "Maude_sym2CASL_sym") (f x) im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSym2CASLOp _ _ = Nothing
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | creates a conjuctive formula distinguishing the size of the list
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateConjForm [] = CAS.True_atom nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateConjForm [a] = a
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateConjForm fs = CAS.Conjunction fs nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | creates a implication formula distinguishing the size of the premises
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateImpForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA -> CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateImpForm (CAS.True_atom _) form = form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateImpForm form1 form2 = CAS.Implication form1 form2 True nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the predicates asserting the "true" sort of the operator if all
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- the arguments have the correct sort
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesops2predPremises :: IdMap -> [MSym.Symbol] -> Int -> ([CAS.CASLTERM], [CAS.CASLFORMULA])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesops2predPremises im (MSym.Sort s : ss) i = (var : terms, form : forms)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where s' = token2id s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes kind = Map.findWithDefault (errorId "mb of op as predicate") s' im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_type = CAS.Pred_type [kind] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_name = CAS.Qual_pred_name s' pred_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes var = newVarIndex i kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Predication pred_name [var] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (terms, forms) = ops2predPremises im ss (i + 1)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where k' = token2id k
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes kind = Map.findWithDefault (errorId "mb of op as predicate") k' im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes var = newVarIndex i kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (terms, forms) = ops2predPremises im ss (i + 1)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesops2predPremises _ _ _ = ([], [])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | traverses the Maude sentences, returning a pair of list of sentences.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- The first list in the pair are the equations without the attribute "owise",
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- while the second one are the equations with this attribute
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessplitOwiseEqs :: [Named MSentence.Sentence] ->
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ([Named MSentence.Sentence], [Named MSentence.Sentence], [Named MSentence.Sentence])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessplitOwiseEqs [] = ([], [], [])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessplitOwiseEqs (s : ss) = res
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes sen = sentence s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes res = case sen of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes MSentence.Equation (MAS.Eq _ _ _ ats) -> case any MAS.owise ats of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes True -> (no_owise_sens, s : owise_sens, mbs_rls)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes False -> (s : no_owise_sens, owise_sens, mbs_rls)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes _ -> (no_owise_sens, owise_sens, s : mbs_rls)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates a Maude equation defined without the "owise" attribute into
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- a CASL formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnoOwiseSen2Formula :: IdMap -> Named MSentence.Sentence
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnoOwiseSen2Formula im s = s'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where MSentence.Equation eq = sentence s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes sen' = noOwiseEq2Formula im eq
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes s' = s { sentence = sen' }
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates a Maude equation defined with the "owise" attribute into
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- a CASL formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesowiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesowiseSen2Formula im owise_forms s = s'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where MSentence.Equation eq = sentence s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes sen' = owiseEq2Formula im owise_forms eq
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes s' = s { sentence = sen' }
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates a Maude membership or rule into a CASL formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmb_rl2formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmb_rl2formula im s = case sen of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes mb' = mb2formula im mb
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in s { sentence = mb' }
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes rl' = rl2formula im rl
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in s { sentence = rl' }
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes _ -> makeNamed "" $ CAS.False_atom nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where sen = sentence s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates a new variable qualified with the given number
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnewVarIndex :: Int -> Id -> CAS.CASLTERM
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnewVarIndex i sort = CAS.Qual_var var sort nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where var = mkSimpleId $ "V" ++ show i
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates a new variable
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnewVar :: Id -> CAS.CASLTERM
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnewVar sort = CAS.Qual_var var sort nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where var = mkSimpleId "V"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | Id for the rew predicate
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewID = token2id $ mkSimpleId "rew"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates a Maude equation without the "owise" attribute into a CASL formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnoOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnoOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ct = maudeTerm2caslTerm im t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ct' = maudeTerm2caslTerm im t'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Strong_equation ct ct' nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnoOwiseEq2Formula im (MAS.Eq t t' conds@(_:_) _) = quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ct = maudeTerm2caslTerm im t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ct' = maudeTerm2caslTerm im t'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes conds_form = conds2formula im conds
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes concl_form = CAS.Strong_equation ct ct' nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = createImpForm conds_form concl_form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | transforms a Maude equation defined with the otherwise attribute into
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- a CASL formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesowiseEq2Formula :: IdMap -> [Named CAS.CASLFORMULA] -> MAS.Equation
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesowiseEq2Formula im no_owise_form eq = form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where (eq_form, vars) = noQuantification $ noOwiseEq2Formula im eq
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (op, ts, _) = fromJust $ getLeftApp eq_form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ex_form = existencialNegationOtherEqs op ts no_owise_form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes imp_form = createImpForm ex_form eq_form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Quantification CAS.Universal vars imp_form nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates a conjunction of negation of existencial quantifiers
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesexistencialNegationOtherEqs :: CAS.OP_SYMB -> [CAS.CASLTERM] ->
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesexistencialNegationOtherEqs op ts forms = form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ex_forms = foldr ((++) . existencialNegationOtherEq op ts) [] forms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = if length ex_forms > 1
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes then CAS.Conjunction ex_forms nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else head ex_forms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | given a formula, if it refers to the same operator indicated by the parameters
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- the predicate creates a list with the negation of the existence of variables that
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- match the pattern described in the formula. In other case it returns an empty list
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesexistencialNegationOtherEq :: CAS.OP_SYMB -> [CAS.CASLTERM] ->
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesexistencialNegationOtherEq req_op terms form = case ok of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (_, ts, conds) = fromJust tpl
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ts' = qualifyExVarsTerms ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes conds' = qualifyExVarsForms conds
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes prems = (createEqs ts' terms) ++ conds'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes conj_form = CAS.Conjunction prems nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ex_form = if vars' /= []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes then CAS.Quantification CAS.Existential vars' conj_form nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else conj_form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes neg_form = CAS.Negation ex_form nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in [neg_form]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where (inner_form, vars) = noQuantification $ sentence form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes vars' = qualifyExVars vars
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes tpl = getLeftApp inner_form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ok = case tpl of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> False
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just _ -> let (op, ts, _) = fromJust tpl
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in req_op == op && length terms == length ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | qualifies the variables in a list of formulas with the suffix "_ex" to
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- distinguish them from the variables already bound
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsForms :: [CAS.CASLFORMULA] -> [CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsForms = map qualifyExVarsForm
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | qualifies the variables in a formula with the suffix "_ex" to distinguish them
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- from the variables already bound
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsForm (CAS.Strong_equation t t' r) = CAS.Strong_equation qt qt' r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where qt = qualifyExVarsTerm t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes qt' = qualifyExVarsTerm t'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsForm (CAS.Predication op ts r) = CAS.Predication op ts' r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ts' = qualifyExVarsTerms ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsForm f = f
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | qualifies the variables in a list of terms with the suffix "_ex" to
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- distinguish them from the variables already bound
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerms :: [CAS.CASLTERM] -> [CAS.CASLTERM]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerms = map qualifyExVarsTerm
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | qualifies the variables in a term with the suffix "_ex" to distinguish them
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- from the variables already bound
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerm (CAS.Qual_var var sort r) = CAS.Qual_var (qualifyExVarAux var) sort r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerm (CAS.Application op ts r) = CAS.Application op ts' r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ts' = map qualifyExVarsTerm ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerm (CAS.Sorted_term t s r) = CAS.Sorted_term (qualifyExVarsTerm t) s r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerm (CAS.Cast t s r) = CAS.Cast (qualifyExVarsTerm t) s r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerm (CAS.Conditional t1 f t2 r) = CAS.Conditional t1' f t2' r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where t1' = qualifyExVarsTerm t1
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes t2' = qualifyExVarsTerm t2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerm (CAS.Mixfix_term ts) = CAS.Mixfix_term ts'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ts' = map qualifyExVarsTerm ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerm (CAS.Mixfix_parenthesized ts r) = CAS.Mixfix_parenthesized ts' r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ts' = map qualifyExVarsTerm ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerm (CAS.Mixfix_bracketed ts r) = CAS.Mixfix_bracketed ts' r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ts' = map qualifyExVarsTerm ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerm (CAS.Mixfix_braced ts r) = CAS.Mixfix_braced ts' r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ts' = map qualifyExVarsTerm ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarsTerm t = t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | qualifies a list of variables with the suffix "_ex" to
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- distinguish them from the variables already bound
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVars = map qualifyExVar
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | qualifies a variable with the suffix "_ex" to distinguish it from
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- the variables already bound
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVar (CAS.Var_decl vars s r) = CAS.Var_decl vars' s r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where vars' = map qualifyExVarAux vars
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | qualifies a token with the suffix "_ex"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarAux :: Token -> Token
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesqualifyExVarAux var = mkSimpleId $ show var ++ "_ex"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | creates a list of strong equalities from two lists of terms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateEqs :: [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateEqs (t1 : ts1) (t2 : ts2) = CAS.Strong_equation t1 t2 nullRange : ls
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ls = createEqs ts1 ts2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateEqs _ _ = []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | extracts the operator at the top and the arguments of the lefthand side
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- in a strong equation
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetLeftApp :: CAS.CASLFORMULA -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM], [CAS.CASLFORMULA])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetLeftApp (CAS.Strong_equation term _ _) = case getLeftAppTerm term of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> Nothing
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just (op, ts) -> Just (op, ts, [])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetLeftApp (CAS.Implication prem concl _ _) = case getLeftApp concl of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Nothing -> Nothing
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Just (op, ts, _) -> Just (op, ts, conds)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where conds = getPremisesImplication prem
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetLeftApp _ = Nothing
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | extracts the operator at the top and the arguments of the lefthand side
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- in an application term
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetLeftAppTerm :: CAS.CASLTERM -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetLeftAppTerm (CAS.Application op ts _) = Just (op, ts)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetLeftAppTerm _ = Nothing
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | extracts the formulas of the given premise, distinguishing whether it is
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- a conjunction or not
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetPremisesImplication :: CAS.CASLFORMULA -> [CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetPremisesImplication (CAS.Conjunction forms _) = forms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetPremisesImplication form = [form]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translate a Maude membership into a CASL formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmb2formula im (MAS.Mb t s [] _) = quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ct = maudeTerm2caslTerm im t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes s' = token2id $ getName s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Membership ct s' nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmb2formula im (MAS.Mb t s conds@(_ : _) _) = quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ct = maudeTerm2caslTerm im t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes s' = token2id $ getName s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes conds_form = conds2formula im conds
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes concl_form = CAS.Membership ct s' nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Implication conds_form concl_form True nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translate a Maude rule into a CASL formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrl2formula im (MAS.Rl t t' [] _) = quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ty = token2id $ getName $ MAS.getTermType t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes kind = Map.findWithDefault (errorId "rl to formula") ty im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_type = CAS.Pred_type [kind, kind] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_name = CAS.Qual_pred_name rewID pred_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ct = maudeTerm2caslTerm im t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ct' = maudeTerm2caslTerm im t'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Predication pred_name [ct, ct'] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrl2formula im (MAS.Rl t t' conds@(_:_) _) = quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ty = token2id $ getName $ MAS.getTermType t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes kind = Map.findWithDefault (errorId "rl to formula") ty im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_type = CAS.Pred_type [kind, kind] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_name = CAS.Qual_pred_name rewID pred_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ct = maudeTerm2caslTerm im t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ct' = maudeTerm2caslTerm im t'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes conds_form = conds2formula im conds
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes concl_form = CAS.Predication pred_name [ct, ct'] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Implication conds_form concl_form True nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translate a conjunction of Maude conditions to a CASL formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesconds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesconds2formula im conds = CAS.Conjunction forms nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where forms = map (cond2formula im) conds
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translate a single Maude condition to a CASL formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescond2formula im (MAS.EqCond t t') = CAS.Strong_equation ct ct' nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ct = maudeTerm2caslTerm im t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ct' = maudeTerm2caslTerm im t'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescond2formula im (MAS.MatchCond t t') = CAS.Strong_equation ct ct' nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ct = maudeTerm2caslTerm im t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ct' = maudeTerm2caslTerm im t'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescond2formula im (MAS.MbCond t s) = CAS.Membership ct s' nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ct = maudeTerm2caslTerm im t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes s' = token2id $ getName s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescond2formula im (MAS.RwCond t t') = CAS.Predication pred_name [ct, ct'] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ct = maudeTerm2caslTerm im t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ct' = maudeTerm2caslTerm im t'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ty = token2id $ getName $ MAS.getTermType t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes kind = Map.findWithDefault (errorId "rw cond to formula") ty im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_type = CAS.Pred_type [kind, kind] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_name = CAS.Qual_pred_name rewID pred_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates a Maude term into a CASL term
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeTerm2caslTerm :: IdMap -> MAS.Term -> CAS.CASLTERM
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeTerm2caslTerm im (MAS.Var q ty) = CAS.Qual_var q ty' nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ty' = maudeType2caslSort ty im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeTerm2caslTerm im (MAS.Const q ty) = CAS.Application op [] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where name = token2id q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ty' = maudeType2caslSort ty im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes op = CAS.Qual_op_name name op_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeTerm2caslTerm im (MAS.Apply q ts ty) = CAS.Application op tts nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where name = token2id q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes tts = map (maudeTerm2caslTerm im) ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ty' = maudeType2caslSort ty im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes types_tts = getTypes tts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes op_type = CAS.Op_type CAS.Total types_tts ty' nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes op = CAS.Qual_op_name name op_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSymbol2caslSort :: MSym.Symbol -> IdMap -> CAS.SORT
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSymbol2caslSort (MSym.Sort q) _ = token2id q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSymbol2caslSort (MSym.Kind q) im = Map.findWithDefault err q' im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where q' = token2id q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes err = errorId "error translate symbol"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeSymbol2caslSort _ _ = errorId "error translate symbol"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeType2caslSort :: MAS.Type -> IdMap -> CAS.SORT
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeType2caslSort (MAS.TypeSort q) _ = token2id $ getName q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmaudeType2caslSort (MAS.TypeKind q) im = Map.findWithDefault err q' im
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where q' = token2id $ getName q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes err = errorId "error translate type"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | obtains the types of the given terms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetTypes :: [CAS.CASLTERM] -> [Id]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetTypes = mapMaybe getType
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | extracts the type of the temr
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetType :: CAS.CASLTERM -> Maybe Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetType (CAS.Qual_var _ kind _) = Just kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetType (CAS.Application op _ _) = case op of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes CAS.Qual_op_name _ (CAS.Op_type _ _ kind _) _ -> Just kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes _ -> Nothing
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetType _ = Nothing
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the formulas for the rewrite predicates
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredicatesSens = Set.fold rewPredicateSens []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the formulas for the rewrite predicate of the given sort
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredicateSens kind acc = ref : trans : acc
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ref = reflSen kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes trans = transSen kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | creates the reflexivity predicate for the given kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesreflSen :: Id -> Named CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesreflSen kind = makeNamed name $ quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where v = newVar kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_type = CAS.Pred_type [kind, kind] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pn = CAS.Qual_pred_name rewID pred_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Predication pn [v, v] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes name = "rew_refl_" ++ show kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | creates the transitivity predicate for the given kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestransSen :: Id -> Named CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestransSen kind = makeNamed name $ quantifyUniversally form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where v1 = newVarIndex 1 kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v2 = newVarIndex 2 kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v3 = newVarIndex 3 kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pred_type = CAS.Pred_type [kind, kind] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes pn = CAS.Qual_pred_name rewID pred_type nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes prem1 = CAS.Predication pn [v1, v2] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes prem2 = CAS.Predication pn [v2, v3] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes concl = CAS.Predication pn [v1, v3] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes conj_form = CAS.Conjunction [prem1, prem2] nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes form = CAS.Implication conj_form concl True nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes name = "rew_trans_" ++ show kind
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generate the predicates for the rewrites
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredicates :: Set.Set Id -> Map.Map Id (Set.Set CSign.PredType)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generate the predicates for the rewrites of the given sort
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredicate :: Id -> Map.Map Id (Set.Set CSign.PredType)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesrewPredicate kind m = Map.insertWith (Set.union) rewID ar m
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ar = Set.singleton $ CSign.PredType [kind, kind]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | create the predicates that assign sorts to each term
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskindPredicates = Map.foldWithKey kindPredicate Map.empty
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | create the predicates that assign the current sort to the
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- corresponding terms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskindPredicate :: Id -> Id -> Map.Map Id (Set.Set CSign.PredType)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskindPredicate sort kind mis = case sort == (str2id "Universal") of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes False -> let ar = Set.singleton $ CSign.PredType [kind]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | extract the kinds from the map of id's
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskindsFromMap :: IdMap -> Set.Set Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | transform the set of Maude sorts in a set of CASL sorts, including
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- only one sort for each kind.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessortsTranslation :: MSign.SortSet -> MSign.SubsortRel -> Set.Set Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessortsTranslation ss r = sortsTranslationList (Set.toList ss) r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | transform a list representing the Maude sorts in a set of CASL sorts,
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- including only one sort for each kind.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessortsTranslationList :: [MSym.Symbol] -> MSign.SubsortRel -> Set.Set Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessortsTranslationList [] _ = Set.empty
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessortsTranslationList (s : ss) r = Set.insert (sort2id tops) res
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where tops@(top : _) = List.sort $ getTop r s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ss' = deleteRelated ss top r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes res = sortsTranslation ss' r
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | return the maximal elements from the sort relation
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetTop r tok = case succs of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes toks@(_:_) -> foldr ((++) . (getTop r)) [] toks
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | delete from the list of sorts those in the same kind that the parameter
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdeleteRelated :: [MSym.Symbol] -> MSym.Symbol -> MSign.SubsortRel -> MSign.SortSet
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesdeleteRelated ss sym r = foldr (f sym tc) Set.empty ss
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes f = \ sort trC x y -> if MSym.sameKind trC sort x
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | build an Id from a token with the function mkId
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestoken2id :: Token -> Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholestoken2id t = mkId ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where ts = maudeSymbol2validCASLSymbol t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | build an Id from a Maude symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessym2id :: MSym.Symbol -> Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessym2id = token2id . getName
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates an Id from a string
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesstr2id :: String -> Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesstr2id = token2id . mkSimpleId
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | build an Id from a list of sorts, taking the first from the ordered list
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessort2id :: [MSym.Symbol] -> Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessort2id syms = mkId sym''
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where sym = head $ List.sort syms
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes sym' = getName sym
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes sym'' = maudeSymbol2validCASLSymbol sym'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | add universal quantification of all variables in the formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesquantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesquantifyUniversally form = if null var_decl
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else CAS.Quantification CAS.Universal var_decl form nullRange
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where vars = getVars form
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes var_decl = listVarDecl vars
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | traverses a map with sorts as keys and sets of variables as value and creates
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- a list of variable declarations
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeslistVarDecl :: Map.Map Id (Set.Set Token) -> [CAS.VAR_DECL]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeslistVarDecl = Map.foldWithKey f []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where f = \ sort var_set acc -> CAS.Var_decl (Set.toList var_set) sort nullRange : acc
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | removes a quantification from a formula
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnoQuantification :: CAS.CASLFORMULA -> (CAS.CASLFORMULA, [CAS.VAR_DECL])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnoQuantification (CAS.Quantification _ vars form _) = (form, vars)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesnoQuantification form = (form, [])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translate the CASL sorts to symbols
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskinds2syms = Set.map kind2sym
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translate a CASL sort to a CASL symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskind2sym :: Id -> CSign.Symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates the CASL predicates into CASL symbols
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholespreds2syms :: Map.Map Id (Set.Set CSign.PredType) -> Set.Set CSign.Symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates a CASL predicate into a CASL symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholespred2sym :: Id -> Set.Set CSign.PredType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholespred2sym pn spt acc = Set.fold (createSym4id pn) acc spt
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | creates a CASL symbol for a predicate
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateSym4id :: Id -> CSign.PredType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateSym4id pn pt acc = Set.insert sym acc
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where sym = CSign.Symbol pn $ CSign.PredAsItemType pt
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates the CASL operators into CASL symbols
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | translates a CASL operator into a CASL symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesop2sym :: Id -> Set.Set CSign.OpType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesop2sym on sot acc = Set.union set acc
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where set = Set.fold (createSymOp4id on) Set.empty sot
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | creates a CASL symbol for an operator
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateSymOp4id :: Id -> CSign.OpType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholescreateSymOp4id on ot acc = Set.insert sym acc
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where sym = CSign.Symbol on $ CSign.OpAsItemType ot
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | extract the variables from a CASL formula and put them in a map
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- with keys the sort of the variables and value the set of variables
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- in this sort
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars :: CAS.CASLFORMULA -> Map.Map Id (Set.Set Token)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Quantification _ _ f _) = getVars f
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Conjunction fs _) = foldr (Map.unionWith (Set.union) . getVars) Map.empty fs
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Disjunction fs _) = foldr (Map.unionWith (Set.union) . getVars) Map.empty fs
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Implication f1 f2 _ _) = Map.unionWith (Set.union) v1 v2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where v1 = getVars f1
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v2 = getVars f2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Equivalence f1 f2 _) = Map.unionWith (Set.union) v1 v2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where v1 = getVars f1
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v2 = getVars f2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Negation f _) = getVars f
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Predication _ ts _) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Definedness t _) = getVarsTerm t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Existl_equation t1 t2 _) = Map.unionWith (Set.union) v1 v2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where v1 = getVarsTerm t1
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v2 = getVarsTerm t2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Strong_equation t1 t2 _) = Map.unionWith (Set.union) v1 v2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where v1 = getVarsTerm t1
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v2 = getVarsTerm t2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Membership t _ _) = getVarsTerm t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVars (CAS.Mixfix_formula t) = getVarsTerm t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | extract the variables of a CASL term
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm :: CAS.CASLTERM -> Map.Map Id (Set.Set Token)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm (CAS.Qual_var var sort _) = Map.insert sort (Set.singleton var) Map.empty
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm (CAS.Application _ ts _) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm (CAS.Cast t _ _) = getVarsTerm t
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm (CAS.Conditional t1 f t2 _) = Map.unionWith (Set.union) v3 m
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where v1 = getVarsTerm t1
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v2 = getVarsTerm t2
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes v3 = getVars f
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm (CAS.Mixfix_term ts) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm (CAS.Mixfix_parenthesized ts _) =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm (CAS.Mixfix_bracketed ts _) =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm (CAS.Mixfix_braced ts _) =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesgetVarsTerm _ = Map.empty
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | generates the constructor constraint
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesctorSen isFree (sorts, _, ops) = do
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes let sortList = Set.toList sorts
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (CSign.toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops
5aa455d45abacfa675c88d4ff53fbe97c44ce545bnicholes allSyms = opSyms
1223ef8a85a044b5e3a8df29391a66530153aefcbnicholes resType _ (CAS.Op_name _) = False
5aa455d45abacfa675c88d4ff53fbe97c44ce545bnicholes resType s (CAS.Qual_op_name _ t _) = CAS.res_OP_TYPE t == s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes getIndex s = maybe (-1) id $ List.findIndex (== s) sortList
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes addIndices (CAS.Op_name _) =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes error "CASL/StaticAna: Internal error in function addIndices"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes addIndices os@(CAS.Qual_op_name _ t _) =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes (os,map getIndex $ CAS.args_OP_TYPE t)
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes collectOps s =
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes constrs = map collectOps sortList
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes f = CAS.Sort_gen_ax constrs isFree
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes makeNamed ("ga_generated_" ++ showSepList (showString "_") showId sortList "") f
1223ef8a85a044b5e3a8df29391a66530153aefcbnicholes-- | transforms a maude identifier into a valid CASL identifier
5aa455d45abacfa675c88d4ff53fbe97c44ce545bnicholesmaudeSymbol2validCASLSymbol :: Token -> [Token]
5aa455d45abacfa675c88d4ff53fbe97c44ce545bnicholesmaudeSymbol2validCASLSymbol t = splitDoubleUnderscores str ""
1223ef8a85a044b5e3a8df29391a66530153aefcbnicholes where str = ms2vcs $ show t
5aa455d45abacfa675c88d4ff53fbe97c44ce545bnicholes-- | transforms a string coding a Maude identifier into another string
5aa455d45abacfa675c88d4ff53fbe97c44ce545bnicholes-- representing a CASL identifier
5aa455d45abacfa675c88d4ff53fbe97c44ce545bnicholesms2vcs :: String -> String
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesms2vcs s@('k' : 'i' : 'n' : 'd' : '_' : _) = s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesms2vcs s = case Map.member s stringMap of
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes True -> Map.findWithDefault "" s stringMap
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes False -> let f = \ x y -> if Map.member x charMap
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes then (charMap Map.! x) ++ ['\''] ++ y
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else if x == '_'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes then "__" ++ y
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes in foldr f [] s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | map of reserved words
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesstringMap :: Map.Map String String
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes [("true", "maudeTrue"),
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ("false", "maudeFalse"),
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ("not_", "neg__"),
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ("s_", "suc"),
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ("_+_", "__+__"),
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ("_*_", "__*__"),
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ("_<_", "__<__"),
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ("_<=_", "__<=__"),
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ("_>_", "__>__"),
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ("_>=_", "__>=__"),
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes ("_and_", "__maudeAnd__")]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | splits the string into a list of tokens, separating the double
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- underscores from the rest of characters
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessplitDoubleUnderscores :: String -> String -> [Token]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessplitDoubleUnderscores [] acc = if null acc
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else [mkSimpleId acc]
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessplitDoubleUnderscores ('_' : '_' : cs) acc = if null acc
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes then dut : rest
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes else acct : dut : rest
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where acct = mkSimpleId acc
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes dut = mkSimpleId "__"
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes rest = splitDoubleUnderscores cs []
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholessplitDoubleUnderscores (c : cs) acc = splitDoubleUnderscores cs (acc ++ [c])
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-- | error Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeserrorId :: String -> Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeserrorId s = token2id $ mkSimpleId $ "ERROR: " ++ s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskindId :: Id -> Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskindId i = token2id $ mkSimpleId $ "kind_" ++ show i
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskindMapId :: MSign.KindRel -> IdMap
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholeskindMapId kr = Map.fromList krl'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where krl = Map.toList kr
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes krl' = map (\ (x, y) -> (mSym2caslId x, mSym2caslId y)) krl
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmSym2caslId :: MSym.Symbol -> Id
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmSym2caslId (MSym.Sort q) = token2id q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmSym2caslId (MSym.Kind q) = kindId q'
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes where q' = token2id q
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmSym2caslId _ = errorId "error translate symbol"