aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/xmlprotocol.ml
blob: 88bd2c17fe0d41250576113b4bba16dc1b208f9d (plain)
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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \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]
  | 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))
  | _ -> 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
    | 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; 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: *)