aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/xmlprotocol.ml
blob: 5f82a8898b503e18459bc290b8978468f5bc2138 (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
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
(************************************************************************)
(*  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 = "20150913"

(** * 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
  | x -> raise (Marshal_error("search",PCData x)))

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;
  }
| 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_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 }
  | 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 of_richpp x = Element ("richpp", [], [Richpp.repr x])
let to_richpp xml = match xml with
  | Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x
  | x -> raise Serialize.(Marshal_error("richpp",x))

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 = of_stateid id in
  Element ("value", ["val", "fail"] @ loc, [id; of_richpp 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, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in
    let id = to_stateid id in
    let msg = to_richpp 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_richpp g.goal_hyp in
  let ccl = of_richpp 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_richpp hyp in
    let ccl = to_richpp ccl in
    let id = to_string id in
    { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
  | 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_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; }
  | 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 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 _ 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
    | Evar : evar val_t
    | State : status val_t
    | Option_state : option_state val_t
    | Option_value : option_value val_t
    | Coq_info : coq_info val_t
    | Coq_object : 'a val_t -> 'a coq_object val_t
    | State_id : state_id val_t
    | Search_cst : search_constraint 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 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 : 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
      | Coq_info      -> of_coq_info
      | Goals         -> of_goals
      | Evar          -> of_evar
      | List t        -> (of_list (convert t))
      | Option t      -> (of_option (convert t))
      | Coq_object t  -> (of_coq_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
      | Search_cst    -> of_search_cst
    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
      | Coq_info      -> to_coq_info
      | Goals         -> to_goals
      | Evar          -> to_evar
      | List t        -> (to_list (convert t))
      | Option t      -> (to_option (convert t))
      | Coq_object t  -> (to_coq_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
      | Search_cst    -> 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_goal { goal_hyp = hyps; goal_ccl = goal } =
        "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^
            Richpp.raw_print 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_state_id = Stateid.to_string

  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 : 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
  | Coq_info      -> pr_coq_info
  | Goals         -> pr_goal
  | Evar          -> pr_evar
  | List t        -> (pr_list (print t))
  | Option t      -> (pr_option (print t))
  | Coq_object t  -> pr_coq_object
  | Pair (t1,t2)  -> (pr_pair (print t1) (print t2))
  | Union (t1,t2) -> (pr_union (print t1) (print t2))
  | State_id      -> pr_state_id

  (* 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"
  | 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_val_t t)
  | Option t      -> Printf.sprintf "(%s option)" (print_val_t t)
  | Coq_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"

  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)));
    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_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        : 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
  (* retrocompatibility *)
  | Interp     : interp_sty -> interp_rty call
  | PrintAst   : print_ast_sty -> print_ast_rty call
  | Annotate   : annotate_sty -> annotate_rty call

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
  | 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_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 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 : type a. _ -> a call -> a value = fun handler c ->
  let mkGood : type a. a -> a value = fun x -> 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)
    | 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 = CErrors.push any in
    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       )
  | 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   )

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       )
  | 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   )

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)
  | 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"        -> 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))
    | "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))
    | 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^" ["^Richpp.raw_print str^"]"
  | Fail (id,Some(i,j),str) ->
      "FAIL "^Stateid.to_string id^
        " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print 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
  | 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
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
    | 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),Richpp.richpp_of_string "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" -> Debug
  | "info" -> Info
  | "notice" -> Notice
  | "warning" -> Warning
  | "error" -> 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_richpp 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_richpp content)
  | x -> raise (Marshal_error("message",x))

let is_message xml =
  try begin match to_message xml with
    | Message(l,c,m) -> Some (l,c,m)
    | _              -> None
  end with | Marshal_error _ -> None

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_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_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 = function
  | Edit id -> ["object","edit"], of_edit_id id
  | State 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.id in
  let route = string_of_int msg.route in
  Element ("feedback", obj @ ["route",route], [id;content])

let to_feedback xml = match xml with
  | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
      id = Edit(to_edit_id id);
      route = int_of_string route;
      contents = to_feedback_content content }
  | Element ("feedback", ["object","state";"route",route], [id;content]) -> { 
      id = State(to_stateid id);
      route = int_of_string route;
      contents = to_feedback_content content }
  | x -> raise (Marshal_error("feedback",x))

let is_feedback = function
  | Element ("feedback", _, _) -> true
  | _ -> false

(* vim: set foldmethod=marker: *)