...

[helm.git] / helm / software / components / ng_refiner / check.ml

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index bb423690b177a2865aae6b19914822e555ffa61f..4cb18817012d7fb6de7f5432668cddeb494447f8 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -53,15 +53,15 @@ let logger =
 
 let mk_type n = 
   if n = 0 then
-     [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+     [`Type, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-     [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+     [`Type, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 let mk_cprop n = 
   if n = 0 then 
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
   else
-    [false, NUri.uri_of_string ("cic:/matita/pts/CProp"^string_of_int n^".univ")]
+    [`CProp, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
 ;;
 
 
@@ -151,16 +151,9 @@ let _ =
     try
     let rec aux = function
       | a::(b::_ as tl) ->
-         NCicEnvironment.add_constraint true (mk_type a) (mk_type b);
-         NCicEnvironment.add_constraint true (mk_cprop a) (mk_cprop b);
-         NCicEnvironment.add_constraint true (mk_cprop a) (mk_type b);
-         NCicEnvironment.add_constraint true (mk_type a) (mk_cprop b);
-         NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
-         NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
+         NCicEnvironment.add_lt_constraint (mk_type a) (mk_type b);
+         NCicEnvironment.add_lt_constraint (mk_cprop a) (mk_cprop b);
          aux tl
-      | [a] -> 
-         NCicEnvironment.add_constraint false (mk_type a) (mk_cprop a);
-         NCicEnvironment.add_constraint false (mk_cprop a) (mk_type a);
       | _ -> ()
     in
        aux lll
@@ -187,13 +180,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
     )
@@ -220,12 +213,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)
@@ -268,12 +264,13 @@ let _ =
           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 [] [] [] bo None
+              NCicRefiner.typeof rdb [] [] [] bo None
             in
             let metasenv, subst = 
               try 
-                NCicUnification.unify metasenv subst [] infty ty
+                NCicUnification.unify rdb metasenv subst [] infty ty
               with
               | NCicUnification.Uncertain msg 
               | NCicUnification.UnificationFailure msg 
@@ -282,7 +279,7 @@ let _ =
                   metasenv, subst
               | Sys.Break -> metasenv, subst
             in
-            if (NCicReduction.are_convertible ~subst [] infty ty)
+            if (NCicReduction.are_convertible ~metasenv ~subst [] infty ty)
             then
               prerr_endline ("OK: " ^ NUri.string_of_uri u)
             else
@@ -308,11 +305,16 @@ let _ =
               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))
+             prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+          | e -> 
+             prerr_endline (Printexc.to_string e); 
+             prerr_endline ("FAIL: " ^ NUri.string_of_uri u)
+             )
       | _ -> ())
     alluris;
 ;;