Ssreflect Users Discussion List

[Georges Gonthier <>]

  This is an unfortunate limitation of the implementation of extraction, and 
not per se a problem of the ssreflect library.
Naming structure fields has a significant impact on the efficiency of type 
inference (each named field triggers insertion in the global canonical 
projection table), so the ssreflect library uses them sparingly. The 
extractor needs field names to declare OCaml records, and simply gives up 
rather than either implementing the structure with a single-constructor 
datatype or inventing a field name, on the erroneous assumption that naming 
fields in a Coq library is inconsequential.
  The upshot is that extraction cannot be used for code that actually uses 
the ssreflect "operator" structures such as eqType, finType, ringType, etc.
In the foo2 definition "i'"actually ranges over the ordinal x (or 'I_x) type, 
and the extracted code will iterate over the list extracted from ord_enum x, 
which will be roughly
       pmap (fun i => if i < x then Some i else None) (iota 0 x)
This should be basically the same thing as iota 0 ( x - 0), the list used by 
the foo1 definition, except for the dynamic check for the i < x condition, 
which extraction can't eliminate. As "i < x" is defined as
   i.+1 - x == 0
in the ssrnat library, this check uses the unnamed Equality.class field of 
the nat_eqType canonical instance; this is why you are getting this error 
message.
Even if the definition of "<" did not use the eqType interface, you would get 
a similar complaint concerning the use of the Finite.class field of the 
ordinal_finType instance (whose value is ord_enum x).
  You might perhaps want to file for a feature wish on the Coq bug tracker.

Best,
   Georges

-----Original Message-----
From:  [] 
Sent: 09 June 2011 22:55
To: 
Subject: Extraction problem.

Hi.

I'm tring extraction and find some construct cannot be extracted.

Definition foo1 (x : nat) : nat := \sum_(0 <= i < x) i.
Definition foo2 (x : nat) : nat := \sum_(i < x) i.
Definition foo3 (x : 3.-tuple nat) : nat := \sum_(i <- x) i.

Extraction Language Ocaml.
Extraction "foo.ml" foo1 foo2 foo3.

'foo1' and 'foo3' are extracted correctly, but 'foo2' is not.
Error message is:
==
Error: Record Equality.mixin_of has an anonymous field.
To help extraction, please use an explicit name.
==

Is this an implementation policy?
And is there a way to write program without concern?