diff options
Diffstat (limited to 'ide/protocol')
| -rw-r--r-- | ide/protocol/dune | 7 | ||||
| -rw-r--r-- | ide/protocol/ideprotocol.mllib | 7 | ||||
| -rw-r--r-- | ide/protocol/interface.ml | 263 | ||||
| -rw-r--r-- | ide/protocol/richpp.ml | 171 | ||||
| -rw-r--r-- | ide/protocol/richpp.mli | 53 | ||||
| -rw-r--r-- | ide/protocol/serialize.ml | 123 | ||||
| -rw-r--r-- | ide/protocol/serialize.mli | 41 | ||||
| -rw-r--r-- | ide/protocol/xml_lexer.mli | 44 | ||||
| -rw-r--r-- | ide/protocol/xml_lexer.mll | 317 | ||||
| -rw-r--r-- | ide/protocol/xml_parser.ml | 232 | ||||
| -rw-r--r-- | ide/protocol/xml_parser.mli | 106 | ||||
| -rw-r--r-- | ide/protocol/xml_printer.ml | 147 | ||||
| -rw-r--r-- | ide/protocol/xml_printer.mli | 31 | ||||
| -rw-r--r-- | ide/protocol/xmlprotocol.ml | 962 | ||||
| -rw-r--r-- | ide/protocol/xmlprotocol.mli | 73 |
15 files changed, 0 insertions, 2577 deletions
diff --git a/ide/protocol/dune b/ide/protocol/dune deleted file mode 100644 index 801ceb20ec..0000000000 --- a/ide/protocol/dune +++ /dev/null @@ -1,7 +0,0 @@ -(library - (name protocol) - (public_name coqide-server.protocol) - (wrapped false) - (libraries coq.lib)) - -(ocamllex xml_lexer) diff --git a/ide/protocol/ideprotocol.mllib b/ide/protocol/ideprotocol.mllib deleted file mode 100644 index 8317a08681..0000000000 --- a/ide/protocol/ideprotocol.mllib +++ /dev/null @@ -1,7 +0,0 @@ -Xml_lexer -Xml_parser -Xml_printer -Serialize -Richpp -Interface -Xmlprotocol diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml deleted file mode 100644 index 646012dcaa..0000000000 --- a/ide/protocol/interface.ml +++ /dev/null @@ -1,263 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** * Declarative part of the interface of CoqIde calls to Coq *) - -(** * Generic structures *) - -type raw = bool -type verbose = bool - -(** The type of coqtop goals *) -type goal = { - goal_id : string; - (** Unique goal identifier *) - goal_hyp : Pp.t list; - (** List of hypotheses *) - goal_ccl : Pp.t; - (** Goal conclusion *) -} - -type evar = { - evar_info : string; - (** A string describing an evar: type, number, environment *) -} - -type status = { - status_path : string list; - (** Module path of the current proof *) - status_proofname : string option; - (** Current proof name. [None] if no focused proof is in progress *) - status_allproofs : string list; - (** List of all pending proofs. Order is not significant *) - status_proofnum : int; - (** An id describing the state of the current proof. *) -} - -type 'a pre_goals = { - fg_goals : 'a list; - (** List of the focused goals *) - bg_goals : ('a list * 'a list) list; - (** Zipper representing the unfocused background goals *) - shelved_goals : 'a list; - (** List of the goals on the shelf. *) - given_up_goals : 'a list; - (** List of the goals that have been given up *) -} - -type goals = goal pre_goals - -type hint = (string * string) list -(** A list of tactics applicable and their appearance *) - -type option_name = string list - -type option_value = - | BoolValue of bool - | IntValue of int option - | StringValue of string - | StringOptValue of string option - -(** Summary of an option status *) -type option_state = { - opt_sync : bool; - (** Whether an option is synchronous *) - opt_depr : bool; - (** Whether an option is deprecated *) - opt_value : option_value; - (** The current value of the option *) -} - -type search_constraint = -| Name_Pattern of string -(** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) - -| Type_Pattern of string -(** Whether the object type satisfies a pattern *) - -| SubType_Pattern of string -(** Whether some subtype of object type satisfies a pattern *) - -| In_Module of string list -(** Whether the object pertains to a module *) - -| Include_Blacklist -(** Bypass the Search blacklist *) - -(** A list of search constraints; the boolean flag is set to [false] whenever - the flag should be negated. *) -type search_flags = (search_constraint * bool) list - -(** A named object in Coq. [coq_object_qualid] is the shortest path defined for - the user. [coq_object_prefix] is the missing part to recover the fully - qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid]. - [coq_object_object] is the actual content of the object. *) -type 'a coq_object = { - coq_object_prefix : string list; - coq_object_qualid : string list; - coq_object_object : 'a; -} - -type coq_info = { - coqtop_version : string; - protocol_version : string; - release_date : string; - compile_date : string; -} - -(** Calls result *) - -type location = (int * int) option (* start and end of the error *) -type state_id = Stateid.t -type route_id = Feedback.route_id - -(* Obsolete *) -type edit_id = int - -(* The fail case carries the current state_id of the prover, the GUI - should probably retract to that point *) -type 'a value = - | Good of 'a - | Fail of (state_id * location * Pp.t) - -type ('a, 'b) union = ('a, 'b) Util.union - -(* Request/Reply message protocol between Coq and CoqIde *) - -(** [add ((s,eid),(sid,v))] adds the phrase [s] with edit id [eid] - on top of the current edit position (that is asserted to be [sid]) - verbosely if [v] is true. The response [(id,(rc,s)] is the new state - [id] assigned to the phrase. [rc] is [Inl] if the new - state id is the tip of the edit point, or [Inr tip] if the new phrase - closes a focus and [tip] is the new edit tip - - [s] used to contain Coq's console output and has been deprecated - in favor of sending feedback, it will be removed in a future - version of the protocol. *) -type add_sty = (string * edit_id) * (state_id * verbose) -type add_rty = state_id * ((unit, state_id) union * string) - -(** [edit_at id] declares the user wants to edit just after [id]. - The response is [Inl] if the document has been rewound to that point, - [Inr (start,(stop,tip))] if [id] is in a zone that can be focused. - In that case the zone is delimited by [start] and [stop] while [tip] - is the new document [tip]. Edits made by subsequent [add] are always - performed on top of [id]. *) -type edit_at_sty = state_id -type edit_at_rty = (unit, state_id * (state_id * state_id)) union - -(** [query s id] executes [s] at state [id]. - - query used to reply with the contents of Coq's console output, and - has been deprecated in favor of sending the query answers as - feedback. It will be removed in a future version of the protocol. -*) -type query_sty = route_id * (string * state_id) -type query_rty = unit - -(** Fetching the list of current goals. Return [None] if no proof is in - progress, [Some gl] otherwise. *) -type goals_sty = unit -type goals_rty = goals option - -(** Retrieve the list of uninstantiated evars in the current proof. [None] if no - proof is in progress. *) -type evars_sty = unit -type evars_rty = evar list option - -(** Retrieving the tactics applicable to the current goal. [None] if there is - no proof in progress. *) -type hints_sty = unit -type hints_rty = (hint list * hint) option - -(** The status, for instance "Ready in SomeSection, proving Foo", the - input boolean (if true) forces the evaluation of all unevaluated - statements *) -type status_sty = bool -type status_rty = status - -(** Search for objects satisfying the given search flags. *) -type search_sty = search_flags -type search_rty = string coq_object list - -(** Retrieve the list of options of the current toplevel *) -type get_options_sty = unit -type get_options_rty = (option_name * option_state) list - -(** Set the options to the given value. Warning: this is not atomic, so whenever - the call fails, the option state can be messed up... This is the caller duty - to check that everything is correct. *) -type set_options_sty = (option_name * option_value) list -type set_options_rty = unit - -(** Create a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. *) -type mkcases_sty = string -type mkcases_rty = string list list - -(** Quit gracefully the interpreter. *) -type quit_sty = unit -type quit_rty = unit - -(* Initialize, and return the initial state id. The argument is the filename. - * If its directory is not in dirpath, it adds it. It also loads - * compilation hints for the filename. *) -type init_sty = string option -type init_rty = state_id - -type about_sty = unit -type about_rty = coq_info - -type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * Pp.t - -(* Retrocompatibility stuff *) -type interp_sty = (raw * verbose) * string -(* spiwack: [Inl] for safe and [Inr] for unsafe. *) -type interp_rty = state_id * (string,string) Util.union - -type stop_worker_sty = string -type stop_worker_rty = unit - -type print_ast_sty = state_id -type print_ast_rty = Xml_datatype.xml - -type annotate_sty = string -type annotate_rty = Xml_datatype.xml - -type wait_sty = unit -type wait_rty = unit - -type handler = { - add : add_sty -> add_rty; - edit_at : edit_at_sty -> edit_at_rty; - query : query_sty -> query_rty; - goals : goals_sty -> goals_rty; - evars : evars_sty -> evars_rty; - hints : hints_sty -> hints_rty; - status : status_sty -> status_rty; - search : search_sty -> search_rty; - get_options : get_options_sty -> get_options_rty; - set_options : set_options_sty -> set_options_rty; - mkcases : mkcases_sty -> mkcases_rty; - about : about_sty -> about_rty; - stop_worker : stop_worker_sty -> stop_worker_rty; - print_ast : print_ast_sty -> print_ast_rty; - annotate : annotate_sty -> annotate_rty; - handle_exn : handle_exn_sty -> handle_exn_rty; - init : init_sty -> init_rty; - quit : quit_sty -> quit_rty; - (* for internal use (fake_id) only, do not use *) - wait : wait_sty -> wait_rty; - (* Retrocompatibility stuff *) - interp : interp_sty -> interp_rty; -} - diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml deleted file mode 100644 index 7aa38792fc..0000000000 --- a/ide/protocol/richpp.ml +++ /dev/null @@ -1,171 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Util -open Xml_datatype - -type 'annotation located = { - annotation : 'annotation option; - startpos : int; - endpos : int -} - -type 'a stack = -| Leaf -| Node of string * 'a located gxml list * int * 'a stack - -type 'a context = { - mutable stack : 'a stack; - (** Pending opened nodes *) - mutable offset : int; - (** Quantity of characters printed so far *) -} - -(** We use Format to introduce tags inside the pretty-printed document. - Each inserted tag is a fresh index that we keep in sync with the contents - of annotations. - - We build an XML tree on the fly, by plugging ourselves in Format tag - marking functions. As those functions are called when actually writing to - the device, the resulting tree is correct. -*) -let rich_pp width ppcmds = - - let context = { - stack = Leaf; - offset = 0; - } in - - let pp_buffer = Buffer.create 180 in - - let push_pcdata () = - (* Push the optional PCData on the above node *) - let len = Buffer.length pp_buffer in - if len = 0 then () - else match context.stack with - | Leaf -> assert false - | Node (node, child, pos, ctx) -> - let data = Buffer.contents pp_buffer in - let () = Buffer.clear pp_buffer in - let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in - context.offset <- context.offset + len - in - - let open_xml_tag tag = - let () = push_pcdata () in - context.stack <- Node (tag, [], context.offset, context.stack) - in - - let close_xml_tag tag = - let () = push_pcdata () in - match context.stack with - | Leaf -> assert false - | Node (node, child, pos, ctx) -> - let () = assert (String.equal tag node) in - let annotation = { - annotation = Some tag; - startpos = pos; - endpos = context.offset; - } in - let xml = Element (node, annotation, List.rev child) in - match ctx with - | Leaf -> - (* Final node: we keep the result in a dummy context *) - context.stack <- Node ("", [xml], 0, Leaf) - | Node (node, child, pos, ctx) -> - context.stack <- Node (node, xml :: child, pos, ctx) - in - - let open Format in - - let ft = formatter_of_buffer pp_buffer in - - let tag_functions = { - mark_open_tag = (fun tag -> let () = open_xml_tag tag in ""); - mark_close_tag = (fun tag -> let () = close_xml_tag tag in ""); - print_open_tag = ignore; - print_close_tag = ignore; - } in - - pp_set_formatter_tag_functions ft tag_functions [@warning "-3"]; - pp_set_mark_tags ft true; - - (* Setting the formatter *) - pp_set_margin ft width; - let m = max (64 * width / 100) (width-30) in - pp_set_max_indent ft m; - pp_set_max_boxes ft 50 ; - pp_set_ellipsis_text ft "..."; - - (* The whole output must be a valid document. To that - end, we nest the document inside <pp> tags. *) - pp_open_box ft 0; - pp_open_tag ft "pp" [@warning "-3"]; - Pp.(pp_with ft ppcmds); - pp_close_tag ft () [@warning "-3"]; - pp_close_box ft (); - - (* Get the resulting XML tree. *) - let () = pp_print_flush ft () in - let () = assert (Buffer.length pp_buffer = 0) in - match context.stack with - | Node ("", [xml], 0, Leaf) -> xml - | _ -> assert false - - -let annotations_positions xml = - let rec node accu = function - | Element (_, { annotation = Some annotation; startpos; endpos }, cs) -> - children ((annotation, (startpos, endpos)) :: accu) cs - | Element (_, _, cs) -> - children accu cs - | _ -> - accu - and children accu cs = - List.fold_left node accu cs - in - node [] xml - -let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = - let rec node = function - | Element (index, { annotation; startpos; endpos }, cs) -> - let attributes = - [ "startpos", string_of_int startpos; - "endpos", string_of_int endpos - ] - @ (match annotation with - | None -> [] - | Some annotation -> attributes_of_annotation annotation - ) - in - let tag = - match annotation with - | None -> index - | Some annotation -> tag_of_annotation annotation - in - Element (tag, attributes, List.map node cs) - | PCData s -> - PCData s - in - node xml - -type richpp = xml - -let richpp_of_pp width pp = - let rec drop = function - | PCData s -> [PCData s] - | Element (_, annotation, cs) -> - let cs = List.concat (List.map drop cs) in - match annotation.annotation with - | None -> cs - | Some s -> [Element (s, [], cs)] - in - let xml = rich_pp width pp in - Element ("_", [], drop xml) diff --git a/ide/protocol/richpp.mli b/ide/protocol/richpp.mli deleted file mode 100644 index 3b83e7b15c..0000000000 --- a/ide/protocol/richpp.mli +++ /dev/null @@ -1,53 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** This module offers semi-structured pretty-printing. *) - -(** Each annotation of the semi-structured document refers to the - substring it annotates. *) -type 'annotation located = { - annotation : 'annotation option; - startpos : int; - endpos : int -} - -(* XXX: The width parameter should be moved to a `formatter_property` - record shared with Topfmt *) - -(** [rich_pp width ppcmds] returns the interpretation - of [ppcmds] as a semi-structured document - that represents (located) annotations of this string. - The [get_annotations] function is used to convert tags into the desired - annotation. [width] sets the printing width of the formatter. *) -val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml - -(** [annotations_positions ssdoc] returns a list associating each - annotations with its position in the string from which [ssdoc] is - built. *) -val annotations_positions : - 'annotation located Xml_datatype.gxml -> - ('annotation * (int * int)) list - -(** [xml_of_rich_pp ssdoc] returns an XML representation of the - semi-structured document [ssdoc]. *) -val xml_of_rich_pp : - ('annotation -> string) -> - ('annotation -> (string * string) list) -> - 'annotation located Xml_datatype.gxml -> - Xml_datatype.xml - -(** {5 Enriched text} *) - -type richpp = Xml_datatype.xml - -(** Type of text with style annotations *) - -val richpp_of_pp : int -> Pp.t -> richpp -(** Extract style information from formatted text *) diff --git a/ide/protocol/serialize.ml b/ide/protocol/serialize.ml deleted file mode 100644 index bdbec5b30f..0000000000 --- a/ide/protocol/serialize.ml +++ /dev/null @@ -1,123 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Xml_datatype - -exception Marshal_error of string * xml - -(** Utility functions *) - -let rec get_attr attr = function - | [] -> raise Not_found - | (k, v) :: l when CString.equal k attr -> v - | _ :: l -> get_attr attr l - -let massoc x l = - try get_attr x l - with Not_found -> raise (Marshal_error("attribute " ^ x,PCData "not there")) - -let constructor t c args = Element (t, ["val", c], args) -let do_match t mf = function - | Element (s, attrs, args) when CString.equal s t -> - let c = massoc "val" attrs in - mf c args - | x -> raise (Marshal_error (t,x)) - -let singleton = function - | [x] -> x - | l -> raise (Marshal_error - ("singleton",PCData ("list of length " ^ string_of_int (List.length l)))) - -let raw_string = function - | [] -> "" - | [PCData s] -> s - | x::_ -> raise (Marshal_error("raw string",x)) - -(** Base types *) - -let of_unit () = Element ("unit", [], []) -let to_unit : xml -> unit = function - | Element ("unit", [], []) -> () - | x -> raise (Marshal_error ("unit",x)) - -let of_bool (b : bool) : xml = - if b then constructor "bool" "true" [] - else constructor "bool" "false" [] -let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with - | "true" -> true - | "false" -> false - | x -> raise (Marshal_error("bool",PCData x))) - -let of_list (f : 'a -> xml) (l : 'a list) = - Element ("list", [], List.map f l) -let to_list (f : xml -> 'a) : xml -> 'a list = function - | Element ("list", [], l) -> List.map f l - | x -> raise (Marshal_error("list",x)) - -let of_option (f : 'a -> xml) : 'a option -> xml = function - | None -> Element ("option", ["val", "none"], []) - | Some x -> Element ("option", ["val", "some"], [f x]) -let to_option (f : xml -> 'a) : xml -> 'a option = function - | Element ("option", ["val", "none"], []) -> None - | Element ("option", ["val", "some"], [x]) -> Some (f x) - | x -> raise (Marshal_error("option",x)) - -let of_string (s : string) : xml = Element ("string", [], [PCData s]) -let to_string : xml -> string = function - | Element ("string", [], l) -> raw_string l - | x -> raise (Marshal_error("string",x)) - -let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)]) -let to_int : xml -> int = function - | Element ("int", [], [PCData s]) -> - (try int_of_string s with Failure _ -> raise(Marshal_error("int",PCData s))) - | x -> raise (Marshal_error("int",x)) - -let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml = - Element ("pair", [], [f (fst x); g (snd x)]) -let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function - | Element ("pair", [], [x; y]) -> (f x, g y) - | x -> raise (Marshal_error("pair",x)) - -let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function - | CSig.Inl x -> Element ("union", ["val","in_l"], [f x]) - | CSig.Inr x -> Element ("union", ["val","in_r"], [g x]) -let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function - | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x) - | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x) - | x -> raise (Marshal_error("union",x)) - -(** More elaborate types *) - -let of_edit_id i = Element ("edit_id",["val",string_of_int i],[]) -let to_edit_id = function - | Element ("edit_id",["val",i],[]) -> - let id = int_of_string i in - assert (id <= 0 ); - id - | x -> raise (Marshal_error("edit_id",x)) - -let of_loc loc = - let start, stop = Loc.unloc loc in - Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[]) -let to_loc xml = - match xml with - | Element ("loc", l,[]) -> - let start = massoc "start" l in - let stop = massoc "stop" l in - (try - Loc.make_loc (int_of_string start, int_of_string stop) - with Not_found | Invalid_argument _ -> raise (Marshal_error("loc",PCData(start^":"^stop)))) - | x -> raise (Marshal_error("loc",x)) - -let of_xml x = Element ("xml", [], [x]) -let to_xml xml = match xml with -| Element ("xml", [], [x]) -> x -| x -> raise (Marshal_error("xml",x)) diff --git a/ide/protocol/serialize.mli b/ide/protocol/serialize.mli deleted file mode 100644 index 5d88defe55..0000000000 --- a/ide/protocol/serialize.mli +++ /dev/null @@ -1,41 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Xml_datatype - -exception Marshal_error of string * xml - -val massoc: string -> (string * string) list -> string -val constructor: string -> string -> xml list -> xml -val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b -val singleton: 'a list -> 'a -val raw_string: xml list -> string -val of_unit: unit -> xml -val to_unit: xml -> unit -val of_bool: bool -> xml -val to_bool: xml -> bool -val of_list: ('a -> xml) -> 'a list -> xml -val to_list: (xml -> 'a) -> xml -> 'a list -val of_option: ('a -> xml) -> 'a option -> xml -val to_option: (xml -> 'a) -> xml -> 'a option -val of_string: string -> xml -val to_string: xml -> string -val of_int: int -> xml -val to_int: xml -> int -val of_pair: ('a -> xml) -> ('b -> xml) -> 'a * 'b -> xml -val to_pair: (xml -> 'a) -> (xml -> 'b) -> xml -> 'a * 'b -val of_union: ('a -> xml) -> ('b -> xml) -> ('a, 'b) CSig.union -> xml -val to_union: (xml -> 'a) -> (xml -> 'b) -> xml -> ('a, 'b) CSig.union -val of_edit_id: int -> xml -val to_edit_id: xml -> int -val of_loc : Loc.t -> xml -val to_loc : xml -> Loc.t -val of_xml : xml -> xml -val to_xml : xml -> xml diff --git a/ide/protocol/xml_lexer.mli b/ide/protocol/xml_lexer.mli deleted file mode 100644 index 920de9f9c3..0000000000 --- a/ide/protocol/xml_lexer.mli +++ /dev/null @@ -1,44 +0,0 @@ -(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -type error = - | EUnterminatedComment - | EUnterminatedString - | EIdentExpected - | ECloseExpected - | ENodeExpected - | EAttributeNameExpected - | EAttributeValueExpected - | EUnterminatedEntity - -exception Error of error - -type token = - | Tag of string * (string * string) list * bool - | PCData of string - | Endtag of string - | Eof - -type pos = int * int * int * int - -val init : Lexing.lexbuf -> unit -val close : unit -> unit -val token : Lexing.lexbuf -> token -val pos : Lexing.lexbuf -> pos -val restore : pos -> unit diff --git a/ide/protocol/xml_lexer.mll b/ide/protocol/xml_lexer.mll deleted file mode 100644 index e8bf7e16ae..0000000000 --- a/ide/protocol/xml_lexer.mll +++ /dev/null @@ -1,317 +0,0 @@ -{(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -open Lexing - -type error = - | EUnterminatedComment - | EUnterminatedString - | EIdentExpected - | ECloseExpected - | ENodeExpected - | EAttributeNameExpected - | EAttributeValueExpected - | EUnterminatedEntity - -exception Error of error - -type pos = int * int * int * int - -type token = - | Tag of string * (string * string) list * bool - | PCData of string - | Endtag of string - | Eof - -let last_pos = ref 0 -and current_line = ref 0 -and current_line_start = ref 0 - -let tmp = Buffer.create 200 - -let idents = Hashtbl.create 0 - -let _ = begin - Hashtbl.add idents "nbsp;" " "; - Hashtbl.add idents "gt;" ">"; - Hashtbl.add idents "lt;" "<"; - Hashtbl.add idents "amp;" "&"; - Hashtbl.add idents "apos;" "'"; - Hashtbl.add idents "quot;" "\""; -end - -let init lexbuf = - current_line := 1; - current_line_start := lexeme_start lexbuf; - last_pos := !current_line_start - -let close lexbuf = - Buffer.reset tmp - -let pos lexbuf = - !current_line , !current_line_start , - !last_pos , - lexeme_start lexbuf - -let restore (cl,cls,lp,_) = - current_line := cl; - current_line_start := cls; - last_pos := lp - -let newline lexbuf = - incr current_line; - last_pos := lexeme_end lexbuf; - current_line_start := !last_pos - -let error lexbuf e = - last_pos := lexeme_start lexbuf; - raise (Error e) - -} - -let newline = ['\n'] -let break = ['\r'] -let space = [' ' '\t'] -let identchar = ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.'] -let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar* -let entitychar = ['A'-'Z' 'a'-'z'] -let pcchar = [^ '\r' '\n' '<' '>' '&'] - -rule token = parse - | newline | (newline break) | break - { - newline lexbuf; - PCData "\n" - } - | "<!--" - { - last_pos := lexeme_start lexbuf; - comment lexbuf; - token lexbuf - } - | "<?" - { - last_pos := lexeme_start lexbuf; - header lexbuf; - token lexbuf; - } - | '<' space* '/' space* - { - last_pos := lexeme_start lexbuf; - let tag = ident_name lexbuf in - ignore_spaces lexbuf; - close_tag lexbuf; - Endtag tag - } - | '<' space* - { - last_pos := lexeme_start lexbuf; - let tag = ident_name lexbuf in - ignore_spaces lexbuf; - let attribs, closed = attributes lexbuf in - Tag(tag, attribs, closed) - } - | "&#" - { - last_pos := lexeme_start lexbuf; - Buffer.reset tmp; - Buffer.add_string tmp (lexeme lexbuf); - PCData (pcdata lexbuf) - } - | '&' - { - last_pos := lexeme_start lexbuf; - Buffer.reset tmp; - Buffer.add_string tmp (entity lexbuf); - PCData (pcdata lexbuf) - } - | pcchar+ - { - last_pos := lexeme_start lexbuf; - Buffer.reset tmp; - Buffer.add_string tmp (lexeme lexbuf); - PCData (pcdata lexbuf) - } - | eof { Eof } - | _ - { error lexbuf ENodeExpected } - -and ignore_spaces = parse - | newline | (newline break) | break - { - newline lexbuf; - ignore_spaces lexbuf - } - | space + - { ignore_spaces lexbuf } - | "" - { () } - -and comment = parse - | newline | (newline break) | break - { - newline lexbuf; - comment lexbuf - } - | "-->" - { () } - | eof - { raise (Error EUnterminatedComment) } - | _ - { comment lexbuf } - -and header = parse - | newline | (newline break) | break - { - newline lexbuf; - header lexbuf - } - | "?>" - { () } - | eof - { error lexbuf ECloseExpected } - | _ - { header lexbuf } - -and pcdata = parse - | newline | (newline break) | break - { - Buffer.add_char tmp '\n'; - newline lexbuf; - pcdata lexbuf - } - | pcchar+ - { - Buffer.add_string tmp (lexeme lexbuf); - pcdata lexbuf - } - | "&#" - { - Buffer.add_string tmp (lexeme lexbuf); - pcdata lexbuf; - } - | '&' - { - Buffer.add_string tmp (entity lexbuf); - pcdata lexbuf - } - | "" - { Buffer.contents tmp } - -and entity = parse - | entitychar+ ';' - { - let ident = lexeme lexbuf in - try - Hashtbl.find idents (String.lowercase_ascii ident) - with - Not_found -> "&" ^ ident - } - | _ | eof - { raise (Error EUnterminatedEntity) } - -and ident_name = parse - | ident - { lexeme lexbuf } - | _ | eof - { error lexbuf EIdentExpected } - -and close_tag = parse - | '>' - { () } - | _ | eof - { error lexbuf ECloseExpected } - -and attributes = parse - | '>' - { [], false } - | "/>" - { [], true } - | "" (* do not read a char ! *) - { - let key = attribute lexbuf in - let data = attribute_data lexbuf in - ignore_spaces lexbuf; - let others, closed = attributes lexbuf in - (key, data) :: others, closed - } - -and attribute = parse - | ident - { lexeme lexbuf } - | _ | eof - { error lexbuf EAttributeNameExpected } - -and attribute_data = parse - | space* '=' space* '"' - { - Buffer.reset tmp; - last_pos := lexeme_end lexbuf; - dq_string lexbuf - } - | space* '=' space* '\'' - { - Buffer.reset tmp; - last_pos := lexeme_end lexbuf; - q_string lexbuf - } - | _ | eof - { error lexbuf EAttributeValueExpected } - -and dq_string = parse - | '"' - { Buffer.contents tmp } - | '\\' [ '"' '\\' ] - { - Buffer.add_char tmp (lexeme_char lexbuf 1); - dq_string lexbuf - } - | '&' - { - Buffer.add_string tmp (entity lexbuf); - dq_string lexbuf - } - | eof - { raise (Error EUnterminatedString) } - | _ - { - Buffer.add_char tmp (lexeme_char lexbuf 0); - dq_string lexbuf - } - -and q_string = parse - | '\'' - { Buffer.contents tmp } - | '\\' [ '\'' '\\' ] - { - Buffer.add_char tmp (lexeme_char lexbuf 1); - q_string lexbuf - } - | '&' - { - Buffer.add_string tmp (entity lexbuf); - q_string lexbuf - } - | eof - { raise (Error EUnterminatedString) } - | _ - { - Buffer.add_char tmp (lexeme_char lexbuf 0); - q_string lexbuf - } diff --git a/ide/protocol/xml_parser.ml b/ide/protocol/xml_parser.ml deleted file mode 100644 index 8db3f9e8ba..0000000000 --- a/ide/protocol/xml_parser.ml +++ /dev/null @@ -1,232 +0,0 @@ -(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * Copyright (C) 2003 Jacques Garrigue - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -open Printf -open Xml_datatype - -type xml = Xml_datatype.xml - -type error_pos = { - eline : int; - eline_start : int; - emin : int; - emax : int; -} - -type error_msg = - | UnterminatedComment - | UnterminatedString - | UnterminatedEntity - | IdentExpected - | CloseExpected - | NodeExpected - | AttributeNameExpected - | AttributeValueExpected - | EndOfTagExpected of string - | EOFExpected - | Empty - -type error = error_msg * error_pos - -exception Error of error - -exception File_not_found of string - -type t = { - mutable check_eof : bool; - mutable concat_pcdata : bool; - source : Lexing.lexbuf; - stack : Xml_lexer.token Stack.t; -} - -type source = - | SChannel of in_channel - | SString of string - | SLexbuf of Lexing.lexbuf - -exception Internal_error of error_msg -exception NoMoreData - -let xml_error = ref (fun _ -> assert false) -let file_not_found = ref (fun _ -> assert false) - -let is_blank s = - let len = String.length s in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = s.[!i] in - (* no '\r' because we replaced them in the lexer *) - if c = ' ' || c = '\n' || c = '\t' then incr i - else break := false - done; - !i = len - -let _raises e f = - xml_error := e; - file_not_found := f - -let make source = - let source = match source with - | SChannel chan -> Lexing.from_channel chan - | SString s -> Lexing.from_string s - | SLexbuf lexbuf -> lexbuf - in - let () = Xml_lexer.init source in - { - check_eof = false; - concat_pcdata = true; - source = source; - stack = Stack.create (); - } - -let check_eof p v = p.check_eof <- v - -let pop s = - try - Stack.pop s.stack - with - Stack.Empty -> - Xml_lexer.token s.source - -let push t s = - Stack.push t s.stack - -let canonicalize l = - let has_elt = List.exists (function Element _ -> true | _ -> false) l in - if has_elt then List.filter (function PCData s -> not (is_blank s) | _ -> true) l - else l - -let rec read_xml do_not_canonicalize s = - let rec read_node s = - match pop s with - | Xml_lexer.PCData s -> PCData s - | Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, []) - | Xml_lexer.Tag (tag, attr, false) -> - let elements = read_elems tag s in - let elements = - if do_not_canonicalize then elements else canonicalize elements - in - Element (tag, attr, elements) - | t -> - push t s; - raise NoMoreData - - and read_elems tag s = - let elems = ref [] in - (try - while true do - let node = read_node s in - match node, !elems with - | PCData c , (PCData c2) :: q -> - elems := PCData (c2 ^ c) :: q - | _, l -> - elems := node :: l - done - with - NoMoreData -> ()); - match pop s with - | Xml_lexer.Endtag s when s = tag -> List.rev !elems - | t -> raise (Internal_error (EndOfTagExpected tag)) - in - match read_node s with - | (Element _) as node -> - node - | PCData c -> - if is_blank c then - read_xml do_not_canonicalize s - else - raise (Xml_lexer.Error Xml_lexer.ENodeExpected) - -let convert = function - | Xml_lexer.EUnterminatedComment -> UnterminatedComment - | Xml_lexer.EUnterminatedString -> UnterminatedString - | Xml_lexer.EIdentExpected -> IdentExpected - | Xml_lexer.ECloseExpected -> CloseExpected - | Xml_lexer.ENodeExpected -> NodeExpected - | Xml_lexer.EAttributeNameExpected -> AttributeNameExpected - | Xml_lexer.EAttributeValueExpected -> AttributeValueExpected - | Xml_lexer.EUnterminatedEntity -> UnterminatedEntity - -let error_of_exn xparser = function - | NoMoreData when pop xparser = Xml_lexer.Eof -> Empty - | NoMoreData -> NodeExpected - | Internal_error e -> e - | Xml_lexer.Error e -> convert e - | e -> - (*let e = Errors.push e in: We do not record backtrace here. *) - raise e - -let do_parse do_not_canonicalize xparser = - try - Xml_lexer.init xparser.source; - let x = read_xml do_not_canonicalize xparser in - if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected); - Xml_lexer.close (); - x - with any -> - Xml_lexer.close (); - raise (!xml_error (error_of_exn xparser any) xparser.source) - -let parse ?(do_not_canonicalize=false) p = - do_parse do_not_canonicalize p - -let error_msg = function - | UnterminatedComment -> "Unterminated comment" - | UnterminatedString -> "Unterminated string" - | UnterminatedEntity -> "Unterminated entity" - | IdentExpected -> "Ident expected" - | CloseExpected -> "Element close expected" - | NodeExpected -> "Xml node expected" - | AttributeNameExpected -> "Attribute name expected" - | AttributeValueExpected -> "Attribute value expected" - | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag - | EOFExpected -> "End of file expected" - | Empty -> "Empty" - -let error (msg,pos) = - if pos.emin = pos.emax then - sprintf "%s line %d character %d" (error_msg msg) pos.eline - (pos.emin - pos.eline_start) - else - sprintf "%s line %d characters %d-%d" (error_msg msg) pos.eline - (pos.emin - pos.eline_start) (pos.emax - pos.eline_start) - -let line e = e.eline - -let range e = - e.emin - e.eline_start , e.emax - e.eline_start - -let abs_range e = - e.emin , e.emax - -let pos source = - let line, lstart, min, max = Xml_lexer.pos source in - { - eline = line; - eline_start = lstart; - emin = min; - emax = max; - } - -let () = _raises (fun x p -> - (* local cast : Xml.error_msg -> error_msg *) - Error (x, pos p)) - (fun f -> File_not_found f) diff --git a/ide/protocol/xml_parser.mli b/ide/protocol/xml_parser.mli deleted file mode 100644 index ac2eab352f..0000000000 --- a/ide/protocol/xml_parser.mli +++ /dev/null @@ -1,106 +0,0 @@ -(* - * Xml Light, an small Xml parser/printer with DTD support. - * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com) - * - * This library is free software; you can redistribute it and/or - * modify it under the terms of the GNU Lesser General Public - * License as published by the Free Software Foundation; either - * version 2.1 of the License, or (at your option) any later version. - * - * This library is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU - * Lesser General Public License for more details. - * - * You should have received a copy of the GNU Lesser General Public - * License along with this library; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA - *) - -(** Xml Light Parser - - While basic parsing functions can be used in the {!Xml} module, this module - is providing a way to create, configure and run an Xml parser. - -*) - - -(** An Xml node is either - [Element (tag-name, attributes, children)] or [PCData text] *) -type xml = Xml_datatype.xml - -(** Abstract type for an Xml parser. *) -type t - -(** {6:exc Xml Exceptions} *) - -(** Several exceptions can be raised when parsing an Xml document : {ul - {li {!Xml.Error} is raised when an xml parsing error occurs. the - {!Xml.error_msg} tells you which error occurred during parsing - and the {!Xml.error_pos} can be used to retrieve the document - location where the error occurred at.} - {li {!Xml.File_not_found} is raised when an error occurred while - opening a file with the {!Xml.parse_file} function.} - } - *) - -type error_pos - -type error_msg = - | UnterminatedComment - | UnterminatedString - | UnterminatedEntity - | IdentExpected - | CloseExpected - | NodeExpected - | AttributeNameExpected - | AttributeValueExpected - | EndOfTagExpected of string - | EOFExpected - | Empty - -type error = error_msg * error_pos - -exception Error of error - -exception File_not_found of string - -(** Get a full error message from an Xml error. *) -val error : error -> string - -(** Get the Xml error message as a string. *) -val error_msg : error_msg -> string - -(** Get the line the error occurred at. *) -val line : error_pos -> int - -(** Get the relative character range (in current line) the error occurred at.*) -val range : error_pos -> int * int - -(** Get the absolute character range the error occurred at. *) -val abs_range : error_pos -> int * int - -val pos : Lexing.lexbuf -> error_pos - -(** Several kind of resources can contain Xml documents. *) -type source = -| SChannel of in_channel -| SString of string -| SLexbuf of Lexing.lexbuf - -(** This function returns a new parser with default options. *) -val make : source -> t - -(** When a Xml document is parsed, the parser may check that the end of the - document is reached, so for example parsing ["<A/><B/>"] will fail instead - of returning only the A element. You can turn on this check by setting - [check_eof] to [true] {i (by default, check_eof is false, unlike - in the original Xmllight)}. *) -val check_eof : t -> bool -> unit - -(** Once the parser is configured, you can run the parser on a any kind - of xml document source to parse its contents into an Xml data structure. - - When [do_not_canonicalize] is set, the XML document is given as - is, without trying to remove blank PCDATA elements. *) -val parse : ?do_not_canonicalize:bool -> t -> xml diff --git a/ide/protocol/xml_printer.ml b/ide/protocol/xml_printer.ml deleted file mode 100644 index f526618a6e..0000000000 --- a/ide/protocol/xml_printer.ml +++ /dev/null @@ -1,147 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Xml_datatype - -type xml = Xml_datatype.xml - -type target = TChannel of out_channel | TBuffer of Buffer.t - -type t = target - -let make x = x - -let buffer_pcdata tmp text = - let puts = Buffer.add_string tmp in - let putc = Buffer.add_char tmp in - let l = String.length text in - for p = 0 to l-1 do - match text.[p] with - | ' ' -> puts " "; - | '>' -> puts ">" - | '<' -> puts "<" - | '&' -> - if p < l - 1 && text.[p + 1] = '#' then - putc '&' - else - puts "&" - | '\'' -> puts "'" - | '"' -> puts """ - | c -> putc c - done - -let buffer_attr tmp (n,v) = - let puts = Buffer.add_string tmp in - let putc = Buffer.add_char tmp in - putc ' '; - puts n; - puts "=\""; - let l = String.length v in - for p = 0 to l - 1 do - match v.[p] with - | '\\' -> puts "\\\\" - | '"' -> puts "\\\"" - | '<' -> puts "<" - | '&' -> puts "&" - | c -> putc c - done; - putc '"' - -let to_buffer tmp x = - let pcdata = ref false in - let puts = Buffer.add_string tmp in - let putc = Buffer.add_char tmp in - let rec loop = function - | Element (tag,alist,[]) -> - putc '<'; - puts tag; - List.iter (buffer_attr tmp) alist; - puts "/>"; - pcdata := false; - | Element (tag,alist,l) -> - putc '<'; - puts tag; - List.iter (buffer_attr tmp) alist; - putc '>'; - pcdata := false; - List.iter loop l; - puts "</"; - puts tag; - putc '>'; - pcdata := false; - | PCData text -> - if !pcdata then putc ' '; - buffer_pcdata tmp text; - pcdata := true; - in - loop x - -let pcdata_to_string s = - let b = Buffer.create 13 in - buffer_pcdata b s; - Buffer.contents b - -let to_string x = - let b = Buffer.create 200 in - to_buffer b x; - Buffer.contents b - -let to_string_fmt x = - let tmp = Buffer.create 200 in - let puts = Buffer.add_string tmp in - let putc = Buffer.add_char tmp in - let rec loop ?(newl=false) tab = function - | Element (tag, alist, []) -> - puts tab; - putc '<'; - puts tag; - List.iter (buffer_attr tmp) alist; - puts "/>"; - if newl then putc '\n'; - | Element (tag, alist, [PCData text]) -> - puts tab; - putc '<'; - puts tag; - List.iter (buffer_attr tmp) alist; - puts ">"; - buffer_pcdata tmp text; - puts "</"; - puts tag; - putc '>'; - if newl then putc '\n'; - | Element (tag, alist, l) -> - puts tab; - putc '<'; - puts tag; - List.iter (buffer_attr tmp) alist; - puts ">\n"; - List.iter (loop ~newl:true (tab^" ")) l; - puts tab; - puts "</"; - puts tag; - putc '>'; - if newl then putc '\n'; - | PCData text -> - buffer_pcdata tmp text; - if newl then putc '\n'; - in - loop "" x; - Buffer.contents tmp - -let print t xml = - let tmp, flush = match t with - | TChannel oc -> - let b = Buffer.create 200 in - b, (fun () -> Buffer.output_buffer oc b; flush oc) - | TBuffer b -> - b, (fun () -> ()) - in - to_buffer tmp xml; - flush () diff --git a/ide/protocol/xml_printer.mli b/ide/protocol/xml_printer.mli deleted file mode 100644 index e60e3392ed..0000000000 --- a/ide/protocol/xml_printer.mli +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type xml = Xml_datatype.xml - -type t -type target = TChannel of out_channel | TBuffer of Buffer.t - -val make : target -> t - -(** Print the xml data structure to a source into a compact xml string (without - any user-readable formatting ). *) -val print : t -> xml -> unit - -(** Print the xml data structure into a compact xml string (without - any user-readable formatting ). *) -val to_string : xml -> string - -(** Print the xml data structure into an user-readable string with - tabs and lines break between different nodes. *) -val to_string_fmt : xml -> string - -(** Print PCDATA as a string by escaping XML entities. *) -val pcdata_to_string : string -> string diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml deleted file mode 100644 index 6cb0cec008..0000000000 --- a/ide/protocol/xmlprotocol.ml +++ /dev/null @@ -1,962 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Protocol version of this file. This is the date of the last modification. *) - -(** WARNING: TO BE UPDATED WHEN MODIFIED! *) - -let protocol_version = "20170413" - -type msg_format = Richpp of int | Ppcmds -let msg_format = ref (Richpp 72) - -(** * Interface of calls to Coq by CoqIde *) - -open Util -open Interface -open Serialize -open Xml_datatype - -(* Marshalling of basic types and type constructors *) -module Xml_marshalling = struct - -let of_search_cst = function - | Name_Pattern s -> - constructor "search_cst" "name_pattern" [of_string s] - | Type_Pattern s -> - constructor "search_cst" "type_pattern" [of_string s] - | SubType_Pattern s -> - constructor "search_cst" "subtype_pattern" [of_string s] - | In_Module m -> - constructor "search_cst" "in_module" [of_list of_string m] - | Include_Blacklist -> - constructor "search_cst" "include_blacklist" [] -let to_search_cst = do_match "search_cst" (fun s args -> match s with - | "name_pattern" -> Name_Pattern (to_string (singleton args)) - | "type_pattern" -> Type_Pattern (to_string (singleton args)) - | "subtype_pattern" -> SubType_Pattern (to_string (singleton args)) - | "in_module" -> In_Module (to_list to_string (singleton args)) - | "include_blacklist" -> Include_Blacklist - | x -> raise (Marshal_error("search",PCData x))) - -let of_coq_object f ans = - let prefix = of_list of_string ans.coq_object_prefix in - let qualid = of_list of_string ans.coq_object_qualid in - let obj = f ans.coq_object_object in - Element ("coq_object", [], [prefix; qualid; obj]) - -let to_coq_object f = function -| Element ("coq_object", [], [prefix; qualid; obj]) -> - let prefix = to_list to_string prefix in - let qualid = to_list to_string qualid in - let obj = f obj in { - coq_object_prefix = prefix; - coq_object_qualid = qualid; - coq_object_object = obj; - } -| x -> raise (Marshal_error("coq_object",x)) - -let of_option_value = function - | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i] - | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b] - | StringValue s -> constructor "option_value" "stringvalue" [of_string s] - | StringOptValue s -> constructor "option_value" "stringoptvalue" [of_option of_string s] -let to_option_value = do_match "option_value" (fun s args -> match s with - | "intvalue" -> IntValue (to_option to_int (singleton args)) - | "boolvalue" -> BoolValue (to_bool (singleton args)) - | "stringvalue" -> StringValue (to_string (singleton args)) - | "stringoptvalue" -> StringOptValue (to_option to_string (singleton args)) - | x -> raise (Marshal_error("*value",PCData x))) - -let of_option_state s = - Element ("option_state", [], [ - of_bool s.opt_sync; - of_bool s.opt_depr; - of_option_value s.opt_value]) -let to_option_state = function - | Element ("option_state", [], [sync; depr; value]) -> { - opt_sync = to_bool sync; - opt_depr = to_bool depr; - opt_value = to_option_value value } - | x -> raise (Marshal_error("option_state",x)) - -let to_stateid = function - | Element ("state_id",["val",i],[]) -> - let id = int_of_string i in - Stateid.of_int id - | _ -> raise (Invalid_argument "to_state_id") - -let of_stateid i = Element ("state_id",["val",string_of_int (Stateid.to_int i)],[]) - -let to_routeid = function - | Element ("route_id",["val",i],[]) -> - let id = int_of_string i in id - | _ -> raise (Invalid_argument "to_route_id") - -let of_routeid i = Element ("route_id",["val",string_of_int i],[]) - -let of_box (ppb : Pp.block_type) = let open Pp in match ppb with - | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] - | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] - | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i] - | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i] - -let to_box = let open Pp in - do_match "ppbox" (fun s args -> match s with - | "hbox" -> Pp_hbox (to_int (singleton args)) - | "vbox" -> Pp_vbox (to_int (singleton args)) - | "hvbox" -> Pp_hvbox (to_int (singleton args)) - | "hovbox" -> Pp_hovbox (to_int (singleton args)) - | x -> raise (Marshal_error("*ppbox",PCData x)) - ) - -let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with - | Ppcmd_empty -> constructor "ppdoc" "empty" [] - | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] - | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] - | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] - | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair of_string of_pp (t,s)] - | Ppcmd_print_break (i,j) - -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)] - | Ppcmd_force_newline -> constructor "ppdoc" "newline" [] - | Ppcmd_comment cmd -> constructor "ppdoc" "comment" [of_list of_string cmd] - - -let rec to_pp xpp = let open Pp in - Pp.unrepr @@ - do_match "ppdoc" (fun s args -> match s with - | "empty" -> Ppcmd_empty - | "string" -> Ppcmd_string (to_string (singleton args)) - | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) - | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in - Ppcmd_box(bt,s) - | "tag" -> let (tg,s) = to_pair to_string to_pp (singleton args) in - Ppcmd_tag(tg,s) - | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in - Ppcmd_print_break(i, j) - | "newline" -> Ppcmd_force_newline - | "comment" -> Ppcmd_comment (to_list to_string (singleton args)) - | x -> raise (Marshal_error("*ppdoc",PCData x)) - ) xpp - -let of_richpp x = Element ("richpp", [], [x]) - -(* Run-time Selectable *) -let of_pp (pp : Pp.t) = - match !msg_format with - | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp) - | Ppcmds -> of_pp pp - -let of_value f = function -| Good x -> Element ("value", ["val", "good"], [f x]) -| Fail (id,loc, msg) -> - let loc = match loc with - | None -> [] - | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in - let id = of_stateid id in - Element ("value", ["val", "fail"] @ loc, [id; of_pp msg]) - -let to_value f = function -| Element ("value", attrs, l) -> - let ans = massoc "val" attrs in - if ans = "good" then Good (f (singleton l)) - else if ans = "fail" then - let loc = - try - let loc_s = int_of_string (Serialize.massoc "loc_s" attrs) in - let loc_e = int_of_string (Serialize.massoc "loc_e" attrs) in - Some (loc_s, loc_e) - with Marshal_error _ | Failure _ -> None - in - let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in - let id = to_stateid id in - let msg = to_pp msg in - Fail (id, loc, msg) - else raise (Marshal_error("good or fail",PCData ans)) -| x -> raise (Marshal_error("value",x)) - -let of_status s = - let of_so = of_option of_string in - let of_sl = of_list of_string in - Element ("status", [], [ - of_sl s.status_path; - of_so s.status_proofname; - of_sl s.status_allproofs; - of_int s.status_proofnum; ]) -let to_status = function - | Element ("status", [], [path; name; prfs; pnum]) -> { - status_path = to_list to_string path; - status_proofname = to_option to_string name; - status_allproofs = to_list to_string prfs; - status_proofnum = to_int pnum; } - | x -> raise (Marshal_error("status",x)) - -let of_evar s = Element ("evar", [], [PCData s.evar_info]) -let to_evar = function - | Element ("evar", [], data) -> { evar_info = raw_string data; } - | x -> raise (Marshal_error("evar",x)) - -let of_goal g = - let hyp = of_list of_pp g.goal_hyp in - let ccl = of_pp g.goal_ccl in - let id = of_string g.goal_id in - Element ("goal", [], [id; hyp; ccl]) -let to_goal = function - | Element ("goal", [], [id; hyp; ccl]) -> - let hyp = to_list to_pp hyp in - let ccl = to_pp ccl in - let id = to_string id in - { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } - | x -> raise (Marshal_error("goal",x)) - -let of_goals g = - let of_glist = of_list of_goal in - let fg = of_list of_goal g.fg_goals in - let bg = of_list (of_pair of_glist of_glist) g.bg_goals in - let shelf = of_list of_goal g.shelved_goals in - let given_up = of_list of_goal g.given_up_goals in - Element ("goals", [], [fg; bg; shelf; given_up]) -let to_goals = function - | Element ("goals", [], [fg; bg; shelf; given_up]) -> - let to_glist = to_list to_goal in - let fg = to_list to_goal fg in - let bg = to_list (to_pair to_glist to_glist) bg in - let shelf = to_list to_goal shelf in - let given_up = to_list to_goal given_up in - { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; - given_up_goals = given_up } - | x -> raise (Marshal_error("goals",x)) - -let of_coq_info info = - let version = of_string info.coqtop_version in - let protocol = of_string info.protocol_version in - let release = of_string info.release_date in - let compile = of_string info.compile_date in - Element ("coq_info", [], [version; protocol; release; compile]) -let to_coq_info = function - | Element ("coq_info", [], [version; protocol; release; compile]) -> { - coqtop_version = to_string version; - protocol_version = to_string protocol; - release_date = to_string release; - compile_date = to_string compile; } - | x -> raise (Marshal_error("coq_info",x)) - -end -include Xml_marshalling - -(* Reification of basic types and type constructors, and functions - from to xml *) -module ReifType : sig - - type 'a val_t - - val unit_t : unit val_t - val string_t : string val_t - val int_t : int val_t - val bool_t : bool val_t - val xml_t : Xml_datatype.xml val_t - - val option_t : 'a val_t -> 'a option val_t - val list_t : 'a val_t -> 'a list val_t - val pair_t : 'a val_t -> 'b val_t -> ('a * 'b) val_t - val union_t : 'a val_t -> 'b val_t -> ('a ,'b) union val_t - - val goals_t : goals val_t - val evar_t : evar val_t - val state_t : status val_t - val option_state_t : option_state val_t - val option_value_t : option_value val_t - val coq_info_t : coq_info val_t - val coq_object_t : 'a val_t -> 'a coq_object val_t - val state_id_t : state_id val_t - val route_id_t : route_id val_t - val search_cst_t : search_constraint val_t - - val of_value_type : 'a val_t -> 'a -> xml - val to_value_type : 'a val_t -> xml -> 'a - - val print : 'a val_t -> 'a -> string - - type value_type - val erase : 'a val_t -> value_type - val print_type : value_type -> string - - val document_type_encoding : (xml -> string) -> unit - -end = struct - - type _ val_t = - | Unit : unit val_t - | String : string val_t - | Int : int val_t - | Bool : bool val_t - | Xml : Xml_datatype.xml val_t - - | Option : 'a val_t -> 'a option val_t - | List : 'a val_t -> 'a list val_t - | Pair : 'a val_t * 'b val_t -> ('a * 'b) val_t - | Union : 'a val_t * 'b val_t -> ('a, 'b) union val_t - - | Goals : goals val_t - | Evar : evar val_t - | State : status val_t - | Option_state : option_state val_t - | Option_value : option_value val_t - | Coq_info : coq_info val_t - | Coq_object : 'a val_t -> 'a coq_object val_t - | State_id : state_id val_t - | Route_id : route_id val_t - | Search_cst : search_constraint val_t - - type value_type = Value_type : 'a val_t -> value_type - - let erase (x : 'a val_t) = Value_type x - - let unit_t = Unit - let string_t = String - let int_t = Int - let bool_t = Bool - let xml_t = Xml - - let option_t x = Option x - let list_t x = List x - let pair_t x y = Pair (x, y) - let union_t x y = Union (x, y) - - let goals_t = Goals - let evar_t = Evar - let state_t = State - let option_state_t = Option_state - let option_value_t = Option_value - let coq_info_t = Coq_info - let coq_object_t x = Coq_object x - let state_id_t = State_id - let route_id_t = Route_id - let search_cst_t = Search_cst - - let of_value_type (ty : 'a val_t) : 'a -> xml = - let rec convert : type a. a val_t -> a -> xml = function - | Unit -> of_unit - | Bool -> of_bool - | Xml -> (fun x -> x) - | String -> of_string - | Int -> of_int - | State -> of_status - | Option_state -> of_option_state - | Option_value -> of_option_value - | Coq_info -> of_coq_info - | Goals -> of_goals - | Evar -> of_evar - | List t -> (of_list (convert t)) - | Option t -> (of_option (convert t)) - | Coq_object t -> (of_coq_object (convert t)) - | Pair (t1,t2) -> (of_pair (convert t1) (convert t2)) - | Union (t1,t2) -> (of_union (convert t1) (convert t2)) - | State_id -> of_stateid - | Route_id -> of_routeid - | Search_cst -> of_search_cst - in - convert ty - - let to_value_type (ty : 'a val_t) : xml -> 'a = - let rec convert : type a. a val_t -> xml -> a = function - | Unit -> to_unit - | Bool -> to_bool - | Xml -> (fun x -> x) - | String -> to_string - | Int -> to_int - | State -> to_status - | Option_state -> to_option_state - | Option_value -> to_option_value - | Coq_info -> to_coq_info - | Goals -> to_goals - | Evar -> to_evar - | List t -> (to_list (convert t)) - | Option t -> (to_option (convert t)) - | Coq_object t -> (to_coq_object (convert t)) - | Pair (t1,t2) -> (to_pair (convert t1) (convert t2)) - | Union (t1,t2) -> (to_union (convert t1) (convert t2)) - | State_id -> to_stateid - | Route_id -> to_routeid - | Search_cst -> to_search_cst - in - convert ty - - let pr_unit () = "" - let pr_string s = Printf.sprintf "%S" s - let pr_int i = string_of_int i - let pr_bool b = Printf.sprintf "%B" b - let pr_goal (g : goals) = - if g.fg_goals = [] then - if g.bg_goals = [] then "Proof completed." - else - let rec pr_focus _ = function - | [] -> assert false - | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg) - | (lg, rg) :: l -> - Printf.sprintf "%i:%a" - (List.length lg + List.length rg) pr_focus l in - Printf.sprintf "Still focused: [%a]." pr_focus g.bg_goals - else - let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^ - Pp.string_of_ppcmds goal ^ "]" in - String.concat " " (List.map pr_goal g.fg_goals) - let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" - let pr_status (s : status) = - let path = - let l = String.concat "." s.status_path in - "path=" ^ l ^ ";" in - let name = match s.status_proofname with - | None -> "no proof;" - | Some n -> "proof = " ^ n ^ ";" in - "Status: " ^ path ^ name - let pr_coq_info (i : coq_info) = "FIXME" - let pr_option_value = function - | IntValue None -> "none" - | IntValue (Some i) -> string_of_int i - | StringValue s -> s - | StringOptValue None -> "none" - | StringOptValue (Some s) -> s - | BoolValue b -> if b then "true" else "false" - let pr_option_state (s : option_state) = - Printf.sprintf "sync := %b; depr := %b; value := %s\n" - s.opt_sync s.opt_depr (pr_option_value s.opt_value) - let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]" - let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")" - let pr_coq_object (o : 'a coq_object) = "FIXME" - let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")" - let pr_union pr1 pr2 = function Inl x -> "Inl "^pr1 x | Inr x -> "Inr "^pr2 x - let pr_state_id = Stateid.to_string - - let pr_search_cst = function - | Name_Pattern s -> "Name_Pattern " ^ s - | Type_Pattern s -> "Type_Pattern " ^ s - | SubType_Pattern s -> "SubType_Pattern " ^ s - | In_Module s -> "In_Module " ^ String.concat "." s - | Include_Blacklist -> "Include_Blacklist" - - let rec print : type a. a val_t -> a -> string = function - | Unit -> pr_unit - | Bool -> pr_bool - | String -> pr_string - | Xml -> Xml_printer.to_string_fmt - | Int -> pr_int - | State -> pr_status - | Option_state -> pr_option_state - | Option_value -> pr_option_value - | Search_cst -> pr_search_cst - | Coq_info -> pr_coq_info - | Goals -> pr_goal - | Evar -> pr_evar - | List t -> (pr_list (print t)) - | Option t -> (pr_option (print t)) - | Coq_object t -> pr_coq_object - | Pair (t1,t2) -> (pr_pair (print t1) (print t2)) - | Union (t1,t2) -> (pr_union (print t1) (print t2)) - | State_id -> pr_state_id - | Route_id -> pr_int - - (* This is to break if a rename/refactoring makes the strings below outdated *) - type 'a exists = bool - - let rec print_val_t : type a. a val_t -> string = function - | Unit -> "unit" - | Bool -> "bool" - | String -> "string" - | Xml -> "xml" - | Int -> "int" - | State -> assert(true : status exists); "Interface.status" - | Option_state -> assert(true : option_state exists); "Interface.option_state" - | Option_value -> assert(true : option_value exists); "Interface.option_value" - | Search_cst -> assert(true : search_constraint exists); "Interface.search_constraint" - | Coq_info -> assert(true : coq_info exists); "Interface.coq_info" - | Goals -> assert(true : goals exists); "Interface.goals" - | Evar -> assert(true : evar exists); "Interface.evar" - | List t -> Printf.sprintf "(%s list)" (print_val_t t) - | Option t -> Printf.sprintf "(%s option)" (print_val_t t) - | Coq_object t -> assert(true : 'a coq_object exists); - Printf.sprintf "(%s Interface.coq_object)" (print_val_t t) - | Pair (t1,t2) -> Printf.sprintf "(%s * %s)" (print_val_t t1) (print_val_t t2) - | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists); - Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2) - | State_id -> assert(true : Stateid.t exists); "Stateid.t" - | Route_id -> assert(true : route_id exists); "route_id" - - let print_type = function Value_type ty -> print_val_t ty - - let document_type_encoding pr_xml = - Printf.printf "\n=== Data encoding by examples ===\n\n"; - Printf.printf "%s:\n\n%s\n\n" (print_val_t Unit) (pr_xml (of_unit ())); - Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t Bool) - (pr_xml (of_bool true)) (pr_xml (of_bool false)); - Printf.printf "%s:\n\n%s\n\n" (print_val_t String) (pr_xml (of_string "hello")); - Printf.printf "%s:\n\n%s\n\n" (print_val_t Int) (pr_xml (of_int 256)); - Printf.printf "%s:\n\n%s\n\n" (print_val_t State_id) (pr_xml (of_stateid Stateid.initial)); - Printf.printf "%s:\n\n%s\n\n" (print_val_t (List Int)) (pr_xml (of_list of_int [3;4;5])); - Printf.printf "%s:\n\n%s\n%s\n\n" (print_val_t (Option Int)) - (pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None)); - Printf.printf "%s:\n\n%s\n\n" (print_val_t (Pair (Bool,Int))) - (pr_xml (of_pair of_bool of_int (false,3))); - Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int))) - (pr_xml (of_union of_bool of_int (Inl false))); - print_endline ("All other types are records represented by a node named like the OCaml\n"^ - "type which contains a flattened n-tuple. We provide one example.\n"); - Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state) - (pr_xml (of_option_state { opt_sync = true; opt_depr = false; - opt_value = IntValue (Some 37) })); - -end -open ReifType - -(** Types reification, checked with explicit casts *) -let add_sty_t : add_sty val_t = - pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t) -let edit_at_sty_t : edit_at_sty val_t = state_id_t -let query_sty_t : query_sty val_t = pair_t route_id_t (pair_t string_t state_id_t) -let goals_sty_t : goals_sty val_t = unit_t -let evars_sty_t : evars_sty val_t = unit_t -let hints_sty_t : hints_sty val_t = unit_t -let status_sty_t : status_sty val_t = bool_t -let search_sty_t : search_sty val_t = list_t (pair_t search_cst_t bool_t) -let get_options_sty_t : get_options_sty val_t = unit_t -let set_options_sty_t : set_options_sty val_t = - list_t (pair_t (list_t string_t) option_value_t) -let mkcases_sty_t : mkcases_sty val_t = string_t -let quit_sty_t : quit_sty val_t = unit_t -let wait_sty_t : wait_sty val_t = unit_t -let about_sty_t : about_sty val_t = unit_t -let init_sty_t : init_sty val_t = option_t string_t -let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t -let stop_worker_sty_t : stop_worker_sty val_t = string_t -let print_ast_sty_t : print_ast_sty val_t = state_id_t -let annotate_sty_t : annotate_sty val_t = string_t - -let add_rty_t : add_rty val_t = - pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) -let edit_at_rty_t : edit_at_rty val_t = - union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t)) -let query_rty_t : query_rty val_t = unit_t -let goals_rty_t : goals_rty val_t = option_t goals_t -let evars_rty_t : evars_rty val_t = option_t (list_t evar_t) -let hints_rty_t : hints_rty val_t = - let hint = list_t (pair_t string_t string_t) in - option_t (pair_t (list_t hint) hint) -let status_rty_t : status_rty val_t = state_t -let search_rty_t : search_rty val_t = list_t (coq_object_t string_t) -let get_options_rty_t : get_options_rty val_t = - list_t (pair_t (list_t string_t) option_state_t) -let set_options_rty_t : set_options_rty val_t = unit_t -let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t) -let quit_rty_t : quit_rty val_t = unit_t -let wait_rty_t : wait_rty val_t = unit_t -let about_rty_t : about_rty val_t = coq_info_t -let init_rty_t : init_rty val_t = state_id_t -let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t) -let stop_worker_rty_t : stop_worker_rty val_t = unit_t -let print_ast_rty_t : print_ast_rty val_t = xml_t -let annotate_rty_t : annotate_rty val_t = xml_t - -let ($) x = erase x -let calls = [| - "Add", ($)add_sty_t, ($)add_rty_t; - "Edit_at", ($)edit_at_sty_t, ($)edit_at_rty_t; - "Query", ($)query_sty_t, ($)query_rty_t; - "Goal", ($)goals_sty_t, ($)goals_rty_t; - "Evars", ($)evars_sty_t, ($)evars_rty_t; - "Hints", ($)hints_sty_t, ($)hints_rty_t; - "Status", ($)status_sty_t, ($)status_rty_t; - "Search", ($)search_sty_t, ($)search_rty_t; - "GetOptions", ($)get_options_sty_t, ($)get_options_rty_t; - "SetOptions", ($)set_options_sty_t, ($)set_options_rty_t; - "MkCases", ($)mkcases_sty_t, ($)mkcases_rty_t; - "Quit", ($)quit_sty_t, ($)quit_rty_t; - "Wait", ($)wait_sty_t, ($)wait_rty_t; - "About", ($)about_sty_t, ($)about_rty_t; - "Init", ($)init_sty_t, ($)init_rty_t; - "Interp", ($)interp_sty_t, ($)interp_rty_t; - "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t; - "PrintAst", ($)print_ast_sty_t, ($)print_ast_rty_t; - "Annotate", ($)annotate_sty_t, ($)annotate_rty_t; -|] - -type 'a call = - | Add : add_sty -> add_rty call - | Edit_at : edit_at_sty -> edit_at_rty call - | Query : query_sty -> query_rty call - | Goal : goals_sty -> goals_rty call - | Evars : evars_sty -> evars_rty call - | Hints : hints_sty -> hints_rty call - | Status : status_sty -> status_rty call - | Search : search_sty -> search_rty call - | GetOptions : get_options_sty -> get_options_rty call - | SetOptions : set_options_sty -> set_options_rty call - | MkCases : mkcases_sty -> mkcases_rty call - | Quit : quit_sty -> quit_rty call - | About : about_sty -> about_rty call - | Init : init_sty -> init_rty call - | StopWorker : stop_worker_sty -> stop_worker_rty call - (* internal use (fake_ide) only, do not use *) - | Wait : wait_sty -> wait_rty call - (* retrocompatibility *) - | Interp : interp_sty -> interp_rty call - | PrintAst : print_ast_sty -> print_ast_rty call - | Annotate : annotate_sty -> annotate_rty call - -let id_of_call : type a. a call -> int = function - | Add _ -> 0 - | Edit_at _ -> 1 - | Query _ -> 2 - | Goal _ -> 3 - | Evars _ -> 4 - | Hints _ -> 5 - | Status _ -> 6 - | Search _ -> 7 - | GetOptions _ -> 8 - | SetOptions _ -> 9 - | MkCases _ -> 10 - | Quit _ -> 11 - | Wait _ -> 12 - | About _ -> 13 - | Init _ -> 14 - | Interp _ -> 15 - | StopWorker _ -> 16 - | PrintAst _ -> 17 - | Annotate _ -> 18 - -let str_of_call c = pi1 calls.(id_of_call c) - -type unknown_call = Unknown : 'a call -> unknown_call - -(** We use phantom types and GADT to protect ourselves against wild casts *) -let add x : add_rty call = Add x -let edit_at x : edit_at_rty call = Edit_at x -let query x : query_rty call = Query x -let goals x : goals_rty call = Goal x -let evars x : evars_rty call = Evars x -let hints x : hints_rty call = Hints x -let status x : status_rty call = Status x -let get_options x : get_options_rty call = GetOptions x -let set_options x : set_options_rty call = SetOptions x -let mkcases x : mkcases_rty call = MkCases x -let search x : search_rty call = Search x -let quit x : quit_rty call = Quit x -let init x : init_rty call = Init x -let wait x : wait_rty call = Wait x -let interp x : interp_rty call = Interp x -let stop_worker x : stop_worker_rty call = StopWorker x -let print_ast x : print_ast_rty call = PrintAst x -let annotate x : annotate_rty call = Annotate x - -let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> - let mkGood : type a. a -> a value = fun x -> Good x in - try - match c with - | Add x -> mkGood (handler.add x) - | Edit_at x -> mkGood (handler.edit_at x) - | Query x -> mkGood (handler.query x) - | Goal x -> mkGood (handler.goals x) - | Evars x -> mkGood (handler.evars x) - | Hints x -> mkGood (handler.hints x) - | Status x -> mkGood (handler.status x) - | Search x -> mkGood (handler.search x) - | GetOptions x -> mkGood (handler.get_options x) - | SetOptions x -> mkGood (handler.set_options x) - | MkCases x -> mkGood (handler.mkcases x) - | Quit x -> mkGood (handler.quit x) - | Wait x -> mkGood (handler.wait x) - | About x -> mkGood (handler.about x) - | Init x -> mkGood (handler.init x) - | Interp x -> mkGood (handler.interp x) - | StopWorker x -> mkGood (handler.stop_worker x) - | PrintAst x -> mkGood (handler.print_ast x) - | Annotate x -> mkGood (handler.annotate x) - with any -> - let any = Exninfo.capture any in - Fail (handler.handle_exn any) - -(** brain dead code, edit if protocol messages are added/removed *) -let of_answer : type a. a call -> a value -> xml = function - | Add _ -> of_value (of_value_type add_rty_t ) - | Edit_at _ -> of_value (of_value_type edit_at_rty_t ) - | Query _ -> of_value (of_value_type query_rty_t ) - | Goal _ -> of_value (of_value_type goals_rty_t ) - | Evars _ -> of_value (of_value_type evars_rty_t ) - | Hints _ -> of_value (of_value_type hints_rty_t ) - | Status _ -> of_value (of_value_type status_rty_t ) - | Search _ -> of_value (of_value_type search_rty_t ) - | GetOptions _ -> of_value (of_value_type get_options_rty_t) - | SetOptions _ -> of_value (of_value_type set_options_rty_t) - | MkCases _ -> of_value (of_value_type mkcases_rty_t ) - | Quit _ -> of_value (of_value_type quit_rty_t ) - | Wait _ -> of_value (of_value_type wait_rty_t ) - | About _ -> of_value (of_value_type about_rty_t ) - | Init _ -> of_value (of_value_type init_rty_t ) - | Interp _ -> of_value (of_value_type interp_rty_t ) - | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) - | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) - | Annotate _ -> of_value (of_value_type annotate_rty_t ) - -let of_answer msg_fmt = - msg_format := msg_fmt; of_answer - -let to_answer : type a. a call -> xml -> a value = function - | Add _ -> to_value (to_value_type add_rty_t ) - | Edit_at _ -> to_value (to_value_type edit_at_rty_t ) - | Query _ -> to_value (to_value_type query_rty_t ) - | Goal _ -> to_value (to_value_type goals_rty_t ) - | Evars _ -> to_value (to_value_type evars_rty_t ) - | Hints _ -> to_value (to_value_type hints_rty_t ) - | Status _ -> to_value (to_value_type status_rty_t ) - | Search _ -> to_value (to_value_type search_rty_t ) - | GetOptions _ -> to_value (to_value_type get_options_rty_t) - | SetOptions _ -> to_value (to_value_type set_options_rty_t) - | MkCases _ -> to_value (to_value_type mkcases_rty_t ) - | Quit _ -> to_value (to_value_type quit_rty_t ) - | Wait _ -> to_value (to_value_type wait_rty_t ) - | About _ -> to_value (to_value_type about_rty_t ) - | Init _ -> to_value (to_value_type init_rty_t ) - | Interp _ -> to_value (to_value_type interp_rty_t ) - | StopWorker _ -> to_value (to_value_type stop_worker_rty_t) - | PrintAst _ -> to_value (to_value_type print_ast_rty_t ) - | Annotate _ -> to_value (to_value_type annotate_rty_t ) - -let of_call : type a. a call -> xml = fun q -> - let mkCall x = constructor "call" (str_of_call q) [x] in - match q with - | Add x -> mkCall (of_value_type add_sty_t x) - | Edit_at x -> mkCall (of_value_type edit_at_sty_t x) - | Query x -> mkCall (of_value_type query_sty_t x) - | Goal x -> mkCall (of_value_type goals_sty_t x) - | Evars x -> mkCall (of_value_type evars_sty_t x) - | Hints x -> mkCall (of_value_type hints_sty_t x) - | Status x -> mkCall (of_value_type status_sty_t x) - | Search x -> mkCall (of_value_type search_sty_t x) - | GetOptions x -> mkCall (of_value_type get_options_sty_t x) - | SetOptions x -> mkCall (of_value_type set_options_sty_t x) - | MkCases x -> mkCall (of_value_type mkcases_sty_t x) - | Quit x -> mkCall (of_value_type quit_sty_t x) - | Wait x -> mkCall (of_value_type wait_sty_t x) - | About x -> mkCall (of_value_type about_sty_t x) - | Init x -> mkCall (of_value_type init_sty_t x) - | Interp x -> mkCall (of_value_type interp_sty_t x) - | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x) - | PrintAst x -> mkCall (of_value_type print_ast_sty_t x) - | Annotate x -> mkCall (of_value_type annotate_sty_t x) - -let to_call : xml -> unknown_call = - do_match "call" (fun s a -> - let mkCallArg vt a = to_value_type vt (singleton a) in - match s with - | "Add" -> Unknown (Add (mkCallArg add_sty_t a)) - | "Edit_at" -> Unknown (Edit_at (mkCallArg edit_at_sty_t a)) - | "Query" -> Unknown (Query (mkCallArg query_sty_t a)) - | "Goal" -> Unknown (Goal (mkCallArg goals_sty_t a)) - | "Evars" -> Unknown (Evars (mkCallArg evars_sty_t a)) - | "Hints" -> Unknown (Hints (mkCallArg hints_sty_t a)) - | "Status" -> Unknown (Status (mkCallArg status_sty_t a)) - | "Search" -> Unknown (Search (mkCallArg search_sty_t a)) - | "GetOptions" -> Unknown (GetOptions (mkCallArg get_options_sty_t a)) - | "SetOptions" -> Unknown (SetOptions (mkCallArg set_options_sty_t a)) - | "MkCases" -> Unknown (MkCases (mkCallArg mkcases_sty_t a)) - | "Quit" -> Unknown (Quit (mkCallArg quit_sty_t a)) - | "Wait" -> Unknown (Wait (mkCallArg wait_sty_t a)) - | "About" -> Unknown (About (mkCallArg about_sty_t a)) - | "Init" -> Unknown (Init (mkCallArg init_sty_t a)) - | "Interp" -> Unknown (Interp (mkCallArg interp_sty_t a)) - | "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a)) - | "PrintAst" -> Unknown (PrintAst (mkCallArg print_ast_sty_t a)) - | "Annotate" -> Unknown (Annotate (mkCallArg annotate_sty_t a)) - | x -> raise (Marshal_error("call",PCData x))) - -(** Debug printing *) - -let pr_value_gen pr = function - | Good v -> "GOOD " ^ pr v - | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]" - | Fail (id,Some(i,j),str) -> - "FAIL "^Stateid.to_string id^ - " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]" -let pr_value v = pr_value_gen (fun _ -> "FIXME") v -let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with - | Add _ -> pr_value_gen (print add_rty_t ) value - | Edit_at _ -> pr_value_gen (print edit_at_rty_t ) value - | Query _ -> pr_value_gen (print query_rty_t ) value - | Goal _ -> pr_value_gen (print goals_rty_t ) value - | Evars _ -> pr_value_gen (print evars_rty_t ) value - | Hints _ -> pr_value_gen (print hints_rty_t ) value - | Status _ -> pr_value_gen (print status_rty_t ) value - | Search _ -> pr_value_gen (print search_rty_t ) value - | GetOptions _ -> pr_value_gen (print get_options_rty_t) value - | SetOptions _ -> pr_value_gen (print set_options_rty_t) value - | MkCases _ -> pr_value_gen (print mkcases_rty_t ) value - | Quit _ -> pr_value_gen (print quit_rty_t ) value - | Wait _ -> pr_value_gen (print wait_rty_t ) value - | About _ -> pr_value_gen (print about_rty_t ) value - | Init _ -> pr_value_gen (print init_rty_t ) value - | Interp _ -> pr_value_gen (print interp_rty_t ) value - | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) value - | PrintAst _ -> pr_value_gen (print print_ast_rty_t ) value - | Annotate _ -> pr_value_gen (print annotate_rty_t ) value -let pr_call : type a. a call -> string = fun call -> - let return what x = str_of_call call ^ " " ^ print what x in - match call with - | Add x -> return add_sty_t x - | Edit_at x -> return edit_at_sty_t x - | Query x -> return query_sty_t x - | Goal x -> return goals_sty_t x - | Evars x -> return evars_sty_t x - | Hints x -> return hints_sty_t x - | Status x -> return status_sty_t x - | Search x -> return search_sty_t x - | GetOptions x -> return get_options_sty_t x - | SetOptions x -> return set_options_sty_t x - | MkCases x -> return mkcases_sty_t x - | Quit x -> return quit_sty_t x - | Wait x -> return wait_sty_t x - | About x -> return about_sty_t x - | Init x -> return init_sty_t x - | Interp x -> return interp_sty_t x - | StopWorker x -> return stop_worker_sty_t x - | PrintAst x -> return print_ast_sty_t x - | Annotate x -> return annotate_sty_t x - -let document to_string_fmt = - Printf.printf "=== Available calls ===\n\n"; - Array.iter (fun (cname, csty, crty) -> - Printf.printf "%12s : %s\n %14s %s\n" - ("\""^cname^"\"") (print_type csty) "->" (print_type crty)) - calls; - Printf.printf "\n=== Calls XML encoding ===\n\n"; - Printf.printf "A call \"C\" carrying input a is encoded as:\n\n%s\n\n" - (to_string_fmt (constructor "call" "C" [PCData "a"])); - Printf.printf "A response carrying output b can either be:\n\n%s\n\n" - (to_string_fmt (of_value (fun _ -> PCData "b") (Good ()))); - Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n" - (to_string_fmt (of_value (fun _ -> PCData "b") - (Fail (Stateid.initial,Some (15,34), Pp.str "error message")))); - document_type_encoding to_string_fmt - -(* Moved from feedback.mli : This is IDE specific and we don't want to - pollute the core with it *) - -open Feedback - -let of_message_level = function - | Debug -> - Serialize.constructor "message_level" "debug" [] - | Info -> Serialize.constructor "message_level" "info" [] - | Notice -> Serialize.constructor "message_level" "notice" [] - | Warning -> Serialize.constructor "message_level" "warning" [] - | Error -> Serialize.constructor "message_level" "error" [] -let to_message_level = - Serialize.do_match "message_level" (fun s args -> match s with - | "debug" -> Debug - | "info" -> Info - | "notice" -> Notice - | "warning" -> Warning - | "error" -> Error - | x -> raise Serialize.(Marshal_error("error level",PCData x))) - -let of_message lvl loc msg = - let lvl = of_message_level lvl in - let xloc = of_option of_loc loc in - let content = of_pp msg in - Xml_datatype.Element ("message", [], [lvl; xloc; content]) - -let to_message xml = match xml with - | Xml_datatype.Element ("message", [], [lvl; xloc; content]) -> - Message(to_message_level lvl, to_option to_loc xloc, to_pp content) - | x -> raise (Marshal_error("message",x)) - -let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with - | "addedaxiom", _ -> AddedAxiom - | "processed", _ -> Processed - | "processingin", [where] -> ProcessingIn (to_string where) - | "incomplete", _ -> Incomplete - | "complete", _ -> Complete - | "globref", [loc; filepath; modpath; ident; ty] -> - GlobRef(to_loc loc, to_string filepath, - to_string modpath, to_string ident, to_string ty) - | "globdef", [loc; ident; secpath; ty] -> - GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) - | "inprogress", [n] -> InProgress (to_int n) - | "workerstatus", [ns] -> - let n, s = to_pair to_string to_string ns in - WorkerStatus(n,s) - | "custom", [loc;name;x]-> Custom (to_option to_loc loc, to_string name, x) - | "filedependency", [from; dep] -> - FileDependency (to_option to_string from, to_string dep) - | "fileloaded", [dirpath; filename] -> - FileLoaded (to_string dirpath, to_string filename) - | "message", [x] -> to_message x - | x,l -> raise (Marshal_error("feedback_content",PCData (x ^ " with attributes " ^ string_of_int (List.length l))))) - -let of_feedback_content = function - | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] - | Processed -> constructor "feedback_content" "processed" [] - | ProcessingIn where -> - constructor "feedback_content" "processingin" [of_string where] - | Incomplete -> constructor "feedback_content" "incomplete" [] - | Complete -> constructor "feedback_content" "complete" [] - | GlobRef(loc, filepath, modpath, ident, ty) -> - constructor "feedback_content" "globref" [ - of_loc loc; - of_string filepath; - of_string modpath; - of_string ident; - of_string ty ] - | GlobDef(loc, ident, secpath, ty) -> - constructor "feedback_content" "globdef" [ - of_loc loc; - of_string ident; - of_string secpath; - of_string ty ] - | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] - | WorkerStatus(n,s) -> - constructor "feedback_content" "workerstatus" - [of_pair of_string of_string (n,s)] - | Custom (loc, name, x) -> - constructor "feedback_content" "custom" [of_option of_loc loc; of_string name; x] - | FileDependency (from, depends_on) -> - constructor "feedback_content" "filedependency" [ - of_option of_string from; - of_string depends_on] - | FileLoaded (dirpath, filename) -> - constructor "feedback_content" "fileloaded" [ - of_string dirpath; - of_string filename ] - | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ] - -let of_edit_or_state_id id = ["object","state"], of_stateid id - -let of_feedback msg = - let content = of_feedback_content msg.contents in - let obj, id = of_edit_or_state_id msg.span_id in - let route = string_of_int msg.route in - Element ("feedback", obj @ ["route",route], [id;content]) - -let of_feedback msg_fmt = - msg_format := msg_fmt; of_feedback - -let to_feedback xml = match xml with - | Element ("feedback", ["object","state";"route",route], [id;content]) -> { - doc_id = 0; - span_id = to_stateid id; - route = int_of_string route; - contents = to_feedback_content content } - | x -> raise (Marshal_error("feedback",x)) - -let is_feedback = function - | Element ("feedback", _, _) -> true - | _ -> false - -(* vim: set foldmethod=marker: *) - diff --git a/ide/protocol/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli deleted file mode 100644 index 44584d44d7..0000000000 --- a/ide/protocol/xmlprotocol.mli +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** * Applicative part of the interface of CoqIde calls to Coq *) - -open Interface -open Xml_datatype - -type 'a call - -type unknown_call = Unknown : 'a call -> unknown_call - -val add : add_sty -> add_rty call -val edit_at : edit_at_sty -> edit_at_rty call -val query : query_sty -> query_rty call -val goals : goals_sty -> goals_rty call -val hints : hints_sty -> hints_rty call -val status : status_sty -> status_rty call -val mkcases : mkcases_sty -> mkcases_rty call -val evars : evars_sty -> evars_rty call -val search : search_sty -> search_rty call -val get_options : get_options_sty -> get_options_rty call -val set_options : set_options_sty -> set_options_rty call -val quit : quit_sty -> quit_rty call -val init : init_sty -> init_rty call -val stop_worker : stop_worker_sty -> stop_worker_rty call -(* internal use (fake_ide) only, do not use *) -val wait : wait_sty -> wait_rty call -(* retrocompatibility *) -val interp : interp_sty -> interp_rty call -val print_ast : print_ast_sty -> print_ast_rty call -val annotate : annotate_sty -> annotate_rty call - -val abstract_eval_call : handler -> 'a call -> 'a value - -(** * Protocol version *) - -val protocol_version : string - -(** By default, we still output messages in Richpp so we are - compatible with 8.6, however, 8.7 aware clients will want to - set this to Ppcmds *) -type msg_format = Richpp of int | Ppcmds - -(** * XML data marshalling *) - -val of_call : 'a call -> xml -val to_call : xml -> unknown_call - -val of_answer : msg_format -> 'a call -> 'a value -> xml -val to_answer : 'a call -> xml -> 'a value - -(* Prints the documentation of this module *) -val document : (xml -> string) -> unit - -(** * Debug printing *) - -val pr_call : 'a call -> string -val pr_value : 'a value -> string -val pr_full_value : 'a call -> 'a value -> string - -(** * Serializaiton of feedback *) -val of_feedback : msg_format -> Feedback.feedback -> xml -val to_feedback : xml -> Feedback.feedback - -val is_feedback : xml -> bool |