aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/fake_ide.ml
blob: 5fafe2991c42f3e6673604fb8423932fe83e9029 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(** Fake_ide : Simulate a [coqide] talking to a [coqtop -ideslave] *)

exception Comment

type coqtop = {
  in_chan : in_channel;
  out_chan : out_channel;
  xml_parser : Xml_parser.t;
}

let logger level content = ()

let eval_call call coqtop =
  prerr_endline (Serialize.pr_call call);
  let xml_query = Serialize.of_call call in
  Xml_utils.print_xml coqtop.out_chan xml_query;
  flush coqtop.out_chan;
  let rec loop () =
    let xml = Xml_parser.parse coqtop.xml_parser in
    if Serialize.is_message xml then
      let message = Serialize.to_message xml in
      let level = message.Interface.message_level in
      let content = message.Interface.message_content in
      let () = logger level content in
      loop ()
    else (Serialize.to_answer xml call)
  in
  let res = loop () in
  prerr_endline (Serialize.pr_full_value call res);
  match res with Interface.Fail _ -> exit 1 | _ -> ()

let commands =
  [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.interp (true,false,s)));
    "INTERPRAW", (fun s -> eval_call (Serialize.interp (true,true,s)));
    "INTERPSILENT", (fun s -> eval_call (Serialize.interp (false,false,s)));
    "INTERP", (fun s -> eval_call (Serialize.interp (false,true,s)));
    "REWIND", (fun s -> eval_call (Serialize.rewind (int_of_string s)));
    "GOALS", (fun _ -> eval_call Serialize.goals);
    "HINTS", (fun _ -> eval_call Serialize.hints);
    "GETOPTIONS", (fun _ -> eval_call Serialize.get_options);
    "STATUS", (fun _ -> eval_call Serialize.status);
    "INLOADPATH", (fun s -> eval_call (Serialize.inloadpath s));
    "MKCASES", (fun s -> eval_call (Serialize.mkcases s));
    "#", (fun _ -> raise Comment);
  ]

let read_eval_print line =
  let lline = String.length line in
  let rec find_cmd = function
    | [] -> prerr_endline ("Error: Unknown API Command :"^line); exit 1
    | (cmd,fn) :: cmds ->
      let lcmd = String.length cmd in
      if lline >= lcmd && String.sub line 0 lcmd = cmd then
	let arg = try String.sub line (lcmd+1) (lline-lcmd-1) with _ -> ""
	in fn arg
      else find_cmd cmds
  in
  find_cmd commands

let usage () =
  Printf.printf
    "A fake coqide process talking to a coqtop -ideslave.\n\
     Usage: %s [<coqtop>]\n\
     Input syntax is one API call per line, the keyword coming first,\n\
     with the rest of the line as string argument (e.g. INTERP Check plus.)\n\
     Supported API keywords are:\n" (Filename.basename Sys.argv.(0));
  List.iter (fun (s,_) -> Printf.printf "\t%s\n" s) commands;
  exit 1

let main =
  Sys.set_signal Sys.sigpipe
    (Sys.Signal_handle
       (fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
  let coqtop_name = match Array.length Sys.argv with
    | 1 -> "coqtop"
    | 2 when Sys.argv.(1) <> "-help" -> Sys.argv.(1)
    | _ -> usage ()
  in
  let coqtop =
    let (cin, cout) = Unix.open_process (coqtop_name^" -ideslave") in
    let p = Xml_parser.make (Xml_parser.SChannel cin) in
    let () = Xml_parser.check_eof p false in {
      in_chan = cin;
      out_chan = cout;
      xml_parser = p;
    }
  in
  while true do
    let l = try read_line () with End_of_file -> exit 0
    in
    try read_eval_print l coqtop
    with
      | Comment -> ()
      | e ->
	prerr_endline ("Uncaught exception" ^ Printexc.to_string e); exit 1
  done