From 23b7119d915c6ff6ba3c89267bd91f7312afe619 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 13 Aug 2009 15:45:34 +0000 Subject: [PATCH] Let's refresh the universe to avoid assert failure. However, the effect of this is still unclear to me. --- .../software/components/ng_refiner/nCicUnification.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index ed650a3c3..325cd3e5f 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -104,13 +104,12 @@ let ppmetasenv ~subst:_subst _metasenv = "...";; let pp _ = ();; -let fix_sorts swap metasenv subst context meta t = +let fix_sorts swap exc t = let rec aux () = function | NCic.Sort (NCic.Type u) as orig -> if swap then match NCicEnvironment.sup u with - | None -> prerr_endline "no sup for" ; - raise (fail_exc metasenv subst context meta t) + | None -> prerr_endline "no sup for" ; raise exc | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1) else NCic.Sort (NCic.Type ( @@ -192,12 +191,13 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^ ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^ ppmetasenv ~subst metasenv)); + let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in let t, ty_t = try t, NCicTypeChecker.typeof ~subst ~metasenv context t with | NCicTypeChecker.AssertFailure msg -> (pp (lazy "fine typeof (fallimento)"); - let ft=fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t in + let ft = fix_sorts swap exc_to_be t in if ft == t then (prerr_endline ( ("ILLTYPED: " ^ NCicPp.ppterm ~metasenv ~subst ~context t @@ -217,6 +217,7 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = prerr_endline (Lazy.force msg); pp msg; assert false in + let ty_t = fix_sorts swap exc_to_be ty_t in let lty = NCicSubstitution.subst_meta lc ty in match ty_t with | NCic.Implicit _ -> @@ -352,7 +353,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = (C.Meta (i,l)) lambda_Mj, i | NCic.Meta (i,_) -> (metasenv, subst), i - | _ -> assert false + | _ -> prerr_endline ("XXX: " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.whd ~subst context t1)); assert false in let t1 = NCicReduction.whd ~subst context t1 in let j, lj = -- 2.39.2