3 let lexbuf = Lexing.from_channel stdin in
6 match CicTextualParserContext.main
7 (UriManager.uri_of_string "cic:/dummy") [] []
8 CicTextualLexer.token lexbuf
11 | Some (_, expr) -> terms := expr :: ! terms
15 CicTextualParser0.Eof -> ! terms
18 let u = UriManager.uri_of_string uri in
19 let s = match (CicEnvironment.get_obj u) with
20 | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty
21 | Cic.Axiom (_, ty, _) -> CicPp.ppterm ty
22 | Cic.Variable (_, _, ty) -> CicPp.ppterm ty
23 | _ -> "Current proof or inductive definition."
25 | Cic.CurrentProof (_,conjs,te,ty) ->
26 | C.InductiveDefinition _ ->
28 in print_endline s; flush stdout
31 print_endline (MQueryGenerator.locate_html name);
34 let rec display = function
38 print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
41 let rec levels = function
45 print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
46 print_endline (MQueryGenerator.levels [] [] term);
50 let queries = ref [] in
52 if List.mem query ! queries then false
53 else begin queries := query :: ! queries; true end
55 let rec backward level = function
59 print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
60 print_endline (MQueryGenerator.backward [] [] term level);
63 MQueryGenerator.call_back issue;
64 for level = max m n downto min m n do
65 prerr_endline ("toplevel: backward: trying level " ^
69 prerr_endline ("toplevel: backward: " ^
70 string_of_int (List.length ! queries) ^
72 MQueryGenerator.call_back (fun _ -> true)
75 let rec parse = function
77 | ("-d"|"-display") :: rem -> display (get_terms ())
78 | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
79 | ("-l"|"-levels") :: rem -> levels (get_terms ())
80 | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
81 | ("-B"|"-backward") :: arg :: rem ->
82 let m = (int_of_string arg) in
83 mbackward m m (get_terms ())
84 | ("-MB"|"-mbackward") :: arg :: rem ->
85 let m = (int_of_string arg) in
86 mbackward m 0 (get_terms ())
87 | _ :: rem -> parse rem
89 parse (List.tl (Array.to_list Sys.argv))
93 Logger.log_callback :=
95 ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
96 MQueryGenerator.init ();
98 MQueryGenerator.close ();
99 prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^