Skip to content

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.

Edited by waldmann