diff options
Diffstat (limited to 'plugins')
28 files changed, 561 insertions, 309 deletions
diff --git a/plugins/extraction/ExtrOcamlChar.v b/plugins/extraction/ExtrOcamlChar.v new file mode 100644 index 0000000000..1e68365dd3 --- /dev/null +++ b/plugins/extraction/ExtrOcamlChar.v @@ -0,0 +1,45 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Extraction to Ocaml : extract ascii to OCaml's char type *) + +Require Coq.extraction.Extraction. + +Require Import Ascii String Coq.Strings.Byte. + +Extract Inductive ascii => char +[ +"(* If this appears, you're using Ascii internals. Please don't *) + (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> + let f b i = if b then 1 lsl i else 0 in + Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))" +] +"(* If this appears, you're using Ascii internals. Please don't *) + (fun f c -> + let n = Char.code c in + let h i = (n land (1 lsl i)) <> 0 in + f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". + +Extract Constant zero => "'\000'". +Extract Constant one => "'\001'". +Extract Constant shift => + "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)". + +Extract Inlined Constant ascii_dec => "(=)". +Extract Inlined Constant Ascii.eqb => "(=)". + +(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *) +Extract Inductive byte => char +["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"]. + +Extract Inlined Constant Byte.eqb => "(=)". +Extract Inlined Constant Byte.byte_eq_dec => "(=)". +Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)". +Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)". diff --git a/plugins/extraction/ExtrOcamlNativeString.v b/plugins/extraction/ExtrOcamlNativeString.v new file mode 100644 index 0000000000..ec3da1e444 --- /dev/null +++ b/plugins/extraction/ExtrOcamlNativeString.v @@ -0,0 +1,87 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Extraction to Ocaml : extract ascii to OCaml's char type + and string to OCaml's string type. *) + +Require Coq.extraction.Extraction. + +Require Import Ascii String Coq.Strings.Byte. +Require Export ExtrOcamlChar. + +(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *) +Extract Inductive byte => char +["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"]. + +Extract Inlined Constant Byte.eqb => "(=)". +Extract Inlined Constant Byte.byte_eq_dec => "(=)". +Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)". +Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)". + +(* This differs from ExtrOcamlString.v: the latter extracts "string" + to "char list", and we extract "string" to "string" *) + +Extract Inductive string => "string" +[ +(* EmptyString *) +"(* If this appears, you're using String internals. Please don't *) + """" +" +(* String *) +"(* If this appears, you're using String internals. Please don't *) + (fun (c, s) -> String.make 1 c ^ s) +" +] +"(* If this appears, you're using String internals. Please don't *) + (fun f0 f1 s -> + let l = String.length s in + if l = 0 then f0 else f1 (String.get s 0) (String.sub s 1 (l-1))) +". + +Extract Inlined Constant String.string_dec => "(=)". +Extract Inlined Constant String.eqb => "(=)". +Extract Inlined Constant String.append => "(^)". +Extract Inlined Constant String.concat => "String.concat". +Extract Inlined Constant String.prefix => + "(fun s1 s2 -> + let l1 = String.length s1 and l2 = String.length s2 in + l1 <= l2 && String.sub s2 0 l1 = s1)". +Extract Inlined Constant String.string_of_list_ascii => + "(fun l -> + let a = Array.of_list l in + String.init (Array.length a) (fun i -> a.(i)))". +Extract Inlined Constant String.list_ascii_of_string => + "(fun s -> + Array.to_list (Array.init (String.length s) (fun i -> s.[i])))". +Extract Inlined Constant String.string_of_list_byte => + "(fun l -> + let a = Array.of_list l in + String.init (Array.length a) (fun i -> a.(i)))". +Extract Inlined Constant String.list_byte_of_string => + "(fun s -> + Array.to_list (Array.init (String.length s) (fun i -> s.[i])))". + +(* Other operations in module String (at the time of this writing): + String.length + String.get + String.substring + String.index + String.findex + They all use type "nat". If we know that "nat" extracts + to O | S of nat, we can provide OCaml implementations + for these functions that work directly on OCaml's strings. + However "nat" could be extracted to other OCaml types... +*) + +(* +Definition test := "ceci est un test"%string. + +Recursive Extraction test Ascii.zero Ascii.one. +*) diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index 6265a67577..18c5ed3fe4 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -13,43 +13,6 @@ Require Coq.extraction.Extraction. Require Import Ascii String Coq.Strings.Byte. - -Extract Inductive ascii => char -[ -"(* If this appears, you're using Ascii internals. Please don't *) - (fun (b0,b1,b2,b3,b4,b5,b6,b7) -> - let f b i = if b then 1 lsl i else 0 in - Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))" -] -"(* If this appears, you're using Ascii internals. Please don't *) - (fun f c -> - let n = Char.code c in - let h i = (n land (1 lsl i)) <> 0 in - f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))". - -Extract Constant zero => "'\000'". -Extract Constant one => "'\001'". -Extract Constant shift => - "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)". - -Extract Inlined Constant ascii_dec => "(=)". -Extract Inlined Constant Ascii.eqb => "(=)". +Require Export ExtrOcamlChar. Extract Inductive string => "char list" [ "[]" "(::)" ]. - -(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *) -Extract Inductive byte => char -["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"]. - -Extract Inlined Constant Byte.eqb => "(=)". -Extract Inlined Constant Byte.byte_eq_dec => "(=)". -Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)". -Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)". - -(* -Definition test := "ceci est un test"%string. -Definition test2 := List.map (option_map Byte.to_nat) (List.map Byte.of_nat (List.seq 0 256)). -Definition test3 := List.map ascii_of_nat (List.seq 0 256). - -Recursive Extraction test Ascii.zero Ascii.one test2 test3 byte_rect. -*) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 2f3f42c5f6..29da12de40 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -14,7 +14,6 @@ open Names open ModPath open Namegen open Nameops -open Libnames open Table open Miniml open Mlutil @@ -616,10 +615,15 @@ let pp_module mp = [Extract Inductive ascii => char] has been declared, then the constants are directly turned into chars *) -let mk_ind path s = - MutInd.make2 (MPfile (dirpath_of_string path)) (Label.make s) +let ascii_type_name = "core.ascii.type" +let ascii_constructor_name = "core.ascii.ascii" -let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" +let is_ascii_registered () = + Coqlib.has_ref ascii_type_name + && Coqlib.has_ref ascii_constructor_name + +let ascii_type_ref () = Coqlib.lib_ref ascii_type_name +let ascii_constructor_ref () = Coqlib.lib_ref ascii_constructor_name let check_extract_ascii () = try @@ -628,15 +632,18 @@ let check_extract_ascii () = | Haskell -> "Prelude.Char" | _ -> raise Not_found in - String.equal (find_custom (GlobRef.IndRef (ind_ascii, 0))) (char_type) + String.equal (find_custom @@ ascii_type_ref ()) (char_type) with Not_found -> false let is_list_cons l = List.for_all (function MLcons (_,GlobRef.ConstructRef(_,_),[]) -> true | _ -> false) l let is_native_char = function - | MLcons(_,GlobRef.ConstructRef ((kn,0),1),l) -> - MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l + | MLcons(_,gr,l) -> + is_ascii_registered () + && GlobRef.equal gr (ascii_constructor_ref ()) + && check_extract_ascii () + && is_list_cons l | _ -> false let get_native_char c = @@ -649,3 +656,84 @@ let get_native_char c = Char.chr (cumul l) let pp_native_char c = str ("'"^Char.escaped (get_native_char c)^"'") + +(** Special hack for constants of type String.string : if an + [Extract Inductive string => string] has been declared, then + the constants are directly turned into string literals *) + +let string_type_name = "core.string.type" +let empty_string_name = "core.string.empty" +let string_constructor_name = "core.string.string" + +let is_string_registered () = + Coqlib.has_ref string_type_name + && Coqlib.has_ref empty_string_name + && Coqlib.has_ref string_constructor_name + +let string_type_ref () = Coqlib.lib_ref string_type_name +let empty_string_ref () = Coqlib.lib_ref empty_string_name +let string_constructor_ref () = Coqlib.lib_ref string_constructor_name + +let check_extract_string () = + try + let string_type = match lang () with + | Ocaml -> "string" + | Haskell -> "Prelude.String" + | _ -> raise Not_found + in + String.equal (find_custom @@ string_type_ref ()) string_type + with Not_found -> false + +(* The argument is known to be of type Coq.Strings.String.string. + Check that it is built from constructors EmptyString and String + with constant ascii arguments. *) + +let rec is_native_string_rec empty_string_ref string_constructor_ref = function + (* "EmptyString" constructor *) + | MLcons(_, gr, []) -> GlobRef.equal gr empty_string_ref + (* "String" constructor *) + | MLcons(_, gr, [hd; tl]) -> + GlobRef.equal gr string_constructor_ref + && is_native_char hd + && is_native_string_rec empty_string_ref string_constructor_ref tl + (* others *) + | _ -> false + +(* Here we first check that the argument is the type registered as + core.string.type and that extraction to native strings was + requested. Then we check every character via + [is_native_string_rec]. *) + +let is_native_string c = + match c with + | MLcons(_, GlobRef.ConstructRef(ind, j), l) -> + is_string_registered () + && GlobRef.equal (GlobRef.IndRef ind) (string_type_ref ()) + && check_extract_string () + && is_native_string_rec (empty_string_ref ()) (string_constructor_ref ()) c + | _ -> false + +(* Extract the underlying string. *) + +let get_native_string c = + let buf = Buffer.create 64 in + let rec get = function + (* "EmptyString" constructor *) + | MLcons(_, gr, []) when GlobRef.equal gr (empty_string_ref ()) -> + Buffer.contents buf + (* "String" constructor *) + | MLcons(_, gr, [hd; tl]) when GlobRef.equal gr (string_constructor_ref ()) -> + Buffer.add_char buf (get_native_char hd); + get tl + (* others *) + | _ -> assert false + in get c + +(* Printing the underlying string. *) + +let pp_native_string c = + str ("\"" ^ String.escaped (get_native_string c) ^ "\"") + +(* Registered sig type *) + +let sig_type_ref () = Coqlib.lib_ref "core.sig.type" diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index e4e9c4c527..9dbc09dd06 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -70,10 +70,6 @@ val reset_renaming_tables : reset_kind -> unit val set_keywords : Id.Set.t -> unit -(** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *) - -val mk_ind : string -> string -> MutInd.t - (** Special hack for constants of type Ascii.ascii : if an [Extract Inductive ascii => char] has been declared, then the constants are directly turned into chars *) @@ -81,3 +77,14 @@ val mk_ind : string -> string -> MutInd.t val is_native_char : ml_ast -> bool val get_native_char : ml_ast -> char val pp_native_char : ml_ast -> Pp.t + +(** Special hack for constants of type String.string : if an + [Extract Inductive string => string] has been declared, then + the constants are directly turned into string literals *) + +val is_native_string : ml_ast -> bool +val get_native_string : ml_ast -> string +val pp_native_string : ml_ast -> Pp.t + +(* Registered sig type *) +val sig_type_ref : unit -> GlobRef.t diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 35110552ab..853be82eb8 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -27,32 +27,7 @@ open Common (***************************************) let toplevel_env () = - let get_reference = function - | (_,kn), Lib.Leaf Libobject.AtomicObject o -> - let mp,l = KerName.repr kn in - begin match Libobject.object_tag o with - | "CONSTANT" -> - let constant = Global.lookup_constant (Constant.make1 kn) in - Some (l, SFBconst constant) - | "INDUCTIVE" -> - let inductive = Global.lookup_mind (MutInd.make1 kn) in - Some (l, SFBmind inductive) - | _ -> None - end - | (_,kn), Lib.Leaf Libobject.ModuleObject _ -> - let mp,l = KerName.repr kn in - let modl = Global.lookup_module (MPdot (mp, l)) in - Some (l, SFBmodule modl) - | (_,kn), Lib.Leaf Libobject.ModuleTypeObject _ -> - let mp,l = KerName.repr kn in - let modtype = Global.lookup_modtype (MPdot (mp, l)) in - Some (l, SFBmodtype modtype) - | (_,kn), Lib.Leaf Libobject.IncludeObject _ -> - user_err Pp.(str "No extraction of toplevel Include yet.") - | _ -> None - in - List.rev (List.map_filter get_reference (Lib.contents ())) - + List.rev (Safe_typing.structure_body_of_safe_env (Global.safe_env ())) let environment_until dir_opt = let rec parse = function diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index f0053ba6b5..eef050efbd 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -109,8 +109,8 @@ let rec pp_type par vl t = (try Id.print (List.nth vl (pred i)) with Failure _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r - | Tglob (GlobRef.IndRef(kn,0),l) - when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> + | Tglob (gr,l) + when not (keep_singleton ()) && GlobRef.equal gr (sig_type_ref ()) -> pp_type true vl (List.hd l) | Tglob (r,l) -> pp_par par @@ -171,6 +171,7 @@ let rec pp_expr par env args = assert (List.is_empty args); begin match a with | _ when is_native_char c -> pp_native_char c + | _ when is_native_string c -> pp_native_string c | [] -> pp_global Cons r | [a] -> pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 66429833b9..97cad87825 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -165,8 +165,8 @@ let pp_type par vl t = | Tglob (r,[a1;a2]) when is_infix r -> pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) | Tglob (r,[]) -> pp_global Type r - | Tglob (GlobRef.IndRef(kn,0),l) - when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> + | Tglob (gr,l) + when not (keep_singleton ()) && GlobRef.equal gr (sig_type_ref ()) -> pp_tuple_light pp_rec l | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r @@ -249,6 +249,7 @@ let rec pp_expr par env args = assert (List.is_empty args); begin match a with | _ when is_native_char c -> pp_native_char c + | _ when is_native_string c -> pp_native_string c | [a1;a2] when is_infix r -> let pp = pp_expr true env [] in pp_par par (pp a1 ++ str (get_infix r) ++ pp a2) diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index c87eb7c3c9..3ea4974a87 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -26,9 +26,9 @@ module NamedDecl = Context.Named.Declaration (* The instantiate tactic *) -let instantiate_evar evk (ist,rawc) sigma = +let instantiate_evar evk (ist,rawc) env sigma = let evi = Evd.find sigma evk in - let filtered = Evd.evar_filtered_env evi in + let filtered = Evd.evar_filtered_env env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in let lvar = { ltac_constrs = constrvars; @@ -36,7 +36,7 @@ let instantiate_evar evk (ist,rawc) sigma = ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; } in - let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in + let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in tclEVARS sigma' let evar_list sigma c = @@ -48,6 +48,7 @@ let evar_list sigma c = let instantiate_tac n c ido = Proofview.V82.tactic begin fun gl -> + let env = Global.env () in let sigma = gl.sigma in let evl = match ido with @@ -69,16 +70,17 @@ let instantiate_tac n c ido = user_err Pp.(str "Not enough uninstantiated existential variables."); if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let evk,_ = List.nth evl (n-1) in - instantiate_evar evk c sigma gl + instantiate_evar evk c env sigma gl end let instantiate_tac_by_name id c = Proofview.V82.tactic begin fun gl -> + let env = Global.env () in let sigma = gl.sigma in let evk = try Evd.evar_key id sigma with Not_found -> user_err Pp.(str "Unknown existential variable.") in - instantiate_evar evk c sigma gl + instantiate_evar evk c env sigma gl end let let_evar name typ = diff --git a/plugins/micromega/Zify.v b/plugins/micromega/Zify.v index 785a53fafa..18cd196148 100644 --- a/plugins/micromega/Zify.v +++ b/plugins/micromega/Zify.v @@ -87,4 +87,4 @@ Ltac applySpec S := (** [zify_post_hook] is there to be redefined. *) Ltac zify_post_hook := idtac. -Ltac zify := zify_op ; (iter_specs applySpec) ; zify_post_hook. +Ltac zify := zify_op ; (zify_iter_specs applySpec) ; zify_post_hook. diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v index 97f6fe0613..edfb5a2a94 100644 --- a/plugins/micromega/ZifyInst.v +++ b/plugins/micromega/ZifyInst.v @@ -523,3 +523,22 @@ Instance SatProdPos : Saturate Z.mul := SatOk := Z.mul_pos_pos |}. Add Saturate SatProdPos. + +Lemma pow_pos_strict : + forall a b, + 0 < a -> 0 < b -> 0 < a ^ b. +Proof. + intros. + apply Z.pow_pos_nonneg; auto. + apply Z.lt_le_incl;auto. +Qed. + + +Instance SatPowPos : Saturate Z.pow := + {| + PArg1 := fun x => 0 < x; + PArg2 := fun y => 0 < y; + PRes := fun r => 0 < r; + SatOk := pow_pos_strict + |}. +Add Saturate SatPowPos. diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index cb15274736..61234145e1 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -395,50 +395,40 @@ let saturate_by_linear_equalities sys = output_sys sys output_sys sys'; sys' -(* let saturate_linear_equality_non_linear sys0 = - let (l,_) = extract_all (is_substitution false) sys0 in - let rec elim l acc = - match l with - | [] -> acc - | (v,pc)::l' -> - let nc = saturate (non_linear_pivot sys0 pc v) (sys0@acc) in - elim l' (nc@acc) in - elim l [] - *) - -let bounded_vars (sys : WithProof.t list) = - let l = fst (extract_all (fun ((p, o), prf) -> LinPoly.is_variable p) sys) in - List.fold_left (fun acc (i, wp) -> IMap.add i wp acc) IMap.empty l - -let rec power n p = if n = 1 then p else WithProof.product p (power (n - 1) p) - -let bound_monomial mp m = - if Monomial.is_var m || Monomial.is_const m then None - else - try - Some - (Monomial.fold - (fun v i acc -> - let wp = IMap.find v mp in - WithProof.product (power i wp) acc) - m (WithProof.const (Int 1))) - with Not_found -> None - let bound_monomials (sys : WithProof.t list) = - let mp = bounded_vars sys in - let m = + let l = + extract_all + (fun ((p, o), _) -> + match LinPoly.get_bound p with + | None -> None + | Some Vect.Bound.{cst; var; coeff} -> + Some (Monomial.degree (LinPoly.MonT.retrieve var))) + sys + in + let deg = + List.fold_left (fun acc ((p, o), _) -> max acc (LinPoly.degree p)) 0 sys + in + let vars = List.fold_left - (fun acc ((p, _), _) -> - Vect.fold - (fun acc v _ -> - let m = LinPoly.MonT.retrieve v in - match bound_monomial mp m with - | None -> acc - | Some r -> IMap.add v r acc) - acc p) - IMap.empty sys + (fun acc ((p, o), _) -> ISet.union (LinPoly.monomials p) acc) + ISet.empty sys + in + let bounds = + saturate_bin + (fun (i1, w1) (i2, w2) -> + if i1 + i2 > deg then None + else + match WithProof.mul_bound w1 w2 with + | None -> None + | Some b -> Some (i1 + i2, b)) + (fst l) + in + let has_mon (_, ((p, o), _)) = + match LinPoly.get_bound p with + | None -> false + | Some Vect.Bound.{cst; var; coeff} -> ISet.mem var vars in - IMap.fold (fun _ e acc -> e :: acc) m [] + List.map snd (List.filter has_mon bounds) @ snd l let develop_constraints prfdepth n_spec sys = LinPoly.MonT.clear (); diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 92a2222cfa..cdadde8621 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -2416,6 +2416,36 @@ let nqa = (fun _ x -> x) Mc.cnfQ qq_domain_spec dump_qexpr nlinear_prover_R +let print_lia_profile () = + Simplex.( + let { number_of_successes + ; number_of_failures + ; success_pivots + ; failure_pivots + ; average_pivots + ; maximum_pivots } = + Simplex.get_profile_info () + in + Feedback.msg_notice + Pp.( + (* successes *) + str "number of successes: " + ++ int number_of_successes ++ fnl () + (* success pivots *) + ++ str "number of success pivots: " + ++ int success_pivots ++ fnl () + (* failure *) + ++ str "number of failures: " + ++ int number_of_failures ++ fnl () + (* failure pivots *) + ++ str "number of failure pivots: " + ++ int failure_pivots ++ fnl () + (* Other *) + ++ str "average number of pivots: " + ++ int average_pivots ++ fnl () + ++ str "maximum number of pivots: " + ++ int maximum_pivots ++ fnl ())) + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli index 37ea560241..bcfc47357f 100644 --- a/plugins/micromega/coq_micromega.mli +++ b/plugins/micromega/coq_micromega.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*val is_ground_tac : EConstr.constr -> unit Proofview.tactic*) val psatz_Z : int -> unit Proofview.tactic -> unit Proofview.tactic val psatz_Q : int -> unit Proofview.tactic -> unit Proofview.tactic val psatz_R : int -> unit Proofview.tactic -> unit Proofview.tactic @@ -21,6 +20,7 @@ val sos_Q : unit Proofview.tactic -> unit Proofview.tactic val sos_R : unit Proofview.tactic -> unit Proofview.tactic val lra_Q : unit Proofview.tactic -> unit Proofview.tactic val lra_R : unit Proofview.tactic -> unit Proofview.tactic +val print_lia_profile : unit -> unit (** {5 Use Micromega independently from tactics. } *) diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg index edf8106f30..d0f70bceac 100644 --- a/plugins/micromega/g_micromega.mlg +++ b/plugins/micromega/g_micromega.mlg @@ -28,10 +28,6 @@ open Tacarg DECLARE PLUGIN "micromega_plugin" -TACTIC EXTEND RED -| [ "myred" ] -> { Tactics.red_in_concl } -END - TACTIC EXTEND PsatzZ | [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i (Tacinterp.tactic_of_value ist t)) @@ -87,3 +83,6 @@ TACTIC EXTEND PsatzQ | [ "psatz_Q" tactic(t) ] -> { (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) } END +VERNAC COMMAND EXTEND ShowLiaProfile CLASSIFIED AS QUERY +| [ "Show" "Lia" "Profile" ] -> { Coq_micromega.print_lia_profile () } +END diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 66f263c0b1..2b5fac32a2 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -34,12 +34,13 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF END TACTIC EXTEND ITER -| [ "iter_specs" tactic(t)] -> { Zify.iter_specs t } +| [ "zify_iter_specs" tactic(t)] -> { Zify.iter_specs t } END TACTIC EXTEND TRANS | [ "zify_op" ] -> { Zify.zify_tac } -| [ "saturate" ] -> { Zify.saturate } +| [ "zify_saturate" ] -> { Zify.saturate } +| [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t } END VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 03f042647c..160b492d3d 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -140,6 +140,25 @@ let saturate p f sys = Printexc.print_backtrace stdout; raise x +let saturate_bin (f : 'a -> 'a -> 'a option) (l : 'a list) = + let rec map_with acc e l = + match l with + | [] -> acc + | e' :: l' -> ( + match f e e' with + | None -> map_with acc e l' + | Some r -> map_with (r :: acc) e l' ) + in + let rec map2_with acc l' = + match l' with [] -> acc | e' :: l' -> map2_with (map_with acc e' l) l' + in + let rec iterate acc l' = + match map2_with [] l' with + | [] -> List.rev_append l' acc + | res -> iterate (List.rev_append l' acc) res + in + iterate [] l + open Num open Big_int diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index ef8d154b13..5dcaf3be44 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -116,6 +116,7 @@ val simplify : ('a -> 'a option) -> 'a list -> 'a list option val saturate : ('a -> 'b option) -> ('b * 'a -> 'a -> 'a option) -> 'a list -> 'a list +val saturate_bin : ('a -> 'a -> 'a option) -> 'a list -> 'a list val generate : ('a -> 'b option) -> 'a list -> 'b list val app_funs : ('a -> 'b option) list -> 'a -> 'b option val command : string -> string array -> 'a -> 'b diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index a4f9b60b14..b20213979b 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -379,6 +379,8 @@ module LinPoly = struct else acc) [] l + let get_bound p = Vect.Bound.of_vect p + let min_list (l : int list) = match l with [] -> None | e :: l -> Some (List.fold_left min e l) @@ -892,8 +894,9 @@ module WithProof = struct if Vect.is_null r && n >/ Int 0 then ((LinPoly.product p p1, o1), ProofFormat.mul_cst_proof n prf1) else ( - Printf.printf "mult_error %a [*] %a\n" LinPoly.pp p output - ((p1, o1), prf1); + if debug then + Printf.printf "mult_error %a [*] %a\n" LinPoly.pp p output + ((p1, o1), prf1); raise InvalidProof ) let cutting_plane ((p, o), prf) = @@ -1027,6 +1030,31 @@ module WithProof = struct else None in saturate select gen sys0 + + open Vect.Bound + + let mul_bound w1 w2 = + let (p1, o1), prf1 = w1 in + let (p2, o2), prf2 = w2 in + match (LinPoly.get_bound p1, LinPoly.get_bound p2) with + | None, _ | _, None -> None + | ( Some {cst = c1; var = v1; coeff = c1'} + , Some {cst = c2; var = v2; coeff = c2'} ) -> ( + let good_coeff b o = + match o with + | Eq -> Some (minus_num b) + | _ -> if b <=/ Int 0 then Some (minus_num b) else None + in + match (good_coeff c1 o2, good_coeff c2 o1) with + | None, _ | _, None -> None + | Some c1, Some c2 -> + let ext_mult c w = + if c =/ Int 0 then zero else mult (LinPoly.constant c) w + in + Some + (addition + (addition (product w1 w2) (ext_mult c1 w2)) + (ext_mult c2 w1)) ) end (* Local Variables: *) diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index 7e905ac69b..4b56b037e0 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -224,6 +224,8 @@ module LinPoly : sig p is linear in x i.e x does not occur in b and a is a constant such that [pred a] *) + val get_bound : t -> Vect.Bound.t option + val product : t -> t -> t (** [product p q] @return the product of the polynomial [p*q] *) @@ -372,4 +374,5 @@ module WithProof : sig val saturate_subst : bool -> t list -> t list val is_substitution : bool -> t -> var option + val mul_bound : t -> t -> t option end diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index ade8143f3c..54976221bc 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -18,6 +18,49 @@ type ('a, 'b) sum = Inl of 'a | Inr of 'b let debug = false +(** Exploiting profiling information *) + +let profile_info = ref [] +let nb_pivot = ref 0 + +type profile_info = + { number_of_successes : int + ; number_of_failures : int + ; success_pivots : int + ; failure_pivots : int + ; average_pivots : int + ; maximum_pivots : int } + +let init_profile = + { number_of_successes = 0 + ; number_of_failures = 0 + ; success_pivots = 0 + ; failure_pivots = 0 + ; average_pivots = 0 + ; maximum_pivots = 0 } + +let get_profile_info () = + let update_profile + { number_of_successes + ; number_of_failures + ; success_pivots + ; failure_pivots + ; average_pivots + ; maximum_pivots } (b, i) = + { number_of_successes = (number_of_successes + if b then 1 else 0) + ; number_of_failures = (number_of_failures + if b then 0 else 1) + ; success_pivots = (success_pivots + if b then i else 0) + ; failure_pivots = (failure_pivots + if b then 0 else i) + ; average_pivots = average_pivots + 1 (* number of proofs *) + ; maximum_pivots = max maximum_pivots i } + in + let p = List.fold_left update_profile init_profile !profile_info in + profile_info := []; + { p with + average_pivots = + ( try (p.success_pivots + p.failure_pivots) / p.average_pivots + with Division_by_zero -> 0 ) } + type iset = unit IMap.t type tableau = Vect.t IMap.t @@ -60,10 +103,7 @@ let output_tableau o t = t let output_env o t = - IMap.iter - (fun k v -> - Printf.fprintf o "%a : %a\n" LinPoly.pp_var k WithProof.output v) - t + IMap.iter (fun k v -> Printf.fprintf o "%i : %a\n" k WithProof.output v) t let output_vars o m = IMap.iter (fun k _ -> Printf.fprintf o "%a " LinPoly.pp_var k) m @@ -224,6 +264,7 @@ let pivot_with (m : tableau) (v : var) (p : Vect.t) = IMap.map (fun (r : Vect.t) -> pivot_row r v p) m let pivot (m : tableau) (r : var) (c : var) = + incr nb_pivot; let row = safe_find "pivot" r m in let piv = solve_column c r row in IMap.add c piv (pivot_with (IMap.remove r m) c piv) @@ -477,8 +518,11 @@ let make_farkas_proof (env : WithProof.t IMap.t) vm v = try let x', b = IMap.find x vm in let n = if b then n else Num.minus_num n in - WithProof.mult (Vect.cst n) (IMap.find x' env) - with Not_found -> WithProof.mult (Vect.cst n) (IMap.find x env) + let prf = IMap.find x' env in + WithProof.mult (Vect.cst n) prf + with Not_found -> + let prf = IMap.find x env in + WithProof.mult (Vect.cst n) prf end) WithProof.zero v @@ -493,21 +537,43 @@ type ('a, 'b) hitkind = let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) = let n, r = Vect.decomp_cst v in - let f = frac_num n in - if f =/ Int 0 then Forget (* The solution is integral *) + let fn = frac_num n in + if fn =/ Int 0 then Forget (* The solution is integral *) else - (* This is potentially a cut *) - let t = - if f </ Int 1 // Int 2 then - let t' = Int 1 // f in - if Num.is_integer_num t' then t' -/ Int 1 else Num.floor_num t' - else Int 1 - in - let cut_coeff1 v = + (* The cut construction is from: + Letchford and Lodi. Strengthening Chvatal-Gomory cuts and Gomory fractional cuts. + + We implement the classic Proposition 2 from the "known results" + *) + + (* Proposition 3 requires all the variables to be restricted and is + therefore not always applicable. *) + (* let ccoeff_prop1 v = frac_num v in + let ccoeff_prop3 v = + (* mixed integer cut *) let fv = frac_num v in - if fv <=/ Int 1 -/ f then fv // (Int 1 -/ f) else (Int 1 -/ fv) // f + Num.min_num fv (fn */ (Int 1 -/ fv) // (Int 1 -/ fn)) in - let cut_coeff2 v = frac_num (t */ v) in + let ccoeff_prop3 = + if Restricted.is_restricted x rst then ("Prop3", ccoeff_prop3) + else ("Prop1", ccoeff_prop1) + in *) + let n0_5 = Int 1 // Int 2 in + (* If the fractional part [fn] is small, we construct the t-cut. + If the fractional part [fn] is big, we construct the t-cut of the negated row. + (This is only a cut if all the fractional variables are restricted.) + *) + let ccoeff_prop2 = + let tmin = + if fn </ n0_5 then (* t-cut *) + Num.ceiling_num (n0_5 // fn) + else + (* multiply by -1 & t-cut *) + minus_num (Num.ceiling_num (n0_5 // (Int 1 -/ fn))) + in + ("Prop2", fun v -> frac_num (v */ tmin)) + in + let ccoeff = ccoeff_prop2 in let cut_vector ccoeff = Vect.fold (fun acc x n -> @@ -516,35 +582,31 @@ let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) = Vect.null r in let lcut = - List.map - (fun cv -> Vect.normalise (cut_vector cv)) - [cut_coeff1; cut_coeff2] + ( fst ccoeff + , make_farkas_proof env vm (Vect.normalise (cut_vector (snd ccoeff))) ) in - let lcut = List.map (make_farkas_proof env vm) lcut in - let check_cutting_plane c = + let check_cutting_plane (p, c) = match WithProof.cutting_plane c with | None -> if debug then - Printf.printf "This is not a cutting plane for %a\n%a:" LinPoly.pp_var - x WithProof.output c; + Printf.printf "%s: This is not a cutting plane for %a\n%a:" p + LinPoly.pp_var x WithProof.output c; None | Some (v, prf) -> if debug then ( - Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x; + Printf.printf "%s: This is a cutting plane for %a:" p LinPoly.pp_var x; Printf.printf " %a\n" WithProof.output (v, prf) ); - if snd v = Eq then (* Unsat *) Some (x, (v, prf)) - else - let vl = Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol) in - if eval_op Ge vl (Int 0) then ( - if debug then - Printf.printf "The cut is feasible %s >= 0 \n" - (Num.string_of_num vl); - None ) - else Some (x, (v, prf)) + Some (x, (v, prf)) in - match find_some check_cutting_plane lcut with + match check_cutting_plane lcut with | Some r -> Hit r - | None -> Keep (x, v) + | None -> + let has_unrestricted = + Vect.fold + (fun acc v vl -> acc || not (Restricted.is_restricted v rst)) + false r + in + if has_unrestricted then Keep (x, v) else Forget let merge_result_old oldr f x = match oldr with @@ -681,12 +743,16 @@ let integer_solver lp = isolve env None vr res let integer_solver lp = + nb_pivot := 0; if debug then Printf.printf "Input integer solver\n%a\n" WithProof.output_sys (List.map WithProof.of_cstr lp); match integer_solver lp with - | None -> None + | None -> + profile_info := (false, !nb_pivot) :: !profile_info; + None | Some prf -> + profile_info := (true, !nb_pivot) :: !profile_info; if debug then Printf.fprintf stdout "Proof %a\n" ProofFormat.output_proof prf; Some prf diff --git a/plugins/micromega/simplex.mli b/plugins/micromega/simplex.mli index 19bcce3590..ff672edafd 100644 --- a/plugins/micromega/simplex.mli +++ b/plugins/micromega/simplex.mli @@ -9,6 +9,20 @@ (************************************************************************) open Polynomial +(** Profiling *) + +type profile_info = + { number_of_successes : int + ; number_of_failures : int + ; success_pivots : int + ; failure_pivots : int + ; average_pivots : int + ; maximum_pivots : int } + +val get_profile_info : unit -> profile_info + +(** Simplex interface *) + val optimise : Vect.t -> cstr list -> (Num.num option * Num.num option) option val find_point : cstr list -> Vect.t option val find_unsat_certificate : cstr list -> Vect.t option diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 5d8ae83853..e71c89b4db 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -965,6 +965,43 @@ let trans_concl t = let tclTHENOpt e tac tac' = match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac' +let assert_inj t = + init_cache (); + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + try + ignore (get_injection env evd t); + Tacticals.New.tclIDTAC + with Not_found -> + Tacticals.New.tclFAIL 0 (Pp.str " InjTyp does not exist")) + +let do_let tac (h : Constr.named_declaration) = + match h with + | Context.Named.Declaration.LocalAssum _ -> Tacticals.New.tclIDTAC + | Context.Named.Declaration.LocalDef (id, t, ty) -> + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + try + ignore (get_injection env evd (EConstr.of_constr ty)); + tac id.Context.binder_name t ty + with Not_found -> Tacticals.New.tclIDTAC) + +let iter_let tac = + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let sign = Environ.named_context env in + Tacticals.New.tclMAP (do_let tac) sign) + +let iter_let (tac : Ltac_plugin.Tacinterp.Value.t) = + init_cache (); + iter_let (fun (id : Names.Id.t) (t : Constr.types) (ty : Constr.types) -> + Ltac_plugin.Tacinterp.Value.apply tac + [ Ltac_plugin.Tacinterp.Value.of_constr (EConstr.mkVar id) + ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr t) + ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr ty) ]) + let zify_tac = Proofview.Goal.enter (fun gl -> Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"]; diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli index 9e3cf5d24c..4930a845c9 100644 --- a/plugins/micromega/zify.mli +++ b/plugins/micromega/zify.mli @@ -27,3 +27,5 @@ module Saturate : S val zify_tac : unit Proofview.tactic val saturate : unit Proofview.tactic val iter_specs : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic +val assert_inj : EConstr.constr -> unit Proofview.tactic +val iter_let : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index f5d53cbbf3..34533670f8 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -573,27 +573,16 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. Require Import ZifyClasses ZifyInst. Require Zify. - -(** [is_inj T] returns true iff the type T has an injection *) -Ltac is_inj T := - match T with - | _ => let x := constr:(_ : InjTyp T _ ) in true - | _ => false - end. - (* [elim_let] replaces a let binding (x := e : t) by an equation (x = e) if t is an injected type *) -Ltac elim_let := - repeat - match goal with - | x := ?t : ?ty |- _ => - let b := is_inj ty in - match b with - | true => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - end - end. +Ltac elim_binding x t ty := + let h := fresh "heq_" x in + pose proof (@eq_refl ty x : @eq ty x t) as h; + try clearbody x. + +Ltac elim_let := zify_iter_let elim_binding. Ltac zify := intros ; elim_let ; - Zify.zify ; ZifyInst.saturate. + Zify.zify ; ZifyInst.zify_saturate. diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg index 84964a7bd2..7c653b223e 100644 --- a/plugins/omega/g_omega.mlg +++ b/plugins/omega/g_omega.mlg @@ -21,40 +21,9 @@ DECLARE PLUGIN "omega_plugin" { open Ltac_plugin -open Names -open Coq_omega -open Stdarg - -let eval_tactic name = - let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in - let kn = KerName.make (ModPath.MPfile dp) (Label.make name) in - let tac = Tacenv.interp_ltac kn in - Tacinterp.eval_tactic tac - -let omega_tactic l = - let tacs = List.map - (function - | "nat" -> eval_tactic "zify_nat" - | "positive" -> eval_tactic "zify_positive" - | "N" -> eval_tactic "zify_N" - | "Z" -> eval_tactic "zify_op" - | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s))) - (Util.List.sort_uniquize String.compare l) - in - Tacticals.New.tclTHEN - (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) - (omega_solver) } TACTIC EXTEND omega -| [ "omega" ] -> { omega_tactic [] } +| [ "omega" ] -> { Coq_omega.omega_solver } END - -TACTIC EXTEND omega' -| [ "omega" "with" ne_ident_list(l) ] -> - { omega_tactic (List.map Names.Id.to_string l) } -| [ "omega" "with" "*" ] -> - { Tacticals.New.tclTHEN (eval_tactic "zify") (omega_tactic []) } -END - diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v index 609c9d5ab8..7c5cd135fe 100644 --- a/plugins/ssr/ssrsetoid.v +++ b/plugins/ssr/ssrsetoid.v @@ -18,9 +18,7 @@ than [eq] or [iff], e.g. a [RewriteRelation], by doing: [Require Import ssreflect. Require Setoid.] - This file's instances have priority 12 > other stdlib instances - and each [Under_rel] instance comes with a [Hint Cut] directive - (otherwise Ring_polynom.v won't compile because of unbounded search). + This file's instances have priority 12 > other stdlib instances. (Note: this file could be skipped when porting [under] to stdlib2.) *) @@ -38,85 +36,3 @@ Instance compat_Reflexive : RelationClasses.Reflexive R -> ssrclasses.Reflexive R | 12. Proof. now trivial. Qed. - -(** Add instances so that ['Under[ F i ]] terms, - that is, [Under_rel T R (F i) (?G i)] terms, - can be manipulated with rewrite/setoid_rewrite with lemmas on [R]. - Note that this requires that [R] is a [Prop] relation, otherwise - a [bool] relation may need to be "lifted": see the [TestPreOrder] - section in test-suite/ssr/under.v *) - -Instance Under_subrelation {A} (R : relation A) : subrelation R (Under_rel _ R) | 12. -Proof. now rewrite Under_relE. Qed. - -(* see also Morphisms.trans_co_eq_inv_impl_morphism *) - -Instance Under_Reflexive {A} (R : relation A) : - RelationClasses.Reflexive R -> - RelationClasses.Reflexive (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Reflexive Under_Reflexive] : typeclass_instances. - -(* These instances are a bit off-topic given that (Under_rel A R) will - typically be reflexive, to be able to trigger the [over] terminator - -Instance under_Irreflexive {A} (R : relation A) : - RelationClasses.Irreflexive R -> - RelationClasses.Irreflexive (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Irreflexive Under_Irreflexive] : typeclass_instances. - -Instance under_Asymmetric {A} (R : relation A) : - RelationClasses.Asymmetric R -> - RelationClasses.Asymmetric (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Asymmetric Under_Asymmetric] : typeclass_instances. - -Instance under_StrictOrder {A} (R : relation A) : - RelationClasses.StrictOrder R -> - RelationClasses.StrictOrder (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Strictorder Under_Strictorder] : typeclass_instances. - *) - -Instance Under_Symmetric {A} (R : relation A) : - RelationClasses.Symmetric R -> - RelationClasses.Symmetric (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Symmetric Under_Symmetric] : typeclass_instances. - -Instance Under_Transitive {A} (R : relation A) : - RelationClasses.Transitive R -> - RelationClasses.Transitive (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Transitive Under_Transitive] : typeclass_instances. - -Instance Under_PreOrder {A} (R : relation A) : - RelationClasses.PreOrder R -> - RelationClasses.PreOrder (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_PreOrder Under_PreOrder] : typeclass_instances. - -Instance Under_PER {A} (R : relation A) : - RelationClasses.PER R -> - RelationClasses.PER (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_PER Under_PER] : typeclass_instances. - -Instance Under_Equivalence {A} (R : relation A) : - RelationClasses.Equivalence R -> - RelationClasses.Equivalence (Under_rel.Under_rel A R) | 12. -Proof. now rewrite Under_rel.Under_relE. Qed. - -Hint Cut [_* Under_Equivalence Under_Equivalence] : typeclass_instances. - -(* Don't handle Antisymmetric and PartialOrder classes for now, - as these classes depend on two relation symbols... *) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 70c1077106..f6fbdaa958 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -164,7 +164,7 @@ let rawnum_of_r c = match DAst.get c with let s, i = if is_pos_or_zero i then SPlus, i else SMinus, neg i in let i = Bigint.to_string i in let se = if is_gr md glob_Rdiv then "-" else "" in - let e = se ^ Bigint.to_string e in + let e = "e" ^ se ^ Bigint.to_string e in s, { NumTok.int = i; frac = ""; exp = e } | _ -> raise Non_closed_number end |