Maude-help mailing list

[Andrew Cholewa <acholew2 AT illinois.edu>]

Expanding on what Steven Eker wrote:

The xmatch command:

xmatch pattern <=? subject-term {such that condition} .

You can find it under chapter 23.3: Matching commands (of the Maude book, not sure if it's the same in the online manual)

pattern is the lefthand side of the rule you'd like to check, while subject-term is the term you actually want to rewrite.

condition is the condition being used by your rule if you're trying to check a conditional rule.

If there is a match, then Maude will print out all the matching substitutions. If there is no match, Maude will return something like "no match."

Unfortunately, you need to copy the lefthand side of the rule explicitly, you can't write something like:

mod BLAH is
...
rl [maRule] : Blah => Blah .

endm

xmatch maRule <=? f(x) .

You'll need to use the metalevel if you want to do that (not worth it in my opinion).

Unfortunately, this command doesn't tell how you the match failed, just that it failed. To handle that, I will usually simplify the subject-term by replacing subterms with variables of the correct sort until a match is successful. Then I begin iteratively re-instantiating those variables until the match fails. At that point, I know which subterm is giving me problems.

Andrew

On 05/11/2015 03: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