The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I just happened to run into this recently, doing some experiments with
an alternate definition of Pos.lt, and then a reimplementation of
Pos.compare using the same algorithm.

Require Import ZArith.

Open Scope positive_scope.

Inductive Plt : positive -> positive -> Prop :=
| Plt_1_p0 p : Plt 1 (p~0)
| Plt_1_p1 p : Plt 1 (p~1)
| Plt_Plt_0_0 p q : Plt p q -> Plt (p~0) (q~0)
| Plt_Plt_0_1 p q : Plt p q -> Plt (p~0) (q~1)
| Plt_Plt_1_0 p q : Plt p q -> Plt (p~1) (q~0)
| Plt_Plt_1_1 p q : Plt p q -> Plt (p~1) (q~1)
| Plt_p0_p1 p : Plt (p~0) (p~1).

Inductive Pos_comparison (p q : positive) : Set :=
| IsLt : Plt p q -> Pos_comparison p q
| IsEq : p = q -> Pos_comparison p q
| IsGt : Plt q p -> Pos_comparison p q.

Require Import Program.

Obligation Tactic := program_simpl; eauto using Plt.
Program Fixpoint pos_compare_aux (p q : positive)
  {p0 q0 : positive} (_ : Plt p q -> Plt p0 q0)
  (_ : Plt q p -> Plt q0 p0) (eq_case : p = q -> Pos_comparison p0 q0) :
  Pos_comparison p0 q0 :=
match p, q with
| 1, 1 => eq_case _
| 1, q'~0 => IsLt _ _ _
| 1, q'~1 => IsLt _ _ _
| p'~0, 1 => IsGt _ _ _
| p'~1, 1 => IsGt _ _ _
| p'~0, q'~0 => pos_compare_aux p' q' _ _ (fun _ => eq_case _)
| p'~0, q'~1 => pos_compare_aux p' q' _ _ (fun _ => IsLt _ _ _)
| p'~1, q'~0 => pos_compare_aux p' q' _ _ (fun _ => IsGt _ _ _)
| p'~1, q'~1 => pos_compare_aux p' q' _ _ (fun _ => eq_case _)
end.

Program Definition pos_compare (p q : positive) :
  Pos_comparison p q :=
pos_compare_aux p q _ _ (fun _ => IsEq _ _ _).

Extraction Implicit pos_compare_aux [p0 q0].

Recursive Extraction pos_compare.
==>
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type positive =
| XI of positive
| XO of positive
| XH

type pos_comparison =
| IsLt
| IsEq
| IsGt

(** val pos_compare_aux :
    positive -> positive -> (__ -> pos_comparison) -> pos_comparison **)

let rec pos_compare_aux p q eq_case =
  match p with
  | XI p' ->
    (match q with
     | XI q' -> pos_compare_aux p' q' (fun _ -> eq_case __)
     | XO q' -> pos_compare_aux p' q' (fun _ -> IsGt)
     | XH -> IsGt)
  | XO p' ->
    (match q with
     | XI q' -> pos_compare_aux p' q' (fun _ -> IsLt)
     | XO q' -> pos_compare_aux p' q' (fun _ -> eq_case __)
     | XH -> IsGt)
  | XH ->
    (match q with
     | XH -> eq_case __
     | _ -> IsLt)

(** val pos_compare : positive -> positive -> pos_comparison **)

let pos_compare p q =
  pos_compare_aux p q (fun _ -> IsEq)

I agree that it would be nice to be able to have the extraction drop
the proof argument of the eq_case argument.
-- 
Daniel Schepler

On Sat, Jul 5, 2014 at 7:10 PM, Jonathan 
<jonikelee AT gmail.com>
 wrote:
> 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
>