helm/ocaml/metadata/test.ml

   1
   2 let _ = Helm_registry.set "getter.mode" "remote";
   3 let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in
   4 let dbd =
   5   Mysql.quick_connect ~host:"mowgli.cs.unibo.it" ~user:"helm" ~database:"matita"
   6     ()
   7 in
   8 let owner =
   9   try
  10     Sys.argv.(2)
  11   with Invalid_argument _ -> "matita_test"
  12 in
  13 let _ = MetadataTypes.ownerize_tables owner in
  14 if Sys.argv.(1) = "clean" then begin
  15   prerr_endline "foo";
  16   ignore (MetadataDb.clean ~dbd)
  17 end else
  18   let fname = Sys.argv.(1) in
  19   let n = ref 0 in
  20   let ic = open_in fname in
  21   try
  22     while true do
  23       let line = input_line ic in
  24       incr n;
  25       Printf.printf "%d\t%s\n" !n line; flush stdout;
  26       let uri = UriManager.uri_of_string line in
  27       (match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
  28       | Cic.Constant (_, body, ty, _, _), _ ->
  29           MetadataDb.index_constant ~body ~ty ~uri ~dbd
  30       | Cic.Variable (_, body, ty, _, _), _ ->
  31           MetadataDb.index_constant ~body ~ty ~uri ~dbd
  32       | Cic.InductiveDefinition (types, _, _, _), _ ->
  33           MetadataDb.index_inductive_def ~dbd ~uri ~types
  34       | _ -> assert false)
  35     done
  36   with End_of_file -> close_in ic
  37