From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 1 Oct 2009 08:46:53 +0000 (+0000)
Subject: sortification simplified
X-Git-Tag: make_still_working~3406
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7110ed13ffccb214bc3aafe37f6a7c24f59a49e5;p=helm.git

sortification simplified
---

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"))