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   NCicPp.set_ppterm NCicPp.trivial_pp_term;
   9   Helm_registry.load_from "conf.xml";
  10   let alluris =
  11     try
  12       let s = Sys.argv.(1) in
  13       if s = "-alluris" then
  14        begin
  15         let uri_re = Str.regexp ".*\\(ind\\|var\\|con\\)$" in
  16         let uris = Http_getter.getalluris () in
  17         let alluris = List.filter (fun u -> Str.string_match uri_re u 0) uris in
  18         let oc = open_out "alluris.txt" in
  19         List.iter (fun s -> output_string oc (s^"\n")) alluris;
  20         close_out oc;
  21         []
  22        end
  23       else [s]
  24     with Invalid_argument _ ->
  25       let r = ref [] in
  26       let ic = open_in "alluris.txt" in
  27       try while true do r := input_line ic :: !r; done; []
  28       with _ -> List.rev !r
  29   in
  30   List.iter (fun uu ->
  31     if uu.[0] = '#' then prerr_endline "SKIP" else begin
  32     prerr_endline ("************* INIZIO **************** " ^ uu);
  33     let u = UriManager.uri_of_string uu in
  34     let _,o = NCicEnvironment.get_obj (NUri.nuri_of_ouri u) in
  35     try
  36       NCicTypeChecker.typecheck_obj o;
  37       prerr_endline ("************* FINE ****************" ^ uu);
  38     with
  39     | NCicTypeChecker.AssertFailure s
  40     | NCicTypeChecker.TypeCheckerFailure s as e ->
  41 (*        prerr_endline ("Obj: " ^ NCicPp.ppobj o); *)
  42        prerr_endline (Lazy.force s); raise e
  43     | CicEnvironment.Object_not_found s ->
  44                     prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s);
  45     end)
  46     alluris
  47 ;;