diff options
Diffstat (limited to 'ide/xmlprotocol.ml')
| -rw-r--r-- | ide/xmlprotocol.ml | 737 |
1 files changed, 737 insertions, 0 deletions
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml new file mode 100644 index 00000000..d337a911 --- /dev/null +++ b/ide/xmlprotocol.ml @@ -0,0 +1,737 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Protocol version of this file. This is the date of the last modification. *) + +(** WARNING: TO BE UPDATED WHEN MODIFIED! *) + +let protocol_version = "20140312" + +(** * 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 + | _ -> raise Marshal_error) + +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 + +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] +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)) + | _ -> raise Marshal_error) + +let of_option_state s = + Element ("option_state", [], [ + of_bool s.opt_sync; + of_bool s.opt_depr; + of_string s.opt_name; + of_option_value s.opt_value]) +let to_option_state = function + | Element ("option_state", [], [sync; depr; name; value]) -> { + opt_sync = to_bool sync; + opt_depr = to_bool depr; + opt_name = to_string name; + opt_value = to_option_value value } + | _ -> raise Marshal_error + + +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 = Stateid.to_xml id in + Element ("value", ["val", "fail"] @ loc, [id;PCData 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 = Stateid.of_xml (List.hd l) in + let msg = raw_string (List.tl l) in + Fail (id, loc, msg) + else raise Marshal_error +| _ -> raise Marshal_error + +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; } + | _ -> raise Marshal_error + +let of_evar s = Element ("evar", [], [PCData s.evar_info]) +let to_evar = function + | Element ("evar", [], data) -> { evar_info = raw_string data; } + | _ -> raise Marshal_error + +let of_goal g = + let hyp = of_list of_string g.goal_hyp in + let ccl = of_string 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_string hyp in + let ccl = to_string ccl in + let id = to_string id in + { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } + | _ -> raise Marshal_error + +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 } + | _ -> raise Marshal_error + +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; } + | _ -> raise Marshal_error + +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 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 value_type = + | Unit | String | Int | Bool | Xml + + | Option of value_type + | List of value_type + | Pair of value_type * value_type + | Union of value_type * value_type + + | Goals | Evar | State | Option_state | Option_value | Coq_info + | Coq_object of value_type + | State_id + | Search_cst + + 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 search_cst_t = Search_cst + + let of_value_type (ty : 'a val_t) : 'a -> xml = + let rec convert ty : 'a -> xml = match ty with + | Unit -> Obj.magic of_unit + | Bool -> Obj.magic of_bool + | Xml -> Obj.magic (fun x -> x) + | String -> Obj.magic of_string + | Int -> Obj.magic of_int + | State -> Obj.magic of_status + | Option_state -> Obj.magic of_option_state + | Option_value -> Obj.magic of_option_value + | 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)) + | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2)) + | State_id -> Obj.magic Stateid.to_xml + | Search_cst -> Obj.magic of_search_cst + in + convert ty + + let to_value_type (ty : 'a val_t) : xml -> 'a = + let rec convert ty : xml -> 'a = match ty with + | Unit -> Obj.magic to_unit + | Bool -> Obj.magic to_bool + | Xml -> Obj.magic (fun x -> x) + | String -> Obj.magic to_string + | Int -> Obj.magic to_int + | State -> Obj.magic to_status + | Option_state -> Obj.magic to_option_state + | Option_value -> Obj.magic to_option_value + | 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)) + | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2)) + | State_id -> Obj.magic Stateid.of_xml + | Search_cst -> Obj.magic 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 focussed: [%a]." pr_focus g.bg_goals + else + let pr_menu s = s in + let pr_goal { goal_hyp = hyps; goal_ccl = goal } = + "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ + pr_menu 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 + | BoolValue b -> if b then "true" else "false" + let pr_option_state (s : option_state) = + Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" + s.opt_sync s.opt_depr s.opt_name (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_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 = function + | Unit -> Obj.magic pr_unit + | Bool -> Obj.magic pr_bool + | String -> Obj.magic pr_string + | Xml -> Obj.magic Xml_printer.to_string_fmt + | Int -> Obj.magic pr_int + | State -> Obj.magic pr_status + | Option_state -> Obj.magic pr_option_state + | Option_value -> Obj.magic pr_option_value + | Search_cst -> Obj.magic pr_search_cst + | Coq_info -> Obj.magic pr_coq_info + | Goals -> Obj.magic pr_goal + | Evar -> Obj.magic pr_evar + | List t -> Obj.magic (pr_list (print t)) + | Option t -> Obj.magic (pr_option (print t)) + | Coq_object t -> Obj.magic pr_coq_object + | Pair (t1,t2) -> Obj.magic (pr_pair (print t1) (print t2)) + | Union (t1,t2) -> Obj.magic (pr_union (print t1) (print t2)) + | State_id -> Obj.magic pr_int + + (* This is to break if a rename/refactoring makes the strings below outdated *) + type 'a exists = bool + + let rec print_type = 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_type t) + | Option t -> Printf.sprintf "(%s option)" (print_type t) + | Coq_object t -> assert(true : 'a coq_object exists); + Printf.sprintf "(%s Interface.coq_object)" (print_type t) + | Pair (t1,t2) -> Printf.sprintf "(%s * %s)" (print_type t1) (print_type t2) + | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists); + Printf.sprintf "((%s, %s) CSig.union)" (print_type t1) (print_type t2) + | State_id -> assert(true : Stateid.t exists); "Stateid.t" + + let document_type_encoding pr_xml = + Printf.printf "\n=== Data encoding by examples ===\n\n"; + Printf.printf "%s:\n\n%s\n\n" (print_type Unit) (pr_xml (of_unit ())); + Printf.printf "%s:\n\n%s\n%s\n\n" (print_type Bool) + (pr_xml (of_bool true)) (pr_xml (of_bool false)); + Printf.printf "%s:\n\n%s\n\n" (print_type String) (pr_xml (of_string "hello")); + Printf.printf "%s:\n\n%s\n\n" (print_type Int) (pr_xml (of_int 256)); + Printf.printf "%s:\n\n%s\n\n" (print_type State_id) (pr_xml (Stateid.to_xml Stateid.initial)); + Printf.printf "%s:\n\n%s\n\n" (print_type (List Int)) (pr_xml (of_list of_int [3;4;5])); + Printf.printf "%s:\n\n%s\n%s\n\n" (print_type (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_type (Pair (Bool,Int))) + (pr_xml (of_pair of_bool of_int (false,3))); + Printf.printf "%s:\n\n%s\n\n" (print_type (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_type Option_state) + (pr_xml (of_option_state { opt_sync = true; opt_depr = false; + opt_name = "name1"; 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 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 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 = string_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 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; + "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 of add_sty + | Edit_at of edit_at_sty + | Query of query_sty + | Goal of goals_sty + | Evars of evars_sty + | Hints of hints_sty + | Status of status_sty + | Search of search_sty + | GetOptions of get_options_sty + | SetOptions of set_options_sty + | MkCases of mkcases_sty + | Quit of quit_sty + | About of about_sty + | Init of init_sty + | StopWorker of stop_worker_sty + (* retrocompatibility *) + | Interp of interp_sty + | PrintAst of print_ast_sty + | Annotate of annotate_sty + +let id_of_call = 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 + | About _ -> 12 + | Init _ -> 13 + | Interp _ -> 14 + | StopWorker _ -> 15 + | PrintAst _ -> 16 + | Annotate _ -> 17 + +let str_of_call c = pi1 calls.(id_of_call c) + +type unknown + +(** 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 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 handler (c : 'a call) : 'a value = + let mkGood x : 'a value = Good (Obj.magic 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) + | 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 = Errors.push any in + Fail (handler.handle_exn any) + +(** brain dead code, edit if protocol messages are added/removed *) +let of_answer (q : 'a call) (v : 'a value) : xml = match q with + | Add _ -> of_value (of_value_type add_rty_t ) (Obj.magic v) + | Edit_at _ -> of_value (of_value_type edit_at_rty_t ) (Obj.magic v) + | Query _ -> of_value (of_value_type query_rty_t ) (Obj.magic v) + | Goal _ -> of_value (of_value_type goals_rty_t ) (Obj.magic v) + | Evars _ -> of_value (of_value_type evars_rty_t ) (Obj.magic v) + | Hints _ -> of_value (of_value_type hints_rty_t ) (Obj.magic v) + | Status _ -> of_value (of_value_type status_rty_t ) (Obj.magic v) + | Search _ -> of_value (of_value_type search_rty_t ) (Obj.magic v) + | GetOptions _ -> of_value (of_value_type get_options_rty_t) (Obj.magic v) + | SetOptions _ -> of_value (of_value_type set_options_rty_t) (Obj.magic v) + | MkCases _ -> of_value (of_value_type mkcases_rty_t ) (Obj.magic v) + | Quit _ -> of_value (of_value_type quit_rty_t ) (Obj.magic v) + | About _ -> of_value (of_value_type about_rty_t ) (Obj.magic v) + | Init _ -> of_value (of_value_type init_rty_t ) (Obj.magic v) + | Interp _ -> of_value (of_value_type interp_rty_t ) (Obj.magic v) + | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) (Obj.magic v) + | PrintAst _ -> of_value (of_value_type print_ast_rty_t ) (Obj.magic v) + | Annotate _ -> of_value (of_value_type annotate_rty_t ) (Obj.magic v) + +let to_answer (q : 'a call) (x : xml) : 'a value = match q with + | Add _ -> Obj.magic (to_value (to_value_type add_rty_t ) x) + | Edit_at _ -> Obj.magic (to_value (to_value_type edit_at_rty_t ) x) + | Query _ -> Obj.magic (to_value (to_value_type query_rty_t ) x) + | Goal _ -> Obj.magic (to_value (to_value_type goals_rty_t ) x) + | Evars _ -> Obj.magic (to_value (to_value_type evars_rty_t ) x) + | Hints _ -> Obj.magic (to_value (to_value_type hints_rty_t ) x) + | Status _ -> Obj.magic (to_value (to_value_type status_rty_t ) x) + | Search _ -> Obj.magic (to_value (to_value_type search_rty_t ) x) + | GetOptions _ -> Obj.magic (to_value (to_value_type get_options_rty_t) x) + | SetOptions _ -> Obj.magic (to_value (to_value_type set_options_rty_t) x) + | MkCases _ -> Obj.magic (to_value (to_value_type mkcases_rty_t ) x) + | Quit _ -> Obj.magic (to_value (to_value_type quit_rty_t ) x) + | About _ -> Obj.magic (to_value (to_value_type about_rty_t ) x) + | Init _ -> Obj.magic (to_value (to_value_type init_rty_t ) x) + | Interp _ -> Obj.magic (to_value (to_value_type interp_rty_t ) x) + | StopWorker _ -> Obj.magic (to_value (to_value_type stop_worker_rty_t) x) + | PrintAst _ -> Obj.magic (to_value (to_value_type print_ast_rty_t ) x) + | Annotate _ -> Obj.magic (to_value (to_value_type annotate_rty_t ) x) + +let of_call (q : 'a call) : xml = + 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) + | 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" -> Add (mkCallArg add_sty_t a) + | "Edit_at" -> Edit_at (mkCallArg edit_at_sty_t a) + | "Query" -> Query (mkCallArg query_sty_t a) + | "Goal" -> Goal (mkCallArg goals_sty_t a) + | "Evars" -> Evars (mkCallArg evars_sty_t a) + | "Hints" -> Hints (mkCallArg hints_sty_t a) + | "Status" -> Status (mkCallArg status_sty_t a) + | "Search" -> Search (mkCallArg search_sty_t a) + | "GetOptions" -> GetOptions (mkCallArg get_options_sty_t a) + | "SetOptions" -> SetOptions (mkCallArg set_options_sty_t a) + | "MkCases" -> MkCases (mkCallArg mkcases_sty_t a) + | "Quit" -> Quit (mkCallArg quit_sty_t a) + | "About" -> About (mkCallArg about_sty_t a) + | "Init" -> Init (mkCallArg init_sty_t a) + | "Interp" -> Interp (mkCallArg interp_sty_t a) + | "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a) + | "PrintAst" -> PrintAst (mkCallArg print_ast_sty_t a) + | "Annotate" -> Annotate (mkCallArg annotate_sty_t a) + | _ -> raise Marshal_error) + +(** Debug printing *) + +let pr_value_gen pr = function + | Good v -> "GOOD " ^ pr v + | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]" + | Fail (id,Some(i,j),str) -> + "FAIL "^Stateid.to_string id^ + " ("^string_of_int i^","^string_of_int j^")["^str^"]" +let pr_value v = pr_value_gen (fun _ -> "FIXME") v +let pr_full_value call value = match call with + | Add _ -> pr_value_gen (print add_rty_t ) (Obj.magic value) + | Edit_at _ -> pr_value_gen (print edit_at_rty_t ) (Obj.magic value) + | Query _ -> pr_value_gen (print query_rty_t ) (Obj.magic value) + | Goal _ -> pr_value_gen (print goals_rty_t ) (Obj.magic value) + | Evars _ -> pr_value_gen (print evars_rty_t ) (Obj.magic value) + | Hints _ -> pr_value_gen (print hints_rty_t ) (Obj.magic value) + | Status _ -> pr_value_gen (print status_rty_t ) (Obj.magic value) + | Search _ -> pr_value_gen (print search_rty_t ) (Obj.magic value) + | GetOptions _ -> pr_value_gen (print get_options_rty_t) (Obj.magic value) + | SetOptions _ -> pr_value_gen (print set_options_rty_t) (Obj.magic value) + | MkCases _ -> pr_value_gen (print mkcases_rty_t ) (Obj.magic value) + | Quit _ -> pr_value_gen (print quit_rty_t ) (Obj.magic value) + | About _ -> pr_value_gen (print about_rty_t ) (Obj.magic value) + | Init _ -> pr_value_gen (print init_rty_t ) (Obj.magic value) + | Interp _ -> pr_value_gen (print interp_rty_t ) (Obj.magic value) + | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) (Obj.magic value) + | PrintAst _ -> pr_value_gen (print print_ast_rty_t ) (Obj.magic value) + | Annotate _ -> pr_value_gen (print annotate_rty_t ) (Obj.magic value) +let pr_call 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 + | 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),"error message")))); + document_type_encoding to_string_fmt + +(* vim: set foldmethod=marker: *) |