fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis{- |

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorModule : $Header$

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorDescription : Maude Comorphisms

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

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorLicense : GPLv2 or higher, see LICENSE.txt

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorMaintainer : ariesco@fdi.ucm.es

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorStability : experimental

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorPortability : portable

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorComorphism from Maude to CASL.

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor-}

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormodule Maude.PreComorphism where

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport Data.Maybe

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified Data.List as List

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified Data.Set as Set

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified Data.Map as Map

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified Maude.Sign as MSign

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified Maude.Sentence as MSentence

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified Maude.Morphism as MMorphism

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified Maude.AS_Maude as MAS

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified Maude.Symbol as MSym

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport Maude.Meta.HasName

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentisimport qualified CASL.Sign as CSign

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified CASL.Morphism as CMorphism

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified CASL.AS_Basic_CASL as CAS

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentisimport CASL.StaticAna

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentisimport CASL.Logic_CASL

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport Common.Id

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport Common.Result

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentisimport Common.AS_Annotation

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport Common.ProofUtils (charMap)

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentisimport qualified Common.Lib.Rel as Rel

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport qualified Common.Lib.MapSet as MapSet

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentisimport Comorphisms.GetPreludeLib (readLib)

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport System.IO.Unsafe

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport Static.GTheory

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport Logic.Prover

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorimport Logic.Coerce

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentistype IdMap = Map.Map Id Id

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentistype OpTransTuple = (CSign.OpMap, CSign.OpMap, Set.Set Component)

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor-- | generates a CASL morphism from a Maude morphism

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormapMorphism :: MMorphism.Morphism -> Result CMorphism.CASLMor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormapMorphism morph =

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor let

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis src = MMorphism.source morph

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis tgt = MMorphism.target morph

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor mk = kindMapId $ MSign.kindRel src

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor mk' = kindMapId $ MSign.kindRel tgt

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis smap = MMorphism.sortMap morph

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis omap = MMorphism.opMap morph

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis smap' = applySortMap2CASLSorts smap mk mk'

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor omap' = maudeOpMap2CASLOpMap mk omap

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor pmap = createPredMap mk smap

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor (src', _) = maude2casl src []

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor (tgt', _) = maude2casl tgt []

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

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

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentisbetween operators -}

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor{- | translates the mapping between two symbols representing operators into

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzora CASL operators map -}

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzortranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor -> CMorphism.Op_map

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzortranslateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor = copm'

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor where f = token2id . getName

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor g x = Map.findWithDefault (errorId "translate op map entry")

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis (f x) im

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

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis cop = (token2id from, ot)

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor to' = (token2id to, CAS.Total)

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor copm' = Map.insert cop to' copm

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentistranslateOpMapEntry _ _ _ _ = Map.empty

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis-- | generates a set of CASL symbol from a Maude Symbol

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormapSymbol sg (MSym.Sort q) = Set.singleton csym

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor where mk = kindMapId $ MSign.kindRel sg

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor sym_id = token2id q

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor kind = Map.findWithDefault (errorId "map symbol") sym_id mk

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis pred_data = CSign.PredType [kind]

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentismapSymbol sg (MSym.Operator q ar co) = Set.singleton csym

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis where mk = kindMapId $ MSign.kindRel sg

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis q' = token2id q

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis ar' = map (maudeSort2caslId mk) ar

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis co' = token2id $ getName co

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor op_data = CSign.OpType CAS.Total ar' co'

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor csym = CSign.Symbol q' $ CSign.OpAsItemType op_data

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentismapSymbol _ _ = Set.empty

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor-- | returns the sort in CASL of the Maude sort symbol

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormaudeSort2caslId :: IdMap -> MSym.Symbol -> Id

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormaudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id")

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor (token2id $ getName sym) im

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor{- | creates the predicate map for the CASL morphism from the Maude sort map and

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorthe map between sorts and kinds -}

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentiscreatePredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentiscreatePredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor-- | creates an entry of the predicate map for a single sort

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorcreatePredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor -> CMorphism.Pred_map

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorcreatePredMap4sort im from to = Map.insert key id_to

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis where id_from = token2id $ getName from

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis id_to = token2id $ getName to

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor kind = Map.findWithDefault (errorId "predicate for sort")

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor id_from im

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor key = (id_from, CSign.PredType [kind])

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor{- | computes the sort morphism of CASL from the sort morphism in Maude

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorand the set of kinds -}

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorapplySortMap2CASLSorts :: MMorphism.SortMap -> IdMap -> IdMap

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor -> CMorphism.Sort_map

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorapplySortMap2CASLSorts sm im im' = Map.fromList sml'

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor where sml = Map.toList sm

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor sml' = foldr (applySortMap2CASLSort im im') [] sml

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis-- | computes the morphism for a single sort pair

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorapplySortMap2CASLSort :: IdMap -> IdMap -> (MSym.Symbol, MSym.Symbol)

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor -> [(Id, Id)] -> [(Id, Id)]

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorapplySortMap2CASLSort im im' (s1, s2) l = l'

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis where p1 = (mSym2caslId s1, mSym2caslId s2)

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor f x = Map.findWithDefault

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor (errorId $ "err" ++ show (mSym2caslId x)) (mSym2caslId x)

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis p2 = (f s1 im, f s2 im')

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis l' = if s1 == s2

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor then p1 : l

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis else p1 : p2 : l

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis-- | renames the sorts in a given kind

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorrename :: MMorphism.SortMap -> Token -> Token

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorrename sm tok = new_tok

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor where sym = MSym.Sort tok

4f1f74609a2656ae7d9061991ccfd16d25f1befalgentis sym' = if Map.member sym sm

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor then fromJust $ Map.lookup sym sm

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor else sym

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor new_tok = getName sym'

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis-- | translates a Maude sentence into a CASL formula

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentismapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentismapSentence sg sen = let

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis mk = kindMapId $ MSign.kindRel sg

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis named = makeNamed "" sen

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis form = mb_rl2formula mk named

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis in return $ sentence $ case sen of

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

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis (no_owise_sens, _, _) = splitOwiseEqs sg_sens

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis in owiseSen2Formula mk no_owise_forms named

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor else noOwiseSen2Formula mk named

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor MSentence.Membership (MAS.Mb {}) -> form

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor MSentence.Rule (MAS.Rl {}) -> form

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor{- | applies maude2casl to compute the CASL signature and sentences from

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorthe Maude ones, and wraps them into a Result datatype -}

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormapTheory :: (MSign.Sign, [Named MSentence.Sentence])

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor -> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormapTheory (sg, nsens) = return $ maude2casl sg nsens

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis{- | computes new signature and sentences of CASL associated to the

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorgiven Maude signature and sentences -}

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormaude2casl :: MSign.Sign -> [Named MSentence.Sentence]

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor -> (CSign.CASLSign, [Named CAS.CASLFORMULA])

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentismaude2casl msign nsens = (csign {

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis CSign.sortRel =

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor Rel.union (Rel.fromKeysSet cs) sbs',

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis CSign.opMap = cops',

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor CSign.assocOps = assoc_ops,

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor CSign.predMap = preds,

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor CSign.declaredSymbols = syms }, new_sens)

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor where csign = CSign.emptySign ()

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor ss = MSign.sorts msign

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor ss' = Set.map sym2id ss

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor mk = kindMapId $ MSign.kindRel msign

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor sbs = MSign.subsorts msign

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor sbs' = maudeSbs2caslSbs sbs mk

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis cs = Set.union ss' $ kindsFromMap mk

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis preds = rewPredicates cs

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis rs = rewPredicatesSens cs

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis ops = deleteUniversal $ MSign.ops msign

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor ksyms = kinds2syms cs

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor (cops, assoc_ops, _) = translateOps mk ops -- (cops, assoc_ops, comps)

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis axSens = axiomsSens mk ops

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis cops' = universalOps cs cops $ booleanImported ops

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis rs' = rewPredicatesCongSens cops'

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor pred_forms = loadLibraries (MSign.sorts msign) ops

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor ops_syms = ops2symbols cops'

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor preds_syms = preds2syms preds

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor syms = Set.union ksyms $ Set.union ops_syms preds_syms

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis new_sens = concat [rs, rs', no_owise_forms, owise_forms,

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis mb_rl_forms, ctor_sen, pred_forms, axSens]

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentis{- | translates the Maude subsorts into CASL subsorts, and adds the subsorts

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzorfor the kinds -}

fdcdd4e9cdf3f0213c5f63dac906531a1e5707a7lgentismaudeSbs2caslSbs :: MSign.SubsortRel -> IdMap -> Rel.Rel CAS.SORT

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzormaudeSbs2caslSbs sbs im = Rel.fromMap m4

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor where l = Map.toList $ Rel.toMap sbs

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor l1 = [] -- map maudeSb2caslSb l

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor l2 = idList2Subsorts $ Map.toList im

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor l3 = map subsorts2Ids l

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor m1 = Map.fromList l1

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor m2 = Map.fromList l2

1ffad0b9e645e3d784e55b63f972293da99d81a7gryzor m3 = Map.fromList l3

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

idList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]

