Hi everyone, I had a question and wanted to know if this was the right place to ask. I'm currently working on extracting some Coq code to OCaml, and am running into an issue trying to extract the
fold_left Coq term to OCaml's List.fold_left.
The Coq fold_left has the type signature
(A -> B -> A) -> List B -> A -> A
but the OCaml List.fold_left has the signature
('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
Since the arguments are in the wrong order, I can't actually run
Extract Inlined Constant fold_left => "List.fold_left"
since the arguments in the wrong order.
Is there a way to extract something inline in such a way that it will switch the argument order around when the ML code is generated?
Can't you write
Extract Inlined Constant fold_left => "(fun f l a -> List.fold_left f a l)"?
The optimizer will certainly do the beta-reduction.
Gotcha, I will give it a shot. It'll take a fair bit of time for me to make the other changes I need to be able to test, but thanks for the suggestion!
In the spirit of trying to fully understand: do you expect
List.fold_left to be faster than the Coq implementation? I am skeptical that they are different in any significant way.
This is part of a larger program, where I (and I say "I", but technically other members of my research team. I didn't write the Coq code, I was just given the task of fixing the extraction) am writing a large, verified program to do something and then extract the entire program to OCaml. That way the extracted program can be run without needing to re-check all the proofs
So I'm not worried necessarily worried about
List.fold_left being faster, since it's a small part of a much larger section of code
What do you hope to gain from using the OCaml
List.fold_left rather than the extracted Coq
Huh, I didn't really think about just extracting Coq
fold_left. I'm not the author of this code segment, but the original author did the
Extract Inlined Constant to OCaml's
List.fold_left. I don't know if they had a compelling reason to do that over extracting Coq
fold_left. I will make a note to ask them later.
Also, an extraction question that likely doesn't warrant it's own thread: I need to extract
<= over Z, specifically
Z.leb, to OCaml to operate on OCaml int. Currently, it is:
Extract Inlined Constant Z.leb => "(<=)".
This works more or less, but in certain cases, specifically if the expression is inside an
if statement, the operator precedence (I think ) means that something like:
if (<=) a b then [...]
the OCaml compiler isn't able to understand and will compiler error, saying:
Error: This expression has type 'a -> 'a -> bool but an expression was expected of type int
Manually changing to
if a <= b then [...]
Is there a way to extract in such a way I can get the
Z.leb extracted for this kind of expression? Or is my problem in some other area? Should I maybe swap to creating my own non-inlined function call?
let () = if (<=) 1 2 then Printf.printf "HI\n" else Printf.printf "X_X"
works fine for me
b look like for you?
Interesting. My extracted expression looks more like this, inside a larger function (this expression is part of an if statement itself)
then let o = <<< a complex expression that has type int>>> in if (<=) -1024 o then (<) o 1024 else false
a is an integer constant,
b is a definition of something that should have type
I haven't played more with just an OCaml scratch code, so I might do that more later as time permits.
looks like it doesn't like the
-, you need something like
(<=) (-1024) o
I don't know if that's an ocaml bug or an extraction bug or a bug in your Extraction instructions
Interesting, I will give that a look. Thanks!
I don't think Coq knows how to extract literal constants, and OCaml is right to complain, so I would say: neither of them. I wonder if this is not hardcoded in the
.v file, something like
Extract Constant minint "-1024".
The constants definitely are hardcoded as translation from Coq constant to OCaml integer constant. Since it's a long program, there is a pretty long list of said constants. In the process of working on this project, I've found at least one bug where something in the Coq code was using a number and not the constant, which caused the extraction to break.
Both constants are declared in Coq as
Definition Z1024 := 1024. Definition Z_1024 := -1024. (* other code *) Extract Inlined Constant Z1024 => "1024". Extract Inlined Constant Z_1024 => "-1024".
@Gaëtan Gilbert It looks like it really was the
-, changing the extracted code to the
(<=) (-1024) o fixed that. So changing the extraction to
Extract Inlined Constant Z_1024 => "(-1024)".
fixed it. Thanks so much!
Extracting Coq Z to OCaml int looks like looking for trouble to me...
It's definitely been a fair bit of trouble. It's slightly frustrating how close Coq and OCaml are, since it makes the differences all the more frustrating.
Right now, the last extraction bug I need to fix for this program is finding some way to extract Coq's
Z.pow, but that is more of a problem because OCaml's standard library doesn't, as far as I have found, have an exponent function that is
int -> int -> int. OCaml's
Zarith library has a
Z.pow that is
Z.t -> int -> Z.t, and the
( ** ) operator is
float -> float -> float. Which is an OCaml problem more than a Coq and Coq extraction problem, as far as I can tell.
I meant that whatever you proved in Coq using Z is not semantically preserved by extraction.
In the Coq code, the exponent only shows up as
2 ^ 20 and
2 ^ 30, so I'm going to speak with the author about just inlining the constant. Or maybe having in Coq:
Definition my_cool_constant := 2^20. (* *) Extract Inlined Constant my_cool_constant => "1048576".
I don't know if that will affect the proof, or how much they want me to change the Coq source.
@Pierre-Marie Pédrot Right. I believe the general idea with this specific thing is that Z being not semantically preserved by extraction was going to be okay, as long as the extraction was reasonably clear and logical. That the loss of assurance would be a reasonable cost. It's generally not my decision on this project, though.
Alright, I got the extraction working! Thanks so much, everyone! All this was information I couldn't find anywhere else or don't have the experience for, so I greatly appreciate everyone taking time to help me.
Last updated: Jan 27 2023 at 02:04 UTC