Class Module

java.lang.Object
es.ucm.maude.bindings.Module

public class Module extends Object
A Maude module.
  • Method Details

    • delete

      public void delete()
    • getModuleType

      public Module.ModuleType getModuleType()
      Get the module type.

      This allows distinguishing modules from theories, and the
      functional, system and strategy variants within them.
    • getSorts

      public SortVector getSorts()
      Get the sorts declared in the module.
    • getSymbols

      public SymbolVector getSymbols()
      Get the symbols declared in the module.
    • getKinds

      public KindVector getKinds()
      Get the kinds defined in the module.
    • getMembershipAxioms

      public SubsortVector getMembershipAxioms()
      Get the membership axioms defined in the module.
    • getEquations

      public EquationVector getEquations()
      Get the equations defined in the module.
    • getRules

      public RuleVector getRules()
      Get the rules defined in the module.
    • getStrategies

      public StratVector getStrategies()
      Get the strategies declared in the module.
    • getStrategyDefinitions

      public StratDefVector 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

      public Module getParameterTheory(int index)
      Get the theory of the given parameter.
    • getParameterName

      public String getParameterName(int index)
      Get the name of a module parameter.

      Parameters:
      index - Index of the parameter.
    • findSort

      public Sort findSort(String name)
      Finds a sort by its name in the module.

      Parameters:
      name - The name of the sort.

      Returns:
      The sort or null if it does not exist.
    • findSymbol

      public Symbol findSymbol(String name, KindVector domainKinds, Kind rangeKind)
      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

      public Term parseTerm(TokenVector bubble, Kind kind)
      Parse a term.

      Parameters:
      bubble - Tokenized term.
      kind - Restrict parsing to terms of the given kind.
    • parseTerm

      public Term parseTerm(TokenVector bubble)
      Parse a term.

      Parameters:
      bubble - Tokenized term.
    • parseTerm

      public Term parseTerm(String term_str, Kind kind, TermVector vars)
      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

      public Term parseTerm(String term_str, Kind kind)
      Parse a term.

      Parameters:
      term_str - A term represented as a string.
      kind - Restrict parsing to terms of the given kind.
    • parseTerm

      public Term parseTerm(String term_str)
      Parse a term.

      Parameters:
      term_str - A term represented as a string.

    • parseStrategy

      public StrategyExpression parseStrategy(String strat_str, TermVector vars)
      Parse a strategy expression.


      Parameters:
      vars - Variables that may appear without explicit type
      annotation in the strategy.
    • parseStrategy

      public StrategyExpression parseStrategy(String strat_str)
      Parse a strategy expression.


    • downTerm

      public Term downTerm(Term term)
      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 the Term sort in META-TERM.
      This term must belong to a module where the META-LEVEL
      module is included. The term will be reduced.

      Returns:
      The term or null if the metarepresentation was
      not valid.
    • downStrategy

      public StrategyExpression downStrategy(Term term)
      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 the Strategy sort in META-STRATEGY.
      This term must belong to a module where the META-LEVEL
      module is included. The term will be reduced.

      Returns:
      The strategy expression or null if the
      metarepresentation was not valid.
    • upTerm

      public Term upTerm(Term term)
      Get the metarepresentation in this module of a term
      in (possibly) another module. This module must contain
      META-LEVEL.

      Parameters:
      term - Any term.

      Returns:
      The metarepresentation term or null.
    • upStrategy

      public Term upStrategy(StrategyExpression expr)
      Get the metarepresentation in this module of a strategy
      expression in (possibly) another module. This module must
      contain META-LEVEL.

      Parameters:
      expr - Any strategy expression.

      Returns:
      The metarepresented strategy or null.
    • unify

      public UnificationProblem unify(TermPairVector problem, boolean irredundant)
      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

      public UnificationProblem unify(TermPairVector problem)
      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

      public VariantUnifierSearch variant_unify(TermPairVector problem, TermVector irreducible)
      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

      public VariantUnifierSearch variant_unify(TermPairVector problem)
      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

      public VariantUnifierSearch 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.

      Parameters:
      problem - A list of pairs of terms to be matched.
      irreducible - Irreducible terms.

      Returns:
      An object to iterate through unifiers.
    • variant_match

      public VariantUnifierSearch 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.

      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, or filter 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

      public NarrowingSequenceSearch vu_narrow(TermVector subject, SearchType type, Term target)
      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

      public String toLatex(boolean all)
      Obtain the LaTeX representation of this module.

      Parameters:
      all - Whether to show all statements by transitivity.
    • toLatex

      public String toLatex()
      Obtain the LaTeX representation of this module.

    • toString

      public String toString()
      Overrides:
      toString in class Object