From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- proofs/refine.ml | 103 ++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 63 insertions(+), 40 deletions(-) (limited to 'proofs/refine.ml') diff --git a/proofs/refine.ml b/proofs/refine.ml index 3f552706..909556b1 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -1,16 +1,19 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* () - | LocalDef (_,body,_) -> Typing.e_check env evdref body t + | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t in (!evdref, Environ.push_named decl env) in @@ -40,7 +43,7 @@ let typecheck_evar ev env sigma = let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in (** Typecheck the conclusion *) let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in + let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in !evdref let typecheck_proof c concl env sigma = @@ -68,38 +71,48 @@ let add_side_effect env = function let add_side_effects env effects = List.fold_left (fun env eff -> add_side_effect env eff) env effects -let make_refine_enter ?(unsafe = true) f = - { enter = fun gl -> - let gl = Proofview.Goal.assume gl in +let generic_refine ~typecheck f gl = let sigma = Proofview.Goal.sigma gl in - let sigma = Sigma.to_evar_map sigma in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in + let state = Proofview.Goal.state gl in (** Save the [future_goals] state to restore them after the refinement. *) - let prev_future_goals = Evd.future_goals sigma in - let prev_principal_goal = Evd.principal_future_goal sigma in + let prev_future_goals = Evd.save_future_goals sigma in (** Create the refinement term *) - let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in - let evs = Evd.future_goals sigma in - let evkmain = Evd.principal_future_goal sigma in + Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> + f >>= fun (v, c) -> + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.V82.wrap_exceptions begin fun () -> + let evs = Evd.save_future_goals sigma in (** Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in let sideff = Safe_typing.side_effects_of_private_constants privates_csts in let env = add_side_effects env sideff in (** Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in - let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in + let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in (** Check that the refined term is typesafe *) - let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in + let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in (** Check that the goal itself does not appear in the refined term *) let self = Proofview.Goal.goal gl in let _ = if not (Evarutil.occur_evar_upto sigma self c) then () else Pretype_errors.error_occur_check env sigma self c in + (** Restore the [future goals] state. *) + let sigma = Evd.restore_future_goals sigma prev_future_goals in + (** Select the goals *) + let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in + let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in (** Proceed to the refinement *) - let sigma = match evkmain with + let c = EConstr.Unsafe.to_constr c in + let sigma = match Proofview.Unsafe.advance sigma self with + | None -> + (** Nothing to do, the goal has been solved by side-effect *) + sigma + | Some self -> + match evkmain with | None -> Evd.define self c sigma | Some evk -> let id = Evd.evar_ident self sigma in @@ -108,25 +121,37 @@ let make_refine_enter ?(unsafe = true) f = | None -> sigma | Some id -> Evd.rename evk id sigma in - (** Restore the [future goals] state. *) - let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in - (** Select the goals *) - let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in + (** Mark goals *) let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in + let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> Proofview.Unsafe.tclSETGOALS comb <*> + Proofview.Unsafe.tclPUTSHELF shelf <*> + Proofview.Unsafe.tclPUTGIVENUP given_up <*> Proofview.tclUNIT v - } + end -let refine_one ?(unsafe = true) f = - Proofview.Goal.enter_one (make_refine_enter ~unsafe f) +let lift c = + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.V82.wrap_exceptions begin fun () -> + let (sigma, c) = c sigma in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.tclUNIT c + end -let refine ?(unsafe = true) f = - let f = { run = fun sigma -> let Sigma (c,sigma,p) = f.run sigma in Sigma (((),c),sigma,p) } in - Proofview.Goal.enter (make_refine_enter ~unsafe f) +let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl + +let refine_one ~typecheck f = + Proofview.Goal.enter_one (make_refine_enter ~typecheck f) + +let refine ~typecheck f = + let f evd = + let (evd,c) = f evd in (evd,((), c)) + in + Proofview.Goal.enter (make_refine_enter ~typecheck f) (** Useful definitions *) @@ -134,21 +159,19 @@ let with_type env evd c t = let my_type = Retyping.get_type_of env evd c in let j = Environ.make_judge c my_type in let (evd,j') = - Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t + Coercion.inh_conv_coerce_to true env evd j t in evd , j'.Environ.uj_val -let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> - let gl = Proofview.Goal.assume gl in +let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - let f = { run = fun h -> - let Sigma (c, h, p) = f.run h in - let sigma, c = with_type env (Sigma.to_evar_map h) c concl in - Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) - } in - refine ?unsafe f -end } + let f h = + let (h, c) = f h in + with_type env h c concl + in + refine ~typecheck f +end (** {7 solve_constraints} -- cgit v1.2.3