diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 6 | ||||
| -rw-r--r-- | stm/lemmas.ml | 35 | ||||
| -rw-r--r-- | stm/lemmas.mli | 9 | ||||
| -rw-r--r-- | stm/stm.ml | 47 | ||||
| -rw-r--r-- | stm/stm.mli | 5 | ||||
| -rw-r--r-- | stm/texmacspp.ml | 30 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 20 |
7 files changed, 75 insertions, 77 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 f06abfcce7..ac54028eb7 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 @@ -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/stm.ml b/stm/stm.ml index a6d119f0cd..92032e9bc3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -101,7 +101,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = | VernacResetName _ | VernacResetInitial | VernacBack _ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el + | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> internal_command e | _ -> false in if internal_command expr then begin prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) @@ -186,7 +186,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; @@ -649,10 +649,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 +1140,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 @@ -1414,7 +1414,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 +1431,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 +1440,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 +1484,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 +1496,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 +1533,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 +1549,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 +1649,7 @@ end = struct (* {{{ *) let vernac_interp switch prev id q = assert(TaskQueue.n_workers (Option.get !queue) > 0); TaskQueue.enqueue_task (Option.get !queue) - QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch) + QueryTask.({ t_where = prev; t_for = id; t_what = q }, switch) let init () = queue := Some (TaskQueue.create (if !Flags.async_proofs_full then 1 else 0)) diff --git a/stm/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..2d2ea1f8b0 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 @@ -668,7 +668,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 +694,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 +723,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..ecaf0fb7c5 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -60,7 +60,7 @@ let undo_classifier = ref (fun _ -> assert false) let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = - let rec static_classifier e = match e with + let static_classifier e = match e with (* PG compatibility *) | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) @@ -86,7 +86,7 @@ let rec classify_vernac e = make_polymorphic (classify_vernac e) else classify_vernac e | VernacTimeout (_,e) -> classify_vernac e - | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e + | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ @@ -102,12 +102,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 @@ -175,11 +173,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 +188,6 @@ let rec classify_vernac e = | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ - | VernacTacticNotation _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) @@ -208,7 +200,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 +208,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 |