package coqide-server

  1. Overview
  2. Docs

Source file serialize.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
(************************************************************************)
(*         *      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)         *)
(************************************************************************)

open Xml_datatype

exception Marshal_error of string * xml

(** Utility functions *)

let rec get_attr attr = function
  | [] -> raise Not_found
  | (k, v) :: l when CString.equal k attr -> v
  | _ :: l -> get_attr attr l

let massoc x l =
  try get_attr x l
  with Not_found -> raise (Marshal_error("attribute " ^ x,PCData "not there"))

let constructor t c args = Element (t, ["val", c], args)
let do_match t mf = function
  | Element (s, attrs, args) when CString.equal s t ->
      let c = massoc "val" attrs in
      mf c args
  | x -> raise (Marshal_error (t,x))

let singleton = function
  | [x] -> x
  | l -> raise (Marshal_error
      ("singleton",PCData ("list of length " ^ string_of_int (List.length l))))

let empty = function
  | [] -> ()
  | l -> raise (Marshal_error
      ("empty",PCData ("list of length " ^ string_of_int (List.length l))))

let raw_string = function
  | [] -> ""
  | [PCData s] -> s
  | x::_ -> raise (Marshal_error("raw string",x))

(** Base types *)

let of_unit () = Element ("unit", [], [])
let to_unit : xml -> unit = function
  | Element ("unit", [], []) -> ()
  | x -> raise (Marshal_error ("unit",x))

let of_bool (b : bool) : xml =
  if b then constructor "bool" "true" []
  else constructor "bool" "false" []
let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with
  | "true" -> true
  | "false" -> false
  | x -> raise (Marshal_error("bool",PCData x)))

let of_list (f : 'a -> xml) (l : 'a list) =
  Element ("list", [], List.map f l)
let to_list (f : xml -> 'a) : xml -> 'a list = function
  | Element ("list", [], l) -> List.map f l
  | x -> raise (Marshal_error("list",x))

let of_option (f : 'a -> xml) : 'a option -> xml = function
  | None -> Element ("option", ["val", "none"], [])
  | Some x -> Element ("option", ["val", "some"], [f x])
let to_option (f : xml -> 'a) : xml -> 'a option = function
  | Element ("option", ["val", "none"], []) -> None
  | Element ("option", ["val", "some"], [x]) -> Some (f x)
  | x -> raise (Marshal_error("option",x))

let of_string (s : string) : xml = Element ("string", [], [PCData s])
let to_string : xml -> string = function
  | Element ("string", [], l) -> raw_string l
  | x -> raise (Marshal_error("string",x))

let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)])
let to_int : xml -> int = function
  | Element ("int", [], [PCData s]) ->
    (try int_of_string s with Failure _ -> raise(Marshal_error("int",PCData s)))
  | x -> raise (Marshal_error("int",x))

let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml =
  Element ("pair", [], [f (fst x); g (snd x)])
let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function
  | Element ("pair", [], [x; y]) -> (f x, g y)
  | x -> raise (Marshal_error("pair",x))

let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function
  | CSig.Inl x -> Element ("union", ["val","in_l"], [f x])
  | CSig.Inr x -> Element ("union", ["val","in_r"], [g x])
let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function
  | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x)
  | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x)
  | x -> raise (Marshal_error("union",x))

(** More elaborate types *)

let of_edit_id i = Element ("edit_id",["val",string_of_int i],[])
let to_edit_id = function
  | Element ("edit_id",["val",i],[]) ->
      let id = int_of_string i in
      assert (id <= 0 );
      id
  | x -> raise (Marshal_error("edit_id",x))

let of_loc loc =
  let {
    Loc.fname
  ; line_nb
  ; bol_pos
  ; line_nb_last
  ; bol_pos_last
  ; bp
  ; ep
  } = loc in
  let fname = match fname with
  | ToplevelInput -> []
  | InFile { dirpath = None; file } -> [ ("file", file) ]
  | InFile { dirpath = Some dir; file } -> [ ("dirpath", dir); ("file", file) ] in
  Element ("loc",
           fname @
           [ ("line_nb", string_of_int line_nb)
           ; ("bol_pos", string_of_int bol_pos)
           ; ("line_nb_last", string_of_int line_nb_last)
           ; ("bol_pos_last", string_of_int bol_pos_last)
           ; ("start", string_of_int bp)
           ; ("stop", string_of_int ep )
           ],
           [])

let to_loc xml =
  match xml with
  | Element ("loc", l,[]) as x ->
    (try
       let fname =
         let dirpath = try Some (get_attr "dirpath" l) with Not_found -> None in
         let file = try Some (get_attr "file" l) with Not_found -> None in
         match dirpath, file with
         | None, None -> Loc.ToplevelInput
         | dirpath, Some file -> Loc.InFile { dirpath; file }
         | Some _, None -> raise (Marshal_error("loc",x)) in
       let line_nb = massoc "line_nb" l |> int_of_string in
       let bol_pos = massoc "bol_pos" l |> int_of_string in
       let line_nb_last = massoc "line_nb_last" l |> int_of_string in
       let bol_pos_last = massoc "bol_pos_last" l |> int_of_string in
       let bp = massoc "start" l |> int_of_string in
       let ep = massoc "stop" l |> int_of_string in
       { Loc.fname
       ; line_nb
       ; bol_pos
       ; line_nb_last
       ; bol_pos_last
       ; bp
       ; ep }
     with Not_found | Invalid_argument _ ->
       raise (Marshal_error("loc",x)))
  | x -> raise (Marshal_error("loc",x))

let of_xml x = Element ("xml", [], [x])
let to_xml xml = match xml with
| Element ("xml", [], [x]) -> x
| x -> raise (Marshal_error("xml",x))
OCaml

Innovation. Community. Security.