package coq-serapi

You can search for identifiers within the package.

in-package search v0.2.0

Serialization library and protocol for machine interaction with the Coq proof assistant

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

Maintainers

E

e@x80.org

Sources

coq-serapi-8.15.0.0.15.1.tbz

sha256=31d1e4661f5b1b917d7004c749cc05eb73546d3190ac632faddc37348531a0a5

sha512=a9816915f9dc4051e76c5b0e615b27c1bb0a6a5ffd445af94ad2ed1582a0e704a7f49f69b6764fa92dbfa092aa8e41ee3151a1330b394eb0338c796d6460fa20

doc/src/coq-serapi.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
(************************************************************************)
(*  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        *)
(************************************************************************)

(************************************************************************)
(* Coq serialization API/Plugin                                         *)
(* Copyright 2016-2018 MINES ParisTech                                  *)
(************************************************************************)
(* Status: Very Experimental                                            *)
(************************************************************************)

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
let ser_wit_bool   = Ser_genarg.mk_uniform sexp_of_bool bool_of_sexp
let ser_wit_int    = Ser_genarg.mk_uniform sexp_of_int int_of_sexp
let ser_wit_string = Ser_genarg.mk_uniform sexp_of_string string_of_sexp
let ser_wit_pre_ident = Ser_genarg.mk_uniform sexp_of_string string_of_sexp

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
  }

(* 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;
  }

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;
  }

let ser_wit_ident  = Ser_genarg.mk_uniform Ser_names.Id.sexp_of_t Ser_names.Id.t_of_sexp

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;
  }

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;
  }

(* 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;
  }

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;
  }

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;
  }

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