better test

[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 c1ce4260794ce9bb4388dc6a3f756f34eaa2ab5b..3a155329e679ba235f2c5da77987ae69455b96c4 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -66,6 +66,7 @@ let mk_cprop n =
 
 
 let _ =
+  Sys.catch_break true;
   let do_old_logging = ref true in
   HelmLogger.register_log_callback
    (fun ?append_NL html_msg ->
@@ -73,7 +74,6 @@ let _ =
       prerr_endline (HelmLogger.string_of_html_msg html_msg));
   CicParser.impredicative_set := false;
   NCicTypeChecker.set_logger logger;
-  NCicPp.set_ppterm NCicPp.trivial_pp_term;
   Helm_registry.load_from "conf.xml";
   let alluris = 
     try
@@ -193,23 +193,60 @@ let _ =
   NCicTypeChecker.set_logger (fun _ -> ());
   do_old_logging := false;
   prerr_endline "typechecking, first with the new and then with the old kernel";
-  let prima = Unix.gettimeofday () in
   List.iter 
     (fun u ->
-       let u= OCic2NCic.nuri_of_ouri u in
+      let u = OCic2NCic.nuri_of_ouri u in
       indent := 0;
-      NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u))
+      match NCicLibrary.get_obj u with
+      | _,_,_,_,NCic.Constant (_,_,Some bo, ty, _) ->
+          let rec intros = function
+            | NCic.Prod (name, s, t) ->
+                let ctx, t = intros t in
+                ctx @ [(name, (NCic.Decl s))] , t
+            | t -> [], t
+          in
+          let ctx, ity = intros ty in
+          let sty, menv, _ = 
+            NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
+          in
+          let ctx, ty = intros ty in
+          let whd ty =
+            match ty with
+            | NCic.Appl [eq;t;a;b] ->
+               NCic.Appl [eq;t;NCicReduction.whd ~delta:0 ctx a;b]
+            | t -> NCicReduction.whd ~delta:0 ctx t
+          in
+(*
+                prerr_endline 
+                 (Printf.sprintf "%s == %s"
+                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
+                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
+*)
+          let metasenv, subst = 
+            try 
+(*                     prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *)
+              NCicUnification.unify menv [] ctx ity (whd sty) 
+            with
+            | NCicUnification.Uncertain msg 
+            | NCicUnification.UnificationFailure msg 
+            | NCicMetaSubst.MetaSubstFailure msg ->
+                prerr_endline (Lazy.force msg); 
+                prerr_endline 
+                 (Printf.sprintf "RESULT OF UNIF\n%s\n%s == %s\n"
+                 (NCicPp.ppcontext ~metasenv:menv ~subst:[] ctx)
+                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
+                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
+                [], []
+            | Sys.Break -> [],[]
+          in
+          if (NCicReduction.are_convertible ~subst ctx ity sty)
+          then
+            prerr_endline ("OK: " ^ NUri.string_of_uri u)
+          else
+            prerr_endline ("FAIL: " ^ NUri.string_of_uri u);
+          (*let inferred_ty = 
+            NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] bo
+          in*)
+      | _ -> ())
     alluris;
-  let dopo = Unix.gettimeofday () in
-  Gc.compact ();
-  let dopo2 = Unix.gettimeofday () in
-  Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -.  dopo);
-  CicEnvironment.invalidate ();
-  Gc.compact ();
-  let prima = Unix.gettimeofday () in
-  List.iter (fun u -> ignore (CicTypeChecker.typecheck u)) alluris;
-  let dopo = Unix.gettimeofday () in
-  Gc.compact ();
-  let dopo2 = Unix.gettimeofday () in
-  Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo)
 ;;