af84459fbf938e508fd10b01cb8d699c79083813takashi{- |

af84459fbf938e508fd10b01cb8d699c79083813takashiModule : $Header$

fd9abdda70912b99b24e3bf1a38f26fde908a74cndDescription : Maude Comorphisms

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashiMaintainer : ariesco@fdi.ucm.es

af84459fbf938e508fd10b01cb8d699c79083813takashiStability : experimental

af84459fbf938e508fd10b01cb8d699c79083813takashiPortability : portable

96ad5d81ee4a2cc66a4ae19893efc8aa6d06fae7jailletc

af84459fbf938e508fd10b01cb8d699c79083813takashiComorphism from Maude to CASL.

af84459fbf938e508fd10b01cb8d699c79083813takashi-}

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

2e545ce2450a9953665f701bb05350f0d3f26275ndmodule Maude.PreComorphism where

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenimport Data.Maybe

af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Data.List as List

af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Data.Set as Set

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowenimport qualified Data.Map as Map

3f08db06526d6901aa08c110b5bc7dde6bc39905nd

af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Maude.Sign as MSign

af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Maude.Sentence as MSentence

af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Maude.Morphism as MMorphism

3f08db06526d6901aa08c110b5bc7dde6bc39905ndimport qualified Maude.AS_Maude as MAS

af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Maude.Symbol as MSym

af84459fbf938e508fd10b01cb8d699c79083813takashiimport Maude.Meta.HasName

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified CASL.Sign as CSign

af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified CASL.Morphism as CMorphism

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjungimport qualified CASL.AS_Basic_CASL as CAS

af84459fbf938e508fd10b01cb8d699c79083813takashiimport CASL.StaticAna

a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coarimport CASL.Logic_CASL

a99c5d4cc3cab6a62b04d52000dbc22ce1fa2d94coar

af84459fbf938e508fd10b01cb8d699c79083813takashiimport Common.Id

af84459fbf938e508fd10b01cb8d699c79083813takashiimport Common.Result

af84459fbf938e508fd10b01cb8d699c79083813takashiimport Common.AS_Annotation

af84459fbf938e508fd10b01cb8d699c79083813takashiimport Common.ProofUtils (charMap)

af84459fbf938e508fd10b01cb8d699c79083813takashiimport qualified Common.Lib.Rel as Rel

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashiimport Comorphisms.GetPreludeLib (readLib)

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashiimport System.IO.Unsafe

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashiimport Static.GTheory

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashiimport Logic.Prover

af84459fbf938e508fd10b01cb8d699c79083813takashiimport Logic.Coerce

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashitype IdMap = Map.Map Id Id

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates a CASL morphism from a Maude morphism

af84459fbf938e508fd10b01cb8d699c79083813takashimapMorphism :: MMorphism.Morphism -> Result (CMorphism.CASLMor)

af84459fbf938e508fd10b01cb8d699c79083813takashimapMorphism morph =

af84459fbf938e508fd10b01cb8d699c79083813takashi let

af84459fbf938e508fd10b01cb8d699c79083813takashi src = MMorphism.source morph

af84459fbf938e508fd10b01cb8d699c79083813takashi tgt = MMorphism.target morph

af84459fbf938e508fd10b01cb8d699c79083813takashi mk = arrangeKinds (MSign.sorts src) (MSign.subsorts src)

af84459fbf938e508fd10b01cb8d699c79083813takashi cs = kindsFromMap mk

af84459fbf938e508fd10b01cb8d699c79083813takashi smap = MMorphism.sortMap morph

af84459fbf938e508fd10b01cb8d699c79083813takashi omap = MMorphism.opMap morph

af84459fbf938e508fd10b01cb8d699c79083813takashi smap' = applySortMap2CASLSorts smap cs

30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh omap' = maudeOpMap2CASLOpMap mk omap

af84459fbf938e508fd10b01cb8d699c79083813takashi pmap = createPredMap mk smap

