package coqide-server
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
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/serialize.ml.html
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))
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>