The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Hi, I've been experimenting with a tree-based representation of a
"vector A n" type, in order to allow for efficient random access to an
element.  The idea is that it uses the structure of an element of
positive directly as instructions for how to traverse the tree; thus,
for example, element 1 is the root, the left subtree contains even
numbered elements, and the right subtree contains odd numbered
elements other than the first.  (See attached TreeVector.v.)  Anyway,
my question is: why does tree_vector_index_safe extract as

(** val tree_vector_index_safe :
    n -> 'a1 tree_vector -> positive -> 'a1 option **)

let rec tree_vector_index_safe n0 t i =
  match t with
  | Null -> None
  | Internal_node (wildcard', l, x, r) ->
    (match i with
     | XI j ->
       let filtered_var = tree_vector_index_safe (pm1_half wildcard') r j in
       (match filtered_var with
        | Some y -> Some y
        | None -> None)
     | XO j ->
       let filtered_var = tree_vector_index_safe (phalf wildcard') l j in
       (match filtered_var with
        | Some y -> Some y
        | None -> None)
     | XH -> Some x)

I know that in some other circumstances I've seen the extractor
optimize things like this to something more like:

let rec tree_vector_index_safe n0 t i =
  match t with
  | Null -> None
  | Internal_node (wildcard', l, x, r) ->
    (match i with
      | XI j -> tree_vector_index_safe (pm1_half wildcard') r j
      | XO j -> tree_vector_index_safe (phalf wildcard') l j
      | XH -> Some x)

So why isn't it able to do so in this case?  (This is with version 8.4pl2.)

Also, on a side note, I've been toying with the idea of making the
"Extraction Ignore" mechanism more flexible by being able to tag
certain arguments of constructors or functions as something like
"noextract N" and having Coq reject definitions where the extraction
would depend on the value of the parameter -- similar to what's
currently done with forbidding extracting proof structure to Type,
though I haven't worked out the full details of what rules would be
needed.  So for example, I would be able to eliminate the "wildcard'"
and "n0" arguments in the above.  Any thoughts on how hard it would be
to implement something like this as an extension to the Coq kernel?
-- 
Daniel Schepler

Attachment: TreeVector.v
Description: Binary data