diff options
| -rw-r--r-- | pretyping/evarconv.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 45 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 5 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/rewrite.v | 10 |
5 files changed, 47 insertions, 25 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 180aac5900..236bc1b43c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -227,7 +227,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, MaybeFlexible flex2 -> let f1 i = - match is_unification_pattern env term1 l1 (applist appr2) with + match is_unification_pattern_evar env ev1 l1 (applist appr2) with | Some l1' -> (* Miller-Pfenning's patterns unification *) (* Preserve generality (except that CCI has no eta-conversion) *) @@ -260,7 +260,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = | MaybeFlexible flex1, Flexible ev2 -> let f1 i = - match is_unification_pattern env term2 l2 (applist appr1) with + match is_unification_pattern_evar env ev2 l2 (applist appr1) with | Some l1' -> (* Miller-Pfenning's patterns unification *) (* Preserve generality (except that CCI has no eta-conversion) *) @@ -358,7 +358,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)] | Flexible ev1, (Rigid _ | PseudoRigid _) -> - (match is_unification_pattern env term1 l1 (applist appr2) with + (match is_unification_pattern_evar env ev1 l1 (applist appr2) with | Some l1 -> (* Miller-Pfenning's pattern unification *) (* Preserve generality thanks to eta-conversion) *) @@ -372,7 +372,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = true) | (Rigid _ | PseudoRigid _), Flexible ev2 -> - (match is_unification_pattern env term2 l2 (applist appr1) with + (match is_unification_pattern_evar env ev2 l2 (applist appr1) with | Some l2 -> (* Miller-Pfenning's pattern unification *) (* Preserve generality thanks to eta-conversion) *) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 6a622d9aa3..af9db2cdea 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1335,30 +1335,39 @@ let get_actual_deps aliases l t = (* Check if an applied evar "?X[args] l" is a Miller's pattern *) -let find_unification_pattern_args env args l t = +let find_unification_pattern_args env l t = if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then let aliases = make_alias_map env in - let l' = Array.to_list args @ l in - match (try Some (expand_and_check_vars aliases l') with Exit -> None) with - | Some l when constr_list_distinct (get_actual_deps aliases l t) -> - Some (list_skipn (Array.length args) l) - | _ -> - None + match (try Some (expand_and_check_vars aliases l) with Exit -> None) with + | Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x + | _ -> None + else + None + +let is_unification_pattern_meta env nb m l t = + (* Variables from context and rels > nb are implicitly all there *) + (* so we need to be a rel <= nb *) + if List.for_all (fun x -> isRel x && destRel x <= nb) l then + match find_unification_pattern_args env l t with + | Some _ as x when not (dependent (mkMeta m) t) -> x + | _ -> None else None -let is_unification_pattern env f l t = +let is_unification_pattern_evar env (evk,args) l t = + if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then + let n = Array.length args in + match find_unification_pattern_args env (Array.to_list args @ l) t with + | Some l when not (occur_evar evk t) -> Some (list_skipn n l) + | _ -> None + else + None + +let is_unification_pattern (env,nb) f l t = match kind_of_term f with - | Meta m -> - (match find_unification_pattern_args env [||] l t with - | Some _ as x when not (dependent f t) -> x - | _ -> None) - | Evar (evk,args) -> - (match find_unification_pattern_args env args l t with - | Some _ as x when not (occur_evar evk t) -> x - | _ -> None) - | _ -> - None + | Meta m -> is_unification_pattern_meta env nb m l t + | Evar ev -> is_unification_pattern_evar env ev l t + | _ -> None (* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)" (pattern unification). It is assumed that l is made of rel's that diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 3652768531..c0c4252e68 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -96,7 +96,10 @@ val define_evar_as_product : evar_map -> existential -> evar_map * types val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types val define_evar_as_sort : evar_map -> existential -> evar_map * sorts -val is_unification_pattern : env -> constr -> constr list -> +val is_unification_pattern_evar : env -> existential -> constr list -> + constr -> constr list option + +val is_unification_pattern : env * int -> constr -> constr list -> constr -> constr list option val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 250d83cc4c..6fff81cfe6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -437,13 +437,13 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | App (f1,l1), _ when (isMeta f1 && use_metas_pattern_unification flags nb l1 || use_evars_pattern_unification flags && isAllowedEvar flags f1) & - store whenmem (is_unification_pattern curenv f1 (Array.to_list l1) cN) -> + store whenmem (is_unification_pattern curenvnb f1 (Array.to_list l1) cN) -> solve_pattern_eqn_array curenvnb f1 (restore whenmem) cN substn | _, App (f2,l2) when (isMeta f2 && use_metas_pattern_unification flags nb l2 || use_evars_pattern_unification flags && isAllowedEvar flags f2) & - store whenmem (is_unification_pattern curenv f2 (Array.to_list l2) cM) -> + store whenmem (is_unification_pattern curenvnb f2 (Array.to_list l2) cM) -> solve_pattern_eqn_array curenvnb f2 (restore whenmem) cM substn | App (f1,l1), App (f2,l2) -> diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 3d49d3cf93..08c406be94 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -118,4 +118,14 @@ Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p). Definition P := (nat * nat)%type. Goal forall x:P, x = x. intros. rewrite s. +Abort. + +(* Test second-order unification and failure of pattern-unification *) + +Goal forall (P: forall Y, Y -> Prop) Y a, Y = nat -> (True -> P Y a) -> False. +intros. +(* The next line used to succeed between June and November 2011 *) +(* causing ill-typed rewriting *) +Fail rewrite H in H0. +Abort. |