Imported Upstream version 8.5~beta3+dfsg

11 files changed, 187 insertions, 12 deletions

diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index fbcd01a1..cf97ae3a 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -193,7 +193,7 @@ beginning of files. Possible clashes are dealt with.
 in extracted code. 
 
 
-* A few constants are explicitely declared to be inlined in extracted code. 
+* A few constants are explicitly declared to be inlined in extracted code.
 For the moment there are: 
 	Wf.Acc_rec
 	Wf.Acc_rect
@@ -234,12 +234,12 @@ Those two commands enable a precise control of what is inlined and what is not.
 
 Print Extraction Inline. 
 
-Sum up the current state of the table recording the custom inlings 
+Sum up the current state of the table recording the custom inlinings
 (Extraction (No)Inline). 
 
 Reset Extraction Inline. 
 
-Put the table recording the custom inlings back to empty. 
+Put the table recording the custom inlinings back to empty.
 
 As a consequence, there is no more need for options inside the commands of 
 extraction: 
diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/plugins/extraction/ExtrHaskellNatInt.v
new file mode 100644
index 00000000..e94e7d42
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellNatInt.v
@@ -0,0 +1,13 @@
+(** Extraction of [nat] into Haskell's [Int] *)
+
+Require Import Arith.
+Require Import ExtrHaskellNatNum.
+
+(**
+ * Disclaimer: trying to obtain efficient certified programs
+ * by extracting [nat] into [Int] is definitively *not* a good idea.
+ * See comments in [ExtrOcamlNatInt.v].
+ *)
+
+Extract Inductive nat => "Prelude.Int" [ "0" "Prelude.succ" ]
+  "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/plugins/extraction/ExtrHaskellNatInteger.v
new file mode 100644
index 00000000..038f0ed8
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellNatInteger.v
@@ -0,0 +1,13 @@
+(** Extraction of [nat] into Haskell's [Integer] *)
+
+Require Import Arith.
+Require Import ExtrHaskellNatNum.
+
+(**
+ * Disclaimer: trying to obtain efficient certified programs
+ * by extracting [nat] into [Integer] isn't necessarily a good idea.
+ * See comments in [ExtrOcamlNatInt.v].
+*)
+
+Extract Inductive nat => "Prelude.Integer" [ "0" "Prelude.succ" ]
+  "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
new file mode 100644
index 00000000..244eb85f
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -0,0 +1,35 @@
+(**
+ * Efficient (but uncertified) extraction of usual [nat] functions
+ * into equivalent versions in Haskell's Prelude that are defined
+ * for any [Num] typeclass instances.  Useful in combination with
+ * [Extract Inductive nat] that maps [nat] onto a Haskell type that
+ * implements [Num].
+ *)
+
+Require Import Arith.
+Require Import EqNat.
+
+Extract Inlined Constant Nat.add => "(Prelude.+)".
+Extract Inlined Constant Nat.mul => "(Prelude.*)".
+Extract Inlined Constant Nat.max => "Prelude.max".
+Extract Inlined Constant Nat.min => "Prelude.min".
+Extract Inlined Constant Init.Nat.add => "(Prelude.+)".
+Extract Inlined Constant Init.Nat.mul => "(Prelude.*)".
+Extract Inlined Constant Init.Nat.max => "Prelude.max".
+Extract Inlined Constant Init.Nat.min => "Prelude.min".
+Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)".
+Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)".
+Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)".
+Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)".
+Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)".
+Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)".
+
+Extract Constant Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+Extract Constant Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+Extract Constant Init.Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+
+Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
+Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
\ No newline at end of file
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
new file mode 100644
index 00000000..3558f4f2
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -0,0 +1,38 @@
+(**
+ * Special handling of ascii and strings for extraction to Haskell.
+ *)
+
+Require Import Ascii.
+Require Import String.
+
+(**
+ * At the moment, Coq's extraction has no way to add extra import
+ * statements to the extracted Haskell code.  You will have to
+ * manually add:
+ *
+ *   import qualified Data.Bits
+ *   import qualified Data.Char
+ *)
+
+Extract Inductive ascii => "Prelude.Char"
+  [ "(\b0 b1 b2 b3 b4 b5 b6 b7 -> Data.Char.chr (
+      (if b0 then Data.Bits.shiftL 1 0 else 0) Prelude.+
+      (if b1 then Data.Bits.shiftL 1 1 else 0) Prelude.+
+      (if b2 then Data.Bits.shiftL 1 2 else 0) Prelude.+
+      (if b3 then Data.Bits.shiftL 1 3 else 0) Prelude.+
+      (if b4 then Data.Bits.shiftL 1 4 else 0) Prelude.+
+      (if b5 then Data.Bits.shiftL 1 5 else 0) Prelude.+
+      (if b6 then Data.Bits.shiftL 1 6 else 0) Prelude.+
+      (if b7 then Data.Bits.shiftL 1 7 else 0)))" ]
+  "(\f a -> f (Data.Bits.testBit (Data.Char.ord a) 0)
+              (Data.Bits.testBit (Data.Char.ord a) 1)
+              (Data.Bits.testBit (Data.Char.ord a) 2)
+              (Data.Bits.testBit (Data.Char.ord a) 3)
+              (Data.Bits.testBit (Data.Char.ord a) 4)
+              (Data.Bits.testBit (Data.Char.ord a) 5)
+              (Data.Bits.testBit (Data.Char.ord a) 6)
+              (Data.Bits.testBit (Data.Char.ord a) 7))".
+Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)".
+
+Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
+Extract Inlined Constant String.string_dec => "(Prelude.==)".
diff --git a/plugins/extraction/ExtrHaskellZInt.v b/plugins/extraction/ExtrHaskellZInt.v
new file mode 100644
index 00000000..66690851
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellZInt.v
@@ -0,0 +1,24 @@
+(** Extraction of [Z] into Haskell's [Int] *)
+
+Require Import ZArith.
+Require Import ExtrHaskellZNum.
+
+(**
+ * Disclaimer: trying to obtain efficient certified programs
+ * by extracting [Z] into [Int] is definitively *not* a good idea.
+ * See comments in [ExtrOcamlNatInt.v].
+ *)
+
+Extract Inductive positive => "Prelude.Int" [
+  "(\x -> 2 Prelude.* x Prelude.+ 1)"
+  "(\x -> 2 Prelude.* x)"
+  "1" ]
+  "(\fI fO fH n -> if n Prelude.== 1 then fH () else
+                   if Prelude.odd n
+                   then fI (n `Prelude.div` 2)
+                   else fO (n `Prelude.div` 2))".
+
+Extract Inductive Z => "Prelude.Int" [ "0" "(\x -> x)" "Prelude.negate" ]
+  "(\fO fP fN n -> if n Prelude.== 0 then fO () else
+                   if n Prelude.> 0 then fP n else
+                   fN (Prelude.negate n))".
diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/plugins/extraction/ExtrHaskellZInteger.v
new file mode 100644
index 00000000..f192f16e
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellZInteger.v
@@ -0,0 +1,23 @@
+(** Extraction of [Z] into Haskell's [Integer] *)
+
+Require Import ZArith.
+Require Import ExtrHaskellZNum.
+
+(** Disclaimer: trying to obtain efficient certified programs
+    by extracting [Z] into [Integer] isn't necessarily a good idea.
+    See comments in [ExtrOcamlNatInt.v].
+*)
+
+Extract Inductive positive => "Prelude.Integer" [
+  "(\x -> 2 Prelude.* x Prelude.+ 1)"
+  "(\x -> 2 Prelude.* x)"
+  "1" ]
+  "(\fI fO fH n -> if n Prelude.== 1 then fH () else
+                   if Prelude.odd n
+                   then fI (n `Prelude.div` 2)
+                   else fO (n `Prelude.div` 2))".
+
+Extract Inductive Z => "Prelude.Integer" [ "0" "(\x -> x)" "Prelude.negate" ]
+  "(\fO fP fN n -> if n Prelude.== 0 then fO () else
+                   if n Prelude.> 0 then fP n else
+                   fN (Prelude.negate n))".
diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v
new file mode 100644
index 00000000..cbbfda75
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellZNum.v
@@ -0,0 +1,21 @@
+(**
+ * Efficient (but uncertified) extraction of usual [Z] functions
+ * into equivalent versions in Haskell's Prelude that are defined
+ * for any [Num] typeclass instances.  Useful in combination with
+ * [Extract Inductive Z] that maps [Z] onto a Haskell type that
+ * implements [Num].
+ *)
+
+Require Import ZArith.
+Require Import EqNat.
+
+Extract Inlined Constant Z.add => "(Prelude.+)".
+Extract Inlined Constant Z.sub => "(Prelude.-)".
+Extract Inlined Constant Z.mul => "(Prelude.*)".
+Extract Inlined Constant Z.max => "Prelude.max".
+Extract Inlined Constant Z.min => "Prelude.min".
+Extract Inlined Constant Z_ge_lt_dec => "(Prelude.>=)".
+Extract Inlined Constant Z_gt_le_dec => "(Prelude.>)".
+
+Extract Constant Z.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Z.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 080512b2..6ae519ef 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -633,7 +633,8 @@ let rec extract_term env mle mlt c args =
     | Construct (cp,u) ->
 	extract_cons_app env mle mlt cp u args
     | Proj (p, c) ->
