package coqide-server
The Rocq Prover, XML protocol server
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/src/coqide-server.protocol/xmlprotocol.ml.html
Source file xmlprotocol.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154
(************************************************************************) (* * The Rocq Prover / The Rocq 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. *) let protocol_version = "20240517" (** See xml-protocol.md for a description of the protocol. *) (** UPDATE xml-protocol.md WHEN YOU UPDATE THE PROTOCOL *) type msg_format = Richpp of { width : int; depth : int } | Ppcmds let msg_format = ref (Richpp { width = 72; depth = max_int }) (** * Interface of calls to Rocq by RocqIDE *) 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" -> empty args; Include_Blacklist | x -> raise (Marshal_error("search",PCData x))) let of_rocq_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_rocq_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 -> 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" -> 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)) | 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" -> 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 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 { width; depth } -> of_richpp (Richpp.richpp_of_pp ~width ~depth pp) | Ppcmds -> of_pp pp let of_dbcontinue_opt opt = let code = match opt with | StepIn -> 0 | StepOver -> 1 | StepOut -> 2 | Continue -> 3 | Interrupt -> 4 in of_int code let to_dbcontinue_opt opt = match to_int opt with | 0 -> StepIn | 1 -> StepOver | 2 -> StepOut | 3 -> Continue | 4 -> Interrupt | _ -> failwith "to_dbcontinue_opt" let of_value f = function | Good x -> Element ("value", ["val", "good"], [f x]) | Fail (id,loc, msg) -> let id = of_stateid id in Element ("value", ["val", "fail"], [id; of_option of_loc loc; 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 (id, loc, msg) = match l with [id; loc; msg] -> (id, loc, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in let id = to_stateid id in let loc = to_option to_loc loc 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 let name = of_option of_string g.goal_name in Element ("goal", [], [id; hyp; ccl; name]) let to_goal = function | Element ("goal", [], [id; hyp; ccl; name]) -> let hyp = to_list to_pp hyp in let ccl = to_pp ccl in let id = to_string id in let name = to_option to_string name in { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; goal_name = name; } | 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_goal_flags f = let mode = of_string f.gf_mode in let fg = of_bool f.gf_fg in let bg = of_bool f.gf_bg in let shelved = of_bool f.gf_shelved in let given_up = of_bool f.gf_given_up in Element ("goal_flags", [], [mode; fg; bg; shelved; given_up]) let to_goal_flags = function | Element ("goal_flags", [], [mode; fg; bg; shelved; given_up]) -> { gf_mode = to_string mode; gf_fg = to_bool fg; gf_bg = to_bool bg; gf_shelved = to_bool shelved; gf_given_up = to_bool given_up } | x -> raise (Marshal_error("goal_flags", x)) let of_rocq_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_rocq_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 goal_flags_t : goal_flags 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 rocq_info_t : coq_info val_t val rocq_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 pp_t : Pp.t val_t val db_cont_opt_t : db_continue_opt 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 | Goal_flags : goal_flags val_t | Evar : evar val_t | State : status val_t | Option_state : option_state val_t | Option_value : option_value val_t | Rocq_info : coq_info val_t | Rocq_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 | Pp : Pp.t val_t | DbContinueOpt : db_continue_opt 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 goal_flags_t = Goal_flags let evar_t = Evar let state_t = State let option_state_t = Option_state let option_value_t = Option_value let rocq_info_t = Rocq_info let rocq_object_t x = Rocq_object x let state_id_t = State_id let route_id_t = Route_id let search_cst_t = Search_cst let pp_t = Pp let db_cont_opt_t = DbContinueOpt 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 | Rocq_info -> of_rocq_info | Goals -> of_goals | Goal_flags -> of_goal_flags | Evar -> of_evar | List t -> (of_list (convert t)) | Option t -> (of_option (convert t)) | Rocq_object t -> (of_rocq_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 | Pp -> of_pp | DbContinueOpt -> of_dbcontinue_opt 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 | Rocq_info -> to_rocq_info | Goals -> to_goals | Goal_flags -> to_goal_flags | Evar -> to_evar | List t -> (to_list (convert t)) | Option t -> (to_option (convert t)) | Rocq_object t -> (to_rocq_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 | Pp -> to_pp | DbContinueOpt -> to_dbcontinue_opt 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_goal_flags (g : goal_flags) = Printf.sprintf "{ fg := %s; bg := %s; shelved := %s; given_up := %s }" (pr_bool g.gf_fg) (pr_bool g.gf_bg) (pr_bool g.gf_shelved) (pr_bool g.gf_given_up) 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_rocq_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_rocq_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_db_continue_opt = function | StepIn -> "StepIn" | StepOver -> "StepOver" | StepOut -> "StepOut" | Continue -> "Continue" | Interrupt -> "Interrupt" 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 pr_pp = Pp.string_of_ppcmds 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 | Rocq_info -> pr_rocq_info | Goals -> pr_goal | Goal_flags -> pr_goal_flags | Evar -> pr_evar | List t -> (pr_list (print t)) | Option t -> (pr_option (print t)) | Rocq_object t -> pr_rocq_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 | Pp -> pr_pp | DbContinueOpt -> pr_db_continue_opt (* 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" | Rocq_info -> assert(true : coq_info exists); "Interface.coq_info" | Goals -> assert(true : goals exists); "Interface.goals" | Goal_flags -> assert(true : goal_flags exists); "Interface.goal_flags" | 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) | Rocq_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" | Pp -> assert(true : Pp.t exists); "Pp.t" | DbContinueOpt -> assert(true : db_continue_opt exists); "Interface.dbcontinue_opt" 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))); 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) (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 (pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t)) int_t) (pair_t int_t int_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 proof_diff_sty_t : proof_diff_sty val_t = pair_t string_t state_id_t let db_cmd_sty_t : db_cmd_sty val_t = string_t let db_upd_bpts_sty_t : db_upd_bpts_sty val_t = list_t (pair_t (pair_t string_t int_t) bool_t) let db_continue_sty_t : db_continue_sty val_t = db_cont_opt_t let db_stack_sty_t : db_stack_sty val_t = unit_t let db_vars_sty_t : db_vars_sty val_t = int_t let db_configd_sty_t : db_configd_sty val_t = unit_t let subgoals_sty_t : subgoals_sty val_t = goal_flags_t let add_rty_t : add_rty val_t = pair_t state_id_t (union_t unit_t state_id_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 (rocq_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 = rocq_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 proof_diff_rty_t : proof_diff_rty val_t = pp_t let db_cmd_rty_t : db_cmd_rty val_t = unit_t let db_upd_bpts_rty_t : db_upd_bpts_rty val_t = unit_t let db_continue_rty_t : db_continue_rty val_t = unit_t let db_stack_rty_t : db_stack_rty val_t = list_t (pair_t string_t (option_t (pair_t string_t (list_t int_t)))) let db_vars_rty_t : db_vars_rty val_t = list_t (pair_t string_t pp_t) let db_configd_rty_t : db_configd_rty val_t = unit_t let subgoals_rty_t : subgoals_rty val_t = option_t goals_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; "PDiff", ($)proof_diff_sty_t, ($)proof_diff_rty_t; "Db_cmd", ($)db_cmd_sty_t, ($)db_cmd_rty_t; "Db_upd_bpts",($)db_upd_bpts_sty_t, ($)db_upd_bpts_rty_t; "Db_continue",($)db_continue_sty_t, ($)db_continue_rty_t; "Db_stack", ($)db_stack_sty_t, ($)db_stack_rty_t; "Db_vars", ($)db_vars_sty_t, ($)db_vars_rty_t; "Db_configd", ($)db_configd_sty_t, ($)db_configd_rty_t; "Subgoals", ($)subgoals_sty_t, ($)subgoals_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 | PDiff : proof_diff_sty -> proof_diff_rty call | Db_cmd : db_cmd_sty -> db_cmd_rty call | Db_upd_bpts: db_upd_bpts_sty -> db_upd_bpts_rty call | Db_continue: db_continue_sty -> db_continue_rty call | Db_stack : db_stack_sty -> db_stack_rty call | Db_vars : db_vars_sty -> db_vars_rty call | Db_configd : db_configd_sty -> db_configd_rty call | Subgoals : subgoals_sty -> subgoals_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 | 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 | PDiff _ -> 19 | Db_cmd _ -> 20 | Db_upd_bpts _-> 21 | Db_continue _-> 22 | Db_stack _ -> 23 | Db_vars _ -> 24 | Db_configd _ -> 25 | Subgoals _ -> 26 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 proof_diff x : proof_diff_rty call = PDiff x let db_cmd x : db_cmd_rty call = Db_cmd x let db_upd_bpts x : db_upd_bpts_rty call = Db_upd_bpts x let db_continue x : db_continue_rty call = Db_continue x let db_stack x : db_stack_rty call = Db_stack x let db_vars x : db_vars_rty call = Db_vars x let db_configd x : db_configd_rty call = Db_configd x let subgoals x : subgoals_rty call = Subgoals x let abstract_eval_call : type a. _ -> a call -> bool * a value = fun handler c -> let send = ref true in let mkGood : type a. a -> bool * a value = fun x -> !send, (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) | PDiff x -> mkGood (handler.proof_diff x) | Db_cmd x -> mkGood (handler.db_cmd x) | Db_upd_bpts x-> mkGood (handler.db_upd_bpts x) | Db_continue x-> mkGood (handler.db_continue x) | Db_stack x -> send := false; mkGood (handler.db_stack x) | Db_vars x -> send := false; mkGood (handler.db_vars x) | Db_configd x -> mkGood (handler.db_configd x) | Subgoals x -> mkGood (handler.subgoals x) with any -> let any = Exninfo.capture any in true, 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 ) | PDiff _ -> of_value (of_value_type proof_diff_rty_t ) | Db_cmd _ -> of_value (of_value_type db_cmd_rty_t ) | Db_upd_bpts _-> of_value (of_value_type db_upd_bpts_rty_t) | Db_continue _-> of_value (of_value_type db_continue_rty_t) | Db_stack _ -> of_value (of_value_type db_stack_rty_t ) | Db_vars _ -> of_value (of_value_type db_vars_rty_t ) | Db_configd _ -> of_value (of_value_type db_configd_rty_t ) | Subgoals _ -> of_value (of_value_type subgoals_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 ) | PDiff _ -> to_value (to_value_type proof_diff_rty_t ) | Db_cmd _ -> to_value (to_value_type db_cmd_rty_t ) | Db_upd_bpts _-> to_value (to_value_type db_upd_bpts_rty_t) | Db_continue _-> to_value (to_value_type db_continue_rty_t) | Db_stack _ -> to_value (to_value_type db_stack_rty_t ) | Db_vars _ -> to_value (to_value_type db_vars_rty_t ) | Db_configd _ -> to_value (to_value_type db_configd_rty_t ) | Subgoals _ -> to_value (to_value_type subgoals_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) | PDiff x -> mkCall (of_value_type proof_diff_sty_t x) | Db_cmd x -> mkCall (of_value_type db_cmd_sty_t x) | Db_upd_bpts x-> mkCall (of_value_type db_upd_bpts_sty_t x) | Db_continue x-> mkCall (of_value_type db_continue_sty_t x) | Db_stack x -> mkCall (of_value_type db_stack_sty_t x) | Db_vars x -> mkCall (of_value_type db_vars_sty_t x) | Db_configd x -> mkCall (of_value_type db_configd_sty_t x) | Subgoals x -> mkCall (of_value_type subgoals_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)) | "PDiff" -> Unknown (PDiff (mkCallArg proof_diff_sty_t a)) | "Db_cmd" -> Unknown (Db_cmd (mkCallArg db_cmd_sty_t a)) | "Db_upd_bpts"-> Unknown (Db_upd_bpts(mkCallArg db_upd_bpts_sty_t a)) | "Db_continue"-> Unknown (Db_continue(mkCallArg db_continue_sty_t a)) | "Db_stack" -> Unknown (Db_stack (mkCallArg db_stack_sty_t a)) | "Db_vars" -> Unknown (Db_vars (mkCallArg db_vars_sty_t a)) | "Db_configd" -> Unknown (Db_configd (mkCallArg db_configd_sty_t a)) | "Subgoals" -> Unknown (Subgoals (mkCallArg subgoals_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 loc,str) -> Printf.sprintf "FAIL %s (%d, %d)[%s]" (Stateid.to_string id) loc.bp loc.ep (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 | PDiff _ -> pr_value_gen (print proof_diff_rty_t ) value | Db_cmd _ -> pr_value_gen (print db_cmd_rty_t ) value | Db_upd_bpts _-> pr_value_gen (print db_upd_bpts_rty_t) value | Db_continue _-> pr_value_gen (print db_continue_rty_t) value | Db_stack _ -> pr_value_gen (print db_stack_rty_t ) value | Db_vars _ -> pr_value_gen (print db_vars_rty_t ) value | Db_configd _ -> pr_value_gen (print db_configd_rty_t ) value | Subgoals _ -> pr_value_gen (print subgoals_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 | PDiff x -> return proof_diff_sty_t x | Db_cmd x -> return db_cmd_sty_t x | Db_upd_bpts x-> return db_upd_bpts_sty_t x | Db_continue x-> return db_continue_sty_t x | Db_stack x -> return db_stack_sty_t x | Db_vars x -> return db_vars_sty_t x | Db_configd x -> return db_configd_sty_t x | Subgoals x -> return subgoals_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\n" (to_string_fmt (of_value (fun _ -> PCData "b") (Fail (Stateid.initial, Some (Loc.{fname=ToplevelInput; line_nb=4; bol_pos=0; line_nb_last=6; bol_pos_last=10; bp=15; ep=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" -> 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 = 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 of_ltac_debug_answer ~tag msg = let wrap s = Element ("ltac_debug", [], s) in wrap [PCData tag; of_pp msg] let to_ltac_debug_answer xml = match xml with | Element ("ltac_debug", [], [PCData tag; pp]) -> let msg = to_pp pp in tag, msg | x -> raise (Marshal_error("ltac_debug_answer",x)) type msg_type = Feedback | LtacDebugInfo | Other let msg_kind = function | Element ("feedback", _, _) -> Feedback | Element ("ltac_debug", _, _) -> LtacDebugInfo | _ -> Other let of_vars vars = of_value (of_list (of_pair of_string of_pp)) (Good vars) let of_stack frames = of_value (of_list (of_pair of_string (of_option (of_pair of_string (of_list of_int))))) (Good frames) (* vim: set foldmethod=marker: *)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>