The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 26 Apr 2012 11:39:41 -0700,
Daniel Schepler 
<dschepler AT gmail.com>
 a écrit :

> Suppose I define a bst_insert function as in the attached file, and
> then in the extraction I want to drop the l and r parameters in the
> binary_search_tree type and the bst_insert function.  First of all,
> this doesn't work the way I'd expect:
> 
> Extraction Implicit empty_bst [l r].
> Extraction Implicit bst_node [l r].
> 
> It looks like it's making nothing implicit in empty_bst, and the wrong
> arguments implicit in bst_node.  (Looks like a probable bug.)  I can
> fix that by instead saying:
> 
> Extraction Implicit empty_bst [1 2].
> Extraction Implicit bst_node [1 2].

Neither of them works on my coq version (an "old" 8.4 trunk)

> Then the extraction of the binary_search_tree type looks like what I'd
> expect.  But I haven't been able to find any Extraction Implicit
> declarations which will allow bst_insert to extract, using either
> parameter names or parameter numbers.
> 
> Also, on a minor note, would there be any way to get rid of the type
> dependency in comparison_pf, which doesn't make sense in the extracted
> version?
> 
> (All this is using 8.3pl4.)

I think you cannot naïvely remove [l] and [r] from binary_search_tree
without having bad surprises.

Consider the following code:

===============

Definition ub l r (t : binary_search_tree l r) : option A :=
  match t with
  | empty_bst _ up => up
  | bst_node _ up _ _ _ _ => up
  end.
End binary_search_tree.

Extraction ub.

»let ub l r = function
»| Empty_bst (l0, up) -> up
»| Bst_node (l0, up, x, b, b0) -> up

==============

Of course it is equivalent to the following one:

Definition ub l r (t : binary_search_tree l r) : option A :=
  match t with
  | empty_bst _ _ => r
  | bst_node _ _ _ _ _ _ => r
  end.

But I think that the Extraction should do some quite smart things to
realise it and translate it into a code without which does not require
[l] and [r] as indice.

Of course, you could define an extraction as a partial function,
allowed to fail when such a case is encountered, but that also means,
that you will lose some kind of modularity.


=============
For recursive patterns, you need to provide arguments in the same order
(for reasons which are unknown to me).

That is:

Notation "{ x , .. , z } @> f" :=
  ((.. (f x) ..) z)
  (at level 3).

works, but not:

Notation "{ x , .. , z } @> f" :=
  (reverse_appl z (.. (reverse_appl x f) ..))
  (at level 3).

I guess a patch for that would be easy to provide.

(*  Can't get this to work...
Notation "( x , y , .. , z ) @> f" :=
  (reverse_appl z .. (reverse_appl y (reverse_appl x f)) ..)
  (left associativity, at level 91).
*)