restricted mode to use when the database is down :)

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

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 21663939990419ee98e69990c5f63849a678c1af..9992e409369e8c33de911cc622840b8615c376a2 100644 (file)
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -1,18 +1,47 @@
+let use_db = ref true
+
+let db_down = ref true
+
+let check_db () =
+   if ! db_down then begin
+      if ! use_db then begin 
+         MQueryGenerator.init (); db_down := false
+      end else
+        raise (Failure "Operation impossible in restricted mode")
+   end
+      
 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
+         match CicTextualParserContext.main  
+           (UriManager.uri_of_string "cic:/dummy") [] []
+           CicTextualLexer.token lexbuf
+           with
+            | None           -> ()
+            | Some (_, expr) -> terms := expr :: ! terms
       done;
       ! terms
    with
       CicTextualParser0.Eof -> ! terms
 
-let locate name = 
-   print_endline (MQueryGenerator.locate name);
+let pp_type_of uri = 
+   let u = UriManager.uri_of_string uri in  
+   let s = match (CicEnvironment.get_obj u) with
+      | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty
+      | Cic.Axiom (_, ty, _)         -> CicPp.ppterm ty
+      | Cic.Variable (_, _, ty)      -> CicPp.ppterm ty
+      | _                            -> "Current proof or inductive definition."      
+(*
+      | Cic.CurrentProof (_,conjs,te,ty) ->
+      | C.InductiveDefinition _ ->
+*)
+   in print_endline s; flush stdout
+
+let locate name =
+   check_db ();
+   print_endline (MQueryGenerator.locate_html name);
    flush stdout
 
 let rec display = function
@@ -22,44 +51,65 @@ let rec display = function
       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
+let rec levels = function
    | []           -> ()
    | term :: tail -> 
-      backward level tail;
+      levels tail;
       print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
-      print_endline (MQueryGenerator.backward [] [] term level);
+      print_endline (MQueryGenerator.levels [] [] term);
       flush stdout
-      
+   
+let mbackward n m l =
+   let queries = ref [] in
+   let issue query = 
+      if List.mem query ! queries then false
+      else begin queries := query :: ! queries; true end
+   in
+   let rec backward level = function
+      | []           -> ()
+      | term :: tail -> 
+         backward level tail;
+         print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
+         print_endline (MQueryGenerator.backward [] [] term level);
+         flush stdout
+   in
+   check_db ();
+   MQueryGenerator.call_back issue;
+   for level = max m n downto min m n do
+      prerr_endline ("toplevel: backward: trying level " ^
+                     string_of_int level);
+      backward level l
+   done;
+   prerr_endline ("toplevel: backward: " ^ 
+                  string_of_int (List.length ! queries) ^
+                  " queries issued");
+   MQueryGenerator.call_back (fun _ -> true)
+   
 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 ())
+      | ("-d"|"-display") :: rem -> display (get_terms ())
+      | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
+      | ("-l"|"-levels") :: rem -> levels (get_terms ())
+      | ("-r"|"-restricted") :: rem -> use_db := false; parse rem
+      | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
+      | ("-B"|"-backward") :: arg :: rem ->
+         let m = (int_of_string arg) in
+         mbackward m m (get_terms ())
+      | ("-MB"|"-mbackward") :: arg :: rem ->
+         let m = (int_of_string arg) in
+         mbackward m 0 (get_terms ())
       | _ :: rem -> parse rem
    in  
       parse (List.tl (Array.to_list Sys.argv))
 
 let _ =
-   CicCooking.init () ;
+   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 ();
+   if not ! db_down then MQueryGenerator.close ();
+   prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^
+                  " seconds");
    exit 0
-;;