aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml11
-rw-r--r--stm/lemmas.ml45
-rw-r--r--stm/lemmas.mli9
-rw-r--r--stm/spawned.ml13
-rw-r--r--stm/stm.ml194
-rw-r--r--stm/stm.mli13
-rw-r--r--stm/stm.mllib1
-rw-r--r--stm/texmacspp.ml770
-rw-r--r--stm/texmacspp.mli12
-rw-r--r--stm/vernac_classifier.ml34
10 files changed, 155 insertions, 947 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 1214fc4da9..a7b381ad62 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
@@ -106,7 +104,8 @@ module Make(T : Task) = struct
marshal_err ("unmarshal_more_data: "^s)
let report_status ?(id = !Flags.async_proofs_worker_id) s =
- Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s))
+ let open Feedback in
+ feedback ~id:(State Stateid.initial) (WorkerStatus(id, s))
module Worker = Spawn.Sync(struct end)
@@ -304,8 +303,8 @@ module Make(T : Task) = struct
let main_loop () =
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 ();
+ Feedback.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
+ Feedback.set_logger Feedback.feedback_logger;
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 5b205e79ef..0a63a3a0fe 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -31,6 +31,7 @@ open Reductionops
open Constrexpr
open Constrintern
open Impargs
+open Context.Rel.Declaration
type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
let mk_hook hook = hook
@@ -44,7 +45,8 @@ let call_hook fix_exn hook l c =
let retrieve_first_recthm = function
| VarRef id ->
- (pi2 (Global.lookup_named id),variable_opacity id)
+ let open Context.Named.Declaration in
+ (get_value (Global.lookup_named id),variable_opacity id)
| ConstRef cst ->
let cb = Global.lookup_constant cst in
(Global.body_of_constant_body cb, is_opaque cb)
@@ -107,11 +109,12 @@ let find_mutually_recursive_statements thms =
(fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
(Global.env()) hyps in
let ind_hyps =
- List.flatten (List.map_i (fun i (_,b,t) ->
+ List.flatten (List.map_i (fun i decl ->
+ let t = get_type decl in
match kind_of_term t with
| Ind ((kn,_ as ind),u) when
let mind = Global.lookup_mind kn in
- mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b ->
+ mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
[ind,x,i]
| _ ->
[]) 0 (List.rev whnf_hyp_hds)) in
@@ -147,7 +150,7 @@ let find_mutually_recursive_statements thms =
assert (List.is_empty rest);
(* One occ. of common coind ccls and no common inductive hyps *)
if not (List.is_empty common_same_indhyp) then
- if_verbose msg_info (str "Assuming mutual coinductive statements.");
+ if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
flush_all ();
indccl, true, []
| [], _::_ ->
@@ -155,7 +158,7 @@ let find_mutually_recursive_statements thms =
| ind :: _ ->
if List.distinct_f ind_ord (List.map pi1 ind)
then
- if_verbose msg_info
+ if_verbose Feedback.msg_info
(strbrk
("Coinductive statements do not follow the order of "^
"definition, assuming the proof to be by induction."));
@@ -303,7 +306,7 @@ let admit (id,k,e) pl hook () =
let () = match k with
| Global, _, _ -> ()
| Local, _, _ | Discharge, _, _ ->
- msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
+ Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
str "declared as an axiom.")
in
let () = assumption_message id in
@@ -329,10 +332,11 @@ 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
+ Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
let is_opaque, export_seff, exports = match opaque with
| Vernacexpr.Transparent -> false, true, []
@@ -347,12 +351,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 +369,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
@@ -392,7 +403,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
| Anonymous -> Tactics.intro) (List.rev ids) in
let init_tac,guard = match recguard with
| Some (finite,guard,init_tac) ->
- let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in
+ let rec_tac = rec_tac_initializer finite guard thms snl in
Some (match init_tac with
| None ->
if Flags.is_auto_intros () then
@@ -422,7 +433,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
@@ -442,7 +453,7 @@ let start_proof_com kind thms hook =
let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
let t', imps' = interp_type_evars_impls ~impls env evdref t in
evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
- let ids = List.map pi1 ctx in
+ let ids = List.map get_name ctx in
(compute_proof_name (pi1 kind) sopt,
(nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
(ids, imps @ lift_implicits (List.length ids) imps'),
@@ -494,7 +505,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 +515,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 ca6af9a3fa..f751598f04 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/spawned.ml b/stm/spawned.ml
index c6df872679..2eae6f5e24 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -13,19 +13,6 @@ let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
type chandescr = AnonPipe | Socket of string * int * int
-let handshake cin cout =
- try
- match input_value cin with
- | Hello(v, pid) when v = proto_version ->
- prerr_endline (Printf.sprintf "Handshake with %d OK" pid);
- output_value cout (Hello (proto_version,Unix.getpid ())); flush cout
- | _ -> raise (Failure "handshake protocol")
- with
- | Failure s | Invalid_argument s | Sys_error s ->
- pr_err ("Handshake failed: " ^ s); raise (Failure "handshake")
- | End_of_file ->
- pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
-
let open_bin_connection h pr pw =
let open Unix in
let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
diff --git a/stm/stm.ml b/stm/stm.ml
index 95cecb7fe2..e2acb10293 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -18,6 +18,7 @@ open Names
open Util
open Ppvernac
open Vernac_classifier
+open Feedback
module Hooks = struct
@@ -27,28 +28,23 @@ let with_fail, with_fail_hook = Hook.make ()
let state_computed, state_computed_hook = Hook.make
~default:(fun state_id ~in_cache ->
- feedback ~state_id Feedback.Processed) ()
+ feedback ~id:(State state_id) Processed) ()
let state_ready, state_ready_hook = Hook.make
~default:(fun state_id -> ()) ()
let forward_feedback, forward_feedback_hook = Hook.make
~default:(function
- | { Feedback.id = Feedback.Edit edit_id; route; contents } ->
- feedback ~edit_id ~route contents
- | { Feedback.id = Feedback.State state_id; route; contents } ->
- feedback ~state_id ~route contents) ()
+ | { id = id; route; contents } ->
+ feedback ~id:id ~route contents) ()
let parse_error, parse_error_hook = Hook.make
- ~default:(function
- | Feedback.Edit edit_id -> fun loc msg ->
- feedback ~edit_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))
- | Feedback.State state_id -> fun loc msg ->
- feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+ ~default:(fun id loc msg ->
+ feedback ~id (ErrorMsg (loc, Pp.string_of_ppcmds msg))) ()
let execution_error, execution_error_hook = Hook.make
~default:(fun state_id loc msg ->
- feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+ feedback ~id:(State state_id) (ErrorMsg (loc, Pp.string_of_ppcmds msg))) ()
let unreachable_state, unreachable_state_hook = Hook.make
~default:(fun _ _ -> ()) ()
@@ -83,6 +79,8 @@ let async_proofs_workers_extra_env = ref [||]
type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
let pr_ast { expr } = pr_vernac expr
+let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+
(* Commands piercing opaque *)
let may_pierce_opaque = function
| { expr = VernacPrint (PrintName _) } -> true
@@ -101,14 +99,14 @@ 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 (fun () -> "ignoring " ^ string_of_ppcmds(pr_vernac expr))
+ prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
end else begin
- set_id_for_feedback ?route (Feedback.State id);
+ set_id_for_feedback ?route (State id);
Aux_file.record_in_aux_set_at loc;
- prerr_endline (fun () -> "interpreting " ^ string_of_ppcmds(pr_vernac expr));
+ prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
with e ->
let e = Errors.push e in
@@ -118,8 +116,8 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } =
(* Wrapper for Vernac.parse_sentence to set the feedback id *)
let vernac_parse ?newtip ?route eid s =
let feedback_id =
- if Option.is_empty newtip then Feedback.Edit eid
- else Feedback.State (Option.get newtip) in
+ if Option.is_empty newtip then Edit eid
+ else State (Option.get newtip) in
set_id_for_feedback ?route feedback_id;
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
Flags.with_option Flags.we_are_parsing (fun () ->
@@ -136,7 +134,7 @@ let vernac_parse ?newtip ?route eid s =
let pr_open_cur_subgoals () =
try Printer.pr_open_subgoals ()
- with Proof_global.NoCurrentProof -> str""
+ with Proof_global.NoCurrentProof -> Pp.str ""
let update_global_env () =
if Proof_global.there_are_pending_proofs () then
@@ -154,7 +152,7 @@ type branch_type =
proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ]
type cmd_t = {
ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
- ceff : bool; (* is a side-effecting command *)
+ ceff : bool; (* is a side-effecting command in the middle of a proof *)
cast : ast;
cids : Id.t list;
cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] }
@@ -186,7 +184,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;
@@ -228,7 +226,7 @@ end = struct (* {{{ *)
let find_proof_at_depth vcs pl =
try List.find (function
| _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
- | _, { Vcs_.kind = `Edit _ } -> anomaly(str"find_proof_at_depth")
+ | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
| _ -> false)
(List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
with Not_found -> failwith "find_proof_at_depth"
@@ -236,9 +234,9 @@ end = struct (* {{{ *)
exception Expired
let visit vcs id =
if Stateid.equal id Stateid.initial then
- anomaly(str"Visiting the initial state id")
+ anomaly(Pp.str "Visiting the initial state id")
else if Stateid.equal id Stateid.dummy then
- anomaly(str"Visiting the dummy state id")
+ anomaly(Pp.str "Visiting the dummy state id")
else
try
match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
@@ -254,7 +252,7 @@ end = struct (* {{{ *)
| [n, Sideff (Some x); p, Noop]
| [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n }
| [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n}
- | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id))
+ | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id))
with Not_found -> raise Expired
end (* }}} *)
@@ -313,7 +311,7 @@ module VCS : sig
val proof_nesting : unit -> int
val checkout_shallowest_proof_branch : unit -> unit
- val propagate_sideff : ast option -> unit
+ val propagate_sideff : replay:ast option -> unit
val gc : unit -> unit
@@ -337,10 +335,10 @@ end = struct (* {{{ *)
"stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
let string_of_transaction = function
| Cmd { cast = t } | Fork (t, _,_,_) ->
- (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+ (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
| Sideff (Some t) ->
sprintf "Sideff(%s)"
- (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+ (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
| Sideff None -> "EnvChange"
| Noop -> " "
| Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
@@ -482,10 +480,10 @@ end = struct (* {{{ *)
Proof_global.activate_proof_mode mode
with Failure _ ->
checkout Branch.master;
- Proof_global.disactivate_proof_mode "Classic"
+ Proof_global.disactivate_current_proof_mode ()
(* copies the transaction on every open branch *)
- let propagate_sideff t =
+ let propagate_sideff ~replay:t =
List.iter (fun b ->
checkout b;
let id = new_node () in
@@ -649,10 +647,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 =
@@ -739,7 +736,7 @@ end = struct (* {{{ *)
let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
f id
=
- feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id);
+ feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id);
let str_id = Stateid.to_string id in
if is_cached id && not redefine then
anomaly (str"defining state "++str str_id++str" twice");
@@ -1061,7 +1058,7 @@ end = struct (* {{{ *)
List.iter (fun (id,s) -> State.assign id s) l; `End
| `Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop },
RespBuiltProof (pl, time) ->
- feedback (Feedback.InProgress ~-1);
+ feedback (InProgress ~-1);
t_assign (`Val pl);
record_pb_time t_name t_loc time;
if !Flags.async_proofs_full || t_drop
@@ -1069,7 +1066,7 @@ end = struct (* {{{ *)
else `End
| `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
- feedback (Feedback.InProgress ~-1);
+ feedback (InProgress ~-1);
let info = Stateid.add ~valid Exninfo.null e_error_at in
let e = (RemoteException e_msg, info) in
t_assign (`Exn e);
@@ -1085,7 +1082,7 @@ end = struct (* {{{ *)
let e = (RemoteException (strbrk s), info) in
t_assign (`Exn e);
Hooks.(call execution_error start Loc.ghost (strbrk s));
- feedback (Feedback.InProgress ~-1)
+ feedback (InProgress ~-1)
let build_proof_here ~drop_pt (id,valid) loc eop =
Future.create (State.exn_on id ~valid) (fun () ->
@@ -1096,7 +1093,7 @@ end = struct (* {{{ *)
Aux_file.record_in_aux_at loc "proof_build_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
let p = Proof_global.return_proof ~allow_partial:drop_pt () in
- if drop_pt then Pp.feedback ~state_id:id Feedback.Complete;
+ if drop_pt then feedback ~id:(State id) Complete;
p)
let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
@@ -1141,9 +1138,10 @@ end = struct (* {{{ *)
let perform_states query =
if query = [] then [] else
- let is_tac = function
- | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true
- | _ -> false in
+ let is_tac e = match classify_vernac e with
+ | VtProofStep _, _ -> true
+ | _ -> false
+ in
let initial =
let rec aux id =
try match VCS.visit id with { next } -> aux next
@@ -1188,7 +1186,7 @@ end = struct (* {{{ *)
"The system state could not be sent to the worker process. "^
"Falling back to local, lazy, evaluation."));
t_assign(`Comp(build_proof_here ~drop_pt t_exn_info t_loc t_stop));
- feedback (Feedback.InProgress ~-1)
+ feedback (InProgress ~-1)
end (* }}} *)
@@ -1268,7 +1266,7 @@ end = struct (* {{{ *)
let (e, info) = Errors.push e in
(try match Stateid.get info with
| None ->
- pperrnl (
+ msg_error (
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
| Some (_, cur) ->
@@ -1278,12 +1276,12 @@ end = struct (* {{{ *)
| { step = `Qed ( { qast = { loc } }, _) }
| { step = `Sideff (`Ast ( { loc }, _)) } ->
let start, stop = Loc.unloc loc in
- pperrnl (
+ msg_error (
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
str ": chars " ++ int start ++ str "-" ++ int stop ++
spc () ++ iprint (e, info))
| _ ->
- pperrnl (
+ msg_error (
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
with e ->
@@ -1343,7 +1341,6 @@ end = struct (* {{{ *)
let set_perspective idl =
ProofTask.set_perspective idl;
TaskQueue.broadcast (Option.get !queue);
- let open Stateid in
let open ProofTask in
let overlap s1 s2 =
List.exists (fun x -> CList.mem_f Stateid.equal x s2) s1 in
@@ -1377,7 +1374,7 @@ end = struct (* {{{ *)
else
let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
let t_uuid = Future.uuid f in
- feedback (Feedback.InProgress 1);
+ feedback (InProgress 1);
let task = ProofTask.(BuildProof {
t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt;
t_loc = loc; t_uuid; t_name = pname;
@@ -1414,7 +1411,7 @@ and TacTask : sig
t_state : Stateid.t;
t_state_fb : Stateid.t;
t_assign : output Future.assignement -> unit;
- t_ast : ast;
+ t_ast : int * ast;
t_goal : Goal.goal;
t_kill : unit -> unit;
t_name : string }
@@ -1431,7 +1428,7 @@ end = struct (* {{{ *)
t_state : Stateid.t;
t_state_fb : Stateid.t;
t_assign : output Future.assignement -> unit;
- t_ast : ast;
+ t_ast : int * ast;
t_goal : Goal.goal;
t_kill : unit -> unit;
t_name : string }
@@ -1440,7 +1437,7 @@ end = struct (* {{{ *)
r_state : Stateid.t;
r_state_fb : Stateid.t;
r_document : VCS.vcs option;
- r_ast : ast;
+ r_ast : int * ast;
r_goal : Goal.goal;
r_name : string }
@@ -1484,6 +1481,9 @@ end = struct (* {{{ *)
| Some { t_kill } -> t_kill ()
| _ -> ()
+ let command_focus = Proof.new_focus_kind ()
+ let focus_cond = Proof.no_cond command_focus
+
let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
Option.iter VCS.restore vcs;
try
@@ -1493,15 +1493,15 @@ end = struct (* {{{ *)
let g = Evd.find sigma0 r_goal in
if not (
Evarutil.is_ground_term sigma0 Evd.(evar_concl g) &&
- List.for_all (fun (_,bo,ty) ->
- Evarutil.is_ground_term sigma0 ty &&
- Option.cata (Evarutil.is_ground_term sigma0) true bo)
- Evd.(evar_context g))
+ List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
+ Evd.(evar_context g))
then
Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^
"goals only"))
else begin
- vernac_interp r_state_fb r_ast;
+ let (i, ast) = r_ast in
+ Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
+ vernac_interp r_state_fb ast;
let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
match Evd.(evar_body (find sigma r_goal)) with
| Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
@@ -1530,12 +1530,11 @@ end = struct (* {{{ *)
module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } =
- let e, etac, time, fail =
+ let e, 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
+ | _ -> e, time, fail in find false false e in
Hooks.call Hooks.with_fail fail (fun () ->
(if time then System.with_time false else (fun x -> x)) (fun () ->
ignore(TaskQueue.with_n_workers nworkers (fun queue ->
@@ -1547,8 +1546,7 @@ end = struct (* {{{ *)
Future.create_delegate
~name:(Printf.sprintf "subgoal %d" i)
(State.exn_on id ~valid:safe_id) in
- let t_ast =
- { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
+ let t_ast = (i, { verbose; loc; expr = e }) in
let t_name = Goal.uid g in
TaskQueue.enqueue_task queue
({ t_state = safe_id; t_state_fb = id;
@@ -1623,11 +1621,11 @@ end = struct (* {{{ *)
Reach.known_state ~cache:`No r_where;
try
vernac_interp r_for { r_what with verbose = true };
- feedback ~state_id:r_for Feedback.Processed
+ feedback ~id:(State r_for) Processed
with e when Errors.noncritical e ->
let e = Errors.push e in
let msg = string_of_ppcmds (iprint e) in
- feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
+ feedback ~id:(State r_for) (ErrorMsg (Loc.ghost, msg))
let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
@@ -1648,7 +1646,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))
@@ -1895,7 +1893,7 @@ let known_state ?(redefine_qed=false) ~cache id =
if not delegate then ignore(Future.compute fp);
reach view.next;
vernac_interp id ~proof x;
- feedback ~state_id:id Feedback.Incomplete
+ feedback ~id:(State id) Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
Proof_global.discard_all ()
@@ -2032,7 +2030,6 @@ let check_task name (tasks,rcbackup) i =
let vcs = VCS.backup () in
try
let rc = Future.purify (Slaves.check_task name tasks) i in
- pperr_flush ();
VCS.restore vcs;
rc
with e when Errors.noncritical e -> VCS.restore vcs; false
@@ -2042,7 +2039,6 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
let finish_task u (_,_,i) =
let vcs = VCS.backup () in
let u = Future.purify (Slaves.finish_task name u d p t) i in
- pperr_flush ();
VCS.restore vcs;
u in
try
@@ -2050,7 +2046,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
(u,a,true), p
with e ->
let e = Errors.push e in
- pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
+ msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
exit 1
let merge_proof_branch ?valid ?id qast keep brname =
@@ -2126,7 +2122,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
let head = VCS.current_branch () in
VCS.checkout head;
let rc = begin
- prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c);
+ prerr_endline (fun () ->
+ " classified as: " ^ string_of_vernac_classification c);
match c with
(* PG stuff *)
| VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
@@ -2192,7 +2189,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
may_pierce_opaque x
then `SkipQueue
else `MainQueue in
- VCS.commit id (Cmd {ctac=false;ceff=false;cast = x; cids = []; cqueue = queue });
+ VCS.commit id (Cmd {
+ ctac=false;ceff=false;cast = x; cids = []; cqueue = queue });
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtQuery (false,_), VtLater ->
anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
@@ -2215,7 +2213,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
anomaly(str"VtProofMode must be executed VtNow")
| VtProofMode mode, VtNow ->
let id = VCS.new_node ~id:newtip () in
- VCS.commit id (Cmd {ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue});
+ VCS.commit id (Cmd {
+ ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue});
List.iter
(fun bn -> match VCS.get_branch bn with
| { VCS.root; kind = `Master; pos } -> ()
@@ -2233,7 +2232,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
| VtProofStep paral, w ->
let id = VCS.new_node ~id:newtip () in
let queue = if paral then `TacQueue (ref false) else `MainQueue in
- VCS.commit id (Cmd {ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
+ VCS.commit id (Cmd {
+ ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
Backtrack.record (); if w == VtNow then finish (); `Ok
| VtQed keep, w ->
let valid = if tty then Some(VCS.get_branch_pos head) else None in
@@ -2247,20 +2247,23 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
vernac_interp (VCS.get_branch_pos head) x; `Ok
| VtSideff l, w ->
- let ceff_in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
+ let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
let id = VCS.new_node ~id:newtip () in
VCS.checkout VCS.Branch.master;
+ VCS.commit id (Cmd {
+ ctac=false;ceff=in_proof;cast=x;cids=l;cqueue=`MainQueue });
+ (* We can't replay a Definition since universes may be differently
+ * inferred. This holds in Coq >= 8.5 *)
let replay = match x.expr with
| VernacDefinition(_, _, DefineBody _) -> None
- | _ -> Some x
- in
- VCS.commit id (Cmd {ctac=false;ceff=ceff_in_proof;cast=x;cids=l;cqueue=`MainQueue});
- VCS.propagate_sideff replay;
+ | _ -> Some x in
+ VCS.propagate_sideff ~replay;
VCS.checkout_shallowest_proof_branch ();
Backtrack.record (); if w == VtNow then finish (); `Ok
(* Unknown: we execute it, check for open goals and propagate sideeff *)
| VtUnknown, VtNow ->
+ let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
let id = VCS.new_node ~id:newtip () in
let head_id = VCS.get_branch_pos head in
Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *)
@@ -2270,21 +2273,23 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
Reach.known_state ~cache:(interactive ()) mid;
vernac_interp id x;
(* Vernac x may or may not start a proof *)
- if VCS.Branch.equal head VCS.Branch.master &&
- Proof_global.there_are_pending_proofs ()
- then begin
+ if not in_proof && Proof_global.there_are_pending_proofs () then
+ begin
let bname = VCS.mk_branch_name x in
let opacity_of_produced_term =
match x.expr with
+ (* This AST is ambiguous, hence we check it dynamically *)
| VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
| _ -> Doesn'tGuaranteeOpacity in
VCS.commit id (Fork (x,bname,opacity_of_produced_term,[]));
- VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
- Proof_global.activate_proof_mode "Classic";
+ let proof_mode = default_proof_mode () in
+ VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1));
+ Proof_global.activate_proof_mode proof_mode;
end else begin
- VCS.commit id (Cmd {ctac = false; ceff = true;
- cast = x; cids = []; cqueue = `MainQueue});
- VCS.propagate_sideff (Some x);
+ VCS.commit id (Cmd {
+ ctac=false;ceff=in_proof;cast=x;cids=[];cqueue=`MainQueue });
+ (* We hope it can be replayed, but we can't really know *)
+ VCS.propagate_sideff ~replay:(Some x);
VCS.checkout_shallowest_proof_branch ();
end in
State.define ~safe_id:head_id ~cache:`Yes step id;
@@ -2309,18 +2314,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
let e = Errors.push e in
handle_failure e vcs tty
-let print_ast id =
- try
- match VCS.visit id with
- | { step = `Cmd { cast = { loc; expr } } }
- | { step = `Fork (({ loc; expr }, _, _, _), _) }
- | { step = `Qed ({ qast = { loc; expr } }, _) } ->
- let xml =
- try Texmacspp.tmpp expr loc
- with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e) in
- xml;
- | _ -> Xml_datatype.PCData "ERROR"
- with _ -> Xml_datatype.PCData "ERROR"
+let get_ast id =
+ match VCS.visit id with
+ | { step = `Cmd { cast = { loc; expr } } }
+ | { step = `Fork (({ loc; expr }, _, _, _), _) }
+ | { step = `Qed ({ qast = { loc; expr } }, _) } ->
+ Some (expr, loc)
+ | _ -> None
let stop_worker n = Slaves.cancel_worker n
@@ -2346,7 +2346,7 @@ type focus = {
tip : Stateid.t
}
-let query ~at ?(report_with=(Stateid.dummy,Feedback.default_route)) s =
+let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
Future.purify (fun s ->
if Stateid.equal at Stateid.dummy then finish ()
else Reach.known_state ~cache:`Yes at;
diff --git a/stm/stm.mli b/stm/stm.mli
index ad89eb71f3..6ffe0beb44 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -9,6 +9,7 @@
open Vernacexpr
open Names
open Feedback
+open Loc
(** state-transaction-machine interface *)
@@ -19,7 +20,7 @@ open Feedback
The sentence [s] is parsed in the state [ontop].
If [newtip] is provided, then the returned state id is guaranteed to be
[newtip] *)
-val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr -> unit) ->
+val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(vernac_expr located -> unit) ->
bool -> edit_id -> string ->
Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
@@ -75,7 +76,9 @@ val get_current_state : unit -> Stateid.t
(* Misc *)
val init : unit -> unit
-val print_ast : Stateid.t -> Xml_datatype.xml
+
+(* This returns the node at that position *)
+val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option
(* Filename *)
val set_compilation_hints : string -> unit
@@ -124,9 +127,9 @@ val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ]
(** read-eval-print loop compatible interface ****************************** **)
(* Adds a new line to the document. It replaces the core of Vernac.interp.
- [finish] is called as the last bit of this function is the system
+ [finish] is called as the last bit of this function if the system
is running interactively (-emacs or coqtop). *)
-val interp : bool -> located_vernac_expr -> unit
+val interp : bool -> vernac_expr located -> unit
(* Queries for backward compatibility *)
val current_proof_depth : unit -> int
@@ -134,7 +137,7 @@ val get_all_proof_names : unit -> Id.t list
val get_current_proof_name : unit -> Id.t option
val show_script : ?proof:Proof_global.closed_proof -> unit -> unit
-(** Reverse dependency hooks *)
+(* Hooks to be set by other Coq components in order to break file cycles *)
val process_error_hook : Future.fix_exn Hook.t
val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 92b3a869a9..bd792b01f6 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -7,6 +7,5 @@ Vernac_classifier
Lemmas
CoqworkmgrApi
AsyncTaskQueue
-Texmacspp
Stm
Vio_checking
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
deleted file mode 100644
index 85cb45708a..0000000000
--- a/stm/texmacspp.ml
+++ /dev/null
@@ -1,770 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-open Constrexpr
-open Names
-open Misctypes
-open Bigint
-open Decl_kinds
-open Extend
-open Libnames
-
-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)
-
-let get_fst_attr_in_xml_list attr xml_list =
- let attrs_list =
- List.map (function
- | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs)
- | _ -> [])
- xml_list in
- match List.flatten attrs_list with
- | [] -> (attr, "")
- | l -> (List.hd l)
-
-let backstep_loc xmllist =
- let start_att = get_fst_attr_in_xml_list "begin" xmllist in
- let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in
- [start_att ; stop_att]
-
-let compare_begin_att xml1 xml2 =
- let att1 = get_fst_attr_in_xml_list "begin" [xml1] in
- let att2 = get_fst_attr_in_xml_list "begin" [xml2] in
- match att1, att2 with
- | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0
- | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1
- | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
- | _ -> 0
-
-let xmlBeginSection loc name = xmlWithLoc loc "beginsection" ["name", name] []
-
-let xmlEndSegment loc name = xmlWithLoc loc "endsegment" ["name", name] []
-
-let xmlThm typ name loc xml =
- xmlWithLoc loc "theorem" ["type", typ; "name", name] xml
-
-let xmlDef typ name loc xml =
- xmlWithLoc loc "definition" ["type", typ; "name", name] xml
-
-let xmlNotation attr name loc xml =
- xmlWithLoc loc "notation" (("name", name) :: attr) xml
-
-let xmlReservedNotation attr name loc =
- xmlWithLoc loc "reservednotation" (("name", name) :: attr) []
-
-let xmlCst name ?(attr=[]) loc =
- xmlWithLoc loc "constant" (("name", name) :: attr) []
-
-let xmlOperator name ?(attr=[]) ?(pprules=[]) loc =
- xmlWithLoc loc "operator"
- (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
-
-let xmlApply loc ?(attr=[]) xml = xmlWithLoc loc "apply" attr xml
-
-let xmlToken loc ?(attr=[]) xml = xmlWithLoc loc "token" attr xml
-
-let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
-
-let xmlReturn ?(attr=[]) xml = Element("return", attr, xml)
-
-let xmlCase xml = Element("case", [], xml)
-
-let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml)
-
-let xmlWith xml = Element("with", [], xml)
-
-let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
-
-let xmlInductive kind loc xml = xmlWithLoc loc "inductive" ["kind",kind] xml
-
-let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
-
-let xmlFixpoint xml = Element("fixpoint", [], xml)
-
-let xmlCheck loc xml = xmlWithLoc loc "check" [] xml
-
-let xmlAssumption kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml
-
-let xmlComment loc xml = xmlWithLoc loc "comment" [] xml
-
-let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr []
-
-let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr []
-
-let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] []
-
-let xmlReference ref =
- let name = Libnames.string_of_reference ref in
- let i, j = Loc.unloc (Libnames.loc_of_reference ref) in
- let b, e = string_of_int i, string_of_int j in
- Element("reference",["name", name; "begin", b; "end", e] ,[])
-
-let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml
-let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml
-
-let xmlAddLoadPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
-let xmlRemoveLoadPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
-let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr
-
-let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml
-
-let xmlScope loc action ?(attr=[]) name xml =
- xmlWithLoc loc "scope" (["name",name;"action",action] @ attr) xml
-
-let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] []
-
-let xmlProof loc xml = xmlWithLoc loc "proof" [] xml
-
-let xmlRawTactic name rtac =
- Element("rawtactic", ["name",name],
- [PCData (Pp.string_of_ppcmds (Pptactic.pr_raw_tactic rtac))])
-
-let xmlSectionSubsetDescr name ssd =
- Element("sectionsubsetdescr",["name",name],
- [PCData (Proof_using.to_string ssd)])
-
-let xmlDeclareMLModule loc s =
- xmlWithLoc loc "declarexmlmodule" []
- (List.map (fun x -> Element("path",["value",x],[])) s)
-
-(* tactics *)
-let xmlLtac loc xml = xmlWithLoc loc "ltac" [] xml
-
-(* toplevel commands *)
-let xmlGallina loc xml = xmlWithLoc loc "gallina" [] xml
-
-let xmlTODO loc x =
- xmlWithLoc loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
-let string_of_name n =
- match n with
- | Anonymous -> "_"
- | Name id -> Id.to_string id
-
-let string_of_glob_sort s =
- match s with
- | GProp -> "Prop"
- | GSet -> "Set"
- | GType _ -> "Type"
-
-let string_of_cast_sort c =
- match c with
- | CastConv _ -> "CastConv"
- | CastVM _ -> "CastVM"
- | CastNative _ -> "CastNative"
- | CastCoerce -> "CastCoerce"
-
-let string_of_case_style s =
- match s with
- | LetStyle -> "Let"
- | IfStyle -> "If"
- | LetPatternStyle -> "LetPattern"
- | MatchStyle -> "Match"
- | RegularStyle -> "Regular"
-
-let attribute_of_syntax_modifier sm =
-match sm with
- | SetItemLevel (sl, NumLevel n) ->
- List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n]
- | SetItemLevel (sl, NextLevel) ->
- List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"]
- | SetLevel i -> ["level", string_of_int i]
- | SetAssoc a ->
- begin match a with
- | NonA -> ["",""]
- | RightA -> ["associativity", "right"]
- | LeftA -> ["associativity", "left"]
- end
- | SetEntryType (s, _) -> ["entrytype", s]
- | SetOnlyParsing v -> ["compat", Flags.pr_version v]
- | SetFormat (system, (loc, s)) ->
- let start, stop = unlock loc in
- ["format-"^system, s; "begin", start; "end", stop]
-
-let string_of_assumption_kind l a many =
- match l, a, many with
- | (Discharge, Logical, true) -> "Hypotheses"
- | (Discharge, Logical, false) -> "Hypothesis"
- | (Discharge, Definitional, true) -> "Variables"
- | (Discharge, Definitional, false) -> "Variable"
- | (Global, Logical, true) -> "Axioms"
- | (Global, Logical, false) -> "Axiom"
- | (Global, Definitional, true) -> "Parameters"
- | (Global, Definitional, false) -> "Parameter"
- | (Local, Logical, true) -> "Local Axioms"
- | (Local, Logical, false) -> "Local Axiom"
- | (Local, Definitional, true) -> "Local Parameters"
- | (Local, Definitional, false) -> "Local Parameter"
- | (Global, Conjectural, _) -> "Conjecture"
- | ((Discharge | Local), Conjectural, _) -> assert false
-
-let rec pp_bindlist bl =
- let tlist =
- List.flatten
- (List.map
- (fun (loc_names, _, e) ->
- let names =
- (List.map
- (fun (loc, name) ->
- xmlCst (string_of_name name) loc) loc_names) in
- match e with
- | CHole _ -> names
- | _ -> names @ [pp_expr e])
- bl) in
- match tlist with
- | [e] -> e
- | l -> xmlTyped l
-and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
- Element ("decl_notation", ["name", s], [pp_expr ce])
-and pp_local_binder lb = (* don't know what it is for now *)
- match lb with
- | LocalRawDef ((_, nam), ce) ->
- let attrs = ["name", string_of_name nam] in
- pp_expr ~attr:attrs ce
- | LocalRawAssum (namll, _, ce) ->
- let ppl =
- List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
- xmlTyped (ppl @ [pp_expr ce])
-and pp_local_decl_expr lde = (* don't know what it is for now *)
- match lde with
- | AssumExpr (_, ce) -> pp_expr ce
- | DefExpr (_, ce, _) -> pp_expr ce
-and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
- (* inductive_expr *)
- let b,e = Loc.unloc l in
- let location = ["begin", string_of_int b; "end", string_of_int e] in
- [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
- begin match cl_or_rdexpr with
- | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel
- | RecordDecl (_, ldewwwl) ->
- List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl
- end @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end @
- (List.map pp_local_binder lbl)
-and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
- let attrs =
- match optid with
- | None -> []
- | Some (loc, id) ->
- let start, stop = unlock loc in
- ["begin", start; "end", stop ; "name", Id.to_string id] in
- let kind, expr =
- match roe with
- | CStructRec -> "struct", []
- | CWfRec e -> "rec", [pp_expr e]
- | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
- | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
- Element ("recursion_order", ["kind", kind] @ attrs, expr)
-and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
- (* fixpoint_expr *)
- let start, stop = unlock loc in
- let id = Id.to_string id in
- [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
- (* fixpoint name *)
- [pp_recursion_order_expr optid roe] @
- (List.map pp_local_binder lbl) @
- [pp_expr ce] @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end
-and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
- (* Nota: it is like fixpoint_expr without (optid, roe)
- * so could be merged if there is no more differences *)
- let start, stop = unlock loc in
- let id = Id.to_string id in
- [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
- (* cofixpoint name *)
- (List.map pp_local_binder lbl) @
- [pp_expr ce] @
- begin match ceo with (* don't know what it is for now *)
- | Some ce -> [pp_expr ce]
- | None -> []
- end
-and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
-and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
-and pp_cases_pattern_expr cpe =
- match cpe with
- | CPatAlias (loc, cpe, id) ->
- xmlApply loc
- (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
- [pp_cases_pattern_expr cpe])
- | CPatCstr (loc, ref, cpel1, cpel2) ->
- xmlApply loc
- (xmlOperator "reference"
- ~attr:["name", Libnames.string_of_reference ref] loc ::
- [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
- Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
- | CPatAtom (loc, optr) ->
- let attrs = match optr with
- | None -> []
- | Some r -> ["name", Libnames.string_of_reference r] in
- xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
- | CPatOr (loc, cpel) ->
- xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
- | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
- xmlApply loc
- (xmlOperator "notation" loc ::
- [xmlOperator n loc;
- Element ("subst", [],
- [Element ("subterms", [],
- List.map pp_cases_pattern_expr subst_constr);
- Element ("recsubterms", [],
- List.map
- (fun (cpel) ->
- Element ("recsubterm", [],
- List.map pp_cases_pattern_expr cpel))
- subst_rec)]);
- Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
- | CPatPrim (loc, tok) -> pp_token loc tok
- | CPatRecord (loc, rcl) ->
- xmlApply loc
- (xmlOperator "record" loc ::
- List.map (fun (r, cpe) ->
- Element ("field",
- ["reference", Libnames.string_of_reference r],
- [pp_cases_pattern_expr cpe]))
- rcl)
- | CPatDelimiters (loc, delim, cpe) ->
- xmlApply loc
- (xmlOperator "delimiter" ~attr:["name", delim] loc ::
- [pp_cases_pattern_expr cpe])
-and pp_case_expr (e, (name, pat)) =
- match name, pat with
- | None, None -> xmlScrutinee [pp_expr e]
- | Some (loc, name), None ->
- let start, stop= unlock loc in
- xmlScrutinee ~attr:["name", string_of_name name;
- "begin", start; "end", stop] [pp_expr e]
- | Some (loc, name), Some p ->
- let start, stop= unlock loc in
- xmlScrutinee ~attr:["name", string_of_name name;
- "begin", start; "end", stop]
- [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
- | None, Some p ->
- xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
-and pp_branch_expr_list bel =
- xmlWith
- (List.map
- (fun (_, cpel, e) ->
- let ppcepl =
- List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
- let ppe = [pp_expr e] in
- xmlCase (ppcepl @ ppe))
- bel)
-and pp_token loc tok =
- let tokstr =
- match tok with
- | String s -> PCData s
- | Numeral n -> PCData (to_string n) in
- xmlToken loc [tokstr]
-and pp_local_binder_list lbl =
- let l = (List.map pp_local_binder lbl) in
- Element ("recurse", (backstep_loc l), l)
-and pp_const_expr_list cel =
- let l = List.map pp_expr cel in
- Element ("recurse", (backstep_loc l), l)
-and pp_expr ?(attr=[]) e =
- match e with
- | CRef (r, _) ->
- xmlCst ~attr
- (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
- | CProdN (loc, bl, e) ->
- xmlApply loc
- (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
- | CApp (loc, (_, hd), args) ->
- xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
- | CAppExpl (loc, (_, r, _), args) ->
- xmlApply ~attr loc
- (xmlCst (Libnames.string_of_reference r)
- (Libnames.loc_of_reference r) :: List.map pp_expr args)
- | CNotation (loc, notation, ([],[],[])) ->
- xmlOperator notation loc
- | CNotation (loc, notation, (args, cell, lbll)) ->
- let fmts = Notation.find_notation_extra_printing_rules notation in
- let oper = xmlOperator notation loc ~pprules:fmts in
- let cels = List.map pp_const_expr_list cell in
- let lbls = List.map pp_local_binder_list lbll in
- let args = List.map pp_expr args in
- xmlApply loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
- | CSort(loc, s) ->
- xmlOperator (string_of_glob_sort s) loc
- | CDelimiters (loc, scope, ce) ->
- xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
- [pp_expr ce])
- | CPrim (loc, tok) -> pp_token loc tok
- | CGeneralization (loc, kind, _, e) ->
- let kind= match kind with
- | Explicit -> "explicit"
- | Implicit -> "implicit" in
- xmlApply loc
- (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e])
- | CCast (loc, e, tc) ->
- begin match tc with
- | CastConv t | CastVM t |CastNative t ->
- xmlApply loc
- (xmlOperator ":" loc ~attr:["kind", (string_of_cast_sort tc)] ::
- [pp_expr e; pp_expr t])
- | CastCoerce ->
- xmlApply loc
- (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] ::
- [pp_expr e])
- end
- | CEvar (loc, ek, cel) ->
- let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
- xmlApply loc
- (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
- ppcel)
- | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
- | CHole (loc, _, _, _) -> xmlCst ~attr "_" loc
- | CIf (loc, test, (_, ret), th, el) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "if" loc ::
- return @ [pp_expr th] @ [pp_expr el])
- | CLetTuple (loc, names, (_, ret), value, body) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "lettuple" loc ::
- return @
- (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
- [pp_expr value; pp_expr body])
- | CCases (loc, sty, ret, cel, bel) ->
- let return = match ret with
- | None -> []
- | Some r -> [xmlReturn [pp_expr r]] in
- xmlApply loc
- (xmlOperator "match" loc ~attr:["style", (string_of_case_style sty)] ::
- (return @
- [Element ("scrutinees", [], List.map pp_case_expr cel)] @
- [pp_branch_expr_list bel]))
- | CRecord (_, _, _) -> assert false
- | CLetIn (loc, (varloc, var), value, body) ->
- xmlApply loc
- (xmlOperator "let" loc ::
- [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
- | CLambdaN (loc, bl, e) ->
- xmlApply loc
- (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
- | CCoFix (_, _, _) -> assert false
- | CFix (loc, lid, fel) ->
- xmlApply loc
- (xmlOperator "fix" loc ::
- List.flatten (List.map
- (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
- fel))
-
-let pp_comment (c) =
- match c with
- | CommentConstr e -> [pp_expr e]
- | CommentString s -> [Element ("string", [], [PCData s])]
- | CommentInt i -> [PCData (string_of_int i)]
-
-let rec tmpp v loc =
- match v with
- (* Control *)
- | VernacLoad (verbose,f) ->
- xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
- | VernacTime l ->
- xmlApply loc (Element("time",[],[]) ::
- List.map (fun(loc,e) ->tmpp e loc) l)
- | VernacRedirect (s, l) ->
- xmlApply loc (Element("redirect",["path", s],[]) ::
- List.map (fun(loc,e) ->tmpp e loc) l)
- | VernacTimeout (s,e) ->
- xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
- [tmpp e loc])
- | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
- | VernacError _ -> xmlWithLoc loc "error" [] []
-
- (* Syntax *)
- | VernacTacticNotation _ as x ->
- xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- | VernacSyntaxExtension (_, ((_, name), sml)) ->
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- xmlReservedNotation attrs name loc
-
- | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
- | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
- | VernacDelimiters (name,Some tag) ->
- xmlScope loc "delimit" name ~attr:["delimiter",tag] []
- | VernacDelimiters (name,None) ->
- xmlScope loc "undelimit" name ~attr:[] []
- | VernacBindScope (name,l) ->
- xmlScope loc "bind" name
- (List.map (function
- | ByNotation(loc,name,None) -> xmlNotation [] name loc []
- | ByNotation(loc,name,Some d) ->
- xmlNotation ["delimiter",d] name loc []
- | AN ref -> xmlReference ref) l)
- | VernacInfix (_,((_,name),sml),ce,sn) ->
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- let sc_attr =
- match sn with
- | Some scope -> ["scope", scope]
- | None -> [] in
- xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
- | VernacNotation (_, ce, (lstr, sml), sn) ->
- let name = snd lstr in
- let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
- let sc_attr =
- match sn with
- | Some scope -> ["scope", scope]
- | None -> [] in
- xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
- | VernacNotationAddFormat _ as x -> xmlTODO loc x
- | VernacUniverse _
- | VernacConstraint _
- | VernacPolymorphic (_, _) as x -> xmlTODO loc x
- (* Gallina *)
- | VernacDefinition (ldk, ((_,id),_), de) ->
- let l, dk =
- match ldk with
- | Some l, dk -> (l, dk)
- | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *)
- let e =
- match de with
- | ProveBody (_, ce) -> ce
- | DefineBody (_, Some _, ce, None) -> ce
- | DefineBody (_, None , ce, None) -> ce
- | DefineBody (_, Some _, ce, Some _) -> ce
- | DefineBody (_, None , ce, Some _) -> ce in
- let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
- let str_id = Id.to_string id in
- (xmlDef str_dk str_id loc [pp_expr e])
- | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
- let str_tk = Kindops.string_of_theorem_kind tk in
- let str_id = Id.to_string id in
- (xmlThm str_tk str_id loc [pp_expr statement])
- | VernacStartTheoremProof _ as x -> xmlTODO loc x
- | VernacEndProof pe ->
- begin
- match pe with
- | Admitted -> xmlQed loc
- | Proved (_, Some ((_, id), Some tk)) ->
- let nam = Id.to_string id in
- let typ = Kindops.string_of_theorem_kind tk in
- xmlQed ~attr:["name", nam; "type", typ] loc
- | Proved (_, Some ((_, id), None)) ->
- let nam = Id.to_string id in
- xmlQed ~attr:["name", nam] loc
- | Proved _ -> xmlQed loc
- end
- | VernacExactProof _ as x -> xmlTODO loc x
- | VernacAssumption ((l, a), _, sbwcl) ->
- let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
- let many =
- List.length (List.flatten (List.map fst binders)) > 1 in
- let exprs =
- List.flatten (List.map pp_simple_binder binders) in
- let l = match l with Some x -> x | None -> Decl_kinds.Global in
- let kind = string_of_assumption_kind l a many in
- xmlAssumption kind loc exprs
- | VernacInductive (_, _, iednll) ->
- let kind =
- let (_, _, _, k, _),_ = List.hd iednll in
- begin
- match k with
- | Record -> "Record"
- | Structure -> "Structure"
- | Inductive_kw -> "Inductive"
- | CoInductive -> "CoInductive"
- | Class _ -> "Class"
- | Variant -> "Variant"
- end in
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (ie, dnl) -> (pp_inductive_expr ie) @
- (List.map pp_decl_notation dnl)) iednll) in
- xmlInductive kind loc exprs
- | VernacFixpoint (_, fednll) ->
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
- (List.map pp_decl_notation dnl)) fednll) in
- xmlFixpoint exprs
- | VernacCoFixpoint (_, cfednll) ->
- (* Nota: it is like VernacFixpoint without so could be merged *)
- let exprs =
- List.flatten (* should probably not be flattened *)
- (List.map
- (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
- (List.map pp_decl_notation dnl)) cfednll) in
- xmlCoFixpoint exprs
- | VernacScheme _ as x -> xmlTODO loc x
- | VernacCombinedScheme _ as x -> xmlTODO loc x
-
- (* Gallina extensions *)
- | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
- | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
- | VernacNameSectionHypSet _ as x -> xmlTODO loc x
- | VernacRequire (from, import, l) ->
- let import = match import with
- | None -> []
- | Some true -> ["export","true"]
- | Some false -> ["import","true"]
- in
- let from = match from with
- | None -> []
- | Some r -> ["from", Libnames.string_of_reference r]
- in
- xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
- xmlReference ref) l)
- | VernacImport (true,l) ->
- xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
- xmlReference ref) l)
- | VernacImport (false,l) ->
- xmlImport loc (List.map (fun ref ->
- xmlReference ref) l)
- | VernacCanonical r ->
- let attr =
- match r with
- | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
- | AN (Ident (_, id)) -> ["id", Id.to_string id]
- | ByNotation (_, s, _) -> ["notation", s] in
- xmlCanonicalStructure attr loc
- | VernacCoercion _ as x -> xmlTODO loc x
- | VernacIdentityCoercion _ as x -> xmlTODO loc x
-
- (* Type classes *)
- | VernacInstance _ as x -> xmlTODO loc x
-
- | VernacContext _ as x -> xmlTODO loc x
-
- | VernacDeclareInstances _ as x -> xmlTODO loc x
-
- | VernacDeclareClass _ as x -> xmlTODO loc x
-
- (* Modules and Module Types *)
- | VernacDeclareModule _ as x -> xmlTODO loc x
- | VernacDefineModule _ as x -> xmlTODO loc x
- | VernacDeclareModuleType _ as x -> xmlTODO loc x
- | VernacInclude _ as x -> xmlTODO loc x
-
- (* Solving *)
-
- | (VernacSolve _ | VernacSolveExistential _) as x ->
- xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- (* Auxiliary file and library management *)
- | VernacAddLoadPath (recf,name,None) ->
- xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] []
- | VernacAddLoadPath (recf,name,Some dp) ->
- xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name]
- [PCData (Names.DirPath.to_string dp)]
- | VernacRemoveLoadPath name -> xmlRemoveLoadPath loc ~attr:["path",name] []
- | VernacAddMLPath (recf,name) ->
- xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] []
- | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl
- | VernacChdir _ as x -> xmlTODO loc x
-
- (* State management *)
- | VernacWriteState _ as x -> xmlTODO loc x
- | VernacRestoreState _ as x -> xmlTODO loc x
-
- (* Resetting *)
- | VernacResetName _ as x -> xmlTODO loc x
- | VernacResetInitial as x -> xmlTODO loc x
- | VernacBack _ as x -> xmlTODO loc x
- | VernacBackTo _ -> PCData "VernacBackTo"
-
- (* Commands *)
- | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x
- | VernacCreateHintDb _ as x -> xmlTODO loc x
- | VernacRemoveHints _ as x -> xmlTODO loc x
- | VernacHints _ as x -> xmlTODO loc x
- | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
- let name = Id.to_string name in
- let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
- xmlNotation attrs name loc [pp_expr ce]
- | VernacDeclareImplicits _ as x -> xmlTODO loc x
- | VernacArguments _ as x -> xmlTODO loc x
- | VernacArgumentsScope _ as x -> xmlTODO loc x
- | VernacReserve _ as x -> xmlTODO loc x
- | VernacGeneralizable _ as x -> xmlTODO loc x
- | VernacSetOpacity _ as x -> xmlTODO loc x
- | VernacSetStrategy _ as x -> xmlTODO loc x
- | VernacUnsetOption _ as x -> xmlTODO loc x
- | VernacSetOption _ as x -> xmlTODO loc x
- | VernacAddOption _ as x -> xmlTODO loc x
- | VernacRemoveOption _ as x -> xmlTODO loc x
- | VernacMemOption _ as x -> xmlTODO loc x
- | VernacPrintOption _ as x -> xmlTODO loc x
- | VernacCheckMayEval (_,_,e) -> xmlCheck loc [pp_expr e]
- | VernacGlobalCheck _ as x -> xmlTODO loc x
- | VernacDeclareReduction _ as x -> xmlTODO loc x
- | VernacPrint _ as x -> xmlTODO loc x
- | VernacSearch _ as x -> xmlTODO loc x
- | VernacLocate _ as x -> xmlTODO loc x
- | 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
-
- (* Proof management *)
- | VernacGoal _ as x -> xmlTODO loc x
- | VernacAbort _ as x -> xmlTODO loc x
- | VernacAbortAll -> PCData "VernacAbortAll"
- | VernacRestart as x -> xmlTODO loc x
- | VernacUndo _ as x -> xmlTODO loc x
- | VernacUndoTo _ as x -> xmlTODO loc x
- | VernacBacktrack _ as x -> xmlTODO loc x
- | VernacFocus _ as x -> xmlTODO loc x
- | VernacUnfocus as x -> xmlTODO loc x
- | VernacUnfocused as x -> xmlTODO loc x
- | VernacBullet _ as x -> xmlTODO loc x
- | VernacSubproof _ as x -> xmlTODO loc x
- | VernacEndSubproof as x -> xmlTODO loc x
- | VernacShow _ as x -> xmlTODO loc x
- | VernacCheckGuard as x -> xmlTODO loc x
- | VernacProof (tac,using) ->
- let tac = Option.map (xmlRawTactic "closingtactic") tac in
- let using = Option.map (xmlSectionSubsetDescr "using") using in
- xmlProof loc (Option.List.(cons tac (cons using [])))
- | VernacProofMode name -> xmlProofMode loc name
-
- (* Toplevel control *)
- | VernacToplevelControl _ as x -> xmlTODO loc x
-
- (* For extension *)
- | VernacExtend _ as x ->
- xmlExtend loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
-
- (* Flags *)
- | VernacProgram e -> xmlApply loc (Element("program",[],[]) :: [tmpp e loc])
- | VernacLocal (b,e) ->
- xmlApply loc (Element("local",["flag",string_of_bool b],[]) ::
- [tmpp e loc])
-
-let tmpp v loc =
- match tmpp v loc with
- | Element("ltac",_,_) as x -> x
- | xml -> xmlGallina loc [xml]
diff --git a/stm/texmacspp.mli b/stm/texmacspp.mli
deleted file mode 100644
index 858847fb6a..0000000000
--- a/stm/texmacspp.mli
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-open Vernacexpr
-
-val tmpp : vernac_expr -> Loc.t -> xml
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index edb54ece40..b1df3c9ca6 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -10,6 +10,8 @@ open Vernacexpr
open Errors
open Pp
+let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
+
let string_of_in_script b = if b then " (inside script)" else ""
let string_of_vernac_type = function
@@ -60,7 +62,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 +88,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 _
@@ -102,12 +104,10 @@ let rec classify_vernac e =
| VernacCheckMayEval _ ->
VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
(* ProofStep *)
- | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater
| VernacProof _
| VernacBullet _
| VernacFocus _ | VernacUnfocus
| VernacSubproof _ | VernacEndSubproof
- | VernacSolve _
| VernacCheckGuard
| VernacUnfocused
| VernacSolveExistential _ -> VtProofStep false, VtLater
@@ -117,27 +117,27 @@ let rec classify_vernac e =
(* StartProof *)
| VernacDefinition (
(Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
- VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
+ VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
| VernacDefinition (_,((_,i),_),ProveBody _) ->
- VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
+ VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
| VernacStartTheoremProof (_,l,_) ->
let ids =
CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
- VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
- | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
+ VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
+ | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater
| VernacFixpoint (_,l) ->
let ids, open_proof =
List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
- then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+ then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
| VernacCoFixpoint (_,l) ->
let ids, open_proof =
List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
- then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+ then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
(* Sideff: apply to all open branches. usually run on master only *)
| VernacAssumption (_,_,l) ->
@@ -175,11 +175,6 @@ let rec classify_vernac e =
| VernacRegister _
| VernacNameSectionHypSet _
| VernacComments _ -> VtSideff [], VtLater
- | VernacDeclareTacticDefinition (_,l) ->
- let open Libnames in
- VtSideff (List.map (function
- | (Ident (_,r),_,_) -> r
- | (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater
(* Who knows *)
| VernacLoad _ -> VtSideff [], VtNow
(* (Local) Notations have to disappear *)
@@ -195,7 +190,6 @@ let rec classify_vernac e =
| VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
| VernacSyntaxExtension _
| VernacSyntacticDefinition _
- | VernacTacticNotation _
| VernacRequire _ | VernacImport _ | VernacInclude _
| VernacDeclareMLModule _
| VernacContext _ (* TASSI: unsure *)
@@ -208,7 +202,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 +210,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-04 05:32:14 +0000