Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe contex…

…t of an evar_map

in tactics, avoiding useless and potentially costly merge's of constraints.
- Implement revert and generalize using the new tactics (not bound to syntax though,
as they are not backwards-compatible yet).
  • Loading branch information...
commit b440899b0f07a23dfce69ae38b0a2b993cc6370c 1 parent a6c966a
@mattam82 mattam82 authored
View
3  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
View
1  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
View
3  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
View
3  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.
View
2  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
View
1  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
View
63 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 ->
View
4 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
Please sign in to comment.
Something went wrong with that request. Please try again.