aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/constrMatching.ml76
-rw-r--r--pretyping/evarconv.ml15
-rw-r--r--pretyping/evarsolve.ml8
-rw-r--r--pretyping/evarsolve.mli6
-rw-r--r--pretyping/retyping.ml6
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--test-suite/bugs/closed/3637.v11
8 files changed, 65 insertions, 63 deletions
diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index 95fb7ac68..d4cbad054 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -154,7 +154,7 @@ let merge_binding allow_bound_rels stk n cT subst =
else raise PatternMatchingFailure
in
constrain n c subst
-
+
let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
let convref ref c =
match ref, kind_of_term c with
@@ -221,65 +221,28 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
else (* Might be a projection on the right *)
match kind_of_term c2 with
| Proj (pr, c) ->
- if diff == -1 then (* Do as if it was p c args2 *)
- let subst = sorec stk env subst (PApp (PMeta meta, [|args1.(0)|])) c2 in
- Array.fold_left2 (sorec stk env) subst (Array.tl args1) args2
- else (* diff < 0, Expand the projection completely: p params c args2 *)
- let ty = Retyping.get_type_of env sigma c in
- let (i,u), ind_args = Inductive.find_rectype env ty in
- let term = mkApp (mkConstU (pr,u),
- Array.of_list (ind_args @ (c :: Array.to_list args2)))
- in
- sorec stk env subst p term
+ let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
+ sorec stk env subst p term
| _ -> raise PatternMatchingFailure)
| PApp (c1,arg1), App (c2,arg2) ->
- let diff = Array.length arg2 - Array.length arg1 in
(match c1, kind_of_term c2 with
+ | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r pr) ->
+ raise PatternMatchingFailure
(* eta-expanded version of projection against projection *)
- | PRef (ConstRef r), Proj (p,c) when eq_constant r p ->
- let pb = Environ.lookup_projection p env in
- let npars = pb.Declarations.proj_npars in
- let narg1 = Array.length arg1 in
- if narg1 >= npars + 1 then
- let pars, args = Array.chop (npars + 1) arg1 in
- let subst = sorec stk env subst (PApp (c1, pars)) c2 in
- try Array.fold_left2 (sorec stk env) subst args arg2
- with Invalid_argument _ -> raise PatternMatchingFailure
- else raise PatternMatchingFailure
- (* meta against projection *)
- | PMeta meta, Proj (p,c) when diff != 0 ->
- if diff == -1 then (* One more arg for the meta *)
- Array.fold_left2 (sorec stk env) (sorec stk env subst (PApp (c1, [|arg1.(0)|])) c2)
- (Array.tl arg1) arg2
- else raise PatternMatchingFailure
- | _ ->
+ | _, Proj (pr,c) ->
+ let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
+ sorec stk env subst p term
+ | _, _ ->
try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
with Invalid_argument _ -> raise PatternMatchingFailure)
-
- | PApp (PMeta (Some n), args), Proj (pr, c2) ->
- let ty = Retyping.get_type_of env sigma c2 in
- let (i,u), ind_args = Inductive.find_rectype env ty in
- if Array.length args == 1 then
- let term = mkApp (mkConstU (pr,u), Array.of_list ind_args) in
- let subst = merge_binding allow_bound_rels stk n term subst in
- sorec stk env subst args.(0) c2
- else
- let term =
- mkApp (mkConstU (pr,u), Array.of_list (ind_args @ [c2]))
- in
- sorec stk env subst p term
-
- | PApp (PRef (ConstRef c1),arg1), Proj (p2,c2) when eq_constant c1 p2 ->
- let pb = Environ.lookup_projection p2 env in
- let npars = pb.Declarations.proj_npars in
- if Array.length arg1 == npars + 1 then
- let ty = Retyping.get_type_of env sigma c2 in
- let _, pars' = Inductive.find_rectype env ty in
- let subst = List.fold_left2 (sorec stk env) subst
- (Array.to_list (Array.sub arg1 0 npars)) pars' in
- sorec stk env subst arg1.(npars) c2
- else raise PatternMatchingFailure
+
+ | PApp (PRef (ConstRef c1), _), Proj (pr, c2) when not (eq_constant c1 pr) ->
+ raise PatternMatchingFailure
+
+ | PApp (c, args), Proj (pr, c2) ->
+ let term = Retyping.expand_projection env sigma pr c2 [] in
+ sorec stk env subst p term
| PProj (p1,c1), Proj (p2,c2) when eq_constant p1 p2 ->
sorec stk env subst c1 c2
@@ -464,7 +427,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
authorized_occ env sigma partial_app closed pat c mk_ctx next
| Proj (p,c') ->
let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
- let next () = try_aux [env] [c'] next_mk_ctx next in
+ let next () =
+ if partial_app then
+ let term = Retyping.expand_projection env sigma p c' [] in
+ aux env term mk_ctx next
+ else
+ try_aux [env] [c'] next_mk_ctx next in
authorized_occ env sigma partial_app closed pat c mk_ctx next
| Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
authorized_occ env sigma partial_app closed pat c mk_ctx next
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f8e959075..15b16a36b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -835,8 +835,8 @@ let choose_less_dependent_instance evk evd term args =
| [] -> None
| (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
-let apply_on_subterm evdref f c t =
- let rec applyrec (k,c as kc) t =
+let apply_on_subterm env evdref f c t =
+ let rec applyrec (env,(k,c) as acc) t =
(* By using eq_constr, we make an approximation, for instance, we *)
(* could also be interested in finding a term u convertible to t *)
(* such that c occurs in u *)
@@ -845,13 +845,14 @@ let apply_on_subterm evdref f c t =
match kind_of_term t with
| Evar (evk,args) when Evd.is_undefined !evdref evk ->
let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
- let g (_,b,_) a = if Option.is_empty b then applyrec kc a else a in
+ let g (_,b,_) a = if Option.is_empty b then applyrec acc a else a in
mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
| _ ->
- map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c))
- applyrec kc t
+ map_constr_with_binders_left_to_right
+ (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
+ applyrec acc !evdref t
in
- applyrec (0,c) t
+ applyrec (env,(0,c)) t
let filter_possible_projections c ty ctxt args =
let fv1 = free_rels c in
@@ -932,7 +933,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
evdref := evd;
evsref := (fst (destEvar ev),evty)::!evsref;
ev in
- set_holes evdref (apply_on_subterm evdref set_var c rhs) subst
+ set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst
| [] -> rhs in
let subst = make_subst (ctxt,Array.to_list args,argoccs) in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ba877d35c..e47fad81b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -101,6 +101,14 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
in
if !modified then !evdref, t' else !evdref, t
+let map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
+ match kind_of_term c with
+ | Proj (p, r) -> (* Treat specially for partial applications *)
+ let t = Retyping.expand_projection env sigma p r [] in
+ map_constr_with_binders_left_to_right g f acc t
+ | _ -> map_constr_with_binders_left_to_right g f acc c
+
+
(************************)
(* Unification results *)
(************************)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 0d0f3c0e5..86c9908c8 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -69,3 +69,9 @@ val check_evar_instance :
val remove_instance_local_defs :
evar_map -> existential_key -> constr array -> constr list
+
+(* This is up to partial applications and primitive projection expansion *)
+val map_constr_with_binders_left_to_right :
+ (Context.rel_declaration -> (env * 'a) -> (env * 'a)) ->
+ ((env * 'a) -> constr -> constr) ->
+ (env * 'a) -> evar_map -> constr -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 8f1a16dce..3374da327 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -241,3 +241,9 @@ let sorts_of_context env evc ctxt =
let s = get_sort_of env evc t in
(push_rel d env,s::sorts) in
snd (aux ctxt)
+
+let expand_projection env sigma pr c args =
+ let ty = get_type_of env sigma c in
+ let (i,u), ind_args = Inductive.find_rectype env ty in
+ mkApp (mkConstU (pr,u),
+ Array.of_list (ind_args @ (c :: args)))
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index a694faf4e..3cbbc8a5d 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -45,3 +45,5 @@ val type_of_global_reference_knowing_conclusion :
env -> evar_map -> constr -> types -> evar_map * types
val sorts_of_context : env -> evar_map -> rel_context -> sorts list
+
+val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index acae69b68..8875d1d93 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -973,9 +973,9 @@ let e_contextually byhead (occs,c) f env sigma t =
else
t
with ConstrMatching.PatternMatchingFailure ->
- map_constr_with_binders_left_to_right
+ Evarsolve.map_constr_with_binders_left_to_right
(fun d (env,c) -> (push_rel d env,lift_pattern 1 c))
- traverse envc t
+ traverse envc sigma t
in
let t' = traverse (env,c) t in
if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
diff --git a/test-suite/bugs/closed/3637.v b/test-suite/bugs/closed/3637.v
new file mode 100644
index 000000000..a451d2997
--- /dev/null
+++ b/test-suite/bugs/closed/3637.v
@@ -0,0 +1,11 @@
+
+Set Implicit Arguments.
+Set Primitive Projections.
+Record prod A B := pair { fst : A ; snd : B }.
+Goal forall x y : prod Set Set, fst x = fst y.
+ intros.
+ lazymatch goal with
+ | [ |- context[@fst ?A ?B] ] => pose (@fst A B) as fst';
+ progress change (@fst Set Set) with fst'
+end.
+Abort.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 07:49:48 +0000