helm/software/components/ng_kernel/check.ml

   1 let _ =
   2   NCicTypeChecker.set_logger
   3     (function
   4     | `Start_type_checking s -> ()
   5 (*        prerr_endline ("Start: " ^ NUri.string_of_uri s) *)
   6     | `Type_checking_completed s ->  ()
   7 (*        prerr_endline ("End: " ^ NUri.string_of_uri s) *)
   8        );
   9   NCicPp.set_ppterm NCicPp.trivial_pp_term;
  10   Helm_registry.load_from "conf.xml";
  11   let alluris =
  12     try
  13       let s = Sys.argv.(1) in
  14       if s = "-alluris" then
  15        begin
  16         let uri_re = Str.regexp ".*\\(ind\\|var\\|con\\)$" in
  17         let uris = Http_getter.getalluris () in
  18         let alluris = List.filter (fun u -> Str.string_match uri_re u 0) uris in
  19         let oc = open_out "alluris.txt" in
  20         List.iter (fun s -> output_string oc (s^"\n")) alluris;
  21         close_out oc;
  22         []
  23        end
  24       else [s]
  25     with Invalid_argument _ ->
  26       let r = ref [] in
  27       let ic = open_in "alluris.txt" in
  28       try while true do r := input_line ic :: !r; done; []
  29       with _ -> List.rev !r
  30   in
  31   let alluris =
  32     HExtlib.filter_map
  33       (fun u -> try Some (NUri.nuri_of_ouri (UriManager.uri_of_string u)) with _
  34       -> None) alluris
  35   in
  36   prerr_endline "caching objects";
  37   List.iter (fun uu ->
  38 (*     prerr_endline ("************* INIZIO **************** " ^ NUri.string_of_uri uu); *)
  39     let _,o = NCicEnvironment.get_obj uu in
  40     try
  41       NCicTypeChecker.typecheck_obj o;
  42 (*       prerr_endline ("************* FINE ****************" ^ NUri.string_of_uri uu); *)
  43     with
  44     | NCicTypeChecker.AssertFailure s
  45     | NCicTypeChecker.TypeCheckerFailure s as e ->
  46 (*        prerr_endline ("Obj: " ^ NCicPp.ppobj o); *)
  47        prerr_endline (Lazy.force s); raise e
  48     | CicEnvironment.Object_not_found s ->
  49                     prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s);
  50     )
  51   alluris;
  52   NCicEnvironment.invalidate ();
  53   Gc.compact ();
  54   let prima = Unix.gettimeofday () in
  55   List.iter
  56     (fun u -> NCicTypeChecker.typecheck_obj (snd (NCicEnvironment.get_obj u)))
  57     alluris;
  58   let dopo = Unix.gettimeofday () in
  59   Gc.compact ();
  60   let dopo2 = Unix.gettimeofday () in
  61   Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n" (dopo -. prima) (dopo2 -.  dopo);
  62   CicEnvironment.invalidate ();
  63   let alluris = List.map NUri.ouri_of_nuri alluris in
  64   Gc.compact ();
  65   let prima = Unix.gettimeofday () in
  66   List.iter (fun u -> ignore (CicTypeChecker.typecheck u)) alluris;
  67   let dopo = Unix.gettimeofday () in
  68   Gc.compact ();
  69   let dopo2 = Unix.gettimeofday () in
  70   Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n" (dopo -. prima) (dopo2 -. dopo)
  71 ;;