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
Safe Haskell	None

Maude.PreComorphism

Description

Comorphism from Maude to CASL.

Synopsis

type IdMap = Map Id Id
type OpTransTuple = (OpMap, OpMap, Set Component)
mapMorphism :: Morphism -> Result CASLMor
maudeOpMap2CASLOpMap :: IdMap -> OpMap -> Op_map
translateOpMapEntry :: IdMap -> Symbol -> Symbol -> Op_map -> Op_map
mapSymbol :: Sign -> Symbol -> Set Symbol
maudeSort2caslId :: IdMap -> Symbol -> Id
createPredMap :: IdMap -> SortMap -> Pred_map
createPredMap4sort :: IdMap -> Symbol -> Symbol -> Pred_map -> Pred_map
applySortMap2CASLSorts :: SortMap -> IdMap -> IdMap -> Sort_map
applySortMap2CASLSort :: IdMap -> IdMap -> (Symbol, Symbol) -> [(Id, Id)] -> [(Id, Id)]
rename :: SortMap -> Token -> Token
mapSentence :: Sign -> Sentence -> Result CASLFORMULA
mapTheory :: (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA])
maude2casl :: Sign -> [Named Sentence] -> (CASLSign, [Named CASLFORMULA])
maudeSbs2caslSbs :: SubsortRel -> IdMap -> Rel SORT
idList2Subsorts :: [(Id, Id)] -> [(Id, Set Id)]
maudeSb2caslSb :: (Symbol, Set Symbol) -> (Id, Set Id)
subsorts2Ids :: (Symbol, Set Symbol) -> (Id, Set Id)
sortSym2id :: Symbol -> Id
rewPredicatesCongSens :: OpMap -> [Named CASLFORMULA]
rewPredCong :: Id -> OpType -> [Named CASLFORMULA] -> [Named CASLFORMULA]
rewPredCongPremise :: Int -> [SORT] -> [CASLTERM]
rewPredsCong :: [SORT] -> [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
loadLibraries :: SortSet -> OpMap -> [Named CASLFORMULA]
loadNaturalNatSens :: [Named CASLFORMULA]
ctorCons :: Named CASLFORMULA -> Bool
booleanImported :: OpMap -> Bool
natImported :: SortSet -> OpMap -> Bool
specialZeroSet :: OpDeclSet -> Bool
specialZero :: OpDecl -> Bool -> Bool
isSpecial :: [Attr] -> Bool
deleteUniversal :: OpMap -> OpMap
universalOps :: Set Id -> OpMap -> Bool -> OpMap
universalOpKind :: Id -> OpMap -> OpMap
universalSens :: Set Id -> [Named CASLFORMULA]
universalSensKind :: Id -> [Named CASLFORMULA] -> [Named CASLFORMULA]
ifSens :: Id -> [Named CASLFORMULA]
equalitySens :: Id -> [Named CASLFORMULA]
nonEqualitySens :: Id -> [Named CASLFORMULA]
axiomsSens :: IdMap -> OpMap -> [Named CASLFORMULA]
axiomsSensODS :: IdMap -> OpDeclSet -> [Named CASLFORMULA] -> [Named CASLFORMULA]
axiomsSensOD :: IdMap -> OpDecl -> [Named CASLFORMULA] -> [Named CASLFORMULA]
axiomsSensSS :: IdMap -> [Attr] -> Symbol -> [Named CASLFORMULA] -> [Named CASLFORMULA]
commSen :: IdMap -> Qid -> Symbols -> Symbol -> [Named CASLFORMULA]
translateOps :: IdMap -> OpMap -> OpTransTuple
translateOpDeclSet :: IdMap -> OpDeclSet -> OpTransTuple -> OpTransTuple
translateOpDecl :: IdMap -> OpDecl -> OpTransTuple -> OpTransTuple
maudeSym2CASLOp :: IdMap -> Symbol -> Maybe (Id, OpType, OpType)
createConjForm :: [CASLFORMULA] -> CASLFORMULA
createImpForm :: CASLFORMULA -> CASLFORMULA -> CASLFORMULA
ops2predPremises :: IdMap -> [Symbol] -> Int -> ([CASLTERM], [CASLFORMULA])
splitOwiseEqs :: [Named Sentence] -> ([Named Sentence], [Named Sentence], [Named Sentence])
noOwiseSen2Formula :: IdMap -> Named Sentence -> Named CASLFORMULA
owiseSen2Formula :: IdMap -> [Named CASLFORMULA] -> Named Sentence -> Named CASLFORMULA
mb_rl2formula :: IdMap -> Named Sentence -> Named CASLFORMULA
newVarIndex :: Int -> Id -> CASLTERM
newVar :: Id -> CASLTERM
rewID :: Id
noOwiseEq2Formula :: IdMap -> Equation -> CASLFORMULA
owiseEq2Formula :: IdMap -> [Named CASLFORMULA] -> Equation -> CASLFORMULA
existencialNegationOtherEqs :: OP_SYMB -> [CASLTERM] -> [Named CASLFORMULA] -> CASLFORMULA
existencialNegationOtherEq :: OP_SYMB -> [CASLTERM] -> Named CASLFORMULA -> [CASLFORMULA]
qualifyExVarsForms :: [CASLFORMULA] -> [CASLFORMULA]
qualifyExVarsForm :: CASLFORMULA -> CASLFORMULA
qualifyExVarsTerms :: [CASLTERM] -> [CASLTERM]
qualifyExVarsTerm :: CASLTERM -> CASLTERM
qualifyExVars :: [VAR_DECL] -> [VAR_DECL]
qualifyExVar :: VAR_DECL -> VAR_DECL
qualifyExVarAux :: Token -> Token
createEqs :: [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
getLeftApp :: CASLFORMULA -> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
getLeftAppTerm :: CASLTERM -> Maybe (OP_SYMB, [CASLTERM])
getPremisesImplication :: CASLFORMULA -> [CASLFORMULA]
mb2formula :: IdMap -> Membership -> CASLFORMULA
rl2formula :: IdMap -> Rule -> CASLFORMULA
conds2formula :: IdMap -> [Condition] -> CASLFORMULA
cond2formula :: IdMap -> Condition -> CASLFORMULA
maudeTerm2caslTerm :: IdMap -> Term -> CASLTERM
maudeSymbol2caslSort :: Symbol -> IdMap -> SORT
maudeType2caslSort :: Type -> IdMap -> SORT
getTypes :: [CASLTERM] -> [Id]
getType :: CASLTERM -> Maybe Id
rewPredicatesSens :: Set Id -> [Named CASLFORMULA]
rewPredicateSens :: Id -> [Named CASLFORMULA] -> [Named CASLFORMULA]
reflSen :: Id -> Named CASLFORMULA
transSen :: Id -> Named CASLFORMULA
rewPredicates :: Set Id -> PredMap
rewPredicate :: Id -> PredMap -> PredMap
kindPredicates :: IdMap -> Map Id (Set PredType)
kindPredicate :: Id -> Id -> Map Id (Set PredType) -> Map Id (Set PredType)
kindsFromMap :: IdMap -> Set Id
sortsTranslation :: SortSet -> SubsortRel -> Set Id
sortsTranslationList :: [Symbol] -> SubsortRel -> Set Id
getTop :: SubsortRel -> Symbol -> [Symbol]
deleteRelated :: [Symbol] -> Symbol -> SubsortRel -> SortSet
token2id :: Token -> Id
sym2id :: Symbol -> Id
str2id :: String -> Id
sort2id :: [Symbol] -> Id
quantifyUniversally :: CASLFORMULA -> CASLFORMULA
listVarDecl :: Map Id (Set Token) -> [VAR_DECL]
noQuantification :: CASLFORMULA -> (CASLFORMULA, [VAR_DECL])
kinds2syms :: Set Id -> Set Symbol
kind2sym :: Id -> Symbol
preds2syms :: PredMap -> Set Symbol
createSym4id :: Id -> PredType -> Set Symbol -> Set Symbol
ops2symbols :: OpMap -> Set Symbol
createSymOp4id :: Id -> OpType -> Set Symbol -> Set Symbol
getVars :: CASLFORMULA -> Map Id (Set Token)
getVarsTerm :: CASLTERM -> Map Id (Set Token)
ctorSen :: Bool -> GenAx -> Named CASLFORMULA
maudeSymbol2validCASLSymbol :: Token -> [Token]
ms2vcs :: String -> String
stringMap :: Map String String
splitDoubleUnderscores :: String -> String -> [Token]
errorId :: String -> Id
kindId :: Id -> Id
kindMapId :: KindRel -> IdMap
mSym2caslId :: Symbol -> Id
atLeastOneSort :: OpMap -> OpMap
filterAtLeastOneSort :: [(Qid, OpDeclSet)] -> [(Qid, OpDeclSet)]
atLeastOneSortODS :: OpDeclSet -> OpDeclSet
atLeastOneSortLODS :: [OpDecl] -> [OpDecl]
atLeastOneSortSS :: Set Symbol -> Set Symbol
hasOneSort :: Symbol -> Bool
isSymSort :: Symbol -> Bool
translateOps' :: IdMap -> OpMap -> OpTransTuple
translateOpDeclSet' :: IdMap -> OpDeclSet -> OpTransTuple -> OpTransTuple
translateOpDecl' :: IdMap -> OpDecl -> OpTransTuple -> OpTransTuple
maudeSym2CASLOp' :: IdMap -> Symbol -> Maybe (Id, OpType, OpType)
maudeSymbol2caslSort' :: Symbol -> IdMap -> SORT

Documentation

type IdMap = Map Id Id Source #

type OpTransTuple = (OpMap, OpMap, Set Component) Source #

mapMorphism :: Morphism -> Result CASLMor Source #

generates a CASL morphism from a Maude morphism

maudeOpMap2CASLOpMap :: IdMap -> OpMap -> Op_map Source #

translates the Maude morphism between operators into a CASL morpshim between operators

translateOpMapEntry :: IdMap -> Symbol -> Symbol -> Op_map -> Op_map Source #

translates the mapping between two symbols representing operators into a CASL operators map

mapSymbol :: Sign -> Symbol -> Set Symbol Source #

generates a set of CASL symbol from a Maude Symbol

maudeSort2caslId :: IdMap -> Symbol -> Id Source #

returns the sort in CASL of the Maude sort symbol

createPredMap :: IdMap -> SortMap -> Pred_map Source #

creates the predicate map for the CASL morphism from the Maude sort map and the map between sorts and kinds

createPredMap4sort :: IdMap -> Symbol -> Symbol -> Pred_map -> Pred_map Source #

creates an entry of the predicate map for a single sort

applySortMap2CASLSorts :: SortMap -> IdMap -> IdMap -> Sort_map Source #

computes the sort morphism of CASL from the sort morphism in Maude and the set of kinds

applySortMap2CASLSort :: IdMap -> IdMap -> (Symbol, Symbol) -> [(Id, Id)] -> [(Id, Id)] Source #

computes the morphism for a single sort pair

rename :: SortMap -> Token -> Token Source #

renames the sorts in a given kind

mapSentence :: Sign -> Sentence -> Result CASLFORMULA Source #

translates a Maude sentence into a CASL formula

mapTheory :: (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA]) Source #

applies maude2casl to compute the CASL signature and sentences from the Maude ones, and wraps them into a Result datatype

maude2casl :: Sign -> [Named Sentence] -> (CASLSign, [Named CASLFORMULA]) Source #

computes new signature and sentences of CASL associated to the given Maude signature and sentences

maudeSbs2caslSbs :: SubsortRel -> IdMap -> Rel SORT Source #

translates the Maude subsorts into CASL subsorts, and adds the subsorts for the kinds

idList2Subsorts :: [(Id, Id)] -> [(Id, Set Id)] Source #

maudeSb2caslSb :: (Symbol, Set Symbol) -> (Id, Set Id) Source #

subsorts2Ids :: (Symbol, Set Symbol) -> (Id, Set Id) Source #

sortSym2id :: Symbol -> Id Source #

rewPredicatesCongSens :: OpMap -> [Named CASLFORMULA] Source #

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

rewPredCong :: Id -> OpType -> [Named CASLFORMULA] -> [Named CASLFORMULA] Source #

generates the sentences to state that the rew predicates are a congruence for a single operator

rewPredCongPremise :: Int -> [SORT] -> [CASLTERM] Source #

generates a list of variables of the given sorts

rewPredsCong :: [SORT] -> [CASLTERM] -> [CASLTERM] -> [CASLFORMULA] Source #

generates a list of rew predicates with the given variables

loadLibraries :: SortSet -> OpMap -> [Named CASLFORMULA] Source #

load the CASL libraries for the Maude built-in operators

loadNaturalNatSens :: [Named CASLFORMULA] Source #

loads the sentences associated to the natural numbers

ctorCons :: Named CASLFORMULA -> Bool Source #

checks if a sentence is an constructor sentence

booleanImported :: OpMap -> Bool Source #

checks if the boolean values are imported

natImported :: SortSet -> OpMap -> Bool Source #

checks if the natural numbers are imported

specialZeroSet :: OpDeclSet -> Bool Source #

specialZero :: OpDecl -> Bool -> Bool Source #

isSpecial :: [Attr] -> Bool Source #

deleteUniversal :: OpMap -> OpMap Source #

delete the universal operators from Maude specifications, that will be substituted for one operator for each sort in the specification

universalOps :: Set Id -> OpMap -> Bool -> OpMap Source #

generates the universal operators for all the sorts in the module

universalOpKind :: Id -> OpMap -> OpMap Source #

generates the universal operators for a concrete module

universalSens :: Set Id -> [Named CASLFORMULA] Source #

generates the formulas for the universal operators

universalSensKind :: Id -> [Named CASLFORMULA] -> [Named CASLFORMULA] Source #

generates the formulas for the universal operators for the given sort

ifSens :: Id -> [Named CASLFORMULA] Source #

generates the formulas for the if statement

equalitySens :: Id -> [Named CASLFORMULA] Source #

generates the formulas for the equality

nonEqualitySens :: Id -> [Named CASLFORMULA] Source #

generates the formulas for the inequality

axiomsSens :: IdMap -> OpMap -> [Named CASLFORMULA] Source #

generates the sentences for the operator attributes

axiomsSensODS :: IdMap -> OpDeclSet -> [Named CASLFORMULA] -> [Named CASLFORMULA] Source #

axiomsSensOD :: IdMap -> OpDecl -> [Named CASLFORMULA] -> [Named CASLFORMULA] Source #

axiomsSensSS :: IdMap -> [Attr] -> Symbol -> [Named CASLFORMULA] -> [Named CASLFORMULA] Source #

commSen :: IdMap -> Qid -> Symbols -> Symbol -> [Named CASLFORMULA] Source #

translateOps :: IdMap -> OpMap -> OpTransTuple Source #

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

translateOpDeclSet :: IdMap -> OpDeclSet -> OpTransTuple -> OpTransTuple Source #

translates an operator declaration set into a tern as described above

translateOpDecl :: IdMap -> OpDecl -> OpTransTuple -> OpTransTuple Source #

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

maudeSym2CASLOp :: IdMap -> Symbol -> Maybe (Id, OpType, OpType) Source #

translates a Maude operator symbol into a pair with the id of the operator and its CASL type

createConjForm :: [CASLFORMULA] -> CASLFORMULA Source #

creates a conjuctive formula distinguishing the size of the list

createImpForm :: CASLFORMULA -> CASLFORMULA -> CASLFORMULA Source #

creates a implication formula distinguishing the size of the premises

ops2predPremises :: IdMap -> [Symbol] -> Int -> ([CASLTERM], [CASLFORMULA]) Source #

generates the predicates asserting the "true" sort of the operator if all the arguments have the correct sort

splitOwiseEqs :: [Named Sentence] -> ([Named Sentence], [Named Sentence], [Named Sentence]) Source #

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

noOwiseSen2Formula :: IdMap -> Named Sentence -> Named CASLFORMULA Source #

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

owiseSen2Formula :: IdMap -> [Named CASLFORMULA] -> Named Sentence -> Named CASLFORMULA Source #

translates a Maude equation defined with the "owise" attribute into a CASL formula

mb_rl2formula :: IdMap -> Named Sentence -> Named CASLFORMULA Source #

translates a Maude membership or rule into a CASL formula

newVarIndex :: Int -> Id -> CASLTERM Source #

generates a new variable qualified with the given number

newVar :: Id -> CASLTERM Source #

generates a new variable

rewID :: Id Source #

Id for the rew predicate

noOwiseEq2Formula :: IdMap -> Equation -> CASLFORMULA Source #

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

owiseEq2Formula :: IdMap -> [Named CASLFORMULA] -> Equation -> CASLFORMULA Source #

transforms a Maude equation defined with the otherwise attribute into a CASL formula

existencialNegationOtherEqs :: OP_SYMB -> [CASLTERM] -> [Named CASLFORMULA] -> CASLFORMULA Source #

generates a conjunction of negation of existencial quantifiers

existencialNegationOtherEq :: OP_SYMB -> [CASLTERM] -> Named CASLFORMULA -> [CASLFORMULA] Source #

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

qualifyExVarsForms :: [CASLFORMULA] -> [CASLFORMULA] Source #

qualifies the variables in a list of formulas with the suffix "_ex" to distinguish them from the variables already bound

qualifyExVarsForm :: CASLFORMULA -> CASLFORMULA Source #

qualifies the variables in a formula with the suffix "_ex" to distinguish them from the variables already bound

qualifyExVarsTerms :: [CASLTERM] -> [CASLTERM] Source #

qualifies the variables in a list of terms with the suffix "_ex" to distinguish them from the variables already bound

qualifyExVarsTerm :: CASLTERM -> CASLTERM Source #

qualifies the variables in a term with the suffix "_ex" to distinguish them from the variables already bound

qualifyExVars :: [VAR_DECL] -> [VAR_DECL] Source #

qualifies a list of variables with the suffix "_ex" to distinguish them from the variables already bound

qualifyExVar :: VAR_DECL -> VAR_DECL Source #

qualifies a variable with the suffix "_ex" to distinguish it from the variables already bound

qualifyExVarAux :: Token -> Token Source #

qualifies a token with the suffix "_ex"

createEqs :: [CASLTERM] -> [CASLTERM] -> [CASLFORMULA] Source #

creates a list of strong equalities from two lists of terms

getLeftApp :: CASLFORMULA -> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA]) Source #

