From 7110ed13ffccb214bc3aafe37f6a7c24f59a49e5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 1 Oct 2009 08:46:53 +0000 Subject: [PATCH] sortification simplified --- .../components/ng_refiner/nCicUnification.ml | 29 +++++++------------ 1 file changed, 10 insertions(+), 19 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 8e3cf216e..e56832fd5 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -214,20 +214,14 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = let t, ty_t = try t, NCicTypeChecker.typeof ~subst ~metasenv context t with - | NCicTypeChecker.AssertFailure msg -> - pp(lazy("we try to fix the sort\n"^Lazy.force msg^"\n"^NCicPp.ppmetasenv ~subst - metasenv)); + | NCicTypeChecker.AssertFailure msg as exn -> + pp(lazy("we try to fix the sort\n"^ + Lazy.force msg^"\n"^NCicPp.ppmetasenv ~subst metasenv)); let ft = fix_sorts swap exc_to_be t in pp(lazy("unable to fix the sort")); - if ft == t then begin - raise (UnificationFailure (lazy ("unable to fix sorts of: "^ - NCicPp.ppterm ~metasenv ~subst ~context t))) - end; + if ft == t then raise exn; (try ft, NCicTypeChecker.typeof ~subst ~metasenv context ft - with NCicTypeChecker.AssertFailure _ -> - raise (UnificationFailure (lazy - ("fix sorts generated an ill-typed: "^ - NCicPp.ppterm ~metasenv ~subst ~context t)))) + with NCicTypeChecker.AssertFailure _ -> raise exn) | NCicTypeChecker.TypeCheckerFailure msg -> prerr_endline (Lazy.force msg); prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); @@ -264,7 +258,7 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = | _ -> false in let rec sortify metasenv subst = function - | NCic.Implicit (`Typeof _) + | NCic.Implicit (`Typeof _) -> assert false | NCic.Sort _ as t -> metasenv, subst, t, 0 | NCic.Meta (i,_) as t -> let tags, context, ty = NCicUtils.lookup_meta i metasenv in @@ -273,15 +267,12 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = let ty = NCicReduction.whd ~subst context ty in let metasenv, subst, ty, _ = sortify metasenv subst ty in let metasenv, j, m, _ = - NCicMetaSubst.mk_meta metasenv [] (`WithType ty) + NCicMetaSubst.mk_meta metasenv ~attrs:[`IsSort] [] (`WithType ty) in pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j)); - let metasenv,subst = unify test_eq_only metasenv subst context t m in - let j = if swap then i else j in - let tags, context, ty = NCicUtils.lookup_meta j metasenv in - let tags = `IsSort :: tags in - let metasenv = List.filter (fun x,_ -> x <> j) metasenv in - let metasenv = (j,(tags,context,ty)) ::metasenv in + let subst_entry = i, (tags, context, m, ty) in + let subst = subst_entry :: subst in + let metasenv = List.filter (fun x,_ -> i <> x) metasenv in metasenv, subst, m, j | t -> if could_reduce t then raise (Uncertain(lazy "not a sort")) -- 2.39.2