aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml111
-rw-r--r--tactics/eqdecide.ml3
-rw-r--r--tactics/tactics.ml43
4 files changed, 60 insertions, 99 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 8e296de617..76cbdee0d5 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -226,7 +226,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in
let eqclause =
if metas then eqclause
- else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
+ else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd))
in
let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in
let rec split_last_two = function
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9bd406e14d..81cf9289d1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -494,15 +494,15 @@ let top_sort evm undefs =
let tosee = ref undefs in
let rec visit ev evi =
let evs = Evarutil.undefined_evars_of_evar_info evm evi in
- tosee := Evar.Map.remove ev !tosee;
+ tosee := Evar.Set.remove ev !tosee;
Evar.Set.iter (fun ev ->
- if Evar.Map.mem ev !tosee then
- visit ev (Evar.Map.find ev !tosee)) evs;
+ if Evar.Set.mem ev !tosee then
+ visit ev (Evd.find evm ev)) evs;
l' := ev :: !l';
in
- while not (Evar.Map.is_empty !tosee) do
- let ev, evi = Evar.Map.min_binding !tosee in
- visit ev evi
+ while not (Evar.Set.is_empty !tosee) do
+ let ev = Evar.Set.choose !tosee in
+ visit ev (Evd.find evm ev)
done;
List.rev !l'
@@ -512,15 +512,9 @@ let top_sort evm undefs =
*)
let evars_to_goals p evm =
- let goals = ref Evar.Map.empty in
- let map ev evi =
- let evi, goal = p evm ev evi in
- let () = if goal then goals := Evar.Map.add ev evi !goals in
- evi
- in
- let evm = Evd.raw_map_undefined map evm in
- if Evar.Map.is_empty !goals then None
- else Some (!goals, evm)
+ let goals, nongoals = Evar.Set.partition (p evm) (Evd.get_typeclass_evars evm) in
+ if Evar.Set.is_empty goals then None
+ else Some (goals, nongoals)
(** Making local hints *)
let make_resolve_hyp env sigma st flags only_classes pri decl =
@@ -641,14 +635,6 @@ module Search = struct
occur_existential evd concl
else true
- let mark_unresolvables sigma goals =
- List.fold_left
- (fun sigma gl ->
- let evi = Evd.find_undefined sigma gl in
- let evi' = Typeclasses.mark_unresolvable evi in
- Evd.add sigma gl evi')
- sigma goals
-
(** The general hint application tactic.
tac1 + tac2 .... The choice of OR or ORELSE is determined
depending on the dependencies of the goal and the unique/Prop
@@ -779,7 +765,7 @@ module Search = struct
shelve_goals shelved <*>
(if List.is_empty goals then tclUNIT ()
else
- let sigma' = mark_unresolvables sigma goals in
+ let sigma' = make_unresolvables (fun x -> List.mem_f Evar.equal x goals) sigma in
with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>=
fun s -> result s i (Some (Option.default 0 k + j)))
end
@@ -941,14 +927,15 @@ module Search = struct
let run_on_evars env evm p tac =
match evars_to_goals p evm with
| None -> None (* This happens only because there's no evar having p *)
- | Some (goals, evm') ->
+ | Some (goals, nongoals) ->
let goals =
if !typeclasses_dependency_order then
- top_sort evm' goals
- else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
+ top_sort evm goals
+ else Evar.Set.elements goals
in
+ let evm = Evd.set_typeclass_evars evm Evar.Set.empty in
let fgoals = Evd.save_future_goals evm in
- let _, pv = Proofview.init evm' [] in
+ let _, pv = Proofview.init evm [] in
let pv = Proofview.unshelve goals pv in
try
let (), pv', (unsafe, shelved, gaveup), _ =
@@ -967,7 +954,13 @@ module Search = struct
acc && okev) evm' true);
let fgoals = Evd.shelve_on_future_goals shelved fgoals in
let evm' = Evd.restore_future_goals evm' fgoals in
+ let nongoals' =
+ Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with
+ | Some ev' -> Evar.Set.add ev acc
+ | None -> acc) nongoals (Evd.get_typeclass_evars evm')
+ in
let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
+ let evm' = Evd.set_typeclass_evars evm' nongoals' in
Some evm'
else raise Not_found
with Logic_monad.TacticFailure _ -> raise Not_found
@@ -1019,7 +1012,7 @@ let deps_of_constraints cstrs evm p =
let evar_dependencies pred evm p =
Evd.fold_undefined
(fun ev evi _ ->
- if Typeclasses.is_resolvable evi && pred evm ev evi then
+ if Evd.is_typeclass_evar evm ev && pred evm ev evi then
let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
in Intpart.union_set evars p
else ())
@@ -1035,8 +1028,7 @@ let split_evars pred evm =
let is_inference_forced p evd ev =
try
- let evi = Evd.find_undefined evd ev in
- if Typeclasses.is_resolvable evi && snd (p ev evi)
+ if Evar.Set.mem ev (Evd.get_typeclass_evars evd) && p ev
then
let (loc, k) = evar_source ev evd in
match k with
@@ -1068,55 +1060,32 @@ let error_unresolvable env comp evd =
Pretype_errors.unsatisfiable_constraints env evd ev comp
(** Check if an evar is concerned by the current resolution attempt,
- (and in particular is in the current component), and also update
- its evar_info.
- Invariant : this should only be applied to undefined evars,
- and return undefined evar_info *)
+ (and in particular is in the current component).
+ Invariant : this should only be applied to undefined evars. *)
-let select_and_update_evars p oevd in_comp evd ev evi =
- assert (evi.evar_body == Evar_empty);
+let select_and_update_evars p oevd in_comp evd ev =
try
- let oevi = Evd.find_undefined oevd ev in
- if Typeclasses.is_resolvable oevi then
- Typeclasses.mark_unresolvable evi,
- (in_comp ev && p evd ev evi)
- else evi, false
- with Not_found ->
- Typeclasses.mark_unresolvable evi, p evd ev evi
+ if Evd.is_typeclass_evar oevd ev then
+ (in_comp ev && p evd ev (Evd.find evd ev))
+ else false
+ with Not_found -> false
(** Do we still have unresolved evars that should be resolved ? *)
let has_undefined p oevd evd =
- let check ev evi = snd (p oevd ev evi) in
+ let check ev evi = p oevd ev in
Evar.Map.exists check (Evd.undefined_map evd)
-(** Revert the resolvability status of evars after resolution,
- potentially unprotecting some evars that were set unresolvable
- just for this call to resolution. *)
-
-let revert_resolvability oevd evd =
- let map ev evi =
- try
- if not (Typeclasses.is_resolvable evi) then
- let evi' = Evd.find_undefined oevd ev in
- if Typeclasses.is_resolvable evi' then
- Typeclasses.mark_resolvable evi
- else evi
- else evi
- with Not_found -> evi
- in
- Evd.raw_map_undefined map evd
-
exception Unresolved
(** If [do_split] is [true], we try to separate the problem in
several components and then solve them separately *)
let resolve_all_evars debug depth unique env p oevd do_split fail =
- let split = if do_split then split_evars p oevd else [Evar.Set.empty] in
- let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true
- in
+ let tcs = Evd.get_typeclass_evars oevd in
+ let split = if do_split then split_evars p oevd else [tcs] in
+ let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true in
let rec docomp evd = function
- | [] -> revert_resolvability oevd evd
+ | [] -> evd
| comp :: comps ->
let p = select_and_update_evars p oevd (in_comp comp) in
try
@@ -1134,7 +1103,9 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
let initial_select_evars filter =
fun evd ev evi ->
- filter ev (snd evi.Evd.evar_source) &&
+ filter ev (Lazy.from_val (snd evi.Evd.evar_source)) &&
+ (** Typeclass evars can contain evars whose conclusion is not
+ yet determined to be a class or not. *)
Typeclasses.is_class_evar evd evi
let resolve_typeclass_evars debug depth unique env evd filter split fail =
@@ -1161,8 +1132,7 @@ let _ =
let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
let (term, sigma) = Hints.wrap_hint_warning_fun env sigma begin fun sigma ->
let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in
- let (gl,t,sigma) =
- Goal.V82.mk_goal sigma nc gl Store.empty in
+ let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl in
let (ev, _) = destEvar sigma t in
let gls = { it = gl ; sigma = sigma; } in
let hints = searchtable_map typeclasses_db in
@@ -1227,5 +1197,6 @@ let autoapply c i =
unify_e_resolve false flags gl
((c,cty,Univ.ContextSet.empty),0,ce) <*>
Proofview.tclEVARMAP >>= (fun sigma ->
- let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in
+ let sigma = Typeclasses.make_unresolvables
+ (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
Proofview.Unsafe.tclEVARS sigma) end
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index f2bc679aac..6388aa2c33 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -72,11 +72,10 @@ let choose_noteq eqonleft =
let generalize_right mk typ c1 c2 =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let store = Proofview.Goal.extra gl in
Refine.refine ~typecheck:false begin fun sigma ->
let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in
let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
- let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
+ let (sigma, x) = Evarutil.new_evar env sigma ~principal:true newconcl in
(sigma, mkApp (x, [|c2|]))
end
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 18ddc9318d..a6a104ccca 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -117,14 +117,14 @@ let _ =
(** This tactic creates a partial proof realizing the introduction rule, but
does not check anything. *)
-let unsafe_intro env store decl b =
+let unsafe_intro env decl b =
Refine.refine ~typecheck:false begin fun sigma ->
let ctx = named_context_val env in
let nctx = push_named_context_val decl ctx in
let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
let ninst = mkRel 1 :: inst in
let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
- let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+ let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ninst in
(sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev)
end
@@ -133,7 +133,6 @@ let introduction id =
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
let hyps = named_context_val (Proofview.Goal.env gl) in
- let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
let () = if mem_named_context_val id hyps then
user_err ~hdr:"Tactics.introduction"
@@ -141,8 +140,8 @@ let introduction id =
in
let open Context.Named.Declaration in
match EConstr.kind sigma concl with
- | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
- | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
+ | Prod (_, t, b) -> unsafe_intro env (LocalAssum (id, t)) b
+ | LetIn (_, c, t, b) -> unsafe_intro env (LocalDef (id, c, t)) b
| _ -> raise (RefinerError (env, sigma, IntroNeedsProduct))
end
@@ -152,7 +151,6 @@ let error msg = CErrors.user_err Pp.(str msg)
let convert_concl ?(check=true) ty k =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let store = Proofview.Goal.extra gl in
let conclty = Proofview.Goal.concl gl in
Refine.refine ~typecheck:false begin fun sigma ->
let sigma =
@@ -162,7 +160,7 @@ let convert_concl ?(check=true) ty k =
| None -> error "Not convertible."
| Some sigma -> sigma
end else sigma in
- let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
+ let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in
let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
(sigma, ans)
end
@@ -173,11 +171,10 @@ let convert_hyp ?(check=true) d =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let ty = Proofview.Goal.concl gl in
- let store = Proofview.Goal.extra gl in
let sign = convert_hyp check (named_context_val env) sigma d in
let env = reset_with_named_context sign env in
Refine.refine ~typecheck:false begin fun sigma ->
- Evarutil.new_evar env sigma ~principal:true ~store ty
+ Evarutil.new_evar env sigma ~principal:true ty
end
end
@@ -284,12 +281,11 @@ let move_hyp id dest =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let ty = Proofview.Goal.concl gl in
- let store = Proofview.Goal.extra gl in
let sign = named_context_val env in
let sign' = move_hyp_in_named_context env sigma id dest sign in
let env = reset_with_named_context sign' env in
Refine.refine ~typecheck:false begin fun sigma ->
- Evarutil.new_evar env sigma ~principal:true ~store ty
+ Evarutil.new_evar env sigma ~principal:true ty
end
end
@@ -313,7 +309,6 @@ let rename_hyp repl =
Proofview.Goal.enter begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
let concl = Proofview.Goal.concl gl in
- let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
(** Check that we do not mess variables *)
@@ -344,7 +339,7 @@ let rename_hyp repl =
let nctx = val_of_named_context nhyps in
let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
Refine.refine ~typecheck:false begin fun sigma ->
- Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
+ Evarutil.new_evar_instance nctx sigma nconcl ~principal:true instance
end
end
@@ -445,7 +440,6 @@ let internal_cut_gen ?(check=true) dir replace id t =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
- let store = Proofview.Goal.extra gl in
let sign = named_context_val env in
let sign',t,concl,sigma =
if replace then
@@ -464,10 +458,10 @@ let internal_cut_gen ?(check=true) dir replace id t =
let (sigma,ev,ev') =
if dir then
let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
- let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+ let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
(sigma,ev,ev')
else
- let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+ let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
(sigma,ev,ev') in
let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in
@@ -2102,11 +2096,10 @@ let keep hyps =
let apply_type ~typecheck newcl args =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let store = Proofview.Goal.extra gl in
Refine.refine ~typecheck begin fun sigma ->
let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in
let (sigma, ev) =
- Evarutil.new_evar env sigma ~principal:true ~store newcl in
+ Evarutil.new_evar env sigma ~principal:true newcl in
(sigma, applist (ev, args))
end
end
@@ -2120,13 +2113,12 @@ let bring_hyps hyps =
else
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let store = Proofview.Goal.extra gl in
let concl = Tacmach.New.pf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
let args = Array.of_list (Context.Named.to_instance mkVar hyps) in
Refine.refine ~typecheck:false begin fun sigma ->
let (sigma, ev) =
- Evarutil.new_evar env sigma ~principal:true ~store newcl in
+ Evarutil.new_evar env sigma ~principal:true newcl in
(sigma, mkApp (ev, args))
end
end
@@ -2668,7 +2660,7 @@ let mk_eq_name env id {CAst.loc;v=ido} =
(* unsafe *)
-let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
+let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty =
let open Context.Named.Declaration in
let t = match ty with Some t -> t | _ -> typ_of env sigma c in
let decl = if dep then LocalDef (id,c,t)
@@ -2683,11 +2675,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
let eq = applist (eq,args) in
let refl = applist (refl, [t;mkVar id]) in
let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
- let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
+ let (sigma, x) = new_evar newenv sigma ~principal:true ccl in
(sigma, mkNamedLetIn id c t (mkNamedLetIn heq refl eq x))
| None ->
let newenv = insert_before [decl] lastlhyp env in
- let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
+ let (sigma, x) = new_evar newenv sigma ~principal:true ccl in
(sigma, mkNamedLetIn id c t x)
let pose_tac na c =
@@ -4431,7 +4423,6 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let ccl = Proofview.Goal.concl gl in
- let store = Proofview.Goal.extra gl in
let check = check_enough_applied env sigma elim in
let (sigma', c) = use_bindings env sigma elim false (c0,lbind) t0 in
let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in
@@ -4457,7 +4448,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
let b = not with_evars && with_eq != None in
let (sigma, c) = use_bindings env sigma elim b (c0,lbind) t0 in
let t = Retyping.get_type_of env sigma c in
- mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t)
+ mkletin_goal env sigma with_eq false (id,lastlhyp,ccl,c) (Some t)
end;
if with_evars then Proofview.shelve_unifiable else guard_no_unifiable;
if is_arg_pure_hyp
@@ -4478,7 +4469,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
let tac =
Tacticals.New.tclTHENLIST [
Refine.refine ~typecheck:false begin fun sigma ->
- mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
+ mkletin_goal env sigma with_eq true (id,lastlhyp,ccl,c) None
end;
(tac inhyps)
]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-27 23:48:57 +0000