extracts the operator at the top and the arguments of the lefthand side in a strong equation

getLeftAppTerm :: CASLTERM -> Maybe (OP_SYMB, [CASLTERM]) Source #

extracts the operator at the top and the arguments of the lefthand side in an application term

getPremisesImplication :: CASLFORMULA -> [CASLFORMULA] Source #

extracts the formulas of the given premise, distinguishing whether it is a conjunction or not

mb2formula :: IdMap -> Membership -> CASLFORMULA Source #

translate a Maude membership into a CASL formula

rl2formula :: IdMap -> Rule -> CASLFORMULA Source #

translate a Maude rule into a CASL formula

conds2formula :: IdMap -> [Condition] -> CASLFORMULA Source #

translate a conjunction of Maude conditions to a CASL formula

cond2formula :: IdMap -> Condition -> CASLFORMULA Source #

translate a single Maude condition to a CASL formula

maudeTerm2caslTerm :: IdMap -> Term -> CASLTERM Source #

translates a Maude term into a CASL term

maudeSymbol2caslSort :: Symbol -> IdMap -> SORT Source #

maudeType2caslSort :: Type -> IdMap -> SORT Source #

getTypes :: [CASLTERM] -> [Id] Source #

obtains the types of the given terms

getType :: CASLTERM -> Maybe Id Source #

