search

hazelgrove / hazel

Hazel, a live functional programming environment with typed holes
http://hazel.org/
MIT License
684 stars 45 forks source link

prevent unnecessary fixpoints in elaboration #1274

Closed pigumar1 closed 1 month ago

pigumar1 commented 2 months ago

This PR tries to fix #1268 by checking if there are self-references in the function body/bodies during elaboration and decide whether to include the fixpoint based on that information.

For potential mutual recursive functions, the fixpoint is included as long as one of the function names occur in the definition as a free variable (by looking at the co-context)

A non-recursive function: image

A recursive function: image

Non-recursive functions: image

Mutual recursive functions: image

pigumar1 commented 2 months ago

image I'm not sure whether Alcotest should fail here: it seems that in this case, there is no reference of f in the body of the function (BinIntOp (Plus, (IntLit 1), (BoundVar "x"))). Should we wrap it with a fixpoint?

cyrus- commented 2 months ago

@pigumar1 That test should be updated with the new behavior.

cyrus- commented 2 months ago

@pigumar1 marking as draft until the test is updated