aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml6
-rw-r--r--stm/lemmas.ml24
-rw-r--r--stm/lemmas.mli9
-rw-r--r--stm/stm.ml13
-rw-r--r--stm/texmacspp.ml14
-rw-r--r--stm/vernac_classifier.ml20
6 files changed, 43 insertions, 43 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 222f02c007..e0315dec52 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,9 +60,7 @@ module Make(T : Task) = struct
type more_data =
| MoreDataUnivLevel of Univ.universe_level list
-
- let request_expiry_of_task (t, c) = T.request_of_task t, c
-
+
let slave_respond (Request r) =
let res = T.perform r in
Response res
@@ -298,7 +296,7 @@ module Make(T : Task) = struct
let slave_feeder oc fb =
Marshal.to_channel oc (RespFeedback fb) []; flush oc in
Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
- Pp.log_via_feedback ();
+ Pp.log_via_feedback (fun msg -> Richpp.repr (Richpp.richpp_of_pp msg));
Universes.set_remote_new_univ_level (bufferize (fun () ->
marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
match unmarshal_more_data (Option.get !slave_ic) with
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 5f4e4deb47..0a542c9c03 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -329,7 +329,8 @@ let check_exist =
)
let universe_proof_terminator compute_guard hook =
- let open Proof_global in function
+ let open Proof_global in
+ make_terminator begin function
| Admitted (id,k,pe,(ctx,pl)) ->
admit (id,k,pe) pl (hook (Some ctx)) ();
Pp.feedback Feedback.AddedAxiom
@@ -347,12 +348,16 @@ let universe_proof_terminator compute_guard hook =
save_anonymous_with_strength ~export_seff proof kind id
end;
check_exist exports
+ end
let standard_proof_terminator compute_guard hook =
universe_proof_terminator compute_guard (fun _ -> hook)
-let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
- let terminator = standard_proof_terminator compute_guard hook in
+let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+ let terminator = match terminator with
+ | None -> standard_proof_terminator compute_guard hook
+ | Some terminator -> terminator compute_guard hook
+ in
let sign =
match sign with
| Some sign -> sign
@@ -361,8 +366,11 @@ let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
!start_hook c;
Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
-let start_proof_univs id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
- let terminator = universe_proof_terminator compute_guard hook in
+let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+ let terminator = match terminator with
+ | None -> universe_proof_terminator compute_guard hook
+ | Some terminator -> terminator compute_guard hook
+ in
let sign =
match sign with
| Some sign -> sign
@@ -422,7 +430,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
let body,opaq = retrieve_first_recthm ref in
let subst = Evd.evar_universe_context_subst ctx in
let norm c = Universes.subst_opt_univs_constr subst c in
- let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in
+ let ctx = UState.context_set (*FIXME*) ctx in
let body = Option.map norm body in
List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
@@ -494,7 +502,7 @@ let save_proof ?proof = function
Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
(universes, Some binders))
in
- Proof_global.get_terminator() pe
+ Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
| Vernacexpr.Proved (is_opaque,idopt) ->
let (proof_obj,terminator) =
match proof with
@@ -504,7 +512,7 @@ let save_proof ?proof = function
in
(* if the proof is given explicitly, nothing has to be deleted *)
if Option.is_empty proof then Pfedit.delete_current_proof ();
- terminator (Proof_global.Proved (is_opaque,idopt,proof_obj))
+ Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
(* Miscellaneous *)
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 376374cb85..93f24b42cb 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -9,8 +9,6 @@
open Names
open Term
open Decl_kinds
-open Constrexpr
-open Vernacexpr
open Pfedit
type 'a declaration_hook
@@ -24,11 +22,13 @@ val call_hook :
val set_start_hook : (types -> unit) -> unit
val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
+ ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
unit declaration_hook -> unit
val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
+ ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> types ->
?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards ->
(Evd.evar_universe_context option -> unit declaration_hook) -> unit
@@ -43,6 +43,11 @@ val start_proof_with_initialization :
(types * (Name.t list * Impargs.manual_explicitation list))) list
-> int list option -> unit declaration_hook -> unit
+val universe_proof_terminator :
+ Proof_global.lemma_possible_guards ->
+ (Evd.evar_universe_context option -> unit declaration_hook) ->
+ Proof_global.proof_terminator
+
val standard_proof_terminator :
Proof_global.lemma_possible_guards -> unit declaration_hook ->
Proof_global.proof_terminator
diff --git a/stm/stm.ml b/stm/stm.ml
index 168d8bf084..e08f69a0e9 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -86,7 +86,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
| VernacResetName _ | VernacResetInitial | VernacBack _
| VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
| VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
- | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el
+ | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e
| _ -> false in
if internal_command expr then begin
prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
@@ -171,7 +171,7 @@ type visit = { step : step; next : Stateid.t }
(* Parts of the system state that are morally part of the proof state *)
let summary_pstate = [ Evarutil.meta_counter_summary_name;
- Evarutil.evar_counter_summary_name;
+ Evd.evar_counter_summary_name;
"program-tcc-table" ]
type state = {
system : States.state;
@@ -631,10 +631,9 @@ end = struct (* {{{ *)
States.unfreeze system; Proof_global.unfreeze proof
(* hack to make futures functional *)
- let in_t, out_t = Dyn.create "state4future"
let () = Future.set_freeze
- (fun () -> in_t (freeze_global_state `No, !cur_id))
- (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
+ (fun () -> Obj.magic (freeze_global_state `No, !cur_id))
+ (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i)
type frozen_state = state
type proof_part =
@@ -1515,7 +1514,7 @@ end = struct (* {{{ *)
let e, etac, time, fail =
let rec find time fail = function
| VernacSolve(_,_,re,b) -> re, b, time, fail
- | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e
+ | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
| VernacFail e -> find time true e
| _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
Hooks.call Hooks.with_fail fail (fun () ->
@@ -1630,7 +1629,7 @@ end = struct (* {{{ *)
let vernac_interp switch prev id q =
assert(TaskQueue.n_workers (Option.get !queue) > 0);
TaskQueue.enqueue_task (Option.get !queue)
- QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch)
+ QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch)
let init () = queue := Some (TaskQueue.create
(if !Flags.async_proofs_full then 1 else 0))
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index b912080413..b18e35a472 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -20,9 +20,6 @@ let unlock loc =
let start, stop = Loc.unloc loc in
(string_of_int start, string_of_int stop)
-let xmlNoop = (* almost noop *)
- PCData ""
-
let xmlWithLoc loc ename attr xml =
let start, stop = unlock loc in
Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
@@ -347,7 +344,7 @@ and pp_cases_pattern_expr cpe =
xmlApply loc
(xmlOperator "delimiter" ~attr:["name", delim] loc ::
[pp_cases_pattern_expr cpe])
-and pp_case_expr (e, (name, pat)) =
+and pp_case_expr (e, name, pat) =
match name, pat with
| None, None -> xmlScrutinee [pp_expr e]
| Some (loc, name), None ->
@@ -487,12 +484,12 @@ let rec tmpp v loc =
(* Control *)
| VernacLoad (verbose,f) ->
xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
- | VernacTime l ->
+ | VernacTime (loc,e) ->
xmlApply loc (Element("time",[],[]) ::
- List.map (fun(loc,e) ->tmpp e loc) l)
- | VernacRedirect (s, l) ->
+ [tmpp e loc])
+ | VernacRedirect (s, (loc,e)) ->
xmlApply loc (Element("redirect",["path", s],[]) ::
- List.map (fun(loc,e) ->tmpp e loc) l)
+ [tmpp e loc])
| VernacTimeout (s,e) ->
xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
[tmpp e loc])
@@ -724,7 +721,6 @@ let rec tmpp v loc =
| VernacRegister _ as x -> xmlTODO loc x
| VernacComments (cl) ->
xmlComment loc (List.flatten (List.map pp_comment cl))
- | VernacNop as x -> xmlTODO loc x
(* Stm backdoor *)
| VernacStm _ as x -> xmlTODO loc x
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index a898c687be..dcb6700941 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -60,7 +60,7 @@ let undo_classifier = ref (fun _ -> assert false)
let set_undo_classifier f = undo_classifier := f
let rec classify_vernac e =
- let rec static_classifier e = match e with
+ let static_classifier e = match e with
(* PG compatibility *)
| VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
| VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
@@ -86,7 +86,7 @@ let rec classify_vernac e =
make_polymorphic (classify_vernac e)
else classify_vernac e
| VernacTimeout (_,e) -> classify_vernac e
- | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e
+ | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
@@ -175,11 +175,13 @@ let rec classify_vernac e =
| VernacRegister _
| VernacNameSectionHypSet _
| VernacComments _ -> VtSideff [], VtLater
- | VernacDeclareTacticDefinition (_,l) ->
+ | VernacDeclareTacticDefinition l ->
let open Libnames in
+ let open Vernacexpr in
VtSideff (List.map (function
- | (Ident (_,r),_,_) -> r
- | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater
+ | TacticDefinition ((_,r),_) -> r
+ | TacticRedefinition (Ident (_,r),_) -> r
+ | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
(* Who knows *)
| VernacLoad _ -> VtSideff [], VtNow
(* (Local) Notations have to disappear *)
@@ -208,7 +210,6 @@ let rec classify_vernac e =
| VernacResetName _ | VernacResetInitial
| VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e
(* What are these? *)
- | VernacNop
| VernacToplevelControl _
| VernacRestoreState _
| VernacWriteState _ -> VtUnknown, VtNow
@@ -217,13 +218,6 @@ let rec classify_vernac e =
| VernacExtend (s,l) ->
try List.assoc s !classifiers l ()
with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
- and classify_vernac_list = function
- (* spiwack: It would be better to define a monoid on classifiers.
- So that the classifier of the list would be the composition of
- the classifier of the individual commands. Currently: special
- case for singleton lists.*)
- | [_,c] -> static_classifier c
- | l -> VtUnknown,VtNow
in
let res = static_classifier e in
if Flags.is_universe_polymorphism () then
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 05:55:35 +0000