extracts the type of the temr

rewPredicatesSens :: Set Id -> [Named CASLFORMULA] Source #

generates the formulas for the rewrite predicates

rewPredicateSens :: Id -> [Named CASLFORMULA] -> [Named CASLFORMULA] Source #

generates the formulas for the rewrite predicate of the given sort

reflSen :: Id -> Named CASLFORMULA Source #

creates the reflexivity predicate for the given kind

transSen :: Id -> Named CASLFORMULA Source #

creates the transitivity predicate for the given kind

rewPredicates :: Set Id -> PredMap Source #

generate the predicates for the rewrites

rewPredicate :: Id -> PredMap -> PredMap Source #

generate the predicates for the rewrites of the given sort

kindPredicates :: IdMap -> Map Id (Set PredType) Source #

create the predicates that assign sorts to each term

kindPredicate :: Id -> Id -> Map Id (Set PredType) -> Map Id (Set PredType) Source #

create the predicates that assign the current sort to the corresponding terms

kindsFromMap :: IdMap -> Set Id Source #

extract the kinds from the map of id's

sortsTranslation :: SortSet -> SubsortRel -> Set Id Source #

transform the set of Maude sorts in a set of CASL sorts, including only one sort for each kind.

sortsTranslationList :: [Symbol] -> SubsortRel -> Set Id Source #

