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? :smiley:

[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]

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\""]