diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/ExtrHaskellString.v | 20 | ||||
| -rw-r--r-- | plugins/extraction/ExtrOcamlString.v | 16 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 74 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 20 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 8 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 3 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 3 | ||||
| -rw-r--r-- | plugins/rtauto/g_rtauto.mlg | 2 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 246 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.mli | 19 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 19 | ||||
| -rw-r--r-- | plugins/ssr/ssrview.ml | 13 | ||||
| -rw-r--r-- | plugins/syntax/ascii_syntax.ml | 100 | ||||
| -rw-r--r-- | plugins/syntax/ascii_syntax_plugin.mlpack | 1 | ||||
| -rw-r--r-- | plugins/syntax/g_string.mlg | 25 | ||||
| -rw-r--r-- | plugins/syntax/numeral.ml | 2 | ||||
| -rw-r--r-- | plugins/syntax/plugin_base.dune | 22 | ||||
| -rw-r--r-- | plugins/syntax/string_notation.ml | 98 | ||||
| -rw-r--r-- | plugins/syntax/string_notation.mli | 16 | ||||
| -rw-r--r-- | plugins/syntax/string_notation_plugin.mlpack | 2 | ||||
| -rw-r--r-- | plugins/syntax/string_syntax.ml | 81 | ||||
| -rw-r--r-- | plugins/syntax/string_syntax_plugin.mlpack | 1 |
22 files changed, 364 insertions, 427 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/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/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 ec2adf065a..47f593ff3e 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -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 *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e626df5579..4bb52f599a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -632,7 +632,8 @@ let solve_remaining_by env sigma holes by = | 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 diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 284642b38c..816741b894 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -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/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 f1fa694356..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 9fea3ddcda..65201d922f 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -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/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/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 |