From cdce80d3615fa6ba24e20ed5c9e1f55622ddd755 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 29 Sep 2008 12:07:33 +0000 Subject: [PATCH] ... --- .../components/ng_refiner/nCicUnification.ml | 54 +++++++++---------- 1 file changed, 25 insertions(+), 29 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 98b06f94e..147bb555f 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -39,34 +39,26 @@ let flexible l = exception WrongShape;; -let eta_reduce after_beta_expansion after_beta_expansion_body - before_beta_expansion - = - 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] -> [] - | [_] -> if check_last then raise WrongShape else [] - | he::tl -> he::(all_but_last check_last tl) - in - let all_but_last check_last l = - match all_but_last check_last l with - | [] -> assert false - | [he] -> he - | l -> NCic.Appl 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 eta_reduce = + let delift_if_not_occur body orig = + try + NCicSubstitution.psubst ~avoid_beta_redexes:true + (fun () -> raise WrongShape) [()] body + with WrongShape -> orig + in + function + | NCic.Lambda(name, src, NCic.Appl [hd; NCic.Rel 1]) as orig -> + delift_if_not_occur hd orig + | NCic.Lambda(name, src, NCic.Appl (hd :: l)) as orig + when HExtlib.list_last l = NCic.Rel 1 -> + let body = + let args, _ = Hextlib.split_nth (List.length l - 1) l in + NCic.Appl (hd::args) + in + delift_if_not_occur body orig + | t -> 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 @@ -100,8 +92,12 @@ let rec beta_expand num test_eq_only swap metasenv subst context t arg = let fresh_name = "Hbeta" ^ string_of_int num in 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 + let t2 = eta_reduce (C.Lambda (fresh_name,argty,t1)) in + try + ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2); + metasenv, subst, t2 + with NCicTypeChecker.TypeCheckerFailure _ -> + NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg) and beta_expand_many test_equality_only metasenv subst context t args ugraph = let _, subst, metasenv, hd = -- 2.39.2