diff options
| -rw-r--r-- | pretyping/evd.ml | 3 | ||||
| -rw-r--r-- | pretyping/evd.mli | 1 | ||||
| -rw-r--r-- | proofs/proofview.ml | 3 | ||||
| -rw-r--r-- | proofs/proofview.mli | 3 | ||||
| -rw-r--r-- | proofs/refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.mli | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 63 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 |
8 files changed, 68 insertions, 12 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 5a9281c89..1f462197c 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -743,6 +743,9 @@ let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d = let merge_universe_context evd uctx' = { evd with universes = union_evar_universe_context evd.universes uctx' } +let set_universe_context evd uctx' = + { evd with universes = uctx' } + let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = (find d evk).evar_source diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 49a91f524..a360351b7 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -468,6 +468,7 @@ val universes : evar_map -> Univ.universes val merge_universe_context : evar_map -> evar_universe_context -> evar_map +val set_universe_context : evar_map -> evar_universe_context -> evar_map val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 83a703a3a..6651e4965 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -682,6 +682,9 @@ module V82 = struct let tclEVARS evd = Proof.modify (fun ps -> { ps with solution = evd }) + let tclEVARUNIVCONTEXT ctx = + Proof.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) + let has_unresolved_evar pv = Evd.has_undefined pv.solution diff --git a/proofs/proofview.mli b/proofs/proofview.mli index dddf9b1c2..6177803c7 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -298,6 +298,9 @@ module V82 : sig val tclEVARS : Evd.evar_map -> unit tactic + (* Set the evar universe context *) + val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic + val has_unresolved_evar : proofview -> bool (* Main function in the implementation of Grab Existential Variables. diff --git a/proofs/refiner.ml b/proofs/refiner.ml index da9e8c68d..157faae3d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -325,6 +325,8 @@ let rec tclREPEAT_MAIN t g = (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} +let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx} + (* Push universe context *) let tclPUSHCONTEXT rigid ctx tac gl = tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 25ab1fb76..a74d8a46d 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -33,6 +33,7 @@ val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic +val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic val tclPUSHCONTEXT : Evd.rigid -> Univ.universe_context_set -> tactic -> tactic val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0a3141e0a..b21f7f31d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1226,7 +1226,7 @@ let vm_cast_no_check c gl = let exact_proof c gl = let c,ctx = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl) - in tclTHEN (tclPUSHEVARUNIVCONTEXT ctx) (refine_no_check c) gl + in tclTHEN (tclEVARUNIVCONTEXT ctx) (refine_no_check c) gl let assumption = let rec arec gl only_eq = function @@ -1729,14 +1729,17 @@ let generalized_name c t ids cl = function constante dont on aurait pu prendre directement le nom *) named_hd (Global.env()) t Anonymous -let generalize_goal gl i ((occs,c,b),na) (cl,evd) = - let t = pf_type_of gl c in +let generalize_goal_gen ids i ((occs,c,b),na) t (cl,evd) = let decls,cl = decompose_prod_n_assum i cl in let dummy_prod = it_mkProd_or_LetIn mkProp decls in let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in let cl',evd' = subst_closed_term_univs_occ evd occs c (it_mkProd_or_LetIn cl newdecls) in - let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in - mkProd_or_LetIn (na,b,t) cl', evd + let na = generalized_name c t ids cl' na in + mkProd_or_LetIn (na,b,t) cl', evd' + +let generalize_goal gl i ((occs,c,b),na as o) cl = + let t = pf_type_of gl c in + generalize_goal_gen (pf_ids_of_hyps gl) i o t cl let generalize_dep ?(with_let=false) c gl = let env = pf_env gl in @@ -1770,7 +1773,7 @@ let generalize_dep ?(with_let=false) c gl = (cl',project gl) in let args = instance_from_named_context to_quantify_rev in tclTHENLIST - [tclPUSHEVARUNIVCONTEXT (Evd.evar_universe_context evd); + [tclEVARS evd; apply_type cl'' (if Option.is_empty body then c::args else args); thin (List.rev tothin')] gl @@ -1780,17 +1783,46 @@ let generalize_gen_let lconstr gl = List.fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl,project gl) in - tclTHEN (tclPUSHEVARUNIVCONTEXT (Evd.evar_universe_context evd)) + tclTHEN (tclEVARS evd) (apply_type newcl (List.map_filter (fun ((_,c,b),_) -> if Option.is_empty b then Some c else None) lconstr)) gl +let new_generalize_gen_let lconstr = + Proofview.Goal.raw_enter begin fun gl -> + let gl = Proofview.Goal.assume gl in + let concl = Proofview.Goal.concl gl in + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let ids = Tacmach.New.pf_ids_of_hyps gl in + let (newcl, sigma), args = + List.fold_right_i + (fun i ((_,c,b),_ as o) (cl, args) -> + let t = Tacmach.New.pf_type_of gl c in + let args = if Option.is_empty b then c :: args else args in + generalize_goal_gen ids i o t cl, args) + 0 lconstr ((concl, sigma), []) + in + Proofview.V82.tclEVARS sigma <*> + Proofview.Refine.refine begin fun h -> + let (h, ev) = Proofview.Refine.new_evar h env newcl in + (h, (applist (ev, args))) + end + end + let generalize_gen lconstr = generalize_gen_let (List.map (fun ((occs,c),na) -> (occs,c,None),na) lconstr) + +let new_generalize_gen lconstr = + new_generalize_gen_let (List.map (fun ((occs,c),na) -> + (occs,c,None),na) lconstr) let generalize l = generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l) +let new_generalize l = + new_generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l) + let revert hyps gl = let lconstr = List.map (fun id -> let (_, b, _) = pf_get_hyp gl id in @@ -1798,6 +1830,13 @@ let revert hyps gl = hyps in tclTHEN (generalize_gen_let lconstr) (clear hyps) gl +let new_revert hyps = + Proofview.Goal.raw_enter begin fun gl -> + let gl = Proofview.Goal.assume gl in + let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in + (bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps)) + end + (* Faudra-t-il une version avec plusieurs args de generalize_dep ? Cela peut-être troublant de faire "Generalize Dependent H n" dans "n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la @@ -1897,10 +1936,10 @@ let make_pattern_test env sigma0 (sigma,c) = (fun test -> match test.testing_state with | None -> let ctx, c = finish_evar_resolution env sigma0 (sigma,c) in - Proofview.V82.tactic (tclPUSHEVARUNIVCONTEXT ctx), c + Proofview.V82.tclEVARUNIVCONTEXT ctx, c | Some (sigma,_) -> let univs, subst = nf_univ_variables sigma in - Proofview.V82.tactic (tclPUSHEVARUNIVCONTEXT (Evd.evar_universe_context univs)), + Proofview.V82.tclEVARUNIVCONTEXT (Evd.evar_universe_context univs), subst_univs_constr subst (nf_evar sigma c)) let letin_abstract id c (test,out) (occs,check_occs) gl = @@ -1974,10 +2013,10 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs = let make_eq_test evd c = let out cstr = - let tac = tclPUSHEVARUNIVCONTEXT (Evd.evar_universe_context cstr.testing_state) in - Proofview.V82.tactic tac, c + let tac = Proofview.V82.tclEVARUNIVCONTEXT (Evd.evar_universe_context cstr.testing_state) in + tac, c in - (Tacred.make_eq_univs_test Evd.empty c, out) + (Tacred.make_eq_univs_test evd c, out) let letin_tac with_eq name c ty occs = Proofview.tclEVARMAP >>= fun sigma -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 937efdae1..c48ef4451 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -166,6 +166,7 @@ val move_hyp : bool -> Id.t -> Id.t move_location -> tactic val rename_hyp : (Id.t * Id.t) list -> tactic val revert : Id.t list -> tactic +val new_revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) @@ -352,6 +353,9 @@ val pose_proof : Name.t -> constr -> unit Proofview.tactic val generalize : constr list -> tactic val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic +val new_generalize : constr list -> unit Proofview.tactic +val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic + val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic val unify : ?state:Names.transparent_state -> constr -> constr -> tactic |