From 4a102707c40a5b082a21c45330c3d2cd2a7a8614 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 25 Sep 2008 16:59:31 +0000 Subject: [PATCH] ... --- .../components/ng_refiner/nCicUnification.ml | 35 ++++++++++++------- 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index fa3ba4988..98b06f94e 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -45,6 +45,8 @@ let eta_reduce after_beta_expansion after_beta_expansion_body try match before_beta_expansion,after_beta_expansion_body with | NCic.Appl l1, NCic.Appl l2 -> + NCicUtils.does_not_occur 0 1 (NCic.Appl (List.tail (List.rev l2))) + ... let rec all_but_last check_last = function | [] -> assert false | [NCic.Rel 1] -> [] @@ -57,42 +59,49 @@ let eta_reduce after_beta_expansion after_beta_expansion_body | [he] -> he | l -> NCic.Appl l in - let t = - NCicSubstitution.subst (NCic.Sort NCic.Prop) (all_but_last true l2) in - let all_but_last = all_but_last false l in + let impossible_term = NCic.Rel ~-1 in + let t = NCicSubstitution.subst impossible_term (all_but_last true l2) in + let all_but_last = all_but_last false l1 in if t = all_but_last then all_but_last else after_beta_expansion | _ -> after_beta_expansion with WrongShape -> after_beta_expansion ;; -let rec beta_expand num test_equality_only metasenv subst context t arg = - let rec aux (n,context as k) (metasenv, subst as acc) t' = +let rec beta_expand num test_eq_only swap metasenv subst context t arg = + let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' = try let metasenv, subst = - unify (* test_equality_only *) metasenv subst context + unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t' in (metasenv, subst), C.Rel (1 + n) with Uncertain _ | UnificationFailure _ -> match t' with - | NCic.Rel m -> - (metasenv, subst), if m <= n then NCic.Rel m else NCic.Rel (m+1) + | NCic.Rel m orig -> + (metasenv, subst), if m <= n then orig else NCic.Rel (m+1) (* andrea: in general, beta_expand can create badly typed terms. This happens quite seldom in practice, UNLESS we iterate on the local context. For this reason, we renounce to iterate and just lift *) | NCic.Meta (i,(shift,lc)) -> (metasenv,subst), NCic.Meta (i,(shift+1,lc)) + | NCic.Prod (name, src, tgt) as orig -> + let (metasenv, subst), src1 = aux (n,context,true) acc src in + let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in + let (metasenv,subst), tgt1 = aux k (metasenv, subst) tgt in + if src == src1 && tgt == tgt1 then orig else + NCic.Prod (name, src1, tgt1) | t -> NCicUntrusted.map_term_fold_a - (fun e (n,ctx) -> n+i,e::ctx) k aux acc t + (fun e (n,ctx) -> n+1,e::ctx) k aux acc t in let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in let fresh_name = "Hbeta" ^ string_of_int num in - let (metasenv,subst), t = aux (0, context) (metasenv, subst) t in - let t = eta_reduce (C.Lambda (fresh_name,argty,t)) t t in - metasenv, subst, t + let (metasenv,subst,_), t1 = + aux (0, context, test_eq_only) (metasenv, subst) t in + let t2 = eta_reduce (C.Lambda (fresh_name,argty,t1)) t1 t in + metasenv, subst, t2 and beta_expand_many test_equality_only metasenv subst context t args ugraph = let _, subst, metasenv, hd = @@ -231,7 +240,7 @@ and unify metasenv subst context t1 t2 = (* we verify that none of the args is a Meta, since beta expanding w.r.t a metavariable makes no sense *) let subst, metasenv, beta_expanded = - beta_expand_many + beta_expand_many (* passare swap *) test_equality_only metasenv subst context t2 args ugraph in aux test_eq_only metasenv subst context -- 2.39.2