idList2Subsorts [] = []

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

where t1 = (id1, Set.singleton id2)

maudeSb2caslSb :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)

maudeSb2caslSb (sym, st) = (sortSym2id sym, Set.map (kindId . sortSym2id) st)

subsorts2Ids :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)

subsorts2Ids (sym, st) = (sortSym2id sym, Set.map sortSym2id st)

sortSym2id :: MSym.Symbol -> Id

sortSym2id (MSym.Sort q) = token2id q

sortSym2id _ = token2id $ mkSimpleId "error_translation"

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

rewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]

rewPredicatesCongSens = MapSet.foldWithKey rewPredCong []

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

for a single operator -}

rewPredCong :: Id -> CSign.OpType -> [Named CAS.CASLFORMULA]

-> [Named CAS.CASLFORMULA]

rewPredCong op ot fs = case args of

[] -> fs

_ -> nq_form : fs

where args = CSign.opArgs ot

vars1 = rewPredCongPremise 0 args

vars2 = rewPredCongPremise (length args) args

res = CSign.opRes ot

res_pred_type = CAS.Pred_type [res, res] nullRange

pn = CAS.Qual_pred_name rewID res_pred_type nullRange

name = "rew_cong_" ++ show op

prems = rewPredsCong args vars1 vars2

prems_conj = createConjForm prems

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

