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 u = UriManager.uri_of_string Sys.argv.(1) in
  11   let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in
  12   let l = OCic2NCic.convert_obj u o in
  13   List.iter
  14     (fun (u,_,_,_,_ as o) ->
  15        prerr_endline ("CHECK: " ^ NUri.string_of_uri u ^"\n"^NCicPp.ppobj o);
  16        try NCicTypeChecker.typecheck_obj o
  17        with
  18        | NCicTypeChecker.AssertFailure s
  19        | NCicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s)
  20        (*| CicEnvironment.Object_not_found s ->
  21            prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s)*))
  22     l
  23 ;;