Allow syntactic abstraction of refinements via "Interpreted" Functions dfn

[ranjitjhala]

I've keenly felt the absence of this feature for awhile -- it lets you lift common patterns into flux-level functions which are really macros that get inlined into the relevant places in the specifications. See

• flux-tests/tests/pos/surface/ealias00.rs
• flux-tests/tests/pos/surface/ealias01.rs
• flux-tests/tests/pos/surface/ealias02.rs

(and neg versions)

Mostly self contained in the expand.rs so we can easily revert later.

Note: The one thing I cannot figure out is the bizarre DefinitionCycle error - which is thrown if you have cyclic / mutually recursive dfn . Currently, I get some strange cannot find fluent bundle run-time error, so just using the panic! till this gets sorted out later.

[nilehmann]

@ranjitjhala I have one major comment

[ranjitjhala]

btw, this PR was somewhat motivated by wanting to do this example

43bfa89#diff-b41377276614e16abfd86f1948720ceef91e72bae75241b28898b0b49cad0e9a

it would be nice I think at some future point to not have to "duplicate" the definitions of is_leap_year and such... maybe with some macro tricks?

[ranjitjhala]

@nilehmann - I shifted all the stuff to rty level - very civilized & pleasant to use the TypeFolder API!

[ranjitjhala]

Still have to keep the Span to fail for cyclic defns - in theory could check that in FHir but that seems like gross duplication…

[nilehmann]

@ranjitjhala A couple of suggestions, but otherwise looks good.

re keeping spans in rty: In theory, we still have the span in the fhir::Map, so we could look it up for error reporting. This is perhaps cleaner, but more cumbersome. We do something similar for reporting errors on invariants https://github.com/liquid-rust/flux/blob/e03dd11fe7ee909a9cdc7b0c92a06b435eb87026/flux-typeck/src/invariants.rs#L21 No strong feelings about this one.

[nilehmann]

I prefer def over dfn. Mentally, I parse dfn as an acronym. But no strong feelings about this one.

note: For a while, I've been feeling that it wasn't such a good idea to have separate attributes for everything. Maybe flux::sig, flux::field, flux::variant and flux::refined_by work, but for these top-level definitions we could have a single attribute and parse different items, e.g.,

#![flux {
    fn nat(x: int) -> bool {
        x >= 0
    }
    
    fn uninterpreted(x: int) -> bool;
    
    qualif MyQ1(x: int, a: int)  {
        x == a + FORTY_TOO
    }
}]

[ranjitjhala]

interesting thought! It does seem a lot cleaner.

btw, if you saw the date.rs test there is a bunch of "duplication" so I wonder if instead we should use a macro like Prusti so:

flux::def! { fn nat(x: i32) -> bool { 0 <= x } } 

Generates both the flux-level def and the rust-level fn ?

Something to ponder...

[ranjitjhala]

Ah, yes I think I picked dfn vs ufn but I just realized your point is you can just use fn and disambiguate based on presence of definition! Definitely better.

[ranjitjhala]

I missed the bit about re keeping spans in rty -- by "this is cleaner" do you mean
(a) keeping the Span in rty or
(b) using the Map

I totally forgot about the Map thing, so yes we can definitely use that, but didn't
follow which one you thought is cleaner -- (I assume you meant using the Map
to avoid duplicating the Span?)

Btw, the real puzzler for me is the "missing fluent bundle" thing, I could never figure
that out so have left the cycle error as a panic for now :-( ...

[nilehmann]

I think (b) is cleaner, but if it makes the code much more complicated, having the Span in rty is not that big of a deal I guess.

Were you emitting the error with FluxSession::emit or with tcx.sess().emit()? this is one reason I can think of you could be getting a missing fluent bundle. You have to use the emit in FluxSession

[ranjitjhala]

Sounds good I’ll try to fix these two first thing tomorrow!

…

On Thu, Dec 8, 2022 at 8:18 PM Nico Lehmann ***@***.***> wrote: I think (b) is cleaner, but if it makes the code much more complicated having the Span in rty is not that big of a deal I guess. Were you emitting the error with FluxSession::emit or with tcx.sess().emit()? this is one reason I can think of you could be getting a missing fluent bundle. You have to use the the emit in FluxSession — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/liquid-rust/flux/pull/238*issuecomment-1343826359__;Iw!!Mih3wA!AVGg8bJgNEjKfslST2JL7gVVYCbfKjOOwbggomzuyMfPIb0ACVP5_1sxTbiqJyYB_idf4JZtYSM5s1_e5laAhXAf$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4ODWHFNOYTXTEPCBPW3WMKXH7ANCNFSM6AAAAAASSR3QOI__;!!Mih3wA!AVGg8bJgNEjKfslST2JL7gVVYCbfKjOOwbggomzuyMfPIb0ACVP5_1sxTbiqJyYB_idf4JZtYSM5s1_e5gabp4qS$> . You are receiving this because you modified the open/close state.Message ID: ***@***.***>