{- |
Module : ./Maude/PreComorphism.hs
Description : Maude Comorphisms
Copyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009
License : GPLv2 or higher, see LICENSE.txt
Maintainer : ariesco@fdi.ucm.es
Stability : experimental
Portability : portable
Comorphism from Maude to CASL.
-}
module Maude.PreComorphism where
import Data.Maybe
import qualified Data.List as List
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Maude.Sign as MSign
import qualified Maude.Sentence as MSentence
import qualified Maude.Morphism as MMorphism
import qualified Maude.AS_Maude as MAS
import qualified Maude.Symbol as MSym
import Maude.Meta.HasName
import qualified CASL.Sign as CSign
import qualified CASL.Morphism as CMorphism
import qualified CASL.AS_Basic_CASL as CAS
import CASL.StaticAna
import Common.Id
import Common.Result
import Common.AS_Annotation
import Common.ProofUtils (charMap)
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet
type IdMap = Map.Map Id Id
-- | generates a CASL morphism from a Maude morphism
mapMorphism :: MMorphism.Morphism -> Result CMorphism.CASLMor
mapMorphism morph =
let
src = MMorphism.source morph
tgt = MMorphism.target morph
mk = kindMapId $ MSign.kindRel src
mk' = kindMapId $ MSign.kindRel tgt
smap = MMorphism.sortMap morph
omap = MMorphism.opMap morph
smap' = applySortMap2CASLSorts smap mk mk'
omap' = maudeOpMap2CASLOpMap mk omap
pmap = createPredMap mk smap
(src', _) = maude2casl src []
(tgt', _) = maude2casl tgt []
in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()
{- | translates the Maude morphism between operators into a CASL morpshim
between operators -}
maudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map
maudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty
{- | translates the mapping between two symbols representing operators into
a CASL operators map -}
translateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm
= copm'
where f = token2id . getName
g x = Map.findWithDefault (errorId "translate op map entry")
(f x) im
ot = CSign.OpType CAS.Total (map g ar) (g co)
cop = (token2id from, ot)
to' = (token2id to, CAS.Total)
copm' = Map.insert cop to' copm
translateOpMapEntry _ _ _ _ = Map.empty
-- | generates a set of CASL symbol from a Maude Symbol
mapSymbol sg (MSym.Sort q) = Set.singleton csym
where mk = kindMapId $ MSign.kindRel sg
sym_id = token2id q
kind = Map.findWithDefault (errorId "map symbol") sym_id mk
pred_data = CSign.PredType [kind]
csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data
mapSymbol sg (MSym.Operator q ar co) = Set.singleton csym
where mk = kindMapId $ MSign.kindRel sg
q' = token2id q
ar' = map (maudeSort2caslId mk) ar
co' = token2id $ getName co
op_data = CSign.OpType CAS.Total ar' co'
csym = CSign.Symbol q' $ CSign.OpAsItemType op_data
mapSymbol _ _ = Set.empty
-- | returns the sort in CASL of the Maude sort symbol
maudeSort2caslId :: IdMap -> MSym.Symbol -> Id
maudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id")
(token2id $ getName sym) im
{- | creates the predicate map for the CASL morphism from the Maude sort map and
the map between sorts and kinds -}
createPredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map
createPredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty
-- | creates an entry of the predicate map for a single sort
createPredMap4sort im from to = Map.insert key id_to
where id_from = token2id $ getName from
id_to = token2id $ getName to
kind = Map.findWithDefault (errorId "predicate for sort")
id_from im
key = (id_from, CSign.PredType [kind])
{- | computes the sort morphism of CASL from the sort morphism in Maude
and the set of kinds -}
applySortMap2CASLSorts :: MMorphism.SortMap -> IdMap -> IdMap
applySortMap2CASLSorts sm im im' = Map.fromList sml'
where sml = Map.toList sm
sml' = foldr (applySortMap2CASLSort im im') [] sml
-- | computes the morphism for a single sort pair
applySortMap2CASLSort :: IdMap -> IdMap -> (MSym.Symbol, MSym.Symbol)
-> [(Id, Id)] -> [(Id, Id)]
applySortMap2CASLSort im im' (s1, s2) l = l'
where p1 = (mSym2caslId s1, mSym2caslId s2)
f x = Map.findWithDefault
(errorId $ "err" ++ show (mSym2caslId x)) (mSym2caslId x)
p2 = (f s1 im, f s2 im')
l' = p1 : if s1 == s2
then l else p2 : l
-- | renames the sorts in a given kind
rename :: MMorphism.SortMap -> Token -> Token
rename sm tok = new_tok
where sym = MSym.Sort tok
sym' = if Map.member sym sm
then fromJust $ Map.lookup sym sm
else sym
new_tok = getName sym'
-- | translates a Maude sentence into a CASL formula
mapSentence sg sen = let
mk = kindMapId $ MSign.kindRel sg
named = makeNamed "" sen
form = mb_rl2formula mk named
in return $ sentence $ case sen of
sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg
(no_owise_sens, _, _) = splitOwiseEqs sg_sens
no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
in owiseSen2Formula mk no_owise_forms named
else noOwiseSen2Formula mk named
MSentence.Membership (MAS.Mb {}) -> form
MSentence.Rule (MAS.Rl {}) -> form
{- | applies maude2casl to compute the CASL signature and sentences from
the Maude ones, and wraps them into a Result datatype -}
mapTheory :: (MSign.Sign, [Named MSentence.Sentence])
-> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])
mapTheory (sg, nsens) = return $ maude2casl sg nsens
{- | computes new signature and sentences of CASL associated to the
given Maude signature and sentences -}
maude2casl :: MSign.Sign -> [Named MSentence.Sentence]
-> (CSign.CASLSign, [Named CAS.CASLFORMULA])
maude2casl msign nsens = (csign {
Rel.union (Rel.fromKeysSet cs) sbs',
CSign.opMap = cops',
CSign.assocOps = assoc_ops,
CSign.predMap = preds,
CSign.declaredSymbols = syms }, new_sens)
where csign = CSign.emptySign ()
ss = MSign.sorts msign
ss' = Set.map sym2id ss
mk = kindMapId $ MSign.kindRel msign
sbs = MSign.subsorts msign
sbs' = maudeSbs2caslSbs sbs mk
cs = Set.union ss' $ kindsFromMap mk
preds = rewPredicates cs
rs = rewPredicatesSens cs
ops = deleteUniversal $ MSign.ops msign
ksyms = kinds2syms cs
(cops, assoc_ops, _) = translateOps mk ops -- (cops, assoc_ops, comps)
axSens = axiomsSens mk ops
ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]
cops' = universalOps cs cops $ booleanImported ops
rs' = rewPredicatesCongSens cops'
pred_forms = loadLibraries (MSign.sorts msign) ops
ops_syms = ops2symbols cops'
(no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens
no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens
mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens
preds_syms = preds2syms preds
new_sens = concat [rs, rs', no_owise_forms, owise_forms,
mb_rl_forms, ctor_sen, pred_forms, axSens]
{- | translates the Maude subsorts into CASL subsorts, and adds the subsorts
for the kinds -}
maudeSbs2caslSbs sbs im = Rel.fromMap m4
where l = Map.toList $ Rel.toMap sbs
l1 = [] -- map maudeSb2caslSb l
l2 = idList2Subsorts $ Map.toList im
l3 = map subsorts2Ids l
m1 = Map.fromList l1
m2 = Map.fromList l2
m3 = Map.fromList l3
idList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]
idList2Subsorts [] = []
idList2Subsorts ((id1, id2) : il) = t1 : idList2Subsorts il
where t1 = (id1, Set.singleton id2)
maudeSb2caslSb (sym, st) = (sortSym2id sym, Set.map (kindId . sortSym2id) st)
subsorts2Ids (sym, st) = (sortSym2id sym, Set.map sortSym2id st)
sortSym2id :: MSym.Symbol -> Id
sortSym2id (MSym.Sort q) = token2id q
sortSym2id _ = token2id $ mkSimpleId "error_translation"
-- | generates the sentences to state that the rew predicates are a congruence
rewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]
rewPredicatesCongSens = MapSet.foldWithKey rewPredCong []
{- | generates the sentences to state that the rew predicates are a congruence
for a single operator -}
rewPredCong :: Id -> CSign.OpType -> [Named CAS.CASLFORMULA]
-> [Named CAS.CASLFORMULA]
rewPredCong op ot fs = case args of
[] -> fs
_ -> nq_form : fs
where args = CSign.opArgs ot
vars1 = rewPredCongPremise 0 args
vars2 = rewPredCongPremise (length args) args
res = CSign.opRes ot
res_pred_type = CAS.Pred_type [res, res] nullRange
pn = CAS.Qual_pred_name rewID res_pred_type nullRange
name = "rew_cong_" ++ show op
prems = rewPredsCong args vars1 vars2
prems_conj = createConjForm prems
os = CAS.Qual_op_name op (CSign.toOP_TYPE ot) nullRange
conc_term1 = CAS.Application os vars1 nullRange
conc_term2 = CAS.Application os vars2 nullRange
conc_form = CAS.Predication pn [conc_term1, conc_term2] nullRange
form = createImpForm prems_conj conc_form
nq_form = makeNamed name $ quantifyUniversally form
-- | generates a list of variables of the given sorts
rewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]
rewPredCongPremise n (s : ss) = newVarIndex n s : rewPredCongPremise (n + 1) ss
rewPredCongPremise _ [] = []
-- | generates a list of rew predicates with the given variables
-> [CAS.CASLFORMULA]
rewPredsCong (s : ss) (t : ts) (t' : ts') = form : forms
where pred_type = CAS.Pred_type [s, s] nullRange
pn = CAS.Qual_pred_name rewID pred_type nullRange
form = CAS.Predication pn [t, t'] nullRange
forms = rewPredsCong ss ts ts'
rewPredsCong _ _ _ = []
-- | load the CASL libraries for the Maude built-in operators
loadLibraries ss om = if natImported ss om then loadNaturalNatSens else []
-- | loads the sentences associated to the natural numbers
loadNaturalNatSens :: [Named CAS.CASLFORMULA]
loadNaturalNatSens = [] -- retrieve code from Rev 17944 if needed again!
-- | checks if a sentence is an constructor sentence
ctorCons :: Named CAS.CASLFORMULA -> Bool
ctorCons f = case sentence f of
CAS.Sort_gen_ax _ _ -> True
_ -> False
-- | checks if the boolean values are imported
booleanImported :: MSign.OpMap -> Bool
booleanImported = Map.member (mkSimpleId "if_then_else_fi")
-- | checks if the natural numbers are imported
natImported :: MSign.SortSet -> MSign.OpMap -> Bool
natImported ss om = b1 && b2 && b3
where b1 = Set.member (MSym.Sort $ mkSimpleId "Nat") ss
b2 = Map.member (mkSimpleId "s_") om
b3 = not b2 || 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 kinds om True = Set.fold universalOpKind om kinds
universalOps _ om False = om
-- | generates the universal operators for a concrete module
universalOpKind :: Id -> CSign.OpMap -> CSign.OpMap
universalOpKind kind = MapSet.union $ MapSet.fromList
[ (if_id, [if_opt]), (double_eq_id, [eq_opt]), (neg_double_eq_id, [eq_opt]) ]
where if_id = str2id "if_then_else_fi"
double_eq_id = str2id "_==_"
neg_double_eq_id = str2id "_=/=_"
bool_id = str2id "Bool"
if_opt = CSign.OpType CAS.Total [bool_id, kind, kind] kind
eq_opt = CSign.OpType CAS.Total [kind, kind] bool_id
-- | generates the formulas for the universal operators
universalSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
universalSens = Set.fold universalSensKind []
-- | generates the formulas for the universal operators for the given sort
universalSensKind :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
universalSensKind kind acc = concat [iss, eqs, neqs, acc]
where iss = ifSens kind
eqs = equalitySens kind
neqs = nonEqualitySens kind
-- | generates the formulas for the if statement
ifSens :: Id -> [Named CAS.CASLFORMULA]
ifSens kind = [form'', neg_form'']
where v1 = newVarIndex 1 kind
v2 = newVarIndex 2 kind
bk = str2id "Bool"
bv = newVarIndex 2 bk
true_type = CAS.Op_type CAS.Total [] bk nullRange
true_id = CAS.Qual_op_name (str2id "true") true_type nullRange
true_term = CAS.Application true_id [] nullRange
if_type = CAS.Op_type CAS.Total [bk, kind, kind] kind nullRange
if_name = str2id "if_then_else_fi"
if_id = CAS.Qual_op_name if_name if_type nullRange
if_term = CAS.Application if_id [bv, v1, v2] nullRange
prem = CAS.mkStEq bv true_term
concl = CAS.mkStEq if_term v1
form = CAS.mkImpl prem concl
form' = quantifyUniversally form
neg_prem = CAS.Negation prem nullRange
neg_concl = CAS.mkStEq if_term v2
neg_form = CAS.mkImpl neg_prem neg_concl
neg_form' = quantifyUniversally neg_form
name1 = show kind ++ "_if_true"
name2 = show kind ++ "_if_false"
form'' = makeNamed name1 form'
neg_form'' = makeNamed name2 neg_form'
-- | generates the formulas for the equality
equalitySens :: Id -> [Named CAS.CASLFORMULA]
equalitySens kind = [form'', comp_form'']
where v1 = newVarIndex 1 kind
v2 = newVarIndex 2 kind
bk = str2id "Bool"
b_type = CAS.Op_type CAS.Total [] bk nullRange
true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
true_term = CAS.Application true_id [] nullRange
false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
false_term = CAS.Application false_id [] nullRange
prem = CAS.mkStEq v1 v2
double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind
nullRange
double_eq_name = str2id "_==_"
double_eq_id = CAS.mkQualOp double_eq_name double_eq_type
double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
concl = CAS.mkStEq double_eq_term true_term
form = CAS.mkImpl prem concl
form' = quantifyUniversally form
neg_prem = CAS.Negation prem nullRange
new_concl = CAS.mkStEq double_eq_term false_term
comp_form = CAS.mkImpl neg_prem new_concl
comp_form' = quantifyUniversally comp_form
name1 = show kind ++ "_==_true"
name2 = show kind ++ "_==_false"
form'' = makeNamed name1 form'
comp_form'' = makeNamed name2 comp_form'
-- | generates the formulas for the inequality
nonEqualitySens :: Id -> [Named CAS.CASLFORMULA]
nonEqualitySens kind = [form'', comp_form'']
where v1 = newVarIndex 1 kind
v2 = newVarIndex 2 kind
bk = str2id "Bool"
b_type = CAS.Op_type CAS.Total [] bk nullRange
true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
true_term = CAS.Application true_id [] nullRange
false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
false_term = CAS.Application false_id [] nullRange
prem = CAS.mkStEq v1 v2
double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind
nullRange
double_eq_name = str2id "_==_"
double_eq_id = CAS.mkQualOp double_eq_name double_eq_type
double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
concl = CAS.mkStEq double_eq_term false_term
form = CAS.mkImpl prem concl
form' = quantifyUniversally form
neg_prem = CAS.Negation prem nullRange
new_concl = CAS.mkStEq double_eq_term true_term
comp_form = CAS.mkImpl neg_prem new_concl
comp_form' = quantifyUniversally comp_form
name1 = show kind ++ "_=/=_false"
name2 = show kind ++ "_=/=_true"
form'' = makeNamed name1 form'
comp_form'' = makeNamed name2 comp_form'
-- | generates the sentences for the operator attributes
axiomsSens :: IdMap -> MSign.OpMap -> [Named CAS.CASLFORMULA]
axiomsSens im = Map.fold (axiomsSensODS im) []
axiomsSensODS :: IdMap -> MSign.OpDeclSet -> [Named CAS.CASLFORMULA]
-> [Named CAS.CASLFORMULA]
axiomsSensODS im ods l = Set.fold (axiomsSensOD im) l ods
axiomsSensOD :: IdMap -> MSign.OpDecl -> [Named CAS.CASLFORMULA]
-> [Named CAS.CASLFORMULA]
axiomsSensOD im (ss, ats) l = Set.fold (axiomsSensSS im ats) l ss
-> [Named CAS.CASLFORMULA]
axiomsSensSS im ats (MSym.Operator q ar co) l = l ++ l1
where l1 = if elem MAS.Comm ats
then commSen im q ar co
else []
axiomsSensSS _ _ _ l = l
-> [Named CAS.CASLFORMULA]
commSen im q ar@[ar1, ar2] co = [form']
where q' = token2id q
f = (`maudeSymbol2caslSort` im)
ar1' = f ar1
ar2' = f ar2
ot = CAS.Op_type CAS.Total (map f ar) (f co) nullRange
os = CAS.Qual_op_name q' ot nullRange
v1 = newVarIndex 1 ar1'
v2 = newVarIndex 2 ar2'
t1 = CAS.Application os [v1, v2] nullRange
t2 = CAS.Application os [v2, v1] nullRange
form = CAS.mkStEq t1 t2
name = "comm_" ++ ms2vcs (show q') ++ "_" ++ show ar1'
form' = makeNamed name $ quantifyUniversally form
commSen _ _ _ _ = []
-- (newVarIndex 1 (hd ar))
-- maudeSymbol2caslSort x im
{- | translates the Maude operator map into a tuple of CASL operators, CASL
associative operators, membership induced from each Maude operator,
and the set of sorts with the ctor attribute -}
translateOps :: IdMap -> MSign.OpMap -> OpTransTuple
translateOps im = Map.fold (translateOpDeclSet im)
-- | translates an operator declaration set into a tern as described above
translateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
translateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods
{- | given an operator declaration updates the accumulator with the translation
to CASL operator, checking if the operator has the assoc attribute to insert
it in the map of associative operators, generating the membership predicate
induced by the operator declaration, and checking if it has the ctor
attribute to introduce the operator in the generators sentence -}
translateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
translateOpDecl im (syms, ats) (ops, assoc_ops, cs) = case tl of
[] -> (ops', assoc_ops', cs')
_ -> translateOpDecl im (syms', ats) (ops', assoc_ops', cs')
where sym : tl = Set.toList syms
syms' = Set.fromList tl
(cop_id, ot, _) = fromJust $ maudeSym2CASLOp im sym
ops' = MapSet.insert cop_id ot ops
assoc_ops' = if any MAS.assoc ats
then MapSet.insert cop_id ot assoc_ops
else assoc_ops
cs' = if any MAS.ctor ats
then Set.insert (Component cop_id ot) cs
else cs
{- | translates a Maude operator symbol into a pair with the id of the operator
and its CASL type -}
maudeSym2CASLOp :: IdMap -> MSym.Symbol
-> Maybe (Id, CSign.OpType, CSign.OpType)
maudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot, ot')
where f = token2id . getName
g = (`maudeSymbol2caslSort` im)
ot = CSign.OpType CAS.Total (map g ar) (g co)
ot' = CSign.OpType CAS.Total (map f ar) (f co)
maudeSym2CASLOp _ _ = Nothing
-- | creates a conjuctive formula distinguishing the size of the list
createConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA
createConjForm = CAS.conjunct
-- | creates a implication formula distinguishing the size of the premises
createImpForm (CAS.Atom True _) form = form
createImpForm form1 form2 = CAS.mkImpl form1 form2
{- | generates the predicates asserting the "true" sort of the operator if all
the arguments have the correct sort -}
ops2predPremises :: IdMap -> [MSym.Symbol] -> Int
-> ([CAS.CASLTERM], [CAS.CASLFORMULA])
ops2predPremises im (MSym.Sort s : ss) i = (var : terms, form : forms)
where s' = token2id s
kind = Map.findWithDefault (errorId "mb of op as predicate")
s' im
pred_type = CAS.Pred_type [kind] nullRange
pred_name = CAS.Qual_pred_name s' pred_type nullRange
var = newVarIndex i kind
form = CAS.Predication pred_name [var] nullRange
(terms, forms) = ops2predPremises im ss (i + 1)
ops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)
where k' = token2id k
kind = Map.findWithDefault (errorId "mb of op as predicate")
k' im
var = newVarIndex i kind
(terms, forms) = ops2predPremises im ss (i + 1)
ops2predPremises _ _ _ = ([], [])
{- | traverses the Maude sentences, returning a pair of list of sentences.
The first list in the pair are the equations without the attribute "owise",
while the second one are the equations with this attribute -}
splitOwiseEqs :: [Named MSentence.Sentence] -> ([Named MSentence.Sentence]
, [Named MSentence.Sentence], [Named MSentence.Sentence])
splitOwiseEqs [] = ([], [], [])
splitOwiseEqs (s : ss) = res
where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss
sen = sentence s
res = case sen of
MSentence.Equation (MAS.Eq _ _ _ ats) ->
if any MAS.owise ats
then (no_owise_sens, s : owise_sens, mbs_rls)
else (s : no_owise_sens, owise_sens, mbs_rls)
_ -> (no_owise_sens, owise_sens, s : mbs_rls)
{- | translates a Maude equation defined without the "owise" attribute into
a CASL formula -}
noOwiseSen2Formula :: IdMap -> Named MSentence.Sentence
-> Named CAS.CASLFORMULA
noOwiseSen2Formula im s = s'
where MSentence.Equation eq = sentence s
sen' = noOwiseEq2Formula im eq
s' = s { sentence = sen' }
{- | translates a Maude equation defined with the "owise" attribute into
a CASL formula -}
owiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]
-> Named MSentence.Sentence -> Named CAS.CASLFORMULA
owiseSen2Formula im owise_forms s = s'
where MSentence.Equation eq = sentence s
sen' = owiseEq2Formula im owise_forms eq
s' = s { sentence = sen' }
-- | translates a Maude membership or rule into a CASL formula
mb_rl2formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
mb_rl2formula im s = case sen of
MSentence.Membership mb -> let
mb' = mb2formula im mb
in s { sentence = mb' }
MSentence.Rule rl -> let
rl' = rl2formula im rl
in s { sentence = rl' }
_ -> makeNamed "" CAS.falseForm
where sen = sentence s
-- | generates a new variable qualified with the given number
newVarIndex :: Int -> Id -> CAS.CASLTERM
newVarIndex i sort = CAS.Qual_var var sort nullRange
where var = mkSimpleId $ 'V' : show i
-- | generates a new variable
newVar :: Id -> CAS.CASLTERM
newVar sort = CAS.Qual_var var sort nullRange
where var = mkSimpleId "V"
-- | Id for the rew predicate
rewID :: Id
rewID = token2id $ mkSimpleId "rew"
{- | translates a Maude equation without the "owise" attribute into a CASL
formula -}
noOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA
noOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally form
where ct = maudeTerm2caslTerm im t
ct' = maudeTerm2caslTerm im t'
form = CAS.mkStEq ct ct'
noOwiseEq2Formula im (MAS.Eq t t' conds@(_ : _) _) = quantifyUniversally form
where ct = maudeTerm2caslTerm im t
ct' = maudeTerm2caslTerm im t'
conds_form = conds2formula im conds
concl_form = CAS.mkStEq ct ct'
form = createImpForm conds_form concl_form
{- | transforms a Maude equation defined with the otherwise attribute into
a CASL formula -}
owiseEq2Formula :: IdMap -> [Named CAS.CASLFORMULA] -> MAS.Equation
owiseEq2Formula im no_owise_form eq = form
where (eq_form, vars) = noQuantification $ noOwiseEq2Formula im eq
(op, ts, _) = fromJust $ getLeftApp eq_form
ex_form = existencialNegationOtherEqs op ts no_owise_form
imp_form = createImpForm ex_form eq_form
form = CAS.mkForall vars imp_form
-- | generates a conjunction of negation of existencial quantifiers
existencialNegationOtherEqs :: CAS.OP_SYMB -> [CAS.CASLTERM] ->
[Named CAS.CASLFORMULA] -> CAS.CASLFORMULA
existencialNegationOtherEqs op ts forms = form
where ex_forms = concatMap (existencialNegationOtherEq op ts) forms
form = CAS.conjunct ex_forms
{- | given a formula, if it refers to the same operator indicated by the
parameters the predicate creates a list with the negation of the existence of
variables that match the pattern described in the formula. In other case it
returns an empty list -}
existencialNegationOtherEq :: CAS.OP_SYMB -> [CAS.CASLTERM]
-> Named CAS.CASLFORMULA -> [CAS.CASLFORMULA]
existencialNegationOtherEq req_op terms form = if ok then let
(_, ts, conds) = fromJust tpl
ts' = qualifyExVarsTerms ts
conds' = qualifyExVarsForms conds
prems = createEqs ts' terms ++ conds'
conj_form = CAS.conjunct prems
ex_form = if null vars' then conj_form else
CAS.mkExist vars' conj_form
neg_form = CAS.mkNeg ex_form
in [neg_form]
else []
where (inner_form, vars) = noQuantification $ sentence form
vars' = qualifyExVars vars
tpl = getLeftApp inner_form
ok = case tpl of
Nothing -> False
Just _ -> let (op, ts, _) = fromJust tpl
in req_op == op && length terms == length ts
{- | qualifies the variables in a list of formulas with the suffix "_ex" to
distinguish them from the variables already bound -}
qualifyExVarsForms :: [CAS.CASLFORMULA] -> [CAS.CASLFORMULA]
qualifyExVarsForms = map qualifyExVarsForm
{- | qualifies the variables in a formula with the suffix "_ex" to distinguish
them from the variables already bound -}
qualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA
qualifyExVarsForm (CAS.Equation t CAS.Strong t' r) =
CAS.Equation qt CAS.Strong qt' r
where qt = qualifyExVarsTerm t
qt' = qualifyExVarsTerm t'
qualifyExVarsForm (CAS.Predication op ts r) = CAS.Predication op ts' r
where ts' = qualifyExVarsTerms ts
qualifyExVarsForm f = f
{- | qualifies the variables in a list of terms with the suffix "_ex" to
distinguish them from the variables already bound -}
qualifyExVarsTerms :: [CAS.CASLTERM] -> [CAS.CASLTERM]
qualifyExVarsTerms = map qualifyExVarsTerm
{- | qualifies the variables in a term with the suffix "_ex" to distinguish them
from the variables already bound -}
qualifyExVarsTerm :: CAS.CASLTERM -> CAS.CASLTERM
qualifyExVarsTerm (CAS.Qual_var var sort r) =
CAS.Qual_var (qualifyExVarAux var) sort r
qualifyExVarsTerm (CAS.Application op ts r) = CAS.Application op ts' r
where ts' = map qualifyExVarsTerm ts
qualifyExVarsTerm (CAS.Sorted_term t s r) =
CAS.Sorted_term (qualifyExVarsTerm t) s r
qualifyExVarsTerm (CAS.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 (t1 : ts1) (t2 : ts2) = CAS.mkStEq t1 t2 : ls
where ls = createEqs ts1 ts2
createEqs _ _ = []
{- | extracts the operator at the top and the arguments of the lefthand side
in a strong equation -}
getLeftApp :: CAS.CASLFORMULA
getLeftApp (CAS.Equation term CAS.Strong _ _) = case getLeftAppTerm term of
Nothing -> Nothing
Just (op, ts) -> Just (op, ts, [])
getLeftApp (CAS.Relation prem c concl _) = case getLeftApp concl of
Just (op, ts, _) | c /= CAS.Equivalence -> Just (op, ts, conds)
where conds = getPremisesImplication prem
_ -> Nothing
getLeftApp _ = Nothing
{- | extracts the operator at the top and the arguments of the lefthand side
in an application term -}
getLeftAppTerm (CAS.Application op ts _) = Just (op, ts)
getLeftAppTerm _ = Nothing
{- | extracts the formulas of the given premise, distinguishing whether it is
a conjunction or not -}
getPremisesImplication :: CAS.CASLFORMULA -> [CAS.CASLFORMULA]
getPremisesImplication (CAS.Junction CAS.Con forms _) =
concatMap getPremisesImplication forms
getPremisesImplication form = [form]
-- | translate a Maude membership into a CASL formula
mb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA
mb2formula im (MAS.Mb t s [] _) = quantifyUniversally form
where ct = maudeTerm2caslTerm im t
s' = token2id $ getName s
form = CAS.Membership ct s' nullRange
mb2formula im (MAS.Mb t s conds@(_ : _) _) = quantifyUniversally form
where ct = maudeTerm2caslTerm im t
s' = token2id $ getName s
conds_form = conds2formula im conds
concl_form = CAS.Membership ct s' nullRange
form = CAS.mkImpl conds_form concl_form
-- | translate a Maude rule into a CASL formula
rl2formula :: IdMap -> MAS.Rule -> CAS.CASLFORMULA
rl2formula im (MAS.Rl t t' [] _) = quantifyUniversally form
where ty = token2id $ getName $ MAS.getTermType t
kind = Map.findWithDefault (errorId "rl to formula") ty im
pred_type = CAS.Pred_type [kind, kind] nullRange
pred_name = CAS.Qual_pred_name rewID pred_type nullRange
ct = maudeTerm2caslTerm im t
ct' = maudeTerm2caslTerm im t'
form = CAS.Predication pred_name [ct, ct'] nullRange
rl2formula im (MAS.Rl t t' conds@(_ : _) _) = quantifyUniversally form
where ty = token2id $ getName $ MAS.getTermType t
kind = Map.findWithDefault (errorId "rl to formula") ty im
pred_type = CAS.Pred_type [kind, kind] nullRange
pred_name = CAS.Qual_pred_name rewID pred_type nullRange
ct = maudeTerm2caslTerm im t
ct' = maudeTerm2caslTerm im t'
conds_form = conds2formula im conds
concl_form = CAS.Predication pred_name [ct, ct'] nullRange
form = CAS.mkImpl conds_form concl_form
-- | translate a conjunction of Maude conditions to a CASL formula
conds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA
conds2formula im conds = CAS.conjunct forms
where forms = map (cond2formula im) conds
-- | translate a single Maude condition to a CASL formula
cond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA
cond2formula im (MAS.EqCond t t') = CAS.mkStEq ct ct'
where ct = maudeTerm2caslTerm im t
ct' = maudeTerm2caslTerm im t'
cond2formula im (MAS.MatchCond t t') = CAS.mkStEq ct ct'
where ct = maudeTerm2caslTerm im t
ct' = maudeTerm2caslTerm im t'
cond2formula im (MAS.MbCond t s) = CAS.Membership ct s' nullRange
where ct = maudeTerm2caslTerm im t
s' = token2id $ getName s
cond2formula im (MAS.RwCond t t') = CAS.mkPredication pred_name [ct, ct']
where ct = maudeTerm2caslTerm im t
ct' = maudeTerm2caslTerm im t'
ty = token2id $ getName $ MAS.getTermType t
kind = Map.findWithDefault (errorId "rw cond to formula") ty im
pred_type = CAS.Pred_type [kind, kind] nullRange
pred_name = CAS.Qual_pred_name rewID pred_type nullRange
-- | translates a Maude term into a CASL term
maudeTerm2caslTerm :: IdMap -> MAS.Term -> CAS.CASLTERM
maudeTerm2caslTerm im (MAS.Var q ty) = CAS.Qual_var q ty' nullRange
where ty' = maudeType2caslSort ty im
maudeTerm2caslTerm im (MAS.Const q ty) = CAS.Application op [] nullRange
where name = token2id q
ty' = maudeType2caslSort ty im
op_type = CAS.Op_type CAS.Total [] ty' nullRange
op = CAS.Qual_op_name name op_type nullRange
maudeTerm2caslTerm im (MAS.Apply q ts ty) = CAS.Application op tts nullRange
where name = token2id q
tts = map (maudeTerm2caslTerm im) ts
ty' = maudeType2caslSort ty im
types_tts = getTypes tts
op_type = CAS.Op_type CAS.Total types_tts ty' nullRange
op = CAS.Qual_op_name name op_type nullRange
maudeSymbol2caslSort :: MSym.Symbol -> IdMap -> CAS.SORT
maudeSymbol2caslSort (MSym.Sort q) _ = token2id q
maudeSymbol2caslSort (MSym.Kind q) im = Map.findWithDefault err q' im
where q' = token2id q
err = errorId "error translate symbol"
maudeSymbol2caslSort _ _ = errorId "error translate symbol"
maudeType2caslSort (MAS.TypeSort q) _ = token2id $ getName q
maudeType2caslSort (MAS.TypeKind q) im = Map.findWithDefault err q' im
where q' = token2id $ getName q
err = errorId "error translate type"
-- | obtains the types of the given terms
getTypes :: [CAS.CASLTERM] -> [Id]
getTypes = mapMaybe getType
-- | extracts the type of the temr
getType :: CAS.CASLTERM -> Maybe Id
getType (CAS.Qual_var _ kind _) = Just kind
getType (CAS.Application op _ _) = case op of
CAS.Qual_op_name _ (CAS.Op_type _ _ kind _) _ -> Just kind
_ -> Nothing
getType _ = Nothing
-- | generates the formulas for the rewrite predicates
rewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
rewPredicatesSens = Set.fold rewPredicateSens []
-- | generates the formulas for the rewrite predicate of the given sort
rewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
rewPredicateSens kind acc = ref : trans : acc
where ref = reflSen kind
trans = transSen kind
-- | creates the reflexivity predicate for the given kind
reflSen :: Id -> Named CAS.CASLFORMULA
reflSen kind = makeNamed name $ quantifyUniversally form
where v = newVar kind
pred_type = CAS.Pred_type [kind, kind] nullRange
pn = CAS.Qual_pred_name rewID pred_type nullRange
form = CAS.Predication pn [v, v] nullRange
name = "rew_refl_" ++ show kind
-- | creates the transitivity predicate for the given kind
transSen :: Id -> Named CAS.CASLFORMULA
transSen kind = makeNamed name $ quantifyUniversally form
where v1 = newVarIndex 1 kind
v2 = newVarIndex 2 kind
v3 = newVarIndex 3 kind
pred_type = CAS.Pred_type [kind, kind] nullRange
pn = CAS.Qual_pred_name rewID pred_type nullRange
prem1 = CAS.Predication pn [v1, v2] nullRange
prem2 = CAS.Predication pn [v2, v3] nullRange
concl = CAS.Predication pn [v1, v3] nullRange
conj_form = CAS.conjunct [prem1, prem2]
form = CAS.mkImpl conj_form concl
name = "rew_trans_" ++ show kind
-- | generate the predicates for the rewrites
rewPredicates :: Set.Set Id -> CSign.PredMap
rewPredicates = Set.fold rewPredicate MapSet.empty
-- | generate the predicates for the rewrites of the given sort
rewPredicate :: Id -> CSign.PredMap -> CSign.PredMap
rewPredicate kind = MapSet.insert rewID $ CSign.PredType [kind, kind]
-- | create the predicates that assign sorts to each term
kindPredicates = Map.foldWithKey kindPredicate Map.empty
{- | create the predicates that assign the current sort to the
corresponding terms -}
kindPredicate sort kind mis = if sort == str2id "Universal" then mis else
let ar = Set.singleton $ CSign.PredType [kind]
in Map.insertWith Set.union sort ar mis
-- | extract the kinds from the map of id's
kindsFromMap :: IdMap -> Set.Set Id
{- | transform the set of Maude sorts in a set of CASL sorts, including
only one sort for each kind. -}
sortsTranslation = sortsTranslationList . Set.toList
{- | transform a list representing the Maude sorts in a set of CASL sorts,
including only one sort for each kind. -}
sortsTranslationList [] _ = 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 r tok = case succs of
[] -> [tok]
toks@(_ : _) -> concatMap (getTop r) toks
where succs = Set.toList $ Rel.succs r tok
-- | delete from the list of sorts those in the same kind that the parameter
deleteRelated ss sym r = foldr (f sym tc) Set.empty ss
where tc = Rel.transClosure r
f sort trC x y = if MSym.sameKind trC sort x
then y
else Set.insert x y
-- | build an Id from a token with the function mkId
token2id :: Token -> Id
token2id t = mkId ts
where ts = maudeSymbol2validCASLSymbol t
-- | build an Id from a Maude symbol
sym2id :: MSym.Symbol -> Id
sym2id = token2id . getName
-- | generates an Id from a string
str2id :: String -> Id
str2id = token2id . mkSimpleId
-- | build an Id from a list of sorts, taking the first from the ordered list
sort2id :: [MSym.Symbol] -> Id
sort2id syms = mkId sym''
where sym : _ = List.sort syms
sym' = getName sym
sym'' = maudeSymbol2validCASLSymbol sym'
-- | add universal quantification of all variables in the formula
quantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA
quantifyUniversally form = CAS.mkForall var_decl form
where vars = getVars form
var_decl = listVarDecl vars
{- | traverses a map with sorts as keys and sets of variables as value and
creates a list of variable declarations -}
listVarDecl = Map.foldWithKey f []
where f sort var_set =
(CAS.Var_decl (Set.toList var_set) sort nullRange :)
-- | removes a quantification from a formula
noQuantification (CAS.Quantification _ vars form _) = (form, vars)
noQuantification form = (form, [])
-- | translate the CASL sorts to symbols
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 = MapSet.foldWithKey createSym4id Set.empty
-- | creates a CASL symbol for a predicate
createSym4id pn pt = Set.insert sym
where sym = CSign.Symbol pn $ CSign.PredAsItemType pt
-- | translates the CASL operators into CASL symbols
ops2symbols = MapSet.foldWithKey createSymOp4id Set.empty
-- | creates a CASL symbol for an operator
createSymOp4id on ot = Set.insert sym
where sym = CSign.Symbol on $ CSign.OpAsItemType ot
{- | extract the variables from a CASL formula and put them in a map
with keys the sort of the variables and value the set of variables
in this sort -}
getVars (CAS.Quantification _ _ f _) = getVars f
getVars (CAS.Junction _ fs _) =
where v1 = getVars f1
v2 = getVars f2
getVars (CAS.Negation f _) = getVars f
getVars (CAS.Predication _ ts _) =
getVars (CAS.Definedness t _) = getVarsTerm t
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.Qual_var var sort _) =
getVarsTerm (CAS.Application _ ts _) =
getVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t
getVarsTerm (CAS.Cast t _ _) = getVarsTerm t
where v1 = getVarsTerm t1
v2 = getVarsTerm t2
v3 = getVars f
m = Map.unionWith Set.union v1 v2
getVarsTerm (CAS.Mixfix_term ts) =
getVarsTerm (CAS.Mixfix_parenthesized ts _) =
getVarsTerm (CAS.Mixfix_bracketed ts _) =
getVarsTerm (CAS.Mixfix_braced ts _) =
getVarsTerm _ = Map.empty
-- | generates the constructor constraint
ctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA
ctorSen isFree (sorts, _, ops) =
let sortList = Set.toList sorts
opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide
(CSign.toOP_TYPE $ compType c) $ posOfId ide)
$ Set.toList ops
allSyms = opSyms
resType _ (CAS.Op_name _) = False
resType s (CAS.Qual_op_name _ t _) = CAS.res_OP_TYPE t == s
getIndex s = fromMaybe (-1) $ List.elemIndex s sortList
addIndices (CAS.Op_name _) =
error "CASL/StaticAna: Internal error in function addIndices"
addIndices os@(CAS.Qual_op_name _ t _) =
(os, map getIndex $ CAS.args_OP_TYPE t)
collectOps s =
CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s
constrs = map collectOps sortList
f = CAS.mkSort_gen_ax constrs isFree
in makeNamed
("ga_generated_" ++ showSepList (showString "_") showId sortList "") f
-- | transforms a maude identifier into a valid CASL identifier
maudeSymbol2validCASLSymbol :: Token -> [Token]
maudeSymbol2validCASLSymbol t = splitDoubleUnderscores str ""
where str = ms2vcs $ show t
{- | transforms a string coding a Maude identifier into another string
representing a CASL identifier -}
ms2vcs :: String -> String
ms2vcs s@('k' : 'i' : 'n' : 'd' : '_' : _) = s
ms2vcs s = if Map.member s stringMap
then stringMap Map.! s
else let f x y
| Map.member x charMap = (charMap Map.! x) ++ "'" ++ y
| x == '_' = "__" ++ y
| otherwise = x : y
in foldr f [] s
-- | map of reserved words
stringMap :: Map.Map String String
stringMap = Map.fromList
[("true", "maudeTrue"),
("false", "maudeFalse"),
("not_", "neg__"),
("s_", "suc"),
("_+_", "__+__"),
("_*_", "__*__"),
("_<_", "__<__"),
("_<=_", "__<=__"),
("_>_", "__>__"),
("_>=_", "__>=__"),
("_and_", "__maudeAnd__")]
{- | splits the string into a list of tokens, separating the double
underscores from the rest of characters -}
splitDoubleUnderscores :: String -> String -> [Token]
splitDoubleUnderscores [] acc = if null acc
then []
else [mkSimpleId acc]
splitDoubleUnderscores ('_' : '_' : cs) acc = if null acc
then dut : rest
else acct : dut : rest
where acct = mkSimpleId acc
dut = mkSimpleId "__"
rest = splitDoubleUnderscores cs []
splitDoubleUnderscores (c : cs) acc = splitDoubleUnderscores cs (acc ++ [c])
-- | error Id
errorId :: String -> Id
errorId s = token2id $ mkSimpleId $ "ERROR: " ++ s
kindId :: Id -> Id
kindId i = token2id $ mkSimpleId $ "kind_" ++ show i
kindMapId :: MSign.KindRel -> IdMap
kindMapId kr = Map.fromList krl'
where krl = Map.toList kr
krl' = map (\ (x, y) -> (mSym2caslId x, mSym2caslId y)) krl
mSym2caslId :: MSym.Symbol -> Id
mSym2caslId (MSym.Sort q) = token2id q
mSym2caslId (MSym.Kind q) = kindId q'
where q' = token2id q
mSym2caslId _ = errorId "error translate symbol"
-- | checks the profile has at least one sort
atLeastOneSort :: MSign.OpMap -> MSign.OpMap
atLeastOneSort om = Map.fromList lom'
where lom = Map.toList om
lom' = filterAtLeastOneSort lom
filterAtLeastOneSort :: [(MAS.Qid, MSign.OpDeclSet)]
-> [(MAS.Qid, MSign.OpDeclSet)]
filterAtLeastOneSort [] = []
filterAtLeastOneSort ((q, ods) : ls) = hd ++ filterAtLeastOneSort ls
where ods' = atLeastOneSortODS ods
hd = if Set.null ods'
then []
else [(q, ods')]
atLeastOneSortODS :: MSign.OpDeclSet -> MSign.OpDeclSet
atLeastOneSortODS ods = Set.fromList lods'
where lods = Set.toList ods
lods' = atLeastOneSortLODS lods
atLeastOneSortLODS :: [MSign.OpDecl] -> [MSign.OpDecl]
atLeastOneSortLODS [] = []
atLeastOneSortLODS ((ss, ats) : ls) = res ++ atLeastOneSortLODS ls
where ss' = atLeastOneSortSS ss
res = if Set.null ss'
then []
else [(ss', ats)]
atLeastOneSortSS = Set.filter hasOneSort
hasOneSort :: MSym.Symbol -> Bool
hasOneSort (MSym.Operator _ ar co) = any isSymSort (co : ar)
hasOneSort _ = False
isSymSort :: MSym.Symbol -> Bool
isSymSort (MSym.Sort _) = True
isSymSort _ = False
{- | translates the Maude operator map into a tuple of CASL operators, CASL
associative operators, membership induced from each Maude operator,
and the set of sorts with the ctor attribute -}
translateOps' :: IdMap -> MSign.OpMap -> OpTransTuple
translateOps' im = Map.fold (translateOpDeclSet' im)
-- | translates an operator declaration set into a tern as described above
translateOpDeclSet' :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
translateOpDeclSet' im ods tpl = Set.fold (translateOpDecl' im) tpl ods
{- | given an operator declaration updates the accumulator with the translation
to CASL operator, checking if the operator has the assoc attribute to insert
it in the map of associative operators, generating the membership predicate
induced by the operator declaration, and checking if it has the ctor
attribute to introduce the operator in the generators sentence -}
translateOpDecl' :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
translateOpDecl' im (syms, ats) (ops, assoc_ops, cs) =
if Set.null syms'
then (ops', assoc_ops', cs')
else translateOpDecl' im (syms', ats) (ops', assoc_ops', cs')
where (sym, syms') = Set.deleteFindMin syms
Just (cop_id, ot, _) = maudeSym2CASLOp' im sym
ops' = MapSet.insert cop_id ot ops
assoc_ops' = if any MAS.assoc ats
then MapSet.insert cop_id ot assoc_ops
else assoc_ops
cs' = if any MAS.ctor ats
then Set.insert (Component cop_id ot) cs
else cs
{- | translates a Maude operator symbol into a pair with the id of the operator
and its CASL type -}
maudeSym2CASLOp' :: IdMap -> MSym.Symbol
-> Maybe (Id, CSign.OpType, CSign.OpType)
maudeSym2CASLOp' im (MSym.Operator op ar co) = Just (token2id op, ot, ot')
where f = token2id . getName
g = (`maudeSymbol2caslSort'` im)
ot = CSign.OpType CAS.Total (map g ar) (g co)
ot' = CSign.OpType CAS.Total (map f ar) (f co)
maudeSym2CASLOp' _ _ = Nothing
maudeSymbol2caslSort' :: MSym.Symbol -> IdMap -> CAS.SORT
maudeSymbol2caslSort' (MSym.Sort q) _ =
token2id $ mkSimpleId $ "kind_" ++ show q
maudeSymbol2caslSort' (MSym.Kind q) im = Map.findWithDefault err q' im
where q' = token2id q
err = errorId "error translate symbol"
maudeSymbol2caslSort' _ _ = errorId "error translate symbol"