Hets - the Heterogeneous Tool Set

Maude.PreComorphism

Description

Comorphism from Maude to CASL.

Synopsis

# Documentation

type IdMap = Map Id Id Source #

generates a CASL morphism from a Maude morphism

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

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

returns the sort in CASL of the Maude sort symbol

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

creates an entry of the predicate map for a single sort

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

renames the sorts in a given kind

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

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 #

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

load the CASL libraries for the Maude built-in operators

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

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

isSpecial :: [Attr] -> Bool 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

generates the universal operators for a concrete module

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

generates the formulas for the universal operators

generates the formulas for the universal operators for the given sort

generates the formulas for the if statement

generates the formulas for the equality

generates the formulas for the inequality

generates the sentences for the operator attributes

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

translates an operator declaration set into a tern as described above

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

creates a conjuctive formula distinguishing the size of the list

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

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

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

translates a Maude membership or rule into a CASL formula

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

generates a new variable qualified with the given number

generates a new variable

Id for the rew predicate

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

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

generates a conjunction of negation of existencial quantifiers

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

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

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

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

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

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

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

translate a Maude membership into a CASL formula

translate a Maude rule into a CASL formula

translate a conjunction of Maude conditions to a CASL formula

translate a single Maude condition to a CASL formula

translates a Maude term into a CASL term

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

generates the formulas for the rewrite predicate of the given sort

creates the reflexivity predicate for the given kind

creates the transitivity predicate for the given kind

rewPredicates :: Set Id -> PredMap Source #

generate the predicates for the rewrites

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

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

build an Id from a token with the function mkId

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

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

removes a quantification from a formula

kinds2syms :: Set Id -> Set Symbol Source #

translate the CASL sorts to symbols

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

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

checks the profile has at least one sort

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

translates an operator declaration set into a tern as described above

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