Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

You can check whether a lhs pattern matches a particular subject with 
the match and xmatch commands.

At the metalevel, metaApply and metaXapply will let you attempt to 
rewrite with a rule having a given label.

The x part refers to whether you need extension for operators with the 
associative attribute; i.e. whether
you allow matches of a subterm having the same top operator rather than 
the whole term
for a subject headed by an associative or AC operator.

Steven

On 5/11/15, 1:15 PM, Vladimir Klebanov wrote:
> Hi,
>
> I am trying to debug a module with some rules, and in the process I am
> looking for a way to achieve the following.
>
> I would like to give Maude a term and the name of a rule (defined in
> the module) and Maude would tell me if this rule is applicable to the
> term and, if so, what a (or the) result would be. Is there a way to do
> this? I did not find a solution in the manual.
>
> The background is that I am using search, but my rules are buggy, and
> no solution is found, even though the domain knowledge suggests that
> there is one. I want to reenact the solution I have in mind in Maude
> to see where rewriting fails. So far I do not see a good way to do
> this. The mechanism above would help, but other suggestions are also
> very welcome.
>
> Thanks!
>
> Vladimir