From bfb28c7720d9101e2caedff0c1f1f2cdbf0bad65 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 24 Jun 2019 17:08:11 +0200 Subject: Support extraction of Coq's string type to OCaml's string type Instead of the default extraction to OCaml's "char list" type. --- plugins/extraction/ExtrOcamlStringPlus.v | 105 +++++++++++++++++++++++++++++++ plugins/extraction/common.ml | 61 ++++++++++++++++++ plugins/extraction/common.mli | 8 +++ plugins/extraction/ocaml.ml | 1 + 4 files changed, 175 insertions(+) create mode 100644 plugins/extraction/ExtrOcamlStringPlus.v (limited to 'plugins/extraction') diff --git a/plugins/extraction/ExtrOcamlStringPlus.v b/plugins/extraction/ExtrOcamlStringPlus.v new file mode 100644 index 0000000000..fff89a4525 --- /dev/null +++ b/plugins/extraction/ExtrOcamlStringPlus.v @@ -0,0 +1,105 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* 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 => "(=)". + +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)". + +(* 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 Ascii 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 => String.of_seq (List.to_seq l))". +Extract Inlined Constant String.list_ascii_of_string => + "(fun s => List.of_seq (String.to_seq s))". +Extract Inlined Constant String.string_of_list_byte => + "(fun l => String.of_seq (List.to_seq l))". +Extract Inlined Constant String.list_byte_of_string => + "(fun s => List.of_seq (String.to_seq s))". + +(* Other operations in module String: + 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/common.ml b/plugins/extraction/common.ml index 2f3f42c5f6..099a22408a 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -649,3 +649,64 @@ 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 ind_string = mk_ind "Coq.Strings.String" "string" + +let check_extract_string () = + try + let string_type = match lang () with + | Ocaml -> "string" + | _ -> raise Not_found + in + String.equal (find_custom (IndRef (ind_string, 0))) 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 = function + (* "EmptyString" constructor *) + | MLcons(_, ConstructRef(_, 1), []) -> true + (* "String" constructor *) + | MLcons(_, ConstructRef(_, 2), [hd; tl]) -> + is_native_char hd && is_native_string_rec tl + (* others *) + | _ -> false + +(* Here we first check that the argument is of type Coq.Strings.String.string + 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(_, ConstructRef((kn,0), j), l) -> + MutInd.equal kn ind_string + && check_extract_string () + && is_native_string_rec c + | _ -> false + +(* Extract the underlying string. *) + +let rec get_native_string c = + let buf = Buffer.create 64 in + let rec get = function + (* "EmptyString" constructor *) + | MLcons(_, ConstructRef(_, 1), []) -> + Buffer.contents buf + (* "String" constructor *) + | MLcons(_, ConstructRef(_, 2), [hd; tl]) -> + 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) ^ "\"") diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index e4e9c4c527..d13ac7926a 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -81,3 +81,11 @@ 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 diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 66429833b9..ab37bd2d76 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -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) -- cgit v1.2.3 From ef7a95e2ca705f0fd72f15e7352eb77bf9c6eaed Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 11 Jul 2019 09:26:10 +0200 Subject: Support extraction of Coq's string type to OCaml's string type, continued Address issues found in CI testing and in code review. --- plugins/extraction/ExtrOcamlStringPlus.v | 4 +--- plugins/extraction/common.ml | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/ExtrOcamlStringPlus.v b/plugins/extraction/ExtrOcamlStringPlus.v index fff89a4525..45d3ef3d3c 100644 --- a/plugins/extraction/ExtrOcamlStringPlus.v +++ b/plugins/extraction/ExtrOcamlStringPlus.v @@ -38,8 +38,6 @@ Extract Constant shift => Extract Inlined Constant ascii_dec => "(=)". Extract Inlined Constant Ascii.eqb => "(=)". -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'"]. @@ -63,7 +61,7 @@ Extract Inductive string => "string" (fun (c, s) -> String.make 1 c ^ s) " ] -"(* If this appears, you're using Ascii internals. Please don't *) +"(* 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))) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 099a22408a..4ab1ac2fba 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -692,7 +692,7 @@ let is_native_string c = (* Extract the underlying string. *) -let rec get_native_string c = +let get_native_string c = let buf = Buffer.create 64 in let rec get = function (* "EmptyString" constructor *) -- cgit v1.2.3 From 8d1bd82130a39e579986a7ad6821353149fdc38f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 3 Dec 2019 14:27:36 +0100 Subject: Avoid warning 40 --- plugins/extraction/common.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 4ab1ac2fba..219afcf408 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -662,7 +662,7 @@ let check_extract_string () = | Ocaml -> "string" | _ -> raise Not_found in - String.equal (find_custom (IndRef (ind_string, 0))) string_type + String.equal (find_custom (GlobRef.IndRef (ind_string, 0))) string_type with Not_found -> false (* The argument is known to be of type Coq.Strings.String.string. @@ -671,9 +671,9 @@ let check_extract_string () = let rec is_native_string_rec = function (* "EmptyString" constructor *) - | MLcons(_, ConstructRef(_, 1), []) -> true + | MLcons(_, GlobRef.ConstructRef(_, 1), []) -> true (* "String" constructor *) - | MLcons(_, ConstructRef(_, 2), [hd; tl]) -> + | MLcons(_, GlobRef.ConstructRef(_, 2), [hd; tl]) -> is_native_char hd && is_native_string_rec tl (* others *) | _ -> false @@ -684,7 +684,7 @@ let rec is_native_string_rec = function let is_native_string c = match c with - | MLcons(_, ConstructRef((kn,0), j), l) -> + | MLcons(_, GlobRef.ConstructRef((kn,0), j), l) -> MutInd.equal kn ind_string && check_extract_string () && is_native_string_rec c @@ -696,10 +696,10 @@ let get_native_string c = let buf = Buffer.create 64 in let rec get = function (* "EmptyString" constructor *) - | MLcons(_, ConstructRef(_, 1), []) -> + | MLcons(_, GlobRef.ConstructRef(_, 1), []) -> Buffer.contents buf (* "String" constructor *) - | MLcons(_, ConstructRef(_, 2), [hd; tl]) -> + | MLcons(_, GlobRef.ConstructRef(_, 2), [hd; tl]) -> Buffer.add_char buf (get_native_char hd); get tl (* others *) -- cgit v1.2.3 From 9705ff0d0673b9c2df8fa08c8aab01d2c40bc8f6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 4 Dec 2019 13:52:39 +0100 Subject: Avoid hardcoded paths in extraction --- plugins/extraction/common.ml | 63 ++++++++++++++++++++++++++++++------------- plugins/extraction/common.mli | 7 +++-- plugins/extraction/haskell.ml | 4 +-- plugins/extraction/ocaml.ml | 4 +-- 4 files changed, 51 insertions(+), 27 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 219afcf408..e2cde8e0d3 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 = @@ -654,7 +661,18 @@ let pp_native_char c = str ("'"^Char.escaped (get_native_char c)^"'") [Extract Inductive string => string] has been declared, then the constants are directly turned into string literals *) -let ind_string = mk_ind "Coq.Strings.String" "string" +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 @@ -662,32 +680,35 @@ let check_extract_string () = | Ocaml -> "string" | _ -> raise Not_found in - String.equal (find_custom (GlobRef.IndRef (ind_string, 0))) string_type + 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 = function +let rec is_native_string_rec empty_string_ref string_constructor_ref = function (* "EmptyString" constructor *) - | MLcons(_, GlobRef.ConstructRef(_, 1), []) -> true + | MLcons(_, gr, []) -> GlobRef.equal gr empty_string_ref (* "String" constructor *) - | MLcons(_, GlobRef.ConstructRef(_, 2), [hd; tl]) -> - is_native_char hd && is_native_string_rec tl + | 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 of type Coq.Strings.String.string +(* Here we first check that the argument is has a 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((kn,0), j), l) -> - MutInd.equal kn ind_string + | MLcons(_, GlobRef.ConstructRef(ind, j), l) -> + is_string_registered () + && GlobRef.equal (GlobRef.IndRef ind) (string_type_ref ()) && check_extract_string () - && is_native_string_rec c + && is_native_string_rec (empty_string_ref ()) (string_constructor_ref ()) c | _ -> false (* Extract the underlying string. *) @@ -696,10 +717,10 @@ let get_native_string c = let buf = Buffer.create 64 in let rec get = function (* "EmptyString" constructor *) - | MLcons(_, GlobRef.ConstructRef(_, 1), []) -> + | MLcons(_, gr, []) when GlobRef.equal gr (empty_string_ref ()) -> Buffer.contents buf (* "String" constructor *) - | MLcons(_, GlobRef.ConstructRef(_, 2), [hd; tl]) -> + | MLcons(_, gr, [hd; tl]) when GlobRef.equal gr (string_constructor_ref ()) -> Buffer.add_char buf (get_native_char hd); get tl (* others *) @@ -710,3 +731,7 @@ let get_native_string c = 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 d13ac7926a..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 *) @@ -89,3 +85,6 @@ val pp_native_char : ml_ast -> Pp.t 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/haskell.ml b/plugins/extraction/haskell.ml index f0053ba6b5..bde37bcae7 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 diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index ab37bd2d76..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 -- cgit v1.2.3 From 887128c20edcc7d9a0e6d7387291fe0ba05a29e5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 8 Dec 2019 19:01:04 +0100 Subject: Rename ExtrOcamlStringPlus into ExtrOcamlNativeString As suggested during review. That's a much better name. --- plugins/extraction/ExtrOcamlNativeString.v | 103 +++++++++++++++++++++++++++++ plugins/extraction/ExtrOcamlStringPlus.v | 103 ----------------------------- 2 files changed, 103 insertions(+), 103 deletions(-) create mode 100644 plugins/extraction/ExtrOcamlNativeString.v delete mode 100644 plugins/extraction/ExtrOcamlStringPlus.v (limited to 'plugins/extraction') diff --git a/plugins/extraction/ExtrOcamlNativeString.v b/plugins/extraction/ExtrOcamlNativeString.v new file mode 100644 index 0000000000..45d3ef3d3c --- /dev/null +++ b/plugins/extraction/ExtrOcamlNativeString.v @@ -0,0 +1,103 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* 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)". + +(* 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 => String.of_seq (List.to_seq l))". +Extract Inlined Constant String.list_ascii_of_string => + "(fun s => List.of_seq (String.to_seq s))". +Extract Inlined Constant String.string_of_list_byte => + "(fun l => String.of_seq (List.to_seq l))". +Extract Inlined Constant String.list_byte_of_string => + "(fun s => List.of_seq (String.to_seq s))". + +(* Other operations in module String: + 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/ExtrOcamlStringPlus.v b/plugins/extraction/ExtrOcamlStringPlus.v deleted file mode 100644 index 45d3ef3d3c..0000000000 --- a/plugins/extraction/ExtrOcamlStringPlus.v +++ /dev/null @@ -1,103 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* 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)". - -(* 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 => String.of_seq (List.to_seq l))". -Extract Inlined Constant String.list_ascii_of_string => - "(fun s => List.of_seq (String.to_seq s))". -Extract Inlined Constant String.string_of_list_byte => - "(fun l => String.of_seq (List.to_seq l))". -Extract Inlined Constant String.list_byte_of_string => - "(fun s => List.of_seq (String.to_seq s))". - -(* Other operations in module String: - 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. -*) -- cgit v1.2.3 From a3070010c19ec8f46b247875e3c771e2de71dcdf Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 8 Dec 2019 19:02:51 +0100 Subject: Typo in comment --- plugins/extraction/common.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index e2cde8e0d3..742dca612a 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -698,9 +698,10 @@ let rec is_native_string_rec empty_string_ref string_constructor_ref = function (* others *) | _ -> false -(* Here we first check that the argument is has a type registered as core.string.type - and that extraction to native strings was requested. - Then we check every character via [is_native_string_rec]. *) +(* 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 -- cgit v1.2.3 From e78717780b729f9a69d908afd9da156fffddfe52 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 8 Dec 2019 19:20:21 +0100 Subject: Reimplement string <-> char list conversions Using only OCaml stdlib functions available in OCaml 4.05. --- plugins/extraction/ExtrOcamlNativeString.v | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/ExtrOcamlNativeString.v b/plugins/extraction/ExtrOcamlNativeString.v index 45d3ef3d3c..77a16c9524 100644 --- a/plugins/extraction/ExtrOcamlNativeString.v +++ b/plugins/extraction/ExtrOcamlNativeString.v @@ -76,15 +76,21 @@ Extract Inlined Constant String.prefix => 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 => String.of_seq (List.to_seq l))". + "(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 => List.of_seq (String.to_seq s))". + "(fun s -> + Array.to_list (Array.init (String.length s) (fun i -> s.[i])))". Extract Inlined Constant String.string_of_list_byte => - "(fun l => String.of_seq (List.to_seq l))". + "(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 => List.of_seq (String.to_seq s))". + "(fun s -> + Array.to_list (Array.init (String.length s) (fun i -> s.[i])))". -(* Other operations in module String: +(* Other operations in module String (at the time of this writing): String.length String.get String.substring -- cgit v1.2.3 From 3987b5cab0b889ca71b52843abf7563b9b95e946 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 8 Jan 2020 11:21:20 +0100 Subject: Better extraction of string literals in Haskell --- plugins/extraction/common.ml | 1 + plugins/extraction/haskell.ml | 1 + 2 files changed, 2 insertions(+) (limited to 'plugins/extraction') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 742dca612a..29da12de40 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -678,6 +678,7 @@ 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 diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index bde37bcae7..eef050efbd 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -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) -- cgit v1.2.3 From ef938a4ce2c03b1c4f23222a4542ad144a1f209b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 8 Jan 2020 13:52:25 +0100 Subject: Factorize ascii extraction in ExtrOcamlChar.v --- plugins/extraction/ExtrOcamlChar.v | 45 ++++++++++++++++++++++++++++++ plugins/extraction/ExtrOcamlNativeString.v | 24 +--------------- plugins/extraction/ExtrOcamlString.v | 39 +------------------------- 3 files changed, 47 insertions(+), 61 deletions(-) create mode 100644 plugins/extraction/ExtrOcamlChar.v (limited to 'plugins/extraction') 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 *) +(* 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 index 77a16c9524..ec3da1e444 100644 --- a/plugins/extraction/ExtrOcamlNativeString.v +++ b/plugins/extraction/ExtrOcamlNativeString.v @@ -14,29 +14,7 @@ Require Coq.extraction.Extraction. Require Import Ascii String Coq.Strings.Byte. - -(* This is as in ExtrOcamlString.v *) - -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. (* 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 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. -*) -- cgit v1.2.3