From 5089872d20c9e3089676c9267a6394e99cca5121 Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Sat, 23 May 2015 12:22:48 -0700 Subject: Add efficient extraction of [nat], [Z], and [string] to Haskell This mirrors the existing extraction libraries for OCaml. One wart: the extraction for [string] requires that the Haskell code imports Data.Bits and Data.Char. Coq has no way to add extra import statements to the extracted code. So we have to rely on the user to somehow import these libraries (e.g., using the -pgmF ghc option). See also https://coq.inria.fr/bugs/show_bug.cgi?id=4189 Message to github robot: this commit closes #65 --- plugins/extraction/ExtrHaskellNatInt.v | 13 ++++++++++ plugins/extraction/ExtrHaskellNatInteger.v | 13 ++++++++++ plugins/extraction/ExtrHaskellNatNum.v | 27 +++++++++++++++++++++ plugins/extraction/ExtrHaskellString.v | 38 ++++++++++++++++++++++++++++++ plugins/extraction/ExtrHaskellZInt.v | 24 +++++++++++++++++++ plugins/extraction/ExtrHaskellZInteger.v | 23 ++++++++++++++++++ plugins/extraction/ExtrHaskellZNum.v | 19 +++++++++++++++ plugins/extraction/vo.itarget | 9 ++++++- 8 files changed, 165 insertions(+), 1 deletion(-) create mode 100644 plugins/extraction/ExtrHaskellNatInt.v create mode 100644 plugins/extraction/ExtrHaskellNatInteger.v create mode 100644 plugins/extraction/ExtrHaskellNatNum.v create mode 100644 plugins/extraction/ExtrHaskellString.v create mode 100644 plugins/extraction/ExtrHaskellZInt.v create mode 100644 plugins/extraction/ExtrHaskellZInteger.v create mode 100644 plugins/extraction/ExtrHaskellZNum.v 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 -- cgit v1.2.3 From 192e683d414ac86d213e2386da40dd7aa5a2fccd Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 2 May 2015 16:56:16 -0400 Subject: Guard the List.hd call in [Show Intros] Fix for [Anomaly: Uncaught exception Failure("hd")] after running [Show Intros] at the end of a proof: Goal True. trivial. Show Intros. --- toplevel/vernacentries.ml | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 188d2d098f..c4be56f53a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -102,17 +102,19 @@ 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 - let n = List.last l in - msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) - with Failure "List.last" -> () + if 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 + try + 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 -- cgit v1.2.3 From d6ee11ac2190df5adad63e5125a9e583533e49e0 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 2 May 2015 17:36:05 -0400 Subject: Replace 'try ... with Failure "List.last"' with 'if l <> []' --- toplevel/vernacentries.ml | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c4be56f53a..86ba38186c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -105,16 +105,13 @@ let show_intro all = if 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 + 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 - let n = List.last l in - msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) - with Failure "List.last" -> () - end + else if l <> [] then + let n = List.last l in + msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) + end (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name -- cgit v1.2.3 From 4b6b4d8cdd12902d166504ec3d96ca94705d81f6 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Mon, 4 May 2015 14:26:24 -0400 Subject: Remove uses of polymorphic equality from prev. commit Message to the github robot: This closes #63 --- toplevel/vernacentries.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 86ba38186c..80fe26a817 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -102,13 +102,13 @@ let try_print_subgoals () = let show_intro all = let pf = get_pftreestate() in let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in - if gls <> [] then begin + 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 l <> [] then + 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))) end -- cgit v1.2.3