X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=f544d8daeed54aad2216322cc09f344e6bfacfa8;hb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;hp=3b951bec268157e8903d1c8d81364a82c9a16c4f;hpb=4ff2055cabd4ac273b7222f6cf21aedbff5c022d;p=helm.git

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 3b951bec2..f544d8dae 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -169,6 +169,17 @@ let _ =
   in
   prerr_endline "ranked....";
   prerr_endline (NCicEnvironment.pp_constraints ());
+(*
+  let [_,type0_uri] = mk_type 0 in
+  let [_,type1_uri] = mk_type 1 in
+  let [_,type2_uri] = mk_type 2 in
+  prerr_endline 
+   ("Min:" ^ 
+   (match NCicEnvironment.sup [true,type0_uri;true,type2_uri] with
+       | None -> "NO SUP"
+       | Some t -> NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] 
+          (NCic.Sort (NCic.Type t))));
+*)
   HExtlib.profiling_enabled := false;
   List.iter (fun uu ->
     let uu= OCic2NCic.nuri_of_ouri uu in
@@ -176,13 +187,13 @@ let _ =
     let o = NCicLibrary.get_obj uu in
     if print_object then prerr_endline (NCicPp.ppobj o); 
     try 
-      NCicTypeChecker.typecheck_obj o
+      NCicEnvironment.check_and_add_obj o
     with 
     | NCicTypeChecker.AssertFailure s 
     | NCicTypeChecker.TypeCheckerFailure s
     | NCicEnvironment.ObjectNotFound s
     | NCicEnvironment.BadConstraint s
-    | NCicEnvironment.BadDependency s as e -> 
+    | NCicEnvironment.BadDependency (s,_) as e -> 
        prerr_endline ("######### " ^ Lazy.force s);
        if not ignore_exc then raise e
     )
@@ -209,12 +220,15 @@ let _ =
             | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
               when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
                 let metasenv, ty =  perforate ctx metasenv ty in
-                let a,b,_ = NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b
+                let a,_,b,_ = 
+                  NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b
             | t -> 
                 NCicUntrusted.map_term_fold_a
                  (fun e ctx -> e::ctx) ctx perforate metasenv t
           in
           let rec curryfy ctx = function
+            | NCic.Lambda (name, (NCic.Sort _ as s), tgt) ->
+                NCic.Lambda (name, s, curryfy ((name,NCic.Decl s) :: ctx) tgt)
             | NCic.Lambda (name, s, tgt) ->
                 let tgt = curryfy ((name,NCic.Decl s) :: ctx) tgt in
                 NCic.Lambda (name, NCic.Implicit `Type, tgt)
@@ -254,52 +268,60 @@ let _ =
                  (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx ity)
                  (NCicPp.ppterm ~metasenv:metasenv ~subst:[] ~context:ctx sty));
 *)
-          let metasenv, subst, bo, infty = 
-            let bo = curryfy [] bo in
-            try NCicRefiner.typeof [] [] [] bo None
-            with
-            | NCicRefiner.RefineFailure msg 
-            | NCicRefiner.Uncertain msg ->
-               let _, msg = Lazy.force msg in
-               prerr_endline msg;
-               assert false
-          in
-          let metasenv, subst = 
-            try 
-              NCicUnification.unify metasenv subst [] infty ty
-            with
-            | NCicUnification.Uncertain msg 
-            | NCicUnification.UnificationFailure msg 
-            | NCicMetaSubst.MetaSubstFailure msg ->
-                prerr_endline (Lazy.force msg); 
-                metasenv, subst
-            | Sys.Break -> metasenv, subst
-          in
-          if (NCicReduction.are_convertible ~subst [] infty ty)
-          then
-            prerr_endline ("OK: " ^ NUri.string_of_uri u)
-          else
-            (
-          let ctx = [] in
-          let right = infty in
-          let left = ty in
-                    
-                    prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
-                prerr_endline 
-                 (Printf.sprintf 
-                   ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmetasenv:\n%s\n" ^^ 
-                   "context:\n%s\nTERMS NO SUBST:\n%s\n==\n%s\n"^^
-                   "TERMS:\n%s\n==\n%s\n")
-                 (NCicPp.ppsubst ~metasenv subst)
-                 (NCicPp.ppmetasenv ~subst metasenv)
-                 (NCicPp.ppcontext ~metasenv ~subst ctx)
-                 (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx left)
-                 (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx right)
-                 (NCicPp.ppterm ~metasenv ~subst ~context:ctx left)
-                 (NCicPp.ppterm ~metasenv ~subst ~context:ctx right) ))
-          (*let inferred_ty = 
-            NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
-          in*)
+          prerr_endline ("start: " ^ NUri.string_of_uri u);
+          let bo = curryfy [] bo in
+          (try 
+            let rdb = new NRstatus.status in
+            let metasenv, subst, bo, infty = 
+              NCicRefiner.typeof rdb [] [] [] bo None
+            in
+            let metasenv, subst = 
+              try 
+                NCicUnification.unify rdb metasenv subst [] infty ty
+              with
+              | NCicUnification.Uncertain msg 
+              | NCicUnification.UnificationFailure msg 
+              | NCicMetaSubst.MetaSubstFailure msg ->
+                  prerr_endline (Lazy.force msg); 
+                  metasenv, subst
+              | Sys.Break -> metasenv, subst
+            in
+            if (NCicReduction.are_convertible ~metasenv ~subst [] infty ty)
+            then
+              prerr_endline ("OK: " ^ NUri.string_of_uri u)
+            else
+              (
+            let ctx = [] in
+            let right = infty in
+            let left = ty in
+                      
+                      prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+                  prerr_endline 
+                   (Printf.sprintf 
+                     ("\t\tRESULT OF UNIF\n\nsubst:\n%s\nmetasenv:\n%s\n" ^^ 
+                     "context:\n%s\nTERMS NO SUBST:\n%s\n==\n%s\n"^^
+                     "TERMS:\n%s\n==\n%s\n")
+                   (NCicPp.ppsubst ~metasenv subst)
+                   (NCicPp.ppmetasenv ~subst metasenv)
+                   (NCicPp.ppcontext ~metasenv ~subst ctx)
+                   (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx left)
+                   (NCicPp.ppterm ~metasenv ~subst:[] ~context:ctx right)
+                   (NCicPp.ppterm ~metasenv ~subst ~context:ctx left)
+                   (NCicPp.ppterm ~metasenv ~subst ~context:ctx right) ))
+            (*let inferred_ty = 
+              NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
+            in*)
+          with
+          | Sys.Break -> ()
+          | NCicRefiner.RefineFailure msg 
+          | NCicRefiner.Uncertain msg ->
+             let _, msg = Lazy.force msg in
+             prerr_endline msg;
+             prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+          | e -> 
+             prerr_endline (Printexc.to_string e); 
+             prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+             )
       | _ -> ())
     alluris;
 ;;