diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 78 | ||||
| -rw-r--r-- | stm/stm.mli | 23 |
2 files changed, 82 insertions, 19 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 5790bfc07e..04f08e488b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -202,7 +202,7 @@ let mkTransCmd cast cids ceff cqueue = (* Parts of the system state that are morally part of the proof state *) let summary_pstate = Evarutil.meta_counter_summary_tag, Evd.evar_counter_summary_tag, - DeclareObl.program_tcc_summary_tag + Declare.Obls.State.prg_tag type cached_state = | EmptyState @@ -878,7 +878,7 @@ end = struct (* {{{ *) Vernacstate.LemmaStack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) - DeclareObl.ProgramDecl.t CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) + Declare.Obls.State.t type partial_state = [ `Full of Vernacstate.t @@ -1684,7 +1684,9 @@ end = struct (* {{{ *) (* STATE We use the state resulting from reaching start. *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None))); - `OK proof + (* Is this name the same than the one in scope? *) + let name = Declare.get_po_name proof in + `OK name end with e -> let (e, info) = Exninfo.capture e in @@ -1723,7 +1725,7 @@ end = struct (* {{{ *) | `ERROR -> exit 1 | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false - | `OK { Declare.name } -> + | `OK name -> let con = Nametab.locate_constant (Libnames.qualid_of_ident name) in let c = Global.lookup_constant con in let o = match c.Declarations.const_body with @@ -2576,6 +2578,21 @@ end (* }}} *) (******************************************************************************) (** STM initialization options: *) + +type option_command = OptionSet of string option | OptionUnset + +type injection_command = + | OptionInjection of (Goptions.option_name * option_command) + (** Set flags or options before the initial state is ready. *) + | RequireInjection of (string * string option * bool option) + (** Require libraries before the initial state is + ready. Parameters follow [Library], that is to say, + [lib,prefix,import_export] means require library [lib] from + optional [prefix] and [import_export] if [Some false/Some true] + is used. *) + (* -load-vernac-source interleaving is not supported yet *) + (* | LoadInjection of (string * bool) *) + type stm_init_options = { doc_type : stm_doc_type (** The STM does set some internal flags differently depending on @@ -2589,12 +2606,9 @@ type stm_init_options = (** [vo] load paths for the document. Usually extracted from -R options / _CoqProject *) - ; require_libs : (string * string option * bool option) list - (** Require [require_libs] before the initial state is - ready. Parameters follow [Library], that is to say, - [lib,prefix,import_export] means require library [lib] from - optional [prefix] and [import_export] if [Some false/Some true] - is used. *) + ; injections : injection_command list + (** Injects Require and Set/Unset commands before the initial + state is ready *) ; stm_options : AsyncOpts.stm_opt (** Low-level STM options *) @@ -2625,13 +2639,51 @@ let dirpath_of_file f = let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir -let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } = +let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } = let require_file (dir, from, exp) = let mp = Libnames.qualid_of_string dir in let mfrom = Option.map Libnames.qualid_of_string from in Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in + let interp_set_option opt v old = + let open Goptions in + let err expect = + let opt = String.concat " " opt in + let got = v in (* avoid colliding with Pp.v *) + CErrors.user_err + Pp.(str "-set: " ++ str opt ++ + str" expects " ++ str expect ++ + str" but got " ++ str got) + in + match old with + | BoolValue _ -> + let v = match String.trim v with + | "true" -> true + | "false" | "" -> false + | _ -> err "a boolean" + in + BoolValue v + | IntValue _ -> + let v = String.trim v in + let v = match int_of_string_opt v with + | Some _ as v -> v + | None -> if v = "" then None else err "an int" + in + IntValue v + | StringValue _ -> StringValue v + | StringOptValue _ -> StringOptValue (Some v) in + + let set_option = let open Goptions in function + | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt + | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true + | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v in + + let handle_injection = function + | RequireInjection r -> require_file r + (* | LoadInjection l -> *) + | OptionInjection o -> set_option o in + (* Set the options from the new documents *) AsyncOpts.cur_opt := stm_options; @@ -2670,7 +2722,7 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } end; (* Import initial libraries. *) - List.iter require_file require_libs; + List.iter handle_injection injections; (* We record the state at this point! *) State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial; @@ -3258,7 +3310,7 @@ let unreachable_state_hook = Hooks.unreachable_state_hook let document_add_hook = Hooks.document_add_hook let document_edit_hook = Hooks.document_edit_hook let sentence_exec_hook = Hooks.sentence_exec_hook -let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref) +let () = Declare.Obls.stm_get_fix_exn := (fun () -> !State.fix_exn_ref) type document = VCS.vcs let backup () = VCS.backup () diff --git a/stm/stm.mli b/stm/stm.mli index 2c27d63b82..9780c96512 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -52,6 +52,20 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) +type option_command = OptionSet of string option | OptionUnset + +type injection_command = + | OptionInjection of (Goptions.option_name * option_command) + (** Set flags or options before the initial state is ready. *) + | RequireInjection of (string * string option * bool option) + (** Require libraries before the initial state is + ready. Parameters follow [Library], that is to say, + [lib,prefix,import_export] means require library [lib] from + optional [prefix] and [import_export] if [Some false/Some true] + is used. *) + (* -load-vernac-source interleaving is not supported yet *) + (* | LoadInjection of (string * bool) *) + (** STM initialization options: *) type stm_init_options = { doc_type : stm_doc_type @@ -66,12 +80,9 @@ type stm_init_options = (** [vo] load paths for the document. Usually extracted from -R options / _CoqProject *) - ; require_libs : (string * string option * bool option) list - (** Require [require_libs] before the initial state is - ready. Parameters follow [Library], that is to say, - [lib,prefix,import_export] means require library [lib] from - optional [prefix] and [import_export] if [Some false/Some true] - is used. *) + ; injections : injection_command list + (** Injects Require and Set/Unset commands before the initial + state is ready *) ; stm_options : AsyncOpts.stm_opt (** Low-level STM options *) |