When attempting a recursive call for the second time, the same meta was reused, resulting in trying to solve _X with foo _X, constructing an infinite term
Recursive calls were not guaranteed to be terminating, resulting in loops like:
foo x (c y) = _1
_1 := foo y _2 -- Mimer considered this an ok recursive calls because y is under a constructor
_2 := c y -- Constructor applied to variables is always a good solution
The first problem was caused by a minor oversight in how recursive call components were reused and easy to fix.
The second problem is fixed by restricting variables in recursive calls to their original argument position. In the example above only foo _2 y would be considered a valid recursive call.
This PR also improves the debug logging of Mimer, introducing a mimer.trace debug level (between 10 and 60) that produces a human readable trace of what the proof search is doing.
Fixes #7116
There were two problems:
_Xwithfoo _X, constructing an infinite termThe first problem was caused by a minor oversight in how recursive call components were reused and easy to fix.
The second problem is fixed by restricting variables in recursive calls to their original argument position. In the example above only
foo _2 ywould be considered a valid recursive call.This PR also improves the debug logging of Mimer, introducing a
mimer.tracedebug level (between 10 and 60) that produces a human readable trace of what the proof search is doing.