mathQL modified, stderr corrected to stdout im mathql_interpreter,

[helm.git] / helm / gTopLevel / topLevel / topLevel.ml

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
new file mode 100644 (file)
index 0000000..2166393
--- /dev/null
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -0,0 +1,65 @@
+let get_terms () =
+   let terms = ref [] in
+   let lexbuf = Lexing.from_channel stdin in
+   try
+      while true do
+         match CicTextualParser.main CicTextualLexer.token lexbuf with
+            | None -> ()
+            | Some expr -> terms := expr :: ! terms
+      done;
+      ! terms
+   with
+      CicTextualParser0.Eof -> ! terms
+
+let locate name = 
+   print_endline (MQueryGenerator.locate name);
+   flush stdout
+
+let rec display = function
+   | []           -> ()
+   | term :: tail -> 
+      display tail;
+      print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
+      flush stdout
+
+let rec levels level = function
+   | []           -> ()
+   | term :: tail -> 
+      levels level tail;
+      print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
+      print_endline (MQueryGenerator.levels [] [] term level);
+      flush stdout
+
+let rec backward level = function
+   | []           -> ()
+   | term :: tail -> 
+      backward level tail;
+      print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
+      print_endline (MQueryGenerator.backward [] [] term level);
+      flush stdout
+      
+let parse_args () =
+   let rec parse = function
+      | [] -> ()
+      | ("-l"|"-locate") :: arg :: rem -> 
+         locate arg; parse rem
+      | ("-d"|"-display") :: rem -> 
+         display (get_terms ())
+      | ("-t"|"-test") :: arg :: rem -> 
+        levels (int_of_string arg) (get_terms ())
+      | ("-b"|"-backward") :: arg :: rem -> 
+         backward (int_of_string arg) (get_terms ())
+      | _ :: rem -> parse rem
+   in  
+      parse (List.tl (Array.to_list Sys.argv))
+
+let _ =
+   CicCooking.init () ;
+   Logger.log_callback :=
+      (Logger.log_to_html
+      ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
+   MQueryGenerator.init ();
+   parse_args ();
+   MQueryGenerator.close ();
+   exit 0
+;;