Maude-help mailing list

[Paco Durán <duran AT lcc.uma.es>]

Hi Guilherme, 

Debugging shows things that are done, but you seem to want Maude also show 
what is attempted but doesn't happen. I don't think you can get Maude to do 
that for you. I don't know whether it would be at all possible, because in 
general more things that you may think happen under the hood, but may be it's 
worth thinking about it. 

I wonder however whether it wouldn't be enough with a work around. Perhaps it 
does in this case but not in the other more complex examples you refer to. 
What about adding an owise eq

----
fmod EX is
  sort Nat .

  op z : -> Nat [ctor] .
  op s_ : Nat -> Nat [ctor iter] .
  op f : Nat -> Nat .
  var x : Nat .

  ---- added
  op added-for-debugging : -> [Nat] .

  eq f(z) = z .
  eq f(X:[Nat]) = added-for-debugging .
endfm
----

Maude> debug red f(s z) .
debug reduce in EX : f(s z) .
break on symbol: f
Debug(1)> step .
*********** equation
eq f(X:[Nat]) = added-for-debugging .
X:[Nat] --> s z
f(s z)
--->
added-for-debugging
rewrites: 1 in 0ms cpu (14301ms real) (2762 rewrites/second)
result [Nat]: added-for-debugging


Cheers, 

Francisco Durán

> On 10 Jul 2025, at 18:30, Guilherme Horta Alvares Da Silva 
> <alvares AT chalmers.se> wrote:
> 
> I want to debug my Maude program and I want it to show in every equation 
> why it does not pattern match.
> For example:
> ```
> fmod EX is
>   sort Nat .
> 
>   op z : -> Nat [ctor] .
>   op s_ : Nat -> Nat [ctor iter] .
>   op f : Nat -> Nat .
>   var x : Nat .
> 
>   eq f(z) = z .
> endfm
> 
> set break on .
> break select f .
> 
> debug red f(s z) .
> ```
> 
> I would like it to break in the equation f(z), and just says that s z does 
> not match z.
> This example is trivial, but I need this feature for more complex examples. 
> I usually have to manually do a lot ofmatch commands.
> 
> Thank you for reading this question. I didn't find anything the solution in 
> the documentation.