From 60d973e92c466a89410e359e4377ba5f4a7f0316 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 28 Aug 2006 09:22:25 +0000 Subject: Diverses modifications autour de l'unification modulo conversion: - extension de l'unification au cas de motifs (au sens de Dale Miller) [appel de solve_pattern_eqn dans evar_conv_x], - correction de bugs présumés dans real_clean et do_restrict_hyp (prise en compte de la taille courante du contexte de de Bruijn), - ajout d'une heuristique de beta-reduction de tete dans real_clean (cf test-suite/success/unification.v), - suppression de certains "try ... with _ => ...". MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9088 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 6 +++ pretyping/evarconv.ml | 65 +++++++++++++++++++----- pretyping/evarutil.ml | 103 +++++++++++++++++++++++++++------------ pretyping/evarutil.mli | 3 ++ test-suite/success/unification.v | 50 +++++++++++++++++++ 5 files changed, 185 insertions(+), 42 deletions(-) create mode 100644 test-suite/success/unification.v diff --git a/CHANGES b/CHANGES index c1daeecbd..97c02e6c7 100644 --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,9 @@ +Changes from V8.1beta to V8.1 +============================= + +- Support for Miller-Pfenning's patterns unification in type synthesis + (e.g. can infer P such that P x y = phi(x,y)) + Changes from V8.0 to V8.1 ========================= diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 923903bdb..c709a62b4 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -8,12 +8,14 @@ (* $Id$ *) +open Pp open Util open Names open Term open Closure open Reduction open Reductionops +open Termops open Environ open Typing open Classops @@ -83,7 +85,7 @@ let evar_apprec env isevars stack c = | Evar (n,_ as ev) when Evd.is_defined sigma n -> aux (Evd.existential_value sigma ev, stack) | _ -> (t, list_of_stack stack) - in aux (c, append_stack (Array.of_list stack) empty_stack) + in aux (c, append_stack_list stack empty_stack) let apprec_nohdbeta env isevars c = let (t,stack as s) = Reductionops.whd_stack c in @@ -126,7 +128,6 @@ let check_conv_record (t1,l1) (t2,l2) = with _ -> raise Not_found - (* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) @@ -229,7 +230,17 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Flexible ev1, MaybeFlexible flex2 -> let f1 i = - if List.length l1 <= List.length l2 then + if + is_unification_pattern l1 & + not (occur_evar (fst ev1) (applist (term2,l2))) + then + (* Miller-Pfenning's patterns unification *) + let t2 = solve_pattern_eqn env l1 (applist(term2,l2)) in + solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2) + else if + List.length l1 <= List.length l2 + then + (* Try first-order unification *) let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in ise_and i @@ -248,7 +259,17 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | MaybeFlexible flex1, Flexible ev2 -> let f1 i = - if List.length l2 <= List.length l1 then + if + is_unification_pattern l2 & + not (occur_evar (fst ev2) (applist (term1,l1))) + then + (* Miller-Pfenning's patterns unification *) + let t1 = solve_pattern_eqn env l2 (applist(term1,l1)) in + solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1) + else if + List.length l2 <= List.length l1 + then + (* Try first-order unification *) let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in ise_and i (* First compare extra args for better failure message *) @@ -273,8 +294,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = (try conv_record env i (try check_conv_record appr1 appr2 with Not_found -> check_conv_record appr2 appr1) -(* TODO: remove this _ !!! *) - with _ -> (i,false)) + with Not_found -> (i,false)) and f4 i = (* heuristic: unfold second argument first, exception made if the first argument is a beta-redex (expand a constant @@ -295,7 +315,17 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = ise_try isevars [f2; f3; f4] | Flexible ev1, Rigid _ -> - if (List.length l1 <= List.length l2) then + if + is_unification_pattern l1 & + not (occur_evar (fst ev1) (applist (term2,l2))) + then + (* Miller-Pfenning's patterns unification *) + let t2 = solve_pattern_eqn env l1 (applist(term2,l2)) in + solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2) + else if + List.length l1 <= List.length l2 + then + (* Try first-order unification *) let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in ise_and isevars (* First compare extra args for better failure message *) @@ -308,8 +338,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = else solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))] else (isevars,false) + | Rigid _, Flexible ev2 -> - if List.length l2 <= List.length l1 then + if + is_unification_pattern l2 & + not (occur_evar (fst ev2) (applist (term1,l1))) + then + (* Miller-Pfenning's patterns unification *) + let t1 = solve_pattern_eqn env l2 (applist(term1,l1)) in + solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1) + else if + List.length l2 <= List.length l1 + then + (* Try first-order unification *) let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in ise_and isevars (* First compare extra args for better failure message *) @@ -326,7 +367,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | MaybeFlexible flex1, Rigid _ -> let f3 i = (try conv_record env i (check_conv_record appr1 appr2) - with _ -> (i,false)) + with Not_found -> (i,false)) and f4 i = match eval_flexible_term env flex1 with | Some v1 -> @@ -337,8 +378,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Rigid _ , MaybeFlexible flex2 -> let f3 i = - (try (conv_record env i (check_conv_record appr2 appr1)) - with _ -> (i,false)) + (try conv_record env i (check_conv_record appr2 appr1) + with Not_found -> (i,false)) and f4 i = match eval_flexible_term env flex2 with | Some v2 -> @@ -468,7 +509,7 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = params1 params); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1); (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))] - + let the_conv_x env t1 t2 isevars = match evar_conv_x env isevars CONV t1 t2 with (evd',true) -> evd' diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 658bf407f..f803fd9d7 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -21,13 +21,6 @@ open Evd open Reductionops open Pretype_errors - -let rec filter_unique = function - | [] -> [] - | x::l -> - if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l) - else x::filter_unique l - (* Expanding existential variables (pretyping.ml) *) (* 1- whd_ise fails if an existential is undefined *) @@ -310,29 +303,45 @@ let is_defined_equation env evd (ev,inst) rhs = * ?3 <-- ?1 no pb: env of ?3 is larger than ?1's * ?1 <-- (list ?2) pb: ?2 may depend on x, but not ?1. * What we do is that ?2 is defined by a new evar ?4 whose context will be - * a prefix of ?2's env, included in ?1's env. *) + * a prefix of ?2's env, included in ?1's env. -let do_restrict_hyps evd ev args = + Concretely, the assumptions are "env |- ev : T" and "Gamma |- + ev[hyps:=args]" for some Gamma whose de Bruijn context has length k. + We create "env' |- ev' : T" for some env' <= env and define ev:=ev' +*) + +let do_restrict_hyps env k evd ev args = let args = Array.to_list args in let evi = Evd.find (evars_of !evd) ev in - let env = evar_env evi in let hyps = evar_context evi in - let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in + let (hyps',ncargs) = list_filter2 (fun _ a -> closedn k a) (hyps,args) in (* No care is taken in case the evar type uses vars filtered out! - Is it important ? *) - let nc = - let env = - Sign.fold_named_context push_named sign ~init:(reset_context env) in - e_new_evar evd env ~src:(evar_source ev !evd) evi.evar_concl in + Assuming that the restriction comes from a well-typed Flex/Flex + unification problem (see real_clean), the type of the evar cannot + depend on variables that are not in the scope of the other evar, + since this other evar has the same type (up to unification). + Since moreover, the evar contexts uses names only, the + restriction raise no de Bruijn reallocation problem *) + let env' = + Sign.fold_named_context push_named hyps' ~init:(reset_context env) in + let nc = e_new_evar evd env' ~src:(evar_source ev !evd) evi.evar_concl in evd := Evd.evar_define ev nc !evd; let (evn,_) = destEvar nc in mkEvar(evn,Array.of_list ncargs) - -let need_restriction isevars args = not (array_for_all closed0 args) +let need_restriction k args = not (array_for_all (closedn k) args) (* We try to instantiate the evar assuming the body won't depend - * on arguments that are not Rels or Vars, or appearing several times. + * on arguments that are not Rels or Vars, or appearing several times + (i.e. we tackle only Miller-Pfenning patterns unification) + + 1) Let a unification problem "env |- ev[hyps:=args] = rhs" + 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs" + where only Rel's and Var's are relevant in subst + 3) We recur on rhs, "imitating" the term failing if some Rel/Var not in scope + + Note: we don't assume rhs in normal form, it may fail while it would + have succeeded after some reductions *) (* Note: error_not_clean should not be an error: it simply means that the * conversion test that lead to the faulty call to [real_clean] should return @@ -341,36 +350,52 @@ let need_restriction isevars args = not (array_for_all closed0 args) let real_clean env isevars ev evi args rhs = let evd = ref isevars in - let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in + let subst = List.map (fun (x,y) -> (y,mkVar x)) (list_uniquize args) in let rec subs rigid k t = match kind_of_term t with | Rel i -> if i<=k then t - else (try List.assoc (mkRel (i-k)) subst with Not_found -> t) + else + (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *) + (try List.assoc (mkRel (i-k)) subst + with Not_found -> if rigid then raise Exit else t) | Evar (ev,args) -> if Evd.is_defined_evar !evd (ev,args) then subs rigid k (existential_value (evars_of !evd) (ev,args)) else + (* Flex/Flex problem: restriction to a common scope *) let args' = Array.map (subs false k) args in - if need_restriction !evd args' then - do_restrict_hyps evd ev args' + if need_restriction k args' then + do_restrict_hyps (reset_context env) k evd ev args' else mkEvar (ev,args') | Var id -> + (* Flex/Var problem: unifiable as a pattern iff Var in scope of ev *) (try List.assoc t subst with Not_found -> if not rigid + (* I don't understand this line: vars from evar_context evi + are private (especially some of them are freshly + generated in push_rel_context_to_named_context). They + have a priori nothing to do with the vars in env. I + remove the test [HH 25/8/06] + or List.exists (fun (id',_,_) -> id=id') (evar_context evi) + *) then t - else - error_not_clean env (evars_of !evd) ev rhs - (evar_source ev !evd)) - | _ -> map_constr_with_binders succ (subs rigid) k t + else raise Exit) + + | _ -> + (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *) + map_constr_with_binders succ (subs rigid) k t in - let body = subs true 0 (nf_evar (evars_of isevars) rhs) in - if not (closed0 body) - then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd); + let rhs = nf_evar (evars_of isevars) rhs in + let rhs = whd_beta rhs (* heuristic *) in + let body = + try subs true 0 rhs + with Exit -> + error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in (!evd,body) (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated @@ -464,6 +489,24 @@ let head_evar = in hrec +(* Check if an applied evar "?X[args] l" is a Miller's pattern; note + 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 l = + List.for_all isRel l & list_uniquize l = l + +(* From a unification problem "?X l1 = term1 l2" such that l1 is made + of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *) + +let solve_pattern_eqn env l1 c = + let c' = List.fold_right (fun a c -> + let c' = subst_term (lift 1 a) (lift 1 c) in + let n = destRel a in + let (na,_,t) = lookup_rel n env (* if na defined, do as if assumption *) in + (mkLambda (na,lift n t,c'))) l1 c in + whd_eta c' + (* This code (i.e. solve_pb, etc.) takes a unification * problem, and tries to solve it. If it solves it, then it removes * all the conversion problems, and re-runs conversion on each one, in diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 6ce30ff79..2aceece0b 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -82,6 +82,9 @@ val define_evar_as_arrow : 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 : constr list -> bool +val solve_pattern_eqn : env -> constr list -> constr -> constr + (***********************************************************) (* Value/Type constraints *) diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v new file mode 100644 index 000000000..60c03831a --- /dev/null +++ b/test-suite/success/unification.v @@ -0,0 +1,50 @@ +(* Test patterns unification *) + +Lemma l1 : (forall P, (exists x:nat, P x) -> False) + -> forall P, (exists x:nat, P x /\ P x) -> False. +Proof. +intros; apply (H _ H0). +Qed. + +Lemma l2 : forall A:Set, forall Q:A->Set, + (forall (P: forall x:A, Q x -> Prop), + (exists x:A, exists y:Q x, P x y) -> False) + -> forall (P: forall x:A, Q x -> Prop), + (exists x:A, exists y:Q x, P x y /\ P x y) -> False. +Proof. +intros; apply (H _ H0). +Qed. + + +(* Example submitted for Zenon *) + +Axiom zenon_noteq : forall T : Type, forall t : T, ((t <> t) -> False). +Axiom zenon_notall : forall T : Type, forall P : T -> Prop, + (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False). + + (* Must infer "P := fun x => x=x" in zenon_notall *) +Check (fun _h1 => (zenon_notall nat _ (fun _T_0 => + (fun _h2 => (zenon_noteq _ _T_0 _h2))) _h1)). + + +(* Core of an example submitted by Ralph Matthes (#849) + + It used to fail because of the K-variable x in the type of "sum_rec ..." + which was not in the scope of the evar ?B. Solved by a head + beta-reduction of the type "(fun _ : unit + unit => L unit) x" of + "sum_rec ...". Shall we used more reduction when solving evars (in + real_clean)?? Is there a risk of starting too long reductions? + + Note that the example originally came from a non re-typable + pretty-printed term (the checked term is actually re-printed the + same form it is checked). +*) + +Set Implicit Arguments. +Inductive L (A:Set) : Set := c : A -> L A. +Parameter f: forall (A:Set)(B:Set), (A->B) -> L A -> L B. +Parameter t: L (unit + unit). + +Check (f (fun x : unit + unit => + sum_rec (fun _ : unit + unit => L unit) + (fun y => c y) (fun y => c y) x) t). -- cgit v1.2.3