Merge branch 'v8.5' into trunk

9 files changed, 173 insertions, 10 deletions

diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/plugins/extraction/ExtrHaskellNatInt.v
new file mode 100644
index 0000000000..e94e7d42bd
--- /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 0000000000..038f0ed817
--- /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 0000000000..979a1cdc41
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -0,0 +1,27 @@
+(**
+ * 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.div => "Prelude.div".
+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 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 pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+Extract Constant minus => "(\n m -> Prelude.max 0 (n Prelude.- m))".
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
new file mode 100644
index 0000000000..3558f4f254
--- /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 0000000000..66690851a7
--- /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 0000000000..f192f16ee8
--- /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 0000000000..3f645db9b1
--- /dev/null
+++ b/plugins/extraction/ExtrHaskellZNum.v
@@ -0,0 +1,19 @@
+(**
+ * 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.div => "Prelude.div".
+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.>)".
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
index f04890480f..9c30c5eb3e 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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 188d2d098f..80fe26a817 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -102,17 +102,16 @@ let try_print_subgoals () =
 let show_intro all =
   let pf = get_pftreestate() in
   let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
-  let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
-  let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
-  if all
-  then
-    let lid = Tactics.find_intro_names l gl in
-    msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))
-  else
-    try
+  if not (List.is_empty gls) then begin
+    let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
+    let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
+    if all then
+      let lid = Tactics.find_intro_names l gl in
+      msg_notice (hov 0 (prlist_with_sep  spc pr_id lid))
+    else if not (List.is_empty l) then
       let n = List.last l in
       msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
-    with Failure "List.last" -> ()
+  end
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name