Search tree module

[EmilyOng]

Sample program: foldr_length

Note 1

Proof is currently at: [any; unfold rhs] ex v92 v93; req emp; ens tail(xs)=v93/\is_cons(xs)=true; length(v93, v92); ex r; req emp; Norm(r=1+v92/\res=r+init)

Now, the proof succeeds but all does not seem to be respected (because it has a failed any child, hidden due to compact search tree representation). Shouldn't it be ✘?

Note 2

The ✔ [all; unfold lhs] ex v53; req emp; Norm(is_nil(xs)=true/\res=init) flow is marked to succeed though it has an unverified any. Below is a non-compact tree representation.

(tracing) State update over here https://github.com/EmilyOng/AlgebraicEffect/blob/StagedSL/parsing/search.ml#L80

[EmilyOng]

Another question for take_skip

[any; disj rhs] Norm(res=[]) is marked as failed prematurely, should the subsequent flows still be tried?

[dariusf]

"any" means that the parent goal succeeds if any child succeeds. In other words, any of the nodes marked "any" have to succeed.

I went through all 3 examples and think they are correct under this interpretation. For example, in the last one, the "any" has failed because all its children have to succeed, which is no longer possible.

Anyway, I agree that it's confusing. I've tweaked the drawing, hopefully it's more intuitive (and less noisy) now. If not we can always change it back/further.

[EmilyOng]

Thanks very much!