Allow unfolding of basic non-recursive predicates

[EmilyOng]

Closes #10

Allow unfolding of basic non-recursive predicates by travering the predicate's disj_spec body during instantiation to check if the predicate name occurs in any function stages.

[dariusf]

Thanks! Feel free to merge once you find a good place for find_rec.

[dariusf]

Do we need to set this here? Seems like it should already be set.

[EmilyOng]

Thanks! It is not needed

[dariusf]

On second thought, I think you were right to include it initially... I missed the call to instantiateStages, which can replace higher-order stages and change whether a predicate is recursive. Does that agree with your tests?

[EmilyOng]

Thanks! Sorry for the late reply:

I think adding the assignment here might not help. For example, in this program:

let rec call_ret f n
= if n = 0 then f 100
  else let g = call_ret in g f (n - 1)

let test_non_rec_pred n
(*@ ens res=100 @*)
= let id i = i in

  call_ret id n

We will check if the predicate name call_ret occurs in the following staged specification:

ex v74; ens (n==0)=true; v54(100, v74); ens v52=v74 \/ ex v79 v80 v81; ens (n==0)=false/\v81=call_ret/\v80=n-1; v81(v54, v80, v79); ens v52=v79

Which will be false because call_ret != v81 so p_rec will be wrongly assigned as non-recursive.

I tried to fix this by including an additional visit_Atomic in the visitor, so that it can check for v81=call_ret.

[EmilyOng]

I removed _false and moved this into the test file since this example works now

[EmilyOng]

I see, the existing tests still passed after I removed it. I will try to add an example to see if there will be issues.

…

On Thu, 8 Feb 2024, 18:11 Darius Foo, ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In parsing/entail.ml <#12 (comment)> : > @@ -305,7 +305,7 @@ let instantiate_pred : pred_def -> term list -> term -> pred_def = (string_of_list (string_of_list string_of_staged_spec) bbody); *) bbody in - { pred with p_body } + { pred with p_body; p_rec = (find_rec pred.p_name)#visit_disj_spec () p_body } On second thought, I think you were right to include it initially... I missed the call to instantiateStages, which can replace higher-order stages and change whether a predicate is recursive. Does that agree with your tests? — Reply to this email directly, view it on GitHub <#12 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFBX6KOHLFMWS44DLUYH6U3YSSQG3AVCNFSM6AAAAABCZODXP2VHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTQNRZG42DKNRRGI> . You are receiving this because you authored the thread.Message ID: ***@***.***>