From c538b7fd555828d9fba9ea97503fac6c70377b76 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 25 Apr 2018 18:12:41 +0200 Subject: Convert clear_hyps_in_evi to state passing style. --- engine/evarutil.ml | 17 +++++++++-------- engine/evarutil.mli | 8 ++++---- plugins/ssrmatching/ssrmatching.ml4 | 7 +++---- tactics/tactics.ml | 14 ++++++-------- 4 files changed, 22 insertions(+), 24 deletions(-) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 6c27d5937..52610f6f3 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -613,10 +613,11 @@ let rec check_and_clear_in_constr env evdref err ids global c = | _ -> Constr.map (check_and_clear_in_constr env evdref err ids global) c -let clear_hyps_in_evi_main env evdref hyps terms ids = +let clear_hyps_in_evi_main env sigma hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in the contexts of the evars occurring in evi *) + let evdref = ref sigma in let terms = List.map EConstr.Unsafe.to_constr terms in let global = Id.Set.exists is_section_variable ids in let terms = @@ -639,16 +640,16 @@ let clear_hyps_in_evi_main env evdref hyps terms ids = in remove_hyps ids check_context check_value hyps in - (nhyps,List.map EConstr.of_constr terms) + (!evdref, nhyps,List.map EConstr.of_constr terms) -let clear_hyps_in_evi env evdref hyps concl ids = - match clear_hyps_in_evi_main env evdref hyps [concl] ids with - | (nhyps,[nconcl]) -> (nhyps,nconcl) +let clear_hyps_in_evi env sigma hyps concl ids = + match clear_hyps_in_evi_main env sigma hyps [concl] ids with + | (sigma,nhyps,[nconcl]) -> (sigma,nhyps,nconcl) | _ -> assert false -let clear_hyps2_in_evi env evdref hyps t concl ids = - match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with - | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl) +let clear_hyps2_in_evi env sigma hyps t concl ids = + match clear_hyps_in_evi_main env sigma hyps [t;concl] ids with + | (sigma,nhyps,[t;nconcl]) -> (sigma,nhyps,t,nconcl) | _ -> assert false (* spiwack: a few functions to gather evars on which goals depend. *) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 7595de04c..c24660f5b 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -221,11 +221,11 @@ type clear_dependency_error = exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option -val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> - Id.Set.t -> named_context_val * types +val clear_hyps_in_evi : env -> evar_map -> named_context_val -> types -> + Id.Set.t -> evar_map * named_context_val * types -val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> - Id.Set.t -> named_context_val * types * types +val clear_hyps2_in_evi : env -> evar_map -> named_context_val -> types -> types -> + Id.Set.t -> evar_map * named_context_val * types * types type csubst diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a10437a63..0dd3625ba 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1099,15 +1099,14 @@ let thin id sigma goal = let ids = Id.Set.singleton id in let env = Goal.V82.env sigma goal in let cl = Goal.V82.concl sigma goal in - let evdref = ref (Evd.clear_metas sigma) in + let sigma = Evd.clear_metas sigma in let ans = - try Some (Evarutil.clear_hyps_in_evi env evdref (Environ.named_context_val env) cl ids) + try Some (Evarutil.clear_hyps_in_evi env sigma (Environ.named_context_val env) cl ids) with Evarutil.ClearDependencyError _ -> None in match ans with | None -> sigma - | Some (hyps, concl) -> - let sigma = !evdref in + | Some (sigma, hyps, concl) -> let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in sigma diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 178c10815..66505edb5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -247,13 +247,12 @@ let clear_gen fail = function let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let evdref = ref sigma in - let (hyps, concl) = - try clear_hyps_in_evi env evdref (named_context_val env) concl ids + let (sigma, hyps, concl) = + try clear_hyps_in_evi env sigma (named_context_val env) concl ids with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal in let env = reset_with_named_context hyps env in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl end) @@ -431,9 +430,8 @@ let get_previous_hyp_position env sigma id = let clear_hyps2 env sigma ids sign t cl = try - let evdref = ref (Evd.clear_metas sigma) in - let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in - (hyps, t, cl, !evdref) + let sigma = Evd.clear_metas sigma in + Evarutil.clear_hyps2_in_evi env sigma sign t cl ids with Evarutil.ClearDependencyError (id,err,inglobal) -> error_replacing_dependency env sigma id err inglobal @@ -447,7 +445,7 @@ let internal_cut_gen ?(check=true) dir replace id t = let sign',t,concl,sigma = if replace then let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in - let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in + let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in sign',t,concl,sigma else -- cgit v1.2.3