This commit was manufactured by cvs2svn to create branch 'scripts'.

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

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
deleted file mode 100644 (file)
index 1fa790b..0000000
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ /dev/null
@@ -1,115 +0,0 @@
-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 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 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 (snd (MQueryGenerator.locate name)) ;
-   flush stdout
-
-let rec display = function
-   | []           -> ()
-   | term :: tail -> 
-      display tail;
-      print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
-      flush stdout
-
-let rec levels = function
-   | []           -> ()
-   | term :: tail -> 
-      levels tail;
-      print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
-      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 (snd (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
-      | [] -> ()
-      | ("-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 () ; 
-   Logger.log_callback :=
-      (Logger.log_to_html
-      ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
-   parse_args ();
-   if not ! db_down then MQueryGenerator.close ();
-   prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^
-                  " seconds");
-   exit 0