The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I am using extraction into OCaml quite a bit, and one thing I am wondering about is if there is any way to get the extraction of anonymous and local functions (such as those generated by induction) to not be so underscore-happy.  With the extraction of named global functions, Coq does a very good job of pruning out any and all arguments that have no runtime content (like Prop terms).  But, for anonymous and local functions, it just replaces them with underscores, as in the following:

let union t1 t2 =
  let rec f x =
    let recurse = fun y -> f y in
    (fun _ _ _ t3 t4 ->
    match break ordA treeA t3 with
    | BreakLeaf -> t4
    | BreakNode (tl, d, tr) ->
      let Split (found, x0, x1) = split d t4 in
      let x2 = recurse __ __ __ __ tl x0 in let x3 = recurse __ __ __ __ tr x1 in join ordA treeA x2 d x3)
  in f __ __ __ __ t1 t2

The annoying thing is: with named functions, if this was happening, I could probably use Extraction Implicit to fix it.  But I don't see how that could work with anonymous or local functions.

I know the underscores don't do anything - and the OCaml compiler most likely eliminates them - so concern about this can't be very high, but I figured I'd ask anyway.  Keeping the extracted OCaml code as readable as possible is providing surprising benefits to my project.

-- Jonathan