From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- proofs/proof_global.ml | 102 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 67 insertions(+), 35 deletions(-) (limited to 'proofs/proof_global.ml') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5bff3c81..c303f486 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -67,14 +67,14 @@ type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; - entries : Entries.definition_entry list; + entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; (* constraints : Univ.constraints; *) } type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object @@ -250,17 +250,43 @@ let start_dependent_proof id str goals terminator = let get_used_variables () = (cur_pstate ()).section_vars +let proof_using_auto_clear = ref true +let _ = Goptions.declare_bool_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "Proof using Clear Unused"; + Goptions.optkey = ["Proof";"Using";"Clear";"Unused"]; + Goptions.optread = (fun () -> !proof_using_auto_clear); + Goptions.optwrite = (fun b -> proof_using_auto_clear := b) } + let set_used_variables l = 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 + let vars_of = Environ.global_vars_set in + let aux env entry (ctx, all_safe, to_clear as orig) = + match entry with + | (x,None,_) -> + if Id.Set.mem x all_safe then orig + else (ctx, all_safe, (Loc.ghost,x)::to_clear) + | (x,Some 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 + then (decl :: ctx, Id.Set.add x all_safe, to_clear) + else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in + let ctx, _, to_clear = + Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in + let to_clear = if !proof_using_auto_clear then to_clear else [] in match !pstates with | [] -> raise NoCurrentProof | p :: rest -> if not (Option.is_empty p.section_vars) then Errors.error "Used section variables can be declared only once"; pstates := { p with section_vars = Some ctx} :: rest; - ctx + ctx, to_clear let get_open_goals () = let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in @@ -269,16 +295,14 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf -let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = +let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator } = cur_pstate () in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in + let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in - let universes = - if poly || now then Future.force univs - else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) - in - (* Because of dependent subgoals at the begining of proofs, we could + let universes = if poly || now then Future.force univs else initial_euctx in + (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) let subst_evar k = @@ -289,19 +313,26 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = if poly || now then let make_body t (c, eff) = let open Universes in - let body = c and typ = nf t in + let body = c in + let typ = + if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then + nf t + else t + in let used_univs_body = Universes.universes_of_constr body in - let used_univs_typ = Universes.universes_of_constr typ in - let ctx = Evd.evar_universe_context_set universes in - if keep_body_ucst_sepatate then + let used_univs_typ = Universes.universes_of_constr typ in + 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 (* 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. *) let ctx_body = restrict_universe_context ctx used_univs_body in - let ctx_typ = restrict_universe_context ctx used_univs_typ in - let univs_typ = Univ.ContextSet.to_context ctx_typ in - (univs_typ, typ), ((body, ctx_body), eff) + (initunivs, typ), ((body, ctx_body), eff) else + let initunivs = Univ.UContext.empty in + let ctx = Evd.evar_universe_context_set 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 *) @@ -310,14 +341,13 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let univs = Univ.ContextSet.to_context ctx 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 ~pure:true p (make_body t)) else fun t p -> - let initunivs = Evd.evar_context_universe_context universes in - Future.from_val (initunivs, nf t), - Future.chain ~pure:true p (fun (pt,eff) -> - (pt, Evd.evar_universe_context_set (Future.force univs)), eff) + 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) in let entries = Future.map2 (fun p (_, t) -> @@ -336,15 +366,11 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = { id = pid; entries = entries; persistence = strength; universes = universes }, fun pr_ending -> Ephemeron.get terminator pr_ending -type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in if allow_partial then begin - if Proof.is_done proof then begin - msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++ - str" is complete, no need to end it with Admitted"); - end; let proofs = Proof.partial_proof proof in let _,_,_,_, evd = Proof.proof proof in let eff = Evd.eval_side_effects evd in @@ -370,10 +396,7 @@ let return_proof ?(allow_partial=false) () = | Proof.HasUnresolvedEvar-> error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = - if poly || !Flags.compilation_mode = Flags.BuildVo - then Evd.nf_constraints evd - else evd in + let evd = Evd.nf_constraints evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) @@ -382,9 +405,9 @@ let return_proof ?(allow_partial=false) () = proofs, Evd.evar_universe_context evd let close_future_proof ~feedback_id proof = - close_proof ~keep_body_ucst_sepatate:true ~feedback_id ~now:false proof -let close_proof ~keep_body_ucst_sepatate fix_exn = - close_proof ~keep_body_ucst_sepatate ~now:true + close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof +let close_proof ~keep_body_ucst_separate fix_exn = + close_proof ~keep_body_ucst_separate ~now:true (Future.from_val ~fix_exn (return_proof ())) (** Gets the current terminator without checking that the proof has @@ -668,4 +691,13 @@ let freeze ~marshallable = | `No -> !pstates let unfreeze s = pstates := s; update_proof_mode () let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof - +let copy_terminators ~src ~tgt = + assert(List.length src = List.length tgt); + List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt + +let update_global_env () = + with_current_proof (fun _ p -> + Proof.in_proof p (fun sigma -> + let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in + let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in + (p, ()))) -- cgit v1.2.3