transform a list representing the Maude sorts in a set of CASL sorts, including only one sort for each kind.

getTop :: SubsortRel -> Symbol -> [Symbol] Source #

return the maximal elements from the sort relation

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

token2id :: Token -> Id Source #

build an Id from a token with the function mkId

sym2id :: Symbol -> Id Source #

build an Id from a Maude symbol

str2id :: String -> Id Source #

generates an Id from a string

sort2id :: [Symbol] -> Id Source #

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

quantifyUniversally :: CASLFORMULA -> CASLFORMULA Source #

add universal quantification of all variables in the formula

listVarDecl :: Map Id (Set Token) -> [VAR_DECL] Source #

traverses a map with sorts as keys and sets of variables as value and creates a list of variable declarations

noQuantification :: CASLFORMULA -> (CASLFORMULA, [VAR_DECL]) Source #

removes a quantification from a formula

kinds2syms :: Set Id -> Set Symbol Source #

translate the CASL sorts to symbols

kind2sym :: Id -> Symbol Source #

translate a CASL sort to a CASL symbol

preds2syms :: PredMap -> Set Symbol Source #

translates the CASL predicates into CASL symbols

createSym4id :: Id -> PredType -> Set Symbol -> Set Symbol Source #

creates a CASL symbol for a predicate

