From 2e6a92bad35a8f8883c498c6a2f36ea3208d4ddd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 17 Oct 2010 09:12:29 +0000 Subject: [PATCH] backport of patches to unification --- .../components/ng_paramodulation/orderings.ml | 3 +- matita/components/ng_refiner/nCicMetaSubst.ml | 15 ++-- .../components/ng_refiner/nCicMetaSubst.mli | 2 + .../components/ng_refiner/nCicUnification.ml | 68 ++++++++++++++----- 4 files changed, 61 insertions(+), 27 deletions(-) diff --git a/matita/components/ng_paramodulation/orderings.ml b/matita/components/ng_paramodulation/orderings.ml index 1e143605b..f7062b3ab 100644 --- a/matita/components/ng_paramodulation/orderings.ml +++ b/matita/components/ng_paramodulation/orderings.ml @@ -40,7 +40,8 @@ let rec eq_foterm f x y = match x, y with | Terms.Leaf t1, Terms.Leaf t2 -> f t1 t2 | Terms.Var i, Terms.Var j -> i = j - | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2 + | Terms.Node l1, Terms.Node l2 when List.length l1 = List.length l2 -> + List.for_all2 (eq_foterm f) l1 l2 | _ -> false ;; diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml index 8bc281953..b18364509 100644 --- a/matita/components/ng_refiner/nCicMetaSubst.ml +++ b/matita/components/ng_refiner/nCicMetaSubst.ml @@ -259,16 +259,16 @@ and restrict metasenv subst i (restrictions as orig) = | NCicUtils.Meta_not_found _ -> assert false ;; -let rec flexible_arg context subst = function +let rec is_flexible context ~subst = function | NCic.Meta (i,_) -> (try let _,_,t,_ = List.assoc i subst in - flexible_arg context subst t + is_flexible context ~subst t with Not_found -> true) | NCic.Appl (NCic.Meta (i,_) :: args)-> (try let _,_,t,_ = List.assoc i subst in - flexible_arg context subst + is_flexible context ~subst (NCicReduction.head_beta_reduce ~delta:max_int (NCic.Appl (t :: args))) with Not_found -> true) @@ -283,7 +283,7 @@ let rec flexible_arg context subst = function match List.nth context (i-1) with | _,NCic.Def (bo,_) -> - flexible_arg context subst + is_flexible context ~subst (NCicSubstitution.lift i bo) | _ -> false with @@ -332,11 +332,11 @@ let delift ~unify metasenv subst context n l t = match l with | _, NCic.Irl _ -> fun _ _ _ _ _ -> None | shift, NCic.Ctx l -> fun metasenv subst context k t -> - if flexible_arg context subst t || contains_in_scope subst t then None else + if is_flexible context ~subst t || contains_in_scope subst t then None else let lb = List.map (fun t -> let t = NCicSubstitution.lift (k+shift) t in - t, flexible_arg context subst t) + t, is_flexible context ~subst t) l in HExtlib.list_findopt @@ -349,9 +349,6 @@ let delift ~unify metasenv subst context n l t = lb in let rec aux (context,k,in_scope) (metasenv, subst as ms) t = - (* XXX if t is closed, we should just terminate. Speeds up hints! *) - if NCicUntrusted.looks_closed t then ms, t - else match unify_list in_scope metasenv subst context k t with | Some x -> x | None -> diff --git a/matita/components/ng_refiner/nCicMetaSubst.mli b/matita/components/ng_refiner/nCicMetaSubst.mli index a195a2fd8..1c96577a7 100644 --- a/matita/components/ng_refiner/nCicMetaSubst.mli +++ b/matita/components/ng_refiner/nCicMetaSubst.mli @@ -71,3 +71,5 @@ val pack_lc : int * NCic.lc_kind -> int * NCic.lc_kind val is_out_scope_tag : NCic.meta_attrs -> bool val int_of_out_scope_tag : NCic.meta_attrs -> int + +val is_flexible : NCic.context -> subst:NCic.substitution -> NCic.term -> bool diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml index 13744017a..dd1e4b80c 100644 --- a/matita/components/ng_refiner/nCicUnification.ml +++ b/matita/components/ng_refiner/nCicUnification.ml @@ -566,24 +566,58 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap = instantiate rdb test_eq_only metasenv subst context n lc (NCicReduction.head_beta_reduce ~subst t) (not swap) + (* higher order unification case *) | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ -> - let metasenv, lambda_Mj = - lambda_intros rdb metasenv subst context (List.length args) - (NCicTypeChecker.typeof ~metasenv ~subst context meta) - in - let metasenv, subst = - unify rdb test_eq_only metasenv subst context - (C.Meta (i,l)) lambda_Mj swap - in - let metasenv, subst = - unify rdb test_eq_only metasenv subst context t1 t2 swap - in - (try - let name, ctx, term, ty = NCicUtils.lookup_subst i subst in - let term = eta_reduce subst term in - let subst = List.filter (fun (j,_) -> j <> i) subst in - metasenv, ((i, (name, ctx, term, ty)) :: subst) - with Not_found -> assert false) + (* this easy_case handles "(? ?) =?= (f a)", same number of + * args, preferring the instantiation "f" over "\_.f a" for the + * metavariable in head position. Since the arguments of the meta + * are flexible, delift would ignore them generating a constant + * function even in the easy case above *) + let easy_case = + match t2 with + | NCic.Appl (f :: f_args) + when List.length args = List.length f_args && + List.exists (NCicMetaSubst.is_flexible context ~subst) args -> + (try + let metasenv, subst = + unify rdb test_eq_only metasenv subst context meta f swap + in + Some (List.fold_left2 + (fun (m, s) t1 t2 -> + unify rdb test_eq_only m s context t1 t2 swap) + (metasenv, subst) args f_args) + with UnificationFailure _ | Uncertain _ | KeepReducing _ -> + None) + | _ -> None + in + (match easy_case with + | Some ms -> ms + | None -> + (* This case handles "(?_f ..ti..) =?= t2", abstracting every + * non flexible ti (delift skips local context items that are + * flexible) from t2 in two steps: + * 1) ?_f := \..xi.. .? + * 2) ?_f ..ti.. =?= t2 --unif_machines--> + ?_f[..ti..] =?= t2 --instantiate--> + delift [..ti..] t2 *) + let metasenv, lambda_Mj = + lambda_intros rdb metasenv subst context (List.length args) + (NCicTypeChecker.typeof ~metasenv ~subst context meta) + in + let metasenv, subst = + unify rdb test_eq_only metasenv subst context + (C.Meta (i,l)) lambda_Mj swap + in + let metasenv, subst = + unify rdb test_eq_only metasenv subst context t1 t2 swap + in + (try + let name, ctx, term, ty = NCicUtils.lookup_subst i subst in + let term = eta_reduce subst term in + let subst = List.filter (fun (j,_) -> j <> i) subst in + metasenv, ((i, (name, ctx, term, ty)) :: subst) + with Not_found -> assert false)) + | _, NCic.Appl (NCic.Meta (_,_) :: _) -> unify rdb test_eq_only metasenv subst context t2 t1 (not swap) -- 2.39.2