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

Documentation

type IdMap = Map Id Id

type OpTransTuple = (OpMap, OpMap, Set Component)

mapMorphism :: Morphism -> Result CASLMor

generates a CASL morphism from a Maude morphism

maudeOpMap2CASLOpMap :: IdMap -> OpMap -> Op_map

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

translateOpMapEntry :: IdMap -> Symbol -> Symbol -> Op_map -> Op_map

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

mapSymbol :: Sign -> Symbol -> Set Symbol

generates a set of CASL symbol from a Maude Symbol

maudeSort2caslId :: IdMap -> Symbol -> Id

returns the sort in CASL of the Maude sort symbol

createPredMap :: IdMap -> SortMap -> Pred_map

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

creates an entry of the predicate map for a single sort

applySortMap2CASLSorts :: SortMap -> IdMap -> IdMap -> Sort_map

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)]

computes the morphism for a single sort pair

rename :: SortMap -> Token -> Token

renames the sorts in a given kind

mapSentence :: Sign -> Sentence -> Result CASLFORMULA

translates a Maude sentence into a CASL formula

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

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])

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

maudeSbs2caslSbs :: SubsortRel -> IdMap -> Rel SORT

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

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]

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

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

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

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

generates a list of variables of the given sorts

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

generates a list of rew predicates with the given variables

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

load the CASL libraries for the Maude built-in operators

loadNaturalNatSens :: [Named CASLFORMULA]

loads the sentences associated to the natural numbers

ctorCons :: Named CASLFORMULA -> Bool

checks if a sentence is an constructor sentence

booleanImported :: OpMap -> Bool

checks if the boolean values are imported

natImported :: SortSet -> OpMap -> Bool

checks if the natural numbers are imported

specialZeroSet :: OpDeclSet -> Bool

specialZero :: OpDecl -> Bool -> Bool

isSpecial :: [Attr] -> Bool

deleteUniversal :: OpMap -> OpMap

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

generates the universal operators for all the sorts in the module

universalOpKind :: Id -> OpMap -> OpMap

generates the universal operators for a concrete module

universalSens :: Set Id -> [Named CASLFORMULA]

generates the formulas for the universal operators

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

generates the formulas for the universal operators for the given sort

ifSens :: Id -> [Named CASLFORMULA]

generates the formulas for the if statement

equalitySens :: Id -> [Named CASLFORMULA]

generates the formulas for the equality

nonEqualitySens :: Id -> [Named CASLFORMULA]

generates the formulas for the inequality

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

generates the sentences for the operator attributes

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

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

translates an operator declaration set into a tern as described above

translateOpDecl :: IdMap -> OpDecl -> OpTransTuple -> OpTransTuple

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)

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

createConjForm :: [CASLFORMULA] -> CASLFORMULA

creates a conjuctive formula distinguishing the size of the list

createImpForm :: CASLFORMULA -> CASLFORMULA -> CASLFORMULA

creates a implication formula distinguishing the size of the premises

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

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])

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

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

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

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

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

translates a Maude membership or rule into a CASL formula

newVarIndex :: Int -> Id -> CASLTERM

generates a new variable qualified with the given number

newVar :: Id -> CASLTERM

generates a new variable

rewID :: Id

Id for the rew predicate

noOwiseEq2Formula :: IdMap -> Equation -> CASLFORMULA

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

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

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

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

generates a conjunction of negation of existencial quantifiers

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

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]

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

qualifyExVarsForm :: CASLFORMULA -> CASLFORMULA

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

qualifyExVarsTerms :: [CASLTERM] -> [CASLTERM]

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

qualifyExVarsTerm :: CASLTERM -> CASLTERM

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

qualifyExVars :: [VAR_DECL] -> [VAR_DECL]

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

qualifyExVar :: VAR_DECL -> VAR_DECL

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

qualifyExVarAux :: Token -> Token

qualifies a token with the suffix "_ex"

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

creates a list of strong equalities from two lists of terms

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

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

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

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

getPremisesImplication :: CASLFORMULA -> [CASLFORMULA]

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

mb2formula :: IdMap -> Membership -> CASLFORMULA

translate a Maude membership into a CASL formula

rl2formula :: IdMap -> Rule -> CASLFORMULA

translate a Maude rule into a CASL formula

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

translate a conjunction of Maude conditions to a CASL formula

cond2formula :: IdMap -> Condition -> CASLFORMULA

translate a single Maude condition to a CASL formula

maudeTerm2caslTerm :: IdMap -> Term -> CASLTERM

translates a Maude term into a CASL term

maudeSymbol2caslSort :: Symbol -> IdMap -> SORT

maudeType2caslSort :: Type -> IdMap -> SORT

getTypes :: [CASLTERM] -> [Id]

obtains the types of the given terms

getType :: CASLTERM -> Maybe Id

extracts the type of the temr

rewPredicatesSens :: Set Id -> [Named CASLFORMULA]

generates the formulas for the rewrite predicates

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

generates the formulas for the rewrite predicate of the given sort

reflSen :: Id -> Named CASLFORMULA

creates the reflexivity predicate for the given kind

transSen :: Id -> Named CASLFORMULA

creates the transitivity predicate for the given kind

rewPredicates :: Set Id -> PredMap

generate the predicates for the rewrites

rewPredicate :: Id -> PredMap -> PredMap

generate the predicates for the rewrites of the given sort

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

create the predicates that assign sorts to each term

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

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

kindsFromMap :: IdMap -> Set Id

extract the kinds from the map of id's

sortsTranslation :: SortSet -> SubsortRel -> Set Id

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

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

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

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

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

build an Id from a token with the function mkId

sym2id :: Symbol -> Id

build an Id from a Maude symbol

str2id :: String -> Id

generates an Id from a string

sort2id :: [Symbol] -> Id

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

quantifyUniversally :: CASLFORMULA -> CASLFORMULA

add universal quantification of all variables in the formula

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

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])

removes a quantification from a formula

kinds2syms :: Set Id -> Set Symbol

translate the CASL sorts to symbols

kind2sym :: Id -> Symbol

translate a CASL sort to a CASL symbol

preds2syms :: PredMap -> Set Symbol

translates the CASL predicates into CASL symbols

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

creates a CASL symbol for a predicate

ops2symbols :: OpMap -> Set Symbol

translates the CASL operators into CASL symbols

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

creates a CASL symbol for an operator

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

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)

extract the variables of a CASL term

ctorSen :: Bool -> GenAx -> Named CASLFORMULA

generates the constructor constraint

maudeSymbol2validCASLSymbol :: Token -> [Token]

transforms a maude identifier into a valid CASL identifier

ms2vcs :: String -> String

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

stringMap :: Map String String

map of reserved words

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

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

errorId :: String -> Id

error Id

kindId :: Id -> Id

kindMapId :: KindRel -> IdMap

mSym2caslId :: Symbol -> Id

atLeastOneSort :: OpMap -> OpMap

checks the profile has at least one sort

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

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

translates an operator declaration set into a tern as described above

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

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)

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

maudeSymbol2caslSort' :: Symbol -> IdMap -> SORT