Stream: Coq users

Topic: Extraction to List.fold_Left


view this post on Zulip Daniel Garcia (Feb 04 2021 at 00:04):

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?

view this post on Zulip Cody Roux (Feb 04 2021 at 01:53):

Can't you write Extract Inlined Constant fold_left => "(fun f l a -> List.fold_left f a l)"?

view this post on Zulip Cody Roux (Feb 04 2021 at 01:54):

The optimizer will certainly do the beta-reduction.

view this post on Zulip Daniel Garcia (Feb 04 2021 at 02:45):

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!

view this post on Zulip Cody Roux (Feb 04 2021 at 03:40):

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.

view this post on Zulip Daniel Garcia (Feb 04 2021 at 03:46):

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

view this post on Zulip Daniel Garcia (Feb 04 2021 at 03:47):

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

view this post on Zulip Jasper Hugunin (Feb 04 2021 at 04:58):

What do you hope to gain from using the OCaml List.fold_left rather than the extracted Coq fold_left?

view this post on Zulip Daniel Garcia (Feb 04 2021 at 05:51):

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.

view this post on Zulip Daniel Garcia (Feb 04 2021 at 06:19):

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 [...]
compiles correctly.

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?

view this post on Zulip Gaëtan Gilbert (Feb 04 2021 at 08:58):

let () =
  if (<=) 1 2 then Printf.printf "HI\n"
  else Printf.printf "X_X"

works fine for me
what do a and b look like for you?

view this post on Zulip Daniel Garcia (Feb 04 2021 at 14:38):

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

so a is an integer constant, b is a definition of something that should have type int.

I haven't played more with just an OCaml scratch code, so I might do that more later as time permits.

view this post on Zulip Gaëtan Gilbert (Feb 04 2021 at 14:45):

looks like it doesn't like the -, you need something like (<=) (-1024) o

view this post on Zulip Gaëtan Gilbert (Feb 04 2021 at 14:46):

I don't know if that's an ocaml bug or an extraction bug or a bug in your Extraction instructions

view this post on Zulip Daniel Garcia (Feb 04 2021 at 14:51):

Interesting, I will give that a look. Thanks!

view this post on Zulip Guillaume Melquiond (Feb 04 2021 at 14:52):

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".

view this post on Zulip Daniel Garcia (Feb 04 2021 at 14:54):

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".

view this post on Zulip Daniel Garcia (Feb 04 2021 at 15:07):

@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!

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2021 at 15:11):

Extracting Coq Z to OCaml int looks like looking for trouble to me...

view this post on Zulip Daniel Garcia (Feb 04 2021 at 15:16):

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.

view this post on Zulip Pierre-Marie Pédrot (Feb 04 2021 at 15:18):

I meant that whatever you proved in Coq using Z is not semantically preserved by extraction.

view this post on Zulip Daniel Garcia (Feb 04 2021 at 15:19):

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.

view this post on Zulip Daniel Garcia (Feb 04 2021 at 15:21):

@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.

view this post on Zulip Daniel Garcia (Feb 04 2021 at 16:11):

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