4ab980a06412fd86f52a6d054fb7e26de155c530erikabele{- |

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleModule : $Header$

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleDescription : Maude Comorphisms

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleMaintainer : ariesco@fdi.ucm.es

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleStability : experimental

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelePortability : portable

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleComorphism from Maude to CASL.

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-}

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemodule Maude.PreComorphism where

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport Data.Maybe

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified Data.List as List

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified Data.Set as Set

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified Data.Map as Map

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified Maude.Sign as MSign

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified Maude.Sentence as MSentence

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified Maude.Morphism as MMorphism

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified Maude.AS_Maude as MAS

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified Maude.Symbol as MSym

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport Maude.Meta.HasName

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified CASL.Sign as CSign

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified CASL.Morphism as CMorphism

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified CASL.AS_Basic_CASL as CAS

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport CASL.StaticAna

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport CASL.Logic_CASL

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport Common.Id

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport Common.Result

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport Common.AS_Annotation

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport Common.ProofUtils (charMap)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport qualified Common.Lib.Rel as Rel

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport Comorphisms.GetPreludeLib (readLib)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport System.IO.Unsafe

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport Static.GTheory

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport Logic.Prover

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleimport Logic.Coerce

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeletype IdMap = Map.Map Id Id

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeletype OpTransTuple = (CSign.OpMap, CSign.OpMap, Set.Set Component)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | generates a CASL morphism from a Maude morphism

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemapMorphism :: MMorphism.Morphism -> Result (CMorphism.CASLMor)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemapMorphism morph =

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele let

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele src = MMorphism.source morph

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele tgt = MMorphism.target morph

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele mk = arrangeKinds (MSign.sorts src) (MSign.subsorts src)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele cs = kindsFromMap mk

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele smap = MMorphism.sortMap morph

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele omap = MMorphism.opMap morph

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele smap' = applySortMap2CASLSorts smap cs

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele omap' = maudeOpMap2CASLOpMap mk omap

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele pmap = createPredMap mk smap

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele (src', _) = maude2casl src []

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele (tgt', _) = maude2casl tgt []

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | translates the Maude morphism between operators into a CASL morpshim between

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- operators

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | translates the mapping between two symbols representing operators into

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- a CASL operators map

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeletranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele -> CMorphism.Op_map

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeletranslateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm = copm'

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where f = token2id . getName

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

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele cop = (token2id from, ot)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele to' = (token2id to, CAS.Total)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele copm' = Map.insert cop to' copm

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeletranslateOpMapEntry _ _ _ _ = Map.empty

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | generates a set of CASL symbol from a Maude Symbol

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemapSymbol sg (MSym.Sort q) = Set.singleton csym

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele sym_id = token2id q

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele kind = Map.findWithDefault (errorId "map symbol") sym_id mk

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele pred_data = CSign.PredType [kind]

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele q' = token2id q

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele ar' = map (maudeSort2caslId mk) ar

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele co' = token2id $ getName co

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele op_data = CSign.OpType CAS.Total ar' co'

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele csym = CSign.Symbol q' $ CSign.OpAsItemType op_data

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemapSymbol _ _ = Set.empty

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | returns the sort in CASL of the Maude sort symbol

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemaudeSort2caslId :: IdMap -> MSym.Symbol -> Id

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | creates the predicate map for the CASL morphism from the Maude sort map and

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- the map between sorts and kinds

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelecreatePredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelecreatePredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | creates an entry of the predicate map for a single sort

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelecreatePredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele -> CMorphism.Pred_map

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelecreatePredMap4sort im from to m = Map.insert key id_to m

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where id_from = token2id $ getName from

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele id_to = token2id $ getName to

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele kind = Map.findWithDefault (errorId "predicate for sort") id_from im

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele key = (id_from, CSign.PredType [kind])

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | computes the sort morphism of CASL from the sort morphism in Maude and the set

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- of kinds

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleapplySortMap2CASLSorts :: MMorphism.SortMap -> Set.Set Id -> CMorphism.Sort_map

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleapplySortMap2CASLSorts sm = Set.fold (applySortMap2CASLSort sm) Map.empty

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

a3388213b2b4d46b356be205e38204e67b4304d8rbowen-- | computes the morphism for a single kind

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleapplySortMap2CASLSort :: MMorphism.SortMap -> Id -> CMorphism.Sort_map -> CMorphism.Sort_map

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleapplySortMap2CASLSort sm sort csm = new_csm

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where toks = getTokens sort

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele new_toks = map (rename sm) toks

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele new_sort = mkId new_toks

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele new_csm = if new_sort == sort

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele then csm

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele else Map.insert sort new_sort csm

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | renames the sorts in a given kind

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerename :: MMorphism.SortMap -> Token -> Token

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerename sm tok = new_tok

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where sym = MSym.Sort tok

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele sym' = if Map.member sym sm

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele then fromJust $ Map.lookup sym sm

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele else sym

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele new_tok = getName sym'

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | translates a Maude sentence into a CASL formula

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemapSentence sg sen@(MSentence.Equation eq) = case any MAS.owise ats of

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele False -> return $ sentence $ noOwiseSen2Formula mk named

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele True -> let

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele (no_owise_sens, _, _) = splitOwiseEqs sg_sens

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele trans = sentence $ owiseSen2Formula mk no_owise_forms named

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele in return trans

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele MAS.Eq _ _ _ ats = eq

a3388213b2b4d46b356be205e38204e67b4304d8rbowen named = makeNamed "" sen

a3388213b2b4d46b356be205e38204e67b4304d8rbowenmapSentence sg sen@(MSentence.Membership mb) = return $ sentence form

a3388213b2b4d46b356be205e38204e67b4304d8rbowen where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

a3388213b2b4d46b356be205e38204e67b4304d8rbowen MAS.Mb _ _ _ _ = mb

a3388213b2b4d46b356be205e38204e67b4304d8rbowen named = makeNamed "" sen

a3388213b2b4d46b356be205e38204e67b4304d8rbowen form = mb_rl2formula mk named

a3388213b2b4d46b356be205e38204e67b4304d8rbowenmapSentence sg sen@(MSentence.Rule rl) = return $ sentence form

a3388213b2b4d46b356be205e38204e67b4304d8rbowen where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

a3388213b2b4d46b356be205e38204e67b4304d8rbowen MAS.Rl _ _ _ _ = rl

a3388213b2b4d46b356be205e38204e67b4304d8rbowen named = makeNamed "" sen

a3388213b2b4d46b356be205e38204e67b4304d8rbowen form = mb_rl2formula mk named

a3388213b2b4d46b356be205e38204e67b4304d8rbowen

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

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

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele -> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemapTheory (sg, nsens) = return $ maude2casl sg nsens

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | computes new signature and sentences of CASL associated to the

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- given Maude signature and sentences

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemaude2casl :: MSign.Sign -> [Named MSentence.Sentence]

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele -> (CSign.CASLSign, [Named CAS.CASLFORMULA])

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemaude2casl msign nsens = (csign { CSign.sortSet = cs,

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele CSign.sortRel = sbs',

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele CSign.opMap = cops',

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele CSign.assocOps = assoc_ops,

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele CSign.predMap = preds,

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele CSign.declaredSymbols = syms }, new_sens)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where csign = CSign.emptySign ()

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele ss = MSign.sorts msign

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele ss' = Set.map sym2id ss

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele mk = arrangeKinds ss (MSign.subsorts msign)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele sbs = MSign.subsorts msign

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele sbs' = maudeSbs2caslSbs sbs mk

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele cs = Set.union ss' (kindsFromMap mk)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele preds = rewPredicates cs

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele rs = rewPredicatesSens cs

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele ops = deleteUniversal $ MSign.ops msign

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele ksyms = kinds2syms cs

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele (cops, assoc_ops, comps) = translateOps mk ops

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele ctor_sen = [ctorSen False (cs, Rel.empty, comps)]

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele cops' = universalOps cs cops $ booleanImported ops

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele rs' = rewPredicatesCongSens cops'

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele pred_forms = loadLibraries (MSign.sorts msign) ops

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele ops_syms = ops2symbols cops'

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele preds_syms = preds2syms preds

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele syms = Set.union ksyms $ Set.union ops_syms preds_syms

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele new_sens = concat [rs, rs', no_owise_forms, owise_forms,

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele mb_rl_forms, ctor_sen, pred_forms]

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | translates the Maude subsorts into CASL subsorts, and adds the subsorts

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- for the kinds

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemaudeSbs2caslSbs :: MSign.SubsortRel -> IdMap -> Rel.Rel CAS.SORT

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemaudeSbs2caslSbs sbs im = Rel.fromDistinctMap m

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where l = Map.toList $ Rel.toMap sbs

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele l1 = map maudeSb2caslSb l

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele l2 = idList2Subsorts $ Map.toList im

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele m = Map.fromList $ concat [l1, l2]

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleidList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleidList2Subsorts [] = []

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleidList2Subsorts ((id1, id2) : il) = (id1, Set.singleton id2) : idList2Subsorts il

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemaudeSb2caslSb :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelemaudeSb2caslSb (sym, st) = (sortSym2id sym, Set.map sortSym2id st)

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelesortSym2id :: MSym.Symbol -> Id

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelesortSym2id (MSym.Sort q) = token2id q

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelesortSym2id _ = token2id $ mkSimpleId $ "error_translation"

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerewPredicatesCongSens = Map.foldWithKey rewPredCongSet []

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- for the operator types in the set

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerewPredCongSet :: Id -> Set.Set CSign.OpType -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerewPredCongSet idn ots fs = fs ++ fs'

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where fs' = Set.fold (rewPredCong idn) [] ots

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- for a single operator

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerewPredCong op ot fs = case args of

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele [] -> fs

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele _ -> nq_form : fs

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele where args = CSign.opArgs ot

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele vars1 = rewPredCongPremise 0 args

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele vars2 = rewPredCongPremise (length args) args

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele res = CSign.opRes ot

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele res_pred_type = CAS.Pred_type [res, res] nullRange

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele pn = CAS.Qual_pred_name rewID res_pred_type nullRange

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele name = "rew_cong_" ++ show op

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele prems = rewPredsCong args vars1 vars2

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele prems_conj = createConjForm prems

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele conc_term1 = CAS.Application os vars1 nullRange

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele conc_term2 = CAS.Application os vars2 nullRange

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele form = createImpForm prems_conj conc_form

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele nq_form = makeNamed name $ quantifyUniversally form

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerewPredCongPremise _ [] = []

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerewPredsCong (s : ss) (t : ts) (t' : ts') = form : forms

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele pn = CAS.Qual_pred_name rewID pred_type nullRange

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele forms = rewPredsCong ss ts ts'

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelerewPredsCong _ _ _ = []

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

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

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

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleloadLibraries ss om = case natImported ss om of

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele False -> []

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele True -> loadNaturalNatSens

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | loads the sentences associated to the natural numbers

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleloadNaturalNatSens :: [Named CAS.CASLFORMULA]

4ab980a06412fd86f52a6d054fb7e26de155c530erikabeleloadNaturalNatSens =

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele let lib = head $ unsafePerformIO $ readLib "Maude/MaudeNumbers.casl"

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele in case lib of

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele G_theory lid _ _ thSens _ -> let sens = toNamedList thSens

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele in do

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele sens' <- coerceSens lid CASL "" sens

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele filter (not . ctorCons) sens'

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | checks if a sentence is an constructor sentence

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelectorCons :: Named CAS.CASLFORMULA -> Bool

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelectorCons f = case sentence f of

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele CAS.Sort_gen_ax _ _ -> True

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele _ -> False

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | checks if the boolean values are imported

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelebooleanImported :: MSign.OpMap -> Bool

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelebooleanImported = Map.member (mkSimpleId "if_then_else_fi")

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele

4ab980a06412fd86f52a6d054fb7e26de155c530erikabele-- | checks if the natural numbers are imported

4ab980a06412fd86f52a6d054fb7e26de155c530erikabelenatImported :: 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 = case b2 of

False -> True

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

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 om = om3

where if_id = str2id "if_then_else_fi"

double_eq_id = str2id "_==_"

neg_double_eq_id = str2id "_=/=_"

bool_id = str2id "Bool"

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

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

om1 = Map.insertWith Set.union if_id if_opt om

om2 = Map.insertWith Set.union double_eq_id eq_opt om1

om3 = Map.insertWith Set.union neg_double_eq_id eq_opt om2

-- | 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.Strong_equation bv true_term nullRange

concl = CAS.Strong_equation if_term v1 nullRange

form = CAS.Implication prem concl True nullRange

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

neg_concl = CAS.Strong_equation if_term v2 nullRange

neg_form = CAS.Implication neg_prem neg_concl True nullRange

neg_form' = quantifyUniversally neg_form

name1 = show kind ++ "_if_true"

name2 = show kind ++ "_if_false"

form'' = makeNamed name1 form'

neg_form'' = makeNamed name2 neg_form'

-- | generates the formulas for the equality

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

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

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

bk = str2id "Bool"

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

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

true_term = CAS.Application true_id [] nullRange

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

false_term = CAS.Application false_id [] nullRange

prem = CAS.Strong_equation v1 v2 nullRange

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

double_eq_name = str2id "_==_"

double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange

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

concl = CAS.Strong_equation double_eq_term true_term nullRange

form = CAS.Implication prem concl True nullRange

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

new_concl = CAS.Strong_equation double_eq_term false_term nullRange

comp_form = CAS.Implication neg_prem new_concl True nullRange

comp_form' = quantifyUniversally comp_form

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

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

form'' = makeNamed name1 form'

comp_form'' = makeNamed name2 comp_form'

-- | generates the formulas for the inequality

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

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

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

bk = str2id "Bool"

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

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

true_term = CAS.Application true_id [] nullRange

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

false_term = CAS.Application false_id [] nullRange

prem = CAS.Strong_equation v1 v2 nullRange

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

double_eq_name = str2id "_==_"

double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange

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

concl = CAS.Strong_equation double_eq_term false_term nullRange

form = CAS.Implication prem concl True nullRange

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

new_concl = CAS.Strong_equation double_eq_term true_term nullRange

comp_form = CAS.Implication neg_prem new_concl True nullRange

comp_form' = quantifyUniversally comp_form

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

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

form'' = makeNamed name1 form'

comp_form'' = makeNamed name2 comp_form'

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

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

-- and the set of sorts with the ctor attribute

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

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

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

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

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

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

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

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

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

-- to introduce the operator in the generators sentence

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

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

where sym = head $ Set.toList syms

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

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

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

assoc_ops' = if any MAS.assoc ats

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

else assoc_ops

cs' = if any MAS.ctor ats

then Set.insert (Component cop_id ot) cs

else cs

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

-- and its CASL type

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

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

where f = token2id . getName

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

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

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

maudeSym2CASLOp _ _ = Nothing

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

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

createConjForm [] = CAS.True_atom nullRange

createConjForm [a] = a

createConjForm fs = CAS.Conjunction fs nullRange

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

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

createImpForm (CAS.True_atom _) form = form

createImpForm form1 form2 = CAS.Implication form1 form2 True nullRange

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

-- the arguments have the correct sort

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

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

where s' = token2id s

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

pred_type = CAS.Pred_type [kind] nullRange

pred_name = CAS.Qual_pred_name s' pred_type nullRange

var = newVarIndex i kind

form = CAS.Predication pred_name [var] nullRange

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

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

where k' = token2id k

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

var = newVarIndex i kind

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

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

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

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

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

splitOwiseEqs :: [Named MSentence.Sentence] ->

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

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

splitOwiseEqs (s : ss) = res

where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss

sen = sentence s

res = case sen of

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

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

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

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

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

-- a CASL formula

noOwiseSen2Formula :: IdMap -> Named MSentence.Sentence

-> Named CAS.CASLFORMULA

noOwiseSen2Formula im s = s'

where MSentence.Equation eq = sentence s

sen' = noOwiseEq2Formula im eq

s' = s { sentence = sen' }

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

-- a CASL formula

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

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

owiseSen2Formula im owise_forms s = s'

where MSentence.Equation eq = sentence s

sen' = owiseEq2Formula im owise_forms eq

s' = s { sentence = sen' }

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

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

