PreComorphism.hs revision 6d498b6f56ed9f71cced898b6c42fb48f6e60583
af84459fbf938e508fd10b01cb8d699c79083813takashiModule : $Header$
af84459fbf938e508fd10b01cb8d699c79083813takashiDescription : Maude Comorphisms
af84459fbf938e508fd10b01cb8d699c79083813takashiCopyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009
af84459fbf938e508fd10b01cb8d699c79083813takashiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
af84459fbf938e508fd10b01cb8d699c79083813takashiMaintainer : ariesco@fdi.ucm.es
af84459fbf938e508fd10b01cb8d699c79083813takashiStability : experimental
af84459fbf938e508fd10b01cb8d699c79083813takashiPortability : portable
d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenComorphism from Maude to CASL.
af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowenimport qualified Data.List as List
3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport qualified Data.Set as Set
af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Data.Map as Map
af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Maude.Sign as MSign
3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport qualified Maude.Sentence as MSentence
af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Maude.Morphism as MMorphism
af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Maude.AS_Maude as MAS
af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Maude.Symbol as MSym
af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified CASL.Sign as CSign
af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified CASL.Morphism as CMorphism
78f97ce162b66a0dbfd7af4dcd9984f162569b04minfrinimport qualified CASL.AS_Basic_CASL as CAS
af84459fbf938e508fd10b01cb8d699c79083813takashiimport Common.ProofUtils (charMap)
5effc8b39fae5cd169d17f342bfc265705840014rbowenimport qualified Common.Lib.Rel as Rel
5effc8b39fae5cd169d17f342bfc265705840014rbowentype IdMap = Map.Map Id Id
5effc8b39fae5cd169d17f342bfc265705840014rbowentype OpTransTuple = (CSign.OpMap, CSign.OpMap, Set.Set Component)
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates a CASL morphism from a Maude morphism
5effc8b39fae5cd169d17f342bfc265705840014rbowenmapMorphism :: MMorphism.Morphism -> Result (CMorphism.CASLMor)
5effc8b39fae5cd169d17f342bfc265705840014rbowenmapMorphism morph =
5effc8b39fae5cd169d17f342bfc265705840014rbowen mk = kindMapId $ MSign.kindRel src
5effc8b39fae5cd169d17f342bfc265705840014rbowen cs = kindsFromMap mk
5effc8b39fae5cd169d17f342bfc265705840014rbowen smap' = applySortMap2CASLSorts smap cs
5effc8b39fae5cd169d17f342bfc265705840014rbowen omap' = maudeOpMap2CASLOpMap mk omap
5effc8b39fae5cd169d17f342bfc265705840014rbowen pmap = createPredMap mk smap
5effc8b39fae5cd169d17f342bfc265705840014rbowen (src', _) = maude2casl src []
5effc8b39fae5cd169d17f342bfc265705840014rbowen (tgt', _) = maude2casl tgt []
5effc8b39fae5cd169d17f342bfc265705840014rbowen in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | translates the Maude morphism between operators into a CASL morpshim between
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- operators
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map
1c26a593f62800795eddc6cbaf86090e0976e2efrbowenmaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | translates the mapping between two symbols representing operators into
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- a CASL operators map
5effc8b39fae5cd169d17f342bfc265705840014rbowentranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map
5effc8b39fae5cd169d17f342bfc265705840014rbowentranslateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm = copm'
5effc8b39fae5cd169d17f342bfc265705840014rbowen where f = token2id . getName
5effc8b39fae5cd169d17f342bfc265705840014rbowen g = \ x -> Map.findWithDefault (errorId "translate op map entry") (f x) im
5effc8b39fae5cd169d17f342bfc265705840014rbowen cop = (token2id from, ot)
5effc8b39fae5cd169d17f342bfc265705840014rbowen to' = (token2id to, CAS.Total)
5effc8b39fae5cd169d17f342bfc265705840014rbowen copm' = Map.insert cop to' copm
5effc8b39fae5cd169d17f342bfc265705840014rbowentranslateOpMapEntry _ _ _ _ = Map.empty
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates a set of CASL symbol from a Maude Symbol
5effc8b39fae5cd169d17f342bfc265705840014rbowenmapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol
5effc8b39fae5cd169d17f342bfc265705840014rbowen where mk = kindMapId $ MSign.kindRel sg
5effc8b39fae5cd169d17f342bfc265705840014rbowen sym_id = token2id q
5effc8b39fae5cd169d17f342bfc265705840014rbowen kind = Map.findWithDefault (errorId "map symbol") sym_id mk
af84459fbf938e508fd10b01cb8d699c79083813takashi pred_data = CSign.PredType [kind]
af84459fbf938e508fd10b01cb8d699c79083813takashi csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data
af84459fbf938e508fd10b01cb8d699c79083813takashimapSymbol sg (MSym.Operator q ar co) = Set.singleton csym
af84459fbf938e508fd10b01cb8d699c79083813takashi where mk = kindMapId $ MSign.kindRel sg
af84459fbf938e508fd10b01cb8d699c79083813takashi q' = token2id q
af84459fbf938e508fd10b01cb8d699c79083813takashi ar' = map (maudeSort2caslId mk) ar
af84459fbf938e508fd10b01cb8d699c79083813takashi co' = token2id $ getName co
af84459fbf938e508fd10b01cb8d699c79083813takashimapSymbol _ _ = Set.empty
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | returns the sort in CASL of the Maude sort symbol
af84459fbf938e508fd10b01cb8d699c79083813takashimaudeSort2caslId :: IdMap -> MSym.Symbol -> Id
af84459fbf938e508fd10b01cb8d699c79083813takashimaudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id") (token2id $ getName sym) im
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | creates the predicate map for the CASL morphism from the Maude sort map and
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- the map between sorts and kinds
5effc8b39fae5cd169d17f342bfc265705840014rbowencreatePredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map
5effc8b39fae5cd169d17f342bfc265705840014rbowencreatePredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | creates an entry of the predicate map for a single sort
5effc8b39fae5cd169d17f342bfc265705840014rbowencreatePredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map
5effc8b39fae5cd169d17f342bfc265705840014rbowencreatePredMap4sort im from to m = Map.insert key id_to m
5effc8b39fae5cd169d17f342bfc265705840014rbowen where id_from = token2id $ getName from
5effc8b39fae5cd169d17f342bfc265705840014rbowen id_to = token2id $ getName to
5effc8b39fae5cd169d17f342bfc265705840014rbowen kind = Map.findWithDefault (errorId "predicate for sort") id_from im
5effc8b39fae5cd169d17f342bfc265705840014rbowen key = (id_from, CSign.PredType [kind])
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | computes the sort morphism of CASL from the sort morphism in Maude and the set
5effc8b39fae5cd169d17f342bfc265705840014rbowenapplySortMap2CASLSorts :: MMorphism.SortMap -> Set.Set Id -> CMorphism.Sort_map
5effc8b39fae5cd169d17f342bfc265705840014rbowenapplySortMap2CASLSorts sm = Set.fold (applySortMap2CASLSort sm) Map.empty
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | computes the morphism for a single kind
5effc8b39fae5cd169d17f342bfc265705840014rbowenapplySortMap2CASLSort :: MMorphism.SortMap -> Id -> CMorphism.Sort_map -> CMorphism.Sort_map
5effc8b39fae5cd169d17f342bfc265705840014rbowenapplySortMap2CASLSort sm sort csm = new_csm
5effc8b39fae5cd169d17f342bfc265705840014rbowen where toks = getTokens sort
5effc8b39fae5cd169d17f342bfc265705840014rbowen new_toks = map (rename sm) toks
5effc8b39fae5cd169d17f342bfc265705840014rbowen new_sort = mkId new_toks
5effc8b39fae5cd169d17f342bfc265705840014rbowen new_csm = if new_sort == sort
5effc8b39fae5cd169d17f342bfc265705840014rbowen else Map.insert sort new_sort csm
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | renames the sorts in a given kind
5effc8b39fae5cd169d17f342bfc265705840014rbowenrename :: MMorphism.SortMap -> Token -> Token
5effc8b39fae5cd169d17f342bfc265705840014rbowenrename sm tok = new_tok
5effc8b39fae5cd169d17f342bfc265705840014rbowen where sym = MSym.Sort tok
5effc8b39fae5cd169d17f342bfc265705840014rbowen sym' = if Map.member sym sm
5effc8b39fae5cd169d17f342bfc265705840014rbowen then fromJust $ Map.lookup sym sm
5effc8b39fae5cd169d17f342bfc265705840014rbowen new_tok = getName sym'
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | translates a Maude sentence into a CASL formula
5effc8b39fae5cd169d17f342bfc265705840014rbowenmapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA
5effc8b39fae5cd169d17f342bfc265705840014rbowenmapSentence sg sen@(MSentence.Equation eq) = case any MAS.owise ats of
5effc8b39fae5cd169d17f342bfc265705840014rbowen False -> return $ sentence $ noOwiseSen2Formula mk named
5effc8b39fae5cd169d17f342bfc265705840014rbowen True -> let
5effc8b39fae5cd169d17f342bfc265705840014rbowen sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg
5effc8b39fae5cd169d17f342bfc265705840014rbowen (no_owise_sens, _, _) = splitOwiseEqs sg_sens
5effc8b39fae5cd169d17f342bfc265705840014rbowen no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
5effc8b39fae5cd169d17f342bfc265705840014rbowen trans = sentence $ owiseSen2Formula mk no_owise_forms named
5effc8b39fae5cd169d17f342bfc265705840014rbowen in return trans
5effc8b39fae5cd169d17f342bfc265705840014rbowen where mk = kindMapId $ MSign.kindRel sg
5effc8b39fae5cd169d17f342bfc265705840014rbowen MAS.Eq _ _ _ ats = eq
5effc8b39fae5cd169d17f342bfc265705840014rbowen named = makeNamed "" sen
5effc8b39fae5cd169d17f342bfc265705840014rbowenmapSentence sg sen@(MSentence.Membership mb) = return $ sentence form
5effc8b39fae5cd169d17f342bfc265705840014rbowen where mk = kindMapId $ MSign.kindRel sg
5effc8b39fae5cd169d17f342bfc265705840014rbowen MAS.Mb _ _ _ _ = mb
5effc8b39fae5cd169d17f342bfc265705840014rbowen named = makeNamed "" sen
5effc8b39fae5cd169d17f342bfc265705840014rbowen form = mb_rl2formula mk named
5effc8b39fae5cd169d17f342bfc265705840014rbowenmapSentence sg sen@(MSentence.Rule rl) = return $ sentence form
5effc8b39fae5cd169d17f342bfc265705840014rbowen where mk = kindMapId $ MSign.kindRel sg
5effc8b39fae5cd169d17f342bfc265705840014rbowen MAS.Rl _ _ _ _ = rl
5effc8b39fae5cd169d17f342bfc265705840014rbowen named = makeNamed "" sen
5effc8b39fae5cd169d17f342bfc265705840014rbowen form = mb_rl2formula mk named
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | applies maude2casl to compute the CASL signature and sentences from
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- the Maude ones, and wraps them into a Result datatype
5effc8b39fae5cd169d17f342bfc265705840014rbowenmapTheory (sg, nsens) = return $ maude2casl sg nsens
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | computes new signature and sentences of CASL associated to the
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- given Maude signature and sentences
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaude2casl :: MSign.Sign -> [Named MSentence.Sentence]
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaude2casl msign nsens = (csign { CSign.sortSet = cs,
5effc8b39fae5cd169d17f342bfc265705840014rbowen CSign.declaredSymbols = syms }, new_sens)
5effc8b39fae5cd169d17f342bfc265705840014rbowen where csign = CSign.emptySign ()
5effc8b39fae5cd169d17f342bfc265705840014rbowen ss' = Set.map sym2id ss
5effc8b39fae5cd169d17f342bfc265705840014rbowen mk = kindMapId $ MSign.kindRel msign
5effc8b39fae5cd169d17f342bfc265705840014rbowen sbs' = maudeSbs2caslSbs sbs mk
5effc8b39fae5cd169d17f342bfc265705840014rbowen cs = Set.union ss' $ kindsFromMap mk
5effc8b39fae5cd169d17f342bfc265705840014rbowen preds = rewPredicates cs
5effc8b39fae5cd169d17f342bfc265705840014rbowen rs = rewPredicatesSens cs
63befe0983261d711e62457b380e24ecc3b7b79etrawick ops = deleteUniversal $ MSign.ops msign
63befe0983261d711e62457b380e24ecc3b7b79etrawick ksyms = kinds2syms cs
63befe0983261d711e62457b380e24ecc3b7b79etrawick (cops, assoc_ops, _) = translateOps mk ops -- (cops, assoc_ops, comps)
63befe0983261d711e62457b380e24ecc3b7b79etrawick ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]
63befe0983261d711e62457b380e24ecc3b7b79etrawick cops' = universalOps cs cops $ booleanImported ops
63befe0983261d711e62457b380e24ecc3b7b79etrawick rs' = rewPredicatesCongSens cops'
5effc8b39fae5cd169d17f342bfc265705840014rbowen pred_forms = loadLibraries (MSign.sorts msign) ops
5effc8b39fae5cd169d17f342bfc265705840014rbowen ops_syms = ops2symbols cops'
5effc8b39fae5cd169d17f342bfc265705840014rbowen (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens
5effc8b39fae5cd169d17f342bfc265705840014rbowen no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
5effc8b39fae5cd169d17f342bfc265705840014rbowen owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens
5effc8b39fae5cd169d17f342bfc265705840014rbowen mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens
5effc8b39fae5cd169d17f342bfc265705840014rbowen preds_syms = preds2syms preds
5effc8b39fae5cd169d17f342bfc265705840014rbowen syms = Set.union ksyms $ Set.union ops_syms preds_syms
5effc8b39fae5cd169d17f342bfc265705840014rbowen new_sens = concat [rs, rs', no_owise_forms, owise_forms,
5effc8b39fae5cd169d17f342bfc265705840014rbowen mb_rl_forms, ctor_sen, pred_forms]
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | translates the Maude subsorts into CASL subsorts, and adds the subsorts
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- for the kinds
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeSbs2caslSbs :: MSign.SubsortRel -> IdMap -> Rel.Rel CAS.SORT
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeSbs2caslSbs sbs im = Rel.fromDistinctMap m4
5effc8b39fae5cd169d17f342bfc265705840014rbowen l1 = [] -- map maudeSb2caslSb l
5effc8b39fae5cd169d17f342bfc265705840014rbowen l2 = idList2Subsorts $ Map.toList im
5effc8b39fae5cd169d17f342bfc265705840014rbowen l3 = map subsorts2Ids l
5effc8b39fae5cd169d17f342bfc265705840014rbowen m4 = Map.unionWith Set.union m1 $ Map.unionWith Set.union m2 m3
5effc8b39fae5cd169d17f342bfc265705840014rbowenidList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]
5effc8b39fae5cd169d17f342bfc265705840014rbowenidList2Subsorts [] = []
5effc8b39fae5cd169d17f342bfc265705840014rbowenidList2Subsorts ((id1, id2) : il) = t1 : idList2Subsorts il
5effc8b39fae5cd169d17f342bfc265705840014rbowen where t1 = (id1, Set.singleton id2)
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeSb2caslSb :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeSb2caslSb (sym, st) = (sortSym2id sym, Set.map (kindId . sortSym2id) st)
5effc8b39fae5cd169d17f342bfc265705840014rbowensubsorts2Ids :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)
5effc8b39fae5cd169d17f342bfc265705840014rbowensubsorts2Ids (sym, st) = (sortSym2id sym, Set.map sortSym2id st)
af84459fbf938e508fd10b01cb8d699c79083813takashisortSym2id :: MSym.Symbol -> Id
af84459fbf938e508fd10b01cb8d699c79083813takashisortSym2id (MSym.Sort q) = token2id q
af84459fbf938e508fd10b01cb8d699c79083813takashisortSym2id _ = token2id $ mkSimpleId $ "error_translation"
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates the sentences to state that the rew predicates are a congruence
5effc8b39fae5cd169d17f342bfc265705840014rbowenrewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]
af84459fbf938e508fd10b01cb8d699c79083813takashirewPredicatesCongSens = Map.foldWithKey rewPredCongSet []
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates the sentences to state that the rew predicates are a congruence
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- for the operator types in the set
af84459fbf938e508fd10b01cb8d699c79083813takashirewPredCongSet :: Id -> Set.Set CSign.OpType -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
af84459fbf938e508fd10b01cb8d699c79083813takashirewPredCongSet idn ots fs = fs ++ fs'
af84459fbf938e508fd10b01cb8d699c79083813takashi where fs' = Set.fold (rewPredCong idn) [] ots
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates the sentences to state that the rew predicates are a congruence
af84459fbf938e508fd10b01cb8d699c79083813takashi-- for a single operator
af84459fbf938e508fd10b01cb8d699c79083813takashirewPredCong :: Id -> CSign.OpType -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
af84459fbf938e508fd10b01cb8d699c79083813takashirewPredCong op ot fs = case args of
af84459fbf938e508fd10b01cb8d699c79083813takashi _ -> nq_form : fs
af84459fbf938e508fd10b01cb8d699c79083813takashi where args = CSign.opArgs ot
5effc8b39fae5cd169d17f342bfc265705840014rbowen vars1 = rewPredCongPremise 0 args
5effc8b39fae5cd169d17f342bfc265705840014rbowen vars2 = rewPredCongPremise (length args) args
5effc8b39fae5cd169d17f342bfc265705840014rbowen res_pred_type = CAS.Pred_type [res, res] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen pn = CAS.Qual_pred_name rewID res_pred_type nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen name = "rew_cong_" ++ show op
5effc8b39fae5cd169d17f342bfc265705840014rbowen prems = rewPredsCong args vars1 vars2
5effc8b39fae5cd169d17f342bfc265705840014rbowen prems_conj = createConjForm prems
5effc8b39fae5cd169d17f342bfc265705840014rbowen os = CAS.Qual_op_name op (CSign.toOP_TYPE ot) nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen conc_term1 = CAS.Application os vars1 nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen conc_term2 = CAS.Application os vars2 nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen conc_form = CAS.Predication pn [conc_term1, conc_term2] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen form = createImpForm prems_conj conc_form
5effc8b39fae5cd169d17f342bfc265705840014rbowen nq_form = makeNamed name $ quantifyUniversally form
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates a list of variables of the given sorts
5effc8b39fae5cd169d17f342bfc265705840014rbowenrewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]
af84459fbf938e508fd10b01cb8d699c79083813takashirewPredCongPremise n (s : ss) = newVarIndex n s : rewPredCongPremise (n + 1) ss
af84459fbf938e508fd10b01cb8d699c79083813takashirewPredCongPremise _ [] = []
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates a list of rew predicates with the given variables
5effc8b39fae5cd169d17f342bfc265705840014rbowenrewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]
af84459fbf938e508fd10b01cb8d699c79083813takashirewPredsCong (s : ss) (t : ts) (t' : ts') = form : forms
5effc8b39fae5cd169d17f342bfc265705840014rbowen where pred_type = CAS.Pred_type [s, s] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen pn = CAS.Qual_pred_name rewID pred_type nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen form = CAS.Predication pn [t, t'] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen forms = rewPredsCong ss ts ts'
5effc8b39fae5cd169d17f342bfc265705840014rbowenrewPredsCong _ _ _ = []
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | load the CASL libraries for the Maude built-in operators
af84459fbf938e508fd10b01cb8d699c79083813takashiloadLibraries :: MSign.SortSet -> MSign.OpMap -> [Named CAS.CASLFORMULA]
af84459fbf938e508fd10b01cb8d699c79083813takashiloadLibraries ss om = case natImported ss om of
af84459fbf938e508fd10b01cb8d699c79083813takashi False -> []
af84459fbf938e508fd10b01cb8d699c79083813takashi True -> loadNaturalNatSens
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | loads the sentences associated to the natural numbers
af84459fbf938e508fd10b01cb8d699c79083813takashiloadNaturalNatSens :: [Named CAS.CASLFORMULA]
5effc8b39fae5cd169d17f342bfc265705840014rbowenloadNaturalNatSens =
5effc8b39fae5cd169d17f342bfc265705840014rbowen let lib = head $ unsafePerformIO $ readLib "Maude/MaudeNumbers.casl"
5effc8b39fae5cd169d17f342bfc265705840014rbowen in case lib of
5effc8b39fae5cd169d17f342bfc265705840014rbowen G_theory lid _ _ thSens _ -> let sens = toNamedList thSens
5effc8b39fae5cd169d17f342bfc265705840014rbowen sens' <- coerceSens lid CASL "" sens
5effc8b39fae5cd169d17f342bfc265705840014rbowen filter (not . ctorCons) sens'
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | checks if a sentence is an constructor sentence
5effc8b39fae5cd169d17f342bfc265705840014rbowenctorCons :: Named CAS.CASLFORMULA -> Bool
5effc8b39fae5cd169d17f342bfc265705840014rbowenctorCons f = case sentence f of
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | checks if the boolean values are imported
5effc8b39fae5cd169d17f342bfc265705840014rbowenbooleanImported :: MSign.OpMap -> Bool
5effc8b39fae5cd169d17f342bfc265705840014rbowenbooleanImported = Map.member (mkSimpleId "if_then_else_fi")
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | checks if the natural numbers are imported
5effc8b39fae5cd169d17f342bfc265705840014rbowennatImported ss om = b1 && b2 && b3
5effc8b39fae5cd169d17f342bfc265705840014rbowen where b1 = Set.member (MSym.Sort $ mkSimpleId "Nat") ss
5effc8b39fae5cd169d17f342bfc265705840014rbowen b2 = Map.member (mkSimpleId "s_") om
5effc8b39fae5cd169d17f342bfc265705840014rbowen b3 = case b2 of
5effc8b39fae5cd169d17f342bfc265705840014rbowen False -> True
5effc8b39fae5cd169d17f342bfc265705840014rbowen True -> specialZeroSet $ om Map.! (mkSimpleId "s_")
5effc8b39fae5cd169d17f342bfc265705840014rbowenspecialZeroSet :: MSign.OpDeclSet -> Bool
5effc8b39fae5cd169d17f342bfc265705840014rbowenspecialZeroSet = Set.fold specialZero False
5effc8b39fae5cd169d17f342bfc265705840014rbowenspecialZero :: MSign.OpDecl -> Bool -> Bool
5effc8b39fae5cd169d17f342bfc265705840014rbowenspecialZero (_, ats) b = b' || b
5effc8b39fae5cd169d17f342bfc265705840014rbowen where b' = isSpecial ats
5effc8b39fae5cd169d17f342bfc265705840014rbowenisSpecial :: [MAS.Attr] -> Bool
5effc8b39fae5cd169d17f342bfc265705840014rbowenisSpecial [] = False
5effc8b39fae5cd169d17f342bfc265705840014rbowenisSpecial ((MAS.Special _) : _) = True
5effc8b39fae5cd169d17f342bfc265705840014rbowenisSpecial (_ : ats) = isSpecial ats
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | delete the universal operators from Maude specifications, that will be
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- substituted for one operator for each sort in the specification
5effc8b39fae5cd169d17f342bfc265705840014rbowendeleteUniversal om = om5
5effc8b39fae5cd169d17f342bfc265705840014rbowen where om1 = Map.delete (mkSimpleId "if_then_else_fi") om
5effc8b39fae5cd169d17f342bfc265705840014rbowen om2 = Map.delete (mkSimpleId "_==_") om1
af84459fbf938e508fd10b01cb8d699c79083813takashi om3 = Map.delete (mkSimpleId "_=/=_") om2
af84459fbf938e508fd10b01cb8d699c79083813takashi om4 = Map.delete (mkSimpleId "upTerm") om3
af84459fbf938e508fd10b01cb8d699c79083813takashi om5 = Map.delete (mkSimpleId "downTerm") om4
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates the universal operators for all the sorts in the module
5effc8b39fae5cd169d17f342bfc265705840014rbowenuniversalOps :: Set.Set Id -> CSign.OpMap -> Bool -> CSign.OpMap
5effc8b39fae5cd169d17f342bfc265705840014rbowenuniversalOps kinds om True = Set.fold universalOpKind om kinds
5effc8b39fae5cd169d17f342bfc265705840014rbowenuniversalOps _ om False = om
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates the universal operators for a concrete module
af84459fbf938e508fd10b01cb8d699c79083813takashiuniversalOpKind kind om = om3
af84459fbf938e508fd10b01cb8d699c79083813takashi where if_id = str2id "if_then_else_fi"
af84459fbf938e508fd10b01cb8d699c79083813takashi double_eq_id = str2id "_==_"
af84459fbf938e508fd10b01cb8d699c79083813takashi neg_double_eq_id = str2id "_=/=_"
af84459fbf938e508fd10b01cb8d699c79083813takashi bool_id = str2id "Bool"
af84459fbf938e508fd10b01cb8d699c79083813takashi if_opt = Set.singleton $ CSign.OpType CAS.Total [bool_id, kind, kind] kind
af84459fbf938e508fd10b01cb8d699c79083813takashi eq_opt = Set.singleton $ CSign.OpType CAS.Total [kind, kind] bool_id
af84459fbf938e508fd10b01cb8d699c79083813takashi om2 = Map.insertWith Set.union double_eq_id eq_opt om1
af84459fbf938e508fd10b01cb8d699c79083813takashi om3 = Map.insertWith Set.union neg_double_eq_id eq_opt om2
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates the formulas for the universal operators
af84459fbf938e508fd10b01cb8d699c79083813takashiuniversalSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
11495c9f0bd33e51a25b4d532beadfbcf9b944a3nilgununiversalSens = Set.fold universalSensKind []
11495c9f0bd33e51a25b4d532beadfbcf9b944a3nilgun-- | generates the formulas for the universal operators for the given sort
11495c9f0bd33e51a25b4d532beadfbcf9b944a3nilgununiversalSensKind :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
11495c9f0bd33e51a25b4d532beadfbcf9b944a3nilgununiversalSensKind kind acc = concat [iss, eqs, neqs, acc]
11495c9f0bd33e51a25b4d532beadfbcf9b944a3nilgun where iss = ifSens kind
11495c9f0bd33e51a25b4d532beadfbcf9b944a3nilgun eqs = equalitySens kind
af84459fbf938e508fd10b01cb8d699c79083813takashi neqs = nonEqualitySens kind
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates the formulas for the if statement
11495c9f0bd33e51a25b4d532beadfbcf9b944a3nilgunifSens :: Id -> [Named CAS.CASLFORMULA]
11495c9f0bd33e51a25b4d532beadfbcf9b944a3nilgunifSens kind = [form'', neg_form'']
af84459fbf938e508fd10b01cb8d699c79083813takashi where v1 = newVarIndex 1 kind
af84459fbf938e508fd10b01cb8d699c79083813takashi v2 = newVarIndex 2 kind
af84459fbf938e508fd10b01cb8d699c79083813takashi bk = str2id "Bool"
af84459fbf938e508fd10b01cb8d699c79083813takashi bv = newVarIndex 2 bk
af84459fbf938e508fd10b01cb8d699c79083813takashi true_id = CAS.Qual_op_name (str2id "true") true_type nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi true_term = CAS.Application true_id [] nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi if_type = CAS.Op_type CAS.Total [bk, kind, kind] kind nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi if_name = str2id "if_then_else_fi"
af84459fbf938e508fd10b01cb8d699c79083813takashi if_id = CAS.Qual_op_name if_name if_type nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi if_term = CAS.Application if_id [bv, v1, v2] nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi prem = CAS.Strong_equation bv true_term nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi concl = CAS.Strong_equation if_term v1 nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Implication prem concl True nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi form' = quantifyUniversally form
af84459fbf938e508fd10b01cb8d699c79083813takashi neg_prem = CAS.Negation prem nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi neg_concl = CAS.Strong_equation if_term v2 nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi neg_form = CAS.Implication neg_prem neg_concl True nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi neg_form' = quantifyUniversally neg_form
af84459fbf938e508fd10b01cb8d699c79083813takashi name1 = show kind ++ "_if_true"
af84459fbf938e508fd10b01cb8d699c79083813takashi name2 = show kind ++ "_if_false"
af84459fbf938e508fd10b01cb8d699c79083813takashi form'' = makeNamed name1 form'
af84459fbf938e508fd10b01cb8d699c79083813takashi neg_form'' = makeNamed name2 neg_form'
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates the formulas for the equality
5effc8b39fae5cd169d17f342bfc265705840014rbowenequalitySens :: Id -> [Named CAS.CASLFORMULA]
5effc8b39fae5cd169d17f342bfc265705840014rbowenequalitySens kind = [form'', comp_form'']
5effc8b39fae5cd169d17f342bfc265705840014rbowen where v1 = newVarIndex 1 kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen v2 = newVarIndex 2 kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen bk = str2id "Bool"
af84459fbf938e508fd10b01cb8d699c79083813takashi true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen true_term = CAS.Application true_id [] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen false_term = CAS.Application false_id [] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen prem = CAS.Strong_equation v1 v2 nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen double_eq_name = str2id "_==_"
5effc8b39fae5cd169d17f342bfc265705840014rbowen double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen concl = CAS.Strong_equation double_eq_term true_term nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen form = CAS.Implication prem concl True nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen form' = quantifyUniversally form
5effc8b39fae5cd169d17f342bfc265705840014rbowen neg_prem = CAS.Negation prem nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen new_concl = CAS.Strong_equation double_eq_term false_term nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen comp_form = CAS.Implication neg_prem new_concl True nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen comp_form' = quantifyUniversally comp_form
5effc8b39fae5cd169d17f342bfc265705840014rbowen name1 = show kind ++ "_==_true"
af84459fbf938e508fd10b01cb8d699c79083813takashi name2 = show kind ++ "_==_false"
af84459fbf938e508fd10b01cb8d699c79083813takashi form'' = makeNamed name1 form'
af84459fbf938e508fd10b01cb8d699c79083813takashi comp_form'' = makeNamed name2 comp_form'
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates the formulas for the inequality
5effc8b39fae5cd169d17f342bfc265705840014rbowennonEqualitySens :: Id -> [Named CAS.CASLFORMULA]
5effc8b39fae5cd169d17f342bfc265705840014rbowennonEqualitySens kind = [form'', comp_form'']
5effc8b39fae5cd169d17f342bfc265705840014rbowen where v1 = newVarIndex 1 kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen v2 = newVarIndex 2 kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen bk = str2id "Bool"
5effc8b39fae5cd169d17f342bfc265705840014rbowen true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen true_term = CAS.Application true_id [] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen false_term = CAS.Application false_id [] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen prem = CAS.Strong_equation v1 v2 nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi double_eq_name = str2id "_==_"
af84459fbf938e508fd10b01cb8d699c79083813takashi double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi concl = CAS.Strong_equation double_eq_term false_term nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Implication prem concl True nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi form' = quantifyUniversally form
af84459fbf938e508fd10b01cb8d699c79083813takashi neg_prem = CAS.Negation prem nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi new_concl = CAS.Strong_equation double_eq_term true_term nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi comp_form = CAS.Implication neg_prem new_concl True nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi comp_form' = quantifyUniversally comp_form
5effc8b39fae5cd169d17f342bfc265705840014rbowen name1 = show kind ++ "_=/=_false"
5effc8b39fae5cd169d17f342bfc265705840014rbowen name2 = show kind ++ "_=/=_true"
5effc8b39fae5cd169d17f342bfc265705840014rbowen form'' = makeNamed name1 form'
5effc8b39fae5cd169d17f342bfc265705840014rbowen comp_form'' = makeNamed name2 comp_form'
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | translates the Maude operator map into a tuple of CASL operators, CASL
af84459fbf938e508fd10b01cb8d699c79083813takashi-- associative operators, membership induced from each Maude operator,
af84459fbf938e508fd10b01cb8d699c79083813takashi-- and the set of sorts with the ctor attribute
5effc8b39fae5cd169d17f342bfc265705840014rbowentranslateOps :: IdMap -> MSign.OpMap -> OpTransTuple
af84459fbf938e508fd10b01cb8d699c79083813takashitranslateOps im = Map.fold (translateOpDeclSet im) (Map.empty, Map.empty, Set.empty)
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | translates an operator declaration set into a tern as described above
5effc8b39fae5cd169d17f342bfc265705840014rbowentranslateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
5effc8b39fae5cd169d17f342bfc265705840014rbowentranslateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | given an operator declaration updates the accumulator with the translation
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- to CASL operator, checking if the operator has the assoc attribute to insert
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- it in the map of associative operators, generating the membership predicate
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh-- induced by the operator declaration, and checking if it has the ctor attribute
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh-- to introduce the operator in the generators sentence
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohtranslateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohtranslateOpDecl im (syms, ats) (ops, assoc_ops, cs) = case tl of
5effc8b39fae5cd169d17f342bfc265705840014rbowen [] -> (ops', assoc_ops', cs')
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh _ -> translateOpDecl im (syms', ats) (ops', assoc_ops', cs')
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh where sym = head $ Set.toList syms
5effc8b39fae5cd169d17f342bfc265705840014rbowen tl = tail $ Set.toList syms
5effc8b39fae5cd169d17f342bfc265705840014rbowen (cop_id, ot, _) = fromJust $ maudeSym2CASLOp im sym
5effc8b39fae5cd169d17f342bfc265705840014rbowen cop_type = Set.singleton ot -- Set.union (Set.singleton ot) (Set.singleton ot')
5effc8b39fae5cd169d17f342bfc265705840014rbowen ops' = Map.insertWith (Set.union) cop_id cop_type ops
5effc8b39fae5cd169d17f342bfc265705840014rbowen assoc_ops' = if any MAS.assoc ats
5effc8b39fae5cd169d17f342bfc265705840014rbowen then Map.insertWith (Set.union) cop_id cop_type assoc_ops
af84459fbf938e508fd10b01cb8d699c79083813takashi else assoc_ops
af84459fbf938e508fd10b01cb8d699c79083813takashi cs' = if any MAS.ctor ats
af84459fbf938e508fd10b01cb8d699c79083813takashi then Set.insert (Component cop_id ot) cs
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | translates a Maude operator symbol into a pair with the id of the operator
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- and its CASL type
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeSym2CASLOp :: IdMap -> MSym.Symbol -> Maybe (Id, CSign.OpType, CSign.OpType)
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot, ot')
5effc8b39fae5cd169d17f342bfc265705840014rbowen where f = token2id . getName
5effc8b39fae5cd169d17f342bfc265705840014rbowen g = \ x -> maudeSymbol2caslSort x im -- \ x -> Map.findWithDefault (errorId "Maude_sym2CASL_sym") (f x) im
af84459fbf938e508fd10b01cb8d699c79083813takashimaudeSym2CASLOp _ _ = Nothing
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | creates a conjuctive formula distinguishing the size of the list
5effc8b39fae5cd169d17f342bfc265705840014rbowencreateConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA
5effc8b39fae5cd169d17f342bfc265705840014rbowencreateConjForm [] = CAS.True_atom nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowencreateConjForm [a] = a
5effc8b39fae5cd169d17f342bfc265705840014rbowencreateConjForm fs = CAS.Conjunction fs nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | creates a implication formula distinguishing the size of the premises
5effc8b39fae5cd169d17f342bfc265705840014rbowencreateImpForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA -> CAS.CASLFORMULA
af84459fbf938e508fd10b01cb8d699c79083813takashicreateImpForm (CAS.True_atom _) form = form
5effc8b39fae5cd169d17f342bfc265705840014rbowencreateImpForm form1 form2 = CAS.Implication form1 form2 True nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates the predicates asserting the "true" sort of the operator if all
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- the arguments have the correct sort
5effc8b39fae5cd169d17f342bfc265705840014rbowenops2predPremises :: IdMap -> [MSym.Symbol] -> Int -> ([CAS.CASLTERM], [CAS.CASLFORMULA])
5effc8b39fae5cd169d17f342bfc265705840014rbowenops2predPremises im (MSym.Sort s : ss) i = (var : terms, form : forms)
5effc8b39fae5cd169d17f342bfc265705840014rbowen where s' = token2id s
5effc8b39fae5cd169d17f342bfc265705840014rbowen kind = Map.findWithDefault (errorId "mb of op as predicate") s' im
5effc8b39fae5cd169d17f342bfc265705840014rbowen pred_type = CAS.Pred_type [kind] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen pred_name = CAS.Qual_pred_name s' pred_type nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen var = newVarIndex i kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen form = CAS.Predication pred_name [var] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen (terms, forms) = ops2predPremises im ss (i + 1)
5effc8b39fae5cd169d17f342bfc265705840014rbowenops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)
5effc8b39fae5cd169d17f342bfc265705840014rbowen where k' = token2id k
5effc8b39fae5cd169d17f342bfc265705840014rbowen kind = Map.findWithDefault (errorId "mb of op as predicate") k' im
5effc8b39fae5cd169d17f342bfc265705840014rbowen var = newVarIndex i kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen (terms, forms) = ops2predPremises im ss (i + 1)
5effc8b39fae5cd169d17f342bfc265705840014rbowenops2predPremises _ _ _ = ([], [])
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | traverses the Maude sentences, returning a pair of list of sentences.
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- The first list in the pair are the equations without the attribute "owise",
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- while the second one are the equations with this attribute
5effc8b39fae5cd169d17f342bfc265705840014rbowensplitOwiseEqs :: [Named MSentence.Sentence] ->
5effc8b39fae5cd169d17f342bfc265705840014rbowen ([Named MSentence.Sentence], [Named MSentence.Sentence], [Named MSentence.Sentence])
5effc8b39fae5cd169d17f342bfc265705840014rbowensplitOwiseEqs [] = ([], [], [])
5effc8b39fae5cd169d17f342bfc265705840014rbowensplitOwiseEqs (s : ss) = res
5effc8b39fae5cd169d17f342bfc265705840014rbowen where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss
5effc8b39fae5cd169d17f342bfc265705840014rbowen sen = sentence s
5effc8b39fae5cd169d17f342bfc265705840014rbowen res = case sen of
5effc8b39fae5cd169d17f342bfc265705840014rbowen MSentence.Equation (MAS.Eq _ _ _ ats) -> case any MAS.owise ats of
5effc8b39fae5cd169d17f342bfc265705840014rbowen True -> (no_owise_sens, s : owise_sens, mbs_rls)
5effc8b39fae5cd169d17f342bfc265705840014rbowen False -> (s : no_owise_sens, owise_sens, mbs_rls)
5effc8b39fae5cd169d17f342bfc265705840014rbowen _ -> (no_owise_sens, owise_sens, s : mbs_rls)
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | translates a Maude equation defined without the "owise" attribute into
af84459fbf938e508fd10b01cb8d699c79083813takashi-- a CASL formula
af84459fbf938e508fd10b01cb8d699c79083813takashinoOwiseSen2Formula :: IdMap -> Named MSentence.Sentence
af84459fbf938e508fd10b01cb8d699c79083813takashinoOwiseSen2Formula im s = s'
af84459fbf938e508fd10b01cb8d699c79083813takashi where MSentence.Equation eq = sentence s
5effc8b39fae5cd169d17f342bfc265705840014rbowen sen' = noOwiseEq2Formula im eq
5effc8b39fae5cd169d17f342bfc265705840014rbowen s' = s { sentence = sen' }
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | translates a Maude equation defined with the "owise" attribute into
af84459fbf938e508fd10b01cb8d699c79083813takashi-- a CASL formula
5effc8b39fae5cd169d17f342bfc265705840014rbowenowiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]
5effc8b39fae5cd169d17f342bfc265705840014rbowenowiseSen2Formula im owise_forms s = s'
5effc8b39fae5cd169d17f342bfc265705840014rbowen where MSentence.Equation eq = sentence s
5effc8b39fae5cd169d17f342bfc265705840014rbowen sen' = owiseEq2Formula im owise_forms eq
5effc8b39fae5cd169d17f342bfc265705840014rbowen s' = s { sentence = sen' }
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | translates a Maude membership or rule into a CASL formula
af84459fbf938e508fd10b01cb8d699c79083813takashimb_rl2formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
5effc8b39fae5cd169d17f342bfc265705840014rbowenmb_rl2formula im s = case sen of
5effc8b39fae5cd169d17f342bfc265705840014rbowen mb' = mb2formula im mb
5effc8b39fae5cd169d17f342bfc265705840014rbowen in s { sentence = mb' }
5effc8b39fae5cd169d17f342bfc265705840014rbowen rl' = rl2formula im rl
5effc8b39fae5cd169d17f342bfc265705840014rbowen in s { sentence = rl' }
5effc8b39fae5cd169d17f342bfc265705840014rbowen _ -> makeNamed "" $ CAS.False_atom nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen where sen = sentence s
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates a new variable qualified with the given number
5effc8b39fae5cd169d17f342bfc265705840014rbowennewVarIndex :: Int -> Id -> CAS.CASLTERM
5effc8b39fae5cd169d17f342bfc265705840014rbowennewVarIndex i sort = CAS.Qual_var var sort nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen where var = mkSimpleId $ "V" ++ show i
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates a new variable
5effc8b39fae5cd169d17f342bfc265705840014rbowennewVar :: Id -> CAS.CASLTERM
5effc8b39fae5cd169d17f342bfc265705840014rbowennewVar sort = CAS.Qual_var var sort nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen where var = mkSimpleId "V"
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | Id for the rew predicate
af84459fbf938e508fd10b01cb8d699c79083813takashirewID = token2id $ mkSimpleId "rew"
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | translates a Maude equation without the "owise" attribute into a CASL formula
af84459fbf938e508fd10b01cb8d699c79083813takashinoOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA
5effc8b39fae5cd169d17f342bfc265705840014rbowennoOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally form
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ct = maudeTerm2caslTerm im t
5effc8b39fae5cd169d17f342bfc265705840014rbowen ct' = maudeTerm2caslTerm im t'
af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Strong_equation ct ct' nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashinoOwiseEq2Formula im (MAS.Eq t t' conds@(_:_) _) = quantifyUniversally form
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ct = maudeTerm2caslTerm im t
5effc8b39fae5cd169d17f342bfc265705840014rbowen ct' = maudeTerm2caslTerm im t'
5effc8b39fae5cd169d17f342bfc265705840014rbowen conds_form = conds2formula im conds
5effc8b39fae5cd169d17f342bfc265705840014rbowen concl_form = CAS.Strong_equation ct ct' nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen form = createImpForm conds_form concl_form
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | transforms a Maude equation defined with the otherwise attribute into
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- a CASL formula
5effc8b39fae5cd169d17f342bfc265705840014rbowenowiseEq2Formula :: IdMap -> [Named CAS.CASLFORMULA] -> MAS.Equation
5effc8b39fae5cd169d17f342bfc265705840014rbowenowiseEq2Formula im no_owise_form eq = form
5effc8b39fae5cd169d17f342bfc265705840014rbowen where (eq_form, vars) = noQuantification $ noOwiseEq2Formula im eq
5effc8b39fae5cd169d17f342bfc265705840014rbowen (op, ts, _) = fromJust $ getLeftApp eq_form
5effc8b39fae5cd169d17f342bfc265705840014rbowen ex_form = existencialNegationOtherEqs op ts no_owise_form
5effc8b39fae5cd169d17f342bfc265705840014rbowen imp_form = createImpForm ex_form eq_form
5effc8b39fae5cd169d17f342bfc265705840014rbowen form = CAS.Quantification CAS.Universal vars imp_form nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates a conjunction of negation of existencial quantifiers
5effc8b39fae5cd169d17f342bfc265705840014rbowenexistencialNegationOtherEqs :: CAS.OP_SYMB -> [CAS.CASLTERM] ->
5effc8b39fae5cd169d17f342bfc265705840014rbowenexistencialNegationOtherEqs op ts forms = form
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ex_forms = foldr ((++) . existencialNegationOtherEq op ts) [] forms
af84459fbf938e508fd10b01cb8d699c79083813takashi form = if length ex_forms > 1
5effc8b39fae5cd169d17f342bfc265705840014rbowen then CAS.Conjunction ex_forms nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi else head ex_forms
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | given a formula, if it refers to the same operator indicated by the parameters
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- the predicate creates a list with the negation of the existence of variables that
af84459fbf938e508fd10b01cb8d699c79083813takashi-- match the pattern described in the formula. In other case it returns an empty list
5effc8b39fae5cd169d17f342bfc265705840014rbowenexistencialNegationOtherEq :: CAS.OP_SYMB -> [CAS.CASLTERM] ->
5effc8b39fae5cd169d17f342bfc265705840014rbowenexistencialNegationOtherEq req_op terms form = case ok of
5effc8b39fae5cd169d17f342bfc265705840014rbowen False -> []
af84459fbf938e508fd10b01cb8d699c79083813takashi True -> let
5effc8b39fae5cd169d17f342bfc265705840014rbowen (_, ts, conds) = fromJust tpl
af84459fbf938e508fd10b01cb8d699c79083813takashi ts' = qualifyExVarsTerms ts
5effc8b39fae5cd169d17f342bfc265705840014rbowen conds' = qualifyExVarsForms conds
5effc8b39fae5cd169d17f342bfc265705840014rbowen prems = (createEqs ts' terms) ++ conds'
5effc8b39fae5cd169d17f342bfc265705840014rbowen conj_form = CAS.Conjunction prems nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi ex_form = if vars' /= []
5effc8b39fae5cd169d17f342bfc265705840014rbowen then CAS.Quantification CAS.Existential vars' conj_form nullRange
9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf else conj_form
af84459fbf938e508fd10b01cb8d699c79083813takashi neg_form = CAS.Negation ex_form nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi in [neg_form]
5effc8b39fae5cd169d17f342bfc265705840014rbowen where (inner_form, vars) = noQuantification $ sentence form
5effc8b39fae5cd169d17f342bfc265705840014rbowen vars' = qualifyExVars vars
5effc8b39fae5cd169d17f342bfc265705840014rbowen tpl = getLeftApp inner_form
5effc8b39fae5cd169d17f342bfc265705840014rbowen ok = case tpl of
5effc8b39fae5cd169d17f342bfc265705840014rbowen Nothing -> False
5effc8b39fae5cd169d17f342bfc265705840014rbowen Just _ -> let (op, ts, _) = fromJust tpl
5effc8b39fae5cd169d17f342bfc265705840014rbowen in req_op == op && length terms == length ts
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | qualifies the variables in a list of formulas with the suffix "_ex" to
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- distinguish them from the variables already bound
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsForms :: [CAS.CASLFORMULA] -> [CAS.CASLFORMULA]
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsForms = map qualifyExVarsForm
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | qualifies the variables in a formula with the suffix "_ex" to distinguish them
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- from the variables already bound
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsForm (CAS.Strong_equation t t' r) = CAS.Strong_equation qt qt' r
5effc8b39fae5cd169d17f342bfc265705840014rbowen where qt = qualifyExVarsTerm t
5effc8b39fae5cd169d17f342bfc265705840014rbowen qt' = qualifyExVarsTerm t'
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsForm (CAS.Predication op ts r) = CAS.Predication op ts' r
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ts' = qualifyExVarsTerms ts
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsForm f = f
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | qualifies the variables in a list of terms with the suffix "_ex" to
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- distinguish them from the variables already bound
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerms :: [CAS.CASLTERM] -> [CAS.CASLTERM]
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerms = map qualifyExVarsTerm
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | qualifies the variables in a term with the suffix "_ex" to distinguish them
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- from the variables already bound
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerm (CAS.Qual_var var sort r) = CAS.Qual_var (qualifyExVarAux var) sort r
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerm (CAS.Application op ts r) = CAS.Application op ts' r
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ts' = map qualifyExVarsTerm ts
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerm (CAS.Sorted_term t s r) = CAS.Sorted_term (qualifyExVarsTerm t) s r
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerm (CAS.Cast t s r) = CAS.Cast (qualifyExVarsTerm t) s r
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerm (CAS.Conditional t1 f t2 r) = CAS.Conditional t1' f t2' r
5effc8b39fae5cd169d17f342bfc265705840014rbowen where t1' = qualifyExVarsTerm t1
5effc8b39fae5cd169d17f342bfc265705840014rbowen t2' = qualifyExVarsTerm t2
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerm (CAS.Mixfix_term ts) = CAS.Mixfix_term ts'
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ts' = map qualifyExVarsTerm ts
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerm (CAS.Mixfix_parenthesized ts r) = CAS.Mixfix_parenthesized ts' r
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh where ts' = map qualifyExVarsTerm ts
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerm (CAS.Mixfix_bracketed ts r) = CAS.Mixfix_bracketed ts' r
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh where ts' = map qualifyExVarsTerm ts
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedoohqualifyExVarsTerm (CAS.Mixfix_braced ts r) = CAS.Mixfix_braced ts' r
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ts' = map qualifyExVarsTerm ts
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarsTerm t = t
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | qualifies a list of variables with the suffix "_ex" to
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- distinguish them from the variables already bound
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVars = map qualifyExVar
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | qualifies a variable with the suffix "_ex" to distinguish it from
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- the variables already bound
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVar (CAS.Var_decl vars s r) = CAS.Var_decl vars' s r
5effc8b39fae5cd169d17f342bfc265705840014rbowen where vars' = map qualifyExVarAux vars
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | qualifies a token with the suffix "_ex"
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarAux :: Token -> Token
5effc8b39fae5cd169d17f342bfc265705840014rbowenqualifyExVarAux var = mkSimpleId $ show var ++ "_ex"
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | creates a list of strong equalities from two lists of terms
5effc8b39fae5cd169d17f342bfc265705840014rbowencreateEqs :: [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]
5effc8b39fae5cd169d17f342bfc265705840014rbowencreateEqs (t1 : ts1) (t2 : ts2) = CAS.Strong_equation t1 t2 nullRange : ls
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ls = createEqs ts1 ts2
5effc8b39fae5cd169d17f342bfc265705840014rbowencreateEqs _ _ = []
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | extracts the operator at the top and the arguments of the lefthand side
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- in a strong equation
5effc8b39fae5cd169d17f342bfc265705840014rbowengetLeftApp :: CAS.CASLFORMULA -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM], [CAS.CASLFORMULA])
af84459fbf938e508fd10b01cb8d699c79083813takashigetLeftApp (CAS.Strong_equation term _ _) = case getLeftAppTerm term of
af84459fbf938e508fd10b01cb8d699c79083813takashi Nothing -> Nothing
af84459fbf938e508fd10b01cb8d699c79083813takashi Just (op, ts) -> Just (op, ts, [])
af84459fbf938e508fd10b01cb8d699c79083813takashigetLeftApp (CAS.Implication prem concl _ _) = case getLeftApp concl of
af84459fbf938e508fd10b01cb8d699c79083813takashi Nothing -> Nothing
af84459fbf938e508fd10b01cb8d699c79083813takashi Just (op, ts, _) -> Just (op, ts, conds)
af84459fbf938e508fd10b01cb8d699c79083813takashi where conds = getPremisesImplication prem
af84459fbf938e508fd10b01cb8d699c79083813takashigetLeftApp _ = Nothing
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | extracts the operator at the top and the arguments of the lefthand side
af84459fbf938e508fd10b01cb8d699c79083813takashi-- in an application term
af84459fbf938e508fd10b01cb8d699c79083813takashigetLeftAppTerm :: CAS.CASLTERM -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM])
af84459fbf938e508fd10b01cb8d699c79083813takashigetLeftAppTerm (CAS.Application op ts _) = Just (op, ts)
af84459fbf938e508fd10b01cb8d699c79083813takashigetLeftAppTerm _ = Nothing
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | extracts the formulas of the given premise, distinguishing whether it is
3c13a815670b54d1c17bf02954f7d2b066cde95cnd-- a conjunction or not
af84459fbf938e508fd10b01cb8d699c79083813takashigetPremisesImplication :: CAS.CASLFORMULA -> [CAS.CASLFORMULA]
af84459fbf938e508fd10b01cb8d699c79083813takashigetPremisesImplication (CAS.Conjunction forms _) = forms
af84459fbf938e508fd10b01cb8d699c79083813takashigetPremisesImplication form = [form]
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | translate a Maude membership into a CASL formula
af84459fbf938e508fd10b01cb8d699c79083813takashimb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA
af84459fbf938e508fd10b01cb8d699c79083813takashimb2formula im (MAS.Mb t s [] _) = quantifyUniversally form
af84459fbf938e508fd10b01cb8d699c79083813takashi where ct = maudeTerm2caslTerm im t
af84459fbf938e508fd10b01cb8d699c79083813takashi s' = token2id $ getName s
af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Membership ct s' nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashimb2formula im (MAS.Mb t s conds@(_ : _) _) = quantifyUniversally form
af84459fbf938e508fd10b01cb8d699c79083813takashi where ct = maudeTerm2caslTerm im t
af84459fbf938e508fd10b01cb8d699c79083813takashi s' = token2id $ getName s
af84459fbf938e508fd10b01cb8d699c79083813takashi conds_form = conds2formula im conds
5effc8b39fae5cd169d17f342bfc265705840014rbowen concl_form = CAS.Membership ct s' nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Implication conds_form concl_form True nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | translate a Maude rule into a CASL formula
af84459fbf938e508fd10b01cb8d699c79083813takashirl2formula im (MAS.Rl t t' [] _) = quantifyUniversally form
af84459fbf938e508fd10b01cb8d699c79083813takashi where ty = token2id $ getName $ MAS.getTermType t
af84459fbf938e508fd10b01cb8d699c79083813takashi kind = Map.findWithDefault (errorId "rl to formula") ty im
af84459fbf938e508fd10b01cb8d699c79083813takashi pred_type = CAS.Pred_type [kind, kind] nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi pred_name = CAS.Qual_pred_name rewID pred_type nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi ct = maudeTerm2caslTerm im t
af84459fbf938e508fd10b01cb8d699c79083813takashi ct' = maudeTerm2caslTerm im t'
af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Predication pred_name [ct, ct'] nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashirl2formula im (MAS.Rl t t' conds@(_:_) _) = quantifyUniversally form
af84459fbf938e508fd10b01cb8d699c79083813takashi where ty = token2id $ getName $ MAS.getTermType t
af84459fbf938e508fd10b01cb8d699c79083813takashi kind = Map.findWithDefault (errorId "rl to formula") ty im
af84459fbf938e508fd10b01cb8d699c79083813takashi pred_type = CAS.Pred_type [kind, kind] nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi pred_name = CAS.Qual_pred_name rewID pred_type nullRange
3c13a815670b54d1c17bf02954f7d2b066cde95cnd ct = maudeTerm2caslTerm im t
af84459fbf938e508fd10b01cb8d699c79083813takashi ct' = maudeTerm2caslTerm im t'
af84459fbf938e508fd10b01cb8d699c79083813takashi conds_form = conds2formula im conds
af84459fbf938e508fd10b01cb8d699c79083813takashi concl_form = CAS.Predication pred_name [ct, ct'] nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Implication conds_form concl_form True nullRange
3c13a815670b54d1c17bf02954f7d2b066cde95cnd-- | translate a conjunction of Maude conditions to a CASL formula
3c13a815670b54d1c17bf02954f7d2b066cde95cndconds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA
af84459fbf938e508fd10b01cb8d699c79083813takashiconds2formula im conds = CAS.Conjunction forms nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen where forms = map (cond2formula im) conds
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | translate a single Maude condition to a CASL formula
af84459fbf938e508fd10b01cb8d699c79083813takashicond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA
3c13a815670b54d1c17bf02954f7d2b066cde95cndcond2formula im (MAS.EqCond t t') = CAS.Strong_equation ct ct' nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi where ct = maudeTerm2caslTerm im t
af84459fbf938e508fd10b01cb8d699c79083813takashi ct' = maudeTerm2caslTerm im t'
5effc8b39fae5cd169d17f342bfc265705840014rbowencond2formula im (MAS.MatchCond t t') = CAS.Strong_equation ct ct' nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi where ct = maudeTerm2caslTerm im t
af84459fbf938e508fd10b01cb8d699c79083813takashi ct' = maudeTerm2caslTerm im t'
0cf3cdbaa1dad11cbf1ce32e48f1b4ec88cf779fnilguncond2formula im (MAS.MbCond t s) = CAS.Membership ct s' nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi where ct = maudeTerm2caslTerm im t
3c13a815670b54d1c17bf02954f7d2b066cde95cnd s' = token2id $ getName s
3c13a815670b54d1c17bf02954f7d2b066cde95cndcond2formula im (MAS.RwCond t t') = CAS.Predication pred_name [ct, ct'] nullRange
3c13a815670b54d1c17bf02954f7d2b066cde95cnd where ct = maudeTerm2caslTerm im t
af84459fbf938e508fd10b01cb8d699c79083813takashi ct' = maudeTerm2caslTerm im t'
af84459fbf938e508fd10b01cb8d699c79083813takashi ty = token2id $ getName $ MAS.getTermType t
af84459fbf938e508fd10b01cb8d699c79083813takashi kind = Map.findWithDefault (errorId "rw cond to formula") ty im
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh pred_type = CAS.Pred_type [kind, kind] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen pred_name = CAS.Qual_pred_name rewID pred_type nullRange
888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh-- | translates a Maude term into a CASL term
af84459fbf938e508fd10b01cb8d699c79083813takashimaudeTerm2caslTerm :: IdMap -> MAS.Term -> CAS.CASLTERM
af84459fbf938e508fd10b01cb8d699c79083813takashimaudeTerm2caslTerm im (MAS.Var q ty) = CAS.Qual_var q ty' nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi where ty' = maudeType2caslSort ty im
3c13a815670b54d1c17bf02954f7d2b066cde95cndmaudeTerm2caslTerm im (MAS.Const q ty) = CAS.Application op [] nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi where name = token2id q
af84459fbf938e508fd10b01cb8d699c79083813takashi ty' = maudeType2caslSort ty im
0cf3cdbaa1dad11cbf1ce32e48f1b4ec88cf779fnilgun op = CAS.Qual_op_name name op_type nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashimaudeTerm2caslTerm im (MAS.Apply q ts ty) = CAS.Application op tts nullRange
3c13a815670b54d1c17bf02954f7d2b066cde95cnd where name = token2id q
af84459fbf938e508fd10b01cb8d699c79083813takashi tts = map (maudeTerm2caslTerm im) ts
af84459fbf938e508fd10b01cb8d699c79083813takashi ty' = maudeType2caslSort ty im
af84459fbf938e508fd10b01cb8d699c79083813takashi types_tts = getTypes tts
5effc8b39fae5cd169d17f342bfc265705840014rbowen op_type = CAS.Op_type CAS.Total types_tts ty' nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi op = CAS.Qual_op_name name op_type nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashimaudeSymbol2caslSort :: MSym.Symbol -> IdMap -> CAS.SORT
af84459fbf938e508fd10b01cb8d699c79083813takashimaudeSymbol2caslSort (MSym.Sort q) _ = token2id q
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeSymbol2caslSort (MSym.Kind q) im = Map.findWithDefault err q' im
af84459fbf938e508fd10b01cb8d699c79083813takashi where q' = token2id q
af84459fbf938e508fd10b01cb8d699c79083813takashi err = errorId "error translate symbol"
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeSymbol2caslSort _ _ = errorId "error translate symbol"
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeType2caslSort (MAS.TypeSort q) _ = token2id $ getName q
5effc8b39fae5cd169d17f342bfc265705840014rbowenmaudeType2caslSort (MAS.TypeKind q) im = Map.findWithDefault err q' im
5effc8b39fae5cd169d17f342bfc265705840014rbowen where q' = token2id $ getName q
5effc8b39fae5cd169d17f342bfc265705840014rbowen err = errorId "error translate type"
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | obtains the types of the given terms
af84459fbf938e508fd10b01cb8d699c79083813takashigetTypes :: [CAS.CASLTERM] -> [Id]
5effc8b39fae5cd169d17f342bfc265705840014rbowengetTypes = mapMaybe getType
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | extracts the type of the temr
5effc8b39fae5cd169d17f342bfc265705840014rbowengetType :: CAS.CASLTERM -> Maybe Id
5effc8b39fae5cd169d17f342bfc265705840014rbowengetType (CAS.Qual_var _ kind _) = Just kind
5effc8b39fae5cd169d17f342bfc265705840014rbowengetType (CAS.Application op _ _) = case op of
5effc8b39fae5cd169d17f342bfc265705840014rbowen CAS.Qual_op_name _ (CAS.Op_type _ _ kind _) _ -> Just kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen _ -> Nothing
5effc8b39fae5cd169d17f342bfc265705840014rbowengetType _ = Nothing
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates the formulas for the rewrite predicates
5effc8b39fae5cd169d17f342bfc265705840014rbowenrewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
5effc8b39fae5cd169d17f342bfc265705840014rbowenrewPredicatesSens = Set.fold rewPredicateSens []
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates the formulas for the rewrite predicate of the given sort
5effc8b39fae5cd169d17f342bfc265705840014rbowenrewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
5effc8b39fae5cd169d17f342bfc265705840014rbowenrewPredicateSens kind acc = ref : trans : acc
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ref = reflSen kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen trans = transSen kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | creates the reflexivity predicate for the given kind
5effc8b39fae5cd169d17f342bfc265705840014rbowenreflSen :: Id -> Named CAS.CASLFORMULA
5effc8b39fae5cd169d17f342bfc265705840014rbowenreflSen kind = makeNamed name $ quantifyUniversally form
af84459fbf938e508fd10b01cb8d699c79083813takashi where v = newVar kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen pred_type = CAS.Pred_type [kind, kind] nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi pn = CAS.Qual_pred_name rewID pred_type nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen form = CAS.Predication pn [v, v] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen name = "rew_refl_" ++ show kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | creates the transitivity predicate for the given kind
5effc8b39fae5cd169d17f342bfc265705840014rbowentransSen :: Id -> Named CAS.CASLFORMULA
5effc8b39fae5cd169d17f342bfc265705840014rbowentransSen kind = makeNamed name $ quantifyUniversally form
5effc8b39fae5cd169d17f342bfc265705840014rbowen where v1 = newVarIndex 1 kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen v2 = newVarIndex 2 kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen v3 = newVarIndex 3 kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen pred_type = CAS.Pred_type [kind, kind] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen pn = CAS.Qual_pred_name rewID pred_type nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen prem1 = CAS.Predication pn [v1, v2] nullRange
af84459fbf938e508fd10b01cb8d699c79083813takashi prem2 = CAS.Predication pn [v2, v3] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen concl = CAS.Predication pn [v1, v3] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen conj_form = CAS.Conjunction [prem1, prem2] nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen form = CAS.Implication conj_form concl True nullRange
5effc8b39fae5cd169d17f342bfc265705840014rbowen name = "rew_trans_" ++ show kind
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generate the predicates for the rewrites
af84459fbf938e508fd10b01cb8d699c79083813takashirewPredicates :: Set.Set Id -> Map.Map Id (Set.Set CSign.PredType)
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generate the predicates for the rewrites of the given sort
5effc8b39fae5cd169d17f342bfc265705840014rbowenrewPredicate :: Id -> Map.Map Id (Set.Set CSign.PredType)
5effc8b39fae5cd169d17f342bfc265705840014rbowenrewPredicate kind m = Map.insertWith (Set.union) rewID ar m
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ar = Set.singleton $ CSign.PredType [kind, kind]
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | create the predicates that assign sorts to each term
af84459fbf938e508fd10b01cb8d699c79083813takashikindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)
af84459fbf938e508fd10b01cb8d699c79083813takashikindPredicates = Map.foldWithKey kindPredicate Map.empty
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | create the predicates that assign the current sort to the
af84459fbf938e508fd10b01cb8d699c79083813takashi-- corresponding terms
5effc8b39fae5cd169d17f342bfc265705840014rbowenkindPredicate :: Id -> Id -> Map.Map Id (Set.Set CSign.PredType)
5effc8b39fae5cd169d17f342bfc265705840014rbowenkindPredicate sort kind mis = case sort == (str2id "Universal") of
5effc8b39fae5cd169d17f342bfc265705840014rbowen True -> mis
5effc8b39fae5cd169d17f342bfc265705840014rbowen False -> let ar = Set.singleton $ CSign.PredType [kind]
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | extract the kinds from the map of id's
5effc8b39fae5cd169d17f342bfc265705840014rbowenkindsFromMap :: IdMap -> Set.Set Id
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | transform the set of Maude sorts in a set of CASL sorts, including
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- only one sort for each kind.
5effc8b39fae5cd169d17f342bfc265705840014rbowensortsTranslation :: MSign.SortSet -> MSign.SubsortRel -> Set.Set Id
af84459fbf938e508fd10b01cb8d699c79083813takashisortsTranslation ss r = sortsTranslationList (Set.toList ss) r
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | transform a list representing the Maude sorts in a set of CASL sorts,
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- including only one sort for each kind.
5effc8b39fae5cd169d17f342bfc265705840014rbowensortsTranslationList :: [MSym.Symbol] -> MSign.SubsortRel -> Set.Set Id
5effc8b39fae5cd169d17f342bfc265705840014rbowensortsTranslationList [] _ = Set.empty
5effc8b39fae5cd169d17f342bfc265705840014rbowensortsTranslationList (s : ss) r = Set.insert (sort2id tops) res
5effc8b39fae5cd169d17f342bfc265705840014rbowen where tops@(top : _) = List.sort $ getTop r s
af84459fbf938e508fd10b01cb8d699c79083813takashi ss' = deleteRelated ss top r
5effc8b39fae5cd169d17f342bfc265705840014rbowen res = sortsTranslation ss' r
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | return the maximal elements from the sort relation
5effc8b39fae5cd169d17f342bfc265705840014rbowengetTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]
5effc8b39fae5cd169d17f342bfc265705840014rbowengetTop r tok = case succs of
5effc8b39fae5cd169d17f342bfc265705840014rbowen [] -> [tok]
5effc8b39fae5cd169d17f342bfc265705840014rbowen toks@(_:_) -> foldr ((++) . (getTop r)) [] toks
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | delete from the list of sorts those in the same kind that the parameter
5effc8b39fae5cd169d17f342bfc265705840014rbowendeleteRelated :: [MSym.Symbol] -> MSym.Symbol -> MSign.SubsortRel -> MSign.SortSet
5effc8b39fae5cd169d17f342bfc265705840014rbowendeleteRelated ss sym r = foldr (f sym tc) Set.empty ss
5effc8b39fae5cd169d17f342bfc265705840014rbowen f = \ sort trC x y -> if MSym.sameKind trC sort x
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | build an Id from a token with the function mkId
5effc8b39fae5cd169d17f342bfc265705840014rbowentoken2id :: Token -> Id
5effc8b39fae5cd169d17f342bfc265705840014rbowentoken2id t = mkId ts
5effc8b39fae5cd169d17f342bfc265705840014rbowen where ts = maudeSymbol2validCASLSymbol t
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | build an Id from a Maude symbol
5effc8b39fae5cd169d17f342bfc265705840014rbowensym2id :: MSym.Symbol -> Id
5effc8b39fae5cd169d17f342bfc265705840014rbowensym2id = token2id . getName
5effc8b39fae5cd169d17f342bfc265705840014rbowen-- | generates an Id from a string
af84459fbf938e508fd10b01cb8d699c79083813takashistr2id :: String -> Id
af84459fbf938e508fd10b01cb8d699c79083813takashistr2id = token2id . mkSimpleId
af84459fbf938e508fd10b01cb8d699c79083813takashi-- | build an Id from a list of sorts, taking the first from the ordered list
af84459fbf938e508fd10b01cb8d699c79083813takashisort2id :: [MSym.Symbol] -> Id
f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungsort2id syms = mkId sym''
727872d18412fc021f03969b8641810d8896820bhumbedooh where sym = head $ List.sort syms
0d0ba3a410038e179b695446bb149cce6264e0abnd sym' = getName sym
727872d18412fc021f03969b8641810d8896820bhumbedooh sym'' = maudeSymbol2validCASLSymbol sym'
0d0ba3a410038e179b695446bb149cce6264e0abnd-- | add universal quantification of all variables in the formula
cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedoohquantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA
727872d18412fc021f03969b8641810d8896820bhumbedoohquantifyUniversally form = if null var_decl
0d0ba3a410038e179b695446bb149cce6264e0abnd else CAS.Quantification CAS.Universal var_decl form nullRange
0d0ba3a410038e179b695446bb149cce6264e0abnd where vars = getVars form
ac082aefa89416cbdc9a1836eaf3bed9698201c8humbedooh var_decl = listVarDecl vars
0d0ba3a410038e179b695446bb149cce6264e0abnd-- | traverses a map with sorts as keys and sets of variables as value and creates
0d0ba3a410038e179b695446bb149cce6264e0abnd-- a list of variable declarations
727872d18412fc021f03969b8641810d8896820bhumbedoohlistVarDecl :: Map.Map Id (Set.Set Token) -> [CAS.VAR_DECL]
0d0ba3a410038e179b695446bb149cce6264e0abndlistVarDecl = Map.foldWithKey f []
0d0ba3a410038e179b695446bb149cce6264e0abnd where f = \ sort var_set acc -> CAS.Var_decl (Set.toList var_set) sort nullRange : acc
07dc96d063d49299da433f84b5c5681da9bbdf68rbowen-- | removes a quantification from a formula
af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowennoQuantification :: CAS.CASLFORMULA -> (CAS.CASLFORMULA, [CAS.VAR_DECL])
0d0ba3a410038e179b695446bb149cce6264e0abndnoQuantification (CAS.Quantification _ vars form _) = (form, vars)
7fec19672a491661b2fe4b29f685bc7f4efa64d4ndnoQuantification form = (form, [])
7fec19672a491661b2fe4b29f685bc7f4efa64d4nd-- | translate the CASL sorts to symbols
kinds2syms = Set.map kind2sym
kind2sym :: Id -> CSign.Symbol
pred2sym pn spt acc = Set.fold (createSym4id pn) acc spt
createSym4id pn pt acc = Set.insert sym acc
op2sym on sot acc = Set.union set acc
createSymOp4id on ot acc = Set.insert sym acc
getVars (CAS.Quantification _ _ f _) = getVars f
getVars (CAS.Negation f _) = getVars f
getVars (CAS.Definedness t _) = getVarsTerm t
getVars (CAS.Membership t _ _) = getVarsTerm t
getVars (CAS.Mixfix_formula t) = getVarsTerm t
getVars _ = Map.empty
getVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t
getVarsTerm (CAS.Cast t _ _) = getVarsTerm t
getVarsTerm (CAS.Mixfix_parenthesized ts _) =
getVarsTerm (CAS.Mixfix_bracketed ts _) =
getVarsTerm (CAS.Mixfix_braced ts _) =
getVarsTerm _ = Map.empty
ctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA
let sortList = Set.toList sorts
opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide
resType _ (CAS.Op_name _) = False
getIndex s = maybe (-1) id $ List.findIndex (== s) sortList
addIndices (CAS.Op_name _) =
error "CASL/StaticAna: Internal error in function addIndices"
addIndices os@(CAS.Qual_op_name _ t _) =
(os,map getIndex $ CAS.args_OP_TYPE t)
CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s
f = CAS.Sort_gen_ax constrs isFree
ms2vcs s = case Map.member s stringMap of
True -> Map.findWithDefault "" s stringMap
False -> let f = \ x y -> if Map.member x charMap
stringMap :: Map.Map String String
stringMap = Map.fromList
kindMapId :: MSign.KindRel -> IdMap
kindMapId kr = Map.fromList krl'
where krl = Map.toList kr
mSym2caslId :: MSym.Symbol -> Id
mSym2caslId (MSym.Sort q) = token2id q
mSym2caslId (MSym.Kind q) = kindId q'