Initial revision

[helm.git] / helm / interface / theoryParser.ml

diff --git a/helm/interface/theoryParser.ml b/helm/interface/theoryParser.ml
new file mode 100644 (file)
index 0000000..abc3528
--- /dev/null
+++ b/helm/interface/theoryParser.ml
@@ -0,0 +1,29 @@
+exception Warnings;;
+
+class warner =
+  object 
+    method warn w =
+      print_endline ("WARNING: " ^ w) ;
+      (raise Warnings : unit)
+  end
+;;
+
+exception EmptyUri;;
+
+let theory_of_xml filename =
+ let module Y = Pxp_yacc in
+  try 
+    let d =
+     let config = {Y.default_config with Y.warner = new warner} in
+      Y.parse_document_entity config
+(*PXP       (Y.ExtID (Pxp_types.System filename,
+         new Pxp_reader.resolve_as_file ~url_of_id ()))
+*)     (PxpUriResolver.from_file filename)
+       Y.default_spec
+    in
+     TheoryParser2.get_theory d#root
+  with
+   e ->
+     print_endline (Pxp_types.string_of_exn e) ;
+     raise e
+;;