Accumulators as functions base - #22345
Conversation
|
I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor. |
coqbot-app
Bot
added
the
needs: full CI
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
|
@coqbot bench |
| (* Compiles an unsigned int to malfunction code *) | ||
| let compile_mlf i = | ||
| if i >= 0 then Printf.sprintf "(apply (global $Uint63 $of_int) %i)" i | ||
| else Printf.sprintf "(apply (global $Uint63 $of_int) (neg %i))" (-i) |
There was a problem hiding this comment.
Does this code work properly for minint?
| (** differentiates an accumulator from a closure. Should only be used on memory blocks. *) | ||
| and is_accu v = | ||
| let reference = Obj.repr @@ build_accu (Obj.magic 0) in (* we assume Ocaml will build all accumulators similarly *) | ||
| Obj.size v = Obj.size reference && Obj.field v 0 == Obj.field reference 0 (* we check the equality of the function pointer *) |
There was a problem hiding this comment.
This seems quite fragile to me. Even with inline never, there is no guarantee that the function will be uniquely defined. (In fact, it is not uncommon for OCaml functions to be duplicated, so as to support both fast, direct calls and calls through first-order modules.) I don't know of a way to ensure that only a single occurrence exists. Perhaps the build_accu function should also be part of a once generated malfunction code?
| if f < 0. then Printf.sprintf "(apply (global $Float64 $of_float) neg_infinity)" | ||
| else Printf.sprintf "(apply (global $Float64 $of_float) infinity)" | ||
| end else if f < 0. then Printf.sprintf "(apply (global $Float64 $of_float) (neg.f64 %.17e))" (-. f) (* malfunction supports scientific notation *) | ||
| else Printf.sprintf "(apply (global $Float64 $of_float) %.17e)" f |
There was a problem hiding this comment.
There have been bugs in the past when using the decimal scientific notation to perform a roundtrip (i.e., you would get a close but different number, especially for subnormal floating-point numbers). I don't know how safe it is nowadays. Does the malfunction compiler not support the hexadecimal notation?
github-actions
Bot
added
the
needs: rebase
Is now able to compile strings, floats and sequences of mllambda to malfunction
…ld have two dolla sign in front of them
…ted as $() instead of 0
… in a different function to stay compatible with extraction
…ger needed, and removed the useless import of Constructs
…ns that would break our accumulator detection
6257002 to
516eeae
Compare
|
I am not triggering a CI run on this PR because the CI configuration has been modified. CI can be triggered manually by an authorized contributor. |
coqbot-app
Bot
added
needs: full CI
3 participants
Hi, this is the branch with the change in representation of accumulators