conc_term1 = CAS.Application os vars1 nullRange

conc_term2 = CAS.Application os vars2 nullRange

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

form = createImpForm prems_conj conc_form

nq_form = makeNamed name $ quantifyUniversally form

-- | generates a list of variables of the given sorts

rewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]

rewPredCongPremise n (s : ss) = newVarIndex n s : rewPredCongPremise (n + 1) ss

rewPredCongPremise _ [] = []

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

rewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM]

-> [CAS.CASLFORMULA]

rewPredsCong (s : ss) (t : ts) (t' : ts') = form : forms

where pred_type = CAS.Pred_type [s, s] nullRange

pn = CAS.Qual_pred_name rewID pred_type nullRange

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

forms = rewPredsCong ss ts ts'

rewPredsCong _ _ _ = []

-- | load the CASL libraries for the Maude built-in operators

loadLibraries :: MSign.SortSet -> MSign.OpMap -> [Named CAS.CASLFORMULA]

loadLibraries ss om = if natImported ss om then loadNaturalNatSens else []

-- | loads the sentences associated to the natural numbers

loadNaturalNatSens :: [Named CAS.CASLFORMULA]

loadNaturalNatSens =

case unsafePerformIO $ readLib "Maude/MaudeNumbers.casl" of

G_theory lid _ _ _ thSens _ : _ -> do

let sens = toNamedList thSens

sens' <- coerceSens lid CASL "" sens

filter (not . ctorCons) sens'

_ -> error "Maude.loadNaturalNatSens"

-- | checks if a sentence is an constructor sentence

ctorCons :: Named CAS.CASLFORMULA -> Bool

ctorCons f = case sentence f of

CAS.Sort_gen_ax _ _ -> True

_ -> False

-- | checks if the boolean values are imported

booleanImported :: MSign.OpMap -> Bool

booleanImported = Map.member (mkSimpleId "if_then_else_fi")

-- | checks if the natural numbers are imported

natImported :: MSign.SortSet -> MSign.OpMap -> Bool

natImported ss om = b1 && b2 && b3

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

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

b3 = if b2 then specialZeroSet $ om Map.! mkSimpleId "s_" else True

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 = head $ Set.toList syms

tl = tail $ 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 = foldr ((++) . 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@(_ : _) -> 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 : _ = 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.Sort_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) = 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

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"