0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon Ulbricht{- |

0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtModule : ./Maude/PreComorphism.hs

0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtDescription : Maude Comorphisms

0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtCopyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

2643008447e30b6025f742eb6a661f38be756b1eSimon Ulbricht

0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtMaintainer : ariesco@fdi.ucm.es

0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtStability : experimental

0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtPortability : portable

0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon Ulbricht

0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon UlbrichtComorphism from Maude to CASL.

0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon Ulbricht-}

0b152383e04dbeb10dba29bcdfaa0981e4d9df27Simon Ulbricht

2643008447e30b6025f742eb6a661f38be756b1eSimon Ulbrichtmodule Maude.PreComorphism where

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maeder

2643008447e30b6025f742eb6a661f38be756b1eSimon Ulbrichtimport Data.Maybe

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtimport qualified Data.List as List

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtimport qualified Data.Set as Set

d815d2b83e945875100ceca322ebd50d96714206Simon Ulbrichtimport qualified Data.Map as Map

b0adcc203b4267d5535b430372935a5f36726db1Simon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtimport qualified Maude.Sign as MSign

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtimport qualified Maude.Sentence as MSentence

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbrichtimport qualified Maude.Morphism as MMorphism

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbrichtimport qualified Maude.AS_Maude as MAS

d815d2b83e945875100ceca322ebd50d96714206Simon Ulbrichtimport qualified Maude.Symbol as MSym

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbrichtimport Maude.Meta.HasName

6150196e8d99f7161a622fdc1a872fecd378195fSimon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtimport qualified CASL.Sign as CSign

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maederimport qualified CASL.Morphism as CMorphism

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbrichtimport qualified CASL.AS_Basic_CASL as CAS

3209c34f23fb83a86fbbdd6501db6d4bfb949a57Simon Ulbrichtimport CASL.StaticAna

2643008447e30b6025f742eb6a661f38be756b1eSimon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtimport Common.Id

2643008447e30b6025f742eb6a661f38be756b1eSimon Ulbrichtimport Common.Result

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbrichtimport Common.AS_Annotation

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbrichtimport Common.ProofUtils (charMap)

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbrichtimport qualified Common.Lib.Rel as Rel

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maederimport qualified Common.Lib.MapSet as MapSet

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maeder

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maedertype IdMap = Map.Map Id Id

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maedertype OpTransTuple = (CSign.OpMap, CSign.OpMap, Set.Set Component)

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maeder

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maeder-- | generates a CASL morphism from a Maude morphism

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian MaedermapMorphism :: MMorphism.Morphism -> Result CMorphism.CASLMor

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian MaedermapMorphism morph =

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maeder let

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht src = MMorphism.source morph

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maeder tgt = MMorphism.target morph

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maeder mk = kindMapId $ MSign.kindRel src

9da6e0cb2ea6e43f5b09dcd2a9af5468a5d0fcf4Christian Maeder mk' = kindMapId $ MSign.kindRel tgt

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht smap = MMorphism.sortMap morph

