diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/ExtrHaskellString.v | 20 | ||||
| -rw-r--r-- | plugins/extraction/ExtrOcamlString.v | 16 | ||||
| -rw-r--r-- | plugins/extraction/big.ml | 24 | ||||
| -rw-r--r-- | plugins/extraction/common.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 74 |
5 files changed, 84 insertions, 52 deletions
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v index a4a40d3c5a..8c61f4e96b 100644 --- a/plugins/extraction/ExtrHaskellString.v +++ b/plugins/extraction/ExtrHaskellString.v @@ -6,6 +6,7 @@ Require Coq.extraction.Extraction. Require Import Ascii. Require Import String. +Require Import Coq.Strings.Byte. (** * At the moment, Coq's extraction has no way to add extra import @@ -40,3 +41,22 @@ Extract Inlined Constant Ascii.eqb => "(Prelude.==)". Extract Inductive string => "Prelude.String" [ "([])" "(:)" ]. Extract Inlined Constant String.string_dec => "(Prelude.==)". Extract Inlined Constant String.eqb => "(Prelude.==)". + +(* 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 => "Prelude.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 => "(Prelude.==)". +Extract Inlined Constant Byte.byte_eq_dec => "(Prelude.==)". +Extract Inlined Constant Ascii.ascii_of_byte => "(\x -> x)". +Extract Inlined Constant Ascii.byte_of_ascii => "(\x -> x)". + +(* +Require Import ExtrHaskellBasic. +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). + +Extraction Language Haskell. +Recursive Extraction test Ascii.zero Ascii.one test2 test3 byte_rect. +*) diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index a2a6a8fe67..f094d4860e 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -12,7 +12,7 @@ Require Coq.extraction.Extraction. -Require Import Ascii String. +Require Import Ascii String Coq.Strings.Byte. Extract Inductive ascii => char [ @@ -37,7 +37,19 @@ 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)". + (* Definition test := "ceci est un test"%string. -Recursive Extraction test Ascii.zero Ascii.one. +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/big.ml b/plugins/extraction/big.ml index 9c0f373c6a..c675eacc92 100644 --- a/plugins/extraction/big.ml +++ b/plugins/extraction/big.ml @@ -20,8 +20,10 @@ type big_int = Big_int.big_int let zero = zero_big_int (** The big integer [0]. *) + let one = unit_big_int (** The big integer [1]. *) + let two = big_int_of_int 2 (** The big integer [2]. *) @@ -29,28 +31,39 @@ let two = big_int_of_int 2 let opp = minus_big_int (** Unary negation. *) + let abs = abs_big_int (** Absolute value. *) + let add = add_big_int (** Addition. *) + let succ = succ_big_int (** Successor (add 1). *) + let add_int = add_int_big_int (** Addition of a small integer to a big integer. *) + let sub = sub_big_int (** Subtraction. *) + let pred = pred_big_int (** Predecessor (subtract 1). *) + let mult = mult_big_int (** Multiplication of two big integers. *) + let mult_int = mult_int_big_int (** Multiplication of a big integer by a small integer *) + let square = square_big_int (** Return the square of the given big integer *) + let sqrt = sqrt_big_int (** [sqrt_big_int a] returns the integer square root of [a], that is, the largest big integer [r] such that [r * r <= a]. Raise [Invalid_argument] if [a] is negative. *) + let quomod = quomod_big_int (** Euclidean division of two big integers. The first part of the result is the quotient, @@ -58,14 +71,18 @@ let quomod = quomod_big_int Writing [(q,r) = quomod_big_int a b], we have [a = q * b + r] and [0 <= r < |b|]. Raise [Division_by_zero] if the divisor is zero. *) + let div = div_big_int (** Euclidean quotient of two big integers. This is the first result [q] of [quomod_big_int] (see above). *) + let modulo = mod_big_int (** Euclidean modulus of two big integers. This is the second result [r] of [quomod_big_int] (see above). *) + let gcd = gcd_big_int (** Greatest common divisor of two big integers. *) + let power = power_big_int_positive_big_int (** Exponentiation functions. Return the big integer representing the first argument [a] raised to the power [b] @@ -78,18 +95,22 @@ let power = power_big_int_positive_big_int let sign = sign_big_int (** Return [0] if the given big integer is zero, [1] if it is positive, and [-1] if it is negative. *) + let compare = compare_big_int (** [compare_big_int a b] returns [0] if [a] and [b] are equal, [1] if [a] is greater than [b], and [-1] if [a] is smaller than [b]. *) + let eq = eq_big_int let le = le_big_int let ge = ge_big_int let lt = lt_big_int let gt = gt_big_int (** Usual boolean comparisons between two big integers. *) + let max = max_big_int (** Return the greater of its two arguments. *) + let min = min_big_int (** Return the smaller of its two arguments. *) @@ -98,6 +119,7 @@ let min = min_big_int let to_string = string_of_big_int (** Return the string representation of the given big integer, in decimal (base 10). *) + let of_string = big_int_of_string (** Convert a string to a big integer, in decimal. The string consists of an optional [-] or [+] sign, @@ -107,6 +129,7 @@ let of_string = big_int_of_string let of_int = big_int_of_int (** Convert a small integer to a big integer. *) + let is_int = is_int_big_int (** Test whether the given big integer is small enough to be representable as a small integer (type [int]) @@ -115,6 +138,7 @@ let is_int = is_int_big_int [a] is between 2{^30} and 2{^30}-1. On a 64-bit platform, [is_int_big_int a] returns [true] if and only if [a] is between -2{^62} and 2{^62}-1. *) + let to_int = int_of_big_int (** Convert a big integer to a small integer (type [int]). Raises [Failure "int_of_big_int"] if the big integer diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index bdeb6fca60..59c57cc544 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -125,7 +125,7 @@ module KOrd = struct type t = kind * string let compare (k1, s1) (k2, s2) = - let c = Pervasives.compare k1 k2 (** OK *) in + let c = Pervasives.compare k1 k2 (* OK *) in if c = 0 then String.compare s1 s2 else c end diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 16890ea260..2058837b8e 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -621,10 +621,9 @@ let lang_ref = Summary.ref Ocaml ~name:"ExtrLang" let lang () = !lang_ref let extr_lang : lang -> obj = - declare_object - {(default_object "Extraction Lang") with - cache_function = (fun (_,l) -> lang_ref := l); - load_function = (fun _ (_,l) -> lang_ref := l)} + declare_object @@ superglobal_object_nodischarge "Extraction Lang" + ~cache:(fun (_,l) -> lang_ref := l) + ~subst:None let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) @@ -648,15 +647,10 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) let inline_extraction : bool * GlobRef.t list -> obj = - declare_object - {(default_object "Extraction Inline") with - cache_function = (fun (_,(b,l)) -> add_inline_entries b l); - load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); - classify_function = (fun o -> Substitute o); - discharge_function = (fun (_,x) -> Some x); - subst_function = - (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) - } + declare_object @@ superglobal_object "Extraction Inline" + ~cache:(fun (_,(b,l)) -> add_inline_entries b l) + ~subst:(Some (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))) + ~discharge:(fun (_,x) -> Some x) (* Grammar entries. *) @@ -685,10 +679,9 @@ let print_extraction_inline () = (* Reset part *) let reset_inline : unit -> obj = - declare_object - {(default_object "Reset Extraction Inline") with - cache_function = (fun (_,_)-> inline_table := empty_inline_table); - load_function = (fun _ (_,_)-> inline_table := empty_inline_table)} + declare_object @@ superglobal_object_nodischarge "Reset Extraction Inline" + ~cache:(fun (_,_)-> inline_table := empty_inline_table) + ~subst:None let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) @@ -731,13 +724,9 @@ let add_implicits r l = (* Registration of operations for rollback. *) let implicit_extraction : GlobRef.t * int_or_id list -> obj = - declare_object - {(default_object "Extraction Implicit") with - cache_function = (fun (_,(r,l)) -> add_implicits r l); - load_function = (fun _ (_,(r,l)) -> add_implicits r l); - classify_function = (fun o -> Substitute o); - subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l)) - } + declare_object @@ superglobal_object_nodischarge "Extraction Implicit" + ~cache:(fun (_,(r,l)) -> add_implicits r l) + ~subst:(Some (fun (s,(r,l)) -> (fst (subst_global s r), l))) (* Grammar entries. *) @@ -784,12 +773,9 @@ let add_blacklist_entries l = (* Registration of operations for rollback. *) let blacklist_extraction : string list -> obj = - declare_object - {(default_object "Extraction Blacklist") with - cache_function = (fun (_,l) -> add_blacklist_entries l); - load_function = (fun _ (_,l) -> add_blacklist_entries l); - subst_function = (fun (_,x) -> x) - } + declare_object @@ superglobal_object_nodischarge "Extraction Blacklist" + ~cache:(fun (_,l) -> add_blacklist_entries l) + ~subst:None (* Grammar entries. *) @@ -805,10 +791,9 @@ let print_extraction_blacklist () = (* Reset part *) let reset_blacklist : unit -> obj = - declare_object - {(default_object "Reset Extraction Blacklist") with - cache_function = (fun (_,_)-> blacklist_table := Id.Set.empty); - load_function = (fun _ (_,_)-> blacklist_table := Id.Set.empty)} + declare_object @@ superglobal_object_nodischarge "Reset Extraction Blacklist" + ~cache:(fun (_,_)-> blacklist_table := Id.Set.empty) + ~subst:None let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ()) @@ -852,23 +837,14 @@ let find_custom_match pv = (* Registration of operations for rollback. *) let in_customs : GlobRef.t * string list * string -> obj = - declare_object - {(default_object "ML extractions") with - cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); - load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s); - classify_function = (fun o -> Substitute o); - subst_function = - (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) - } + declare_object @@ superglobal_object_nodischarge "ML extractions" + ~cache:(fun (_,(r,ids,s)) -> add_custom r ids s) + ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))) let in_custom_matchs : GlobRef.t * string -> obj = - declare_object - {(default_object "ML extractions custom matchs") with - cache_function = (fun (_,(r,s)) -> add_custom_match r s); - load_function = (fun _ (_,(r,s)) -> add_custom_match r s); - classify_function = (fun o -> Substitute o); - subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s)) - } + declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs" + ~cache:(fun (_,(r,s)) -> add_custom_match r s) + ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s))) (* Grammar entries. *) |