mb_rl2formula im s = case sen of

MSentence.Membership mb -> let

mb' = mb2formula im mb

in s { sentence = mb' }

MSentence.Rule rl -> let

rl' = rl2formula im rl

in s { sentence = rl' }

_ -> makeNamed "" $ CAS.False_atom nullRange

where sen = sentence s

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

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

newVarIndex i sort = CAS.Qual_var var sort nullRange

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

-- | generates a new variable

newVar :: Id -> CAS.CASLTERM

newVar sort = CAS.Qual_var var sort nullRange

where var = mkSimpleId "V"

-- | Id for the rew predicate

rewID :: Id

rewID = token2id $ mkSimpleId "rew"

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

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

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

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

form = CAS.Strong_equation ct ct' nullRange

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

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

conds_form = conds2formula im conds

concl_form = CAS.Strong_equation ct ct' nullRange

form = createImpForm conds_form concl_form

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

-- a CASL formula

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

-> CAS.CASLFORMULA

owiseEq2Formula im no_owise_form eq = form

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

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

ex_form = existencialNegationOtherEqs op ts no_owise_form

imp_form = createImpForm ex_form eq_form

form = CAS.Quantification CAS.Universal vars imp_form nullRange

-- | generates a conjunction of negation of existencial quantifiers

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

[Named CAS.CASLFORMULA] -> CAS.CASLFORMULA

existencialNegationOtherEqs op ts forms = form

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

form = if length ex_forms > 1

then CAS.Conjunction ex_forms nullRange

else head ex_forms

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

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

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

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

Named CAS.CASLFORMULA -> [CAS.CASLFORMULA]

existencialNegationOtherEq req_op terms form = case ok of

False -> []

True -> let

(_, ts, conds) = fromJust tpl

ts' = qualifyExVarsTerms ts

conds' = qualifyExVarsForms conds

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

conj_form = CAS.Conjunction prems nullRange

ex_form = if vars' /= []

then CAS.Quantification CAS.Existential vars' conj_form nullRange

else conj_form

neg_form = CAS.Negation ex_form nullRange

in [neg_form]

where (inner_form, vars) = noQuantification $ sentence form

vars' = qualifyExVars vars

tpl = getLeftApp inner_form

ok = case tpl of

Nothing -> False

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

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

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

-- distinguish them from the variables already bound

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

qualifyExVarsForms = map qualifyExVarsForm

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

-- from the variables already bound

qualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA

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

where qt = qualifyExVarsTerm t

qt' = qualifyExVarsTerm t'

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

where ts' = qualifyExVarsTerms ts

qualifyExVarsForm f = f

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

-- distinguish them from the variables already bound

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

qualifyExVarsTerms = map qualifyExVarsTerm

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

-- from the variables already bound

qualifyExVarsTerm :: CAS.CASLTERM -> CAS.CASLTERM

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

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

where ts' = map qualifyExVarsTerm ts

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

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

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

where t1' = qualifyExVarsTerm t1

t2' = qualifyExVarsTerm t2

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

where ts' = map qualifyExVarsTerm ts

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

where ts' = map qualifyExVarsTerm ts

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

where ts' = map qualifyExVarsTerm ts

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

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm t = t

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

-- distinguish them from the variables already bound

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

qualifyExVars = map qualifyExVar

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

-- the variables already bound

qualifyExVar :: CAS.VAR_DECL -> CAS.VAR_DECL

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

where vars' = map qualifyExVarAux vars

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

qualifyExVarAux :: Token -> Token

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

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

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

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

where ls = createEqs ts1 ts2

createEqs _ _ = []

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

-- in a strong equation

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

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

Nothing -> Nothing

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

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

Nothing -> Nothing

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

where conds = getPremisesImplication prem

getLeftApp _ = Nothing

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

-- in an application term

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

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

getLeftAppTerm _ = Nothing

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

-- a conjunction or not

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

getPremisesImplication (CAS.Conjunction forms _) = forms

getPremisesImplication form = [form]

-- | translate a Maude membership into a CASL formula

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

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

where ct = maudeTerm2caslTerm im t

s' = token2id $ getName s

form = CAS.Membership ct s' nullRange

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

where ct = maudeTerm2caslTerm im t

s' = token2id $ getName s

conds_form = conds2formula im conds

concl_form = CAS.Membership ct s' nullRange

form = CAS.Implication conds_form concl_form True nullRange

-- | translate a Maude rule into a CASL formula

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

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

where ty = token2id $ getName $ MAS.getTermType t

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

pred_type = CAS.Pred_type [kind, kind] nullRange

pred_name = CAS.Qual_pred_name rewID pred_type nullRange

ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

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

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

where ty = token2id $ getName $ MAS.getTermType t

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

pred_type = CAS.Pred_type [kind, kind] nullRange

pred_name = CAS.Qual_pred_name rewID pred_type nullRange

ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

conds_form = conds2formula im conds

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

form = CAS.Implication conds_form concl_form True nullRange

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

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

conds2formula im conds = CAS.Conjunction forms nullRange

where forms = map (cond2formula im) conds

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

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

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

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

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

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

cond2formula im (MAS.MbCond t s) = CAS.Predication pred_name [ct] nullRange

where ct = maudeTerm2caslTerm im t

s' = token2id $ getName s

kind = Map.findWithDefault (errorId "mb cond to formula") s' im

pred_type = CAS.Pred_type [kind] nullRange

pred_name = CAS.Qual_pred_name s' pred_type nullRange

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

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

ty = token2id $ getName $ MAS.getTermType t

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

pred_type = CAS.Pred_type [kind, kind] nullRange

pred_name = CAS.Qual_pred_name rewID pred_type nullRange

-- | translates a Maude term into a CASL term

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

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

where ty' = maudeType2caslSort ty im

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

where name = token2id q

ty' = maudeType2caslSort ty im

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

op = CAS.Qual_op_name name op_type nullRange

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

where name = token2id q

tts = map (maudeTerm2caslTerm im) ts

ty' = maudeType2caslSort ty im

types_tts = getTypes tts

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

op = CAS.Qual_op_name name op_type nullRange

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

maudeSymbol2caslSort (MSym.Sort q) _ = token2id q

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

where q' = token2id q

err = errorId "error translate symbol"

maudeSymbol2caslSort _ _ = errorId "error translate symbol"

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

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

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

where q' = token2id $ getName q

err = errorId "error translate type"

-- | obtains the types of the given terms

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

getTypes = mapMaybe getType

-- | extracts the type of the temr

getType :: CAS.CASLTERM -> Maybe Id

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

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

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

_ -> Nothing

getType _ = Nothing

-- | generates the formulas for the rewrite predicates

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

rewPredicatesSens = Set.fold rewPredicateSens []

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

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

rewPredicateSens kind acc = ref : trans : acc

where ref = reflSen kind

trans = transSen kind

-- | creates the reflexivity predicate for the given kind

reflSen :: Id -> Named CAS.CASLFORMULA

reflSen kind = makeNamed name $ quantifyUniversally form

where v = newVar kind

pred_type = CAS.Pred_type [kind, kind] nullRange

pn = CAS.Qual_pred_name rewID pred_type nullRange

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

name = "rew_refl_" ++ show kind

-- | creates the transitivity predicate for the given kind

transSen :: Id -> Named CAS.CASLFORMULA

transSen kind = makeNamed name $ quantifyUniversally form

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

v3 = newVarIndex 3 kind

pred_type = CAS.Pred_type [kind, kind] nullRange

pn = CAS.Qual_pred_name rewID pred_type nullRange

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

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

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

conj_form = CAS.Conjunction [prem1, prem2] nullRange

form = CAS.Implication conj_form concl True nullRange

name = "rew_trans_" ++ show kind

-- | generate the predicates for the rewrites

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

rewPredicates = Set.fold rewPredicate Map.empty

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

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

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

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

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

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

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

kindPredicates = Map.foldWithKey kindPredicate Map.empty

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

-- corresponding terms

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

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

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

True -> mis

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

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

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

kindsFromMap :: IdMap -> Set.Set Id

kindsFromMap = Map.fold Set.insert Set.empty

-- | return a map where each sort is mapped to its kind, both of them

-- already converted to Id

arrangeKinds :: MSign.SortSet -> MSign.SubsortRel -> IdMap

arrangeKinds ss r = arrangeKindsList (Set.toList ss) r Map.empty

-- | traverse the sorts and creates a table that assigns to each sort its kind

arrangeKindsList :: [MSym.Symbol] -> MSign.SubsortRel -> IdMap -> IdMap

arrangeKindsList [] _ m = m

arrangeKindsList l@(s : _) r m = arrangeKindsList not_rel r m'

where tops = List.sort $ getTop r s

tc = Rel.transClosure r

(rel, not_rel) = sameKindList s tc l

f = \ x y z -> Map.insert (sym2id y) (kindId $ sort2id x) z

m' = foldr (f tops) m rel

-- | creates two list distinguishing in the first componente the symbols

-- with the same kind than the given one and in the second one the

-- symbols with different kind

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

-> ([MSym.Symbol], [MSym.Symbol])

sameKindList _ _ [] = ([], [])

sameKindList t r (t' : ts) = if MSym.sameKind r t t'

then (t' : hold, not_hold)

else (hold, t' : not_hold)

where (hold, not_hold) = sameKindList t r ts

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

-- only one sort for each kind.

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

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

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

-- including only one sort for each kind.

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

sortsTranslationList [] _ = Set.empty

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

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

ss' = deleteRelated ss top r

res = sortsTranslation ss' r

-- | return the maximal elements from the sort relation

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

getTop r tok = case succs of

[] -> [tok]

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

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

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

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

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

where tc = Rel.transClosure r

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

then y

else Set.insert x y

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

token2id :: Token -> Id

token2id t = mkId ts

where ts = maudeSymbol2validCASLSymbol t

-- | build an Id from a Maude symbol

sym2id :: MSym.Symbol -> Id

sym2id = token2id . getName

-- | generates an Id from a string

str2id :: String -> Id

str2id = token2id . mkSimpleId

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

sort2id :: [MSym.Symbol] -> Id

sort2id syms = mkId sym''

where sym = head $ List.sort syms

sym' = getName sym

sym'' = maudeSymbol2validCASLSymbol sym'

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

quantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA

quantifyUniversally form = if null var_decl

then form

else CAS.Quantification CAS.Universal var_decl form nullRange

where vars = getVars form

var_decl = listVarDecl vars

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

-- a list of variable declarations

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

listVarDecl = Map.foldWithKey f []

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

-- | removes a quantification from a formula

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

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

noQuantification form = (form, [])

-- | translate the CASL sorts to symbols

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

kinds2syms = Set.map kind2sym

-- | translate a CASL sort to a CASL symbol

kind2sym :: Id -> CSign.Symbol

kind2sym k = CSign.Symbol k CSign.SortAsItemType

-- | translates the CASL predicates into CASL symbols

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

preds2syms = Map.foldWithKey pred2sym Set.empty

-- | translates a CASL predicate into a CASL symbol

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

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

-- | creates a CASL symbol for a predicate

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

createSym4id pn pt acc = Set.insert sym acc

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

-- | translates the CASL operators into CASL symbols

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

ops2symbols = Map.foldWithKey op2sym Set.empty

-- | translates a CASL operator into a CASL symbol

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

op2sym on sot acc = Set.union set acc

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

-- | creates a CASL symbol for an operator

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

createSymOp4id on ot acc = Set.insert sym acc

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

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

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

-- in this sort

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

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

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

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

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

where v1 = getVars f1

v2 = getVars f2

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

where v1 = getVars f1

v2 = getVars f2

getVars (CAS.Negation f _) = getVars f

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

getVars (CAS.Definedness t _) = getVarsTerm t

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

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

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

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

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

getVars (CAS.Mixfix_formula t) = getVarsTerm t

getVars _ = Map.empty

-- | extract the variables of a CASL term

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

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

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

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

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

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

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

v3 = getVars f

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

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

getVarsTerm (CAS.Mixfix_parenthesized ts _) =

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

getVarsTerm (CAS.Mixfix_bracketed ts _) =

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

getVarsTerm (CAS.Mixfix_braced ts _) =

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

getVarsTerm _ = Map.empty

-- | generates the constructor constraint

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

ctorSen isFree (sorts, _, ops) = do

let sortList = Set.toList sorts

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

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

allSyms = opSyms

resType _ (CAS.Op_name _) = False

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

getIndex s = maybe (-1) id $ List.findIndex (== s) sortList

addIndices (CAS.Op_name _) =

error "CASL/StaticAna: Internal error in function addIndices"

addIndices os@(CAS.Qual_op_name _ t _) =

(os,map getIndex $ CAS.args_OP_TYPE t)

collectOps s =

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

constrs = map collectOps sortList

f = CAS.Sort_gen_ax constrs isFree

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

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

maudeSymbol2validCASLSymbol :: Token -> [Token]

maudeSymbol2validCASLSymbol t = splitDoubleUnderscores str ""

where str = ms2vcs $ show t

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

-- representing a CASL identifier

ms2vcs :: String -> String

ms2vcs s = case Map.member s stringMap of

True -> Map.findWithDefault "" s stringMap

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

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

else if x == '_'

then "__" ++ y

else x : y

in foldr f [] s

-- | map of reserved words

stringMap :: Map.Map String String

stringMap = Map.fromList

[("true", "maudeTrue"),

("false", "maudeFalse"),

("not_", "neg__"),

("s_", "suc"),

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

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

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

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

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

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

("_and_", "__maudeAnd__")]

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

-- underscores from the rest of characters

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

splitDoubleUnderscores [] acc = if null acc

then []

else [mkSimpleId acc]

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

then dut : rest

else acct : dut : rest

where acct = mkSimpleId acc

dut = mkSimpleId "__"

rest = splitDoubleUnderscores cs []

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

-- | error Id

errorId :: String -> Id

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

kindId :: Id -> Id

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

-- | not useful anymore: ops2pred