Add extract_as attribute.

[gebner]

To quote the documentation for the attribute:

(** Replaces the annotated definition
    by the specified implementation during extraction.
    There are no checks whether the implementation
    has the same semantics, or even the same type.

    For example, if you have:

    [@@extract_as (`(fun (x: nat) -> "not a number"))]
    let add_one (x: nat) : nat = x + 42

    Then `add_one` will extract to `let add_one x = "not a number"`,
    and most likely cause the extracted program to crash.

    Note that the argument needs to be a literal quotation.
 *)

[W95Psp]

That looks pretty cool, I'm thinking: this kind of lightweight OCaml "FFI" directly in the compiler F* sources would be kind of awesome, right? 😃

[gebner]

To be clear: this attribute does not replace F* by OCaml. It replaces F* by some other F* code. This is mainly useful when you have a type with extra structure that you want to forget during extraction; in Pulse we have the stt type which comes with extra separation logic pre- and postconditions and we just want to forget about the separation logic stuff during extraction.

For backend-specific implementations, you'd want a different attribute. Maybe something like [@@inline_asm_for "OCaml" "fun x -> \"not a number\""]. Where the code in the second string is actual OCaml code (which can then refer to whatever OCaml libraries you'd like).

[gebner]

@mtzguido Do you have any thoughts on this?

[mtzguido]

Thanks Gabriel, this looks good, just wondering about that true boolean.

More high-level I was wondering if we could have implemented this by using Syntax.Visit.visit_tm to just replace each fvar by its extract_as just before extracting, but that will not interact well with normalization. If we did extraction into OCaml incrementally, and did inlining over the OCaml AST, I think that would work and be easier, but that's for another day : ).

[mtzguido]

The true is interesting here, so we always mark it recursive? Can it really be so since the term that is the argument to extract_as cannot mention the name of this sigelt (without pack_fv trickery)?

[mtzguido]

In any case it's not a big deal, but maybe worth a comment in the attribute's doc and/or here.

[gebner]

As mentioned offline, the implementation can indeed be recursive. This is for example the case with recursive Pulse functions.

I have added a comment to both the attribute and the fixup function here.

[mtzguido]

Not a big deal but probably better to avoid these back-and-forth changes within a PR.

[gebner]

I was going by the contribution guidelines. We should probably update them now.

[mtzguido]

I rebased this btw. If we add a comment about the recursive bit being set then I'm happy merging.

Also: check-world run https://github.com/FStarLang/FStar/actions/runs/11058160723

[kant2002]

I definitely would like to see [@@inline_asm_for "FSharp" "fun x -> \"not a number\""]