]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/ng_kernel/check.ml
fix
[helm.git] / 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 = NCicEnvironment.get_obj (NUri.nuri_of_ouri u) in
12   try NCicTypeChecker.typecheck_obj o
13   with 
14   | NCicTypeChecker.AssertFailure s 
15   | NCicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s)
16   | CicEnvironment.Object_not_found s -> 
17       prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s)
18 ;;