helm/software/components/ng_kernel/rt.ml

   1 let _ =
   2   Helm_registry.load_from "conf.xml";
   3   let u = UriManager.uri_of_string "cic:/matita/tests/f.con" in
   4   let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in
   5   let l = OCic2NCic.convert_obj u o in
   6   let objs =
   7     List.flatten
   8     (List.map NCic2OCic.convert_nobj l) in
   9   List.iter
  10    (fun (u,o) ->
  11      prerr_endline ("------- " ^ UriManager.string_of_uri u);
  12      prerr_endline (CicPp.ppobj o);
  13      try CicTypeChecker.typecheck_obj u o
  14      with CicTypeChecker.TypeCheckerFailure s ->
  15        prerr_endline (Lazy.force s))
  16    objs;
  17 ;;