diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 6 | ||||
| -rw-r--r-- | stm/lemmas.ml | 37 | ||||
| -rw-r--r-- | stm/lemmas.mli | 9 | ||||
| -rw-r--r-- | stm/spawned.ml | 13 | ||||
| -rw-r--r-- | stm/stm.ml | 101 | ||||
| -rw-r--r-- | stm/stm.mli | 5 | ||||
| -rw-r--r-- | stm/texmacspp.ml | 38 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 34 |
8 files changed, 117 insertions, 126 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 8649a14c54..c7faef3333 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 @@ -305,7 +303,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 fb64a10c6c..ce5ef01699 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 @@ -329,7 +332,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 +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 16e54e318e..9120787d1c 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..8f11875b62 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -83,6 +83,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,7 +103,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 (fun () -> "ignoring " ^ string_of_ppcmds(pr_vernac expr)) @@ -154,7 +156,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 +188,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; @@ -313,7 +315,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 @@ -482,10 +484,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 +651,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 = @@ -1141,9 +1142,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 @@ -1343,7 +1345,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 @@ -1414,7 +1415,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 +1432,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 +1441,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 +1485,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 +1497,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 +1534,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 +1550,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; @@ -1648,7 +1650,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)) @@ -2126,7 +2128,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 +2195,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 +2219,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 +2238,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 +2253,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 +2279,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; diff --git a/stm/stm.mli b/stm/stm.mli index ad89eb71f3..4279921b3b 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 ] @@ -126,7 +127,7 @@ val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ] (* 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 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 diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 85cb45708a..d1d6de9ae8 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) @@ -307,7 +304,13 @@ and pp_cases_pattern_expr cpe = xmlApply loc (xmlOperator "alias" ~attr:["name", string_of_id id] loc :: [pp_cases_pattern_expr cpe]) - | CPatCstr (loc, ref, cpel1, cpel2) -> + | CPatCstr (loc, ref, None, cpel2) -> + xmlApply loc + (xmlOperator "reference" + ~attr:["name", Libnames.string_of_reference ref] loc :: + [Element ("impargs", [], []); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatCstr (loc, ref, Some cpel1, cpel2) -> xmlApply loc (xmlOperator "reference" ~attr:["name", Libnames.string_of_reference ref] loc :: @@ -347,7 +350,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 -> @@ -460,7 +463,7 @@ and pp_expr ?(attr=[]) e = (return @ [Element ("scrutinees", [], List.map pp_case_expr cel)] @ [pp_branch_expr_list bel])) - | CRecord (_, _, _) -> assert false + | CRecord (_, _) -> assert false | CLetIn (loc, (varloc, var), value, body) -> xmlApply loc (xmlOperator "let" loc :: @@ -487,12 +490,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]) @@ -500,9 +503,6 @@ let rec tmpp v 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 @@ -513,13 +513,6 @@ let rec tmpp v loc = 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 = @@ -535,6 +528,7 @@ let rec tmpp v loc = | Some scope -> ["scope", scope] | None -> [] in xmlNotation (sc_attr @ attrs) name loc [pp_expr ce] + | VernacBindScope _ as x -> xmlTODO loc x | VernacNotationAddFormat _ as x -> xmlTODO loc x | VernacUniverse _ | VernacConstraint _ @@ -668,7 +662,7 @@ let rec tmpp v loc = (* Solving *) - | (VernacSolve _ | VernacSolveExistential _) as x -> + | (VernacSolveExistential _) as x -> xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] (* Auxiliary file and library management *) @@ -694,7 +688,6 @@ let rec tmpp v loc = | 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 @@ -724,7 +717,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 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 |