-        extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args)
+        let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
+	  extract_term env mle mlt term args
     | Rel n ->
 	(* As soon as the expected [mlt] for the head is known, *)
 	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 9fdb0205..6fc1195f 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -490,8 +490,8 @@ let ast_occurs_itvl k k' t =
     ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false
   with Found -> true
 
-(* Number of occurences of [Rel 1] in [t], with special treatment of match:
-   occurences in different branches aren't added, but we rather use max. *)
+(* Number of occurrences of [Rel 1] in [t], with special treatment of match:
+   occurrences in different branches aren't added, but we rather use max. *)
 
 let nb_occur_match =
   let rec nb k = function
@@ -851,7 +851,7 @@ let factor_branches o typ br =
     else Some (br_factor, br_set)
   end
 
-(*s If all branches are functions, try to permut the case and the functions. *)
+(*s If all branches are functions, try to permute the case and the functions. *)
 
 let rec merge_ids ids ids' = match ids,ids' with
   | [],l -> l
@@ -1127,7 +1127,7 @@ let term_expunge s (ids,c) =
       MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
-(*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and
+(*s [kill_dummy_args ids r t] looks for occurrences of [MLrel r] in [t] and
   purge the args of [MLrel r] corresponding to a [dummy_name].
   It makes eta-expansion if needed. *)
 
@@ -1351,10 +1351,10 @@ let is_not_strict t =
    We expand small terms with at least one non-strict
    variable (i.e. a variable that may not be evaluated).
 
-   Futhermore we don't expand fixpoints.
+   Furthermore we don't expand fixpoints.
 
-   Moreover, as mentionned by X. Leroy (bug #2241),
-   inling a constant from inside an opaque module might
+   Moreover, as mentioned by X. Leroy (bug #2241),
+   inlining a constant from inside an opaque module might
    break types. To avoid that, we require below that
    both [r] and its body are globally visible. This isn't
    fully satisfactory, since [r] might not be visible (functor),
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index f0489048..9c30c5eb 100644
--- a/plugins/extraction/vo.itarget
+++ b/plugins/extraction/vo.itarget
@@ -1,4 +1,11 @@
 ExtrHaskellBasic.vo
+ExtrHaskellNatNum.vo
+ExtrHaskellNatInt.vo
+ExtrHaskellNatInteger.vo
+ExtrHaskellZNum.vo
+ExtrHaskellZInt.vo
+ExtrHaskellZInteger.vo
+ExtrHaskellString.vo
 ExtrOcamlBasic.vo
 ExtrOcamlIntConv.vo
 ExtrOcamlBigIntConv.vo
@@ -6,4 +13,4 @@ ExtrOcamlNatInt.vo
 ExtrOcamlNatBigInt.vo
 ExtrOcamlZInt.vo
 ExtrOcamlZBigInt.vo
-ExtrOcamlString.vo
\ No newline at end of file
+ExtrOcamlString.vo