6150196e8d99f7161a622fdc1a872fecd378195fSimon Ulbricht omap = MMorphism.opMap morph

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht smap' = applySortMap2CASLSorts smap mk mk'

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht omap' = maudeOpMap2CASLOpMap mk omap

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder pmap = createPredMap mk smap

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder (src', _) = maude2casl src []

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder (tgt', _) = maude2casl tgt []

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

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht{- | translates the Maude morphism between operators into a CASL morpshim

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbrichtbetween operators -}

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon UlbrichtmaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon UlbrichtmaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht{- | translates the mapping between two symbols representing operators into

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbrichta CASL operators map -}

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon UlbrichttranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht -> CMorphism.Op_map

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon UlbrichttranslateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht = copm'

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht where f = token2id . getName

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder g x = Map.findWithDefault (errorId "translate op map entry")

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht (f x) im

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

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht cop = (token2id from, ot)

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder to' = (token2id to, CAS.Total)

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht copm' = Map.insert cop to' copm

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon UlbrichttranslateOpMapEntry _ _ _ _ = Map.empty

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht-- | generates a set of CASL symbol from a Maude Symbol

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon UlbrichtmapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon UlbrichtmapSymbol sg (MSym.Sort q) = Set.singleton csym

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht where mk = kindMapId $ MSign.kindRel sg

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht sym_id = token2id q

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht kind = Map.findWithDefault (errorId "map symbol") sym_id mk

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder pred_data = CSign.PredType [kind]

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data

65660c22133e6de16f9ece7b36ac6423014b20aaChristian MaedermapSymbol sg (MSym.Operator q ar co) = Set.singleton csym

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder where mk = kindMapId $ MSign.kindRel sg

432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht q' = token2id q

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht ar' = map (maudeSort2caslId mk) ar

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht co' = token2id $ getName co

432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht op_data = CSign.OpType CAS.Total ar' co'

432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht csym = CSign.Symbol q' $ CSign.OpAsItemType op_data

432ac7c08e2592af0660e026051ffb052e88a100Simon UlbrichtmapSymbol _ _ = Set.empty

432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht

432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht-- | returns the sort in CASL of the Maude sort symbol

432ac7c08e2592af0660e026051ffb052e88a100Simon UlbrichtmaudeSort2caslId :: IdMap -> MSym.Symbol -> Id

432ac7c08e2592af0660e026051ffb052e88a100Simon UlbrichtmaudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id")

432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht (token2id $ getName sym) im

432ac7c08e2592af0660e026051ffb052e88a100Simon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht{- | creates the predicate map for the CASL morphism from the Maude sort map and

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maederthe map between sorts and kinds -}

65660c22133e6de16f9ece7b36ac6423014b20aaChristian MaedercreatePredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map

a210c2e5add831cd438183c8602ed8e610922beaSimon UlbrichtcreatePredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht-- | creates an entry of the predicate map for a single sort

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon UlbrichtcreatePredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder -> CMorphism.Pred_map

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon UlbrichtcreatePredMap4sort im from to = Map.insert key id_to

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht where id_from = token2id $ getName from

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht id_to = token2id $ getName to

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht kind = Map.findWithDefault (errorId "predicate for sort")

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht id_from im

e9a1a4d5820d527a6800d524ebaf29fbad6196c6Simon Ulbricht key = (id_from, CSign.PredType [kind])

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder{- | computes the sort morphism of CASL from the sort morphism in Maude

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maederand the set of kinds -}

6a26171b5bc5b6ec3e1b02ae30dcfb6f03d7ffefSimon UlbrichtapplySortMap2CASLSorts :: MMorphism.SortMap -> IdMap -> IdMap

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht -> CMorphism.Sort_map

abea93ed557b22ea833e1524ee5ca11afc12208aSimon UlbrichtapplySortMap2CASLSorts sm im im' = Map.fromList sml'

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht where sml = Map.toList sm

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht sml' = foldr (applySortMap2CASLSort im im') [] sml

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht-- | computes the morphism for a single sort pair

abea93ed557b22ea833e1524ee5ca11afc12208aSimon UlbrichtapplySortMap2CASLSort :: IdMap -> IdMap -> (MSym.Symbol, MSym.Symbol)

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht -> [(Id, Id)] -> [(Id, Id)]

abea93ed557b22ea833e1524ee5ca11afc12208aSimon UlbrichtapplySortMap2CASLSort im im' (s1, s2) l = l'

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht where p1 = (mSym2caslId s1, mSym2caslId s2)

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht f x = Map.findWithDefault

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht (errorId $ "err" ++ show (mSym2caslId x)) (mSym2caslId x)

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht p2 = (f s1 im, f s2 im')

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht l' = p1 : if s1 == s2

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht then l else p2 : l

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbricht-- | renames the sorts in a given kind

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbrichtrename :: MMorphism.SortMap -> Token -> Token

abea93ed557b22ea833e1524ee5ca11afc12208aSimon Ulbrichtrename sm tok = new_tok

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder where sym = MSym.Sort tok

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder sym' = if Map.member sym sm

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder then fromJust $ Map.lookup sym sm

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder else sym

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht new_tok = getName sym'

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht-- | translates a Maude sentence into a CASL formula

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtmapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtmapSentence sg sen = let

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht mk = kindMapId $ MSign.kindRel sg

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht named = makeNamed "" sen

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht form = mb_rl2formula mk named

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht in return $ sentence $ case sen of

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht MSentence.Equation (MAS.Eq _ _ _ ats) -> if any MAS.owise ats then let

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht (no_owise_sens, _, _) = splitOwiseEqs sg_sens

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht in owiseSen2Formula mk no_owise_forms named

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht else noOwiseSen2Formula mk named

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht MSentence.Membership (MAS.Mb {}) -> form

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht MSentence.Rule (MAS.Rl {}) -> form

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht{- | applies maude2casl to compute the CASL signature and sentences from

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtthe Maude ones, and wraps them into a Result datatype -}

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtmapTheory :: (MSign.Sign, [Named MSentence.Sentence])

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht -> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtmapTheory (sg, nsens) = return $ maude2casl sg nsens

ea9768c548fe6ae05d275380869c2923c3392244Simon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht{- | computes new signature and sentences of CASL associated to the

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtgiven Maude signature and sentences -}

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtmaude2casl :: MSign.Sign -> [Named MSentence.Sentence]

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht -> (CSign.CASLSign, [Named CAS.CASLFORMULA])

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbrichtmaude2casl msign nsens = (csign {

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht CSign.sortRel =

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht Rel.union (Rel.fromKeysSet cs) sbs',

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht CSign.opMap = cops',

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht CSign.assocOps = assoc_ops,

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht CSign.predMap = preds,

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht CSign.declaredSymbols = syms }, new_sens)

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht where csign = CSign.emptySign ()

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht ss = MSign.sorts msign

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht ss' = Set.map sym2id ss

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht mk = kindMapId $ MSign.kindRel msign

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht sbs = MSign.subsorts msign

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht sbs' = maudeSbs2caslSbs sbs mk

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht cs = Set.union ss' $ kindsFromMap mk

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht preds = rewPredicates cs

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht rs = rewPredicatesSens cs

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht ops = deleteUniversal $ MSign.ops msign

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht ksyms = kinds2syms cs

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht (cops, assoc_ops, _) = translateOps mk ops -- (cops, assoc_ops, comps)

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht axSens = axiomsSens mk ops

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht cops' = universalOps cs cops $ booleanImported ops

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht rs' = rewPredicatesCongSens cops'

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht pred_forms = loadLibraries (MSign.sorts msign) ops

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht ops_syms = ops2symbols cops'

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht preds_syms = preds2syms preds

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht syms = Set.union ksyms $ Set.union ops_syms preds_syms

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht new_sens = concat [rs, rs', no_owise_forms, owise_forms,

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht mb_rl_forms, ctor_sen, pred_forms, axSens]

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht{- | translates the Maude subsorts into CASL subsorts, and adds the subsorts

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbrichtfor the kinds -}

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtmaudeSbs2caslSbs :: MSign.SubsortRel -> IdMap -> Rel.Rel CAS.SORT

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtmaudeSbs2caslSbs sbs im = Rel.fromMap m4

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht where l = Map.toList $ Rel.toMap sbs

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht l1 = [] -- map maudeSb2caslSb l

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht l2 = idList2Subsorts $ Map.toList im

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht l3 = map subsorts2Ids l

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht m1 = Map.fromList l1

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht m2 = Map.fromList l2

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht m3 = Map.fromList l3

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht m4 = Map.unionWith Set.union m1 $ Map.unionWith Set.union m2 m3

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon UlbrichtidList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtidList2Subsorts [] = []

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtidList2Subsorts ((id1, id2) : il) = t1 : idList2Subsorts il

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht where t1 = (id1, Set.singleton id2)

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht

a210c2e5add831cd438183c8602ed8e610922beaSimon UlbrichtmaudeSb2caslSb :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtmaudeSb2caslSb (sym, st) = (sortSym2id sym, Set.map (kindId . sortSym2id) st)

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht

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

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbrichtsubsorts2Ids (sym, st) = (sortSym2id sym, Set.map sortSym2id st)

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtsortSym2id :: MSym.Symbol -> Id

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon UlbrichtsortSym2id (MSym.Sort q) = token2id q

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon UlbrichtsortSym2id _ = token2id $ mkSimpleId "error_translation"

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht-- | generates the sentences to state that the rew predicates are a congruence

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtrewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon UlbrichtrewPredicatesCongSens = MapSet.foldWithKey rewPredCong []

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht{- | generates the sentences to state that the rew predicates are a congruence

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbrichtfor a single operator -}

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon UlbrichtrewPredCong :: Id -> CSign.OpType -> [Named CAS.CASLFORMULA]

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht -> [Named CAS.CASLFORMULA]

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtrewPredCong op ot fs = case args of

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht [] -> fs

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht _ -> nq_form : fs

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht where args = CSign.opArgs ot

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht vars1 = rewPredCongPremise 0 args

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht vars2 = rewPredCongPremise (length args) args

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht res = CSign.opRes ot

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht res_pred_type = CAS.Pred_type [res, res] nullRange

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht pn = CAS.Qual_pred_name rewID res_pred_type nullRange

ea9768c548fe6ae05d275380869c2923c3392244Simon Ulbricht name = "rew_cong_" ++ show op

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht prems = rewPredsCong args vars1 vars2

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht prems_conj = createConjForm prems

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht os = CAS.Qual_op_name op (CSign.toOP_TYPE ot) nullRange

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder conc_term1 = CAS.Application os vars1 nullRange

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder conc_term2 = CAS.Application os vars2 nullRange

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder conc_form = CAS.Predication pn [conc_term1, conc_term2] nullRange

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder form = createImpForm prems_conj conc_form

987c9ee1092c7fd8b53242abefe4f3cf8e9a1011Simon Ulbricht nq_form = makeNamed name $ quantifyUniversally form

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht-- | generates a list of variables of the given sorts

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtrewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtrewPredCongPremise n (s : ss) = newVarIndex n s : rewPredCongPremise (n + 1) ss

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtrewPredCongPremise _ [] = []

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht-- | generates a list of rew predicates with the given variables

ea9768c548fe6ae05d275380869c2923c3392244Simon UlbrichtrewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM]

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht -> [CAS.CASLFORMULA]

a210c2e5add831cd438183c8602ed8e610922beaSimon UlbrichtrewPredsCong (s : ss) (t : ts) (t' : ts') = form : forms

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht where pred_type = CAS.Pred_type [s, s] nullRange

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht pn = CAS.Qual_pred_name rewID pred_type nullRange

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht form = CAS.Predication pn [t, t'] nullRange

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht forms = rewPredsCong ss ts ts'

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon UlbrichtrewPredsCong _ _ _ = []

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder

65660c22133e6de16f9ece7b36ac6423014b20aaChristian Maeder-- | load the CASL libraries for the Maude built-in operators

65660c22133e6de16f9ece7b36ac6423014b20aaChristian MaederloadLibraries :: MSign.SortSet -> MSign.OpMap -> [Named CAS.CASLFORMULA]

a210c2e5add831cd438183c8602ed8e610922beaSimon UlbrichtloadLibraries ss om = if natImported ss om then loadNaturalNatSens else []

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht-- | loads the sentences associated to the natural numbers

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon UlbrichtloadNaturalNatSens :: [Named CAS.CASLFORMULA]

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon UlbrichtloadNaturalNatSens = [] -- retrieve code from Rev 17944 if needed again!

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht

3ac14720aa7f1e0715311bd1598e7d78c37dd3c6Simon Ulbricht-- | checks if a sentence is an constructor sentence

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon UlbrichtctorCons :: Named CAS.CASLFORMULA -> Bool

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon UlbrichtctorCons f = case sentence f of

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht CAS.Sort_gen_ax _ _ -> True

7c84f8fd92ed59eb2b9a674e6b1ea93c0f945006Simon Ulbricht _ -> False

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht-- | checks if the boolean values are imported

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon UlbrichtbooleanImported :: MSign.OpMap -> Bool

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon UlbrichtbooleanImported = Map.member (mkSimpleId "if_then_else_fi")

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht-- | checks if the natural numbers are imported

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon UlbrichtnatImported :: MSign.SortSet -> MSign.OpMap -> Bool

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon UlbrichtnatImported ss om = b1 && b2 && b3

53d3b5d18cae658f0e54872ade90ab5259b52b95Simon Ulbricht where b1 = Set.member (MSym.Sort $ mkSimpleId "Nat") ss

a210c2e5add831cd438183c8602ed8e610922beaSimon Ulbricht b2 = Map.member (mkSimpleId "s_") om

1651c7f5055453e18a8c34f96c333e2aa702a34eSimon Ulbricht b3 = not b2 || specialZeroSet (om Map.! mkSimpleId "s_")

369771f5d48a40eda134026b1f45f63b2c00bdb8Simon Ulbricht

specialZeroSet :: MSign.OpDeclSet -> Bool

specialZeroSet = Set.fold specialZero False

specialZero :: MSign.OpDecl -> Bool -> Bool

specialZero (_, ats) b = b' || b

where b' = isSpecial ats

isSpecial :: [MAS.Attr] -> Bool

isSpecial [] = False

isSpecial (MAS.Special _ : _) = True

isSpecial (_ : ats) = isSpecial ats

{- | delete the universal operators from Maude specifications, that will be

substituted for one operator for each sort in the specification -}

deleteUniversal :: MSign.OpMap -> MSign.OpMap

deleteUniversal om = om5

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

om2 = Map.delete (mkSimpleId "_==_") om1

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

om4 = Map.delete (mkSimpleId "upTerm") om3

om5 = Map.delete (mkSimpleId "downTerm") om4

-- | generates the universal operators for all the sorts in the module

universalOps :: Set.Set Id -> CSign.OpMap -> Bool -> CSign.OpMap

universalOps kinds om True = Set.fold universalOpKind om kinds

universalOps _ om False = om

-- | generates the universal operators for a concrete module

universalOpKind :: Id -> CSign.OpMap -> CSign.OpMap

universalOpKind kind = MapSet.union $ MapSet.fromList

[ (if_id, [if_opt]), (double_eq_id, [eq_opt]), (neg_double_eq_id, [eq_opt]) ]

where if_id = str2id "if_then_else_fi"

double_eq_id = str2id "_==_"

neg_double_eq_id = str2id "_=/=_"

bool_id = str2id "Bool"

if_opt = CSign.OpType CAS.Total [bool_id, kind, kind] kind

eq_opt = CSign.OpType CAS.Total [kind, kind] bool_id

-- | generates the formulas for the universal operators

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

universalSens = Set.fold universalSensKind []

-- | generates the formulas for the universal operators for the given sort

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

universalSensKind kind acc = concat [iss, eqs, neqs, acc]

where iss = ifSens kind

eqs = equalitySens kind

neqs = nonEqualitySens kind

-- | generates the formulas for the if statement

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

ifSens kind = [form'', neg_form'']

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

bk = str2id "Bool"

bv = newVarIndex 2 bk

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

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

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.mkStEq bv true_term

concl = CAS.mkStEq if_term v1

form = CAS.mkImpl prem concl

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

neg_concl = CAS.mkStEq if_term v2

neg_form = CAS.mkImpl neg_prem neg_concl

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.mkStEq v1 v2

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

nullRange

double_eq_name = str2id "_==_"

double_eq_id = CAS.mkQualOp double_eq_name double_eq_type

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

concl = CAS.mkStEq double_eq_term true_term

form = CAS.mkImpl prem concl

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

new_concl = CAS.mkStEq double_eq_term false_term

comp_form = CAS.mkImpl neg_prem new_concl

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.mkStEq v1 v2

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

nullRange

double_eq_name = str2id "_==_"

double_eq_id = CAS.mkQualOp double_eq_name double_eq_type

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

concl = CAS.mkStEq double_eq_term false_term

form = CAS.mkImpl prem concl

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

new_concl = CAS.mkStEq double_eq_term true_term

comp_form = CAS.mkImpl neg_prem new_concl

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 = Map.fold (axiomsSensODS im) []

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 = 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 = (`maudeSymbol2caslSort` 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.mkStEq t1 t2

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)

(MapSet.empty, MapSet.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 : tl = Set.toList syms

syms' = Set.fromList tl

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

ops' = MapSet.insert cop_id ot ops

assoc_ops' = if any MAS.assoc ats

then MapSet.insert cop_id ot 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 = (`maudeSymbol2caslSort` 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.conjunct

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

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

createImpForm (CAS.Atom True _) form = form

createImpForm form1 form2 = CAS.mkImpl form1 form2

{- | 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) ->

if any MAS.owise ats

then (no_owise_sens, s : owise_sens, mbs_rls)

else (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.falseForm

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.mkStEq ct ct'

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.mkStEq ct ct'

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.mkForall vars imp_form

-- | 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 = concatMap (existencialNegationOtherEq op ts) forms

form = CAS.conjunct 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 = if ok then let

(_, ts, conds) = fromJust tpl

ts' = qualifyExVarsTerms ts

conds' = qualifyExVarsForms conds

prems = createEqs ts' terms ++ conds'

conj_form = CAS.conjunct prems

ex_form = if null vars' then conj_form else

CAS.mkExist vars' conj_form

neg_form = CAS.mkNeg ex_form

in [neg_form]

else []

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.Equation t CAS.Strong t' r) =

CAS.Equation qt CAS.Strong 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.mkStEq t1 t2 : 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.Equation term CAS.Strong _ _) = case getLeftAppTerm term of

Nothing -> Nothing

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

getLeftApp (CAS.Relation prem c concl _) = case getLeftApp concl of

Just (op, ts, _) | c /= CAS.Equivalence -> Just (op, ts, conds)

where conds = getPremisesImplication prem

_ -> Nothing

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.Junction CAS.Con forms _) =

concatMap getPremisesImplication 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.mkImpl conds_form concl_form

-- | 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.mkImpl conds_form concl_form

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

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

conds2formula im conds = CAS.conjunct forms

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.mkStEq ct ct'

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

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

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.mkPredication pred_name [ct, ct']

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.conjunct [prem1, prem2]

form = CAS.mkImpl conj_form concl

name = "rew_trans_" ++ show kind

-- | generate the predicates for the rewrites

rewPredicates :: Set.Set Id -> CSign.PredMap

rewPredicates = Set.fold rewPredicate MapSet.empty

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

rewPredicate :: Id -> CSign.PredMap -> CSign.PredMap

rewPredicate kind = MapSet.insert rewID $ 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 = if sort == str2id "Universal" then mis else

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 = sortsTranslationList . Set.toList

{- | 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@(_ : _) -> concatMap (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 : _ = 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 = CAS.mkForall var_decl form

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 =

(CAS.Var_decl (Set.toList var_set) sort nullRange :)

-- | 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 :: CSign.PredMap -> Set.Set CSign.Symbol

preds2syms = MapSet.foldWithKey createSym4id Set.empty

-- | creates a CASL symbol for a predicate

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

-> Set.Set CSign.Symbol

createSym4id pn pt = Set.insert sym

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

-- | translates the CASL operators into CASL symbols

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

ops2symbols = MapSet.foldWithKey createSymOp4id Set.empty

-- | creates a CASL symbol for an operator

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

-> Set.Set CSign.Symbol

createSymOp4id on ot = Set.insert sym

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.Junction _ fs _) =

foldr (Map.unionWith Set.union . getVars) Map.empty fs

getVars (CAS.Relation 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.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) =

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 = fromMaybe (-1) $ List.elemIndex 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.mkSort_gen_ax constrs isFree

in 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 = if Map.member s stringMap

then stringMap Map.! s

else let f x y

| Map.member x charMap = (charMap Map.! x) ++ "'" ++ y

| x == '_' = "__" ++ y

| otherwise = 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)

(MapSet.empty, MapSet.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) =

if Set.null syms'

then (ops', assoc_ops', cs')

else translateOpDecl' im (syms', ats) (ops', assoc_ops', cs')

where (sym, syms') = Set.deleteFindMin syms

Just (cop_id, ot, _) = maudeSym2CASLOp' im sym

ops' = MapSet.insert cop_id ot ops

assoc_ops' = if any MAS.assoc ats

then MapSet.insert cop_id ot 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 = (`maudeSymbol2caslSort'` 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"