From 3b4ec24b0bf7b1cd23cdc632fa3fcbb9dbbda139 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 17 Oct 2010 09:08:05 +0000 Subject: [PATCH] new case for higher order unification: (? ?) =?= (f x) is not handled by delift, since flexible arguments in the local context are skipped by delift, resulting in the instantiation of the head meta to a constant function, even if the rhs is structurally the same. --- .../components/ng_refiner/nCicUnification.ml | 68 ++++++++++++++----- 1 file changed, 51 insertions(+), 17 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 13744017a..dd1e4b80c 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/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