af84459fbf938e508fd10b01cb8d699c79083813takashi (src', _) = maude2casl src []

af84459fbf938e508fd10b01cb8d699c79083813takashi (tgt', _) = maude2casl tgt []

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

3c13a815670b54d1c17bf02954f7d2b066cde95cnd-- | translates the Maude morphism between operators into a CASL morpshim between

3c13a815670b54d1c17bf02954f7d2b066cde95cnd-- operators

af84459fbf938e508fd10b01cb8d699c79083813takashimaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map

af84459fbf938e508fd10b01cb8d699c79083813takashimaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | translates the mapping between two symbols representing operators into

af84459fbf938e508fd10b01cb8d699c79083813takashi-- a CASL operators map

af84459fbf938e508fd10b01cb8d699c79083813takashitranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map

af84459fbf938e508fd10b01cb8d699c79083813takashi -> CMorphism.Op_map

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where f = token2id . getName

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi cop = (token2id from, ot)

af84459fbf938e508fd10b01cb8d699c79083813takashi to' = (token2id to, CAS.Total)

af84459fbf938e508fd10b01cb8d699c79083813takashi copm' = Map.insert cop to' copm

af84459fbf938e508fd10b01cb8d699c79083813takashitranslateOpMapEntry _ _ _ _ = Map.empty

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashimapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol

af84459fbf938e508fd10b01cb8d699c79083813takashimapSymbol sg (MSym.Sort q) = Set.singleton csym

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

af84459fbf938e508fd10b01cb8d699c79083813takashi sym_id = token2id q

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

af84459fbf938e508fd10b01cb8d699c79083813takashi pred_data = CSign.PredType [kind]

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

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

3c13a815670b54d1c17bf02954f7d2b066cde95cnd where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)

af84459fbf938e508fd10b01cb8d699c79083813takashi q' = token2id q

3c13a815670b54d1c17bf02954f7d2b066cde95cnd ar' = map (maudeSort2caslId mk) ar

3c13a815670b54d1c17bf02954f7d2b066cde95cnd co' = token2id $ getName co

af84459fbf938e508fd10b01cb8d699c79083813takashi op_data = CSign.OpType CAS.Total ar' co'

3c13a815670b54d1c17bf02954f7d2b066cde95cnd csym = CSign.Symbol q' $ CSign.OpAsItemType op_data

af84459fbf938e508fd10b01cb8d699c79083813takashimapSymbol _ _ = Set.empty

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | returns the sort in CASL of the Maude sort symbol

af84459fbf938e508fd10b01cb8d699c79083813takashimaudeSort2caslId :: IdMap -> MSym.Symbol -> Id

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

3c13a815670b54d1c17bf02954f7d2b066cde95cnd-- the map between sorts and kinds

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashicreatePredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map

af84459fbf938e508fd10b01cb8d699c79083813takashi -> CMorphism.Pred_map

af84459fbf938e508fd10b01cb8d699c79083813takashicreatePredMap4sort im from to m = Map.insert key id_to m

af84459fbf938e508fd10b01cb8d699c79083813takashi where id_from = token2id $ getName from

af84459fbf938e508fd10b01cb8d699c79083813takashi id_to = token2id $ getName to

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- of kinds

af84459fbf938e508fd10b01cb8d699c79083813takashiapplySortMap2CASLSorts :: MMorphism.SortMap -> Set.Set Id -> CMorphism.Sort_map

af84459fbf938e508fd10b01cb8d699c79083813takashiapplySortMap2CASLSorts sm = Set.fold (applySortMap2CASLSort sm) Map.empty

3c13a815670b54d1c17bf02954f7d2b066cde95cnd

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | computes the morphism for a single kind

af84459fbf938e508fd10b01cb8d699c79083813takashiapplySortMap2CASLSort :: MMorphism.SortMap -> Id -> CMorphism.Sort_map -> CMorphism.Sort_map

af84459fbf938e508fd10b01cb8d699c79083813takashiapplySortMap2CASLSort sm sort csm = new_csm

af84459fbf938e508fd10b01cb8d699c79083813takashi where toks = getTokens sort

3c13a815670b54d1c17bf02954f7d2b066cde95cnd new_toks = map (rename sm) toks

af84459fbf938e508fd10b01cb8d699c79083813takashi new_sort = mkId new_toks

af84459fbf938e508fd10b01cb8d699c79083813takashi new_csm = if new_sort == sort

af84459fbf938e508fd10b01cb8d699c79083813takashi then csm

af84459fbf938e508fd10b01cb8d699c79083813takashi else Map.insert sort new_sort csm

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | renames the sorts in a given kind

af84459fbf938e508fd10b01cb8d699c79083813takashirename :: MMorphism.SortMap -> Token -> Token

af84459fbf938e508fd10b01cb8d699c79083813takashirename sm tok = new_tok

af84459fbf938e508fd10b01cb8d699c79083813takashi where sym = MSym.Sort tok

af84459fbf938e508fd10b01cb8d699c79083813takashi sym' = if Map.member sym sm

af84459fbf938e508fd10b01cb8d699c79083813takashi then fromJust $ Map.lookup sym sm

af84459fbf938e508fd10b01cb8d699c79083813takashi else sym

af84459fbf938e508fd10b01cb8d699c79083813takashi new_tok = getName sym'

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi False -> return $ sentence $ noOwiseSen2Formula mk named

af84459fbf938e508fd10b01cb8d699c79083813takashi True -> let

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

af84459fbf938e508fd10b01cb8d699c79083813takashi (no_owise_sens, _, _) = splitOwiseEqs sg_sens

af84459fbf938e508fd10b01cb8d699c79083813takashi no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

af84459fbf938e508fd10b01cb8d699c79083813takashi trans = sentence $ owiseSen2Formula mk no_owise_forms named

af84459fbf938e508fd10b01cb8d699c79083813takashi in return trans

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

af84459fbf938e508fd10b01cb8d699c79083813takashi MAS.Eq _ _ _ ats = eq

3c13a815670b54d1c17bf02954f7d2b066cde95cnd named = makeNamed "" sen

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi MAS.Mb _ _ _ _ = mb

3c13a815670b54d1c17bf02954f7d2b066cde95cnd named = makeNamed "" sen

af84459fbf938e508fd10b01cb8d699c79083813takashi form = mb_rl2formula mk named

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi MAS.Rl _ _ _ _ = rl

af84459fbf938e508fd10b01cb8d699c79083813takashi named = makeNamed "" sen

af84459fbf938e508fd10b01cb8d699c79083813takashi form = mb_rl2formula mk named

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashimapTheory (sg, nsens) = return $ maude2casl sg nsens

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- given Maude signature and sentences

af84459fbf938e508fd10b01cb8d699c79083813takashimaude2casl :: MSign.Sign -> [Named MSentence.Sentence]

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

af84459fbf938e508fd10b01cb8d699c79083813takashimaude2casl msign nsens = (csign { CSign.sortSet = cs,

af84459fbf938e508fd10b01cb8d699c79083813takashi CSign.sortRel = sbs',

af84459fbf938e508fd10b01cb8d699c79083813takashi CSign.opMap = cops',

af84459fbf938e508fd10b01cb8d699c79083813takashi CSign.assocOps = assoc_ops,

af84459fbf938e508fd10b01cb8d699c79083813takashi CSign.predMap = preds,

af84459fbf938e508fd10b01cb8d699c79083813takashi CSign.declaredSymbols = syms }, new_sens)

af84459fbf938e508fd10b01cb8d699c79083813takashi where csign = CSign.emptySign ()

af84459fbf938e508fd10b01cb8d699c79083813takashi ss = MSign.sorts msign

af84459fbf938e508fd10b01cb8d699c79083813takashi ss' = Set.map sym2id ss

af84459fbf938e508fd10b01cb8d699c79083813takashi mk = arrangeKinds ss (MSign.subsorts msign)

af84459fbf938e508fd10b01cb8d699c79083813takashi sbs = MSign.subsorts msign

af84459fbf938e508fd10b01cb8d699c79083813takashi sbs' = maudeSbs2caslSbs sbs mk

af84459fbf938e508fd10b01cb8d699c79083813takashi cs = Set.union ss' (kindsFromMap mk)

af84459fbf938e508fd10b01cb8d699c79083813takashi preds = rewPredicates cs

af84459fbf938e508fd10b01cb8d699c79083813takashi rs = rewPredicatesSens cs

af84459fbf938e508fd10b01cb8d699c79083813takashi ops = deleteUniversal $ MSign.ops msign

af84459fbf938e508fd10b01cb8d699c79083813takashi ksyms = kinds2syms cs

af84459fbf938e508fd10b01cb8d699c79083813takashi (cops, assoc_ops, comps) = translateOps mk ops

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

af84459fbf938e508fd10b01cb8d699c79083813takashi cops' = universalOps cs cops $ booleanImported ops

af84459fbf938e508fd10b01cb8d699c79083813takashi rs' = rewPredicatesCongSens cops'

af84459fbf938e508fd10b01cb8d699c79083813takashi pred_forms = loadLibraries (MSign.sorts msign) ops

af84459fbf938e508fd10b01cb8d699c79083813takashi ops_syms = ops2symbols cops'

af84459fbf938e508fd10b01cb8d699c79083813takashi (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens

af84459fbf938e508fd10b01cb8d699c79083813takashi no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

af84459fbf938e508fd10b01cb8d699c79083813takashi owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens

af84459fbf938e508fd10b01cb8d699c79083813takashi mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens

af84459fbf938e508fd10b01cb8d699c79083813takashi preds_syms = preds2syms preds

af84459fbf938e508fd10b01cb8d699c79083813takashi syms = Set.union ksyms $ Set.union ops_syms preds_syms

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

af84459fbf938e508fd10b01cb8d699c79083813takashi mb_rl_forms, ctor_sen, pred_forms]

af84459fbf938e508fd10b01cb8d699c79083813takashi

ec5fd46fd2a4a263bb5cdf419e8d4106007a2ac8gryzor-- | translates the Maude subsorts into CASL subsorts, and adds the subsorts

af84459fbf938e508fd10b01cb8d699c79083813takashi-- for the kinds

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

af84459fbf938e508fd10b01cb8d699c79083813takashimaudeSbs2caslSbs sbs im = Rel.fromDistinctMap m3

af84459fbf938e508fd10b01cb8d699c79083813takashi where l = Map.toList $ Rel.toMap sbs

af84459fbf938e508fd10b01cb8d699c79083813takashi l1 = map maudeSb2caslSb l

af84459fbf938e508fd10b01cb8d699c79083813takashi l2 = idList2Subsorts $ Map.toList im

af84459fbf938e508fd10b01cb8d699c79083813takashi m1 = Map.fromList l1

af84459fbf938e508fd10b01cb8d699c79083813takashi m2 = Map.fromList l2

af84459fbf938e508fd10b01cb8d699c79083813takashi m3 = Map.unionWith Set.union m1 m2

af84459fbf938e508fd10b01cb8d699c79083813takashi -- m = Map.fromList $ concat [l1, l2]

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashiidList2Subsorts [] = []

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashisortSym2id :: MSym.Symbol -> Id

af84459fbf938e508fd10b01cb8d699c79083813takashisortSym2id (MSym.Sort q) = token2id q

af84459fbf938e508fd10b01cb8d699c79083813takashisortSym2id _ = token2id $ mkSimpleId $ "error_translation"

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashirewPredicatesCongSens = Map.foldWithKey rewPredCongSet []

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- for the operator types in the set

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

af84459fbf938e508fd10b01cb8d699c79083813takashirewPredCongSet idn ots fs = fs ++ fs'

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- for a single operator

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

af84459fbf938e508fd10b01cb8d699c79083813takashirewPredCong op ot fs = case args of

af84459fbf938e508fd10b01cb8d699c79083813takashi [] -> fs

af84459fbf938e508fd10b01cb8d699c79083813takashi _ -> nq_form : fs

af84459fbf938e508fd10b01cb8d699c79083813takashi where args = CSign.opArgs ot

af84459fbf938e508fd10b01cb8d699c79083813takashi vars1 = rewPredCongPremise 0 args

af84459fbf938e508fd10b01cb8d699c79083813takashi vars2 = rewPredCongPremise (length args) args

af84459fbf938e508fd10b01cb8d699c79083813takashi res = CSign.opRes ot

af84459fbf938e508fd10b01cb8d699c79083813takashi res_pred_type = CAS.Pred_type [res, res] nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi pn = CAS.Qual_pred_name rewID res_pred_type nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi name = "rew_cong_" ++ show op

af84459fbf938e508fd10b01cb8d699c79083813takashi prems = rewPredsCong args vars1 vars2

af84459fbf938e508fd10b01cb8d699c79083813takashi prems_conj = createConjForm prems

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

af84459fbf938e508fd10b01cb8d699c79083813takashi conc_term1 = CAS.Application os vars1 nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi conc_term2 = CAS.Application os vars2 nullRange

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

af84459fbf938e508fd10b01cb8d699c79083813takashi form = createImpForm prems_conj conc_form

af84459fbf938e508fd10b01cb8d699c79083813takashi nq_form = makeNamed name $ quantifyUniversally form

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashirewPredCongPremise _ [] = []

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashirewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi pn = CAS.Qual_pred_name rewID pred_type nullRange

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

af84459fbf938e508fd10b01cb8d699c79083813takashi forms = rewPredsCong ss ts ts'

3c13a815670b54d1c17bf02954f7d2b066cde95cndrewPredsCong _ _ _ = []

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashiloadLibraries ss om = case natImported ss om of

af84459fbf938e508fd10b01cb8d699c79083813takashi False -> []

af84459fbf938e508fd10b01cb8d699c79083813takashi True -> loadNaturalNatSens

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | loads the sentences associated to the natural numbers

af84459fbf938e508fd10b01cb8d699c79083813takashiloadNaturalNatSens :: [Named CAS.CASLFORMULA]

af84459fbf938e508fd10b01cb8d699c79083813takashiloadNaturalNatSens =

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

af84459fbf938e508fd10b01cb8d699c79083813takashi in case lib of

af84459fbf938e508fd10b01cb8d699c79083813takashi G_theory lid _ _ thSens _ -> let sens = toNamedList thSens

af84459fbf938e508fd10b01cb8d699c79083813takashi in do

af84459fbf938e508fd10b01cb8d699c79083813takashi sens' <- coerceSens lid CASL "" sens

af84459fbf938e508fd10b01cb8d699c79083813takashi filter (not . ctorCons) sens'

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | checks if a sentence is an constructor sentence

af84459fbf938e508fd10b01cb8d699c79083813takashictorCons :: Named CAS.CASLFORMULA -> Bool

af84459fbf938e508fd10b01cb8d699c79083813takashictorCons f = case sentence f of

af84459fbf938e508fd10b01cb8d699c79083813takashi CAS.Sort_gen_ax _ _ -> True

af84459fbf938e508fd10b01cb8d699c79083813takashi _ -> False

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | checks if the boolean values are imported

af84459fbf938e508fd10b01cb8d699c79083813takashibooleanImported :: MSign.OpMap -> Bool

af84459fbf938e508fd10b01cb8d699c79083813takashibooleanImported = Map.member (mkSimpleId "if_then_else_fi")

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | checks if the natural numbers are imported

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

af84459fbf938e508fd10b01cb8d699c79083813takashinatImported ss om = b1 && b2 && b3

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi b3 = case b2 of

af84459fbf938e508fd10b01cb8d699c79083813takashi False -> True

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashispecialZeroSet :: MSign.OpDeclSet -> Bool

af84459fbf938e508fd10b01cb8d699c79083813takashispecialZeroSet = Set.fold specialZero False

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashispecialZero :: MSign.OpDecl -> Bool -> Bool

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where b' = isSpecial ats

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashiisSpecial :: [MAS.Attr] -> Bool

af84459fbf938e508fd10b01cb8d699c79083813takashiisSpecial [] = False

af84459fbf938e508fd10b01cb8d699c79083813takashiisSpecial ((MAS.Special _) : _) = True

af84459fbf938e508fd10b01cb8d699c79083813takashiisSpecial (_ : ats) = isSpecial ats

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashideleteUniversal :: MSign.OpMap -> MSign.OpMap

af84459fbf938e508fd10b01cb8d699c79083813takashideleteUniversal om = om5

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

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

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashiuniversalOps kinds om True = Set.fold universalOpKind om kinds

af84459fbf938e508fd10b01cb8d699c79083813takashiuniversalOps _ om False = om

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates the universal operators for a concrete module

af84459fbf938e508fd10b01cb8d699c79083813takashiuniversalOpKind :: Id -> CSign.OpMap -> CSign.OpMap

af84459fbf938e508fd10b01cb8d699c79083813takashiuniversalOpKind kind om = om3

af84459fbf938e508fd10b01cb8d699c79083813takashi where if_id = str2id "if_then_else_fi"

af84459fbf938e508fd10b01cb8d699c79083813takashi double_eq_id = str2id "_==_"

af84459fbf938e508fd10b01cb8d699c79083813takashi neg_double_eq_id = str2id "_=/=_"

af84459fbf938e508fd10b01cb8d699c79083813takashi bool_id = str2id "Bool"

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi om1 = Map.insertWith Set.union if_id if_opt om

af84459fbf938e508fd10b01cb8d699c79083813takashi om2 = Map.insertWith Set.union double_eq_id eq_opt om1

af84459fbf938e508fd10b01cb8d699c79083813takashi om3 = Map.insertWith Set.union neg_double_eq_id eq_opt om2

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates the formulas for the universal operators

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

af84459fbf938e508fd10b01cb8d699c79083813takashiuniversalSens = Set.fold universalSensKind []

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where iss = ifSens kind

af84459fbf938e508fd10b01cb8d699c79083813takashi eqs = equalitySens kind

af84459fbf938e508fd10b01cb8d699c79083813takashi neqs = nonEqualitySens kind

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates the formulas for the if statement

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where v1 = newVarIndex 1 kind

af84459fbf938e508fd10b01cb8d699c79083813takashi v2 = newVarIndex 2 kind

af84459fbf938e508fd10b01cb8d699c79083813takashi bk = str2id "Bool"

af84459fbf938e508fd10b01cb8d699c79083813takashi bv = newVarIndex 2 bk

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi true_term = CAS.Application true_id [] nullRange

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

af84459fbf938e508fd10b01cb8d699c79083813takashi if_name = str2id "if_then_else_fi"

af84459fbf938e508fd10b01cb8d699c79083813takashi if_id = CAS.Qual_op_name if_name if_type nullRange

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

af84459fbf938e508fd10b01cb8d699c79083813takashi prem = CAS.Strong_equation bv true_term nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi concl = CAS.Strong_equation if_term v1 nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Implication prem concl True nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi form' = quantifyUniversally form

af84459fbf938e508fd10b01cb8d699c79083813takashi neg_prem = CAS.Negation prem nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi neg_concl = CAS.Strong_equation if_term v2 nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi neg_form = CAS.Implication neg_prem neg_concl True nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi neg_form' = quantifyUniversally neg_form

af84459fbf938e508fd10b01cb8d699c79083813takashi name1 = show kind ++ "_if_true"

af84459fbf938e508fd10b01cb8d699c79083813takashi name2 = show kind ++ "_if_false"

af84459fbf938e508fd10b01cb8d699c79083813takashi form'' = makeNamed name1 form'

af84459fbf938e508fd10b01cb8d699c79083813takashi neg_form'' = makeNamed name2 neg_form'

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates the formulas for the equality

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

156e9dfbbab272a462dadedda424385a706a8637humbedoohequalitySens kind = [form'', comp_form'']

156e9dfbbab272a462dadedda424385a706a8637humbedooh where v1 = newVarIndex 1 kind

156e9dfbbab272a462dadedda424385a706a8637humbedooh v2 = newVarIndex 2 kind

156e9dfbbab272a462dadedda424385a706a8637humbedooh bk = str2id "Bool"

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

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

156e9dfbbab272a462dadedda424385a706a8637humbedooh true_term = CAS.Application true_id [] nullRange

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

35fe7da687551c1d6e0f62e192f10e39f6a55208rbowen false_term = CAS.Application false_id [] nullRange

156e9dfbbab272a462dadedda424385a706a8637humbedooh prem = CAS.Strong_equation v1 v2 nullRange

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

156e9dfbbab272a462dadedda424385a706a8637humbedooh double_eq_name = str2id "_==_"

156e9dfbbab272a462dadedda424385a706a8637humbedooh double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange

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

156e9dfbbab272a462dadedda424385a706a8637humbedooh concl = CAS.Strong_equation double_eq_term true_term nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Implication prem concl True nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi form' = quantifyUniversally form

af84459fbf938e508fd10b01cb8d699c79083813takashi neg_prem = CAS.Negation prem nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi new_concl = CAS.Strong_equation double_eq_term false_term nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi comp_form = CAS.Implication neg_prem new_concl True nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi comp_form' = quantifyUniversally comp_form

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi form'' = makeNamed name1 form'

af84459fbf938e508fd10b01cb8d699c79083813takashi comp_form'' = makeNamed name2 comp_form'

af84459fbf938e508fd10b01cb8d699c79083813takashi

3c13a815670b54d1c17bf02954f7d2b066cde95cnd-- | generates the formulas for the inequality

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where v1 = newVarIndex 1 kind

af84459fbf938e508fd10b01cb8d699c79083813takashi v2 = newVarIndex 2 kind

af84459fbf938e508fd10b01cb8d699c79083813takashi bk = str2id "Bool"

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi true_term = CAS.Application true_id [] nullRange

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

af84459fbf938e508fd10b01cb8d699c79083813takashi false_term = CAS.Application false_id [] nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi prem = CAS.Strong_equation v1 v2 nullRange

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

af84459fbf938e508fd10b01cb8d699c79083813takashi double_eq_name = str2id "_==_"

af84459fbf938e508fd10b01cb8d699c79083813takashi double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange

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

af84459fbf938e508fd10b01cb8d699c79083813takashi concl = CAS.Strong_equation double_eq_term false_term nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Implication prem concl True nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi form' = quantifyUniversally form

af84459fbf938e508fd10b01cb8d699c79083813takashi neg_prem = CAS.Negation prem nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi new_concl = CAS.Strong_equation double_eq_term true_term nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi comp_form = CAS.Implication neg_prem new_concl True nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi comp_form' = quantifyUniversally comp_form

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi form'' = makeNamed name1 form'

af84459fbf938e508fd10b01cb8d699c79083813takashi comp_form'' = makeNamed name2 comp_form'

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

3c13a815670b54d1c17bf02954f7d2b066cde95cnd-- and the set of sorts with the ctor attribute

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- to introduce the operator in the generators sentence

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where sym = head $ Set.toList syms

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi assoc_ops' = if any MAS.assoc ats

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

af84459fbf938e508fd10b01cb8d699c79083813takashi else assoc_ops

af84459fbf938e508fd10b01cb8d699c79083813takashi cs' = if any MAS.ctor ats

af84459fbf938e508fd10b01cb8d699c79083813takashi then Set.insert (Component cop_id ot) cs

af84459fbf938e508fd10b01cb8d699c79083813takashi else cs

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- and its CASL type

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where f = token2id . getName

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

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

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

156e9dfbbab272a462dadedda424385a706a8637humbedoohmaudeSym2CASLOp _ _ = Nothing

156e9dfbbab272a462dadedda424385a706a8637humbedooh

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

156e9dfbbab272a462dadedda424385a706a8637humbedoohcreateConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA

156e9dfbbab272a462dadedda424385a706a8637humbedoohcreateConjForm [] = CAS.True_atom nullRange

156e9dfbbab272a462dadedda424385a706a8637humbedoohcreateConjForm [a] = a

af84459fbf938e508fd10b01cb8d699c79083813takashicreateConjForm fs = CAS.Conjunction fs nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashicreateImpForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA -> CAS.CASLFORMULA

af84459fbf938e508fd10b01cb8d699c79083813takashicreateImpForm (CAS.True_atom _) form = form

af84459fbf938e508fd10b01cb8d699c79083813takashicreateImpForm form1 form2 = CAS.Implication form1 form2 True nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- the arguments have the correct sort

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where s' = token2id s

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

3c13a815670b54d1c17bf02954f7d2b066cde95cnd pred_type = CAS.Pred_type [kind] nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi pred_name = CAS.Qual_pred_name s' pred_type nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi var = newVarIndex i kind

af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Predication pred_name [var] nullRange

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where k' = token2id k

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

af84459fbf938e508fd10b01cb8d699c79083813takashi var = newVarIndex i kind

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

af84459fbf938e508fd10b01cb8d699c79083813takashiops2predPremises _ _ _ = ([], [])

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashisplitOwiseEqs :: [Named MSentence.Sentence] ->

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

af84459fbf938e508fd10b01cb8d699c79083813takashisplitOwiseEqs [] = ([], [], [])

af84459fbf938e508fd10b01cb8d699c79083813takashisplitOwiseEqs (s : ss) = res

af84459fbf938e508fd10b01cb8d699c79083813takashi where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss

af84459fbf938e508fd10b01cb8d699c79083813takashi sen = sentence s

af84459fbf938e508fd10b01cb8d699c79083813takashi res = case sen of

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

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- a CASL formula

af84459fbf938e508fd10b01cb8d699c79083813takashinoOwiseSen2Formula :: IdMap -> Named MSentence.Sentence

af84459fbf938e508fd10b01cb8d699c79083813takashi -> Named CAS.CASLFORMULA

af84459fbf938e508fd10b01cb8d699c79083813takashinoOwiseSen2Formula im s = s'

4aa603e6448b99f9371397d439795c91a93637eand where MSentence.Equation eq = sentence s

4aa603e6448b99f9371397d439795c91a93637eand sen' = noOwiseEq2Formula im eq

888cb40bdeec5abf452bd85d6bf63b26d5913d4chumbedooh s' = s { sentence = sen' }

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- a CASL formula

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashiowiseSen2Formula im owise_forms s = s'

