diff options
Diffstat (limited to 'plugins')
44 files changed, 488 insertions, 519 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 480819ebe1..6f9384941b 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -27,12 +27,12 @@ let start_deriving f suchthat lemma = let sigma = Evd.from_env env in let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in - (** create a sort variable for the type of [f] *) + (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one that looked the most general. *) let (sigma,f_type_sort) = Evd.new_sort_variable Evd.univ_flexible_alg sigma in let f_type_type = EConstr.mkSort f_type_sort in - (** create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) + (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) let goals = let open Proofview in TCons ( env , sigma , f_type_type , (fun sigma f_type -> @@ -45,14 +45,14 @@ let start_deriving f suchthat lemma = TNil sigma)))))) in - (** The terminator handles the registering of constants when the proof is closed. *) + (* The terminator handles the registering of constants when the proof is closed. *) let terminator com = let open Proof_global in - (** Extracts the relevant information from the proof. [Admitted] - and [Save] result in user errors. [opaque] is [true] if the - proof was concluded by [Qed], and [false] if [Defined]. [f_def] - and [lemma_def] correspond to the proof of [f] and of - [suchthat], respectively. *) + (* Extracts the relevant information from the proof. [Admitted] + and [Save] result in user errors. [opaque] is [true] if the + proof was concluded by [Qed], and [false] if [Defined]. [f_def] + and [lemma_def] correspond to the proof of [f] and of + [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") @@ -64,26 +64,26 @@ let start_deriving f suchthat lemma = opaque <> Proof_global.Transparent , f_def , lemma_def | _ -> assert false in - (** The opacity of [f_def] is adjusted to be [false], as it - must. Then [f] is declared in the global environment. *) + (* The opacity of [f_def] is adjusted to be [false], as it + must. Then [f] is declared in the global environment. *) let f_def = { f_def with Entries.const_entry_opaque = false } in let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in let f_kn = Declare.declare_constant f f_def in let f_kn_term = mkConst f_kn in - (** In the type and body of the proof of [suchthat] there can be - references to the variable [f]. It needs to be replaced by - references to the constant [f] declared above. This substitution - performs this precise action. *) + (* In the type and body of the proof of [suchthat] there can be + references to the variable [f]. It needs to be replaced by + references to the constant [f] declared above. This substitution + performs this precise action. *) let substf c = Vars.replace_vars [f,f_kn_term] c in - (** Extracts the type of the proof of [suchthat]. *) + (* Extracts the type of the proof of [suchthat]. *) let lemma_pretype = match Entries.(lemma_def.const_entry_type) with | Some t -> t | None -> assert false (* Proof_global always sets type here. *) in - (** The references of [f] are subsituted appropriately. *) + (* The references of [f] are subsituted appropriately. *) let lemma_type = substf lemma_pretype in - (** The same is done in the body of the proof. *) + (* The same is done in the body of the proof. *) let lemma_body = map_const_entry_body substf Entries.(lemma_def.const_entry_body) in @@ -105,7 +105,3 @@ let start_deriving f suchthat lemma = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p end in () - - - - 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. *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 4cdfc6fac5..12b68e208c 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -41,7 +41,7 @@ let pop t = Vars.lift (-1) t *) let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let princ_type = EConstr.of_constr princ_type in - let princ_type_info = compute_elim_sig Evd.empty princ_type (** FIXME *) in + let princ_type_info = compute_elim_sig Evd.empty princ_type (* FIXME *) in let env = Global.env () in let env_with_params = EConstr.push_rel_context princ_type_info.params env in let tbl = Hashtbl.create 792 in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 19f954c10d..f9938c0356 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -237,7 +237,6 @@ let cache_Function (_,finfos) = from_graph := Indmap.add finfos.graph_ind finfos !from_graph -let load_Function _ = cache_Function let subst_Function (subst,finfos) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst_ind i = Mod_subst.subst_ind subst i @@ -271,9 +270,6 @@ let subst_Function (subst,finfos) = is_general = finfos.is_general } -let classify_Function infos = Libobject.Substitute infos - - let discharge_Function (_,finfos) = Some finfos let pr_ocst c = @@ -302,15 +298,11 @@ let pr_table tb = Pp.prlist_with_sep fnl pr_info l let in_Function : function_info -> Libobject.obj = - Libobject.declare_object - {(Libobject.default_object "FUNCTIONS_DB") with - Libobject.cache_function = cache_Function; - Libobject.load_function = load_Function; - Libobject.classify_function = classify_Function; - Libobject.subst_function = subst_Function; - Libobject.discharge_function = discharge_Function -(* Libobject.open_function = open_Function; *) - } + let open Libobject in + declare_object @@ superglobal_object "FUNCTIONS_DB" + ~cache:cache_Function + ~subst:(Some subst_Function) + ~discharge:discharge_Function let find_or_none id = @@ -500,7 +492,7 @@ type tcc_lemma_value = (* We only "purify" on exceptions. XXX: What is this doing here? *) let funind_purify f x = - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in try f x with e -> let e = CErrors.push e in diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 603dd60cf2..47f593ff3e 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -306,8 +306,8 @@ let add_rewrite_hint ~poly bases ort t lcsr = let ctx = let ctx = UState.context_set ctx in if poly then ctx - else (** This is a global universe context that shouldn't be - refreshed at every use of the hint, declare it globally. *) + else (* This is a global universe context that shouldn't be + refreshed at every use of the hint, declare it globally. *) (Declare.declare_universe_context false ctx; Univ.ContextSet.empty) in @@ -531,11 +531,9 @@ let cache_transitivity_lemma (_,(left,lem)) = let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) let inTransitivity : bool * Constr.t -> obj = - declare_object {(default_object "TRANSITIVITY-STEPS") with - cache_function = cache_transitivity_lemma; - open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); - subst_function = subst_transitivity_lemma; - classify_function = (fun o -> Substitute o) } + declare_object @@ global_object_nodischarge "TRANSITIVITY-STEPS" + ~cache:cache_transitivity_lemma + ~subst:(Some subst_transitivity_lemma) (* Main entry points *) @@ -738,7 +736,8 @@ let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - (** FIXME: this looks really wrong. Does anybody really use this tactic? *) + (* FIXME: this looks really wrong. Does anybody really use + this tactic? *) let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in change_concl c end; diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index ef18dd6cdc..1ea6ff84d4 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -24,7 +24,7 @@ let (set_default_tactic, get_default_tactic, print_default_tactic) = Tactic_option.declare_tactic_option "Program tactic" let () = - (** Delay to recover the tactic imperatively *) + (* Delay to recover the tactic imperatively *) let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> snd (get_default_tactic ()) end in diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 8bf1855fe0..5e3f4df192 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -229,8 +229,8 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_tacarg_using_rule pr_gen l = let l = match l with | TacTerm s :: l -> - (** First terminal token should be considered as the name of the tactic, - so we tag it differently than the other terminal tokens. *) + (* First terminal token should be considered as the name of the tactic, + so we tag it differently than the other terminal tokens. *) primitive s :: tacarg_using_rule_token pr_gen l | _ -> tacarg_using_rule_token pr_gen l in @@ -1174,7 +1174,7 @@ let pr_goal_selector ~toplevel s = pr_constant = pr_evaluable_reference_env env; pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; - (** Those are not used by the atomic printer *) + (* Those are not used by the atomic printer *) pr_generic = (fun _ -> assert false); pr_extend = (fun _ _ _ -> assert false); pr_alias = (fun _ _ _ -> assert false); diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 06783de614..4bb52f599a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -97,7 +97,7 @@ let goalevars evars = fst evars let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = - (** We handle the typeclass resolution of constraints ourselves *) + (* We handle the typeclass resolution of constraints ourselves *) let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false t in let ev, _ = destEvar evd' t in (evd', Evar.Set.add ev cstrs), t @@ -474,7 +474,7 @@ let get_symmetric_proof b = let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.") let rec decompose_app_rel env evd t = - (** Head normalize for compatibility with the old meta mechanism *) + (* Head normalize for compatibility with the old meta mechanism *) let t = Reductionops.whd_betaiota evd t in match EConstr.kind evd t with | App (f, [||]) -> assert false @@ -613,7 +613,7 @@ let solve_remaining_by env sigma holes by = Some evk | _ -> None in - (** Only solve independent holes *) + (* Only solve independent holes *) let indep = List.map_filter map holes in let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in let solve_tac = match tac with @@ -628,11 +628,12 @@ let solve_remaining_by env sigma holes by = in match evi with | None -> sigma - (** Evar should not be defined, but just in case *) + (* Evar should not be defined, but just in case *) | Some evi -> let env = Environ.reset_with_named_context evi.evar_hyps env in let ty = evi.evar_concl in - let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in + let name, poly = Id.of_string "rewrite", false in + let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in Evd.define evk (EConstr.of_constr c) sigma in List.fold_left solve sigma indep @@ -646,6 +647,7 @@ let poly_inverse sort = type rewrite_proof = | RewPrf of constr * constr (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *) + | RewCast of cast_kind (** A proof of convertibility (with casts) *) @@ -1561,7 +1563,7 @@ let newfail n s = let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in - (** For compatibility *) + (* For compatibility *) let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in let treat sigma res = @@ -1611,7 +1613,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let env = match clause with | None -> env | Some id -> - (** Only consider variables not depending on [id] *) + (* Only consider variables not depending on [id] *) let ctx = named_context env in let filter decl = not (occur_var_in_decl env sigma id decl) in let nctx = List.filter filter ctx in @@ -1623,7 +1625,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = in let sigma = match origsigma with None -> sigma | Some sigma -> sigma in treat sigma res <*> - (** For compatibility *) + (* For compatibility *) beta <*> Proofview.shelve_unifiable with | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) -> diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 2aee809eb6..b770b97384 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -169,7 +169,7 @@ let add_tactic_entry (kn, ml, tg) state = let entry, pos = get_tactic_entry tg.tacgram_level in let mkact loc l = let map arg = - (** HACK to handle especially the tactic(...) entry *) + (* HACK to handle especially the tactic(...) entry *) let wit = Genarg.rawwit Tacarg.wit_tactic in if Genarg.has_type arg wit && not ml then Tacexp (Genarg.out_gen wit arg) @@ -223,7 +223,7 @@ let interp_prod_item = function | Some arg -> arg end | Some n -> - (** FIXME: do better someday *) + (* FIXME: do better someday *) assert (String.equal s "tactic"); begin match Tacarg.wit_tactic with | ExtraArg tag -> ArgT.Any tag @@ -241,9 +241,9 @@ let make_fresh_key = | TacNonTerm _ -> "#" in let prods = String.concat "_" (List.map map prods) in - (** We embed the hash of the kernel name in the label so that the identifier - should be mostly unique. This ensures that including two modules - together won't confuse the corresponding labels. *) + (* We embed the hash of the kernel name in the label so that the identifier + should be mostly unique. This ensures that including two modules + together won't confuse the corresponding labels. *) let hash = (cur lxor (ModPath.hash (Lib.current_mp ()))) land 0x7FFFFFFF in let lbl = Id.of_string_soft (Printf.sprintf "%s_%08X" prods hash) in Lib.make_kn lbl @@ -281,7 +281,7 @@ let open_tactic_notation i (_, tobj) = let load_tactic_notation i (_, tobj) = let key = tobj.tacobj_key in let () = check_key key in - (** Only add the printing and interpretation rules. *) + (* Only add the printing and interpretation rules. *) Tacenv.register_alias key tobj.tacobj_body; Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram); if Int.equal i 1 && not tobj.tacobj_local then @@ -342,7 +342,7 @@ let extend_atomic_tactic name entries = let map_prod prods = let (hd, rem) = match prods with | TacTerm s :: rem -> (s, rem) - | _ -> assert false (** Not handled by the ML extension syntax *) + | _ -> assert false (* Not handled by the ML extension syntax *) in let empty_value = function | TacTerm s -> raise NonEmptyArgument @@ -383,8 +383,8 @@ let add_ml_tactic_notation name ~level ?deprecation prods = add_glob_tactic_notation false ~level ?deprecation prods true ids tac in List.iteri iter (List.rev prods); - (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at - tactic_expr level 0) *) + (* We call [extend_atomic_tactic] only for "basic tactics" (the ones + at tactic_expr level 0) *) if Int.equal level 0 then extend_atomic_tactic name prods (**********************************************************************) @@ -474,8 +474,9 @@ let register_ltac local ?deprecation tacl = (name, body) in let defs () = - (** Register locally the tactic to handle recursivity. This function affects - the whole environment, so that we transactify it afterwards. *) + (* Register locally the tactic to handle recursivity. This + function affects the whole environment, so that we transactify + it afterwards. *) let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in let () = List.iter iter_rec recvars in List.map map rfun @@ -557,7 +558,7 @@ let () = register_grammars_by_name "tactic" entries let get_identifier i = - (** Workaround for badly-designed generic arguments lacking a closure *) + (* Workaround for badly-designed generic arguments lacking a closure *) Names.Id.of_string_soft (Printf.sprintf "$%i" i) type _ ty_sig = @@ -650,20 +651,22 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign = in match sign with | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s -> - (** The extension is only made of a name followed by constr entries: we do not - add any grammar nor printing rule and add it as a true Ltac definition. *) + (* The extension is only made of a name followed by constr + entries: we do not add any grammar nor printing rule and add it + as a true Ltac definition. *) let vars = mk_sign_vars 1 s in let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in let tac = match s with | TyNil -> eval ml_tac - (** Special handling of tactics without arguments: such tactics do not do - a Proofview.Goal.nf_enter to compute their arguments. It matters for some - whole-prof tactics like [shelve_unifiable]. *) + (* Special handling of tactics without arguments: such tactics do + not do a Proofview.Goal.nf_enter to compute their arguments. It + matters for some whole-prof tactics like [shelve_unifiable]. *) | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac) in - (** Arguments are not passed directly to the ML tactic in the TacML node, - the ML tactic retrieves its arguments in the [ist] environment instead. - This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) + (* Arguments are not passed directly to the ML tactic in the TacML + node, the ML tactic retrieves its arguments in the [ist] + environment instead. This is the rôle of the + [lift_constr_tac_to_ml_tac] function. *) let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, [])))in let id = Names.Id.of_string name in let obj () = Tacenv.register_ltac true false id body ?deprecation in diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index b99f956ce0..30e316b36d 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -78,12 +78,12 @@ type ('a,'t) match_rule = (** Extension indentifiers for the TACTIC EXTEND mechanism. *) type ml_tactic_name = { + mltac_plugin : string; (** Name of the plugin where the tactic is defined, typically coming from a DECLARE PLUGIN statement in the source. *) - mltac_plugin : string; + mltac_tactic : string; (** Name of the tactic entry where the tactic is defined, typically found after the TACTIC EXTEND statement in the source. *) - mltac_tactic : string; } type ml_tactic_entry = { diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index bd080bf4f0..8b6b14322b 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -78,12 +78,12 @@ type ('a,'t) match_rule = (** Extension indentifiers for the TACTIC EXTEND mechanism. *) type ml_tactic_name = { + mltac_plugin : string; (** Name of the plugin where the tactic is defined, typically coming from a DECLARE PLUGIN statement in the source. *) - mltac_plugin : string; + mltac_tactic : string; (** Name of the tactic entry where the tactic is defined, typically found after the TACTIC EXTEND statement in the source. *) - mltac_tactic : string; } type ml_tactic_entry = { diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 85c6348b52..a1e21aab04 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -843,8 +843,9 @@ let notation_subst bindings tac = (make ?loc @@ Name id, c) :: accu in let bindings = Id.Map.fold fold bindings [] in - (** This is theoretically not correct due to potential variable capture, but - Ltac has no true variables so one cannot simply substitute *) + (* This is theoretically not correct due to potential variable + capture, but Ltac has no true variables so one cannot simply + substitute *) TacLetIn (false, bindings, tac) let () = Genintern.register_ntn_subst0 wit_tactic notation_subst diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index cf5eb442be..816741b894 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -50,7 +50,7 @@ let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v w let Val.Dyn (t, _) = v in let t' = match val_tag wit with | Val.Base t' -> t' - | _ -> assert false (** not used in this module *) + | _ -> assert false (* not used in this module *) in match Val.eq t t' with | None -> false @@ -68,13 +68,13 @@ let in_list tag v = let in_gen wit v = let t = match val_tag wit with | Val.Base t -> t - | _ -> assert false (** not used in this module *) + | _ -> assert false (* not used in this module *) in Val.Dyn (t, v) let out_gen wit v = let t = match val_tag wit with | Val.Base t -> t - | _ -> assert false (** not used in this module *) + | _ -> assert false (* not used in this module *) in match prj t v with None -> assert false | Some x -> x @@ -585,8 +585,8 @@ let interp_pure_open_constr ist = let interp_typed_pattern ist env sigma (_,c,_) = let sigma, c = interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in - (** FIXME: it is necessary to be unsafe here because of the way we handle - evars in the pretyper. Sometimes they get solved eagerly. *) + (* FIXME: it is necessary to be unsafe here because of the way we handle + evars in the pretyper. Sometimes they get solved eagerly. *) pattern_of_constr env sigma (EConstr.Unsafe.to_constr c) (* Interprets a constr expression *) @@ -897,7 +897,7 @@ let interp_destruction_arg ist gl arg = end) in try - (** FIXME: should be moved to taccoerce *) + (* FIXME: should be moved to taccoerce *) let v = Id.Map.find id ist.lfun in if has_type v (topwit wit_intro_pattern) then let v = out_gen (topwit wit_intro_pattern) v in @@ -1020,7 +1020,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr | TacArg {loc;v} -> interp_tacarg ist v | t -> - (** Delayed evaluation *) + (* Delayed evaluation *) Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t))) in let open Ftactic in @@ -1396,12 +1396,12 @@ and interp_match_successes lz ist s = general | Select -> begin - (** Only keep the first matching result, we don't backtrack on it *) + (* Only keep the first matching result, we don't backtrack on it *) let s = Proofview.tclONCE s in s >>= fun ans -> interp_match_success ist ans end | Once -> - (** Once a tactic has succeeded, do not backtrack anymore *) + (* Once a tactic has succeeded, do not backtrack anymore *) Proofview.tclONCE general (* Interprets the Match expressions *) @@ -1438,7 +1438,7 @@ and interp_match_goal ist lz lr lmr = (* Interprets extended tactic generic arguments *) and interp_genarg ist x : Val.t Ftactic.t = let open Ftactic.Notations in - (** Ad-hoc handling of some types. *) + (* Ad-hoc handling of some types. *) let tag = genarg_tag x in if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then interp_genarg_var_list ist x @@ -2031,7 +2031,8 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun = lfun; extra; } in let tac = interp_tactic ist tac in - let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in + let name, poly = Id.of_string "ltac_sub", false in + let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in GlobEnv.register_constr_interp0 wit_tactic eval diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index c949589e22..54924f1644 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -59,7 +59,7 @@ let id_map_try_add_name id x m = the binding of the right-hand argument shadows that of the left-hand argument. *) let id_map_right_biased_union m1 m2 = - if Id.Map.is_empty m1 then m2 (** Don't reconstruct the whole map *) + if Id.Map.is_empty m1 then m2 (* Don't reconstruct the whole map *) else Id.Map.fold Id.Map.add m2 m1 (** Tests whether the substitution [s] is empty. *) @@ -102,7 +102,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) = else raise Not_coherent_metas in let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 in - (** ppedrot: Is that even correct? *) + (* ppedrot: Is that even correct? *) let merged = ln +++ ln1 in (merged, Id.Map.merge merge lcm lm) @@ -263,8 +263,8 @@ module PatternMatching (E:StaticEnvironment) = struct | All lhs -> wildcard_match_term lhs | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs | Pat _ -> - (** Rules with hypotheses, only work in match goal. *) - fail + (* Rules with hypotheses, only work in match goal. *) + fail (** [match_term term rules] matches the term [term] with the set of matching rules [rules].*) diff --git a/plugins/micromega/itv.ml b/plugins/micromega/itv.ml index dc1df7ec9f..44cad820ed 100644 --- a/plugins/micromega/itv.ml +++ b/plugins/micromega/itv.ml @@ -11,10 +11,11 @@ (** Intervals (extracted from mfourier.ml) *) open Num + (** The type of intervals is *) type interval = num option * num option - (** None models the absence of bound i.e. infinity *) - (** As a result, + (** None models the absence of bound i.e. infinity + As a result, - None , None -> \]-oo,+oo\[ - None , Some v -> \]-oo,v\] - Some v, None -> \[v,+oo\[ diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index f5e9a9f34c..23f3470d77 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -103,7 +103,7 @@ module Poly : sig end -type cstr = {coeffs : Vect.t ; op : op ; cst : Num.num} (** Representation of linear constraints *) +type cstr = {coeffs : Vect.t ; op : op ; cst : Num.num} (* Representation of linear constraints *) and op = Eq | Ge | Gt val eval_op : op -> Num.num -> Num.num -> bool diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index 8d8c6ea90b..4465aa1ee1 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -20,6 +20,7 @@ type iset = unit IMap.t type tableau = Vect.t IMap.t (** Mapping basic variables to their equation. All variables >= than a threshold rst are restricted.*) + module Restricted = struct type t = diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index f8fc943713..1825a4d77c 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -609,7 +609,7 @@ type current_problem = { exception NotInIdealUpdate of current_problem let test_dans_ideal cur_pb table metadata p lp len0 = - (** Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) + (* Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) let (c,r) = reduce2 table cur_pb.cur_poly lp in info (fun () -> "remainder: "^(stringPcut metadata r)); let cur_pb = { @@ -657,7 +657,7 @@ let deg_hom p = | (a,m)::_ -> Monomial.deg m let pbuchf table metadata cur_pb homogeneous (lp, lpc) p = - (** Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) + (* Invariant: [lp] is [List.tl (Array.to_list table.allpol)] *) sinfo "computation of the Groebner basis"; let () = match table.hmon with | None -> () diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index ef60a23e80..1777418ef6 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -374,7 +374,7 @@ let remove_zeros lci = let m = List.length lci in let u = Array.make m false in let rec utiles k = - (** TODO: Find a more reasonable implementation of this traversal. *) + (* TODO: Find a more reasonable implementation of this traversal. *) if k >= m || u.(k) then () else let () = u.(k) <- true in diff --git a/plugins/rtauto/g_rtauto.mlg b/plugins/rtauto/g_rtauto.mlg index 9c9fdcfa2f..d8724eb976 100644 --- a/plugins/rtauto/g_rtauto.mlg +++ b/plugins/rtauto/g_rtauto.mlg @@ -17,6 +17,6 @@ open Ltac_plugin DECLARE PLUGIN "rtauto_plugin" TACTIC EXTEND rtauto -| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) } +| [ "rtauto" ] -> { Refl_tauto.rtauto_tac } END diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index e66fa10d5b..a6b6c57ff9 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -16,7 +16,6 @@ open CErrors open Util open Term open Constr -open Tacmach open Proof_search open Context.Named.Declaration @@ -60,12 +59,11 @@ let l_I_Or_r = gen_constant "plugins.rtauto.I_Or_r" let l_E_Or = gen_constant "plugins.rtauto.E_Or" let l_D_Or = gen_constant "plugins.rtauto.D_Or" +let special_whd env sigma c = + Reductionops.clos_whd_flags CClosure.all env sigma c -let special_whd gl c = - Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c - -let special_nf gl c = - Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c +let special_nf env sigma c = + Reductionops.clos_norm_flags CClosure.betaiotazeta env sigma c type atom_env= {mutable next:int; @@ -83,61 +81,58 @@ let make_atom atom_env term= atom_env.next<- i + 1; Atom i -let rec make_form atom_env gls term = +let rec make_form env sigma atom_env term = let open EConstr in let open Vars in - let normalize=special_nf gls in - let cciterm=special_whd gls term in - let sigma = Tacmach.project gls in - match EConstr.kind sigma cciterm with - Prod(_,a,b) -> - if noccurn sigma 1 b && - Retyping.get_sort_family_of - (pf_env gls) sigma a == InProp - then - let fa=make_form atom_env gls a in - let fb=make_form atom_env gls b in - Arrow (fa,fb) - else - make_atom atom_env (normalize term) - | Cast(a,_,_) -> - make_form atom_env gls a - | Ind (ind, _) -> - if Names.eq_ind ind (fst (Lazy.force li_False)) then - Bot - else - make_atom atom_env (normalize term) - | App(hd,argv) when Int.equal (Array.length argv) 2 -> - begin - try - let ind, _ = destInd sigma hd in - if Names.eq_ind ind (fst (Lazy.force li_and)) then - let fa=make_form atom_env gls argv.(0) in - let fb=make_form atom_env gls argv.(1) in - Conjunct (fa,fb) - else if Names.eq_ind ind (fst (Lazy.force li_or)) then - let fa=make_form atom_env gls argv.(0) in - let fb=make_form atom_env gls argv.(1) in - Disjunct (fa,fb) - else make_atom atom_env (normalize term) - with DestKO -> make_atom atom_env (normalize term) - end - | _ -> make_atom atom_env (normalize term) - -let rec make_hyps atom_env gls lenv = function + let normalize = special_nf env sigma in + let cciterm = special_whd env sigma term in + match EConstr.kind sigma cciterm with + Prod(_,a,b) -> + if noccurn sigma 1 b && + Retyping.get_sort_family_of env sigma a == InProp + then + let fa = make_form env sigma atom_env a in + let fb = make_form env sigma atom_env b in + Arrow (fa,fb) + else + make_atom atom_env (normalize term) + | Cast(a,_,_) -> + make_form env sigma atom_env a + | Ind (ind, _) -> + if Names.eq_ind ind (fst (Lazy.force li_False)) then + Bot + else + make_atom atom_env (normalize term) + | App(hd,argv) when Int.equal (Array.length argv) 2 -> + begin + try + let ind, _ = destInd sigma hd in + if Names.eq_ind ind (fst (Lazy.force li_and)) then + let fa = make_form env sigma atom_env argv.(0) in + let fb = make_form env sigma atom_env argv.(1) in + Conjunct (fa,fb) + else if Names.eq_ind ind (fst (Lazy.force li_or)) then + let fa = make_form env sigma atom_env argv.(0) in + let fb = make_form env sigma atom_env argv.(1) in + Disjunct (fa,fb) + else make_atom atom_env (normalize term) + with DestKO -> make_atom atom_env (normalize term) + end + | _ -> make_atom atom_env (normalize term) + +let rec make_hyps env sigma atom_env lenv = function [] -> [] | LocalDef (_,body,typ)::rest -> - make_hyps atom_env gls (typ::body::lenv) rest + make_hyps env sigma atom_env (typ::body::lenv) rest | LocalAssum (id,typ)::rest -> - let hrec= - make_hyps atom_env gls (typ::lenv) rest in - if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id c) lenv || - (Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) typ != InProp) - then - hrec - else - (id,make_form atom_env gls typ)::hrec + let hrec= + make_hyps env sigma atom_env (typ::lenv) rest in + if List.exists (fun c -> Termops.local_occur_var Evd.empty (* FIXME *) id c) lenv || + (Retyping.get_sort_family_of env sigma typ != InProp) + then + hrec + else + (id,make_form env sigma atom_env typ)::hrec let rec build_pos n = if n<=1 then force node_count l_xH @@ -251,73 +246,76 @@ let () = declare_bool_option opt_check open Pp -let rtauto_tac gls= - Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; - let gamma={next=1;env=[]} in - let gl=pf_concl gls in - let () = - if Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) gl != InProp - then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in - let glf=make_form gamma gls gl in - let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in - let formula= - List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in - let search_fun = match Tacinterp.get_debug() with - | Tactic_debug.DebugOn 0 -> Search.debug_depth_first - | _ -> Search.depth_first - in - let () = - begin - reset_info (); +let rtauto_tac = + Proofview.Goal.enter begin fun gl -> + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + Coqlib.check_required_library ["Coq";"rtauto";"Rtauto"]; + let gamma={next=1;env=[]} in + let () = + if Retyping.get_sort_family_of env sigma concl != InProp + then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in + let glf = make_form env sigma gamma concl in + let hyps = make_hyps env sigma gamma [concl] hyps in + let formula= + List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in + let search_fun = match Tacinterp.get_debug() with + | Tactic_debug.DebugOn 0 -> Search.debug_depth_first + | _ -> Search.depth_first + in + let () = + begin + reset_info (); + if !verbose then + Feedback.msg_info (str "Starting proof-search ..."); + end in + let search_start_time = System.get_time () in + let prf = + try project (search_fun (init_state [] formula)) + with Not_found -> + user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in + let search_end_time = System.get_time () in + let () = if !verbose then + begin + Feedback.msg_info (str "Proof tree found in " ++ + System.fmt_time_difference search_start_time search_end_time); + pp_info (); + Feedback.msg_info (str "Building proof term ... ") + end in + let build_start_time=System.get_time () in + let () = step_count := 0; node_count := 0 in + let main = mkApp (force node_count l_Reflect, + [|build_env gamma; + build_form formula; + build_proof [] 0 prf|]) in + let term= + applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in + let build_end_time=System.get_time () in + let () = if !verbose then + begin + Feedback.msg_info (str "Proof term built in " ++ + System.fmt_time_difference build_start_time build_end_time ++ + fnl () ++ + str "Proof size : " ++ int !step_count ++ + str " steps" ++ fnl () ++ + str "Proof term size : " ++ int (!step_count+ !node_count) ++ + str " nodes (constants)" ++ fnl () ++ + str "Giving proof term to Coq ... ") + end in + let tac_start_time = System.get_time () in + let term = EConstr.of_constr term in + let result= + if !check then + Tactics.exact_check term + else + Tactics.exact_no_check term in + let tac_end_time = System.get_time () in + let () = + if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then - Feedback.msg_info (str "Starting proof-search ..."); - end in - let search_start_time = System.get_time () in - let prf = - try project (search_fun (init_state [] formula)) - with Not_found -> - user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in - let search_end_time = System.get_time () in - let () = if !verbose then - begin - Feedback.msg_info (str "Proof tree found in " ++ - System.fmt_time_difference search_start_time search_end_time); - pp_info (); - Feedback.msg_info (str "Building proof term ... ") - end in - let build_start_time=System.get_time () in - let () = step_count := 0; node_count := 0 in - let main = mkApp (force node_count l_Reflect, - [|build_env gamma; - build_form formula; - build_proof [] 0 prf|]) in - let term= - applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in - let build_end_time=System.get_time () in - let () = if !verbose then - begin - Feedback.msg_info (str "Proof term built in " ++ - System.fmt_time_difference build_start_time build_end_time ++ - fnl () ++ - str "Proof size : " ++ int !step_count ++ - str " steps" ++ fnl () ++ - str "Proof term size : " ++ int (!step_count+ !node_count) ++ - str " nodes (constants)" ++ fnl () ++ - str "Giving proof term to Coq ... ") - end in - let tac_start_time = System.get_time () in - let term = EConstr.of_constr term in - let result= - if !check then - Proofview.V82.of_tactic (Tactics.exact_check term) gls - else - Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in - let tac_end_time = System.get_time () in - let () = - if !check then Feedback.msg_info (str "Proof term type-checking is on"); - if !verbose then - Feedback.msg_info (str "Internal tactic executed in " ++ - System.fmt_time_difference tac_start_time tac_end_time) in + Feedback.msg_info (str "Internal tactic executed in " ++ + System.fmt_time_difference tac_start_time tac_end_time) in result - + end diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index a91dd666a6..49b5ee5ac7 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -14,14 +14,15 @@ type atom_env= {mutable next:int; mutable env:(Constr.t*int) list} -val make_form : atom_env -> - Goal.goal Evd.sigma -> EConstr.types -> Proof_search.form +val make_form + : Environ.env -> Evd.evar_map -> atom_env + -> EConstr.types -> Proof_search.form -val make_hyps : - atom_env -> - Goal.goal Evd.sigma -> - EConstr.types list -> - EConstr.named_context -> - (Names.Id.t * Proof_search.form) list +val make_hyps + : Environ.env -> Evd.evar_map + -> atom_env + -> EConstr.types list + -> EConstr.named_context + -> (Names.Id.t * Proof_search.form) list -val rtauto_tac : Tacmach.tactic +val rtauto_tac : unit Proofview.tactic diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 4109e9cf38..65201d922f 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -194,12 +194,12 @@ let exec_tactic env evd n f args = in let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in - (** Build the getter *) + (* Build the getter *) let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in let get_res = TacML (CAst.make (get_res, [TacGeneric n])) in let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in - (** Evaluate the whole result *) + (* Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd = Evd.minimize_universes (Refiner.project gls) in @@ -394,13 +394,9 @@ let subst_th (subst,th) = let theory_to_obj : ring_info -> obj = let cache_th (name,th) = add_entry name th in - declare_object - {(default_object "tactic-new-ring-theory") with - open_function = (fun i o -> if Int.equal i 1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x)} - + declare_object @@ global_object_nodischarge "tactic-new-ring-theory" + ~cache:cache_th + ~subst:(Some subst_th) let setoid_of_relation env evd a r = try @@ -891,12 +887,9 @@ let subst_th (subst,th) = let ftheory_to_obj : field_info -> obj = let cache_th (name,th) = add_field_entry name th in - declare_object - {(default_object "tactic-new-field-theory") with - open_function = (fun i o -> if Int.equal i 1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x) } + declare_object @@ global_object_nodischarge "tactic-new-field-theory" + ~cache:cache_th + ~subst:(Some subst_th) let field_equality evd r inv req = match EConstr.kind !evd req with diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index bb8a0faf2e..11e282e4f5 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -104,6 +104,7 @@ type ssrintrosarg = Tacexpr.raw_tactic_expr * ssripats type ssrfwdid = Id.t + (** Binders (for fwd tactics) *) type 'term ssrbind = | Bvar of Name.t diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index efc4a2c743..cd9af84ed9 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -263,7 +263,7 @@ let of_ftactic ftac gl = let tac = Proofview.V82.of_tactic tac in let { sigma = sigma } = tac gl in let ans = match !r with - | None -> assert false (** If the tactic failed we should not reach this point *) + | None -> assert false (* If the tactic failed we should not reach this point *) | Some ans -> ans in (sigma, ans) diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 0553260472..18b4aeab1e 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -86,9 +86,9 @@ end (* }}} *************************************************************** *) open State -(** [=> *] ****************************************************************) -(** [nb_assums] returns the number of dependent premises *) -(** Warning: unlike [nb_deps_assums], it does not perform reduction *) +(***[=> *] ****************************************************************) +(** [nb_assums] returns the number of dependent premises + Warning: unlike [nb_deps_assums], it does not perform reduction *) let rec nb_assums cur env sigma t = match EConstr.kind sigma t with | Prod(name,ty,body) -> @@ -148,7 +148,7 @@ let tac_case t = Ssrelim.ssrscasetac t end -(** [=> [: id]] ************************************************************) +(***[=> [: id]] ************************************************************) [@@@ocaml.warning "-3"] let mk_abstract_id = let open Coqlib in diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 4ed75cdbe4..191a4e9a20 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -359,7 +359,7 @@ let coerce_search_pattern_to_sort hpat = Pattern.PApp (fp, args') in let hr, na = splay_search_pattern 0 hpat in let dc, ht = - let hr, _ = Typeops.type_of_global_in_context env hr (** FIXME *) in + let hr, _ = Typeops.type_of_global_in_context env hr (* FIXME *) in Reductionops.splay_prod env sigma (EConstr.of_constr hr) in let np = List.length dc in if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 3f974ea063..1aa64d7141 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -45,16 +45,11 @@ module AdaptorDb = struct let t' = Detyping.subst_glob_constr subst t in if t' == t then a else k, t' - let classify_adaptor x = Libobject.Substitute x - let in_db = - Libobject.declare_object { - (Libobject.default_object "VIEW_ADAPTOR_DB") - with - Libobject.open_function = (fun i o -> if i = 1 then cache_adaptor o); - Libobject.cache_function = cache_adaptor; - Libobject.subst_function = subst_adaptor; - Libobject.classify_function = classify_adaptor } + let open Libobject in + declare_object @@ global_object_nodischarge "VIEW_ADAPTOR_DB" + ~cache:cache_adaptor + ~subst:(Some subst_adaptor) let declare kind terms = List.iter (fun term -> Lib.add_anonymous_leaf (in_db (kind,term))) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 6497b6ff98..efd65ade15 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -122,6 +122,7 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t + (** Constructors for constr_expr *) let isCVar = function { CAst.v = CRef (qid,_) } -> qualid_is_ident qid | _ -> false let destCVar = function @@ -139,6 +140,7 @@ let mkCLambda ?loc name ty t = CAst.make ?loc @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((CAst.make ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) + (** Constructors for rawconstr *) let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None) let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) @@ -925,7 +927,7 @@ let of_ftactic ftac gl = let tac = Proofview.V82.of_tactic tac in let { sigma = sigma } = tac gl in let ans = match !r with - | None -> assert false (** If the tactic failed we should not reach this point *) + | None -> assert false (* If the tactic failed we should not reach this point *) | Some ans -> ans in (sigma, ans) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 8672c55767..f0bb6f58a6 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -194,6 +194,7 @@ val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> c (** [do_once r f] calls [f] and updates the ref only once *) val do_once : 'a option ref -> (unit -> 'a) -> unit + (** [assert_done r] return the content of r. @raise Anomaly is r is [None] *) val assert_done : 'a option ref -> 'a diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml deleted file mode 100644 index 94255bab6c..0000000000 --- a/plugins/syntax/ascii_syntax.ml +++ /dev/null @@ -1,100 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <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) *) -(************************************************************************) - - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "ascii_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -open Pp -open CErrors -open Util -open Names -open Glob_term -open Globnames -open Coqlib - -exception Non_closed_ascii - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) - -let is_gr c gr = match DAst.get c with -| GRef (r, _) -> GlobRef.equal r gr -| _ -> false - -let ascii_module = ["Coq";"Strings";"Ascii"] -let ascii_modpath = MPfile (make_dir ascii_module) - -let ascii_path = make_path ascii_module "ascii" - -let ascii_label = Label.make "ascii" -let ascii_kn = MutInd.make2 ascii_modpath ascii_label -let path_of_Ascii = ((ascii_kn,0),1) -let static_glob_Ascii = ConstructRef path_of_Ascii - -let glob_Ascii = lazy (lib_ref "plugins.syntax.Ascii") - -open Lazy - -let interp_ascii ?loc p = - let rec aux n p = - if Int.equal n 0 then [] else - let mp = p mod 2 in - (DAst.make ?loc @@ GRef (lib_ref (if Int.equal mp 0 then "core.bool.false" else "core.bool.true"),None)) - :: (aux (n-1) (p/2)) in - DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) - -let interp_ascii_string ?loc s = - let p = - if Int.equal (String.length s) 1 then int_of_char s.[0] - else - if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2] - then int_of_string s - else - user_err ?loc ~hdr:"interp_ascii_string" - (str "Expects a single character or a three-digits ascii code.") in - interp_ascii ?loc p - -let uninterp_ascii r = - let rec uninterp_bool_list n = function - | [] when Int.equal n 0 -> 0 - | r::l when is_gr r (lib_ref "core.bool.true") -> 1+2*(uninterp_bool_list (n-1) l) - | r::l when is_gr r (lib_ref "core.bool.false") -> 2*(uninterp_bool_list (n-1) l) - | _ -> raise Non_closed_ascii in - try - let aux c = match DAst.get c with - | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l - | _ -> raise Non_closed_ascii in - Some (aux r) - with - Non_closed_ascii -> None - -let make_ascii_string n = - if n>=32 && n<=126 then String.make 1 (char_of_int n) - else Printf.sprintf "%03d" n - -let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let sc = "char_scope" in - register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string); - at_declare_ml_module enable_prim_token_interpretation - { pt_local = false; - pt_scope = sc; - pt_interp_info = Uid sc; - pt_required = (ascii_path,ascii_module); - pt_refs = [static_glob_Ascii]; - pt_in_match = true } diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack deleted file mode 100644 index 7b9213a0e2..0000000000 --- a/plugins/syntax/ascii_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Ascii_syntax diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg new file mode 100644 index 0000000000..1e06cd8ddb --- /dev/null +++ b/plugins/syntax/g_string.mlg @@ -0,0 +1,25 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +DECLARE PLUGIN "string_notation_plugin" + +{ + +open String_notation +open Names +open Stdarg + +} + +VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF + | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) ] -> + { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) } +END diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 10a0af0b8f..470deb4a60 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -125,7 +125,7 @@ let vernac_numeral_notation local ty f g scope opts = | None -> type_error_of g ty true in let o = { to_kind; to_ty; of_kind; of_ty; - num_ty = ty; + ty_name = ty; warning = opts } in (match opts, to_kind with diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune index bfdd480fe9..1ab16c700d 100644 --- a/plugins/syntax/plugin_base.dune +++ b/plugins/syntax/plugin_base.dune @@ -6,6 +6,13 @@ (libraries coq.plugins.ltac)) (library + (name string_notation_plugin) + (public_name coq.plugins.string_notation) + (synopsis "Coq string notation plugin") + (modules g_string string_notation) + (libraries coq.vernac)) + +(library (name r_syntax_plugin) (public_name coq.plugins.r_syntax) (synopsis "Coq syntax plugin: reals") @@ -13,23 +20,8 @@ (libraries coq.vernac)) (library - (name ascii_syntax_plugin) - (public_name coq.plugins.ascii_syntax) - (synopsis "Coq syntax plugin: ASCII") - (modules ascii_syntax) - (libraries coq.vernac)) - -(library - (name string_syntax_plugin) - (public_name coq.plugins.string_syntax) - (synopsis "Coq syntax plugin: strings") - (modules string_syntax) - (libraries coq.plugins.ascii_syntax)) - -(library (name int31_syntax_plugin) (public_name coq.plugins.int31_syntax) (synopsis "Coq syntax plugin: int31") (modules int31_syntax) (libraries coq.vernac)) - diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml new file mode 100644 index 0000000000..12ee4c6eda --- /dev/null +++ b/plugins/syntax/string_notation.ml @@ -0,0 +1,98 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +open Pp +open Util +open Names +open Libnames +open Globnames +open Constrexpr +open Constrexpr_ops +open Notation + +(** * String notation *) + +let get_constructors ind = + let mib,oib = Global.lookup_inductive ind in + let mc = oib.Declarations.mind_consnames in + Array.to_list + (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) + +let qualid_of_ref n = + n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty + +let q_option () = qualid_of_ref "core.option.type" +let q_list () = qualid_of_ref "core.list.type" +let q_byte () = qualid_of_ref "core.byte.type" + +let has_type f ty = + let (sigma, env) = Pfedit.get_current_context () in + let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in + try let _ = Constrintern.interp_constr env sigma c in true + with Pretype_errors.PretypeError _ -> false + +let type_error_to f ty = + CErrors.user_err + (pr_qualid f ++ str " should go from Byte.byte or (list Byte.byte) to " ++ + pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ").") + +let type_error_of g ty = + CErrors.user_err + (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ + str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).") + +let vernac_string_notation local ty f g scope = + let app x y = mkAppC (x,[y]) in + let cref q = mkRefC q in + let cbyte = cref (q_byte ()) in + let clist = cref (q_list ()) in + let coption = cref (q_option ()) in + let opt r = app coption r in + let clist_byte = app clist cbyte in + let tyc = Smartlocate.global_inductive_with_alias ty in + let to_ty = Smartlocate.global_with_alias f in + let of_ty = Smartlocate.global_with_alias g in + let cty = cref ty in + let arrow x y = + mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + in + let constructors = get_constructors tyc in + (* Check the type of f *) + let to_kind = + if has_type f (arrow clist_byte cty) then ListByte, Direct + else if has_type f (arrow clist_byte (opt cty)) then ListByte, Option + else if has_type f (arrow cbyte cty) then Byte, Direct + else if has_type f (arrow cbyte (opt cty)) then Byte, Option + else type_error_to f ty + in + (* Check the type of g *) + let of_kind = + if has_type g (arrow cty clist_byte) then ListByte, Direct + else if has_type g (arrow cty (opt clist_byte)) then ListByte, Option + else if has_type g (arrow cty cbyte) then Byte, Direct + else if has_type g (arrow cty (opt cbyte)) then Byte, Option + else type_error_of g ty + in + let o = { to_kind = to_kind; + to_ty = to_ty; + of_kind = of_kind; + of_ty = of_ty; + ty_name = ty; + warning = () } + in + let i = + { pt_local = local; + pt_scope = scope; + pt_interp_info = StringNotation o; + pt_required = Nametab.path_of_global (IndRef tyc),[]; + pt_refs = constructors; + pt_in_match = true } + in + enable_prim_token_interpretation i diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli new file mode 100644 index 0000000000..9a0174abf2 --- /dev/null +++ b/plugins/syntax/string_notation.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +open Libnames +open Vernacexpr + +(** * String notation *) + +val vernac_string_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> unit diff --git a/plugins/syntax/string_notation_plugin.mlpack b/plugins/syntax/string_notation_plugin.mlpack new file mode 100644 index 0000000000..6aa081dab4 --- /dev/null +++ b/plugins/syntax/string_notation_plugin.mlpack @@ -0,0 +1,2 @@ +String_notation +G_string diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml deleted file mode 100644 index 59e65a0672..0000000000 --- a/plugins/syntax/string_syntax.ml +++ /dev/null @@ -1,81 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <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) *) -(************************************************************************) - -open Names -open Globnames -open Ascii_syntax_plugin.Ascii_syntax -open Glob_term -open Coqlib - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "string_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -exception Non_closed_string - -(* make a string term from the string s *) - -let string_module = ["Coq";"Strings";"String"] - -let string_modpath = MPfile (make_dir string_module) -let string_path = make_path string_module "string" - -let string_kn = MutInd.make2 string_modpath @@ Label.make "string" -let static_glob_EmptyString = ConstructRef ((string_kn,0),1) -let static_glob_String = ConstructRef ((string_kn,0),2) - -let glob_String = lazy (lib_ref "plugins.syntax.String") -let glob_EmptyString = lazy (lib_ref "plugins.syntax.EmptyString") - -let is_gr c gr = match DAst.get c with -| GRef (r, _) -> GlobRef.equal r gr -| _ -> false - -open Lazy - -let interp_string ?loc s = - let le = String.length s in - let rec aux n = - if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else - DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None), - [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)]) - in aux 0 - -let uninterp_string (AnyGlobConstr r) = - try - let b = Buffer.create 16 in - let rec aux c = match DAst.get c with - | GApp (k,[a;s]) when is_gr k (force glob_String) -> - (match uninterp_ascii a with - | Some c -> Buffer.add_char b (Char.chr c); aux s - | _ -> raise Non_closed_string) - | GRef (z,_) when GlobRef.equal z (force glob_EmptyString) -> - Some (Buffer.contents b) - | _ -> - raise Non_closed_string - in aux r - with - Non_closed_string -> None - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let _ = - let sc = "string_scope" in - register_string_interpretation sc (interp_string,uninterp_string); - at_declare_ml_module enable_prim_token_interpretation - { pt_local = false; - pt_scope = sc; - pt_interp_info = Uid sc; - pt_required = (string_path,["Coq";"Strings";"String"]); - pt_refs = [static_glob_String; static_glob_EmptyString]; - pt_in_match = true } diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack deleted file mode 100644 index 45d6e0fa23..0000000000 --- a/plugins/syntax/string_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -String_syntax |