From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- tools/fake_ide.ml | 375 ++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 311 insertions(+), 64 deletions(-) (limited to 'tools/fake_ide.ml') diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index a7203dc8..c2b12668 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* exit 1 | _ -> () - -let commands = - [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (0,true,false,s))); - "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (0,true,true,s))); - "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (0,false,false,s))); - "INTERP", (fun s -> eval_call (Ide_intf.interp (0,false,true,s))); - "REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s))); - "GOALS", (fun _ -> eval_call (Ide_intf.goals ())); - "HINTS", (fun _ -> eval_call (Ide_intf.hints ())); - "GETOPTIONS", (fun _ -> eval_call (Ide_intf.get_options ())); - "STATUS", (fun _ -> eval_call (Ide_intf.status ())); - "INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s)); - "MKCASES", (fun s -> eval_call (Ide_intf.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 +let error s = + prerr_endline ("fake_id: error: "^s); + exit 1 + +type coqtop = { + xml_printer : Xml_printer.t; + xml_parser : Xml_parser.t; +} + +let logger level content = prerr_endline content + +let base_eval_call ?(print=true) ?(fail=true) call coqtop = + if print then prerr_endline (Xmlprotocol.pr_call call); + let xml_query = Xmlprotocol.of_call call in + Xml_printer.print coqtop.xml_printer xml_query; + let rec loop () = + let xml = Xml_parser.parse coqtop.xml_parser in + if Pp.is_message xml then + let message = Pp.to_message xml in + let level = message.Pp.message_level in + let content = message.Pp.message_content in + logger level content; + loop () + else if Feedback.is_feedback xml then + loop () + else (Xmlprotocol.to_answer call xml) in - find_cmd commands + let res = loop () in + if print then prerr_endline (Xmlprotocol.pr_full_value call res); + match res with + | Interface.Fail (_,_,s) when fail -> error s + | Interface.Fail (_,_,s) as x -> prerr_endline s; x + | x -> x + +let eval_call c q = ignore(base_eval_call c q) + +module Parser = struct (* {{{ *) + + exception Err of string + exception More + + type token = + | Tok of string * string + | Top of token list + + type grammar = + | Alt of grammar list + | Seq of grammar list + | Opt of grammar + | Item of (string * (string -> token * int)) + + let eat_rex x = x, fun s -> + if Str.string_match (Str.regexp x) s 0 then begin + let m = Str.match_end () in + let w = String.sub s 0 m in + Tok(x,w), m + end else raise (Err ("Regexp "^x^" not found in: "^s)) + + let eat_balanced c = + let c' = match c with + | '{' -> '}' | '(' -> ')' | '[' -> ']' | _ -> assert false in + let sc, sc' = String.make 1 c, String.make 1 c' in + let name = sc ^ "..." ^ sc' in + let unescape s = + Str.global_replace (Str.regexp ("\\\\"^sc)) sc + (Str.global_replace (Str.regexp ("\\\\"^sc')) sc' s) in + name, fun s -> + if s.[0] = c then + let rec find n m = + if String.length s <= m then raise More; + if s.[m] = c' then + if n = 0 then Tok (name, unescape (String.sub s 1 (m-1))), m+1 + else find (n-1) (m+1) + else if s.[m] = c then find (n+1) (m+1) + else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c then + find n (m+2) + else if s.[m] = '\\' && String.length s > m+1 && s.[m+1] = c' then + find n (m+2) + else find n (m+1) + in find ~-1 0 + else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s)) + + let eat_blanks s = snd (eat_rex "[ \n\t]*") s + + let s = ref "" + + let parse g ic = + let read_more () = s := !s ^ input_line ic ^ "\n" in + let ensure_non_empty n = if n = String.length !s then read_more () in + let cut_after s n = String.sub s n (String.length s - n) in + let rec wrap f n = + try + ensure_non_empty n; + let _, n' = eat_blanks (cut_after !s n) in + ensure_non_empty n'; + let t, m = f (cut_after !s (n+n')) in + let _, m' = eat_blanks (cut_after !s (n+n'+m)) in + t, n+n'+m+m' + with More -> read_more (); wrap f n in + let rec aux n g res : token list * int = + match g with + | Item (_,f) -> + let t, n = wrap f n in + t :: res, n + | Opt g -> + (try let res', n = aux n g [] in Top (List.rev res') :: res, n + with Err _ -> Top [] :: res, n) + | Alt gl -> + let rec fst = function + | [] -> raise (Err ("No more alternatives for: "^cut_after !s n)) + | g :: gl -> + try aux n g res + with Err s -> fst gl in + fst gl + | Seq gl -> + let rec all (res,n) = function + | [] -> res, n + | g :: gl -> all (aux n g res) gl in + all (res,n) gl in + let res, n = aux 0 g [] in + s := cut_after !s n; + List.rev res + + let clean s = Str.global_replace (Str.regexp "\n") "\\n" s + + let rec print g = + match g with + | Item (s,_) -> Printf.sprintf "%s" (clean s) + | Opt g -> Printf.sprintf "[%s]" (print g) + | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs)) + | Seq gs -> String.concat " " (List.map print gs) + + let rec print_toklist = function + | [] -> "" + | Tok(k,v) :: rest when k = v -> clean k ^ " " ^ print_toklist rest + | Tok(k,v) :: rest -> clean k ^ " = \"" ^ clean v ^ "\" " ^ print_toklist rest + | Top l :: rest -> print_toklist l ^ " " ^ print_toklist rest + +end (* }}} *) + +type sentence = { + name : string; + text : string; + edit_id : int; +} + +let doc : sentence Document.document = Document.create () + +let tip_id () = + try Document.tip doc + with + | Document.Empty -> Stateid.initial + | Invalid_argument _ -> error "add_sentence on top of non assigned tip" + +let add_sentence = + let edit_id = ref 0 in + fun ?(name="") text -> + let tip_id = tip_id () in + decr edit_id; + Document.push doc { name; text; edit_id = !edit_id }; + !edit_id, tip_id + +let print_document () = + let ellipsize s = + Str.global_replace (Str.regexp "^[\n ]*") "" + (if String.length s > 20 then String.sub s 0 17 ^ "..." + else s) in + prerr_endline (Pp.string_of_ppcmds + (Document.print doc + (fun b state_id { name; text } -> + Pp.str (Printf.sprintf "%s[%10s, %3s] %s" + (if b then "*" else " ") + name + (Stateid.to_string (Option.default Stateid.dummy state_id)) + (ellipsize text))))) + +(* This module is the logic a GUI has to implement *) +module GUILogic = struct + + let after_add = function + | Interface.Fail (_,_,s) -> error s + | Interface.Good (id, (Util.Inl (), _)) -> + Document.assign_tip_id doc id + | Interface.Good (id, (Util.Inr tip, _)) -> + Document.assign_tip_id doc id; + Document.unfocus doc; + ignore(Document.cut_at doc tip); + print_document () + + let at id id' _ = Stateid.equal id' id + + let after_edit_at (id,need_unfocus) = function + | Interface.Fail (_,_,s) -> error s + | Interface.Good (Util.Inl ()) -> + if need_unfocus then Document.unfocus doc; + ignore(Document.cut_at doc id); + print_document () + | Interface.Good (Util.Inr (stop_id,(start_id,tip))) -> + if need_unfocus then Document.unfocus doc; + ignore(Document.cut_at doc tip); + Document.focus doc ~cond_top:(at start_id) ~cond_bot:(at stop_id); + ignore(Document.cut_at doc id); + print_document () + + let get_id_pred pred = + try Document.find_id doc pred + with Not_found -> error "No state found" + + let get_id id = get_id_pred (fun _ { name } -> name = id) + + let after_fail coq = function + | Interface.Fail (safe_id,_,s) -> + prerr_endline "The command failed as expected"; + let to_id, need_unfocus = + get_id_pred (fun id _ -> Stateid.equal id safe_id) in + after_edit_at (to_id, need_unfocus) + (base_eval_call (Xmlprotocol.edit_at to_id) coq) + | Interface.Good _ -> error "The command was expected to fail but did not" + +end + +open GUILogic + +let eval_print l coq = + let open Parser in + let open Xmlprotocol in + (* prerr_endline ("Interpreting: " ^ print_toklist l); *) + match l with + | [ Tok(_,"ADD"); Top []; Tok(_,phrase) ] -> + let eid, tip = add_sentence phrase in + after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq) + | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] -> + let eid, tip = add_sentence ~name phrase in + after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq) + | [ Tok(_,"GOALS"); ] -> + eval_call (goals ()) coq + | [ Tok(_,"FAILGOALS"); ] -> + after_fail coq (base_eval_call ~fail:false (goals ()) coq) + | [ Tok(_,"EDIT_AT"); Tok(_,id) ] -> + let to_id, need_unfocus = get_id id in + after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq) + | [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] -> + eval_call (query (phrase,tip_id())) coq + | [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] -> + let to_id, _ = get_id id in + eval_call (query (phrase, to_id)) coq + | [ Tok(_,"WAIT") ] -> + let phrase = "Stm Wait." in + eval_call (query (phrase,tip_id())) coq + | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> + let to_id, _ = get_id id in + if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" + else prerr_endline "Good tip" + | Tok("#[^\n]*",_) :: _ -> () + | _ -> error "syntax error" + +let grammar = + let open Parser in + let eat_id = eat_rex "[a-zA-Z_][a-zA-Z0-9_]*" in + let eat_phrase = eat_balanced '{' in + Alt + [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] + ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "WAIT")] + ; Seq [Item (eat_rex "GOALS")] + ; Seq [Item (eat_rex "FAILGOALS")] + ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ] + ; Item (eat_rex "#[^\n]*") + ] + +let read_command inc = Parser.parse grammar inc let usage () = - Printf.printf + error (Printf.sprintf "A fake coqide process talking to a coqtop -ideslave.\n\ - Usage: %s []\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 + Usage: %s (file|-) []\n\ + Input syntax is the following:\n%s\n" + (Filename.basename Sys.argv.(0)) + (Parser.print grammar)) + +module Coqide = Spawn.Sync(struct end) 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 - coqtop := Unix.open_process (coqtop_name^" -ideslave"); + let coqtop_name, coqtop_args, input_file = match Sys.argv with + | [| _; f |] -> "coqtop",[|"-ideslave"|], f + | [| _; f; ct |] -> + let ct = Str.split (Str.regexp " ") ct in + List.hd ct, Array.of_list ("-ideslave" :: List.tl ct), f + | _ -> usage () in + let inc = if input_file = "-" then stdin else open_in input_file in + let coq = + let _p, cin, cout = Coqide.spawn coqtop_name coqtop_args in + let ip = Xml_parser.make (Xml_parser.SChannel cin) in + let op = Xml_printer.make (Xml_printer.TChannel cout) in + Xml_parser.check_eof ip false; + { xml_printer = op; xml_parser = ip } in + let init () = + match base_eval_call ~print:false (Xmlprotocol.init None) coq with + | Interface.Good id -> + let dir = Filename.dirname input_file in + let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in + let eid, tip = add_sentence ~name:"initial" phrase in + after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq) + | Interface.Fail _ -> error "init call failed" in + let finish () = + match base_eval_call (Xmlprotocol.status true) coq with + | Interface.Good _ -> exit 0 + | Interface.Fail (_,_,s) -> error s in + (* The main loop *) + init (); while true do - let l = try read_line () with End_of_file -> exit 0 - in - try read_eval_print l - with - | Comment -> () - | e -> - prerr_endline ("Uncaught exception" ^ Printexc.to_string e); exit 1 + let cmd = try read_command inc with End_of_file -> finish () in + try eval_print cmd coq + with e -> error ("Uncaught exception " ^ Printexc.to_string e) done + +(* vim:set foldmethod=marker: *) -- cgit v1.2.3