diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 8 | ||||
| -rw-r--r-- | stm/stm.ml | 95 | ||||
| -rw-r--r-- | stm/stm.mli | 4 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 12 |
4 files changed, 61 insertions, 58 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index d13763cdec..04f10e7399 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -41,8 +41,8 @@ let simple_goal sigma g gs = let open Evd in let open Evarutil in let evi = Evd.find sigma g in - Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) && - Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) && + Set.is_empty (evars_of_term sigma evi.evar_concl) && + Set.is_empty (evars_of_filtered_evar_info sigma (nf_evar_info sigma evi)) && not (List.exists (Proofview.depends_on sigma g) gs) let is_focused_goal_simple ~doc id = @@ -99,7 +99,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b))) + recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b))) } | `Not -> `Leaks @@ -128,7 +128,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } = `ValidBlock { base_state = id; goals_to_admit = focused; - recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof)) + recovery_command = Some (CAst.make @@ Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof)) } | `Not -> `Leaks diff --git a/stm/stm.ml b/stm/stm.ml index 06bc6e3340..21618bc044 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -121,7 +121,6 @@ let async_proofs_workers_extra_env = ref [||] type aast = { verbose : bool; - loc : Loc.t option; indentation : int; strlen : int; mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *) @@ -1149,12 +1148,12 @@ end (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly reduced... *) -let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t = +let stm_vernac_interp ?proof ?route id st { verbose; expr } : Vernacstate.t = (* The Stm will gain the capability to interpret commmads affecting the whole document state, such as backtrack, etc... so we start to design the stm command interpreter now *) set_id_for_feedback ?route dummy_doc id; - Aux_file.record_in_aux_set_at ?loc (); + Aux_file.record_in_aux_set_at ?loc:expr.CAst.loc (); (* We need to check if a command should be filtered from * vernac_entries, as it cannot handle it. This should go away in * future refactorings. @@ -1175,7 +1174,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t | VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *) | _ -> stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr) + try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st expr with e -> let e = CErrors.push e in Exninfo.iraise Hooks.(call_process_error_once e) @@ -1630,8 +1629,8 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop ~proof:(pobject, terminator) st - { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in + { verbose = false; indentation = 0; strlen = 0; + expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1780,8 +1779,8 @@ end = struct (* {{{ *) (* STATE We use the state resulting from reaching start. *) let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp stop ~proof st - { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }); + { verbose = false; indentation = 0; strlen = 0; + expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }); `OK proof end with e -> @@ -1793,10 +1792,11 @@ end = struct (* {{{ *) spc () ++ iprint (e, info)) | Some (_, cur) -> match VCS.visit cur with - | { step = `Cmd { cast = { loc } } } - | { step = `Fork (( { loc }, _, _, _), _) } - | { step = `Qed ( { qast = { loc } }, _) } - | { step = `Sideff (ReplayCommand { loc }, _) } -> + | { step = `Cmd { cast } } + | { step = `Fork (( cast, _, _, _), _) } + | { step = `Qed ( { qast = cast }, _) } + | { step = `Sideff (ReplayCommand cast, _) } -> + let loc = cast.expr.CAst.loc in let start, stop = Option.cata Loc.unloc (0,0) loc in msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ @@ -2073,20 +2073,20 @@ end = struct (* {{{ *) f () let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id - { indentation; verbose; loc; expr = e; strlen } : unit + { indentation; verbose; expr = e; strlen } : unit = let e, time, batch, fail = - let rec find ~time ~batch ~fail = function - | VernacTime (batch,{CAst.v=e}) -> find ~time:true ~batch ~fail e - | VernacRedirect (_,{CAst.v=e}) -> find ~time ~batch ~fail e - | VernacFail {CAst.v=e} -> find ~time ~batch ~fail:true e - | e -> e, time, batch, fail in + let rec find ~time ~batch ~fail v = CAst.with_loc_val (fun ?loc -> function + | VernacTime (batch,e) -> find ~time:true ~batch ~fail e + | VernacRedirect (_,e) -> find ~time ~batch ~fail e + | VernacFail e -> find ~time ~batch ~fail:true e + | e -> CAst.make ?loc e, time, batch, fail) v in find ~time:false ~batch:false ~fail:false e in let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_fail ~st fail (fun () -> (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> - ignore(TaskQueue.with_n_workers nworkers (fun queue -> - PG_compat.with_current_proof (fun _ p -> + TaskQueue.with_n_workers nworkers (fun queue -> + PG_compat.simple_with_current_proof (fun _ p -> let Proof.{goals} = Proof.data p in let open TacTask in let res = CList.map_i (fun i g -> @@ -2094,7 +2094,7 @@ end = struct (* {{{ *) Future.create_delegate ~name:(Printf.sprintf "subgoal %d" i) (State.exn_on id ~valid:safe_id) in - let t_ast = (i, { indentation; verbose; loc; expr = e; strlen }) in + let t_ast = (i, { indentation; verbose; expr = e; strlen }) in let t_name = Goal.uid g in TaskQueue.enqueue_task queue { t_state = safe_id; t_state_fb = id; @@ -2131,7 +2131,8 @@ end = struct (* {{{ *) if solve then Tacticals.New.tclSOLVE [] else tclUNIT () end) in - Proof.run_tactic (Global.env()) assign_tac p)))) ()) + let p,_,() = Proof.run_tactic (Global.env()) assign_tac p in + p))) ()) end (* }}} *) @@ -2243,7 +2244,7 @@ let collect_proof keep cur hd brkind id = let name = function | [] -> no_name | id :: _ -> Names.Id.to_string id in - let loc = (snd cur).loc in + let loc = (snd cur).expr.CAst.loc in let is_defined_expr = function | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true | _ -> false in @@ -2309,7 +2310,7 @@ let collect_proof keep cur hd brkind id = (try let name, hint = name ids, get_hint_ctx loc in let t, v = proof_no_using last in - v.expr <- VernacExpr([], VernacProof(t, Some hint)); + v.expr <- CAst.map (fun _ -> VernacExpr([], VernacProof(t, Some hint))) v.expr; `ASync (parent last,accn,name,delegate name) with Not_found -> let name = name ids in @@ -2412,7 +2413,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = (* STATE: We use an updated state with proof *) let st = Vernacstate.freeze_interp_state ~marshallable:false in Option.iter (fun expr -> ignore(stm_vernac_interp id st { - verbose = true; loc = None; expr; indentation = 0; + verbose = true; expr; indentation = 0; strlen = 0 } )) recovery_command | _ -> assert false @@ -2532,7 +2533,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | `ASync (block_start, nodes, name, delegate) -> (fun () -> let keep' = get_vtkeep keep in let drop_pt = keep' == VtKeepAxiom in - let block_stop, exn_info, loc = eop, (id, eop), x.loc in + let block_stop, exn_info, loc = eop, (id, eop), x.expr.CAst.loc in log_processing_async id name; VCS.create_proof_task_box nodes ~qed:id ~block_start; begin match brinfo, qed.fproof with @@ -2592,7 +2593,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = log_processing_sync id name reason; reach eop; let wall_clock = Unix.gettimeofday () in - record_pb_time name ?loc:x.loc (wall_clock -. !wall_clock_last_fork); + record_pb_time name ?loc:x.expr.CAst.loc (wall_clock -. !wall_clock_last_fork); let proof = match keep with | VtDrop -> None @@ -2614,7 +2615,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id ?proof st x); let wall_clock3 = Unix.gettimeofday () in - Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" + Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time" (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); PG_compat.discard_all () ), true, true @@ -2934,7 +2935,7 @@ let get_allow_nested_proofs = (** [process_transaction] adds a node in the document *) let process_transaction ~doc ?(newtip=Stateid.fresh ()) - ({ verbose; loc; expr } as x) c = + ({ verbose; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in try @@ -3120,11 +3121,11 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) let get_ast ~doc id = match VCS.visit id with - | { step = `Cmd { cast = { loc; expr } } } - | { step = `Fork (({ loc; expr }, _, _, _), _) } - | { step = `Sideff ((ReplayCommand {loc; expr}) , _) } - | { step = `Qed ({ qast = { loc; expr } }, _) } -> - Some (Loc.tag ?loc expr) + | { step = `Cmd { cast = { expr } } } + | { step = `Fork (({ expr }, _, _, _), _) } + | { step = `Sideff ((ReplayCommand { expr }) , _) } + | { step = `Qed ({ qast = { expr } }, _) } -> + Some expr | _ -> None let stop_worker n = Slaves.cancel_worker n @@ -3141,8 +3142,8 @@ let parse_sentence ~doc sid ~entry pa = let ind_len_loc_of_id sid = if Stateid.equal sid Stateid.initial then None else match (VCS.visit sid).step with - | `Cmd { ctac = true; cast = { indentation; strlen; loc } } -> - Some (indentation, strlen, loc) + | `Cmd { ctac = true; cast = { indentation; strlen; expr } } -> + Some (indentation, strlen, expr.CAst.loc) | _ -> None (* the indentation logic works like this: if the beginning of the @@ -3169,7 +3170,8 @@ let compute_indentation ?loc sid = Option.cata (fun loc -> eff_indent, len ) (0, 0) loc -let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = +let add ~doc ~ontop ?newtip verb ast = + let loc = ast.CAst.loc in let cur_tip = VCS.cur_tip () in if not (Stateid.equal ontop cur_tip) then user_err ?loc ~hdr:"Stm.add" @@ -3179,7 +3181,7 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = let indentation, strlen = compute_indentation ?loc ontop in (* XXX: Classifiy vernac should be moved inside process transaction *) let clas = Vernac_classifier.classify_vernac ast in - let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in + let aast = { verbose = verb; indentation; strlen; expr = ast } in match process_transaction ~doc ?newtip aast clas with | `Ok -> doc, VCS.cur_tip (), `NewTip | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ()) @@ -3199,14 +3201,15 @@ let query ~doc ~at ~route s = let rec loop () = match parse_sentence ~doc at ~entry:Pvernac.main_entry s with | None -> () - | Some {CAst.loc; v=ast} -> - let indentation, strlen = compute_indentation ?loc at in - let st = State.get_cached at in - let aast = { - verbose = true; indentation; strlen; - loc; expr = ast } in - ignore(stm_vernac_interp ~route at st aast); - loop () + | Some ast -> + let loc = ast.CAst.loc in + let indentation, strlen = compute_indentation ?loc at in + let st = State.get_cached at in + let aast = { + verbose = true; indentation; strlen; + expr = ast } in + ignore(stm_vernac_interp ~route at st aast); + loop () in loop () ) diff --git a/stm/stm.mli b/stm/stm.mli index 91651e3534..9d2bf56629 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -111,7 +111,7 @@ val parse_sentence : If [newtip] is provided, then the returned state id is guaranteed to be [newtip] *) val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> - bool -> Vernacexpr.vernac_control CAst.t -> + bool -> Vernacexpr.vernac_control -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] (* Returns the proof state before the last tactic that was applied at or before @@ -175,7 +175,7 @@ val get_current_state : doc:doc -> Stateid.t val get_ldir : doc:doc -> Names.DirPath.t (* This returns the node at that position *) -val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option +val get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control option (* Filename *) val set_compilation_hints : string -> unit diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 243b5c333d..4a4c5c94e9 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -137,7 +137,7 @@ let classify_vernac e = | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ CList.map_filter (function - | ((_,AssumExpr({v=Names.Name n},_)),_),_ -> Some n + | AssumExpr({v=Names.Name n},_), _ -> Some n | _ -> None) l) l in VtSideff (List.flatten ids), VtLater | VernacScheme l -> @@ -200,20 +200,20 @@ let classify_vernac e = try Vernacextend.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in - let rec static_control_classifier = function + let rec static_control_classifier v = v |> CAst.with_val (function | VernacExpr (f, e) -> let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in static_classifier ~poly e - | VernacTimeout (_,{v=e}) -> static_control_classifier e - | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> + | VernacTimeout (_,e) -> static_control_classifier e + | VernacTime (_,e) | VernacRedirect (_, e) -> static_control_classifier e - | VernacFail {v=e} -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) + | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match static_control_classifier e with | ( VtQuery | VtProofStep _ | VtSideff _ | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtLater - | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater) + | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater)) in static_control_classifier e |