aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/subtac_utils.ml2
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarutil.ml98
-rw-r--r--pretyping/evarutil.mli6
-rw-r--r--pretyping/unification.ml4
-rw-r--r--proofs/pfedit.ml8
-rw-r--r--proofs/pfedit.mli7
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--tactics/tactics.ml2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2001.v20
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2017.v15
-rw-r--r--toplevel/command.ml22
-rw-r--r--toplevel/command.mli2
13 files changed, 151 insertions, 45 deletions
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 4079b0f20..cdbc40232 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -369,7 +369,7 @@ let solve_by_tac evi t =
Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
(fun _ _ -> ());
Pfedit.by (tclCOMPLETE t);
- let _,(const,_,_) = Pfedit.cook_proof ignore in
+ let _,(const,_,_,_) = Pfedit.cook_proof ignore in
Pfedit.delete_current_proof (); const.Entries.const_entry_body
with e ->
Pfedit.delete_current_proof();
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6664939fb..18cb9457d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -210,7 +210,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| Flexible ev1, MaybeFlexible flex2 ->
let f1 i =
if
- is_unification_pattern_evar env ev1 l1 &
+ is_unification_pattern_evar env ev1 l1 (applist appr2) &
not (occur_evar (fst ev1) (applist appr2))
then
(* Miller-Pfenning's patterns unification *)
@@ -242,7 +242,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| MaybeFlexible flex1, Flexible ev2 ->
let f1 i =
if
- is_unification_pattern_evar env ev2 l2 &
+ is_unification_pattern_evar env ev2 l2 (applist appr1) &
not (occur_evar (fst ev2) (applist appr1))
then
(* Miller-Pfenning's patterns unification *)
@@ -310,7 +310,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| Flexible ev1, Rigid _ ->
if
- is_unification_pattern_evar env ev1 l1 &
+ is_unification_pattern_evar env ev1 l1 (applist appr2) &
not (occur_evar (fst ev1) (applist appr2))
then
(* Miller-Pfenning's patterns unification *)
@@ -325,7 +325,7 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| Rigid _, Flexible ev2 ->
if
- is_unification_pattern_evar env ev2 l2 &
+ is_unification_pattern_evar env ev2 l2 (applist appr1) &
not (occur_evar (fst ev2) (applist appr1))
then
(* Miller-Pfenning's patterns unification *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 551db4e4f..b23c1cc60 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -490,19 +490,30 @@ let clear_hyps_in_evi evdref hyps concl ids =
dependencies in variables are canonically associated to the most ancient
variable in its family of aliased variables *)
-let rec expand_var env x = match kind_of_term x with
+let rec expand_var_at_least_once env x = match kind_of_term x with
| Rel n ->
- begin try match pi2 (lookup_rel n env) with
- | Some t when isRel t -> expand_var env (lift n t)
- | _ -> x
- with Not_found -> x
+ begin match pi2 (lookup_rel n env) with
+ | Some t when isRel t or isVar t ->
+ let t = lift n t in
+ (try expand_var_at_least_once env t with Not_found -> t)
+ | _ ->
+ raise Not_found
end
| Var id ->
begin match pi2 (lookup_named id env) with
- | Some t when isVar t -> expand_var env t
- | _ -> x
+ | Some t when isVar t ->
+ (try expand_var_at_least_once env t with Not_found -> t)
+ | _ ->
+ raise Not_found
end
- | _ -> x
+ | _ ->
+ raise Not_found
+
+let expand_var env x =
+ try expand_var_at_least_once env x with Not_found -> x
+
+let expand_var_opt env x =
+ try Some (expand_var_at_least_once env x) with Not_found -> None
let rec expand_vars_in_term env t = match kind_of_term t with
| Rel _ | Var _ -> expand_var env t
@@ -967,16 +978,71 @@ let head_evar =
that we don't care whether args itself contains Rel's or even Rel's
distinct from the ones in l *)
-let is_unification_pattern_evar env (_,args) l =
- let l' = Array.to_list args @ l in
- let l' = List.map (expand_var env) l' in
- List.for_all (fun a -> isRel a or isVar a) l' && list_distinct l'
-let is_unification_pattern env f l =
+let rec expand_and_check_vars env = function
+ | [] -> []
+ | a::l ->
+ if isRel a or isVar a then
+ let l = expand_and_check_vars env l in
+ match expand_var_opt env a with
+ | None -> a :: l
+ | Some a' when isRel a' or isVar a' -> list_add_set a' l
+ | _ -> raise Exit
+ else
+ raise Exit
+
+(*
+let is_identity_subst env args l =
+ let n = Array.length args in
+ (* Check named context from most recent to oldest declaration *)
+ let rec aux i = function
+ | [] -> i = 0
+ | (id,_,_)::l -> args.(i) = mkVar id && aux (i-1) l in
+ (* Check named context from oldest to most recent declaration *)
+ let rec aux' i = function
+ | [] -> aux i (named_context env)
+ | _::l -> args.(i) = mkRel (n-i) && aux' (i-1) l in
+ List.for_all (fun c -> not (array_exists ((=) (expand_var env c)) args)) l &&
+ aux' (n-1) (rel_context env)
+*)
+
+let is_unification_pattern_evar env (_,args) l t =
+(*
+ (* Optimize the most common case *)
+ List.for_all (fun x -> isRel x || isVar x) l && is_identity_subst env args l
+ ||
+*)
+ let l' = Array.to_list args @ l in
+ let l'' = try Some (expand_and_check_vars env l') with Exit -> None in
+ match l'' with
+ | Some l ->
+ let deps =
+ if occur_meta_or_existential t then
+ l
+ else
+ let fv_rels = free_rels t in
+ let fv_ids = global_vars env t in
+ List.filter (fun c ->
+ match kind_of_term c with
+ | Var id -> List.mem id fv_ids
+ | Rel n -> Intset.mem n fv_rels
+ | _ -> assert false) l in
+ list_distinct deps
+ | None -> false
+
+(*
+ Pp.ppnl (prlist_with_sep spc (fun c -> match kind_of_term c with Rel _ | Var _ -> print_constr c | _ -> str "..") l'); Pp.flush_all ();
+*)
+
+let is_unification_pattern (env,nb) f l t =
match kind_of_term f with
- | Meta _ -> array_for_all isRel l && array_distinct l
- | Evar ev -> is_unification_pattern_evar env ev (Array.to_list l)
- | _ -> false
+ | Meta _ ->
+ array_for_all (fun c -> isRel c && destRel c <= nb) l
+ && array_distinct l
+ | Evar ev ->
+ is_unification_pattern_evar env ev (Array.to_list l) t
+ | _ ->
+ false
(* From a unification problem "?X l1 = term1 l2" such that l1 is made
of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 3ed39fc19..9190d8a97 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -91,8 +91,10 @@ val define_evar_as_product : evar_defs -> existential -> evar_defs * types
val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types
val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts
-val is_unification_pattern_evar : env -> existential -> constr list -> bool
-val is_unification_pattern : env -> constr -> constr array -> bool
+val is_unification_pattern_evar : env -> existential -> constr list ->
+ constr -> bool
+val is_unification_pattern : env * int -> constr -> constr array ->
+ constr -> bool
val solve_pattern_eqn : env -> constr list -> constr -> constr
val evars_of_term : constr -> Intset.t
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 80d7d34a9..e072af362 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -224,12 +224,12 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
(unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2
| App (f1,l1), _ when
- isMeta f1 & is_unification_pattern curenv f1 l1 &
+ isMeta f1 & is_unification_pattern curenvnb f1 l1 cN &
not (dependent f1 cN) ->
solve_pattern_eqn_array curenvnb sigma f1 l1 cN substn
| _, App (f2,l2) when
- isMeta f2 & is_unification_pattern curenv f2 l2 &
+ isMeta f2 & is_unification_pattern curenvnb f2 l2 cM &
not (dependent f2 cM) ->
solve_pattern_eqn_array curenvnb sigma f2 l2 cM substn
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6dad6471d..62668f7f3 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -34,6 +34,7 @@ open Safe_typing
type proof_topstate = {
mutable top_end_tac : tactic option;
top_init_tac : tactic option;
+ top_compute_guard : bool;
top_goal : goal;
top_strength : Decl_kinds.goal_kind;
top_hook : declaration_hook }
@@ -207,7 +208,7 @@ let set_xml_cook_proof f = xml_cook_proof := f
let cook_proof k =
let (pfs,ts) = get_state()
and ident = get_current_proof_name () in
- let {evar_concl=concl} = ts.top_goal
+ let {evar_concl=concl} = ts.top_goal
and strength = ts.top_strength in
let pfterm = extract_pftreestate pfs in
!xml_cook_proof (strength,pfs);
@@ -217,7 +218,7 @@ let cook_proof k =
const_entry_type = Some concl;
const_entry_opaque = true;
const_entry_boxed = false},
- strength, ts.top_hook))
+ ts.top_compute_guard, strength, ts.top_hook))
let current_proof_statement () =
let ts = get_topstate() in
@@ -251,11 +252,12 @@ let set_end_tac tac =
(* Modifying the current prooftree *)
(*********************************************************************)
-let start_proof na str sign concl ?init_tac hook =
+let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook =
let top_goal = mk_goal sign concl None in
let ts = {
top_end_tac = None;
top_init_tac = init_tac;
+ top_compute_guard = compute_guard;
top_goal = top_goal;
top_strength = str;
top_hook = hook}
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index ad7c5e51a..9a40ba319 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -80,7 +80,7 @@ val get_undo : unit -> int option
val start_proof :
identifier -> goal_kind -> named_context_val -> constr ->
- ?init_tac:tactic -> declaration_hook -> unit
+ ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
(* [restart_proof ()] restarts the current focused proof from the beginning
or fails if no proof is focused *)
@@ -104,10 +104,11 @@ val suspend_proof : unit -> unit
(*s [cook_proof opacity] turns the current proof (assumed completed) into
a constant with its name, kind and possible hook (see [start_proof]);
- it fails if there is no current proof of if it is not completed *)
+ it fails if there is no current proof of if it is not completed;
+ it also tells if the guardness condition has to be inferred. *)
val cook_proof : (Refiner.pftreestate -> unit) ->
- identifier * (Entries.definition_entry * goal_kind * declaration_hook)
+ identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook)
(* To export completed proofs to xml *)
val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7413909b5..9ca68c9a1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1416,7 +1416,7 @@ let solvable_by_tactic env evi (ev,args) src =
begin
try
by (tclCOMPLETE tac);
- let _,(const,_,_) = cook_proof ignore in
+ let _,(const,_,_,_) = cook_proof ignore in
delete_current_proof (); const.const_entry_body
with e when Logic.catchable_exception e ->
delete_current_proof();
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c4b580334..76daeb16b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3090,7 +3090,7 @@ let abstract_subproof name tac gl =
error "\"abstract\" cannot handle existentials.";
let lemme =
start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ());
- let _,(const,kind,_) =
+ let _,(const,_,kind,_) =
try
by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac));
let r = cook_proof ignore in
diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v
new file mode 100644
index 000000000..323021dea
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2001.v
@@ -0,0 +1,20 @@
+(* Automatic computing of guard in "Theorem with"; check that guard is not
+ computed when the user explicitly indicated it *)
+
+Inductive T : Set :=
+| v : T.
+
+Definition f (s:nat) (t:T) : nat.
+fix 2.
+intros s t.
+refine
+ match t with
+ | v => s
+ end.
+Defined.
+
+Lemma test :
+ forall s, f s v = s.
+Proof.
+reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v
new file mode 100644
index 000000000..948cea3ee
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2017.v
@@ -0,0 +1,15 @@
+(* Some check of Miller's pattern inference - used to fail in 8.2 due
+ first to the presence of aliases, secondly due to the absence of
+ restriction of the potential interesting variables to the subset of
+ variables effectively occurring in the term to instantiate *)
+
+Set Implicit Arguments.
+
+Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool.
+
+Variable H : exists x : bool, True.
+
+Definition coef :=
+match Some true with
+ Some _ => @choose _ H |_ => true
+end .
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 07f501956..1273d43fe 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -343,11 +343,11 @@ let (inDec,outDec) =
let start_hook = ref ignore
let set_start_hook = (:=) start_hook
-let start_proof id kind c ?init_tac hook =
+let start_proof id kind c ?init_tac ?(compute_guard=false) hook =
let sign = Global.named_context () in
let sign = clear_proofs sign in
!start_hook c;
- Pfedit.start_proof id kind sign c ?init_tac:init_tac hook
+ Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook
let adjust_guardness_conditions const =
(* Try all combinations... not optimal *)
@@ -361,8 +361,8 @@ let adjust_guardness_conditions const =
{ const with const_entry_body = mkFix ((indexes,0),fixdecls) }
| c -> const
-let save id const (locality,kind) hook =
- let const = adjust_guardness_conditions const in
+let save id const do_guard (locality,kind) hook =
+ let const = if do_guard then adjust_guardness_conditions const else const in
let {const_entry_body = pft;
const_entry_type = tpo;
const_entry_opaque = opacity } = const in
@@ -383,9 +383,9 @@ let save_hook = ref ignore
let set_save_hook f = save_hook := f
let save_named opacity =
- let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in
+ let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
let const = { const with const_entry_opaque = opacity } in
- save id const persistence hook
+ save id const do_guard persistence hook
let make_eq_decidability ind =
(* fetching data *)
@@ -1220,7 +1220,7 @@ let start_proof_com kind thms hook =
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
hook strength ref) thms_data in
- start_proof id kind t ?init_tac:rec_tac hook
+ start_proof id kind t ?init_tac:rec_tac ~compute_guard:true hook
let check_anonymity id save_ident =
if atompart_of_id id <> "Unnamed_thm" then
@@ -1230,17 +1230,17 @@ let check_anonymity id save_ident =
*)
let save_anonymous opacity save_ident =
- let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in
+ let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
let const = { const with const_entry_opaque = opacity } in
check_anonymity id save_ident;
- save save_ident const persistence hook
+ save save_ident const do_guard persistence hook
let save_anonymous_with_strength kind opacity save_ident =
- let id,(const,_,hook) = Pfedit.cook_proof !save_hook in
+ let id,(const,do_guard,_,hook) = Pfedit.cook_proof !save_hook in
let const = { const with const_entry_opaque = opacity } in
check_anonymity id save_ident;
(* we consider that non opaque behaves as local for discharge *)
- save save_ident const (Global, Proof kind) hook
+ save save_ident const do_guard (Global, Proof kind) hook
let admit () =
let (id,k,typ,hook) = Pfedit.current_proof_statement () in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8ccaaed35..7cf088901 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -109,7 +109,7 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
val set_start_hook : (types -> unit) -> unit
val start_proof : identifier -> goal_kind -> types ->
- ?init_tac:Proof_type.tactic -> declaration_hook -> unit
+ ?init_tac:Proof_type.tactic -> ?compute_guard:bool -> declaration_hook -> unit
val start_proof_com : goal_kind ->
(lident option * (local_binder list * constr_expr)) list ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-16 13:16:44 +0000