diff options
Diffstat (limited to 'ide/coqide/protocol/xmlprotocol.ml')
| -rw-r--r-- | ide/coqide/protocol/xmlprotocol.ml | 49 |
1 files changed, 37 insertions, 12 deletions
diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml index 6cb0cec008..6a33ff8abc 100644 --- a/ide/coqide/protocol/xmlprotocol.ml +++ b/ide/coqide/protocol/xmlprotocol.ml @@ -12,7 +12,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20170413" +let protocol_version = "20200911" type msg_format = Richpp of int | Ppcmds let msg_format = ref (Richpp 72) @@ -43,7 +43,7 @@ let to_search_cst = do_match "search_cst" (fun s args -> match s with | "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 + | "include_blacklist" -> empty args; Include_Blacklist | x -> raise (Marshal_error("search",PCData x))) let of_coq_object f ans = @@ -103,14 +103,14 @@ let to_routeid = function 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_hbox -> constructor "ppbox" "hbox" [] | 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)) + | "hbox" -> empty args; Pp_hbox | "vbox" -> Pp_vbox (to_int (singleton args)) | "hvbox" -> Pp_hvbox (to_int (singleton args)) | "hovbox" -> Pp_hovbox (to_int (singleton args)) @@ -132,7 +132,7 @@ let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with let rec to_pp xpp = let open Pp in Pp.unrepr @@ do_match "ppdoc" (fun s args -> match s with - | "empty" -> Ppcmd_empty + | "empty" -> empty args; 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 @@ -278,6 +278,7 @@ module ReifType : sig 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 pp_t : Pp.t val_t val of_value_type : 'a val_t -> 'a -> xml val to_value_type : 'a val_t -> xml -> 'a @@ -314,6 +315,7 @@ end = struct | State_id : state_id val_t | Route_id : route_id val_t | Search_cst : search_constraint val_t + | Pp : Pp.t val_t type value_type = Value_type : 'a val_t -> value_type @@ -340,6 +342,7 @@ end = struct let state_id_t = State_id let route_id_t = Route_id let search_cst_t = Search_cst + let pp_t = Pp let of_value_type (ty : 'a val_t) : 'a -> xml = let rec convert : type a. a val_t -> a -> xml = function @@ -362,6 +365,7 @@ end = struct | State_id -> of_stateid | Route_id -> of_routeid | Search_cst -> of_search_cst + | Pp -> of_pp in convert ty @@ -386,6 +390,7 @@ end = struct | State_id -> to_stateid | Route_id -> to_routeid | Search_cst -> to_search_cst + | Pp -> to_pp in convert ty @@ -443,6 +448,8 @@ end = struct | In_Module s -> "In_Module " ^ String.concat "." s | Include_Blacklist -> "Include_Blacklist" + let pr_pp = Pp.string_of_ppcmds + let rec print : type a. a val_t -> a -> string = function | Unit -> pr_unit | Bool -> pr_bool @@ -463,6 +470,7 @@ end = struct | Union (t1,t2) -> (pr_union (print t1) (print t2)) | State_id -> pr_state_id | Route_id -> pr_int + | Pp -> pr_pp (* This is to break if a rename/refactoring makes the strings below outdated *) type 'a exists = bool @@ -489,6 +497,7 @@ end = struct 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" + | Pp -> assert(true : Pp.t exists); "Pp.t" let print_type = function Value_type ty -> print_val_t ty @@ -507,6 +516,8 @@ end = struct (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))); + Printf.printf "%s:\n\n%s\n\n" (print_val_t Pp) + (pr_xml (of_pp Pp.(hv 3 (str "foo" ++ spc () ++ str "bar") ))); 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) @@ -538,6 +549,7 @@ 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 proof_diff_sty_t : proof_diff_sty val_t = pair_t string_t state_id_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) @@ -563,6 +575,7 @@ let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string 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 proof_diff_rty_t : proof_diff_rty val_t = pp_t let ($) x = erase x let calls = [| @@ -585,6 +598,7 @@ let calls = [| "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; + "PDiff", ($)proof_diff_sty_t, ($)proof_diff_rty_t; |] type 'a call = @@ -609,7 +623,9 @@ type 'a call = | Interp : interp_sty -> interp_rty call | PrintAst : print_ast_sty -> print_ast_rty call | Annotate : annotate_sty -> annotate_rty call + | PDiff : proof_diff_sty -> proof_diff_rty call +(* the order of the entries must match the order in "calls" above *) let id_of_call : type a. a call -> int = function | Add _ -> 0 | Edit_at _ -> 1 @@ -630,6 +646,7 @@ let id_of_call : type a. a call -> int = function | StopWorker _ -> 16 | PrintAst _ -> 17 | Annotate _ -> 18 + | PDiff _ -> 19 let str_of_call c = pi1 calls.(id_of_call c) @@ -652,8 +669,9 @@ 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 print_ast x : print_ast_rty call = PrintAst x +let annotate x : annotate_rty call = Annotate x +let proof_diff x : proof_diff_rty call = PDiff 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 @@ -678,6 +696,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | StopWorker x -> mkGood (handler.stop_worker x) | PrintAst x -> mkGood (handler.print_ast x) | Annotate x -> mkGood (handler.annotate x) + | PDiff x -> mkGood (handler.proof_diff x) with any -> let any = Exninfo.capture any in Fail (handler.handle_exn any) @@ -703,6 +722,7 @@ let of_answer : type a. a call -> a value -> xml = function | 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 ) + | PDiff _ -> of_value (of_value_type proof_diff_rty_t ) let of_answer msg_fmt = msg_format := msg_fmt; of_answer @@ -727,6 +747,7 @@ let to_answer : type a. a call -> xml -> a value = function | 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 ) + | PDiff _ -> to_value (to_value_type proof_diff_rty_t ) let of_call : type a. a call -> xml = fun q -> let mkCall x = constructor "call" (str_of_call q) [x] in @@ -750,6 +771,7 @@ let of_call : type a. a call -> xml = fun q -> | 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) + | PDiff x -> mkCall (of_value_type proof_diff_sty_t x) let to_call : xml -> unknown_call = do_match "call" (fun s a -> @@ -774,6 +796,7 @@ let to_call : xml -> unknown_call = | "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)) + | "PDiff" -> Unknown (PDiff (mkCallArg proof_diff_sty_t a)) | x -> raise (Marshal_error("call",PCData x))) (** Debug printing *) @@ -805,6 +828,7 @@ let pr_full_value : type a. a call -> a value -> string = fun call value -> matc | 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 + | PDiff _ -> pr_value_gen (print proof_diff_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 @@ -827,6 +851,7 @@ let pr_call : type a. a call -> string = fun call -> | StopWorker x -> return stop_worker_sty_t x | PrintAst x -> return print_ast_sty_t x | Annotate x -> return annotate_sty_t x + | PDiff x -> return proof_diff_sty_t x let document to_string_fmt = Printf.printf "=== Available calls ===\n\n"; @@ -858,11 +883,11 @@ let of_message_level = function | 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 + | "debug" -> empty args; Debug + | "info" -> empty args; Info + | "notice" -> empty args; Notice + | "warning" -> empty args; Warning + | "error" -> empty args; Error | x -> raise Serialize.(Marshal_error("error level",PCData x))) let of_message lvl loc msg = |