coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Daniel Schepler <dschepler AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] erased args in extracted anon funs
- Date: Mon, 14 Jul 2014 17:29:37 -0700
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
>
- [Coq-Club] erased args in extracted anon funs, Jonathan, 07/06/2014
- Re: [Coq-Club] erased args in extracted anon funs, Daniel Schepler, 07/15/2014
Archive powered by MHonArc 2.6.18.