From bf12eb93f3f6a6a824a10878878fadd59745aae0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 10:57:43 +0100 Subject: Imported Upstream version 8.4pl1dfsg --- toplevel/ide_intf.ml | 152 +++++++++++++++++++++++++++------------------- toplevel/ide_intf.mli | 4 +- toplevel/ide_slave.ml | 59 +++++++++++------- toplevel/interface.mli | 12 ++-- toplevel/vernacentries.ml | 2 +- 5 files changed, 138 insertions(+), 91 deletions(-) (limited to 'toplevel') diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 0df24c7a..28f97dc8 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -45,7 +45,7 @@ type handler = { evars : unit -> evar list option; hints : unit -> (hint list * hint) option; status : unit -> status; - search : search_flags -> search_answer list; + search : search_flags -> string coq_object list; get_options : unit -> (option_name * option_state) list; set_options : (option_name * option_value) list -> unit; inloadpath : string -> bool; @@ -63,7 +63,7 @@ let goals : goals option call = Goal let evars : evar list option call = Evars let hints : (hint list * hint) option call = Hints let status : status call = Status -let search flags : search_answer list call = Search flags +let search flags : string coq_object list call = Search flags let get_options : (option_name * option_state) list call = GetOptions let set_options l : unit call = SetOptions l let inloadpath s : bool call = InLoadPath s @@ -81,7 +81,7 @@ let abstract_eval_call handler c = | Evars -> Obj.magic (handler.evars () : evar list option) | Hints -> Obj.magic (handler.hints () : (hint list * hint) option) | Status -> Obj.magic (handler.status () : status) - | Search flags -> Obj.magic (handler.search flags : search_answer list) + | Search flags -> Obj.magic (handler.search flags : string coq_object list) | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list) | SetOptions opts -> Obj.magic (handler.set_options opts : unit) | InLoadPath s -> Obj.magic (handler.inloadpath s : bool) @@ -130,6 +130,12 @@ let bool_arg tag b = if b then [tag, ""] else [] (** Base types *) +let of_unit () = Element ("unit", [], []) + +let to_unit = function + | Element ("unit", [], []) -> () + | _ -> raise Marshal_error + let of_bool b = if b then constructor "bool" "true" [] else constructor "bool" "false" [] @@ -166,7 +172,8 @@ let to_string = function let of_int i = Element ("int", [], [PCData (string_of_int i)]) let to_int = function -| Element ("int", [], [PCData s]) -> int_of_string s +| Element ("int", [], [PCData s]) -> + (try int_of_string s with Failure _ -> raise Marshal_error) | _ -> raise Marshal_error let of_pair f g (x, y) = Element ("pair", [], [f x; g y]) @@ -232,20 +239,20 @@ let to_search_constraint xml = do_match xml "search_constraint" | "include_blacklist" -> Include_Blacklist | _ -> raise Marshal_error) -let of_search_answer ans = - let path = of_list of_string ans.search_answer_full_path in - let name = of_string ans.search_answer_base_name in - let tpe = of_string ans.search_answer_type in - Element ("search_answer", [], [path; name; tpe]) - -let to_search_answer = function -| Element ("search_answer", [], [path; name; tpe]) -> - let path = to_list to_string path in - let name = to_string name in - let tpe = to_string tpe in { - search_answer_full_path = path; - search_answer_base_name = name; - search_answer_type = tpe; +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; } | _ -> raise Marshal_error @@ -412,51 +419,74 @@ let to_coq_info = function } | _ -> raise Marshal_error -let of_hints = - let of_hint = of_list (of_pair of_string of_string) in - of_option (of_pair (of_list of_hint) of_hint) - -let of_answer (q : 'a call) (r : 'a value) = - let convert = match q with - | Interp _ -> Obj.magic (of_string : string -> xml) - | Rewind _ -> Obj.magic (of_int : int -> xml) - | Goal -> Obj.magic (of_option of_goals : goals option -> xml) - | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml) - | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml) - | Status -> Obj.magic (of_status : status -> xml) - | Search _ -> Obj.magic (of_list of_search_answer : search_answer list -> xml) - | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml) - | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], [])) - | InLoadPath _ -> Obj.magic (of_bool : bool -> xml) - | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml) - | Quit -> Obj.magic (fun _ -> Element ("unit", [], [])) - | About -> Obj.magic (of_coq_info : coq_info -> xml) +(** Conversions between ['a value] and xml answers + + When decoding an xml answer, we dynamically check that it is compatible + with the original call. For that we now rely on the fact that all + sub-fonctions [to_xxx : xml -> xxx] check that the current xml element + is "xxx", and raise [Marshal_error] if anything goes wrong. +*) + +type value_type = + | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info + | Option of value_type + | List of value_type + | Coq_object of value_type + | Pair of value_type * value_type + +let hint = List (Pair (String, String)) +let option_name = List String + +let expected_answer_type = function + | Interp _ -> String + | Rewind _ -> Int + | Goal -> Option Goals + | Evars -> Option (List Evar) + | Hints -> Option (Pair (List hint, hint)) + | Status -> State + | Search _ -> List (Coq_object String) + | GetOptions -> List (Pair (option_name, Option_state)) + | SetOptions _ -> Unit + | InLoadPath _ -> Bool + | MkCases _ -> List (List String) + | Quit -> Unit + | About -> Coq_info + +let of_answer (q : 'a call) (r : 'a value) : xml = + let rec convert ty : 'a -> xml = match ty with + | Unit -> Obj.magic of_unit + | Bool -> Obj.magic of_bool + | String -> Obj.magic of_string + | Int -> Obj.magic of_int + | State -> Obj.magic of_status + | Option_state -> Obj.magic of_option_state + | Coq_info -> Obj.magic of_coq_info + | Goals -> Obj.magic of_goals + | Evar -> Obj.magic of_evar + | List t -> Obj.magic (of_list (convert t)) + | Option t -> Obj.magic (of_option (convert t)) + | Coq_object t -> Obj.magic (of_coq_object (convert t)) + | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2)) in - of_value convert r - -let to_answer xml = - let rec convert elt = match elt with - | Element (tpe, attrs, l) -> - begin match tpe with - | "unit" -> Obj.magic () - | "string" -> Obj.magic (to_string elt : string) - | "int" -> Obj.magic (to_int elt : int) - | "status" -> Obj.magic (to_status elt : status) - | "bool" -> Obj.magic (to_bool elt : bool) - | "list" -> Obj.magic (to_list convert elt : 'a list) - | "option" -> Obj.magic (to_option convert elt : 'a option) - | "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b)) - | "goals" -> Obj.magic (to_goals elt : goals) - | "evar" -> Obj.magic (to_evar elt : evar) - | "option_value" -> Obj.magic (to_option_value elt : option_value) - | "option_state" -> Obj.magic (to_option_state elt : option_state) - | "coq_info" -> Obj.magic (to_coq_info elt : coq_info) - | "search_answer" -> Obj.magic (to_search_answer elt : search_answer) - | _ -> raise Marshal_error - end - | _ -> raise Marshal_error + of_value (convert (expected_answer_type q)) r + +let to_answer xml (c : 'a call) : 'a value = + let rec convert ty : xml -> 'a = match ty with + | Unit -> Obj.magic to_unit + | Bool -> Obj.magic to_bool + | String -> Obj.magic to_string + | Int -> Obj.magic to_int + | State -> Obj.magic to_status + | Option_state -> Obj.magic to_option_state + | Coq_info -> Obj.magic to_coq_info + | Goals -> Obj.magic to_goals + | Evar -> Obj.magic to_evar + | List t -> Obj.magic (to_list (convert t)) + | Option t -> Obj.magic (to_option (convert t)) + | Coq_object t -> Obj.magic (to_coq_object (convert t)) + | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2)) in - to_value convert xml + to_value (convert (expected_answer_type c)) xml (** * Debug printing *) diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli index 26c6b671..7d0685b1 100644 --- a/toplevel/ide_intf.mli +++ b/toplevel/ide_intf.mli @@ -77,7 +77,7 @@ type handler = { evars : unit -> evar list option; hints : unit -> (hint list * hint) option; status : unit -> status; - search : search_flags -> search_answer list; + search : search_flags -> string coq_object list; get_options : unit -> (option_name * option_state) list; set_options : (option_name * option_value) list -> unit; inloadpath : string -> bool; @@ -104,7 +104,7 @@ val of_call : 'a call -> xml val to_call : xml -> 'a call val of_answer : 'a call -> 'a value -> xml -val to_answer : xml -> 'a value +val to_answer : xml -> 'a call -> 'a value (** * Debug printing *) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 681eec0d..d67b272e 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -127,25 +127,25 @@ let hyp_next_tac sigma env (id,_,ast) = let id_s = Names.string_of_id id in let type_s = string_of_ppcmds (pr_ltype_env env ast) in [ - ("clear "^id_s),("clear "^id_s^".\n"); - ("apply "^id_s),("apply "^id_s^".\n"); - ("exact "^id_s),("exact "^id_s^".\n"); - ("generalize "^id_s),("generalize "^id_s^".\n"); - ("absurd <"^id_s^">"),("absurd "^type_s^".\n") + ("clear "^id_s),("clear "^id_s^"."); + ("apply "^id_s),("apply "^id_s^"."); + ("exact "^id_s),("exact "^id_s^"."); + ("generalize "^id_s),("generalize "^id_s^"."); + ("absurd <"^id_s^">"),("absurd "^type_s^".") ] @ [ - ("discriminate "^id_s),("discriminate "^id_s^".\n"); - ("injection "^id_s),("injection "^id_s^".\n") + ("discriminate "^id_s),("discriminate "^id_s^"."); + ("injection "^id_s),("injection "^id_s^".") ] @ [ - ("rewrite "^id_s),("rewrite "^id_s^".\n"); - ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n") + ("rewrite "^id_s),("rewrite "^id_s^"."); + ("rewrite <- "^id_s),("rewrite <- "^id_s^".") ] @ [ - ("elim "^id_s), ("elim "^id_s^".\n"); - ("inversion "^id_s), ("inversion "^id_s^".\n"); - ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n") + ("elim "^id_s), ("elim "^id_s^"."); + ("inversion "^id_s), ("inversion "^id_s^"."); + ("inversion clear "^id_s), ("inversion_clear "^id_s^".") ] let concl_next_tac sigma concl = - let expand s = (s,s^".\n") in + let expand s = (s,s^".") in List.map expand ([ "intro"; "intros"; @@ -312,16 +312,26 @@ let search flags = in let ans = ref [] in let print_function ref env constr = - let name = Names.string_of_id (Nametab.basename_of_global ref) in - let make_path = Names.string_of_id in - let path = - List.rev_map make_path (Names.repr_dirpath (Nametab.dirpath_of_global ref)) - in - let answer = { - Interface.search_answer_full_path = path; - Interface.search_answer_base_name = name; - Interface.search_answer_type = string_of_ppcmds (pr_lconstr_env env constr); - } in + let fullpath = repr_dirpath (Nametab.dirpath_of_global ref) in + let qualid = Nametab.shortest_qualid_of_global Idset.empty ref in + let (shortpath, basename) = Libnames.repr_qualid qualid in + let shortpath = repr_dirpath shortpath in + (* [shortpath] is a suffix of [fullpath] and we're looking for the missing + prefix *) + let rec prefix full short accu = match full, short with + | _, [] -> + let full = List.rev_map string_of_id full in + (full, accu) + | _ :: full, m :: short -> + prefix full short (string_of_id m :: accu) + | _ -> assert false + in + let (prefix, qualid) = prefix fullpath shortpath [string_of_id basename] in + let answer = { + Interface.coq_object_prefix = prefix; + Interface.coq_object_qualid = qualid; + Interface.coq_object_object = string_of_ppcmds (pr_lconstr_env env constr); + } in ans := answer :: !ans; in let () = Search.gen_filtered_search filter_function print_function in @@ -432,6 +442,9 @@ let loop () = let () = pr_debug ("--> " ^ Ide_intf.pr_full_value q r) in Ide_intf.of_answer q r with + | Xml_parser.Error (Xml_parser.Empty, _) -> + pr_debug ("End of input, exiting"); + exit 0 | Xml_parser.Error (err, loc) -> let msg = "Syntax error in query: " ^ Xml_parser.error_msg err in fail msg diff --git a/toplevel/interface.mli b/toplevel/interface.mli index 39fb2a0e..7b4312a3 100644 --- a/toplevel/interface.mli +++ b/toplevel/interface.mli @@ -86,10 +86,14 @@ type search_constraint = the flag should be negated. *) type search_flags = (search_constraint * bool) list -type search_answer = { - search_answer_full_path : string list; - search_answer_base_name : string; - search_answer_type : string; +(** 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 = { diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fe6bf7db..6618b695 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -208,7 +208,7 @@ let show_match id = str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" in msg (v 1 (str "match # with" ++ fnl () ++ - prlist_with_sep fnl pr_branch patterns ++ fnl ())) + prlist_with_sep fnl pr_branch patterns ++ fnl () ++ str "end" ++ fnl ())) (* "Print" commands *) -- cgit v1.2.3