diff options
| -rw-r--r-- | lib/serialize.ml | 211 | ||||
| -rw-r--r-- | lib/serialize.mli | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
4 files changed, 157 insertions, 59 deletions
diff --git a/lib/serialize.ml b/lib/serialize.ml index 37856b527..2b46df60b 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -401,6 +401,13 @@ module ReifType : sig (* {{{ *) val print : 'a val_t -> 'a -> string + type value_type + val erase : 'a val_t -> value_type + val print_type : value_type -> string + val same_type : 'a val_t -> value_type -> bool + + val document_type_encoding : (xml -> string) -> unit + end = struct type value_type = @@ -417,6 +424,9 @@ end = struct | Search_cst type 'a val_t = value_type + + let erase (x : 'a val_t) : value_type = x + let same_type (x : 'a val_t) (y : value_type) = Pervasives.compare (erase x) y = 0 let unit_t = Unit let string_t = String @@ -553,9 +563,116 @@ end = struct | 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" + | 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 (of_state_id 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 inloadpath_sty_t : inloadpath_sty val_t = string_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 = unit_t +let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_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 inloadpath_rty_t : inloadpath_rty val_t = bool_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 = union_t string_t string_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; + "InLoadPath", ($)inloadpath_sty_t, ($)inloadpath_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; +|] + type 'a call = | Add of add_sty | Edit_at of edit_at_sty @@ -575,23 +692,25 @@ type 'a call = (* retrocompatibility *) | Interp of interp_sty -let str_of_call = function - | Add _ -> "Add" - | Edit_at _ -> "Edit_at" - | Query _ -> "Query" - | Goal _ -> "Goal" - | Evars _ -> "Evars" - | Hints _ -> "Hints" - | Status _ -> "Status" - | Search _ -> "Search" - | GetOptions _ -> "GetOptions" - | SetOptions _ -> "SetOptions" - | InLoadPath _ -> "InLoadPath" - | MkCases _ -> "MkCases" - | Quit _ -> "Quit" - | About _ -> "About" - | Init _ -> "Init" - | Interp _ -> "Interp" +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 + | InLoadPath _ -> 10 + | MkCases _ -> 11 + | Quit _ -> 12 + | About _ -> 13 + | Init _ -> 14 + | Interp _ -> 15 + +let str_of_call c = pi1 calls.(id_of_call c) type unknown @@ -635,48 +754,6 @@ let abstract_eval_call handler (c : 'a call) : 'a value = with any -> Fail (handler.handle_exn any) -(** 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 inloadpath_sty_t : inloadpath_sty val_t = string_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 = unit_t -let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_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 inloadpath_rty_t : inloadpath_rty val_t = bool_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 = union_t string_t string_t - (** 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) @@ -809,4 +886,20 @@ let pr_call call = match call with (* }}} *) +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: *) diff --git a/lib/serialize.mli b/lib/serialize.mli index e74946208..4e5cb2d15 100644 --- a/lib/serialize.mli +++ b/lib/serialize.mli @@ -56,6 +56,9 @@ val is_feedback : xml -> bool val of_answer : '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 diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b97042ede..f3bcee128 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -298,6 +298,7 @@ let parse_args arglist = |"-filteropts" -> filter_opts := true |"-force-load-proofs" -> Flags.load_proofs := Flags.Force |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () + |"--help-XML-protocol" -> Serialize.document Xml_printer.to_string_fmt; exit 0 |"-ideslave" -> Flags.ide_slave := true |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet |"-just-parsing" -> Vernac.just_parsing := true diff --git a/toplevel/usage.ml b/toplevel/usage.ml index e9e576962..b8e94c9cc 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -74,6 +74,7 @@ let print_usage_channel co command = \n some tactics\ \n -time display the time taken by each command\ \n -h, --help print this list of options\ +\n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\ \n" (* print the usage on standard error *) |