From 53bd7590de050214164c4f6b5181699dc38056f6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 24 Jul 2009 21:49:56 +0000 Subject: [PATCH] Beta-expansion was avoided as soon as one argument was flexible. This lead to a different behaviour in the following two unification problems: (\lambda_.?) ? =?= T vs ? ? =?= T or, equivalently ?[?] =?= T The fix is very easy: we always perform beta-expansion and delifting will take care of ignoring the flexible "arguments", both during beta-expansion and during the unification that follows. --- .../components/ng_refiner/nCicMetaSubst.ml | 2 - .../components/ng_refiner/nCicMetaSubst.mli | 2 - .../components/ng_refiner/nCicUnification.ml | 78 +++++++++---------- 3 files changed, 36 insertions(+), 46 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index a445d16be..d18dd1b9d 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -215,8 +215,6 @@ let rec flexible_arg subst = function | _ -> false ;; -let flexible subst l = List.exists (flexible_arg subst) l;; - let in_scope_tag = "tag:in_scope" ;; let out_scope_tag_prefix = "tag:out_scope:" let out_scope_tag n = out_scope_tag_prefix ^ string_of_int n ;; diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 7bde2c1d6..92cfa0908 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -57,8 +57,6 @@ val saturate: NCic.context -> NCic.term -> int -> NCic.term * NCic.metasenv * NCic.term list -val flexible: NCic.substitution -> NCic.term list -> bool - val in_scope_tag : string val out_scope_tag : int -> string val is_out_scope_tag : string -> bool diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index be7a2fe4c..795b85042 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -343,9 +343,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = | _, NCic.Meta (n, _) when is_locked n subst -> (let (metasenv, subst), i = match NCicReduction.whd ~subst context t1 with - | NCic.Appl (NCic.Meta (i,l)::args) when - not (NCicMetaSubst.flexible subst args) - -> + | NCic.Appl (NCic.Meta (i,l)::args) -> let metasenv, subst, lambda_Mj = lambda_intros rdb metasenv subst context t1 args in @@ -423,45 +421,41 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = with Invalid_argument _ -> raise (fail_exc metasenv subst context t1 t2)) - | NCic.Appl (NCic.Meta (i,l)::args), _ when - not (NCicMetaSubst.flexible subst args) -> - (* we verify that none of the args is a Meta, - since beta expanding w.r.t a metavariable makes no sense *) - let metasenv, subst, lambda_Mj = - lambda_intros rdb metasenv subst context t1 args - in - let metasenv, subst = - unify rdb test_eq_only metasenv subst context - (C.Meta (i,l)) lambda_Mj - in - let metasenv, subst = - unify rdb test_eq_only metasenv subst context t1 t2 - 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 (i,l)::args) when - not(NCicMetaSubst.flexible subst args) -> - let metasenv, subst, lambda_Mj = - lambda_intros rdb metasenv subst context t2 args - in - let metasenv, subst = - unify rdb test_eq_only metasenv subst context - lambda_Mj (C.Meta (i,l)) - in - let metasenv, subst = - unify rdb test_eq_only metasenv subst context t1 t2 - 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 (i,l)::args), _ -> + let metasenv, subst, lambda_Mj = + lambda_intros rdb metasenv subst context t1 args + in + let metasenv, subst = + unify rdb test_eq_only metasenv subst context + (C.Meta (i,l)) lambda_Mj + in + let metasenv, subst = + unify rdb test_eq_only metasenv subst context t1 t2 + 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 (i,l)::args) -> + let metasenv, subst, lambda_Mj = + lambda_intros rdb metasenv subst context t2 args + in + let metasenv, subst = + unify rdb test_eq_only metasenv subst context + lambda_Mj (C.Meta (i,l)) + in + let metasenv, subst = + unify rdb test_eq_only metasenv subst context t1 t2 + 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) (* processing this case here we avoid a useless small delta step *) | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) -- 2.39.2