diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 40 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 4 | ||||
| -rw-r--r-- | proofs/proof_using.ml | 168 | ||||
| -rw-r--r-- | proofs/proof_using.mli | 19 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 1 |
6 files changed, 21 insertions, 213 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 23f96b5a32..469e1a011e 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -156,7 +156,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with - const_entry_body = Future.chain ~pure:true ce.const_entry_body + const_entry_body = Future.chain ce.const_entry_body (fun (pt, _) -> pt, ()) } in let (cb, ctx), () = Future.force ce.const_entry_body in let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index f80cb7cc66..4f575ab4be 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -110,10 +110,6 @@ module Strict = struct let push (b:t) pr = focus bullet_cond (b::get_bullets pr) 1 pr - (* Used only in the next function. - TODO: use a recursive function instead? *) - exception SuggestFound of t - let suggest_bullet (prf : proof): suggestion = if is_done prf then ProofFinished else if not (no_focused_goal prf) @@ -122,24 +118,24 @@ module Strict = struct | b::_ -> Unfinished b | _ -> NoBulletInUse else (* There is no goal under focus but some are unfocussed, - let us look at the bullet needed. If no *) - let pcobaye = ref prf in - try - while true do - let pcobaye', b = pop !pcobaye in - (* pop went well, this means that there are no more goals - *under this* bullet b, see if a new b can be pushed. *) - (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *) - raise (SuggestFound b) - with SuggestFound _ as e -> raise e - | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *) - pcobaye := pcobaye' - done; - assert false - with SuggestFound b -> Suggest b - | _ -> NeedClosingBrace (* No push was possible, but there are still - subgoals somewhere: there must be a "}" to use. *) - + let us look at the bullet needed. *) + let rec loop prf = + match pop prf with + | prf, b -> + (* pop went well, this means that there are no more goals + *under this* bullet b, see if a new b can be pushed. *) + begin + try ignore (push b prf); Suggest b + with _ -> + (* b could not be pushed, so we must look for a outer bullet *) + loop prf + end + | exception _ -> + (* No pop was possible, but there are still + subgoals somewhere: there must be a "}" to use. *) + NeedClosingBrace + in + loop prf let rec pop_until (prf : proof) bul : proof = let prf', b = pop prf in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index cd4d1dcf64..621178982d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -373,11 +373,11 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in (univs, typ), ((body, Univ.ContextSet.empty), eff) in - fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t)) + fun t p -> Future.split2 (Future.chain p (make_body t)) else fun t p -> Future.from_val (univctx, nf t), - Future.chain ~pure:true p (fun (pt,eff) -> + Future.chain p (fun (pt,eff) -> (* Deferred proof, we already checked the universe declaration with the initial universes, ensure that the final universes respect the declaration as well. If the declaration is non-extensible, diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml deleted file mode 100644 index 1a321120c6..0000000000 --- a/proofs/proof_using.ml +++ /dev/null @@ -1,168 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Environ -open Util -open Vernacexpr -open Context.Named.Declaration - -module NamedDecl = Context.Named.Declaration - -let to_string e = - let rec aux = function - | SsEmpty -> "()" - | SsSingl (_,id) -> "("^Id.to_string id^")" - | SsCompl e -> "-" ^ aux e^"" - | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" - | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" - | SsFwdClose e -> "("^aux e^")*" - in aux e - -let known_names = Summary.ref [] ~name:"proofusing-nameset" - -let in_nameset = - let open Libobject in - declare_object { (default_object "proofusing-nameset") with - cache_function = (fun (_,x) -> known_names := x :: !known_names); - classify_function = (fun _ -> Dispose); - discharge_function = (fun _ -> None) - } - -let rec close_fwd e s = - let s' = - List.fold_left (fun s decl -> - let vb = match decl with - | LocalAssum _ -> Id.Set.empty - | LocalDef (_,b,_) -> global_vars_set e b - in - let vty = global_vars_set e (NamedDecl.get_type decl) in - let vbty = Id.Set.union vb vty in - if Id.Set.exists (fun v -> Id.Set.mem v s) vbty - then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s) - s (named_context e) - in - if Id.Set.equal s s' then s else close_fwd e s' -;; - -let rec process_expr env e ty = - let rec aux = function - | SsEmpty -> Id.Set.empty - | SsSingl (_,id) -> set_of_id env ty id - | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2) - | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2) - | SsCompl e -> Id.Set.diff (full_set env) (aux e) - | SsFwdClose e -> close_fwd env (aux e) - in - aux e - -and set_of_id env ty id = - if Id.to_string id = "Type" then - List.fold_left (fun acc ty -> - Id.Set.union (global_vars_set env ty) acc) - Id.Set.empty ty - else if Id.to_string id = "All" then - List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty - else if CList.mem_assoc_f Id.equal id !known_names then - process_expr env (CList.assoc_f Id.equal id !known_names) [] - else Id.Set.singleton id - -and full_set env = - List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty - -let process_expr env e ty = - let ty_expr = SsSingl(Loc.tag @@ Id.of_string "Type") in - let v_ty = process_expr env ty_expr ty in - let s = Id.Set.union v_ty (process_expr env e ty) in - Id.Set.elements s - -let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr)) - -let minimize_hyps env ids = - let rec aux ids = - let ids' = - Id.Set.fold (fun id alive -> - let impl_by_id = - Id.Set.remove id (really_needed env (Id.Set.singleton id)) in - if Id.Set.is_empty impl_by_id then alive - else Id.Set.diff alive impl_by_id) - ids ids in - if Id.Set.equal ids ids' then ids else aux ids' - in - aux ids - -let remove_ids_and_lets env s ids = - let not_ids id = not (Id.Set.mem id ids) in - let no_body id = named_body id env = None in - let deps id = really_needed env (Id.Set.singleton id) in - (Id.Set.filter (fun id -> - not_ids id && - (no_body id || - Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s) - -let suggest_Proof_using name env vars ids_typ context_ids = - let module S = Id.Set in - let open Pp in - let print x = Feedback.msg_debug x in - let pr_set parens s = - let wrap ppcmds = - if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" - else ppcmds in - wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in - let used = S.union vars ids_typ in - let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in - let all_needed = really_needed env needed in - let all = List.fold_right S.add context_ids S.empty in - let fwd_typ = close_fwd env ids_typ in - if !Flags.debug then begin - print (str "All " ++ pr_set false all); - print (str "Type " ++ pr_set false ids_typ); - print (str "needed " ++ pr_set false needed); - print (str "all_needed " ++ pr_set false all_needed); - print (str "Type* " ++ pr_set false fwd_typ); - end; - let valid_exprs = ref [] in - let valid e = valid_exprs := e :: !valid_exprs in - if S.is_empty needed then valid (str "Type"); - if S.equal all_needed fwd_typ then valid (str "Type*"); - if S.equal all all_needed then valid(str "All"); - valid (pr_set false needed); - Feedback.msg_info ( - str"The proof of "++ str name ++ spc() ++ - str "should start with one of the following commands:"++spc()++ - v 0 ( - prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs)); - string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) -;; - -let value = ref false - -let _ = - Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "suggest Proof using"; - Goptions.optkey = ["Suggest";"Proof";"Using"]; - Goptions.optread = (fun () -> !value); - Goptions.optwrite = (fun b -> - value := b; - if b then Term_typing.set_suggest_proof_using suggest_Proof_using - else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "") - ) } - -let value = ref None - -let _ = - Goptions.declare_stringopt_option - { Goptions.optdepr = false; - Goptions.optname = "default value for Proof using"; - Goptions.optkey = ["Default";"Proof";"Using"]; - Goptions.optread = (fun () -> !value); - Goptions.optwrite = (fun b -> value := b;) } - - -let get_default_proof_using () = !value diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli deleted file mode 100644 index c882b1827a..0000000000 --- a/proofs/proof_using.mli +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Utility code for section variables handling in Proof using... *) - -val process_expr : - Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list -> - Names.Id.t list - -val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit - -val to_string : Vernacexpr.section_subset_expr -> string - -val get_default_proof_using : unit -> string option diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index eaf0c693e1..058e839b47 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,7 +1,6 @@ Miscprint Goal Evar_refiner -Proof_using Proof_type Logic Refine |