print successful non-branching sub-strategy
Once we have found a proof, we would love to have a strategy expression that finds exactly this proof, without useless work.
This means: replace each Or_Else
, Seq
and First_Of
with the stragegy for the succesful argument.
Also, some things need to be expanded: if a defined name contains a choice node (that will be replaced), the replacement may be different for each usage of that name.
Ha! There is currently one AST node that cannot be expanded: a Branchformer
(only example: EDG decomposition) creates a list of sub-goals, and solves them all, using the same method (transformer, then recurse) for each. But that method might contain choices, and these might turn out different for each sub-goal.
So - we need a non-recursive Branchformer that takes a list of sub-methods. This will look strange (the branchformer seems to know the number of sub-goals) but so be it.