6 if ! db_down then begin
8 MQueryGenerator.init (); db_down := false
10 raise (Failure "Operation impossible in restricted mode")
15 let lexbuf = Lexing.from_channel stdin in
18 match CicTextualParserContext.main
19 (UriManager.uri_of_string "cic:/dummy") [] []
20 CicTextualLexer.token lexbuf
23 | Some (_, expr) -> terms := expr :: ! terms
27 CicTextualParser0.Eof -> ! terms
30 let u = UriManager.uri_of_string uri in
31 let s = match (CicEnvironment.get_obj u) with
32 | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty
33 | Cic.Axiom (_, ty, _) -> CicPp.ppterm ty
34 | Cic.Variable (_, _, ty) -> CicPp.ppterm ty
35 | _ -> "Current proof or inductive definition."
37 | Cic.CurrentProof (_,conjs,te,ty) ->
38 | C.InductiveDefinition _ ->
40 in print_endline s; flush stdout
44 print_endline (MQueryGenerator.locate_html name);
47 let rec display = function
51 print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
54 let rec levels = function
58 print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
59 print_endline (MQueryGenerator.levels [] [] term);
63 let queries = ref [] in
65 if List.mem query ! queries then false
66 else begin queries := query :: ! queries; true end
68 let rec backward level = function
72 print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
73 print_endline (MQueryGenerator.backward [] [] term level);
77 MQueryGenerator.call_back issue;
78 for level = max m n downto min m n do
79 prerr_endline ("toplevel: backward: trying level " ^
83 prerr_endline ("toplevel: backward: " ^
84 string_of_int (List.length ! queries) ^
86 MQueryGenerator.call_back (fun _ -> true)
89 let rec parse = function
91 | ("-d"|"-display") :: rem -> display (get_terms ())
92 | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
93 | ("-l"|"-levels") :: rem -> levels (get_terms ())
94 | ("-r"|"-restricted") :: rem -> use_db := false; parse rem
95 | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
96 | ("-B"|"-backward") :: arg :: rem ->
97 let m = (int_of_string arg) in
98 mbackward m m (get_terms ())
99 | ("-MB"|"-mbackward") :: arg :: rem ->
100 let m = (int_of_string arg) in
101 mbackward m 0 (get_terms ())
102 | _ :: rem -> parse rem
104 parse (List.tl (Array.to_list Sys.argv))
108 Logger.log_callback :=
110 ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
112 if not ! db_down then MQueryGenerator.close ();
113 prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^