Source file `jAgent.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
(* Serialization for agent types *)

(* Implement State.t and Env.t serialization methods *)
module State = Obj_map.Make (Petanque.Agent.State)

module Inspect = struct
  type t = [%import: Petanque.Agent.State.Inspect.t] [@@deriving yojson]
end

(* The typical protocol dance *)

(* What a mess result stuff is, we need this in case result is installed, as
   then the types below will be referenced as plain result ... *)
module Stdlib = struct
  module Result = struct
    include Stdlib.Result

    type ('a, 'e) t = [%import: ('a, 'e) Stdlib.Result.t] [@@deriving yojson]
  end
end

module Result = Stdlib.Result

(* ppx_import < 1.10 hack, for some reason it gets confused with the aliases. *)
module Result_ = Stdlib.Result

module Error = struct
  type t = [%import: Petanque.Agent.Error.t] [@@deriving yojson]
end

module Run_opts = struct
  type t = [%import: Petanque.Agent.Run_opts.t] [@@deriving yojson]
end

module Run_result = struct
  type 'a t = [%import: 'a Petanque.Agent.Run_result.t] [@@deriving yojson]
end

module R = struct
  type 'a t =
    [%import:
      ('a Petanque.Agent.R.t
      [@with
        Stdlib.Result.t := Result_.t;
        Result.t := Result_.t])]
  [@@deriving yojson]
end

module Goals = struct
  type t = string Lsp.JCoq.Goals.reified_pp option [@@deriving yojson]
end

module Lang = struct
  module Range = struct
    type t = Lsp.JLang.Range.t [@@deriving yojson]
  end

  module With_range = struct
    type 'a t = [%import: ('a Lang.With_range.t[@with Lang.Range.t := Range.t])]
    [@@deriving yojson]
  end

  module Ast = struct
    module Name = struct
      type t = [%import: Lang.Ast.Name.t] [@@deriving yojson]
    end

    module Info = struct
      type t =
        [%import:
          (Lang.Ast.Info.t
          [@with
            Lang.Range.t := Range.t;
            Lang.With_range.t := With_range.t])]
      [@@deriving yojson]
    end
  end
end

module Premise = struct
  module Info = struct
    type t = [%import: Petanque.Agent.Premise.Info.t] [@@deriving yojson]
  end

  type t =
    [%import:
      (Petanque.Agent.Premise.t
      [@with
        Stdlib.Result.t := Result_.t;
        Result.t := Result_.t])]
  [@@deriving yojson]
end