af84459fbf938e508fd10b01cb8d699c79083813takashi where MSentence.Equation eq = sentence s

af84459fbf938e508fd10b01cb8d699c79083813takashi sen' = owiseEq2Formula im owise_forms eq

af84459fbf938e508fd10b01cb8d699c79083813takashi s' = s { sentence = sen' }

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashimb_rl2formula im s = case sen of

af84459fbf938e508fd10b01cb8d699c79083813takashi MSentence.Membership mb -> let

af84459fbf938e508fd10b01cb8d699c79083813takashi mb' = mb2formula im mb

af84459fbf938e508fd10b01cb8d699c79083813takashi in s { sentence = mb' }

af84459fbf938e508fd10b01cb8d699c79083813takashi MSentence.Rule rl -> let

af84459fbf938e508fd10b01cb8d699c79083813takashi rl' = rl2formula im rl

af84459fbf938e508fd10b01cb8d699c79083813takashi in s { sentence = rl' }

3c13a815670b54d1c17bf02954f7d2b066cde95cnd _ -> makeNamed "" $ CAS.False_atom nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi where sen = sentence s

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

3c13a815670b54d1c17bf02954f7d2b066cde95cndnewVarIndex :: Int -> Id -> CAS.CASLTERM

af84459fbf938e508fd10b01cb8d699c79083813takashinewVarIndex i sort = CAS.Qual_var var sort nullRange

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates a new variable

af84459fbf938e508fd10b01cb8d699c79083813takashinewVar :: Id -> CAS.CASLTERM

af84459fbf938e508fd10b01cb8d699c79083813takashinewVar sort = CAS.Qual_var var sort nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi where var = mkSimpleId "V"

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | Id for the rew predicate

af84459fbf938e508fd10b01cb8d699c79083813takashirewID :: Id

af84459fbf938e508fd10b01cb8d699c79083813takashirewID = token2id $ mkSimpleId "rew"

3c13a815670b54d1c17bf02954f7d2b066cde95cnd

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

3c13a815670b54d1c17bf02954f7d2b066cde95cndnoOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where ct = maudeTerm2caslTerm im t

af84459fbf938e508fd10b01cb8d699c79083813takashi ct' = maudeTerm2caslTerm im t'

3c13a815670b54d1c17bf02954f7d2b066cde95cnd form = CAS.Strong_equation ct ct' nullRange

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where ct = maudeTerm2caslTerm im t

af84459fbf938e508fd10b01cb8d699c79083813takashi ct' = maudeTerm2caslTerm im t'

af84459fbf938e508fd10b01cb8d699c79083813takashi conds_form = conds2formula im conds

af84459fbf938e508fd10b01cb8d699c79083813takashi concl_form = CAS.Strong_equation ct ct' nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi form = createImpForm conds_form concl_form

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- a CASL formula

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

af84459fbf938e508fd10b01cb8d699c79083813takashi -> CAS.CASLFORMULA

af84459fbf938e508fd10b01cb8d699c79083813takashiowiseEq2Formula im no_owise_form eq = form

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi ex_form = existencialNegationOtherEqs op ts no_owise_form

af84459fbf938e508fd10b01cb8d699c79083813takashi imp_form = createImpForm ex_form eq_form

af84459fbf938e508fd10b01cb8d699c79083813takashi form = CAS.Quantification CAS.Universal vars imp_form nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi

af84459fbf938e508fd10b01cb8d699c79083813takashi-- | generates a conjunction of negation of existencial quantifiers

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

af84459fbf938e508fd10b01cb8d699c79083813takashi [Named CAS.CASLFORMULA] -> CAS.CASLFORMULA

af84459fbf938e508fd10b01cb8d699c79083813takashiexistencialNegationOtherEqs op ts forms = form

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

af84459fbf938e508fd10b01cb8d699c79083813takashi form = if length ex_forms > 1

af84459fbf938e508fd10b01cb8d699c79083813takashi then CAS.Conjunction ex_forms nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi else head ex_forms

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi Named CAS.CASLFORMULA -> [CAS.CASLFORMULA]

af84459fbf938e508fd10b01cb8d699c79083813takashiexistencialNegationOtherEq req_op terms form = case ok of

af84459fbf938e508fd10b01cb8d699c79083813takashi False -> []

af84459fbf938e508fd10b01cb8d699c79083813takashi True -> let

af84459fbf938e508fd10b01cb8d699c79083813takashi (_, ts, conds) = fromJust tpl

156e9dfbbab272a462dadedda424385a706a8637humbedooh ts' = qualifyExVarsTerms ts

156e9dfbbab272a462dadedda424385a706a8637humbedooh conds' = qualifyExVarsForms conds

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

af84459fbf938e508fd10b01cb8d699c79083813takashi conj_form = CAS.Conjunction prems nullRange

af84459fbf938e508fd10b01cb8d699c79083813takashi ex_form = if vars' /= []

156e9dfbbab272a462dadedda424385a706a8637humbedooh then CAS.Quantification CAS.Existential vars' conj_form nullRange

156e9dfbbab272a462dadedda424385a706a8637humbedooh else conj_form

156e9dfbbab272a462dadedda424385a706a8637humbedooh neg_form = CAS.Negation ex_form nullRange

156e9dfbbab272a462dadedda424385a706a8637humbedooh in [neg_form]

af84459fbf938e508fd10b01cb8d699c79083813takashi where (inner_form, vars) = noQuantification $ sentence form

af84459fbf938e508fd10b01cb8d699c79083813takashi vars' = qualifyExVars vars

af84459fbf938e508fd10b01cb8d699c79083813takashi tpl = getLeftApp inner_form

af84459fbf938e508fd10b01cb8d699c79083813takashi ok = case tpl of

af84459fbf938e508fd10b01cb8d699c79083813takashi Nothing -> False

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

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

3c13a815670b54d1c17bf02954f7d2b066cde95cnd

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- distinguish them from the variables already bound

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

af84459fbf938e508fd10b01cb8d699c79083813takashiqualifyExVarsForms = map qualifyExVarsForm

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- from the variables already bound

af84459fbf938e508fd10b01cb8d699c79083813takashiqualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where qt = qualifyExVarsTerm t

af84459fbf938e508fd10b01cb8d699c79083813takashi qt' = qualifyExVarsTerm t'

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where ts' = qualifyExVarsTerms ts

af84459fbf938e508fd10b01cb8d699c79083813takashiqualifyExVarsForm f = f

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- distinguish them from the variables already bound

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

af84459fbf938e508fd10b01cb8d699c79083813takashiqualifyExVarsTerms = map qualifyExVarsTerm

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- from the variables already bound

3c13a815670b54d1c17bf02954f7d2b066cde95cndqualifyExVarsTerm :: CAS.CASLTERM -> CAS.CASLTERM

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where ts' = map qualifyExVarsTerm ts

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

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

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where t1' = qualifyExVarsTerm t1

af84459fbf938e508fd10b01cb8d699c79083813takashi t2' = qualifyExVarsTerm t2

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where ts' = map qualifyExVarsTerm ts

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where ts' = map qualifyExVarsTerm ts

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where ts' = map qualifyExVarsTerm ts

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where ts' = map qualifyExVarsTerm ts

af84459fbf938e508fd10b01cb8d699c79083813takashiqualifyExVarsTerm t = t

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- distinguish them from the variables already bound

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

af84459fbf938e508fd10b01cb8d699c79083813takashiqualifyExVars = map qualifyExVar

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashi-- the variables already bound

af84459fbf938e508fd10b01cb8d699c79083813takashiqualifyExVar :: CAS.VAR_DECL -> CAS.VAR_DECL

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

af84459fbf938e508fd10b01cb8d699c79083813takashi where vars' = map qualifyExVarAux vars

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

af84459fbf938e508fd10b01cb8d699c79083813takashiqualifyExVarAux :: Token -> Token

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

af84459fbf938e508fd10b01cb8d699c79083813takashi

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

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

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

0d0ba3a410038e179b695446bb149cce6264e0abnd where ls = createEqs ts1 ts2

727872d18412fc021f03969b8641810d8896820bhumbedoohcreateEqs _ _ = []

cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh

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

cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh-- in a strong equation

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

0d0ba3a410038e179b695446bb149cce6264e0abndgetLeftApp (CAS.Strong_equation term _ _) = case getLeftAppTerm term of

0d0ba3a410038e179b695446bb149cce6264e0abnd Nothing -> Nothing

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

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

0d0ba3a410038e179b695446bb149cce6264e0abnd Nothing -> Nothing

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

0d0ba3a410038e179b695446bb149cce6264e0abnd where conds = getPremisesImplication prem

727872d18412fc021f03969b8641810d8896820bhumbedoohgetLeftApp _ = Nothing

0d0ba3a410038e179b695446bb149cce6264e0abnd

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

30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh-- in an application term

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

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

0d0ba3a410038e179b695446bb149cce6264e0abndgetLeftAppTerm _ = Nothing

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd

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

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd-- a conjunction or not

af84459fbf938e508fd10b01cb8d699c79083813takashigetPremisesImplication :: 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