e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder{- |

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederModule : $Header$

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederDescription : Maude Comorphisms

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederCopyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederMaintainer : ariesco@fdi.ucm.es

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederStability : experimental

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederPortability : portable

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederComorphism from Maude to CASL.

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-}

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maedermodule Maude.PreComorphism where

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport Data.Maybe

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified Data.List as List

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified Data.Set as Set

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified Data.Map as Map

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified Maude.Sign as MSign

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified Maude.Sentence as MSentence

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified Maude.Morphism as MMorphism

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified Maude.AS_Maude as MAS

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified Maude.Symbol as MSym

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport Maude.Meta.HasName

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified CASL.Sign as CSign

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified CASL.Morphism as CMorphism

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified CASL.AS_Basic_CASL as CAS

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport CASL.StaticAna

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport CASL.Logic_CASL

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport Common.Id

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport Common.Result

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport Common.AS_Annotation

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport Common.ProofUtils (charMap)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport qualified Common.Lib.Rel as Rel

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport Comorphisms.GetPreludeLib (readLib)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport System.IO.Unsafe

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport Static.GTheory

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport Logic.Prover

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederimport Logic.Coerce

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maedertype IdMap = Map.Map Id Id

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maedertype OpTransTuple = (CSign.OpMap, CSign.OpMap, Set.Set Component)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | generates a CASL morphism from a Maude morphism

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermapMorphism :: MMorphism.Morphism -> Result (CMorphism.CASLMor)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermapMorphism morph =

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder let

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder src = MMorphism.source morph

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder tgt = MMorphism.target morph

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder mk = kindMapId $ MSign.kindRel src

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder mk' = kindMapId $ MSign.kindRel tgt

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder smap = MMorphism.sortMap morph

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder omap = MMorphism.opMap morph

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder smap' = applySortMap2CASLSorts smap mk mk'

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder omap' = maudeOpMap2CASLOpMap mk omap

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder pmap = createPredMap mk smap

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder (src', _) = maude2casl src []

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder (tgt', _) = maude2casl tgt []

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | translates the Maude morphism between operators into a CASL morpshim between

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- operators

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | translates the mapping between two symbols representing operators into

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- a CASL operators map

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedertranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder -> CMorphism.Op_map

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedertranslateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm = copm'

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder where f = token2id . getName

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder g = \ x -> Map.findWithDefault (errorId "translate op map entry") (f x) im

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder ot = CSign.OpType CAS.Total (map g ar) (g co)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder cop = (token2id from, ot)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder to' = (token2id to, CAS.Total)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder copm' = Map.insert cop to' copm

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedertranslateOpMapEntry _ _ _ _ = Map.empty

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | generates a set of CASL symbol from a Maude Symbol

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermapSymbol sg (MSym.Sort q) = Set.singleton csym

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder where mk = kindMapId $ MSign.kindRel sg

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder sym_id = token2id q

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder kind = Map.findWithDefault (errorId "map symbol") sym_id mk

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder pred_data = CSign.PredType [kind]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaedermapSymbol sg (MSym.Operator q ar co) = Set.singleton csym

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where mk = kindMapId $ MSign.kindRel sg

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder q' = token2id q

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder ar' = map (maudeSort2caslId mk) ar

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder co' = token2id $ getName co

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder op_data = CSign.OpType CAS.Total ar' co'

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder csym = CSign.Symbol q' $ CSign.OpAsItemType op_data

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaedermapSymbol _ _ = Set.empty

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | returns the sort in CASL of the Maude sort symbol

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermaudeSort2caslId :: IdMap -> MSym.Symbol -> Id

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermaudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id") (token2id $ getName sym) im

adda0e6252b14215228e4071b347c49b808894f8Christian Maeder

adda0e6252b14215228e4071b347c49b808894f8Christian Maeder-- | creates the predicate map for the CASL morphism from the Maude sort map and

adda0e6252b14215228e4071b347c49b808894f8Christian Maeder-- the map between sorts and kinds

adda0e6252b14215228e4071b347c49b808894f8Christian MaedercreatePredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map

adda0e6252b14215228e4071b347c49b808894f8Christian MaedercreatePredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty

adda0e6252b14215228e4071b347c49b808894f8Christian Maeder

adda0e6252b14215228e4071b347c49b808894f8Christian Maeder-- | creates an entry of the predicate map for a single sort

adda0e6252b14215228e4071b347c49b808894f8Christian MaedercreatePredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder -> CMorphism.Pred_map

adda0e6252b14215228e4071b347c49b808894f8Christian MaedercreatePredMap4sort im from to m = Map.insert key id_to m

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder where id_from = token2id $ getName from

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder id_to = token2id $ getName to

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder kind = Map.findWithDefault (errorId "predicate for sort") id_from im

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder key = (id_from, CSign.PredType [kind])

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | computes the sort morphism of CASL from the sort morphism in Maude and the set

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- of kinds

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederapplySortMap2CASLSorts :: MMorphism.SortMap -> IdMap -> IdMap -> CMorphism.Sort_map

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederapplySortMap2CASLSorts sm im im' = Map.fromList sml'

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder where sml = Map.toList sm

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder sml' = foldr (applySortMap2CASLSort im im') [] sml

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | computes the morphism for a single sort pair

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederapplySortMap2CASLSort :: IdMap -> IdMap -> (MSym.Symbol, MSym.Symbol) -> [(Id, Id)]

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder -> [(Id, Id)]

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederapplySortMap2CASLSort im im' (s1, s2) l = l'

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder where p1 = (mSym2caslId s1, mSym2caslId s2)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder f = \ x y -> Map.findWithDefault (errorId $ "err" ++ (show $ mSym2caslId x)) (mSym2caslId x) y

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder p2 = (f s1 im, f s2 im')

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder l' = if s1 == s2

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder then p1 : l

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder else p1 : p2 : l

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | renames the sorts in a given kind

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederrename :: MMorphism.SortMap -> Token -> Token

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maederrename sm tok = new_tok

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder where sym = MSym.Sort tok

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder sym' = if Map.member sym sm

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder then fromJust $ Map.lookup sym sm

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder else sym

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder new_tok = getName sym'

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | translates a Maude sentence into a CASL formula

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaedermapSentence sg sen@(MSentence.Equation eq) = case any MAS.owise ats of

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder False -> return $ sentence $ noOwiseSen2Formula mk named

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder True -> let

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder (no_owise_sens, _, _) = splitOwiseEqs sg_sens

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder trans = sentence $ owiseSen2Formula mk no_owise_forms named

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder in return trans

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where mk = kindMapId $ MSign.kindRel sg

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder MAS.Eq _ _ _ ats = eq

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder named = makeNamed "" sen

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaedermapSentence sg sen@(MSentence.Membership mb) = return $ sentence form

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder where mk = kindMapId $ MSign.kindRel sg

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder MAS.Mb _ _ _ _ = mb

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder named = makeNamed "" sen

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder form = mb_rl2formula mk named

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaedermapSentence sg sen@(MSentence.Rule rl) = return $ sentence form

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where mk = kindMapId $ MSign.kindRel sg

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder MAS.Rl _ _ _ _ = rl

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder named = makeNamed "" sen

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder form = mb_rl2formula mk named

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | applies maude2casl to compute the CASL signature and sentences from

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- the Maude ones, and wraps them into a Result datatype

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermapTheory :: (MSign.Sign, [Named MSentence.Sentence])

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder -> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermapTheory (sg, nsens) = return $ maude2casl sg nsens

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | computes new signature and sentences of CASL associated to the

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- given Maude signature and sentences

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maedermaude2casl :: MSign.Sign -> [Named MSentence.Sentence]

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder -> (CSign.CASLSign, [Named CAS.CASLFORMULA])

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maedermaude2casl msign nsens = (csign { CSign.sortSet = cs,

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder CSign.sortRel = sbs',

adda0e6252b14215228e4071b347c49b808894f8Christian Maeder CSign.opMap = cops',

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder CSign.assocOps = assoc_ops,

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder CSign.predMap = preds,

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder CSign.declaredSymbols = syms }, new_sens)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder where csign = CSign.emptySign ()

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder ss = MSign.sorts msign

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder ss' = Set.map sym2id ss

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder mk = kindMapId $ MSign.kindRel msign

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder sbs = MSign.subsorts msign

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder sbs' = maudeSbs2caslSbs sbs mk

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder cs = Set.union ss' $ kindsFromMap mk

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder preds = rewPredicates cs

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder rs = rewPredicatesSens cs

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder ops = deleteUniversal $ MSign.ops msign

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder ksyms = kinds2syms cs

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder (cops, assoc_ops, _) = translateOps mk ops -- (cops, assoc_ops, comps)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder axSens = axiomsSens mk ops

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder cops' = universalOps cs cops $ booleanImported ops

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder rs' = rewPredicatesCongSens cops'

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder pred_forms = loadLibraries (MSign.sorts msign) ops

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder ops_syms = ops2symbols cops'

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder preds_syms = preds2syms preds

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder syms = Set.union ksyms $ Set.union ops_syms preds_syms

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder new_sens = concat [rs, rs', no_owise_forms, owise_forms,

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder mb_rl_forms, ctor_sen, pred_forms, axSens]

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | translates the Maude subsorts into CASL subsorts, and adds the subsorts

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- for the kinds

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermaudeSbs2caslSbs :: MSign.SubsortRel -> IdMap -> Rel.Rel CAS.SORT

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermaudeSbs2caslSbs sbs im = Rel.fromDistinctMap m4

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where l = Map.toList $ Rel.toMap sbs

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder l1 = [] -- map maudeSb2caslSb l

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder l2 = idList2Subsorts $ Map.toList im

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder l3 = map subsorts2Ids l

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder m1 = Map.fromList l1

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder m2 = Map.fromList l2

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder m3 = Map.fromList l3

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder m4 = Map.unionWith Set.union m1 $ Map.unionWith Set.union m2 m3

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederidList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederidList2Subsorts [] = []

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederidList2Subsorts ((id1, id2) : il) = t1 : idList2Subsorts il

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder where t1 = (id1, Set.singleton id2)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermaudeSb2caslSb :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedermaudeSb2caslSb (sym, st) = (sortSym2id sym, Set.map (kindId . sortSym2id) st)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maedersubsorts2Ids :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maedersubsorts2Ids (sym, st) = (sortSym2id sym, Set.map sortSym2id st)

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedersortSym2id :: MSym.Symbol -> Id

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaedersortSym2id (MSym.Sort q) = token2id q

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaedersortSym2id _ = token2id $ mkSimpleId $ "error_translation"

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | generates the sentences to state that the rew predicates are a congruence

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederrewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederrewPredicatesCongSens = Map.foldWithKey rewPredCongSet []

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- | generates the sentences to state that the rew predicates are a congruence

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder-- for the operator types in the set

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederrewPredCongSet :: Id -> Set.Set CSign.OpType -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian MaederrewPredCongSet idn ots fs = fs ++ fs'

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder where fs' = Set.fold (rewPredCong idn) [] ots

e2ca90217abd35b3d5f98bfe73ecffb34badd837Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | generates the sentences to state that the rew predicates are a congruence

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- for a single operator

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederrewPredCong :: Id -> CSign.OpType -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederrewPredCong op ot fs = case args of

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder [] -> fs

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder _ -> nq_form : fs

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where args = CSign.opArgs ot

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder vars1 = rewPredCongPremise 0 args

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder vars2 = rewPredCongPremise (length args) args

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder res = CSign.opRes ot

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder res_pred_type = CAS.Pred_type [res, res] nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder pn = CAS.Qual_pred_name rewID res_pred_type nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder name = "rew_cong_" ++ show op

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder prems = rewPredsCong args vars1 vars2

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder prems_conj = createConjForm prems

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder os = CAS.Qual_op_name op (CSign.toOP_TYPE ot) nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder conc_term1 = CAS.Application os vars1 nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder conc_term2 = CAS.Application os vars2 nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder conc_form = CAS.Predication pn [conc_term1, conc_term2] nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder form = createImpForm prems_conj conc_form

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder nq_form = makeNamed name $ quantifyUniversally form

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | generates a list of variables of the given sorts

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederrewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederrewPredCongPremise n (s : ss) = newVarIndex n s : rewPredCongPremise (n + 1) ss

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederrewPredCongPremise _ [] = []

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | generates a list of rew predicates with the given variables

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederrewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederrewPredsCong (s : ss) (t : ts) (t' : ts') = form : forms

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where pred_type = CAS.Pred_type [s, s] nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder pn = CAS.Qual_pred_name rewID pred_type nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder form = CAS.Predication pn [t, t'] nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder forms = rewPredsCong ss ts ts'

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederrewPredsCong _ _ _ = []

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | load the CASL libraries for the Maude built-in operators

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederloadLibraries :: MSign.SortSet -> MSign.OpMap -> [Named CAS.CASLFORMULA]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederloadLibraries ss om = case natImported ss om of

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder False -> []

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder True -> loadNaturalNatSens

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | loads the sentences associated to the natural numbers

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederloadNaturalNatSens :: [Named CAS.CASLFORMULA]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederloadNaturalNatSens =

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder let lib = head $ unsafePerformIO $ readLib "Maude/MaudeNumbers.casl"

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder in case lib of

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder G_theory lid _ _ thSens _ -> let sens = toNamedList thSens

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder in do

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder sens' <- coerceSens lid CASL "" sens

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder filter (not . ctorCons) sens'

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | checks if a sentence is an constructor sentence

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederctorCons :: Named CAS.CASLFORMULA -> Bool

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederctorCons f = case sentence f of

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder CAS.Sort_gen_ax _ _ -> True

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder _ -> False

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | checks if the boolean values are imported

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederbooleanImported :: MSign.OpMap -> Bool

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederbooleanImported = Map.member (mkSimpleId "if_then_else_fi")

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | checks if the natural numbers are imported

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaedernatImported :: MSign.SortSet -> MSign.OpMap -> Bool

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaedernatImported ss om = b1 && b2 && b3

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where b1 = Set.member (MSym.Sort $ mkSimpleId "Nat") ss

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder b2 = Map.member (mkSimpleId "s_") om

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder b3 = case b2 of

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder False -> True

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder True -> specialZeroSet $ om Map.! (mkSimpleId "s_")

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederspecialZeroSet :: MSign.OpDeclSet -> Bool

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederspecialZeroSet = Set.fold specialZero False

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederspecialZero :: MSign.OpDecl -> Bool -> Bool

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederspecialZero (_, ats) b = b' || b

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where b' = isSpecial ats

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederisSpecial :: [MAS.Attr] -> Bool

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederisSpecial [] = False

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederisSpecial ((MAS.Special _) : _) = True

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederisSpecial (_ : ats) = isSpecial ats

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | delete the universal operators from Maude specifications, that will be

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- substituted for one operator for each sort in the specification

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederdeleteUniversal :: MSign.OpMap -> MSign.OpMap

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederdeleteUniversal om = om5

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where om1 = Map.delete (mkSimpleId "if_then_else_fi") om

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder om2 = Map.delete (mkSimpleId "_==_") om1

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder om3 = Map.delete (mkSimpleId "_=/=_") om2

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder om4 = Map.delete (mkSimpleId "upTerm") om3

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder om5 = Map.delete (mkSimpleId "downTerm") om4

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | generates the universal operators for all the sorts in the module

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederuniversalOps :: Set.Set Id -> CSign.OpMap -> Bool -> CSign.OpMap

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederuniversalOps kinds om True = Set.fold universalOpKind om kinds

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederuniversalOps _ om False = om

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | generates the universal operators for a concrete module

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederuniversalOpKind :: Id -> CSign.OpMap -> CSign.OpMap

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederuniversalOpKind kind om = om3

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where if_id = str2id "if_then_else_fi"

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder double_eq_id = str2id "_==_"

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder neg_double_eq_id = str2id "_=/=_"

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder bool_id = str2id "Bool"

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder if_opt = Set.singleton $ CSign.OpType CAS.Total [bool_id, kind, kind] kind

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder eq_opt = Set.singleton $ CSign.OpType CAS.Total [kind, kind] bool_id

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder om1 = Map.insertWith Set.union if_id if_opt om

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder om2 = Map.insertWith Set.union double_eq_id eq_opt om1

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder om3 = Map.insertWith Set.union neg_double_eq_id eq_opt om2

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | generates the formulas for the universal operators

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederuniversalSens :: Set.Set Id -> [Named CAS.CASLFORMULA]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederuniversalSens = Set.fold universalSensKind []

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | generates the formulas for the universal operators for the given sort

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederuniversalSensKind :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederuniversalSensKind kind acc = concat [iss, eqs, neqs, acc]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where iss = ifSens kind

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder eqs = equalitySens kind

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder neqs = nonEqualitySens kind

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder-- | generates the formulas for the if statement

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederifSens :: Id -> [Named CAS.CASLFORMULA]

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian MaederifSens kind = [form'', neg_form'']

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder where v1 = newVarIndex 1 kind

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder v2 = newVarIndex 2 kind

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder bk = str2id "Bool"

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder bv = newVarIndex 2 bk

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder true_type = CAS.Op_type CAS.Total [] bk nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder true_id = CAS.Qual_op_name (str2id "true") true_type nullRange

7bffb8b0e6cae4bb7ecb59b99327add6106c06b9Christian Maeder true_term = CAS.Application true_id [] nullRange

if_type = CAS.Op_type CAS.Total [bk, kind, kind] kind nullRange

if_name = str2id "if_then_else_fi"

if_id = CAS.Qual_op_name if_name if_type nullRange

if_term = CAS.Application if_id [bv, v1, v2] nullRange

prem = CAS.Strong_equation bv true_term nullRange

concl = CAS.Strong_equation if_term v1 nullRange

form = CAS.Implication prem concl True nullRange

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

neg_concl = CAS.Strong_equation if_term v2 nullRange

neg_form = CAS.Implication neg_prem neg_concl True nullRange

neg_form' = quantifyUniversally neg_form

name1 = show kind ++ "_if_true"

name2 = show kind ++ "_if_false"

form'' = makeNamed name1 form'

neg_form'' = makeNamed name2 neg_form'

-- | generates the formulas for the equality

equalitySens :: Id -> [Named CAS.CASLFORMULA]

equalitySens kind = [form'', comp_form'']

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

bk = str2id "Bool"

b_type = CAS.Op_type CAS.Total [] bk nullRange

true_id = CAS.Qual_op_name (str2id "true") b_type nullRange

true_term = CAS.Application true_id [] nullRange

false_id = CAS.Qual_op_name (str2id "false") b_type nullRange

false_term = CAS.Application false_id [] nullRange

prem = CAS.Strong_equation v1 v2 nullRange

double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind nullRange

double_eq_name = str2id "_==_"

double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange

double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange

concl = CAS.Strong_equation double_eq_term true_term nullRange

form = CAS.Implication prem concl True nullRange

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

new_concl = CAS.Strong_equation double_eq_term false_term nullRange

comp_form = CAS.Implication neg_prem new_concl True nullRange

comp_form' = quantifyUniversally comp_form

name1 = show kind ++ "_==_true"

name2 = show kind ++ "_==_false"

form'' = makeNamed name1 form'

comp_form'' = makeNamed name2 comp_form'

-- | generates the formulas for the inequality

nonEqualitySens :: Id -> [Named CAS.CASLFORMULA]

nonEqualitySens kind = [form'', comp_form'']

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

bk = str2id "Bool"

b_type = CAS.Op_type CAS.Total [] bk nullRange

true_id = CAS.Qual_op_name (str2id "true") b_type nullRange

true_term = CAS.Application true_id [] nullRange

false_id = CAS.Qual_op_name (str2id "false") b_type nullRange

false_term = CAS.Application false_id [] nullRange

prem = CAS.Strong_equation v1 v2 nullRange

double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind nullRange

double_eq_name = str2id "_==_"

double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange

double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange

concl = CAS.Strong_equation double_eq_term false_term nullRange

form = CAS.Implication prem concl True nullRange

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

new_concl = CAS.Strong_equation double_eq_term true_term nullRange

comp_form = CAS.Implication neg_prem new_concl True nullRange

comp_form' = quantifyUniversally comp_form

name1 = show kind ++ "_=/=_false"

name2 = show kind ++ "_=/=_true"

form'' = makeNamed name1 form'

comp_form'' = makeNamed name2 comp_form'

-- | generates the sentences for the operator attributes

axiomsSens :: IdMap -> MSign.OpMap -> [Named CAS.CASLFORMULA]

axiomsSens im om = Map.fold (axiomsSensODS im) [] om

axiomsSensODS :: IdMap -> MSign.OpDeclSet -> [Named CAS.CASLFORMULA]

-> [Named CAS.CASLFORMULA]

axiomsSensODS im ods l = Set.fold (axiomsSensOD im) l ods

axiomsSensOD :: IdMap -> MSign.OpDecl -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

axiomsSensOD im (ss, ats) l = Set.fold (axiomsSensSS im ats) l ss

axiomsSensSS :: IdMap -> [MAS.Attr] -> MSym.Symbol -> [Named CAS.CASLFORMULA]

-> [Named CAS.CASLFORMULA]

axiomsSensSS im ats (MSym.Operator q ar co) l = concat [l, l1]

where l1 = if elem MAS.Comm ats

then commSen im q ar co

else []

axiomsSensSS _ _ _ l = l

commSen :: IdMap -> MAS.Qid -> MSym.Symbols -> MSym.Symbol -> [Named CAS.CASLFORMULA]

commSen im q ar@[ar1, ar2] co = [form']

where q' = token2id q

f = \ x -> maudeSymbol2caslSort x im

ar1' = f ar1

ar2' = f ar2

ot = CAS.Op_type CAS.Total (map f ar) (f co) nullRange

os = CAS.Qual_op_name q' ot nullRange

v1 = newVarIndex 1 ar1'

v2 = newVarIndex 2 ar2'

t1 = CAS.Application os [v1, v2] nullRange

t2 = CAS.Application os [v2, v1] nullRange

form = CAS.Strong_equation t1 t2 nullRange

name = "comm_" ++ (ms2vcs (show q')) ++ "_" ++ show ar1'

form' = makeNamed name $ quantifyUniversally form

commSen _ _ _ _ = []

-- (newVarIndex 1 (hd ar))

-- maudeSymbol2caslSort x im

-- | translates the Maude operator map into a tuple of CASL operators, CASL

-- associative operators, membership induced from each Maude operator,

-- and the set of sorts with the ctor attribute

translateOps :: IdMap -> MSign.OpMap -> OpTransTuple

translateOps im = Map.fold (translateOpDeclSet im) (Map.empty, Map.empty, Set.empty)

-- | translates an operator declaration set into a tern as described above

translateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple

translateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods

-- | given an operator declaration updates the accumulator with the translation

-- to CASL operator, checking if the operator has the assoc attribute to insert

-- it in the map of associative operators, generating the membership predicate

-- induced by the operator declaration, and checking if it has the ctor attribute

-- to introduce the operator in the generators sentence

translateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple

translateOpDecl im (syms, ats) (ops, assoc_ops, cs) = case tl of

[] -> (ops', assoc_ops', cs')

_ -> translateOpDecl im (syms', ats) (ops', assoc_ops', cs')

where sym = head $ Set.toList syms

tl = tail $ Set.toList syms

syms' = Set.fromList tl

(cop_id, ot, _) = fromJust $ maudeSym2CASLOp im sym

cop_type = Set.singleton ot -- Set.union (Set.singleton ot) (Set.singleton ot')

ops' = Map.insertWith (Set.union) cop_id cop_type ops

assoc_ops' = if any MAS.assoc ats

then Map.insertWith (Set.union) cop_id cop_type assoc_ops

else assoc_ops

cs' = if any MAS.ctor ats

then Set.insert (Component cop_id ot) cs

else cs

-- | translates a Maude operator symbol into a pair with the id of the operator

-- and its CASL type

maudeSym2CASLOp :: IdMap -> MSym.Symbol -> Maybe (Id, CSign.OpType, CSign.OpType)

maudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot, ot')

where f = token2id . getName

g = \ x -> maudeSymbol2caslSort x im

ot = CSign.OpType CAS.Total (map g ar) (g co)

ot' = CSign.OpType CAS.Total (map f ar) (f co)

maudeSym2CASLOp _ _ = Nothing

-- | creates a conjuctive formula distinguishing the size of the list

createConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA

createConjForm [] = CAS.True_atom nullRange

createConjForm [a] = a

createConjForm fs = CAS.Conjunction fs nullRange

-- | creates a implication formula distinguishing the size of the premises

createImpForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA -> CAS.CASLFORMULA

createImpForm (CAS.True_atom _) form = form

createImpForm form1 form2 = CAS.Implication form1 form2 True nullRange

-- | generates the predicates asserting the "true" sort of the operator if all

-- the arguments have the correct sort

ops2predPremises :: IdMap -> [MSym.Symbol] -> Int -> ([CAS.CASLTERM], [CAS.CASLFORMULA])

ops2predPremises im (MSym.Sort s : ss) i = (var : terms, form : forms)

where s' = token2id s

kind = Map.findWithDefault (errorId "mb of op as predicate") s' im

pred_type = CAS.Pred_type [kind] nullRange

pred_name = CAS.Qual_pred_name s' pred_type nullRange

var = newVarIndex i kind

form = CAS.Predication pred_name [var] nullRange

(terms, forms) = ops2predPremises im ss (i + 1)

ops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)

where k' = token2id k

kind = Map.findWithDefault (errorId "mb of op as predicate") k' im

var = newVarIndex i kind

(terms, forms) = ops2predPremises im ss (i + 1)

ops2predPremises _ _ _ = ([], [])

-- | traverses the Maude sentences, returning a pair of list of sentences.

-- The first list in the pair are the equations without the attribute "owise",

-- while the second one are the equations with this attribute

splitOwiseEqs :: [Named MSentence.Sentence] ->

([Named MSentence.Sentence], [Named MSentence.Sentence], [Named MSentence.Sentence])

splitOwiseEqs [] = ([], [], [])

splitOwiseEqs (s : ss) = res

where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss

sen = sentence s

res = case sen of

MSentence.Equation (MAS.Eq _ _ _ ats) -> case any MAS.owise ats of

True -> (no_owise_sens, s : owise_sens, mbs_rls)

False -> (s : no_owise_sens, owise_sens, mbs_rls)

_ -> (no_owise_sens, owise_sens, s : mbs_rls)

-- | translates a Maude equation defined without the "owise" attribute into

-- a CASL formula

noOwiseSen2Formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA

noOwiseSen2Formula im s = s'

where MSentence.Equation eq = sentence s

sen' = noOwiseEq2Formula im eq

s' = s { sentence = sen' }

-- | translates a Maude equation defined with the "owise" attribute into

-- a CASL formula

owiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]

-> Named MSentence.Sentence -> Named CAS.CASLFORMULA

owiseSen2Formula im owise_forms s = s'

where MSentence.Equation eq = sentence s

sen' = owiseEq2Formula im owise_forms eq

s' = s { sentence = sen' }

-- | translates a Maude membership or rule into a CASL formula

mb_rl2formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA

mb_rl2formula im s = case sen of

MSentence.Membership mb -> let

mb' = mb2formula im mb

in s { sentence = mb' }

MSentence.Rule rl -> let

rl' = rl2formula im rl

in s { sentence = rl' }

_ -> makeNamed "" $ CAS.False_atom nullRange

where sen = sentence s

-- | generates a new variable qualified with the given number

newVarIndex :: Int -> Id -> CAS.CASLTERM

newVarIndex i sort = CAS.Qual_var var sort nullRange

where var = mkSimpleId $ "V" ++ show i

-- | generates a new variable

newVar :: Id -> CAS.CASLTERM

newVar sort = CAS.Qual_var var sort nullRange

where var = mkSimpleId "V"

-- | Id for the rew predicate

rewID :: Id

rewID = token2id $ mkSimpleId "rew"

-- | translates a Maude equation without the "owise" attribute into a CASL formula

noOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA

noOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

form = CAS.Strong_equation ct ct' nullRange

noOwiseEq2Formula im (MAS.Eq t t' conds@(_:_) _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

conds_form = conds2formula im conds

concl_form = CAS.Strong_equation ct ct' nullRange

form = createImpForm conds_form concl_form

-- | transforms a Maude equation defined with the otherwise attribute into

-- a CASL formula

owiseEq2Formula :: IdMap -> [Named CAS.CASLFORMULA] -> MAS.Equation

-> CAS.CASLFORMULA

owiseEq2Formula im no_owise_form eq = form

where (eq_form, vars) = noQuantification $ noOwiseEq2Formula im eq

(op, ts, _) = fromJust $ getLeftApp eq_form

ex_form = existencialNegationOtherEqs op ts no_owise_form

imp_form = createImpForm ex_form eq_form

form = CAS.Quantification CAS.Universal vars imp_form nullRange

-- | generates a conjunction of negation of existencial quantifiers

existencialNegationOtherEqs :: CAS.OP_SYMB -> [CAS.CASLTERM] ->

[Named CAS.CASLFORMULA] -> CAS.CASLFORMULA

existencialNegationOtherEqs op ts forms = form

where ex_forms = foldr ((++) . existencialNegationOtherEq op ts) [] forms

form = if length ex_forms > 1

then CAS.Conjunction ex_forms nullRange

else head ex_forms

-- | given a formula, if it refers to the same operator indicated by the parameters

-- the predicate creates a list with the negation of the existence of variables that

-- match the pattern described in the formula. In other case it returns an empty list

existencialNegationOtherEq :: CAS.OP_SYMB -> [CAS.CASLTERM] ->

Named CAS.CASLFORMULA -> [CAS.CASLFORMULA]

existencialNegationOtherEq req_op terms form = case ok of

False -> []

True -> let

(_, ts, conds) = fromJust tpl

ts' = qualifyExVarsTerms ts

conds' = qualifyExVarsForms conds

prems = (createEqs ts' terms) ++ conds'

conj_form = CAS.Conjunction prems nullRange

ex_form = if vars' /= []

then CAS.Quantification CAS.Existential vars' conj_form nullRange

else conj_form

neg_form = CAS.Negation ex_form nullRange

in [neg_form]

where (inner_form, vars) = noQuantification $ sentence form

vars' = qualifyExVars vars

tpl = getLeftApp inner_form

ok = case tpl of

Nothing -> False

Just _ -> let (op, ts, _) = fromJust tpl

in req_op == op && length terms == length ts

-- | qualifies the variables in a list of formulas with the suffix "_ex" to

-- distinguish them from the variables already bound

qualifyExVarsForms :: [CAS.CASLFORMULA] -> [CAS.CASLFORMULA]

qualifyExVarsForms = map qualifyExVarsForm

-- | qualifies the variables in a formula with the suffix "_ex" to distinguish them

-- from the variables already bound

qualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA

qualifyExVarsForm (CAS.Strong_equation t t' r) = CAS.Strong_equation qt qt' r

where qt = qualifyExVarsTerm t

qt' = qualifyExVarsTerm t'

qualifyExVarsForm (CAS.Predication op ts r) = CAS.Predication op ts' r

where ts' = qualifyExVarsTerms ts

qualifyExVarsForm f = f

-- | qualifies the variables in a list of terms with the suffix "_ex" to

-- distinguish them from the variables already bound

qualifyExVarsTerms :: [CAS.CASLTERM] -> [CAS.CASLTERM]

qualifyExVarsTerms = map qualifyExVarsTerm

-- | qualifies the variables in a term with the suffix "_ex" to distinguish them

-- from the variables already bound

qualifyExVarsTerm :: CAS.CASLTERM -> CAS.CASLTERM

qualifyExVarsTerm (CAS.Qual_var var sort r) = CAS.Qual_var (qualifyExVarAux var) sort r

qualifyExVarsTerm (CAS.Application op ts r) = CAS.Application op ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Sorted_term t s r) = CAS.Sorted_term (qualifyExVarsTerm t) s r

qualifyExVarsTerm (CAS.Cast t s r) = CAS.Cast (qualifyExVarsTerm t) s r

qualifyExVarsTerm (CAS.Conditional t1 f t2 r) = CAS.Conditional t1' f t2' r

where t1' = qualifyExVarsTerm t1

t2' = qualifyExVarsTerm t2

qualifyExVarsTerm (CAS.Mixfix_term ts) = CAS.Mixfix_term ts'

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Mixfix_parenthesized ts r) = CAS.Mixfix_parenthesized ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Mixfix_bracketed ts r) = CAS.Mixfix_bracketed ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Mixfix_braced ts r) = CAS.Mixfix_braced ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm t = t

-- | qualifies a list of variables with the suffix "_ex" to

-- distinguish them from the variables already bound

qualifyExVars :: [CAS.VAR_DECL] -> [CAS.VAR_DECL]

qualifyExVars = map qualifyExVar

-- | qualifies a variable with the suffix "_ex" to distinguish it from

-- the variables already bound

qualifyExVar :: CAS.VAR_DECL -> CAS.VAR_DECL

qualifyExVar (CAS.Var_decl vars s r) = CAS.Var_decl vars' s r

where vars' = map qualifyExVarAux vars

-- | qualifies a token with the suffix "_ex"

qualifyExVarAux :: Token -> Token

qualifyExVarAux var = mkSimpleId $ show var ++ "_ex"

-- | creates a list of strong equalities from two lists of terms

createEqs :: [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]

createEqs (t1 : ts1) (t2 : ts2) = CAS.Strong_equation t1 t2 nullRange : ls

where ls = createEqs ts1 ts2

createEqs _ _ = []

-- | extracts the operator at the top and the arguments of the lefthand side

-- in a strong equation

getLeftApp :: CAS.CASLFORMULA -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM], [CAS.CASLFORMULA])

getLeftApp (CAS.Strong_equation term _ _) = case getLeftAppTerm term of

Nothing -> Nothing

Just (op, ts) -> Just (op, ts, [])

getLeftApp (CAS.Implication prem concl _ _) = case getLeftApp concl of

Nothing -> Nothing

Just (op, ts, _) -> Just (op, ts, conds)

where conds = getPremisesImplication prem

getLeftApp _ = Nothing

-- | extracts the operator at the top and the arguments of the lefthand side

-- in an application term

getLeftAppTerm :: CAS.CASLTERM -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM])

getLeftAppTerm (CAS.Application op ts _) = Just (op, ts)

getLeftAppTerm _ = Nothing

-- | extracts the formulas of the given premise, distinguishing whether it is

-- a conjunction or not

getPremisesImplication :: CAS.CASLFORMULA -> [CAS.CASLFORMULA]

getPremisesImplication (CAS.Conjunction forms _) = forms

getPremisesImplication form = [form]

-- | translate a Maude membership into a CASL formula

mb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA

mb2formula im (MAS.Mb t s [] _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

s' = token2id $ getName s

form = CAS.Membership ct s' nullRange

mb2formula im (MAS.Mb t s conds@(_ : _) _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

s' = token2id $ getName s

conds_form = conds2formula im conds

concl_form = CAS.Membership ct s' nullRange

form = CAS.Implication conds_form concl_form True nullRange

-- | translate a Maude rule into a CASL formula

rl2formula :: IdMap -> MAS.Rule -> CAS.CASLFORMULA

rl2formula im (MAS.Rl t t' [] _) = quantifyUniversally form

where ty = token2id $ getName $ MAS.getTermType t

kind = Map.findWithDefault (errorId "rl to formula") ty im

pred_type = CAS.Pred_type [kind, kind] nullRange

pred_name = CAS.Qual_pred_name rewID pred_type nullRange

ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

form = CAS.Predication pred_name [ct, ct'] nullRange

rl2formula im (MAS.Rl t t' conds@(_:_) _) = quantifyUniversally form

where ty = token2id $ getName $ MAS.getTermType t

kind = Map.findWithDefault (errorId "rl to formula") ty im

pred_type = CAS.Pred_type [kind, kind] nullRange

pred_name = CAS.Qual_pred_name rewID pred_type nullRange

ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

conds_form = conds2formula im conds

concl_form = CAS.Predication pred_name [ct, ct'] nullRange

form = CAS.Implication conds_form concl_form True nullRange

-- | translate a conjunction of Maude conditions to a CASL formula

conds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA

conds2formula im conds = CAS.Conjunction forms nullRange

where forms = map (cond2formula im) conds

-- | translate a single Maude condition to a CASL formula

cond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA

cond2formula im (MAS.EqCond t t') = CAS.Strong_equation ct ct' nullRange

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

cond2formula im (MAS.MatchCond t t') = CAS.Strong_equation ct ct' nullRange

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

cond2formula im (MAS.MbCond t s) = CAS.Membership ct s' nullRange

where ct = maudeTerm2caslTerm im t

s' = token2id $ getName s

cond2formula im (MAS.RwCond t t') = CAS.Predication pred_name [ct, ct'] nullRange

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

ty = token2id $ getName $ MAS.getTermType t

kind = Map.findWithDefault (errorId "rw cond to formula") ty im

pred_type = CAS.Pred_type [kind, kind] nullRange

pred_name = CAS.Qual_pred_name rewID pred_type nullRange

-- | translates a Maude term into a CASL term

maudeTerm2caslTerm :: IdMap -> MAS.Term -> CAS.CASLTERM

maudeTerm2caslTerm im (MAS.Var q ty) = CAS.Qual_var q ty' nullRange

where ty' = maudeType2caslSort ty im

maudeTerm2caslTerm im (MAS.Const q ty) = CAS.Application op [] nullRange

where name = token2id q

ty' = maudeType2caslSort ty im

op_type = CAS.Op_type CAS.Total [] ty' nullRange

op = CAS.Qual_op_name name op_type nullRange

maudeTerm2caslTerm im (MAS.Apply q ts ty) = CAS.Application op tts nullRange

where name = token2id q

tts = map (maudeTerm2caslTerm im) ts

ty' = maudeType2caslSort ty im

types_tts = getTypes tts

op_type = CAS.Op_type CAS.Total types_tts ty' nullRange

op = CAS.Qual_op_name name op_type nullRange

maudeSymbol2caslSort :: MSym.Symbol -> IdMap -> CAS.SORT

maudeSymbol2caslSort (MSym.Sort q) _ = token2id q

maudeSymbol2caslSort (MSym.Kind q) im = Map.findWithDefault err q' im

where q' = token2id q

err = errorId "error translate symbol"

maudeSymbol2caslSort _ _ = errorId "error translate symbol"

maudeType2caslSort :: MAS.Type -> IdMap -> CAS.SORT

maudeType2caslSort (MAS.TypeSort q) _ = token2id $ getName q

maudeType2caslSort (MAS.TypeKind q) im = Map.findWithDefault err q' im

where q' = token2id $ getName q

err = errorId "error translate type"

-- | obtains the types of the given terms

getTypes :: [CAS.CASLTERM] -> [Id]

getTypes = mapMaybe getType

-- | extracts the type of the temr

getType :: CAS.CASLTERM -> Maybe Id

getType (CAS.Qual_var _ kind _) = Just kind

getType (CAS.Application op _ _) = case op of

CAS.Qual_op_name _ (CAS.Op_type _ _ kind _) _ -> Just kind

_ -> Nothing

getType _ = Nothing

-- | generates the formulas for the rewrite predicates

rewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]

rewPredicatesSens = Set.fold rewPredicateSens []

-- | generates the formulas for the rewrite predicate of the given sort

rewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

rewPredicateSens kind acc = ref : trans : acc

where ref = reflSen kind

trans = transSen kind

-- | creates the reflexivity predicate for the given kind

reflSen :: Id -> Named CAS.CASLFORMULA

reflSen kind = makeNamed name $ quantifyUniversally form

where v = newVar kind

pred_type = CAS.Pred_type [kind, kind] nullRange

pn = CAS.Qual_pred_name rewID pred_type nullRange

form = CAS.Predication pn [v, v] nullRange

name = "rew_refl_" ++ show kind

-- | creates the transitivity predicate for the given kind

transSen :: Id -> Named CAS.CASLFORMULA

transSen kind = makeNamed name $ quantifyUniversally form

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

v3 = newVarIndex 3 kind

pred_type = CAS.Pred_type [kind, kind] nullRange

pn = CAS.Qual_pred_name rewID pred_type nullRange

prem1 = CAS.Predication pn [v1, v2] nullRange

prem2 = CAS.Predication pn [v2, v3] nullRange

concl = CAS.Predication pn [v1, v3] nullRange

conj_form = CAS.Conjunction [prem1, prem2] nullRange

form = CAS.Implication conj_form concl True nullRange

name = "rew_trans_" ++ show kind

-- | generate the predicates for the rewrites

rewPredicates :: Set.Set Id -> Map.Map Id (Set.Set CSign.PredType)

rewPredicates = Set.fold rewPredicate Map.empty

-- | generate the predicates for the rewrites of the given sort

rewPredicate :: Id -> Map.Map Id (Set.Set CSign.PredType)

-> Map.Map Id (Set.Set CSign.PredType)

rewPredicate kind m = Map.insertWith (Set.union) rewID ar m

where ar = Set.singleton $ CSign.PredType [kind, kind]

-- | create the predicates that assign sorts to each term

kindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)

kindPredicates = Map.foldWithKey kindPredicate Map.empty

-- | create the predicates that assign the current sort to the

-- corresponding terms

kindPredicate :: Id -> Id -> Map.Map Id (Set.Set CSign.PredType)

-> Map.Map Id (Set.Set CSign.PredType)

kindPredicate sort kind mis = case sort == (str2id "Universal") of

True -> mis

False -> let ar = Set.singleton $ CSign.PredType [kind]

in Map.insertWith (Set.union) sort ar mis

-- | extract the kinds from the map of id's

kindsFromMap :: IdMap -> Set.Set Id

kindsFromMap = Map.fold Set.insert Set.empty

-- | transform the set of Maude sorts in a set of CASL sorts, including

-- only one sort for each kind.

sortsTranslation :: MSign.SortSet -> MSign.SubsortRel -> Set.Set Id

sortsTranslation ss r = sortsTranslationList (Set.toList ss) r

-- | transform a list representing the Maude sorts in a set of CASL sorts,

-- including only one sort for each kind.

sortsTranslationList :: [MSym.Symbol] -> MSign.SubsortRel -> Set.Set Id

sortsTranslationList [] _ = Set.empty

sortsTranslationList (s : ss) r = Set.insert (sort2id tops) res

where tops@(top : _) = List.sort $ getTop r s

ss' = deleteRelated ss top r

res = sortsTranslation ss' r

-- | return the maximal elements from the sort relation

getTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]

getTop r tok = case succs of

[] -> [tok]

toks@(_:_) -> foldr ((++) . (getTop r)) [] toks

where succs = Set.toList $ Rel.succs r tok

-- | delete from the list of sorts those in the same kind that the parameter

deleteRelated :: [MSym.Symbol] -> MSym.Symbol -> MSign.SubsortRel -> MSign.SortSet

deleteRelated ss sym r = foldr (f sym tc) Set.empty ss

where tc = Rel.transClosure r

f = \ sort trC x y -> if MSym.sameKind trC sort x

then y

else Set.insert x y

-- | build an Id from a token with the function mkId

token2id :: Token -> Id

token2id t = mkId ts

where ts = maudeSymbol2validCASLSymbol t

-- | build an Id from a Maude symbol

sym2id :: MSym.Symbol -> Id

sym2id = token2id . getName

-- | generates an Id from a string

str2id :: String -> Id

str2id = token2id . mkSimpleId

-- | build an Id from a list of sorts, taking the first from the ordered list

sort2id :: [MSym.Symbol] -> Id

sort2id syms = mkId sym''

where sym = head $ List.sort syms

sym' = getName sym

sym'' = maudeSymbol2validCASLSymbol sym'

-- | add universal quantification of all variables in the formula

quantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA

quantifyUniversally form = if null var_decl

then form

else CAS.Quantification CAS.Universal var_decl form nullRange

where vars = getVars form

var_decl = listVarDecl vars

-- | traverses a map with sorts as keys and sets of variables as value and creates

-- a list of variable declarations

listVarDecl :: Map.Map Id (Set.Set Token) -> [CAS.VAR_DECL]

listVarDecl = Map.foldWithKey f []

where f = \ sort var_set acc -> CAS.Var_decl (Set.toList var_set) sort nullRange : acc

-- | removes a quantification from a formula

noQuantification :: CAS.CASLFORMULA -> (CAS.CASLFORMULA, [CAS.VAR_DECL])

noQuantification (CAS.Quantification _ vars form _) = (form, vars)

noQuantification form = (form, [])

-- | translate the CASL sorts to symbols

kinds2syms :: Set.Set Id -> Set.Set CSign.Symbol

kinds2syms = Set.map kind2sym

-- | translate a CASL sort to a CASL symbol

kind2sym :: Id -> CSign.Symbol

kind2sym k = CSign.Symbol k CSign.SortAsItemType

-- | translates the CASL predicates into CASL symbols

preds2syms :: Map.Map Id (Set.Set CSign.PredType) -> Set.Set CSign.Symbol

preds2syms = Map.foldWithKey pred2sym Set.empty

-- | translates a CASL predicate into a CASL symbol

pred2sym :: Id -> Set.Set CSign.PredType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol

pred2sym pn spt acc = Set.fold (createSym4id pn) acc spt

-- | creates a CASL symbol for a predicate

createSym4id :: Id -> CSign.PredType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol

createSym4id pn pt acc = Set.insert sym acc

where sym = CSign.Symbol pn $ CSign.PredAsItemType pt

-- | translates the CASL operators into CASL symbols

ops2symbols :: CSign.OpMap -> Set.Set CSign.Symbol

ops2symbols = Map.foldWithKey op2sym Set.empty

-- | translates a CASL operator into a CASL symbol

op2sym :: Id -> Set.Set CSign.OpType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol

op2sym on sot acc = Set.union set acc

where set = Set.fold (createSymOp4id on) Set.empty sot

-- | creates a CASL symbol for an operator

createSymOp4id :: Id -> CSign.OpType -> Set.Set CSign.Symbol -> Set.Set CSign.Symbol

createSymOp4id on ot acc = Set.insert sym acc

where sym = CSign.Symbol on $ CSign.OpAsItemType ot

-- | extract the variables from a CASL formula and put them in a map

-- with keys the sort of the variables and value the set of variables

-- in this sort

getVars :: CAS.CASLFORMULA -> Map.Map Id (Set.Set Token)

getVars (CAS.Quantification _ _ f _) = getVars f

getVars (CAS.Conjunction fs _) = foldr (Map.unionWith (Set.union) . getVars) Map.empty fs

getVars (CAS.Disjunction fs _) = foldr (Map.unionWith (Set.union) . getVars) Map.empty fs

getVars (CAS.Implication f1 f2 _ _) = Map.unionWith (Set.union) v1 v2

where v1 = getVars f1

v2 = getVars f2

getVars (CAS.Equivalence f1 f2 _) = Map.unionWith (Set.union) v1 v2

where v1 = getVars f1

v2 = getVars f2

getVars (CAS.Negation f _) = getVars f

getVars (CAS.Predication _ ts _) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVars (CAS.Definedness t _) = getVarsTerm t

getVars (CAS.Existl_equation t1 t2 _) = Map.unionWith (Set.union) v1 v2

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

getVars (CAS.Strong_equation t1 t2 _) = Map.unionWith (Set.union) v1 v2

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

getVars (CAS.Membership t _ _) = getVarsTerm t

getVars (CAS.Mixfix_formula t) = getVarsTerm t

getVars _ = Map.empty

-- | extract the variables of a CASL term

getVarsTerm :: CAS.CASLTERM -> Map.Map Id (Set.Set Token)

getVarsTerm (CAS.Qual_var var sort _) = Map.insert sort (Set.singleton var) Map.empty

getVarsTerm (CAS.Application _ ts _) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t

getVarsTerm (CAS.Cast t _ _) = getVarsTerm t

getVarsTerm (CAS.Conditional t1 f t2 _) = Map.unionWith (Set.union) v3 m

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

v3 = getVars f

m = Map.unionWith (Set.union) v1 v2

getVarsTerm (CAS.Mixfix_term ts) = foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Mixfix_parenthesized ts _) =

foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Mixfix_bracketed ts _) =

foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Mixfix_braced ts _) =

foldr (Map.unionWith (Set.union) . getVarsTerm) Map.empty ts

getVarsTerm _ = Map.empty

-- | generates the constructor constraint

ctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA

ctorSen isFree (sorts, _, ops) = do

let sortList = Set.toList sorts

opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide

(CSign.toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops

allSyms = opSyms

resType _ (CAS.Op_name _) = False

resType s (CAS.Qual_op_name _ t _) = CAS.res_OP_TYPE t == s

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)

collectOps s =

CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s

constrs = map collectOps sortList

f = CAS.Sort_gen_ax constrs isFree

makeNamed ("ga_generated_" ++ showSepList (showString "_") showId sortList "") f

-- | transforms a maude identifier into a valid CASL identifier

maudeSymbol2validCASLSymbol :: Token -> [Token]

maudeSymbol2validCASLSymbol t = splitDoubleUnderscores str ""

where str = ms2vcs $ show t

-- | transforms a string coding a Maude identifier into another string

-- representing a CASL identifier

ms2vcs :: String -> String

ms2vcs s@('k' : 'i' : 'n' : 'd' : '_' : _) = s

ms2vcs s = case Map.member s stringMap of

True -> Map.findWithDefault "" s stringMap

False -> let f = \ x y -> if Map.member x charMap

then (charMap Map.! x) ++ ['\''] ++ y

else if x == '_'

then "__" ++ y

else x : y

in foldr f [] s

-- | map of reserved words

stringMap :: Map.Map String String

stringMap = Map.fromList

[("true", "maudeTrue"),

("false", "maudeFalse"),

("not_", "neg__"),

("s_", "suc"),

("_+_", "__+__"),

("_*_", "__*__"),

("_<_", "__<__"),

("_<=_", "__<=__"),

("_>_", "__>__"),

("_>=_", "__>=__"),

("_and_", "__maudeAnd__")]

-- | splits the string into a list of tokens, separating the double

-- underscores from the rest of characters

splitDoubleUnderscores :: String -> String -> [Token]

splitDoubleUnderscores [] acc = if null acc

then []

else [mkSimpleId acc]

splitDoubleUnderscores ('_' : '_' : cs) acc = if null acc

then dut : rest

else acct : dut : rest

where acct = mkSimpleId acc

dut = mkSimpleId "__"

rest = splitDoubleUnderscores cs []

splitDoubleUnderscores (c : cs) acc = splitDoubleUnderscores cs (acc ++ [c])

-- | error Id

errorId :: String -> Id

errorId s = token2id $ mkSimpleId $ "ERROR: " ++ s

kindId :: Id -> Id

kindId i = token2id $ mkSimpleId $ "kind_" ++ show i

kindMapId :: MSign.KindRel -> IdMap

kindMapId kr = Map.fromList krl'

where krl = Map.toList kr

krl' = map (\ (x, y) -> (mSym2caslId x, mSym2caslId y)) krl

mSym2caslId :: MSym.Symbol -> Id

mSym2caslId (MSym.Sort q) = token2id q

mSym2caslId (MSym.Kind q) = kindId q'

where q' = token2id q

mSym2caslId _ = errorId "error translate symbol"

-- | checks the profile has at least one sort

atLeastOneSort :: MSign.OpMap -> MSign.OpMap

atLeastOneSort om = Map.fromList lom'

where lom = Map.toList om

lom' = filterAtLeastOneSort lom

filterAtLeastOneSort :: [(MAS.Qid, MSign.OpDeclSet)] -> [(MAS.Qid, MSign.OpDeclSet)]

filterAtLeastOneSort [] = []

filterAtLeastOneSort ((q, ods) : ls) = hd ++ filterAtLeastOneSort ls

where ods' = atLeastOneSortODS ods

hd = if Set.null ods'

then []

else [(q, ods')]

atLeastOneSortODS :: MSign.OpDeclSet -> MSign.OpDeclSet

atLeastOneSortODS ods = Set.fromList lods'

where lods = Set.toList ods

lods' = atLeastOneSortLODS lods

atLeastOneSortLODS :: [MSign.OpDecl] -> [MSign.OpDecl]

atLeastOneSortLODS [] = []

atLeastOneSortLODS ((ss, ats) : ls) = res ++ atLeastOneSortLODS ls

where ss' = atLeastOneSortSS ss

res = if Set.null ss'

then []

else [(ss', ats)]

atLeastOneSortSS :: Set.Set MSym.Symbol -> Set.Set MSym.Symbol

atLeastOneSortSS = Set.filter hasOneSort

hasOneSort :: MSym.Symbol -> Bool

hasOneSort (MSym.Operator _ ar co) = any isSymSort (co : ar)

hasOneSort _ = False

isSymSort :: MSym.Symbol -> Bool

isSymSort (MSym.Sort _) = True

isSymSort _ = False

-- | translates the Maude operator map into a tuple of CASL operators, CASL

-- associative operators, membership induced from each Maude operator,

-- and the set of sorts with the ctor attribute

translateOps' :: IdMap -> MSign.OpMap -> OpTransTuple

translateOps' im = Map.fold (translateOpDeclSet' im) (Map.empty, Map.empty, Set.empty)

-- | translates an operator declaration set into a tern as described above

translateOpDeclSet' :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple

translateOpDeclSet' im ods tpl = Set.fold (translateOpDecl' im) tpl ods

-- | given an operator declaration updates the accumulator with the translation

-- to CASL operator, checking if the operator has the assoc attribute to insert

-- it in the map of associative operators, generating the membership predicate

-- induced by the operator declaration, and checking if it has the ctor attribute

-- to introduce the operator in the generators sentence

translateOpDecl' :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple

translateOpDecl' im (syms, ats) (ops, assoc_ops, cs) = case tl of

[] -> (ops', assoc_ops', cs')

_ -> translateOpDecl' im (syms', ats) (ops', assoc_ops', cs')

where sym = head $ Set.toList syms

tl = tail $ Set.toList syms

syms' = Set.fromList tl

(cop_id, ot, _) = fromJust $ maudeSym2CASLOp' im sym

cop_type = Set.singleton ot -- Set.union (Set.singleton ot) (Set.singleton ot')

ops' = Map.insertWith (Set.union) cop_id cop_type ops

assoc_ops' = if any MAS.assoc ats

then Map.insertWith (Set.union) cop_id cop_type assoc_ops

else assoc_ops

cs' = if any MAS.ctor ats

then Set.insert (Component cop_id ot) cs

else cs

-- | translates a Maude operator symbol into a pair with the id of the operator

-- and its CASL type

maudeSym2CASLOp' :: IdMap -> MSym.Symbol -> Maybe (Id, CSign.OpType, CSign.OpType)

maudeSym2CASLOp' im (MSym.Operator op ar co) = Just (token2id op, ot, ot')

where f = token2id . getName

g = \ x -> maudeSymbol2caslSort' x im -- \ x -> Map.findWithDefault (errorId "Maude_sym2CASL_sym") (f x) im

ot = CSign.OpType CAS.Total (map g ar) (g co)

ot' = CSign.OpType CAS.Total (map f ar) (f co)

maudeSym2CASLOp' _ _ = Nothing

maudeSymbol2caslSort' :: MSym.Symbol -> IdMap -> CAS.SORT

maudeSymbol2caslSort' (MSym.Sort q) _ = token2id $ mkSimpleId $ "kind_" ++ show q

maudeSymbol2caslSort' (MSym.Kind q) im = Map.findWithDefault err q' im

where q' = token2id q

err = errorId "error translate symbol"

maudeSymbol2caslSort' _ _ = errorId "error translate symbol"