diff options
Diffstat (limited to 'plugins/extraction')
42 files changed, 1332 insertions, 642 deletions
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES index fbcd01a15e..cf97ae3ab8 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/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v new file mode 100644 index 0000000000..294d61023b --- /dev/null +++ b/plugins/extraction/ExtrHaskellBasic.v @@ -0,0 +1,15 @@ +(** Extraction to Haskell : use of basic Haskell types *) + +Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. +Extract Inductive unit => "()" [ "()" ]. +Extract Inductive list => "([])" [ "([])" "(:)" ]. +Extract Inductive prod => "(,)" [ "(,)" ]. + +Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ]. +Extract Inductive sumor => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ]. +Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ]. + +Extract Inlined Constant andb => "(Prelude.&&)". +Extract Inlined Constant orb => "(Prelude.||)". +Extract Inlined Constant negb => "Prelude.not". 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..244eb85fc2 --- /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 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..cbbfda75e5 --- /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/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index 9dbda8216c..d9b000c2af 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v index 4cc76d86f3..c42938c8ec 100644 --- a/plugins/extraction/ExtrOcamlBigIntConv.v +++ b/plugins/extraction/ExtrOcamlBigIntConv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v index eb43d69fe0..515fa52dfa 100644 --- a/plugins/extraction/ExtrOcamlIntConv.v +++ b/plugins/extraction/ExtrOcamlIntConv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index 1386c2ad5f..3149e70298 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 5f653ee109..7c607f7ae6 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -59,6 +59,7 @@ Extract Constant Compare_dec.nat_compare => "fun n m -> if n=m then Eq else if n<m then Lt else Gt". Extract Inlined Constant Compare_dec.leb => "(<=)". Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)". +Extract Inlined Constant Compare_dec.lt_dec => "(<)". Extract Constant Compare_dec.lt_eq_lt_dec => "fun n m -> if n>m then None else Some (n<m)". diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index ce8025bfba..6af591eed3 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index 3d59669a9c..c9e8eac0c5 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -46,7 +46,7 @@ Extract Constant Pos.max => "Big.max". Extract Constant Pos.compare => "fun x y -> Big.compare_case Eq Lt Gt x y". Extract Constant Pos.compare_cont => - "fun x y c -> Big.compare_case c Lt Gt x y". + "fun c x y -> Big.compare_case c Lt Gt x y". Extract Constant N.add => "Big.add". Extract Constant N.succ => "Big.succ". diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index 79d6749557..4d33174b35 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml index f2a965c902..44b81d762c 100644 --- a/plugins/extraction/big.ml +++ b/plugins/extraction/big.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 21819aa8f1..9446cf667c 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -17,8 +17,8 @@ open Table open Miniml open Mlutil -let string_of_id id = - let s = Names.Id.to_string id in +let ascii_of_id id = + let s = Id.to_string id in for i = 0 to String.length s - 2 do if s.[i] == '_' && s.[i+1] == '_' then warning_id s done; @@ -73,18 +73,19 @@ let fnl2 () = fnl () ++ fnl () let space_if = function true -> str " " | false -> mt () -let is_digit = function - | '0'..'9' -> true - | _ -> false +let begins_with s prefix = + let len = String.length prefix in + String.length s >= len && String.equal (String.sub s 0 len) prefix let begins_with_CoqXX s = let n = String.length s in n >= 4 && s.[0] == 'C' && s.[1] == 'o' && s.[2] == 'q' && let i = ref 3 in try while !i < n do - if s.[!i] == '_' then i:=n (*Stop*) - else if is_digit s.[!i] then incr i - else raise Not_found + match s.[!i] with + | '_' -> i:=n (*Stop*) + | '0'..'9' -> incr i + | _ -> raise Not_found done; true with Not_found -> false @@ -109,9 +110,9 @@ let pseudo_qualify = qualify "__" let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false -let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id)) +let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id)) let uppercase_id id = - let s = string_of_id id in + let s = ascii_of_id id in assert (not (String.is_empty s)); if s.[0] == '_' then Id.of_string ("Coq_"^s) else Id.of_string (String.capitalize s) @@ -144,7 +145,7 @@ type env = Id.t list * Id.Set.t (*s Generic renaming issues for local variable names. *) let rec rename_id id avoid = - if Id.Set.mem id avoid then rename_id (lift_subscript id) avoid else id + if Id.Set.mem id avoid then rename_id (increment_subscript id) avoid else id let rec rename_vars avoid = function | [] -> @@ -171,10 +172,7 @@ let push_vars ids (db,avoid) = let ids',avoid' = rename_vars avoid ids in ids', (ids' @ db, avoid') -let get_db_name n (db,_) = - let id = List.nth db (pred n) in - if Id.equal id dummy_name then Id.of_string "__" else id - +let get_db_name n (db,_) = List.nth db (pred n) (*S Renamings of global objects. *) @@ -334,13 +332,10 @@ let reset_renaming_tables flag = existing. *) let modular_rename k id = - let s = string_of_id id in - let prefix,is_ok = - if upperkind k then "Coq_",is_upper else "coq_",is_lower + let s = ascii_of_id id in + let prefix,is_ok = if upperkind k then "Coq_",is_upper else "coq_",is_lower in - if not (is_ok s) || - (Id.Set.mem id (get_keywords ())) || - (String.length s >= 4 && String.equal (String.sub s 0 4) prefix) + if not (is_ok s) || Id.Set.mem id (get_keywords ()) || begins_with s prefix then prefix ^ s else s @@ -348,21 +343,20 @@ let modular_rename k id = with unique numbers *) let modfstlev_rename = - let add_prefixes,get_prefixes,_ = mktable_id true in + let add_index,get_index,_ = mktable_id true in fun l -> - let coqid = Id.of_string "Coq" in let id = Label.to_id l in try - let coqset = get_prefixes id in - let nextcoq = next_ident_away coqid coqset in - add_prefixes id (nextcoq::coqset); - (string_of_id nextcoq)^"_"^(string_of_id id) + let n = get_index id in + add_index id (n+1); + let s = if n == 0 then "" else string_of_int (n-1) in + "Coq"^s^"_"^(ascii_of_id id) with Not_found -> - let s = string_of_id id in + let s = ascii_of_id id in if is_lower s || begins_with_CoqXX s then - (add_prefixes id [coqid]; "Coq_"^s) + (add_index id 1; "Coq_"^s) else - (add_prefixes id []; s) + (add_index id 0; s) (*s Creating renaming for a [module_path] : first, the real function ... *) @@ -407,7 +401,7 @@ let ref_renaming_fun (k,r) = | [""] -> (* this happens only at toplevel of the monolithic case *) let globs = Id.Set.elements (get_global_ids ()) in let id = next_ident_away (kindcase_id k idg) globs in - string_of_id id + Id.to_string id | _ -> modular_rename k idg in add_global_ids (Id.of_string s); @@ -565,7 +559,7 @@ let pp_ocaml_extern k base rls = match rls with (* Standard situation : object in an opened file *) dottify rls' -(* [pp_ocaml_gen] : choosing between [pp_ocaml_extern] or [pp_ocaml_extern] *) +(* [pp_ocaml_gen] : choosing between [pp_ocaml_local] or [pp_ocaml_extern] *) let pp_ocaml_gen k mp rls olab = match common_prefix_from_list mp (get_visible_mps ()) with @@ -582,8 +576,7 @@ let pp_haskell_gen k mp rls = match rls with | s::rls' -> let str = pseudo_qualify rls' in let str = if is_upper str && not (upperkind k) then ("_"^str) else str in - let prf = if not (ModPath.equal (base_mp mp) (top_visible_mp ())) then s ^ "." else "" in - prf ^ str + if ModPath.equal (base_mp mp) (top_visible_mp ()) then str else s^"."^str (* Main name printing function for a reference *) @@ -600,6 +593,7 @@ let pp_global k r = let rls = List.rev ls in (* for what come next it's easier this way *) match lang () with | Scheme -> unquote s (* no modular Scheme extraction... *) + | JSON -> dottify (List.map unquote rls) | Haskell -> if modular () then pp_haskell_gen k mp rls else s | Ocaml -> pp_ocaml_gen k mp rls (Some l) @@ -628,7 +622,7 @@ let check_extract_ascii () = try let char_type = match lang () with | Ocaml -> "char" - | Haskell -> "Char" + | Haskell -> "Prelude.Char" | _ -> raise Not_found in String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type) diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index a8ab4fd3c8..2f5601964e 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 42e69d342e..52f22ee603 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,13 +13,12 @@ open Names open Libnames open Globnames open Pp -open Errors +open CErrors open Util open Table open Extraction open Modutil open Common -open Mod_subst (***************************************) (*S Part I: computing Coq environment. *) @@ -78,56 +77,51 @@ module type VISIT = sig (* Add reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) val add_ref : global_reference -> unit + val add_kn : kernel_name -> unit val add_decl_deps : ml_decl -> unit val add_spec_deps : ml_spec -> unit (* Test functions: is a particular object a needed dependency for the current extraction ? *) val needed_ind : mutual_inductive -> bool - val needed_con : constant -> bool + val needed_cst : constant -> bool val needed_mp : module_path -> bool val needed_mp_all : module_path -> bool end module Visit : VISIT = struct type must_visit = - { mutable ind : KNset.t; mutable con : KNset.t; - mutable mp : MPset.t; mutable mp_all : MPset.t } + { mutable kn : KNset.t; + mutable mp : MPset.t; + mutable mp_all : MPset.t } (* the imperative internal visit lists *) - let v = { ind = KNset.empty ; con = KNset.empty ; - mp = MPset.empty; mp_all = MPset.empty } + let v = { kn = KNset.empty; mp = MPset.empty; mp_all = MPset.empty } (* the accessor functions *) let reset () = - v.ind <- KNset.empty; - v.con <- KNset.empty; + v.kn <- KNset.empty; v.mp <- MPset.empty; v.mp_all <- MPset.empty - let needed_ind i = KNset.mem (user_mind i) v.ind - let needed_con c = KNset.mem (user_con c) v.con + let needed_ind i = KNset.mem (user_mind i) v.kn + let needed_cst c = KNset.mem (user_con c) v.kn let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all let needed_mp_all mp = MPset.mem mp v.mp_all let add_mp mp = check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp let add_mp_all mp = - check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp; + check_loaded_modfile mp; + v.mp <- MPset.union (prefixes_mp mp) v.mp; v.mp_all <- MPset.add mp v.mp_all - let add_ind i = - let kn = user_mind i in - v.ind <- KNset.add kn v.ind; add_mp (modpath kn) - let add_con c = - let kn = user_con c in - v.con <- KNset.add kn v.con; add_mp (modpath kn) + let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn) let add_ref = function - | ConstRef c -> add_con c - | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_ind ind + | ConstRef c -> add_kn (user_con c) + | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (user_mind ind) | VarRef _ -> assert false let add_decl_deps = decl_iter_references add_ref add_ref add_ref let add_spec_deps = spec_iter_references add_ref add_ref add_ref end let add_field_label mp = function - | (lab, SFBconst _) -> Visit.add_ref (ConstRef (Constant.make2 mp lab)) - | (lab, SFBmind _) -> Visit.add_ref (IndRef (MutInd.make2 mp lab, 0)) + | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make2 mp lab) | (lab, (SFBmodule _|SFBmodtype _)) -> Visit.add_mp_all (MPdot (mp,lab)) let rec add_labels mp = function @@ -182,8 +176,7 @@ let factor_fix env l cb msb = let expand_mexpr env mp me = let inl = Some (Flags.get_inline_level()) in - let sign,_,_,_ = Mod_typing.translate_mse env (Some mp) inl me in - sign + Mod_typing.translate_mse env (Some mp) inl me (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. To check with Elie. *) @@ -193,49 +186,56 @@ let rec mp_of_mexpr = function | MEwith (seb,_) -> mp_of_mexpr seb | _ -> assert false +let no_delta = Mod_subst.empty_delta_resolver + let env_for_mtb_with_def env mp me idl = let struc = Modops.destr_nofunctor me in let l = Label.of_id (List.hd idl) in let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in let before = fst (List.split_when spot struc) in - Modops.add_structure mp before empty_delta_resolver env + Modops.add_structure mp before no_delta env + +let make_cst resolver mp l = + Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l) + +let make_mind resolver mp l = + Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp l) (* From a [structure_body] (i.e. a list of [structure_field_body]) to specifications. *) -let rec extract_structure_spec env mp = function +let rec extract_structure_spec env mp reso = function | [] -> [] | (l,SFBconst cb) :: msig -> - let kn = Constant.make2 mp l in - let s = extract_constant_spec env kn cb in - let specs = extract_structure_spec env mp msig in + let c = make_cst reso mp l in + let s = extract_constant_spec env c cb in + let specs = extract_structure_spec env mp reso msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> - let mind = MutInd.make2 mp l in + let mind = make_mind reso mp l in let s = Sind (mind, extract_inductive env mind) in - let specs = extract_structure_spec env mp msig in + let specs = extract_structure_spec env mp reso msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmodule mb) :: msig -> - let specs = extract_structure_spec env mp msig in + let specs = extract_structure_spec env mp reso msig in let spec = extract_mbody_spec env mb.mod_mp mb in (l,Smodule spec) :: specs | (l,SFBmodtype mtb) :: msig -> - let specs = extract_structure_spec env mp msig in + let specs = extract_structure_spec env mp reso msig in let spec = extract_mbody_spec env mtb.mod_mp mtb in (l,Smodtype spec) :: specs (* From [module_expression] to specifications *) -(* Invariant: the [me] given to [extract_mexpr_spec] should either come - from a [mod_type] or [type_expr] field, or their [_alg] counterparts. - This way, any encountered [MEident] should be a true module type. -*) +(* Invariant: the [me_alg] given to [extract_mexpr_spec] and + [extract_mexpression_spec] should come from a [mod_type_alg] field. + This way, any encountered [MEident] should be a true module type. *) and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with | MEident mp -> Visit.add_mp_all mp; MTident mp - | MEwith(me',WithDef(idl,c))-> + | MEwith(me',WithDef(idl,(c,ctx)))-> let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in let mt = extract_mexpr_spec env mp1 (me_struct,me') in (match extract_with_type env' c with (* cb may contain some kn *) @@ -244,7 +244,9 @@ and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with | MEwith(me',WithMod(idl,mp))-> Visit.add_mp_all mp; MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp)) - | MEapply _ -> extract_msignature_spec env mp1 me_struct + | MEapply _ -> + (* No higher-order module type in OCaml : we use the expanded version *) + extract_msignature_spec env mp1 no_delta (*TODO*) me_struct and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with | MoreFunctor (mbid, mtb, me_alg') -> @@ -258,19 +260,19 @@ and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with extract_mexpression_spec env' mp1 (me_struct',me_alg')) | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m) -and extract_msignature_spec env mp1 = function +and extract_msignature_spec env mp1 reso = function | NoFunctor struc -> - let env' = Modops.add_structure mp1 struc empty_delta_resolver env in - MTsig (mp1, extract_structure_spec env' mp1 struc) + let env' = Modops.add_structure mp1 struc reso env in + MTsig (mp1, extract_structure_spec env' mp1 reso struc) | MoreFunctor (mbid, mtb, me) -> let mp = MPbound mbid in let env' = Modops.add_module_type mp mtb env in MTfunsig (mbid, extract_mbody_spec env mp mtb, - extract_msignature_spec env' mp1 me) + extract_msignature_spec env' mp1 reso me) and extract_mbody_spec env mp mb = match mb.mod_type_alg with | Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty) - | None -> extract_msignature_spec env mp mb.mod_type + | None -> extract_msignature_spec env mp mb.mod_delta mb.mod_type (* From a [structure_body] (i.e. a list of [structure_field_body]) to implementations. @@ -279,31 +281,31 @@ and extract_mbody_spec env mp mb = match mb.mod_type_alg with important: last to first ensures correct dependencies. *) -let rec extract_structure env mp ~all = function +let rec extract_structure env mp reso ~all = function | [] -> [] | (l,SFBconst cb) :: struc -> (try let vl,recd,struc = factor_fix env l cb struc in - let vc = Array.map (Constant.make2 mp) vl in - let ms = extract_structure env mp ~all struc in - let b = Array.exists Visit.needed_con vc in + let vc = Array.map (make_cst reso mp) vl in + let ms = extract_structure env mp reso ~all struc in + let b = Array.exists Visit.needed_cst vc in if all || b then let d = extract_fixpoint env vc recd in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms with Impossible -> - let ms = extract_structure env mp ~all struc in - let c = Constant.make2 mp l in - let b = Visit.needed_con c in + let ms = extract_structure env mp reso ~all struc in + let c = make_cst reso mp l in + let b = Visit.needed_cst c in if all || b then let d = extract_constant env c cb in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) | (l,SFBmind mib) :: struc -> - let ms = extract_structure env mp ~all struc in - let mind = MutInd.make2 mp l in + let ms = extract_structure env mp reso ~all struc in + let mind = make_mind reso mp l in let b = Visit.needed_ind mind in if all || b then let d = Dind (mind, extract_inductive env mind) in @@ -311,14 +313,14 @@ let rec extract_structure env mp ~all = function else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms | (l,SFBmodule mb) :: struc -> - let ms = extract_structure env mp ~all struc in + let ms = extract_structure env mp reso ~all struc in let mp = MPdot (mp,l) in let all' = all || Visit.needed_mp_all mp in if all' || Visit.needed_mp mp then (l,SEmodule (extract_module env mp ~all:all' mb)) :: ms else ms | (l,SFBmodtype mtb) :: struc -> - let ms = extract_structure env mp ~all struc in + let ms = extract_structure env mp reso ~all struc in let mp = MPdot (mp,l) in if all || Visit.needed_mp mp then (l,SEmodtype (extract_mbody_spec env mp mtb)) :: ms @@ -332,7 +334,8 @@ and extract_mexpr env mp = function (* In Haskell/Scheme, we expand everything. For now, we also extract everything, dead code will be removed later (see [Modutil.optimize_struct]. *) - extract_msignature env mp ~all:true (expand_mexpr env mp me) + let sign,_,delta,_ = expand_mexpr env mp me in + extract_msignature env mp delta ~all:true sign | MEident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; Visit.add_mp_all mp; Miniml.MEident mp @@ -350,17 +353,17 @@ and extract_mexpression env mp = function extract_mbody_spec env mp1 mtb, extract_mexpression env' mp me) -and extract_msignature env mp ~all = function +and extract_msignature env mp reso ~all = function | NoFunctor struc -> - let env' = Modops.add_structure mp struc empty_delta_resolver env in - Miniml.MEstruct (mp,extract_structure env' mp ~all struc) + let env' = Modops.add_structure mp struc reso env in + Miniml.MEstruct (mp,extract_structure env' mp reso ~all struc) | MoreFunctor (mbid, mtb, me) -> let mp1 = MPbound mbid in let env' = Modops.add_module_type mp1 mtb env in Miniml.MEfunctor (mbid, extract_mbody_spec env mp1 mtb, - extract_msignature env' mp ~all me) + extract_msignature env' mp reso ~all me) and extract_module env mp ~all mb = (* A module has an empty [mod_expr] when : @@ -376,8 +379,8 @@ and extract_module env mp ~all mb = (* This module has a signature, otherwise it would be FullStruct. We extract just the elements required by this signature. *) let () = add_labels mp mb.mod_type in - extract_msignature env mp ~all:false sign - | FullStruct -> extract_msignature env mp ~all mb.mod_type + extract_msignature env mp mb.mod_delta ~all:false sign + | FullStruct -> extract_msignature env mp mb.mod_delta ~all mb.mod_type in (* Slight optimization: for modules without explicit signatures ([FullStruct] case), we build the type out of the extracted @@ -399,7 +402,7 @@ let mono_environment refs mpl = let l = List.rev (environment_until None) in List.rev_map (fun (mp,struc) -> - mp, extract_structure env mp ~all:(Visit.needed_mp_all mp) struc) + mp, extract_structure env mp no_delta ~all:(Visit.needed_mp_all mp) struc) l (**************************************) @@ -410,6 +413,7 @@ let descr () = match lang () with | Ocaml -> Ocaml.ocaml_descr | Haskell -> Haskell.haskell_descr | Scheme -> Scheme.scheme_descr + | JSON -> Json.json_descr (* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" Works similarly for the other languages. *) @@ -440,7 +444,8 @@ let mono_filename f = let module_filename mp = let f = file_of_modfile mp in let d = descr () in - Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f + let p = d.file_naming mp ^ d.file_suffix in + Some p, Option.map ((^) f) d.sig_suffix, Id.of_string f (*s Extraction of one decl to stdout. *) @@ -453,7 +458,7 @@ let print_one_decl struc mp decl = push_visible mp []; let ans = d.pp_decl decl in pop_visible (); - ans + v 0 ans (*s Extraction of a ml struct to a file. *) @@ -493,8 +498,8 @@ let print_structure_to_file (fn,si,mo) dry struc = let d = descr () in reset_renaming_tables AllButExternal; let unsafe_needs = { - mldummy = struct_ast_search ((==) MLdummy) struc; - tdummy = struct_type_search Mlutil.isDummy struc; + mldummy = struct_ast_search Mlutil.isMLdummy struc; + tdummy = struct_type_search Mlutil.isTdummy struc; tunknown = struct_type_search ((==) Tunknown) struc; magic = if lang () != Haskell then false @@ -536,7 +541,7 @@ let print_structure_to_file (fn,si,mo) dry struc = (if dry then None else si); (* Print the buffer content via Coq standard formatter (ok with coqide). *) if not (Int.equal (Buffer.length buf) 0) then begin - Pp.msg_info (str (Buffer.contents buf)); + Feedback.msg_notice (str (Buffer.contents buf)); Buffer.reset buf end @@ -578,8 +583,8 @@ let rec locate_ref = function | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> - warning_both_mod_and_cst q mp r; - let refs,mps = locate_ref l in refs,mp::mps + warning_ambiguous_name (q,mp,r); + let refs,mps = locate_ref l in refs,mp::mps (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when @@ -630,7 +635,7 @@ let simple_extraction r = in let ans = flag ++ print_one_decl struc (modpath_of_r r) d in reset (); - Pp.msg_info ans + Feedback.msg_notice ans | _ -> assert false @@ -648,7 +653,7 @@ let extraction_library is_rec m = let l = List.rev (environment_until (Some dir_m)) in let select l (mp,struc) = if Visit.needed_mp mp - then (mp, extract_structure env mp true struc) :: l + then (mp, extract_structure env mp no_delta true struc) :: l else l in let struc = List.fold_left select [] l in diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index e5fe76f58a..90f4f911b7 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 080512b273..a980a43f53 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,7 +11,6 @@ open Util open Names open Term open Vars -open Context open Declarations open Declareops open Environ @@ -26,6 +25,7 @@ open Globnames open Miniml open Table open Mlutil +open Context.Rel.Declaration (*i*) exception I of inductive_kind @@ -35,17 +35,18 @@ let current_fixpoints = ref ([] : constant list) let none = Evd.empty +(* NB: In OCaml, [type_of] and [get_of] might raise + [SingletonInductiveBecomeProp]. This exception will be caught + in late wrappers around the exported functions of this file, + in order to display the location of the issue. *) + let type_of env c = - try - let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (strip_outer_cast c) - with SingletonInductiveBecomesProp id -> error_singleton_become_prop id + let polyprop = (lang() == Haskell) in + Retyping.get_type_of ~polyprop env none (strip_outer_cast c) let sort_of env c = - try - let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c) - with SingletonInductiveBecomesProp id -> error_singleton_become_prop id + let polyprop = (lang() == Haskell) in + Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c) (*S Generation of flags and signatures. *) @@ -73,9 +74,9 @@ type flag = info * scheme Really important function. *) let rec flag_of_type env t : flag = - let t = whd_betadeltaiota env none t in + let t = whd_all env none t in match kind_of_term t with - | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c + | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) | Sort _ -> (Info,TypeScheme) | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default) @@ -91,7 +92,7 @@ exception NotDefault of kill_reason let check_default env t = match flag_of_type env t with | _,TypeScheme -> raise (NotDefault Ktype) - | Logic,_ -> raise (NotDefault Kother) + | Logic,_ -> raise (NotDefault Kprop) | _ -> () let is_info_scheme env t = match flag_of_type env t with @@ -101,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> - (if is_info_scheme env t then Keep else Kill Kother) + (if is_info_scheme env t then Keep else Kill Kprop) :: (type_sign (push_rel_assum (n,t) env) d) | _ -> [] let rec type_scheme_nb_args env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in if is_info_scheme env t then n+1 else n @@ -134,15 +135,15 @@ let make_typvar n vl = next_ident_away id' vl let rec type_sign_vl env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in - if not (is_info_scheme env t) then Kill Kother::s, vl + if not (is_info_scheme env t) then Kill Kprop::s, vl else Keep::s, (make_typvar n vl) :: vl | _ -> [],[] let rec nb_default_params env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let n = nb_default_params (push_rel_assum (n,t) env) d in if is_default env t then n+1 else n @@ -154,25 +155,12 @@ let sign_with_implicits r s nb_params = let implicits = implicits_of_global r in let rec add_impl i = function | [] -> [] - | sign::s -> - let sign' = - if sign == Keep && Int.List.mem i implicits - then Kill Kother else sign - in sign' :: add_impl (succ i) s + | Keep::s when Int.Set.mem i implicits -> + Kill (Kimplicit (r,i)) :: add_impl (i+1) s + | sign::s -> sign :: add_impl (i+1) s in add_impl (1+nb_params) s -(* Enriching a exception message *) - -let rec handle_exn r n fn_name = function - | MLexn s -> - (try Scanf.sscanf s "UNBOUND %d%!" - (fun i -> - assert ((0 < i) && (i <= n)); - MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i))) - with Scanf.Scan_failure _ | End_of_file -> MLexn s) - | a -> ast_map (handle_exn r n fn_name) a - (*S Management of type variable contexts. *) (* A De Bruijn variable context (db) is a context for translating Coq [Rel] @@ -214,36 +202,6 @@ let parse_ind_args si args relmax = | _ -> parse (i+1) (j+1) s) in parse 1 1 si -let oib_equal o1 o2 = - Id.equal o1.mind_typename o2.mind_typename && - List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && - begin - match o1.mind_arity, o2.mind_arity with - | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} -> - eq_constr c1 c2 && Sorts.equal s1 s2 - | TemplateArity p1, TemplateArity p2 -> - let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in - List.equal eq p1.template_param_levels p2.template_param_levels && - Univ.Universe.equal p1.template_level p2.template_level - | _, _ -> false - end && - Array.equal Id.equal o1.mind_consnames o2.mind_consnames - -let eq_record x y = - Option.equal (Option.equal (fun (_, x, y) (_, x', y') -> Array.for_all2 eq_constant x x')) x y - -let mib_equal m1 m2 = - Array.equal oib_equal m1.mind_packets m1.mind_packets && - eq_record m1.mind_record m2.mind_record && - (m1.mind_finite : Decl_kinds.recursivity_kind) == m2.mind_finite && - Int.equal m1.mind_ntypes m2.mind_ntypes && - List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps && - Int.equal m1.mind_nparams m2.mind_nparams && - Int.equal m1.mind_nparams_rec m2.mind_nparams_rec && - List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt && - (* Univ.UContext.eq *) m1.mind_universes == m2.mind_universes (** FIXME *) - (* m1.mind_universes = m2.mind_universes *) - (*S Extraction of a type. *) (* [extract_type env db c args] is used to produce an ML type from the @@ -285,13 +243,13 @@ let rec extract_type env db j c args = (match expand env mld with | Tdummy d -> Tdummy d | _ -> - let reason = if lvl == TypeScheme then Ktype else Kother in + let reason = if lvl == TypeScheme then Ktype else Kprop in Tarr (Tdummy reason, mld))) | Sort _ -> Tdummy Ktype (* The two logical cases. *) - | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kother + | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop | Rel n -> (match lookup_rel n env with - | (_,Some t,_) -> extract_type env db j (lift n t) args + | LocalDef (_,t,_) -> extract_type env db j (lift n t) args | _ -> (* Asks [db] a translation for [n]. *) if n > List.length db then Tunknown @@ -328,7 +286,7 @@ let rec extract_type env db j c args = | Ind ((kn,i),u) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in extract_type_app env db (IndRef (kn,i),s) args - | Case _ | Fix _ | CoFix _ -> Tunknown + | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown | _ -> assert false (*s Auxiliary function dealing with type application. @@ -371,16 +329,22 @@ and extract_type_scheme env db c p = (*S Extraction of an inductive type. *) +(* First, a version with cache *) + and extract_ind env kn = (* kn is supposed to be in long form *) let mib = Environ.lookup_mind kn env in - try - (* For a same kn, we can get various bodies due to module substitutions. - We hence check that the mib has not changed from recording - time to retrieving time. Ideally we should also check the env. *) - let (mib0,ml_ind) = lookup_ind kn in - if not (mib_equal mib mib0) then raise Not_found; - ml_ind - with Not_found -> + match lookup_ind kn mib with + | Some ml_ind -> ml_ind + | None -> + try + extract_really_ind env kn mib + with SingletonInductiveBecomesProp id -> + (* TODO : which inductive is concerned in the block ? *) + error_singleton_become_prop id (Some (IndRef (kn,0))) + +(* Then the real function *) + +and extract_really_ind env kn mib = (* First, if this inductive is aliased via a Module, we process the original inductive if possible. When at toplevel of the monolithic case, we cannot do much @@ -407,8 +371,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let packets = Array.mapi (fun i mip -> - let (ind,u), ctx = - Universes.fresh_inductive_instance env (kn,i) in + let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in let info = (fst (flag_of_type env ar) = Info) in let s,v = if info then type_sign_vl env ar else [],[] in @@ -458,7 +421,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) if p.ip_logical then raise (I Standard); if not (Int.equal (Array.length p.ip_types) 1) then raise (I Standard); let typ = p.ip_types.(0) in - let l = List.filter (fun t -> not (isDummy (expand env t))) typ in + let l = List.filter (fun t -> not (isTdummy (expand env t))) typ in if not (keep_singleton ()) && Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); @@ -479,7 +442,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let mp = MutInd.modpath kn in let rec select_fields l typs = match l,typs with | [],[] -> [] - | _::l, typ::typs when isDummy (expand env typ) -> + | _::l, typ::typs when isTdummy (expand env typ) -> select_fields l typs | Anonymous::l, typ::typs -> None :: (select_fields l typs) @@ -525,7 +488,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let env' = push_rel_assum (n,t) env in let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in @@ -536,28 +499,25 @@ and extract_type_cons env db dbmap c i = (*s Recording the ML type abbreviation of a Coq type scheme constant. *) and mlt_env env r = match r with + | IndRef _ | ConstructRef _ | VarRef _ -> None | ConstRef kn -> - (try - if not (visible_con kn) then raise Not_found; - match lookup_term kn with - | Dtype (_,vl,mlt) -> Some mlt + let cb = Environ.lookup_constant kn env in + match cb.const_body with + | Undef _ | OpaqueDef _ -> None + | Def l_body -> + match lookup_typedef kn cb with + | Some _ as o -> o + | None -> + let typ = Typeops.type_of_constant_type env cb.const_type + (* FIXME not sure if we should instantiate univs here *) in + match flag_of_type env typ with + | Info,TypeScheme -> + let body = Mod_subst.force_constr l_body in + let s = type_sign env typ in + let db = db_from_sign s in + let t = extract_type_scheme env db body (List.length s) + in add_typedef kn cb t; Some t | _ -> None - with Not_found -> - let cb = Environ.lookup_constant kn env in - let typ = Typeops.type_of_constant_type env cb.const_type - (* FIXME not sure if we should instantiate univs here *) in - match cb.const_body with - | Undef _ | OpaqueDef _ -> None - | Def l_body -> - (match flag_of_type env typ with - | Info,TypeScheme -> - let body = Mod_subst.force_constr l_body in - let s,vl = type_sign_vl env typ in - let db = db_from_sign s in - let t = extract_type_scheme env db body (List.length s) - in add_term kn (Dtype (r, vl, t)); Some t - | _ -> None)) - | _ -> None and expand env = type_expand (mlt_env env) and type2signature env = type_to_signature (mlt_env env) @@ -568,16 +528,18 @@ let type_expunge_from_sign env = type_expunge_from_sign (mlt_env env) (*s Extraction of the type of a constant. *) let record_constant_type env kn opt_typ = - try - if not (visible_con kn) then raise Not_found; - lookup_type kn - with Not_found -> - let typ = match opt_typ with - | None -> Typeops.type_of_constant_type env (lookup_constant kn env).const_type - | Some typ -> typ - in let mlt = extract_type env [] 1 typ [] - in let schema = (type_maxvar mlt, mlt) - in add_type kn schema; schema + let cb = lookup_constant kn env in + match lookup_cst_type kn cb with + | Some schema -> schema + | None -> + let typ = match opt_typ with + | None -> Typeops.type_of_constant_type env cb.const_type + | Some typ -> typ + in + let mlt = extract_type env [] 1 typ [] in + let schema = (type_maxvar mlt, mlt) in + let () = add_cst_type kn cb schema in + schema (*S Extraction of a term. *) @@ -610,7 +572,7 @@ let rec extract_term env mle mlt c args = put_magic_if magic (MLlam (id, d'))) | LetIn (n, c1, t1, c2) -> let id = id_of_name n in - let env' = push_rel (Name id, Some c1, t1) env in + let env' = push_rel (LocalDef (Name id, c1, t1)) env in (* We directly push the args inside the [LetIn]. TODO: the opt_let_app flag is supposed to prevent that *) let args' = List.map (lift 1) args in @@ -628,12 +590,13 @@ let rec extract_term env mle mlt c args = with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in ast_pop (extract_term env' mle' mlt c2 args')) - | Const (kn,u) -> - extract_cst_app env mle mlt kn u args - | Construct (cp,u) -> - extract_cons_app env mle mlt cp u args + | Const (kn,_) -> + extract_cst_app env mle mlt kn args + | Construct (cp,_) -> + extract_cons_app env mle mlt cp 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]. *) @@ -654,7 +617,7 @@ and extract_maybe_term env mle mlt c = try check_default env (type_of env c); extract_term env mle mlt c [] with NotDefault d -> - put_magic (mlt, Tdummy d) MLdummy + put_magic (mlt, Tdummy d) (MLdummy d) (*s Generic way to deal with an application. *) @@ -681,7 +644,7 @@ and make_mlargs env e s args typs = (*s Extraction of a constant applied to arguments. *) -and extract_cst_app env mle mlt kn u args = +and extract_cst_app env mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) let nb,t = record_constant_type env kn None in let schema = nb, expand env t in @@ -720,20 +683,20 @@ and extract_cst_app env mle mlt kn u args = let l,l' = List.chop (projection_arity (ConstRef kn)) mla in if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l' else mla - with e when Errors.noncritical e -> mla + with e when CErrors.noncritical e -> mla in - (* For strict languages, purely logical signatures with at least - one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left + (* For strict languages, purely logical signatures lead to a dummy lam + (except when [Kill Ktype] everywhere). So a [MLdummy] is left accordingly. *) let optdummy = match sign_kind s_full with - | UnsafeLogicalSig when lang () != Haskell -> [MLdummy] + | UnsafeLogicalSig when lang () != Haskell -> [MLdummy Kprop] | _ -> [] in (* Different situations depending of the number of arguments: *) if la >= ls then (* Enough args, cleanup already done in [mla], we only add the - additionnal dummy if needed. *) + additional dummy if needed. *) put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla)) else (* Partially applied function with some logical arg missing. @@ -747,14 +710,14 @@ and extract_cst_app env mle mlt kn u args = (*s Extraction of an inductive constructor applied to arguments. *) (* \begin{itemize} - \item In ML, contructor arguments are uncurryfied. + \item In ML, constructor arguments are uncurryfied. \item We managed to suppress logical parts inside inductive definitions, but they must appears outside (for partial applications for instance) \item We also suppressed all Coq parameters to the inductives, since they are fixed, and thus are not used for the computation. \end{itemize} *) -and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args = +and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = (* First, we build the type of the constructor, stored in small pieces. *) let mi = extract_ind env kn in let params_nb = mi.ind_nparams in @@ -825,8 +788,8 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (* Logical singleton case: *) (* [match c with C i j k -> t] becomes [t'] *) assert (Int.equal br_size 1); - let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in - let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in + let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in + let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in let e = extract_maybe_term env mle mlt br.(0) in snd (case_expunge s e) end @@ -850,8 +813,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in (* We suppress dummy arguments according to signature. *) let ids,e = case_expunge s e in - let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in - (List.rev ids, Pusual r, e') + (List.rev ids, Pusual r, e) in if mi.ind_kind == Singleton then begin @@ -885,7 +847,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = let decomp_lams_eta_n n m env c t = let rels = fst (splay_prod_n env none n t) in - let rels = List.map (fun (id,_,c) -> (id,c)) rels in + let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in let rels',c = decompose_lam c in let d = n - m in (* we'd better keep rels' as long as possible. *) @@ -959,8 +921,6 @@ let extract_std_constant env kn body typ = let e = extract_term env mle t' c [] in (* Expunging term and type from dummy lambdas. *) let trm = term_expunge s (ids,e) in - let trm = handle_exn (ConstRef kn) n (fun i -> fst (List.nth rels (i-1))) trm - in trm, type_expunge_from_sign env s t (* Extracts the type of an axiom, honors the Extraction Implicit declaration. *) @@ -978,18 +938,20 @@ let extract_axiom env kn typ = let extract_fixpoint env vkn (fi,ti,ci) = let n = Array.length vkn in - let types = Array.make n (Tdummy Kother) - and terms = Array.make n MLdummy in + let types = Array.make n (Tdummy Kprop) + and terms = Array.make n (MLdummy Kprop) in let kns = Array.to_list vkn in current_fixpoints := kns; (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) let sub = List.rev_map mkConst kns in for i = 0 to n-1 do - if sort_of env ti.(i) != InProp then begin - let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in - terms.(i) <- e; - types.(i) <- t; - end + if sort_of env ti.(i) != InProp then + try + let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in + terms.(i) <- e; + types.(i) <- t; + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id (Some (ConstRef vkn.(i))) done; current_fixpoints := []; Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) @@ -1019,13 +981,17 @@ let extract_constant env kn cb = let e,t = extract_std_constant env kn c typ in Dterm (r,e,t) in - match flag_of_type env typ with + try + match flag_of_type env typ with | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype) - | (Logic,Default) -> warn_log (); Dterm (r, MLdummy, Tdummy Kother) + | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop) | (Info,TypeScheme) -> (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () - | Def c -> mk_typ (Mod_subst.force_constr c) + | Def c -> + (match cb.const_proj with + | None -> mk_typ (Mod_subst.force_constr c) + | Some pb -> mk_typ pb.proj_body) | OpaqueDef c -> add_opaque r; if access_opaque () then @@ -1034,19 +1000,25 @@ let extract_constant env kn cb = | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () - | Def c -> mk_def (Mod_subst.force_constr c) + | Def c -> + (match cb.const_proj with + | None -> mk_def (Mod_subst.force_constr c) + | Some pb -> mk_def pb.proj_body) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c) else mk_ax ()) + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id (Some (ConstRef kn)) let extract_constant_spec env kn cb = let r = ConstRef kn in let typ = Typeops.type_of_constant_type env cb.const_type in - match flag_of_type env typ with + try + match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) - | (Logic, Default) -> Sval (r, Tdummy Kother) + | (Logic, Default) -> Sval (r, Tdummy Kprop) | (Info, TypeScheme) -> let s,vl = type_sign_vl env typ in (match cb.const_body with @@ -1059,26 +1031,34 @@ let extract_constant_spec env kn cb = | (Info, Default) -> let t = snd (record_constant_type env kn (Some typ)) in Sval (r, type_expunge env t) + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id (Some (ConstRef kn)) let extract_with_type env c = - let typ = type_of env c in - match flag_of_type env typ with + try + let typ = type_of env c in + match flag_of_type env typ with | (Info, TypeScheme) -> let s,vl = type_sign_vl env typ in let db = db_from_sign s in let t = extract_type_scheme env db c (List.length s) in Some (vl, t) | _ -> None + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id None let extract_constr env c = reset_meta_count (); - let typ = type_of env c in - match flag_of_type env typ with - | (_,TypeScheme) -> MLdummy, Tdummy Ktype - | (Logic,_) -> MLdummy, Tdummy Kother + try + let typ = type_of env c in + match flag_of_type env typ with + | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype + | (Logic,_) -> MLdummy Kprop, Tdummy Kprop | (Info,Default) -> - let mlt = extract_type env [] 1 typ [] in - extract_term env Mlenv.empty mlt c [], mlt + let mlt = extract_type env [] 1 typ [] in + extract_term env Mlenv.empty mlt c [], mlt + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id None let extract_inductive env kn = let ind = extract_ind env kn in @@ -1089,7 +1069,7 @@ let extract_inductive env kn = | [] -> [] | t::l -> let l' = filter (succ i) l in - if isDummy (expand env t) || Int.List.mem i implicits then l' + if isTdummy (expand env t) || Int.Set.mem i implicits then l' else t::l' in filter (1+ind.ind_nparams) l in @@ -1101,11 +1081,11 @@ let extract_inductive env kn = (*s Is a [ml_decl] logical ? *) let logical_decl = function - | Dterm (_,MLdummy,Tdummy _) -> true + | Dterm (_,MLdummy _,Tdummy _) -> true | Dtype (_,[],Tdummy _) -> true | Dfix (_,av,tv) -> - (Array.for_all ((==) MLdummy) av) && - (Array.for_all isDummy tv) + (Array.for_all isMLdummy av) && + (Array.for_all isTdummy tv) | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 6bd2541b24..cdda777a6c 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mlpack index b7f458611a..9184f65017 100644 --- a/plugins/extraction/extraction_plugin.mllib +++ b/plugins/extraction/extraction_plugin.mlpack @@ -6,6 +6,6 @@ Common Ocaml Haskell Scheme +Json Extract_env G_extraction -Extraction_plugin_mod diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 3caa558f9b..e1d6bb4a84 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,9 +8,13 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "extraction_plugin" + (* ML names *) open Genarg +open Stdarg +open Pcoq.Prim open Pp open Names open Nameops @@ -31,7 +35,6 @@ let pr_int_or_id _ _ _ = function | ArgId id -> pr_id id ARGUMENT EXTEND int_or_id - TYPED AS int_or_id PRINTED BY pr_int_or_id | [ preident(id) ] -> [ ArgId (Id.of_string id) ] | [ integer(i) ] -> [ ArgInt i ] @@ -41,12 +44,14 @@ let pr_language = function | Ocaml -> str "Ocaml" | Haskell -> str "Haskell" | Scheme -> str "Scheme" + | JSON -> str "JSON" VERNAC ARGUMENT EXTEND language PRINTED BY pr_language | [ "Ocaml" ] -> [ Ocaml ] | [ "Haskell" ] -> [ Haskell ] | [ "Scheme" ] -> [ Scheme ] +| [ "JSON" ] -> [ JSON ] END (* Extraction commands *) @@ -97,7 +102,7 @@ END VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY | [ "Print" "Extraction" "Inline" ] - -> [ msg_info (print_extraction_inline ()) ] + -> [Feedback. msg_info (print_extraction_inline ()) ] END VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF @@ -119,7 +124,7 @@ END VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY | [ "Print" "Extraction" "Blacklist" ] - -> [ msg_info (print_extraction_blacklist ()) ] + -> [ Feedback.msg_info (print_extraction_blacklist ()) ] END VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 5e08fef5fe..0692c88cd1 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,7 @@ (*s Production of Haskell syntax. *) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -26,7 +26,7 @@ let pr_upper_id id = str (String.capitalize (Id.to_string id)) let keywords = List.fold_right (fun s -> Id.Set.add (Id.of_string s)) - [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else"; + [ "Any"; "case"; "class"; "data"; "default"; "deriving"; "do"; "else"; "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__"; "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ] @@ -35,39 +35,59 @@ let keywords = let pp_comment s = str "-- " ++ s ++ fnl () let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}" +(* Note: do not shorten [str "foo" ++ fnl ()] into [str "foo\n"], + the '\n' character interacts badly with the Format boxing mechanism *) + let preamble mod_name comment used_modules usf = - let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n") + let pp_import mp = str ("import qualified "^ string_of_modfile mp) ++ fnl () in - (if not usf.magic then mt () + (if not (usf.magic || usf.tunknown) then mt () else str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++ - str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}") - ++ fnl () ++ fnl () + str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}" ++ fnl2 ()) ++ (match comment with | None -> mt () - | Some com -> pp_bracket_comment com ++ fnl () ++ fnl ()) + | Some com -> pp_bracket_comment com ++ fnl2 ()) ++ str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++ str "import qualified Prelude" ++ fnl () ++ - prlist pp_import used_modules ++ fnl () ++ - (if List.is_empty used_modules then mt () else fnl ()) ++ + prlist pp_import used_modules ++ fnl () + ++ + (if not (usf.magic || usf.tunknown) then mt () + else + str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ + str "import qualified GHC.Base" ++ fnl () ++ + str "import qualified GHC.Prim" ++ fnl () ++ + str "#else" ++ fnl () ++ + str "-- HUGS" ++ fnl () ++ + str "import qualified IOExts" ++ fnl () ++ + str "#endif" ++ fnl2 ()) + ++ (if not usf.magic then mt () - else str "\ -\n#ifdef __GLASGOW_HASKELL__\ -\nimport qualified GHC.Base\ -\nunsafeCoerce :: a -> b\ -\nunsafeCoerce = GHC.Base.unsafeCoerce#\ -\n#else\ -\n-- HUGS\ -\nimport qualified IOExts\ -\nunsafeCoerce :: a -> b\ -\nunsafeCoerce = IOExts.unsafeCoerce\ -\n#endif" ++ fnl2 ()) + else + str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ + str "unsafeCoerce :: a -> b" ++ fnl () ++ + str "unsafeCoerce = GHC.Base.unsafeCoerce#" ++ fnl () ++ + str "#else" ++ fnl () ++ + str "-- HUGS" ++ fnl () ++ + str "unsafeCoerce :: a -> b" ++ fnl () ++ + str "unsafeCoerce = IOExts.unsafeCoerce" ++ fnl () ++ + str "#endif" ++ fnl2 ()) + ++ + (if not usf.tunknown then mt () + else + str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ + str "type Any = GHC.Prim.Any" ++ fnl () ++ + str "#else" ++ fnl () ++ + str "-- HUGS" ++ fnl () ++ + str "type Any = ()" ++ fnl () ++ + str "#endif" ++ fnl2 ()) ++ (if not usf.mldummy then mt () - else str "__ :: any" ++ fnl () ++ - str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ()) + else + str "__ :: any" ++ fnl () ++ + str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ()) let pp_abst = function | [] -> (mt ()) @@ -102,8 +122,8 @@ let rec pp_type par vl t = pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) | Tdummy _ -> str "()" - | Tunknown -> str "()" - | Taxiom -> str "() -- AXIOM TO BE REALIZED\n" + | Tunknown -> str "Any" + | Taxiom -> str "() -- AXIOM TO BE REALIZED" ++ fnl () in hov 0 (pp_rec par t) @@ -123,7 +143,11 @@ let rec pp_expr par env args = and apply2 st = pp_apply2 st par args in function | MLrel n -> - let id = get_db_name n env in apply (pr_id id) + let id = get_db_name n env in + (* Try to survive to the occurrence of a Dummy rel. + TODO: we should get rid of this hack (cf. #592) *) + let id = if Id.equal id dummy_name then Id.of_string "__" else id in + apply (pr_id id) | MLapp (f,args') -> let stl = List.map (pp_expr true env []) args' in pp_expr par env (stl @ args) f @@ -183,8 +207,11 @@ let rec pp_expr par env args = | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) pp_par par (str "Prelude.error" ++ spc () ++ qs s) - | MLdummy -> - str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLdummy k -> + (* An [MLdummy] may be applied, but I don't really care. *) + (match msg_of_implicit k with + | "" -> str "__" + | s -> str "__" ++ spc () ++ pp_bracket_comment (str s)) | MLmagic a -> pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") @@ -243,12 +270,12 @@ let pp_logical_ind packet = prvect_with_sep spc pr_id packet.ip_consnames) let pp_singleton kn packet = + let name = pp_global Type (IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in - let l' = List.rev l in - hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++ + hov 2 (str "type " ++ name ++ spc () ++ prlist_with_sep spc pr_id l ++ (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++ - pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++ + pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ pp_comment (str "singleton inductive, whose constructor was " ++ pr_id packet.ip_consnames.(0))) @@ -303,7 +330,7 @@ let pp_decl = function prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s with Not_found -> prlist (fun id -> pr_id id ++ str " ") l ++ - if t == Taxiom then str "= () -- AXIOM TO BE REALIZED\n" + if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl () else str "=" ++ spc () ++ pp_type false l t in hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 () @@ -314,11 +341,12 @@ let pp_decl = function prvecti (fun i r -> let void = is_inline_custom r || - (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false) + (not (is_custom r) && + match defs.(i) with MLexn "UNUSED" -> true | _ -> false) in if void then mt () else - names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () ++ + hov 2 (names.(i) ++ str " :: " ++ pp_type false [] typs.(i)) ++ fnl () ++ (if is_custom r then (names.(i) ++ str " = " ++ str (find_custom r)) else @@ -329,7 +357,7 @@ let pp_decl = function if is_inline_custom r then mt () else let e = pp_global Term r in - e ++ str " :: " ++ pp_type false [] t ++ fnl () ++ + hov 2 (e ++ str " :: " ++ pp_type false [] t) ++ fnl () ++ if is_custom r then hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ()) else @@ -346,7 +374,7 @@ and pp_module_expr = function | MEfunctor _ -> mt () (* for the moment we simply discard unapplied functors *) | MEident _ | MEapply _ -> assert false - (* should be expansed in extract_env *) + (* should be expanded in extract_env *) let pp_struct = let pp_sel (mp,sel) = @@ -360,6 +388,7 @@ let pp_struct = let haskell_descr = { keywords = keywords; file_suffix = ".hs"; + file_naming = string_of_modfile; preamble = preamble; pp_struct = pp_struct; sig_suffix = None; diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli index 99559bcedc..6f49320671 100644 --- a/plugins/extraction/haskell.mli +++ b/plugins/extraction/haskell.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml new file mode 100644 index 0000000000..e43c47d050 --- /dev/null +++ b/plugins/extraction/json.ml @@ -0,0 +1,274 @@ +open Pp +open Util +open Names +open Globnames +open Table +open Miniml +open Mlutil +open Common + +let json_str s = + qs s + +let json_int i = + int i + +let json_bool b = + if b then str "true" else str "false" + +let json_global typ ref = + json_str (Common.pp_global typ ref) + +let json_id id = + json_str (Id.to_string id) + +let json_dict_one (k, v) = + json_str k ++ str (": ") ++ v + +let json_dict_open l = + str ("{") ++ fnl () ++ + str (" ") ++ hov 0 (prlist_with_sep pr_comma json_dict_one l) + +let json_dict l = + json_dict_open l ++ fnl () ++ + str ("}") + +let json_list l = + str ("[") ++ fnl () ++ + str (" ") ++ hov 0 (prlist_with_sep pr_comma (fun x -> x) l) ++ fnl () ++ + str ("]") + +let json_listarr a = + str ("[") ++ fnl () ++ + str (" ") ++ hov 0 (prvect_with_sep pr_comma (fun x -> x) a) ++ fnl () ++ + str ("]") + + +let preamble mod_name comment used_modules usf = + (match comment with + | None -> mt () + | Some s -> str "/* " ++ hov 0 s ++ str " */" ++ fnl ()) ++ + json_dict_open [ + ("what", json_str "module"); + ("name", json_id mod_name); + ("need_magic", json_bool (usf.magic)); + ("need_dummy", json_bool (usf.mldummy)); + ("used_modules", json_list + (List.map (fun mf -> json_str (file_of_modfile mf)) used_modules)) + ] + + +(*s Pretty-printing of types. *) + +let rec json_type vl = function + | Tmeta _ | Tvar' _ -> assert false + | Tvar i -> (try + let varid = List.nth vl (pred i) in json_dict [ + ("what", json_str "type:var"); + ("name", json_id varid) + ] + with Failure _ -> json_dict [ + ("what", json_str "type:varidx"); + ("name", json_int i) + ]) + | Tglob (r, l) -> json_dict [ + ("what", json_str "type:glob"); + ("name", json_global Type r); + ("args", json_list (List.map (json_type vl) l)) + ] + | Tarr (t1,t2) -> json_dict [ + ("what", json_str "type:arrow"); + ("left", json_type vl t1); + ("right", json_type vl t2) + ] + | Tdummy _ -> json_dict [("what", json_str "type:dummy")] + | Tunknown -> json_dict [("what", json_str "type:unknown")] + | Taxiom -> json_dict [("what", json_str "type:axiom")] + + +(*s Pretty-printing of expressions. *) + +let rec json_expr env = function + | MLrel n -> json_dict [ + ("what", json_str "expr:rel"); + ("name", json_id (get_db_name n env)) + ] + | MLapp (f, args) -> json_dict [ + ("what", json_str "expr:apply"); + ("func", json_expr env f); + ("args", json_list (List.map (json_expr env) args)) + ] + | MLlam _ as a -> + let fl, a' = collect_lams a in + let fl, env' = push_vars (List.map id_of_mlid fl) env in + json_dict [ + ("what", json_str "expr:lambda"); + ("argnames", json_list (List.map json_id (List.rev fl))); + ("body", json_expr env' a') + ] + | MLletin (id, a1, a2) -> + let i, env' = push_vars [id_of_mlid id] env in + json_dict [ + ("what", json_str "expr:let"); + ("name", json_id (List.hd i)); + ("nameval", json_expr env a1); + ("body", json_expr env' a2) + ] + | MLglob r -> json_dict [ + ("what", json_str "expr:global"); + ("name", json_global Term r) + ] + | MLcons (_, r, a) -> json_dict [ + ("what", json_str "expr:constructor"); + ("name", json_global Cons r); + ("args", json_list (List.map (json_expr env) a)) + ] + | MLtuple l -> json_dict [ + ("what", json_str "expr:tuple"); + ("items", json_list (List.map (json_expr env) l)) + ] + | MLcase (typ, t, pv) -> json_dict [ + ("what", json_str "expr:case"); + ("expr", json_expr env t); + ("cases", json_listarr (Array.map (fun x -> json_one_pat env x) pv)) + ] + | MLfix (i, ids, defs) -> + let ids', env' = push_vars (List.rev (Array.to_list ids)) env in + let ids' = Array.of_list (List.rev ids') in + json_dict [ + ("what", json_str "expr:fix"); + ("funcs", json_listarr (Array.map (fun (fi, ti) -> + json_dict [ + ("what", json_str "fix:item"); + ("name", json_id fi); + ("body", json_function env' ti) + ]) (Array.map2 (fun a b -> a,b) ids' defs))); + ("for", json_int i); + ] + | MLexn s -> json_dict [ + ("what", json_str "expr:exception"); + ("msg", json_str s) + ] + | MLdummy _ -> json_dict [("what", json_str "expr:dummy")] + | MLmagic a -> json_dict [ + ("what", json_str "expr:coerce"); + ("value", json_expr env a) + ] + | MLaxiom -> json_dict [("what", json_str "expr:axiom")] + +and json_one_pat env (ids,p,t) = + let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [ + ("what", json_str "case"); + ("pat", json_gen_pat (List.rev ids') env' p); + ("body", json_expr env' t) + ] + +and json_gen_pat ids env = function + | Pcons (r, l) -> json_cons_pat r (List.map (json_gen_pat ids env) l) + | Pusual r -> json_cons_pat r (List.map json_id ids) + | Ptuple l -> json_dict [ + ("what", json_str "pat:tuple"); + ("items", json_list (List.map (json_gen_pat ids env) l)) + ] + | Pwild -> json_dict [("what", json_str "pat:wild")] + | Prel n -> json_dict [ + ("what", json_str "pat:rel"); + ("name", json_id (get_db_name n env)) + ] + +and json_cons_pat r ppl = json_dict [ + ("what", json_str "pat:constructor"); + ("name", json_global Cons r); + ("argnames", json_list ppl) + ] + +and json_function env t = + let bl, t' = collect_lams t in + let bl, env' = push_vars (List.map id_of_mlid bl) env in + json_dict [ + ("what", json_str "expr:lambda"); + ("argnames", json_list (List.map json_id (List.rev bl))); + ("body", json_expr env' t') + ] + + +(*s Pretty-printing of inductive types declaration. *) + +let json_ind ip pl cv = json_dict [ + ("what", json_str "decl:ind"); + ("name", json_global Type (IndRef ip)); + ("argnames", json_list (List.map json_id pl)); + ("constructors", json_listarr (Array.mapi (fun idx c -> json_dict [ + ("name", json_global Cons (ConstructRef (ip, idx+1))); + ("argtypes", json_list (List.map (json_type pl) c)) + ]) cv)) + ] + + +(*s Pretty-printing of a declaration. *) + +let pp_decl = function + | Dind (kn, defs) -> prvecti_with_sep pr_comma + (fun i p -> if p.ip_logical then str "" + else json_ind (kn, i) p.ip_vars p.ip_types) defs.ind_packets + | Dtype (r, l, t) -> json_dict [ + ("what", json_str "decl:type"); + ("name", json_global Type r); + ("argnames", json_list (List.map json_id l)); + ("value", json_type l t) + ] + | Dfix (rv, defs, typs) -> json_dict [ + ("what", json_str "decl:fixgroup"); + ("fixlist", json_listarr (Array.mapi (fun i r -> + json_dict [ + ("what", json_str "fixgroup:item"); + ("name", json_global Term rv.(i)); + ("type", json_type [] typs.(i)); + ("value", json_function (empty_env ()) defs.(i)) + ]) rv)) + ] + | Dterm (r, a, t) -> json_dict [ + ("what", json_str "decl:term"); + ("name", json_global Term r); + ("type", json_type [] t); + ("value", json_function (empty_env ()) a) + ] + +let rec pp_structure_elem = function + | (l,SEdecl d) -> [ pp_decl d ] + | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr + | (l,SEmodtype m) -> [] + (* for the moment we simply discard module type *) + +and pp_module_expr = function + | MEstruct (mp,sel) -> List.concat (List.map pp_structure_elem sel) + | MEfunctor _ -> [] + (* for the moment we simply discard unapplied functors *) + | MEident _ | MEapply _ -> assert false + (* should be expansed in extract_env *) + +let pp_struct mls = + let pp_sel (mp,sel) = + push_visible mp []; + let p = prlist_with_sep pr_comma identity + (List.concat (List.map pp_structure_elem sel)) in + pop_visible (); p + in + str "," ++ fnl () ++ + str " " ++ qs "declarations" ++ str ": [" ++ fnl () ++ + str " " ++ hov 0 (prlist_with_sep pr_comma pp_sel mls) ++ fnl () ++ + str " ]" ++ fnl () ++ + str "}" ++ fnl () + + +let json_descr = { + keywords = Id.Set.empty; + file_suffix = ".json"; + file_naming = file_of_modfile; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = None; + sig_preamble = (fun _ _ _ _ -> mt ()); + pp_sig = (fun _ -> mt ()); + pp_decl = pp_decl; +} diff --git a/plugins/extraction/json.mli b/plugins/extraction/json.mli new file mode 100644 index 0000000000..3ba240a1d0 --- /dev/null +++ b/plugins/extraction/json.mli @@ -0,0 +1 @@ +val json_descr : Miniml.language_descr diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 1e491d36f7..db33615228 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,11 +16,16 @@ open Globnames object expects, and what these arguments will become in the ML object. *) -(* We eliminate from terms: 1) types 2) logical parts. - [Kother] stands both for logical or other reasons - (for instance user-declared implicit arguments w.r.t. extraction). *) +(* We eliminate from terms: + 1) types + 2) logical parts + 3) user-declared implicit arguments of a constant of constructor +*) -type kill_reason = Ktype | Kother +type kill_reason = + | Ktype + | Kprop + | Kimplicit of global_reference * int (* n-th arg of a cst or construct *) type sign = Keep | Kill of kill_reason @@ -118,7 +123,7 @@ and ml_ast = | MLcase of ml_type * ml_ast * ml_branch array | MLfix of int * Id.t array * ml_ast array | MLexn of string - | MLdummy + | MLdummy of kill_reason | MLaxiom | MLmagic of ml_ast @@ -197,6 +202,7 @@ type language_descr = { (* Concerning the source file *) file_suffix : string; + file_naming : module_path -> string; (* the second argument is a comment to add to the preamble *) preamble : Id.t -> std_ppcmds option -> module_path list -> unsafe_needs -> diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 9fdb0205f5..402fe4ffe6 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -299,10 +299,12 @@ let type_to_signature env t = let isKill = function Kill _ -> true | _ -> false -let isDummy = function Tdummy _ -> true | _ -> false +let isTdummy = function Tdummy _ -> true | _ -> false + +let isMLdummy = function MLdummy _ -> true | _ -> false let sign_of_id = function - | Dummy -> Kill Kother + | Dummy -> Kill Kprop | _ -> Keep (* Classification of signatures *) @@ -310,45 +312,44 @@ let sign_of_id = function type sign_kind = | EmptySig | NonLogicalSig (* at least a [Keep] *) - | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *) | SafeLogicalSig (* only [Kill Ktype] *) + | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *) let rec sign_kind = function | [] -> EmptySig | Keep :: _ -> NonLogicalSig | Kill k :: s -> - match sign_kind s with - | NonLogicalSig -> NonLogicalSig - | UnsafeLogicalSig -> UnsafeLogicalSig - | SafeLogicalSig | EmptySig -> - if k == Kother then UnsafeLogicalSig else SafeLogicalSig + match k, sign_kind s with + | _, NonLogicalSig -> NonLogicalSig + | Ktype, (SafeLogicalSig | EmptySig) -> SafeLogicalSig + | _, _ -> UnsafeLogicalSig (* Removing the final [Keep] in a signature *) let rec sign_no_final_keeps = function | [] -> [] | k :: s -> - let s' = k :: sign_no_final_keeps s in - match s' with [Keep] -> [] | _ -> s' + match k, sign_no_final_keeps s with + | Keep, [] -> [] + | k, l -> k::l (*s Removing [Tdummy] from the top level of a ML type. *) let type_expunge_from_sign env s t = - let rec expunge s t = - if List.is_empty s then t else match t with - | Tmeta {contents = Some t} -> expunge s t - | Tarr (a,b) -> - let t = expunge (List.tl s) b in - if List.hd s == Keep then Tarr (a, t) else t - | Tglob (r,l) -> - (match env r with - | Some mlt -> expunge s (type_subst_list l mlt) - | None -> assert false) - | _ -> assert false + let rec expunge s t = match s, t with + | [], _ -> t + | Keep :: s, Tarr(a,b) -> Tarr (a, expunge s b) + | Kill _ :: s, Tarr(a,b) -> expunge s b + | _, Tmeta {contents = Some t} -> expunge s t + | _, Tglob (r,l) -> + (match env r with + | Some mlt -> expunge s (type_subst_list l mlt) + | None -> assert false) + | _ -> assert false in let t = expunge (sign_no_final_keeps s) t in if lang () != Haskell && sign_kind s == UnsafeLogicalSig then - Tarr (Tdummy Kother, t) + Tarr (Tdummy Kprop, t) else t let type_expunge env t = @@ -385,7 +386,7 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with | MLfix (i1, id1, t1), MLfix (i2, id2, t2) -> Int.equal i1 i2 && Array.equal Id.equal id1 id2 && Array.equal eq_ml_ast t1 t2 | MLexn e1, MLexn e2 -> String.equal e1 e2 -| MLdummy, MLdummy -> true +| MLdummy k1, MLdummy k2 -> k1 == k2 | MLaxiom, MLaxiom -> true | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2 | _ -> false @@ -420,7 +421,7 @@ let ast_iter_rel f = | MLapp (a,l) -> iter n a; List.iter (iter n) l | MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l | MLmagic a -> iter n a - | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> () in iter 0 (*s Map over asts. *) @@ -439,7 +440,7 @@ let ast_map f = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l) | MLtuple l -> MLtuple (List.map f l) | MLmagic a -> MLmagic (f a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a (*s Map over asts, with binding depth as parameter. *) @@ -457,7 +458,7 @@ let ast_map_lift f n = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l) | MLtuple l -> MLtuple (List.map (f n) l) | MLmagic a -> MLmagic (f n a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a (*s Iter over asts. *) @@ -471,7 +472,7 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,_,l) | MLtuple l -> List.iter f l | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> () (*S Operations concerning De Bruijn indices. *) @@ -490,8 +491,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 @@ -507,9 +508,73 @@ let nb_occur_match = | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l | MLmagic a -> nb k a - | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0 + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0 in nb 1 +(* Replace unused variables by _ *) + +let dump_unused_vars a = + let rec ren env a = match a with + | MLrel i -> + let () = (List.nth env (i-1)) := true in a + + | MLlam (id,b) -> + let occ_id = ref false in + let b' = ren (occ_id::env) b in + if !occ_id then if b' == b then a else MLlam(id,b') + else MLlam(Dummy,b') + + | MLletin (id,b,c) -> + let occ_id = ref false in + let b' = ren env b in + let c' = ren (occ_id::env) c in + if !occ_id then + if b' == b && c' == c then a else MLletin(id,b',c') + else + (* 'let' without occurrence: shouldn't happen after simpl *) + MLletin(Dummy,b',c') + + | MLcase (t,e,br) -> + let e' = ren env e in + let br' = Array.smartmap (ren_branch env) br in + if e' == e && br' == br then a else MLcase (t,e',br') + + | MLfix (i,ids,v) -> + let env' = List.init (Array.length ids) (fun _ -> ref false) @ env in + let v' = Array.smartmap (ren env') v in + if v' == v then a else MLfix (i,ids,v') + + | MLapp (b,l) -> + let b' = ren env b and l' = List.smartmap (ren env) l in + if b' == b && l' == l then a else MLapp (b',l') + + | MLcons(t,r,l) -> + let l' = List.smartmap (ren env) l in + if l' == l then a else MLcons (t,r,l') + + | MLtuple l -> + let l' = List.smartmap (ren env) l in + if l' == l then a else MLtuple l' + + | MLmagic b -> + let b' = ren env b in + if b' == b then a else MLmagic b' + + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> a + + and ren_branch env ((ids,p,b) as tr) = + let occs = List.map (fun _ -> ref false) ids in + let b' = ren (List.rev_append occs env) b in + let ids' = + List.map2 + (fun id occ -> if !occ then id else Dummy) + ids occs + in + if b' == b && List.equal eq_ml_ident ids ids' then tr + else (ids',p,b') + in + ren [] a + (*s Lifting on terms. [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *) @@ -559,7 +624,7 @@ let gen_subst v d t = if i' < 1 then a else if i' <= Array.length v then match v.(i'-1) with - | None -> MLexn ("UNBOUND " ^ string_of_int i') + | None -> assert false | Some u -> ast_lift n u else MLrel (i+d) | a -> ast_map_lift subst n a @@ -813,8 +878,8 @@ let census_add, census_max, census_clean = try h := add k i !h with Not_found -> h := (k, Int.Set.singleton i) :: !h in - let maxf k = - let len = ref 0 and lst = ref Int.Set.empty and elm = ref k in + let maxf () = + let len = ref 0 and lst = ref Int.Set.empty and elm = ref MLaxiom in List.iter (fun (e, s) -> let n = Int.Set.cardinal s in @@ -843,7 +908,7 @@ let factor_branches o typ br = if o.opt_case_cst then (try census_add (branch_as_cst br.(i)) i with Impossible -> ()); done; - let br_factor, br_set = census_max MLdummy in + let br_factor, br_set = census_max () in census_clean (); let n = Int.Set.cardinal br_set in if Int.equal n 0 then None @@ -851,7 +916,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 @@ -926,7 +991,7 @@ let iota_gen br hd = in iota 0 hd let is_atomic = function - | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ -> true | _ -> false let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false @@ -948,9 +1013,20 @@ let expand_linear_let o id e = (* Some beta-iota reductions + simplifications. *) +let rec unmagic = function MLmagic e -> unmagic e | e -> e +let is_magic = function MLmagic _ -> true | _ -> false +let magic_hd a = match a with + | MLmagic _ :: _ -> a + | e :: a -> MLmagic e :: a + | [] -> assert false + let rec simpl o = function | MLapp (f, []) -> simpl o f - | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f) + | MLapp (MLapp(f,a),a') -> simpl o (MLapp(f,a@a')) + | MLapp (f, a) -> + (* When the head of the application is magic, no need for magic on args *) + let a = if is_magic f then List.map unmagic a else a in + simpl_app o (List.map (simpl o) a) (simpl o f) | MLcase (typ,e,br) -> let br = Array.map (fun (l,p,t) -> (l,p,simpl o t)) br in simpl_case o typ br (simpl o e) @@ -970,12 +1046,18 @@ let rec simpl o = function if ast_occurs_itvl 1 n c.(i) then MLfix (i, ids, Array.map (simpl o) c) else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *) + | MLmagic(MLmagic _ as e) -> simpl o e + | MLmagic(MLapp (f,l)) -> simpl o (MLapp (MLmagic f, l)) + | MLmagic(MLletin(id,c,e)) -> simpl o (MLletin(id,c,MLmagic e)) + | MLmagic(MLcase(typ,e,br)) -> + let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in + simpl o (MLcase(typ,e,br')) + | MLmagic(MLexn _ as e) -> e | a -> ast_map (simpl o) a (* invariant : list [a] of arguments is non-empty *) and simpl_app o a = function - | MLapp (f',a') -> simpl_app o (a'@a) f' | MLlam (Dummy,t) -> simpl o (MLapp (ast_pop t, List.tl a)) | MLlam (id,t) -> (* Beta redex *) @@ -986,6 +1068,11 @@ and simpl_app o a = function | _ -> let a' = List.map (ast_lift 1) (List.tl a) in simpl o (MLletin (id, List.hd a, MLapp (t, a')))) + | MLmagic (MLlam (id,t)) -> + (* When we've at least one argument, we permute the magic + and the lambda, to simplify things a bit (see #2795). + Alas, the 1st argument must also be magic then. *) + simpl_app o (magic_hd a) (MLlam (id,MLmagic t)) | MLletin (id,e1,e2) when o.opt_let_app -> (* Application of a letin: we push arguments inside *) MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a))) @@ -998,7 +1085,7 @@ and simpl_app o a = function let a' = List.map (ast_lift k) a in (l, p, simpl o (MLapp (t,a')))) br in simpl o (MLcase (typ,e,br')) - | (MLdummy | MLexn _) as e -> e + | (MLdummy _ | MLexn _) as e -> e (* We just discard arguments in those cases. *) | f -> MLapp (f,a) @@ -1049,20 +1136,26 @@ let rec select_via_bl l args = match l,args with (*s [kill_some_lams] removes some head lambdas according to the signature [bl]. This list is build on the identifier list model: outermost lambda is on the right. - [Rels] corresponding to removed lambdas are supposed not to occur, and + [Rels] corresponding to removed lambdas are not supposed to occur + (except maybe in the case of Kimplicit), and the other [Rels] are made correct via a [gen_subst]. Output is not directly a [ml_ast], compose with [named_lams] if needed. *) +let is_impl_kill = function Kill (Kimplicit _) -> true | _ -> false + let kill_some_lams bl (ids,c) = let n = List.length bl in let n' = List.fold_left (fun n b -> if b == Keep then (n+1) else n) 0 bl in if Int.equal n n' then ids,c - else if Int.equal n' 0 then [],ast_lift (-n) c + else if Int.equal n' 0 && not (List.exists is_impl_kill bl) + then [],ast_lift (-n) c else begin let v = Array.make n None in let rec parse_ids i j = function | [] -> () | Keep :: l -> v.(i) <- Some (MLrel j); parse_ids (i+1) (j+1) l + | Kill (Kimplicit _ as k) :: l -> + v.(i) <- Some (MLdummy k); parse_ids (i+1) j l | Kill _ :: l -> parse_ids (i+1) j l in parse_ids 0 1 bl; select_via_bl bl ids, gen_subst v (n'-n) c @@ -1070,11 +1163,19 @@ let kill_some_lams bl (ids,c) = (*s [kill_dummy_lams] uses the last function to kill the lambdas corresponding to a [dummy_name]. It can raise [Impossible] if there is nothing to do, or - if there is no lambda left at all. *) + if there is no lambda left at all. In addition, it now accepts a signature + that may mention some implicits. *) -let kill_dummy_lams c = +let rec merge_implicits ids s = match ids, s with + | [],_ -> [] + | _,[] -> List.map sign_of_id ids + | Dummy::ids, _::s -> Kill Kprop :: merge_implicits ids s + | _::ids, (Kill (Kimplicit _) as k)::s -> k :: merge_implicits ids s + | _::ids, _::s -> Keep :: merge_implicits ids s + +let kill_dummy_lams sign c = let ids,c = collect_lams c in - let bl = List.map sign_of_id ids in + let bl = merge_implicits ids (List.rev sign) in if not (List.memq Keep bl) then raise Impossible; let rec fst_kill n = function | [] -> raise Impossible @@ -1086,7 +1187,7 @@ let kill_dummy_lams c = let _, bl = List.chop skip bl in let c = named_lams ids_skip c in let ids',c = kill_some_lams bl (ids,c) in - ids, named_lams ids' c + (ids,bl), named_lams ids' c (*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c] and a signature [s] and builds a eta-long version. *) @@ -1100,12 +1201,12 @@ let eta_expansion_sign s (ids,c) = let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels in ids, MLapp (ast_lift (i-1) c, a) | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l - | Kill _ :: l -> abs (Dummy :: ids) (MLdummy :: rels) (i+1) l + | Kill k :: l -> abs (Dummy :: ids) (MLdummy k :: rels) (i+1) l in abs ids [] 1 s (*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e] in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas - corresponding to [Del] in [s]. *) + corresponding to [Kill _] in [s]. *) let case_expunge s e = let m = List.length s in @@ -1123,17 +1224,18 @@ let term_expunge s (ids,c) = if List.is_empty s then c else let ids,c = kill_some_lams (List.rev s) (ids,c) in - if List.is_empty ids && lang () != Haskell && List.mem (Kill Kother) s then - MLlam (Dummy, ast_lift 1 c) + if List.is_empty ids && lang () != Haskell && + sign_kind s == UnsafeLogicalSig + then 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 - purge the args of [MLrel r] corresponding to a [dummy_name]. +(*s [kill_dummy_args (ids,bl) r t] looks for occurrences of [MLrel r] in [t] + and purge the args of [MLrel r] corresponding to a [Kill] in [bl]. It makes eta-expansion if needed. *) -let kill_dummy_args ids r t = +let kill_dummy_args (ids,bl) r t = let m = List.length ids in - let bl = List.rev_map sign_of_id ids in + let sign = List.rev bl in let rec found n = function | MLrel r' when Int.equal r' (r + n) -> true | MLmagic e -> found n e @@ -1144,41 +1246,46 @@ let kill_dummy_args ids r t = let k = max 0 (m - (List.length a)) in let a = List.map (killrec n) a in let a = List.map (ast_lift k) a in - let a = select_via_bl bl (a @ (eta_args k)) in + let a = select_via_bl sign (a @ (eta_args k)) in named_lams (List.firstn k ids) (MLapp (ast_lift k e, a)) | e when found n e -> - let a = select_via_bl bl (eta_args m) in + let a = select_via_bl sign (eta_args m) in named_lams ids (MLapp (ast_lift m e, a)) | e -> ast_map_lift killrec n e in killrec 0 t (*s The main function for local [dummy] elimination. *) +let sign_of_args a = + List.map (function MLdummy k -> Kill k | _ -> Keep) a + let rec kill_dummy = function | MLfix(i,fi,c) -> (try - let ids,c = kill_dummy_fix i c in - ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids 1 (MLrel 1)) + let k,c = kill_dummy_fix i c [] in + ast_subst (MLfix (i,fi,c)) (kill_dummy_args k 1 (MLrel 1)) with Impossible -> MLfix (i,fi,Array.map kill_dummy c)) | MLapp (MLfix (i,fi,c),a) -> let a = List.map kill_dummy a in + (* Heuristics: if some arguments are implicit args, we try to + eliminate the corresponding arguments of the fixpoint *) (try - let ids,c = kill_dummy_fix i c in + let k,c = kill_dummy_fix i c (sign_of_args a) in let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in - let fake' = kill_dummy_args ids 1 fake in + let fake' = kill_dummy_args k 1 fake in ast_subst (MLfix (i,fi,c)) fake' with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),a)) | MLletin(id, MLfix (i,fi,c),e) -> (try - let ids,c = kill_dummy_fix i c in - let e = kill_dummy (kill_dummy_args ids 1 e) in + let k,c = kill_dummy_fix i c [] in + let e = kill_dummy (kill_dummy_args k 1 e) in MLletin(id, MLfix(i,fi,c),e) with Impossible -> MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e)) | MLletin(id,c,e) -> (try - let ids,c = kill_dummy_lams (kill_dummy_hd c) in - let e = kill_dummy (kill_dummy_args ids 1 e) in + let k,c = kill_dummy_lams [] (kill_dummy_hd c) in + let e = kill_dummy (kill_dummy_args k 1 e) in let c = kill_dummy c in if is_atomic c then ast_subst c e else MLletin (id, c, e) with Impossible -> MLletin(id,kill_dummy c,kill_dummy e)) @@ -1190,21 +1297,21 @@ and kill_dummy_hd = function | MLlam(id,e) -> MLlam(id, kill_dummy_hd e) | MLletin(id,c,e) -> (try - let ids,c = kill_dummy_lams (kill_dummy_hd c) in - let e = kill_dummy_hd (kill_dummy_args ids 1 e) in + let k,c = kill_dummy_lams [] (kill_dummy_hd c) in + let e = kill_dummy_hd (kill_dummy_args k 1 e) in let c = kill_dummy c in if is_atomic c then ast_subst c e else MLletin (id, c, e) with Impossible -> MLletin(id,kill_dummy c,kill_dummy_hd e)) | a -> a -and kill_dummy_fix i c = +and kill_dummy_fix i c s = let n = Array.length c in - let ids,ci = kill_dummy_lams (kill_dummy_hd c.(i)) in + let k,ci = kill_dummy_lams s (kill_dummy_hd c.(i)) in let c = Array.copy c in c.(i) <- ci; for j = 0 to (n-1) do - c.(j) <- kill_dummy (kill_dummy_args ids (n-i) c.(j)) + c.(j) <- kill_dummy (kill_dummy_args k (n-i) c.(j)) done; - ids,c + k,c (*s Putting things together. *) @@ -1267,7 +1374,7 @@ let rec ml_size = function | MLfix(_,_,f) -> ml_size_array f | MLletin (_,_,t) -> ml_size t | MLmagic t -> ml_size t - | MLglob _ | MLrel _ | MLexn _ | MLdummy | MLaxiom -> 0 + | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom -> 0 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l @@ -1351,10 +1458,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/mlutil.mli b/plugins/extraction/mlutil.mli index 0a71d2c838..c667552490 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -67,7 +67,8 @@ val type_expunge : abbrev_map -> ml_type -> ml_type val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type val eq_ml_type : ml_type -> ml_type -> bool -val isDummy : ml_type -> bool +val isTdummy : ml_type -> bool +val isMLdummy : ml_ast -> bool val isKill : sign -> bool val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast @@ -110,6 +111,8 @@ val ast_subst : ml_ast -> ml_ast -> ml_ast val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast +val dump_unused_vars : ml_ast -> ml_ast + val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast val inline : global_reference -> ml_ast -> bool @@ -125,8 +128,8 @@ exception Impossible type sign_kind = | EmptySig | NonLogicalSig (* at least a [Keep] *) - | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *) | SafeLogicalSig (* only [Kill Ktype] *) + | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *) val sign_kind : signature -> sign_kind diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 8158ac647e..60fe8e7620 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,7 @@ open Names open Globnames -open Errors +open CErrors open Util open Miniml open Table @@ -100,7 +100,7 @@ let ast_iter_references do_term do_cons do_type a = Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ - | MLdummy | MLaxiom | MLmagic _ -> () + | MLdummy _ | MLaxiom | MLmagic _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = @@ -269,7 +269,7 @@ let rec optim_se top to_appear s = function let a = normalize (ast_glob_subst !s a) in let i = inline r a in if i then s := Refmap'.add r a !s; - let d = match optimize_fix a with + let d = match dump_unused_vars (optimize_fix a) with | MLfix (0, _, [|c|]) -> Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|]) | a -> Dterm (r, a, t) @@ -283,7 +283,8 @@ let rec optim_se top to_appear s = function if inline rv.(i) fake_body then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s done; - (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) + let av' = Array.map dump_unused_vars av in + (l,SEdecl (Dfix (rv, av', tv))) :: (optim_se top to_appear s lse) | (l,SEmodule m) :: lse -> let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr} in (l,SEmodule m) :: (optim_se top to_appear s lse) @@ -309,7 +310,7 @@ let base_r = function let reset_needed, add_needed, add_needed_mp, found_needed, is_needed = let needed = ref Refset'.empty and needed_mps = ref MPset.empty in - ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty), + ((fun () -> needed := Refset'.empty; needed_mps := MPset.empty), (fun r -> needed := Refset'.add (base_r r) !needed), (fun mp -> needed_mps := MPset.add mp !needed_mps), (fun r -> needed := Refset'.remove (base_r r) !needed), @@ -379,24 +380,15 @@ let rec depcheck_struct = function let lse' = depcheck_se lse in if List.is_empty lse' then struc' else (mp,lse')::struc' -let is_prefix pre s = - let len = String.length pre in - let rec is_prefix_aux i = - if Int.equal i len then true - else pre.[i] == s.[i] && is_prefix_aux (succ i) +exception RemainingImplicit of kill_reason + +let check_for_remaining_implicits struc = + let check = function + | MLdummy (Kimplicit _ as k) -> raise (RemainingImplicit k) + | _ -> false in - is_prefix_aux 0 - -let check_implicits = function - | MLexn s -> - if String.length s > 8 && (s.[0] == 'U' || s.[0] == 'I') then - begin - if is_prefix "UNBOUND" s then assert false; - if is_prefix "IMPLICIT" s then - error_non_implicit (String.sub s 9 (String.length s - 9)); - end; - false - | _ -> false + try ignore (struct_ast_search check struc) + with RemainingImplicit k -> err_or_warn_remaining_implicit k let optimize_struct to_appear struc = let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in @@ -404,12 +396,16 @@ let optimize_struct to_appear struc = List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse)) struc in - ignore (struct_ast_search check_implicits opt_struc); - if library () then - List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc - else begin - reset_needed (); - List.iter add_needed (fst to_appear); - List.iter add_needed_mp (snd to_appear); - depcheck_struct opt_struc - end + let mini_struc = + if library () then + List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc + else + begin + reset_needed (); + List.iter add_needed (fst to_appear); + List.iter add_needed_mp (snd to_appear); + depcheck_struct opt_struc + end + in + let () = check_for_remaining_implicits mini_struc in + mini_struc diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index ca32f02921..dc8708249a 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 30ac3d3f89..1c29a9bc24 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,7 @@ (*s Production of Ocaml syntax. *) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -55,29 +55,36 @@ let keywords = "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] Id.Set.empty -let pp_open mp = str ("open "^ string_of_modfile mp ^"\n") +(* Note: do not shorten [str "foo" ++ fnl ()] into [str "foo\n"], + the '\n' character interacts badly with the Format boxing mechanism *) + +let pp_open mp = str ("open "^ string_of_modfile mp) ++ fnl () let pp_comment s = str "(* " ++ hov 0 s ++ str " *)" let pp_header_comment = function | None -> mt () - | Some com -> pp_comment com ++ fnl () ++ fnl () + | Some com -> pp_comment com ++ fnl2 () + +let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl () + +let pp_tdummy usf = + if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt () + +let pp_mldummy usf = + if usf.mldummy then + str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl () + else mt () let preamble _ comment used_modules usf = pp_header_comment comment ++ - prlist pp_open used_modules ++ - (if List.is_empty used_modules then mt () else fnl ()) ++ - (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++ - (if usf.mldummy then - str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n" - else mt ()) ++ - (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ()) + then_nl (prlist pp_open used_modules) ++ + then_nl (pp_tdummy usf ++ pp_mldummy usf) let sig_preamble _ comment used_modules usf = - pp_header_comment comment ++ fnl () ++ fnl () ++ - prlist pp_open used_modules ++ - (if List.is_empty used_modules then mt () else fnl ()) ++ - (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt()) + pp_header_comment comment ++ + then_nl (prlist pp_open used_modules) ++ + then_nl (pp_tdummy usf) (*s The pretty-printer for Ocaml syntax*) @@ -171,7 +178,11 @@ let rec pp_expr par env args = and apply2 st = pp_apply2 st par args in function | MLrel n -> - let id = get_db_name n env in apply (pr_id id) + let id = get_db_name n env in + (* Try to survive to the occurrence of a Dummy rel. + TODO: we should get rid of this hack (cf. #592) *) + let id = if Id.equal id dummy_name then Id.of_string "__" else id in + apply (pr_id id) | MLapp (f,args') -> let stl = List.map (pp_expr true env []) args' in pp_expr par env (stl @ args) f @@ -192,15 +203,18 @@ let rec pp_expr par env args = let args = List.skipn (projection_arity r) args in let record = List.hd args in pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) - with e when Errors.noncritical e -> apply (pp_global Term r)) + with e when CErrors.noncritical e -> apply (pp_global Term r)) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)")) - | MLdummy -> - str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLdummy k -> + (* An [MLdummy] may be applied, but I don't really care. *) + (match msg_of_implicit k with + | "" -> str "__" + | s -> str "__" ++ spc () ++ str ("(* "^s^" *)")) | MLmagic a -> pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args) | MLaxiom -> @@ -352,7 +366,7 @@ and pp_function env t = | MLcase(Tglob(r,_),MLrel 1,pv) when not (is_coinductive r) && List.is_empty (get_record_fields r) && not (is_custom_match pv) -> - if not (ast_occurs 1 (MLcase(Tunknown,MLdummy,pv))) then + if not (ast_occurs 1 (MLcase(Tunknown,MLaxiom,pv))) then pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ v 0 (pp_pat env' pv) @@ -378,9 +392,14 @@ and pp_fix par env i (ids,bl) args = fnl () ++ hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) +(* Ad-hoc double-newline in v boxes, with enough negative whitespace + to avoid indenting the intermediate blank line *) + +let cut2 () = brk (0,-100000) ++ brk (0,0) + let pp_val e typ = hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++ - str " **)") ++ fnl2 () + str " **)") ++ cut2 () (*s Pretty-printing of [Dfix] *) @@ -389,11 +408,11 @@ let pp_Dfix (rv,c,t) = (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv in let rec pp init i = - if i >= Array.length rv then - (if init then failwith "empty phrase" else mt ()) + if i >= Array.length rv then mt () else let void = is_inline_custom rv.(i) || - (not (is_custom rv.(i)) && match c.(i) with MLexn "UNUSED" -> true | _ -> false) + (not (is_custom rv.(i)) && + match c.(i) with MLexn "UNUSED" -> true | _ -> false) in if void then pp init (i+1) else @@ -401,7 +420,7 @@ let pp_Dfix (rv,c,t) = if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i)) else pp_function (empty_env ()) c.(i) in - (if init then mt () else fnl2 ()) ++ + (if init then mt () else cut2 ()) ++ pp_val names.(i) t.(i) ++ str (if init then "let rec " else "and ") ++ names.(i) ++ def ++ pp false (i+1) @@ -466,8 +485,8 @@ let pp_coind pl name = let pp_ind co kn ind = let prefix = if co then "__" else "" in - let some = ref false in - let init= ref (str "type ") in + let initkwd = str "type " in + let nextkwd = fnl () ++ str "and " in let names = Array.mapi (fun i p -> if p.ip_logical then mt () else pp_global Type (IndRef (kn,i))) @@ -480,29 +499,20 @@ let pp_ind co kn ind = p.ip_types) ind.ind_packets in - let rec pp i = + let rec pp i kwd = if i >= Array.length ind.ind_packets then mt () else let ip = (kn,i) in let ip_equiv = ind.ind_equiv, i in let p = ind.ind_packets.(i) in - if is_custom (IndRef ip) then pp (i+1) - else begin - some := true; - if p.ip_logical then pp_logical_ind p ++ pp (i+1) - else - let s = !init in - begin - init := (fnl () ++ str "and "); - s ++ - (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ - pp_one_ind - prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++ - pp (i+1) - end - end + if is_custom (IndRef ip) then pp (i+1) kwd + else if p.ip_logical then pp_logical_ind p ++ pp (i+1) kwd + else + kwd ++ (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ + pp_one_ind prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++ + pp (i+1) nextkwd in - let st = pp 0 in if !some then st else failwith "empty phrase" + pp 0 initkwd (*s Pretty-printing of a declaration. *) @@ -515,8 +525,8 @@ let pp_mind kn i = | Standard -> pp_ind false kn i let pp_decl = function - | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase" - | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Dtype (r,_,_) when is_inline_custom r -> mt () + | Dterm (r,_,_) when is_inline_custom r -> mt () | Dind (kn,i) -> pp_mind kn i | Dtype (r, l, t) -> let name = pp_global Type r in @@ -524,13 +534,13 @@ let pp_decl = function let ids, def = try let ids,s = find_type_custom r in - pp_string_parameters ids, str "=" ++ spc () ++ str s + pp_string_parameters ids, str " =" ++ spc () ++ str s with Not_found -> pp_parameters l, - if t == Taxiom then str "(* AXIOM TO BE REALIZED *)" - else str "=" ++ spc () ++ pp_type false l t + if t == Taxiom then str " (* AXIOM TO BE REALIZED *)" + else str " =" ++ spc () ++ pp_type false l t in - hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) + hov 2 (str "type " ++ ids ++ name ++ def) | Dterm (r, a, t) -> let def = if is_custom r then str (" = " ^ find_custom r) @@ -564,8 +574,8 @@ let pp_alias_decl ren = function rv let pp_spec = function - | Sval (r,_) when is_inline_custom r -> failwith "empty phrase" - | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Sval (r,_) when is_inline_custom r -> mt () + | Stype (r,_,_) when is_inline_custom r -> mt () | Sind (kn,i) -> pp_mind kn i | Sval (r,t) -> let def = pp_type false [] t in @@ -577,15 +587,15 @@ let pp_spec = function let ids, def = try let ids, s = find_type_custom r in - pp_string_parameters ids, str "= " ++ str s + pp_string_parameters ids, str " =" ++ spc () ++ str s with Not_found -> let ids = pp_parameters l in match ot with | None -> ids, mt () - | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" - | Some t -> ids, str "=" ++ spc () ++ pp_type false l t + | Some Taxiom -> ids, str " (* AXIOM TO BE REALIZED *)" + | Some t -> ids, str " =" ++ spc () ++ pp_type false l t in - hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) + hov 2 (str "type " ++ ids ++ name ++ def) let pp_alias_spec ren = function | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } @@ -602,7 +612,7 @@ let rec pp_specif = function | (l,Spec s) -> (try let ren = Common.check_duplicate (top_visible_mp ()) l in - hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++ + hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++ fnl () ++ str "end" ++ fnl () ++ pp_alias_spec ren s with Not_found -> pp_spec s) @@ -610,15 +620,15 @@ let rec pp_specif = function let def = pp_module_type [] mt in let def' = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in - hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++ + hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++ (try let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def') + fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def') with Not_found -> Pp.mt ()) | (l,Smodtype mt) -> let def = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in - hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++ (try let ren = Common.check_duplicate (top_visible_mp ()) l in fnl () ++ str ("module type "^ren^" = ") ++ name @@ -634,10 +644,16 @@ and pp_module_type params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MTsig (mp, sign) -> push_visible mp params; - let l = List.map pp_specif sign in + let try_pp_specif l x = + let px = pp_specif x in + if Pp.is_empty px then l else px::l + in + (* We cannot use fold_right here due to side effects in pp_specif *) + let l = List.fold_left try_pp_specif [] sign in + let l = List.rev l in pop_visible (); - str "sig " ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ + str "sig" ++ fnl () ++ + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl () ++ str "end" | MTwith(mt,ML_With_type(idl,vl,typ)) -> let ids = pp_parameters (rename_tvars keywords vl) in @@ -667,7 +683,7 @@ let rec pp_structure_elem = function | (l,SEdecl d) -> (try let ren = Common.check_duplicate (top_visible_mp ()) l in - hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++ + hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++ fnl () ++ str "end" ++ fnl () ++ pp_alias_decl ren d with Not_found -> pp_decl d) @@ -681,8 +697,8 @@ let rec pp_structure_elem = function let def = pp_module_expr [] m.ml_mod_expr in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 - (str "module " ++ name ++ typ ++ str " = " ++ - (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++ + (str "module " ++ name ++ typ ++ str " =" ++ + (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++ (try let ren = Common.check_duplicate (top_visible_mp ()) l in fnl () ++ str ("module "^ren^" = ") ++ name @@ -690,7 +706,7 @@ let rec pp_structure_elem = function | (l,SEmodtype m) -> let def = pp_module_type [] m in let name = pp_modname (MPdot (top_visible_mp (), l)) in - hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++ (try let ren = Common.check_duplicate (top_visible_mp ()) l in fnl () ++ str ("module type "^ren^" = ") ++ name @@ -707,35 +723,47 @@ and pp_module_expr params = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MEstruct (mp, sel) -> push_visible mp params; - let l = List.map pp_structure_elem sel in + let try_pp_structure_elem l x = + let px = pp_structure_elem x in + if Pp.is_empty px then l else px::l + in + (* We cannot use fold_right here due to side effects in pp_structure_elem *) + let l = List.fold_left try_pp_structure_elem [] sel in + let l = List.rev l in pop_visible (); - str "struct " ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ + str "struct" ++ fnl () ++ + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl () ++ str "end" +let rec prlist_sep_nonempty sep f = function + | [] -> mt () + | [h] -> f h + | h::t -> + let e = f h in + let r = prlist_sep_nonempty sep f t in + if Pp.is_empty e then r + else e ++ sep () ++ r + let do_struct f s = - let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt () - in let ppl (mp,sel) = push_visible mp []; - let p = prlist_strict pp sel in + let p = prlist_sep_nonempty cut2 f sel in (* for monolithic extraction, we try to simulate the unavailability of [MPfile] in names by artificially nesting these [MPfile] *) (if modular () then pop_visible ()); p in - let p = prlist_strict ppl s in + let p = prlist_sep_nonempty cut2 ppl s in (if not (modular ()) then repeat (List.length s) pop_visible ()); - p + v 0 p ++ fnl () let pp_struct s = do_struct pp_structure_elem s let pp_signature s = do_struct pp_specif s -let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt () - let ocaml_descr = { keywords = keywords; file_suffix = ".ml"; + file_naming = file_of_modfile; preamble = preamble; pp_struct = pp_struct; sig_suffix = Some ".mli"; @@ -743,5 +771,3 @@ let ocaml_descr = { pp_sig = pp_signature; pp_decl = pp_decl; } - - diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli index 4e796792e3..f579a54b8b 100644 --- a/plugins/extraction/ocaml.mli +++ b/plugins/extraction/ocaml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 69dea25aac..a6309e61f9 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,7 @@ (*s Production of Scheme syntax. *) open Pp -open Errors +open CErrors open Util open Names open Miniml @@ -126,7 +126,7 @@ let rec pp_expr env args = | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) paren (str "error" ++ spc () ++ qs s) - | MLdummy -> + | MLdummy _ -> str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLmagic a -> pp_expr env args a @@ -183,7 +183,8 @@ let pp_decl = function prvecti (fun i r -> let void = is_inline_custom r || - (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false) + (not (is_custom r) && + match defs.(i) with MLexn "UNUSED" -> true | _ -> false) in if void then mt () else @@ -212,7 +213,7 @@ and pp_module_expr = function | MEfunctor _ -> mt () (* for the moment we simply discard unapplied functors *) | MEident _ | MEapply _ -> assert false - (* should be expansed in extract_env *) + (* should be expanded in extract_env *) let pp_struct = let pp_sel (mp,sel) = @@ -225,6 +226,7 @@ let pp_struct = let scheme_descr = { keywords = keywords; file_suffix = ".scm"; + file_naming = file_of_modfile; preamble = preamble; pp_struct = pp_struct; sig_suffix = None; diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli index f0e36e09d9..5e1ec0d5e0 100644 --- a/plugins/extraction/scheme.mli +++ b/plugins/extraction/scheme.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 44d760ccdf..5e7d810c93 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,7 +15,7 @@ open Libobject open Goptions open Libnames open Globnames -open Errors +open CErrors open Util open Pp open Miniml @@ -72,8 +72,6 @@ let mp_length mp = | _ -> 1 in len mp -let visible_con kn = at_toplevel (base_mp (con_modpath kn)) - let rec prefixes_mp mp = match mp with | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp') | _ -> MPset.singleton mp @@ -105,17 +103,30 @@ let labels_of_ref r = (* Theses tables are not registered within coq save/undo mechanism since we reset their contents at each run of Extraction *) -(*s Constants tables. *) +(* We use [constant_body] (resp. [mutual_inductive_body]) as checksum + to ensure that the table contents aren't outdated. *) -let terms = ref (Cmap_env.empty : ml_decl Cmap_env.t) -let init_terms () = terms := Cmap_env.empty -let add_term kn d = terms := Cmap_env.add kn d !terms -let lookup_term kn = Cmap_env.find kn !terms +(*s Constants tables. *) -let types = ref (Cmap_env.empty : ml_schema Cmap_env.t) -let init_types () = types := Cmap_env.empty -let add_type kn s = types := Cmap_env.add kn s !types -let lookup_type kn = Cmap_env.find kn !types +let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t) +let init_typedefs () = typedefs := Cmap_env.empty +let add_typedef kn cb t = + typedefs := Cmap_env.add kn (cb,t) !typedefs +let lookup_typedef kn cb = + try + let (cb0,t) = Cmap_env.find kn !typedefs in + if cb0 == cb then Some t else None + with Not_found -> None + +let cst_types = + ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t) +let init_cst_types () = cst_types := Cmap_env.empty +let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types +let lookup_cst_type kn cb = + try + let (cb0,s) = Cmap_env.find kn !cst_types in + if cb0 == cb then Some s else None + with Not_found -> None (*s Inductives table. *) @@ -124,7 +135,14 @@ let inductives = let init_inductives () = inductives := Mindmap_env.empty let add_ind kn mib ml_ind = inductives := Mindmap_env.add kn (mib,ml_ind) !inductives -let lookup_ind kn = Mindmap_env.find kn !inductives +let lookup_ind kn mib = + try + let (mib0,ml_ind) = Mindmap_env.find kn !inductives in + if mib == mib0 then Some ml_ind + else None + with Not_found -> None + +let unsafe_lookup_ind kn = snd (Mindmap_env.find kn !inductives) let inductive_kinds = ref (Mindmap_env.empty : inductive_kind Mindmap_env.t) @@ -244,10 +262,10 @@ let safe_basename_of_global r = | ConstRef kn -> Label.to_id (con_label kn) | IndRef (kn,0) -> Label.to_id (mind_label kn) | IndRef (kn,i) -> - (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename + (try (unsafe_lookup_ind kn).ind_packets.(i).ip_typename with Not_found -> last_chance r) | ConstructRef ((kn,i),j) -> - (try (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1) + (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) with Not_found -> last_chance r) | VarRef _ -> assert false @@ -275,83 +293,96 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) (*S Warning and Error messages. *) -let err s = errorlabstrm "Extraction" s +let err s = user_err ~hdr:"Extraction" s + +let warn_extraction_axiom_to_realize = + CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction" + (fun axioms -> + let s = if Int.equal (List.length axioms) 1 then "axiom" else "axioms" in + strbrk ("The following "^s^" must be realized in the extracted code:") + ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms) + ++ str "." ++ fnl ()) + +let warn_extraction_logical_axiom = + CWarnings.create ~name:"extraction-logical-axiom" ~category:"extraction" + (fun axioms -> + let s = + if Int.equal (List.length axioms) 1 then "axiom was" else "axioms were" + in + (strbrk ("The following logical "^s^" encountered:") ++ + hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms ++ str ".\n") + ++ strbrk "Having invalid logical axiom in the environment when extracting" + ++ spc () ++ strbrk "may lead to incorrect or non-terminating ML terms." ++ + fnl ())) let warning_axioms () = let info_axioms = Refset'.elements !info_axioms in - if List.is_empty info_axioms then () - else begin - let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in - msg_warning - (str ("The following "^s^" must be realized in the extracted code:") - ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms) - ++ str "." ++ fnl ()) - end; + if not (List.is_empty info_axioms) then + warn_extraction_axiom_to_realize info_axioms; let log_axioms = Refset'.elements !log_axioms in - if List.is_empty log_axioms then () - else begin - let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were" - in - msg_warning - (str ("The following logical "^s^" encountered:") ++ - hov 1 - (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n") - ++ - str "Having invalid logical axiom in the environment when extracting" ++ - spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ - fnl ()) - end + if not (List.is_empty log_axioms) then + warn_extraction_logical_axiom log_axioms + +let warn_extraction_opaque_accessed = + CWarnings.create ~name:"extraction-opaque-accessed" ~category:"extraction" + (fun lst -> strbrk "The extraction is currently set to bypass opacity, " ++ + strbrk "the following opaque constant bodies have been accessed :" ++ + lst ++ str "." ++ fnl ()) + +let warn_extraction_opaque_as_axiom = + CWarnings.create ~name:"extraction-opaque-as-axiom" ~category:"extraction" + (fun lst -> strbrk "The extraction now honors the opacity constraints by default, " ++ + strbrk "the following opaque constants have been extracted as axioms :" ++ + lst ++ str "." ++ fnl () ++ + strbrk "If necessary, use \"Set Extraction AccessOpaque\" to change this." + ++ fnl ()) let warning_opaques accessed = let opaques = Refset'.elements !opaques in - if List.is_empty opaques then () - else + if not (List.is_empty opaques) then let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in - if accessed then - msg_warning - (str "The extraction is currently set to bypass opacity,\n" ++ - str "the following opaque constant bodies have been accessed :" ++ - lst ++ str "." ++ fnl ()) - else - msg_warning - (str "The extraction now honors the opacity constraints by default,\n" ++ - str "the following opaque constants have been extracted as axioms :" ++ - lst ++ str "." ++ fnl () ++ - str "If necessary, use \"Set Extraction AccessOpaque\" to change this." - ++ fnl ()) - -let warning_both_mod_and_cst q mp r = - msg_warning - (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++ - str "do you mean module " ++ - pr_long_mp mp ++ - str " or object " ++ - pr_long_global r ++ str " ?" ++ fnl () ++ - str "First choice is assumed, for the second one please use " ++ - str "fully qualified name." ++ fnl ()) + if accessed then warn_extraction_opaque_accessed lst + else warn_extraction_opaque_as_axiom lst + +let warning_ambiguous_name = + CWarnings.create ~name:"extraction-ambiguous-name" ~category:"extraction" + (fun (q,mp,r) -> strbrk "The name " ++ pr_qualid q ++ strbrk " is ambiguous, " ++ + strbrk "do you mean module " ++ + pr_long_mp mp ++ + strbrk " or object " ++ + pr_long_global r ++ str " ?" ++ fnl () ++ + strbrk "First choice is assumed, for the second one please use " ++ + strbrk "fully qualified name." ++ fnl ()) let error_axiom_scheme r i = err (str "The type scheme axiom " ++ spc () ++ safe_pr_global r ++ spc () ++ str "needs " ++ int i ++ str " type variable(s).") +let warn_extraction_inside_module = + CWarnings.create ~name:"extraction-inside-module" ~category:"extraction" + (fun () -> strbrk "Extraction inside an opened module is experimental." ++ + strbrk "In case of problem, close it first.") + + let check_inside_module () = if Lib.is_modtype () then err (str "You can't do that within a Module Type." ++ fnl () ++ str "Close it and try again.") else if Lib.is_module () then - msg_warning - (str "Extraction inside an opened module is experimental.\n" ++ - str "In case of problem, close it first.\n") + warn_extraction_inside_module () let check_inside_section () = if Lib.sections_are_opened () then err (str "You can't do that within a section." ++ fnl () ++ str "Close it and try again.") -let warning_id s = - msg_warning (str ("The identifier "^s^ - " contains __ which is reserved for the extraction")) +let warn_extraction_reserved_identifier = + CWarnings.create ~name:"extraction-reserved-identifier" ~category:"extraction" + (fun s -> strbrk ("The identifier "^s^ + " contains __ which is reserved for the extraction")) + +let warning_id s = warn_extraction_reserved_identifier s let error_constant r = err (safe_pr_global r ++ str " is not a constant.") @@ -373,9 +404,15 @@ let error_no_module_expr mp = ++ str "some Declare Module outside any Module Type.\n" ++ str "This situation is currently unsupported by the extraction.") -let error_singleton_become_prop id = +let error_singleton_become_prop id og = + let loc = + match og with + | Some g -> fnl () ++ str "in " ++ safe_pr_global g ++ + str " (or in its mutual block)" + | None -> mt () + in err (str "The informative inductive type " ++ pr_id id ++ - str " has a Prop instance.\n" ++ + str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++ str "This happens when a sort-polymorphic singleton inductive type\n" ++ str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++ str "The Ocaml extraction cannot handle this situation yet.\n" ++ @@ -401,29 +438,50 @@ let error_MPfile_as_mod mp b = "Monolithic Extraction cannot deal with this situation.\n"^ "Please "^s2^"use (Recursive) Extraction Library instead.\n")) -let msg_non_implicit r n id = - let name = match id with - | Anonymous -> "" - | Name id -> "(" ^ Id.to_string id ^ ") " - in - "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r) - -let error_non_implicit msg = - err (str (msg ^ " still occurs after extraction.") ++ - fnl () ++ str "Please check the Extraction Implicit declarations.") +let argnames_of_global r = + let typ = Global.type_of_global_unsafe r in + let rels,_ = + decompose_prod (Reduction.whd_all (Global.env ()) typ) in + List.rev_map fst rels + +let msg_of_implicit = function + | Kimplicit (r,i) -> + let name = match List.nth (argnames_of_global r) (i-1) with + | Anonymous -> "" + | Name id -> "(" ^ Id.to_string id ^ ") " + in + (String.ordinal i)^" argument "^name^"of "^(string_of_global r) + | Ktype | Kprop -> "" + +let error_remaining_implicit k = + let s = msg_of_implicit k in + err (str ("An implicit occurs after extraction : "^s^".") ++ fnl () ++ + str "Please check your Extraction Implicit declarations." ++ fnl() ++ + str "You might also try Unset Extraction SafeImplicits to force" ++ + fnl() ++ str "the extraction of unsafe code and review it manually.") + +let warn_extraction_remaining_implicit = + CWarnings.create ~name:"extraction-remaining-implicit" ~category:"extraction" + (fun s -> strbrk ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++ + strbrk "Extraction SafeImplicits is unset, extracting nonetheless," + ++ strbrk "but this code is potentially unsafe, please review it manually.") + +let warning_remaining_implicit k = + let s = msg_of_implicit k in + warn_extraction_remaining_implicit s let check_loaded_modfile mp = match base_mp mp with | MPfile dp -> if not (Library.library_is_loaded dp) then begin match base_mp (Lib.current_mp ()) with | MPfile dp' when not (DirPath.equal dp dp') -> - err (str ("Please load library "^(DirPath.to_string dp^" first."))) + err (str "Please load library " ++ pr_dirpath dp ++ str " first.") | _ -> () end | _ -> () let info_file f = - Flags.if_verbose msg_info + Flags.if_verbose Feedback.msg_info (str ("The file "^f^" has been created by extraction.")) @@ -554,7 +612,7 @@ let _ = declare_string_option (*s Extraction Lang *) -type lang = Ocaml | Haskell | Scheme +type lang = Ocaml | Haskell | Scheme | JSON let lang_ref = Summary.ref Ocaml ~name:"ExtrLang" @@ -635,32 +693,39 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) (*s Extraction Implicit *) +let safe_implicit = my_bool_option "SafeImplicits" true + +let err_or_warn_remaining_implicit k = + if safe_implicit () then + error_remaining_implicit k + else + warning_remaining_implicit k + type int_or_id = ArgInt of int | ArgId of Id.t let implicits_table = Summary.ref Refmap'.empty ~name:"ExtrImplicit" let implicits_of_global r = - try Refmap'.find r !implicits_table with Not_found -> [] + try Refmap'.find r !implicits_table with Not_found -> Int.Set.empty let add_implicits r l = - let typ = Global.type_of_global_unsafe r in - let rels,_ = - decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in - let names = List.rev_map fst rels in + let names = argnames_of_global r in let n = List.length names in - let check = function + let add_arg s = function | ArgInt i -> - if 1 <= i && i <= n then i + if 1 <= i && i <= n then Int.Set.add i s else err (int i ++ str " is not a valid argument number for " ++ safe_pr_global r) | ArgId id -> - (try List.index Name.equal (Name id) names - with Not_found -> - err (str "No argument " ++ pr_id id ++ str " for " ++ - safe_pr_global r)) + try + let i = List.index Name.equal (Name id) names in + Int.Set.add i s + with Not_found -> + err (str "No argument " ++ pr_id id ++ str " for " ++ + safe_pr_global r) in - let l' = List.map check l in - implicits_table := Refmap'.add r l' !implicits_table + let ints = List.fold_left add_arg Int.Set.empty l in + implicits_table := Refmap'.add r ints !implicits_table (* Registration of operations for rollback. *) @@ -815,7 +880,7 @@ let extract_constant_inline inline r ids s = | ConstRef kn -> let env = Global.env () in let typ = Global.type_of_global_unsafe (ConstRef kn) in - let typ = Reduction.whd_betadeltaiota env typ in + let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin let nargs = Hook.get use_type_scheme_nb_args env typ in @@ -851,6 +916,6 @@ let extract_inductive r s l optstr = (*s Tables synchronization. *) let reset_tables () = - init_terms (); init_types (); init_inductives (); + init_typedefs (); init_cst_types (); init_inductives (); init_inductive_kinds (); init_recursors (); init_projs (); init_axioms (); init_opaques (); reset_modfile () diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 1acbe3555f..15a08756c0 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,7 +13,7 @@ open Miniml open Declarations module Refset' : CSig.SetS with type elt = global_reference -module Refmap' : Map.S with type key = global_reference +module Refmap' : CSig.MapS with type key = global_reference val safe_basename_of_global : global_reference -> Id.t @@ -21,8 +21,7 @@ val safe_basename_of_global : global_reference -> Id.t val warning_axioms : unit -> unit val warning_opaques : bool -> unit -val warning_both_mod_and_cst : - qualid -> module_path -> global_reference -> unit +val warning_ambiguous_name : ?loc:Loc.t -> qualid * module_path * global_reference -> unit val warning_id : string -> unit val error_axiom_scheme : global_reference -> int -> 'a val error_constant : global_reference -> 'a @@ -30,7 +29,7 @@ val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : module_path -> module_path -> 'a val error_no_module_expr : module_path -> 'a -val error_singleton_become_prop : Id.t -> 'a +val error_singleton_become_prop : Id.t -> global_reference option -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a @@ -38,8 +37,8 @@ val error_MPfile_as_mod : module_path -> bool -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit val check_loaded_modfile : module_path -> unit -val msg_non_implicit : global_reference -> int -> Name.t -> string -val error_non_implicit : string -> 'a +val msg_of_implicit : kill_reason -> string +val err_or_warn_remaining_implicit : kill_reason -> unit val info_file : string -> unit @@ -55,7 +54,6 @@ val string_of_modfile : module_path -> string val file_of_modfile : module_path -> string val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool -val visible_con : constant -> bool val mp_length : module_path -> int val prefixes_mp : module_path -> MPset.t val common_prefix_from_list : @@ -65,14 +63,22 @@ val labels_of_ref : global_reference -> module_path * Label.t list (*s Some table-related operations *) -val add_term : constant -> ml_decl -> unit -val lookup_term : constant -> ml_decl +(* For avoiding repeated extraction of the same constant or inductive, + we use cache functions below. Indexing by constant name isn't enough, + due to modules we could have a same constant name but different + content. So we check that the [constant_body] hasn't changed from + recording time to retrieving time. Same for inductive : we store + [mutual_inductive_body] as checksum. In both case, we should ideally + also check the env *) -val add_type : constant -> ml_schema -> unit -val lookup_type : constant -> ml_schema +val add_typedef : constant -> constant_body -> ml_type -> unit +val lookup_typedef : constant -> constant_body -> ml_type option + +val add_cst_type : constant -> constant_body -> ml_schema -> unit +val lookup_cst_type : constant -> constant_body -> ml_schema option val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit -val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind +val lookup_ind : mutual_inductive -> mutual_inductive_body -> ml_ind option val add_inductive_kind : mutual_inductive -> inductive_kind -> unit val is_coinductive : global_reference -> bool @@ -142,7 +148,7 @@ val file_comment : unit -> string (*s Target language. *) -type lang = Ocaml | Haskell | Scheme +type lang = Ocaml | Haskell | Scheme | JSON val lang : unit -> lang (*s Extraction modes: modular or monolithic, library or minimal ? @@ -166,7 +172,7 @@ val to_keep : global_reference -> bool (*s Table for implicits arguments *) -val implicits_of_global : global_reference -> int list +val implicits_of_global : global_reference -> Int.Set.t (*s Table for user-given custom ML extractions. *) diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget index 1fe09f6fa2..9c30c5eb3e 100644 --- a/plugins/extraction/vo.itarget +++ b/plugins/extraction/vo.itarget @@ -1,3 +1,11 @@ +ExtrHaskellBasic.vo +ExtrHaskellNatNum.vo +ExtrHaskellNatInt.vo +ExtrHaskellNatInteger.vo +ExtrHaskellZNum.vo +ExtrHaskellZInt.vo +ExtrHaskellZInteger.vo +ExtrHaskellString.vo ExtrOcamlBasic.vo ExtrOcamlIntConv.vo ExtrOcamlBigIntConv.vo @@ -5,4 +13,4 @@ ExtrOcamlNatInt.vo ExtrOcamlNatBigInt.vo ExtrOcamlZInt.vo ExtrOcamlZBigInt.vo -ExtrOcamlString.vo
\ No newline at end of file +ExtrOcamlString.vo |