package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.2.3.9.0.tbz
sha256=8776582dddfe768623870cf540ff6ba1e96a44a36e85db18ab93d238d640f92a
sha512=2837889bf99bfe715bd0e752782211a76a14aac71ed37a4fb784f4f0abe338352c9c6d8caa37daf79c036997add1cb306c523f793625b38709f3b5e245380223
doc/src/coq-lsp.serlib/ser_stdarg.ml.html
Source file ser_stdarg.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 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(************************************************************************) (* * The Coq Proof Assistant / The Coq 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) *) (************************************************************************) (************************************************************************) (* SerAPI: Coq interaction protocol with bidirectional serialization *) (************************************************************************) (* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) (* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) (* Written by: Emilio J. Gallego Arias and others *) (************************************************************************) open Sexplib.Conv module Names = Ser_names module Genredexpr = Ser_genredexpr let ser_wit_unit = Ser_genarg.mk_uniform sexp_of_unit unit_of_sexp Ppx_hash_lib.Std.Hash.Builtin.hash_fold_unit Ppx_compare_lib.Builtin.compare_unit let ser_wit_bool = Ser_genarg.mk_uniform sexp_of_bool bool_of_sexp Ppx_hash_lib.Std.Hash.Builtin.hash_fold_bool Ppx_compare_lib.Builtin.compare_bool let ser_wit_int = Ser_genarg.mk_uniform sexp_of_int int_of_sexp Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int Ppx_compare_lib.Builtin.compare_int let ser_wit_string = Ser_genarg.mk_uniform sexp_of_string string_of_sexp Ppx_hash_lib.Std.Hash.Builtin.hash_fold_string Ppx_compare_lib.Builtin.compare_string let ser_wit_pre_ident = Ser_genarg.mk_uniform sexp_of_string string_of_sexp Ppx_hash_lib.Std.Hash.Builtin.hash_fold_string Ppx_compare_lib.Builtin.compare_string let ser_wit_hyp : (Ser_names.lident, Ser_names.lident, Ser_names.Id.t) Ser_genarg.gen_ser = Ser_genarg. { raw_ser = Ser_names.sexp_of_lident ; glb_ser = Ser_names.sexp_of_lident ; top_ser = Ser_names.Id.sexp_of_t ; raw_des = Ser_names.lident_of_sexp ; glb_des = Ser_names.lident_of_sexp ; top_des = Ser_names.Id.t_of_sexp ; raw_hash = Ser_names.hash_fold_lident ; glb_hash = Ser_names.hash_fold_lident ; top_hash = Ser_names.Id.hash_fold_t ; raw_compare = Ser_names.compare_lident ; glb_compare = Ser_names.compare_lident ; top_compare = Ser_names.Id.compare } (* Same *) let ser_wit_identref = ser_wit_hyp let ser_wit_nat_or_var = Ser_genarg. { raw_ser = Ser_locus.sexp_of_or_var sexp_of_int ; glb_ser = Ser_locus.sexp_of_or_var sexp_of_int ; top_ser = sexp_of_int ; raw_des = Ser_locus.or_var_of_sexp int_of_sexp ; glb_des = Ser_locus.or_var_of_sexp int_of_sexp ; top_des = int_of_sexp ; raw_hash = Ser_locus.hash_fold_or_var Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int ; glb_hash = Ser_locus.hash_fold_or_var Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int ; top_hash = Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int ; raw_compare = Ser_locus.compare_or_var Ppx_compare_lib.Builtin.compare_int ; glb_compare = Ser_locus.compare_or_var Ppx_compare_lib.Builtin.compare_int ; top_compare = Ppx_compare_lib.Builtin.compare_int } let ser_wit_int_or_var = Ser_genarg. { raw_ser = Ser_locus.sexp_of_or_var sexp_of_int ; glb_ser = Ser_locus.sexp_of_or_var sexp_of_int ; top_ser = sexp_of_int ; raw_des = Ser_locus.or_var_of_sexp int_of_sexp ; glb_des = Ser_locus.or_var_of_sexp int_of_sexp ; top_des = int_of_sexp ; raw_hash = Ser_locus.hash_fold_or_var Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int ; glb_hash = Ser_locus.hash_fold_or_var Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int ; top_hash = Ppx_hash_lib.Std.Hash.Builtin.hash_fold_int ; raw_compare = Ser_locus.compare_or_var Ppx_compare_lib.Builtin.compare_int ; glb_compare = Ser_locus.compare_or_var Ppx_compare_lib.Builtin.compare_int ; top_compare = Ppx_compare_lib.Builtin.compare_int } let ser_wit_ident = Ser_genarg.mk_uniform Ser_names.Id.sexp_of_t Ser_names.Id.t_of_sexp Ser_names.Id.hash_fold_t Ser_names.Id.compare let ser_wit_ref = Ser_genarg.{ raw_ser = Ser_libnames.sexp_of_qualid ; glb_ser = Ser_locus.sexp_of_or_var Ser_loc.(sexp_of_located Ser_names.GlobRef.sexp_of_t) ; top_ser = Ser_names.GlobRef.sexp_of_t ; raw_des = Ser_libnames.qualid_of_sexp ; glb_des = Ser_locus.or_var_of_sexp Ser_loc.(located_of_sexp Ser_names.GlobRef.t_of_sexp) ; top_des = Ser_names.GlobRef.t_of_sexp ; raw_hash = Ser_libnames.hash_fold_qualid ; glb_hash = Ser_locus.hash_fold_or_var Ser_loc.(hash_fold_located Ser_names.GlobRef.hash_fold_t) ; top_hash = Ser_names.GlobRef.hash_fold_t ; raw_compare = Ser_libnames.compare_qualid ; glb_compare = Ser_locus.compare_or_var Ser_loc.(compare_located Ser_names.GlobRef.compare) ; top_compare = Ser_names.GlobRef.compare } let ser_wit_sort_family = Ser_genarg.{ raw_ser = Ser_sorts.sexp_of_family ; glb_ser = sexp_of_unit ; top_ser = sexp_of_unit ; raw_des = Ser_sorts.family_of_sexp ; glb_des = unit_of_sexp ; top_des = unit_of_sexp ; raw_hash = Ser_sorts.hash_fold_family ; glb_hash = Ppx_hash_lib.Std.Hash.Builtin.hash_fold_unit ; top_hash = Ppx_hash_lib.Std.Hash.Builtin.hash_fold_unit ; raw_compare = Ser_sorts.compare_family ; glb_compare = Ppx_compare_lib.Builtin.compare_unit ; top_compare = Ppx_compare_lib.Builtin.compare_unit } (* let ser_ref *) let ser_wit_constr = Ser_genarg.{ raw_ser = Ser_constrexpr.sexp_of_constr_expr ; glb_ser = Ser_genintern.sexp_of_glob_constr_and_expr ; top_ser = Ser_eConstr.sexp_of_t ; raw_des = Ser_constrexpr.constr_expr_of_sexp ; glb_des = Ser_genintern.glob_constr_and_expr_of_sexp ; top_des = Ser_eConstr.t_of_sexp ; raw_hash = Ser_constrexpr.hash_fold_constr_expr ; glb_hash = Ser_genintern.hash_fold_glob_constr_and_expr ; top_hash = Ser_eConstr.hash_fold_t ; raw_compare = Ser_constrexpr.compare_constr_expr ; glb_compare = Ser_genintern.compare_glob_constr_and_expr ; top_compare = Ser_eConstr.compare } let ser_wit_uconstr = Ser_genarg.{ raw_ser = Ser_constrexpr.sexp_of_constr_expr ; glb_ser = Ser_genintern.sexp_of_glob_constr_and_expr ; top_ser = Ser_ltac_pretype.sexp_of_closed_glob_constr ; raw_des = Ser_constrexpr.constr_expr_of_sexp ; glb_des = Ser_genintern.glob_constr_and_expr_of_sexp ; top_des = Ser_ltac_pretype.closed_glob_constr_of_sexp ; raw_hash = Ser_constrexpr.hash_fold_constr_expr ; glb_hash = Ser_genintern.hash_fold_glob_constr_and_expr ; top_hash = Ser_ltac_pretype.hash_fold_closed_glob_constr ; raw_compare = Ser_constrexpr.compare_constr_expr ; glb_compare = Ser_genintern.compare_glob_constr_and_expr ; top_compare = Ser_ltac_pretype.compare_closed_glob_constr } let ser_wit_clause_dft_concl = Ser_genarg.{ raw_ser = Ser_locus.sexp_of_clause_expr Ser_names.sexp_of_lident ; glb_ser = Ser_locus.sexp_of_clause_expr Ser_names.sexp_of_lident ; top_ser = Ser_locus.sexp_of_clause_expr Ser_names.Id.sexp_of_t ; raw_des = Ser_locus.clause_expr_of_sexp Ser_names.lident_of_sexp ; glb_des = Ser_locus.clause_expr_of_sexp Ser_names.lident_of_sexp ; top_des = Ser_locus.clause_expr_of_sexp Ser_names.Id.t_of_sexp ; raw_hash = Ser_locus.hash_fold_clause_expr Ser_names.hash_fold_lident ; glb_hash = Ser_locus.hash_fold_clause_expr Ser_names.hash_fold_lident ; top_hash = Ser_locus.hash_fold_clause_expr Ser_names.Id.hash_fold_t ; raw_compare = Ser_locus.compare_clause_expr Ser_names.compare_lident ; glb_compare = Ser_locus.compare_clause_expr Ser_names.compare_lident ; top_compare = Ser_locus.compare_clause_expr Ser_names.Id.compare } let register () = Ser_genarg.register_genser Stdarg.wit_bool ser_wit_bool; Ser_genarg.register_genser Stdarg.wit_clause_dft_concl ser_wit_clause_dft_concl; Ser_genarg.register_genser Stdarg.wit_constr ser_wit_constr; Ser_genarg.register_genser Stdarg.wit_ident ser_wit_ident; Ser_genarg.register_genser Stdarg.wit_identref ser_wit_identref; Ser_genarg.register_genser Stdarg.wit_hyp ser_wit_hyp; Ser_genarg.register_genser Stdarg.wit_int ser_wit_int; Ser_genarg.register_genser Stdarg.wit_int_or_var ser_wit_int_or_var; Ser_genarg.register_genser Stdarg.wit_nat_or_var ser_wit_nat_or_var; Ser_genarg.register_genser Stdarg.wit_open_constr ser_wit_constr; Ser_genarg.register_genser Stdarg.wit_pre_ident ser_wit_pre_ident; Ser_genarg.register_genser Stdarg.wit_ref ser_wit_ref; Ser_genarg.register_genser Stdarg.wit_sort_family ser_wit_sort_family; Ser_genarg.register_genser Stdarg.wit_string ser_wit_string; Ser_genarg.register_genser Stdarg.wit_uconstr ser_wit_uconstr; Ser_genarg.register_genser Stdarg.wit_unit ser_wit_unit; () let _ = register ()