ops2symbols :: OpMap -> Set Symbol Source #

translates the CASL operators into CASL symbols

createSymOp4id :: Id -> OpType -> Set Symbol -> Set Symbol Source #

creates a CASL symbol for an operator

getVars :: CASLFORMULA -> Map Id (Set Token) Source #

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

getVarsTerm :: CASLTERM -> Map Id (Set Token) Source #

extract the variables of a CASL term

ctorSen :: Bool -> GenAx -> Named CASLFORMULA Source #

generates the constructor constraint

maudeSymbol2validCASLSymbol :: Token -> [Token] Source #

transforms a maude identifier into a valid CASL identifier

ms2vcs :: String -> String Source #

transforms a string coding a Maude identifier into another string representing a CASL identifier

stringMap :: Map String String Source #

map of reserved words

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

splits the string into a list of tokens, separating the double underscores from the rest of characters

errorId :: String -> Id Source #

error Id

kindId :: Id -> Id Source #

kindMapId :: KindRel -> IdMap Source #

mSym2caslId :: Symbol -> Id Source #

atLeastOneSort :: OpMap -> OpMap Source #

checks the profile has at least one sort

filterAtLeastOneSort :: [(Qid, OpDeclSet)] -> [(Qid, OpDeclSet)] Source #

atLeastOneSortODS :: OpDeclSet -> OpDeclSet Source #

atLeastOneSortLODS :: [OpDecl] -> [OpDecl] Source #

atLeastOneSortSS :: Set Symbol -> Set Symbol Source #

hasOneSort :: Symbol -> Bool Source #

isSymSort :: Symbol -> Bool Source #

translateOps' :: IdMap -> OpMap -> OpTransTuple Source #

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

translateOpDeclSet' :: IdMap -> OpDeclSet -> OpTransTuple -> OpTransTuple Source #

translates an operator declaration set into a tern as described above

translateOpDecl' :: IdMap -> OpDecl -> OpTransTuple -> OpTransTuple Source #

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

maudeSym2CASLOp' :: IdMap -> Symbol -> Maybe (Id, OpType, OpType) Source #

translates a Maude operator symbol into a pair with the id of the operator and its CASL type

maudeSymbol2caslSort' :: Symbol -> IdMap -> SORT Source #