From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- proofs/proof_global.ml | 134 +++++++++++++++++++++++++++---------------------- 1 file changed, 73 insertions(+), 61 deletions(-) (limited to 'proofs/proof_global.ml') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f22cdbcc..e753e972 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -23,8 +23,9 @@ open Names (* Type of proof modes : - A function [set] to set it *from standard mode* - A function [reset] to reset the *standard mode* from it *) +type proof_mode_name = string type proof_mode = { - name : string ; + name : proof_mode_name ; set : unit -> unit ; reset : unit -> unit } @@ -33,10 +34,10 @@ let proof_modes = Hashtbl.create 6 let find_proof_mode n = try Hashtbl.find proof_modes n with Not_found -> - Errors.error (Format.sprintf "No proof mode named \"%s\"." n) + CErrors.error (Format.sprintf "No proof mode named \"%s\"." n) let register_proof_mode ({name = n} as m) = - Hashtbl.add proof_modes n (Ephemeron.create m) + Hashtbl.add proof_modes n (CEphemeron.create m) (* initial mode: standard mode *) let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) } @@ -45,6 +46,9 @@ let _ = register_proof_mode standard (* Default proof mode, to be set at the beginning of proofs. *) let default_proof_mode = ref (find_proof_mode "No") +let get_default_proof_mode_name () = + (CEphemeron.default !default_proof_mode standard).name + let _ = Goptions.declare_string_option {Goptions. optsync = true ; @@ -52,7 +56,7 @@ let _ = optname = "default proof mode" ; optkey = ["Default";"Proof";"Mode"] ; optread = begin fun () -> - (Ephemeron.default !default_proof_mode standard).name + (CEphemeron.default !default_proof_mode standard).name end; optwrite = begin fun n -> default_proof_mode := find_proof_mode n @@ -83,15 +87,18 @@ type closed_proof = proof_object * proof_terminator type pstate = { pid : Id.t; - terminator : proof_terminator Ephemeron.key; + terminator : proof_terminator CEphemeron.key; endline_tactic : Tacexpr.raw_tactic_expr option; section_vars : Context.section_context option; proof : Proof.proof; strength : Decl_kinds.goal_kind; - mode : proof_mode Ephemeron.key; + mode : proof_mode CEphemeron.key; universe_binders: universe_binders option; } +let make_terminator f = f +let apply_terminator f = f + (* The head of [!pstates] is the actual current proof, the other ones are to be resumed when the current proof is closed or aborted. *) let pstates = ref ([] : pstate list) @@ -103,11 +110,11 @@ let current_proof_mode = ref !default_proof_mode let update_proof_mode () = match !pstates with | { mode = m } :: _ -> - Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); current_proof_mode := m; - Ephemeron.iter_opt !current_proof_mode (fun x -> x.set ()) + CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ()) | _ -> - Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); current_proof_mode := find_proof_mode "No" (* combinators for the current_proof lists *) @@ -115,15 +122,15 @@ let push a l = l := a::!l; update_proof_mode () exception NoSuchProof -let _ = Errors.register_handler begin function - | NoSuchProof -> Errors.error "No such proof." - | _ -> raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | NoSuchProof -> CErrors.error "No such proof." + | _ -> raise CErrors.Unhandled end exception NoCurrentProof -let _ = Errors.register_handler begin function - | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)." - | _ -> raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)." + | _ -> raise CErrors.Unhandled end (*** Proof Global manipulation ***) @@ -183,7 +190,7 @@ let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - Errors.error (Pp.string_of_ppcmds + CErrors.error (Pp.string_of_ppcmds (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++ str"Use \"Abort All\" first or complete proof(s).")) end @@ -195,7 +202,7 @@ let discard (loc,id) = let n = List.length !pstates in discard_gen id; if Int.equal (List.length !pstates) n then - Errors.user_err_loc + CErrors.user_err_loc (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ()) let discard_current () = @@ -215,9 +222,9 @@ let set_proof_mode mn = set_proof_mode (find_proof_mode mn) (get_current_proof_name ()) let activate_proof_mode mode = - Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) -let disactivate_proof_mode mode = - Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ()) + CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) +let disactivate_current_proof_mode () = + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) (** [start_proof sigma id str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and @@ -230,7 +237,7 @@ let disactivate_proof_mode mode = let start_proof sigma id ?pl str goals terminator = let initial_state = { pid = id; - terminator = Ephemeron.create terminator; + terminator = CEphemeron.create terminator; proof = Proof.start sigma goals; endline_tactic = None; section_vars = None; @@ -242,7 +249,7 @@ let start_proof sigma id ?pl str goals terminator = let start_dependent_proof id ?pl str goals terminator = let initial_state = { pid = id; - terminator = Ephemeron.create terminator; + terminator = CEphemeron.create terminator; proof = Proof.dependent_start goals; endline_tactic = None; section_vars = None; @@ -264,18 +271,19 @@ let _ = Goptions.declare_bool_option Goptions.optwrite = (fun b -> proof_using_auto_clear := b) } let set_used_variables l = + let open Context.Named.Declaration in let env = Global.env () in let ids = List.fold_right Id.Set.add l Id.Set.empty in let ctx = Environ.keep_hyps env ids in let ctx_set = - List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in + List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in let vars_of = Environ.global_vars_set in let aux env entry (ctx, all_safe, to_clear as orig) = match entry with - | (x,None,_) -> + | LocalAssum (x,_) -> if Id.Set.mem x all_safe then orig else (ctx, all_safe, (Loc.ghost,x)::to_clear) - | (x,Some bo, ty) as decl -> + | LocalDef (x,bo, ty) as decl -> if Id.Set.mem x all_safe then orig else let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in if Id.Set.subset vars all_safe @@ -288,7 +296,7 @@ let set_used_variables l = | [] -> raise NoCurrentProof | p :: rest -> if not (Option.is_empty p.section_vars) then - Errors.error "Used section variables can be declared only once"; + CErrors.error "Used section variables can be declared only once"; pstates := { p with section_vars = Some ctx} :: rest; ctx, to_clear @@ -299,6 +307,11 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf +let constrain_variables init uctx = + let levels = Univ.Instance.levels (Univ.UContext.instance init) in + let cstrs = UState.constrain_variables levels uctx in + Univ.ContextSet.add_constraints cstrs (UState.context_set uctx) + let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator; universe_binders } = cur_pstate () in @@ -329,7 +342,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in - let ctx = Evd.evar_universe_context_set initunivs universes in + let ctx = constrain_variables initunivs universes in (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) @@ -338,7 +351,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = (initunivs, typ), ((body, ctx_body), eff) else let initunivs = Univ.UContext.empty in - let ctx = Evd.evar_universe_context_set initunivs universes in + let ctx = constrain_variables initunivs universes in (* Since the proof is computed now, we can simply have 1 set of * constraints in which we merge the ones for the body and the ones * for the typ *) @@ -353,7 +366,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let initunivs = Evd.evar_context_universe_context initial_euctx in Future.from_val (initunivs, nf t), Future.chain ~pure:true p (fun (pt,eff) -> - (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff) + (pt,constrain_variables initunivs (Future.force univs)),eff) in let entries = Future.map2 (fun p (_, t) -> @@ -375,7 +388,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = in { id = pid; entries = entries; persistence = strength; universes = (universes, binders) }, - fun pr_ending -> Ephemeron.get terminator pr_ending + fun pr_ending -> CEphemeron.get terminator pr_ending type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context @@ -395,7 +408,7 @@ let return_proof ?(allow_partial=false) () = let evd = let error s = let prf = str " (in proof " ++ Id.print pid ++ str ")" in - raise (Errors.UserError("last tactic before Qed",s ++ prf)) + raise (CErrors.UserError("last tactic before Qed",s ++ prf)) in try Proof.return proof with | Proof.UnfinishedProof -> @@ -423,11 +436,11 @@ let close_proof ~keep_body_ucst_separate fix_exn = (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) -let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator +let get_terminator () = CEphemeron.get ( cur_pstate() ).terminator let set_terminator hook = match !pstates with | [] -> raise NoCurrentProof - | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps + | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps @@ -458,7 +471,7 @@ module Bullet = struct type behavior = { name : string; put : Proof.proof -> t -> Proof.proof; - suggest: Proof.proof -> string option + suggest: Proof.proof -> std_ppcmds } let behaviors = Hashtbl.create 4 @@ -468,7 +481,7 @@ module Bullet = struct let none = { name = "None"; put = (fun x _ -> x); - suggest = (fun _ -> None) + suggest = (fun _ -> mt ()) } let _ = register_behavior none @@ -484,36 +497,30 @@ module Bullet = struct (* give a message only if more informative than the standard coq message *) let suggest_on_solved_goal sugg = match sugg with - | NeedClosingBrace -> Some "Try unfocusing with \"}\"." - | NoBulletInUse -> None - | ProofFinished -> None - | Suggest b -> Some ("Focus next goal with bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^".") - | Unfinished b -> Some ("The current bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is unfinished.") + | NeedClosingBrace -> str"Try unfocusing with \"}\"." + | NoBulletInUse -> mt () + | ProofFinished -> mt () + | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"." + | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished." (* give always a message. *) let suggest_on_error sugg = match sugg with - | NeedClosingBrace -> "Try unfocusing with \"}\"." + | NeedClosingBrace -> str"Try unfocusing with \"}\"." | NoBulletInUse -> assert false (* This should never raise an error. *) - | ProofFinished -> "No more subgoals." - | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is mandatory here.") - | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is not finished.") + | ProofFinished -> str"No more subgoals." + | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here." + | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished." exception FailedBullet of t * suggestion let _ = - Errors.register_handler + CErrors.register_handler (function | FailedBullet (b,sugg) -> - let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in - Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg)) - | _ -> raise Errors.Unhandled) + let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in + CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg) + | _ -> raise CErrors.Unhandled) (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) @@ -610,7 +617,7 @@ module Bullet = struct let _ = register_behavior strict end - (* Current bullet behavior, controled by the option *) + (* Current bullet behavior, controlled by the option *) let current_behavior = ref Strict.strict let _ = @@ -626,7 +633,7 @@ module Bullet = struct current_behavior := try Hashtbl.find behaviors n with Not_found -> - Errors.error ("Unknown bullet behavior: \"" ^ n ^ "\".") + CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".") end } @@ -657,21 +664,26 @@ let _ = let default_goal_selector = ref (Vernacexpr.SelectNth 1) let get_default_goal_selector () = !default_goal_selector +let print_range_selector (i, j) = + if i = j then string_of_int i + else string_of_int i ^ "-" ^ string_of_int j + let print_goal_selector = function | Vernacexpr.SelectAll -> "all" | Vernacexpr.SelectNth i -> string_of_int i + | Vernacexpr.SelectList l -> "[" ^ + String.concat ", " (List.map print_range_selector l) ^ "]" | Vernacexpr.SelectId id -> Id.to_string id - | Vernacexpr.SelectAllParallel -> "par" let parse_goal_selector = function | "all" -> Vernacexpr.SelectAll | i -> - let err_msg = "A selector must be \"all\" or a natural number." in + let err_msg = "The default selector must be \"all\" or a natural number." in begin try let i = int_of_string i in - if i < 0 then Errors.error err_msg; + if i < 0 then CErrors.error err_msg; Vernacexpr.SelectNth i - with Failure _ -> Errors.error err_msg + with Failure _ -> CErrors.error err_msg end let _ = @@ -700,7 +712,7 @@ type state = pstate list let freeze ~marshallable = match marshallable with | `Yes -> - Errors.anomaly (Pp.str"full marshalling of proof state not supported") + CErrors.anomaly (Pp.str"full marshalling of proof state not supported") | `Shallow -> !pstates | `No -> !pstates let unfreeze s = pstates := s; update_proof_mode () -- cgit v1.2.3