X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2Ftest.ml;fp=helm%2Focaml%2Fmetadata%2Ftest.ml;h=27be47c23cb1c545c14eef1e3241764f9ff66e96;hb=21758b512843088d19e81830d9fb121725c8a16e;hp=0000000000000000000000000000000000000000;hpb=dd8726f655e4fdad063baf456fcfc95f82e079cc;p=helm.git

diff --git a/helm/ocaml/metadata/test.ml b/helm/ocaml/metadata/test.ml
new file mode 100644
index 000000000..27be47c23
--- /dev/null
+++ b/helm/ocaml/metadata/test.ml
@@ -0,0 +1,23 @@
+
+module DB = Dbi_mysql
+
+let _ = Helm_registry.set "getter.mode" "remote";
+let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in
+let dbh = new DB.connection ~host:"mowgli.cs.unibo.it" ~user:"helm" "matita" in
+let owner =
+  try
+    Sys.argv.(2)
+  with Invalid_argument _ -> "matita_test"
+in
+if Sys.argv.(1) = "clean" then
+  MetadataDb.clean ~dbh ~owner
+else
+  let uri_str = Sys.argv.(1) in
+  let uri = UriManager.uri_of_string uri_str in
+  match CicEnvironment.get_obj uri with
+  | Cic.Constant (_, body, ty, _) ->
+      MetadataDb.index_constant ~body ~ty ~uri ~owner ~dbh
+  | Cic.InductiveDefinition (types, _, _) ->
+      MetadataDb.index_inductive_def ~dbh ~owner ~uri ~types
+  | _ -> assert false
+