Class Module
java.lang.Object
es.ucm.maude.bindings.Module
-
Nested Class Summary
Nested ClassesModifier and TypeClassDescriptionstatic final class
Module or theory type (function, system or strategy). -
Method Summary
Modifier and TypeMethodDescriptionvoid
delete()
downStrategy
(Term term) Get a strategy expression in this module from its
metarepresentation in (possibly) another module.
Get a term in this module from its metarepresentation
in (possibly) another module.
Finds a sort by its name in the module.
findSymbol
(String name, KindVector domainKinds, Kind rangeKind) Find a symbol by its name and signature in the module.
Get the equations defined in the module.getKinds()
Get the kinds defined in the module.Get the membership axioms defined in the module.Get the module type.
This allows distinguishing modules from theories, and the
functional, system and strategy variants within them.int
Number of sorts imported from other modules or parameters.int
Number of strategies imported from other modules or parameters.int
Number of symbols imported from other modules or parameters.int
Number of equations from this module.int
Number of rules from this module.int
Number of strategy definitions from this module.int
Number of parameters of the parameterized module.getParameterName
(int index) Get the name of a module parameter.
getParameterTheory
(int index) Get the theory of the given parameter.getRules()
Get the rules defined in the module.getSorts()
Get the sorts declared in the module.Get the strategies declared in the module.Get the strategy definitions defined in the module.Get the symbols declared in the module.boolean
Is this a parameterized module with free parameters?parseStrategy
(String strat_str) Parse a strategy expression.
parseStrategy
(String strat_str, TermVector vars) Parse a strategy expression.
parseTerm
(TokenVector bubble) Parse a term.
parseTerm
(TokenVector bubble, Kind kind) Parse a term.
Parse a term.
Parse a term.
parseTerm
(String term_str, Kind kind, TermVector vars) Parse a term.
toLatex()
Obtain the LaTeX representation of this module.
toLatex
(boolean all) Obtain the LaTeX representation of this module.
toString()
unify
(TermPairVector problem) Solves the given unification problem.
unify
(TermPairVector problem, boolean irredundant) Solves the given unification problem.
upStrategy
(StrategyExpression expr) Get the metarepresentation in this module of a strategy
expression in (possibly) another module.Get the metarepresentation in this module of a term
in (possibly) another module.variant_match
(TermPairVector problem) Computes a complete set of order-sorted matches modulo the equations
declared with the variant attribute (which must satisfy the finite
variant property) plus the (supported) equational axioms in the
given module.
variant_match
(TermPairVector problem, TermVector irreducible) Computes a complete set of order-sorted matches modulo the equations
declared with the variant attribute (which must satisfy the finite
variant property) plus the (supported) equational axioms in the
given module.
variant_unify
(TermPairVector problem) Solves the given unification problem using variants.
variant_unify
(TermPairVector problem, TermVector irreducible) Solves the given unification problem using variants.
variant_unify
(TermPairVector problem, TermVector irreducible, boolean filtered) Solves the given unification problem using variants.
vu_narrow
(TermVector subject, SearchType type, Term target) Narrowing-based search of terms that unify with the given target
with multiple initial states.
vu_narrow
(TermVector subject, SearchType type, Term target, int depth) Narrowing-based search of terms that unify with the given target
with multiple initial states.
vu_narrow
(TermVector subject, SearchType type, Term target, int depth, int flags) Narrowing-based search of terms that unify with the given target
with multiple initial states.
-
Method Details
-
delete
public void delete() -
getModuleType
Get the module type.
This allows distinguishing modules from theories, and the
functional, system and strategy variants within them. -
getSorts
Get the sorts declared in the module. -
getSymbols
Get the symbols declared in the module. -
getKinds
Get the kinds defined in the module. -
getMembershipAxioms
Get the membership axioms defined in the module. -
getEquations
Get the equations defined in the module. -
getRules
Get the rules defined in the module. -
getStrategies
Get the strategies declared in the module. -
getStrategyDefinitions
Get the strategy definitions defined in the module. -
getNrParameters
public int getNrParameters()Number of parameters of the parameterized module. -
hasFreeParameters
public boolean hasFreeParameters()Is this a parameterized module with free parameters? -
getNrImportedSorts
public int getNrImportedSorts()Number of sorts imported from other modules or parameters. -
getNrImportedSymbols
public int getNrImportedSymbols()Number of symbols imported from other modules or parameters. -
getNrImportedStrategies
public int getNrImportedStrategies()Number of strategies imported from other modules or parameters. -
getNrOriginalEquations
public int getNrOriginalEquations()Number of equations from this module. -
getNrOriginalRules
public int getNrOriginalRules()Number of rules from this module. -
getNrOriginalStrategyDefinitions
public int getNrOriginalStrategyDefinitions()Number of strategy definitions from this module. -
getParameterTheory
Get the theory of the given parameter. -
getParameterName
Get the name of a module parameter.
- Parameters:
index
- Index of the parameter.
-
findSort
-
findSymbol
Find a symbol by its name and signature in the module.
- Parameters:
name
- The name of the sort.domainKinds
- Kinds of the symbol domain.rangeKind
- Range kind of the symbol.
- Returns:
- The symbol or null if it does not exist.
-
parseTerm
Parse a term.
- Parameters:
bubble
- Tokenized term.kind
- Restrict parsing to terms of the given kind.
-
parseTerm
-
parseTerm
Parse a term.
- Parameters:
term_str
- A term represented as a string.kind
- Restrict parsing to terms of the given kind.vars
- Variables that may appear without explicit type
annotation in the strategy.
-
parseTerm
-
parseTerm
-
parseStrategy
Parse a strategy expression.
- Parameters:
vars
- Variables that may appear without explicit type
annotation in the strategy.
-
parseStrategy
Parse a strategy expression.
-
downTerm
Get a term in this module from its metarepresentation
in (possibly) another module.
- Parameters:
term
- The metarepresentation of a term, that is,
a valid element of theTerm
sort inMETA-TERM
.
This term must belong to a module where theMETA-LEVEL
module is included. The term will be reduced.
- Returns:
- The term or null if the metarepresentation was
not valid.
-
downStrategy
Get a strategy expression in this module from its
metarepresentation in (possibly) another module.
- Parameters:
term
- The metarepresentation of a strategy, that is,
a valid element of theStrategy
sort inMETA-STRATEGY
.
This term must belong to a module where theMETA-LEVEL
module is included. The term will be reduced.
- Returns:
- The strategy expression or null if the
metarepresentation was not valid.
-
upTerm
-
upStrategy
Get the metarepresentation in this module of a strategy
expression in (possibly) another module. This module must
containMETA-LEVEL
.
- Parameters:
expr
- Any strategy expression.
- Returns:
- The metarepresented strategy or null.
-
unify
Solves the given unification problem.
- Parameters:
problem
- A list of pairs of terms to be unified.irredundant
- Whether to compute a minimal set of unifiers.
- Returns:
- An object to iterate through unifiers.
-
unify
Solves the given unification problem.
- Parameters:
problem
- A list of pairs of terms to be unified.
- Returns:
- An object to iterate through unifiers.
-
variant_unify
public VariantUnifierSearch variant_unify(TermPairVector problem, TermVector irreducible, boolean filtered) Solves the given unification problem using variants.
- Parameters:
problem
- A list of pairs of terms to be unified.irreducible
- Irreducible terms.filtered
- Whether to compute a minimal set of unifiers.
- Returns:
- An object to iterate through unifiers.
-
variant_unify
Solves the given unification problem using variants.
- Parameters:
problem
- A list of pairs of terms to be unified.irreducible
- Irreducible terms.
- Returns:
- An object to iterate through unifiers.
-
variant_unify
Solves the given unification problem using variants.
- Parameters:
problem
- A list of pairs of terms to be unified.
- Returns:
- An object to iterate through unifiers.
-
variant_match
Computes a complete set of order-sorted matches modulo the equations
declared with the variant attribute (which must satisfy the finite
variant property) plus the (supported) equational axioms in the
given module.
- Parameters:
problem
- A list of pairs of terms to be matched.irreducible
- Irreducible terms.
- Returns:
- An object to iterate through unifiers.
-
variant_match
Computes a complete set of order-sorted matches modulo the equations
declared with the variant attribute (which must satisfy the finite
variant property) plus the (supported) equational axioms in the
given module.
- Parameters:
problem
- A list of pairs of terms to be matched.
- Returns:
- An object to iterate through unifiers.
-
vu_narrow
public NarrowingSequenceSearch vu_narrow(TermVector subject, SearchType type, Term target, int depth, int flags) Narrowing-based search of terms that unify with the given target
with multiple initial states.
- Parameters:
subject
- Subject terms where to start the search.type
- Type of the search (number of steps).target
- Term that found states must unify with.depth
- Depth bound (-1
for unbounded)flags
- Narrowing search flags (fold
,vfold
,path
,delay
, orfilter
flag).
-
vu_narrow
public NarrowingSequenceSearch vu_narrow(TermVector subject, SearchType type, Term target, int depth) Narrowing-based search of terms that unify with the given target
with multiple initial states.
- Parameters:
subject
- Subject terms where to start the search.type
- Type of the search (number of steps).target
- Term that found states must unify with.depth
- Depth bound (-1
for unbounded)
-
vu_narrow
Narrowing-based search of terms that unify with the given target
with multiple initial states.
- Parameters:
subject
- Subject terms where to start the search.type
- Type of the search (number of steps).target
- Term that found states must unify with.
-
toLatex
Obtain the LaTeX representation of this module.
- Parameters:
all
- Whether to show all statements by transitivity.
-
toLatex
Obtain the LaTeX representation of this module.
-
toString
-