From d7a5f439de0208c4a543a81158107b8ccecb6ced Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 03:27:46 +0100 Subject: [vernac] Increase table size. As of Nov 2017, the standard number of entries is 85, it easily goes up with some other plugins, so 211 seems like a good compromise. --- vernac/vernacinterp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac') diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 41fee6bd08..d2687161a1 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -15,7 +15,7 @@ type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit (* Table of vernac entries *) let vernac_tab = - (Hashtbl.create 51 : + (Hashtbl.create 211 : (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t) let vinterp_add depr s f = -- cgit v1.2.3 From dc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 03:40:45 +0100 Subject: [plugins] Prepare plugin API for functional handling of state. To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state. --- vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 43 +++++++++++++------------------------------ vernac/vernacentries.mli | 14 ++------------ vernac/vernacinterp.ml | 8 +++++--- vernac/vernacinterp.mli | 16 ++++++++++------ vernac/vernacstate.ml | 29 +++++++++++++++++++++++++++++ vernac/vernacstate.mli | 19 +++++++++++++++++++ 7 files changed, 79 insertions(+), 51 deletions(-) create mode 100644 vernac/vernacstate.ml create mode 100644 vernac/vernacstate.mli (limited to 'vernac') diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 850902d6ba..8673155e28 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -15,6 +15,7 @@ Command Classes Record Assumptions +Vernacstate Vernacinterp Mltop Topfmt diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5bcb3b1e15..a71794f5ee 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1909,7 +1909,7 @@ let vernac_load interp fname = * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) -let interp ?proof ?loc locality poly c = +let interp ?proof ?loc locality poly st c = vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c); match c with (* The below vernac are candidates for removal from the main type @@ -2069,7 +2069,10 @@ let interp ?proof ?loc locality poly c = | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"] (* Extensions *) - | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args) + | VernacExtend (opn,args) -> + (* XXX: Here we are returning the state! :) *) + let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) st in + () (* Vernaculars that take a locality flag *) let check_vernac_supports_locality c l = @@ -2147,28 +2150,6 @@ let locate_if_not_already ?loc (e, info) = exception HasNotFailed exception HasFailed of Pp.t -type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} - -let s_cache = ref (States.freeze ~marshallable:`No) -let s_proof = ref (Proof_global.freeze ~marshallable:`No) - -let invalidate_cache () = - s_cache := Obj.magic 0; - s_proof := Obj.magic 0 - -let freeze_interp_state marshallable = - { system = (s_cache := States.freeze ~marshallable; !s_cache); - proof = (s_proof := Proof_global.freeze ~marshallable; !s_proof); - shallow = marshallable = `Shallow } - -let unfreeze_interp_state { system; proof } = - if (!s_cache != system) then (s_cache := system; States.unfreeze system); - if (!s_proof != proof) then (s_proof := proof; Proof_global.unfreeze proof) - (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) let with_fail st b f = @@ -2187,8 +2168,8 @@ let with_fail st b f = (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) with e when CErrors.noncritical e -> (* Restore the previous state XXX Careful here with the cache! *) - invalidate_cache (); - unfreeze_interp_state st; + Vernacstate.invalidate_cache (); + Vernacstate.unfreeze_interp_state st; let (e, _) = CErrors.push e in match e with | HasNotFailed -> @@ -2230,8 +2211,8 @@ let interp ?(verbosely=true) ?proof st (loc,c) = try vernac_timeout begin fun () -> if verbosely - then Flags.verbosely (interp ?proof ?loc locality poly) c - else Flags.silently (interp ?proof ?loc locality poly) c; + then Flags.verbosely (interp ?proof ?loc locality poly st) c + else Flags.silently (interp ?proof ?loc locality poly st) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode; ignore (Flags.use_polymorphic_flag ()) @@ -2252,7 +2233,9 @@ let interp ?(verbosely=true) ?proof st (loc,c) = if verbosely then Flags.verbosely (aux false) c else aux false c +(* XXX: There is a bug here in case of an exception, see @gares + comments on the PR *) let interp ?verbosely ?proof st cmd = - unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; interp ?verbosely ?proof st cmd; - freeze_interp_state `No + Vernacstate.freeze_interp_state `No diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 56635c8011..67001bc24e 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -14,21 +14,11 @@ val dump_global : Libnames.reference or_by_notation -> unit val vernac_require : Libnames.reference option -> bool option -> Libnames.reference list -> unit -type interp_state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} - -val freeze_interp_state : Summary.marshallable -> interp_state -val unfreeze_interp_state : interp_state -> unit - (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - interp_state -> - Vernacexpr.vernac_expr Loc.located -> interp_state + Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -40,7 +30,7 @@ val make_cases : string -> string list list (* XXX STATE: this type hints that restoring the state should be the caller's responsibility *) -val with_fail : interp_state -> bool -> (unit -> unit) -> unit +val with_fail : Vernacstate.t -> bool -> (unit -> unit) -> unit val command_focus : unit Proof.focus_kind diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index d2687161a1..1d024386e2 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -11,7 +11,8 @@ open Pp open CErrors type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> + Vernacstate.t -> Vernacstate.t (* Table of vernac entries *) let vernac_tab = @@ -66,8 +67,9 @@ let call ?locality ?loc (opn,converted_args) = let hunk = callback converted_args in phase := "Executing command"; Locality.LocalityFixme.set locality; - hunk loc; - Locality.LocalityFixme.assert_consumed() + let res = hunk loc in + Locality.LocalityFixme.assert_consumed (); + res with | Drop -> raise Drop | reraise -> diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 84370fdc29..1c66b1c045 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -9,12 +9,16 @@ (** Interpretation of extended vernac phrases. *) type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit -val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit -val overwriting_vinterp_add : - Vernacexpr.extend_name -> vernac_command -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> + Vernacstate.t -> Vernacstate.t + +val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit + +val overwriting_vinterp_add : Vernacexpr.extend_name -> vernac_command -> unit val vinterp_init : unit -> unit -val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit + +val call : ?locality:bool -> ?loc:Loc.t -> + Vernacexpr.extend_name * Genarg.raw_generic_argument list -> + Vernacstate.t -> Vernacstate.t diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml new file mode 100644 index 0000000000..9802a03cad --- /dev/null +++ b/vernac/vernacstate.ml @@ -0,0 +1,29 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t +val unfreeze_interp_state : t -> unit + +(* WARNING: Do not use, it will go away in future releases *) +val invalidate_cache : unit -> unit -- cgit v1.2.3