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.14.0.0.14.0.tbz

sha256=1c16d8e37b0970f97313d99b57456013ff5ec94135dffc7a3d6d15c2f23b5dfe

sha512=e2a2b6f7cba9f31aed022058718efe3b5233b6f67a4a8aa79470697c640986053e19508866cf886318f2cc4f26e067583a908fad8c9655aa309ad359000abf1e

doc/src/serlib_funind/ser_g_indfun.ml.html

Source file `ser_g_indfun.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
open Sexplib.Conv
open Serlib

module CAst       = Ser_cAst
module Constrexpr = Ser_constrexpr
module Tactypes   = Ser_tactypes
module Genintern  = Ser_genintern
module EConstr    = Ser_eConstr
module Tacexpr    = Serlib_ltac.Ser_tacexpr

module A1 = struct

type h1 = Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t option
[@@deriving sexp]
type h2 = Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t option
[@@deriving sexp]
type h3 = Tacexpr.intro_pattern option
[@@deriving sexp]

end

let ser_wit_with_names =
  let open A1 in
  Ser_genarg.{
    raw_ser = sexp_of_h1;
    raw_des = h1_of_sexp;

    glb_ser = sexp_of_h2;
    glb_des = h2_of_sexp;

    top_ser = sexp_of_h3;
    top_des = h3_of_sexp;
  }

module A2 = struct
type h1 = Constrexpr.constr_expr Tactypes.with_bindings option
[@@deriving sexp]
type h2 = Genintern.glob_constr_and_expr Tactypes.with_bindings option
[@@deriving sexp]
type h3 = EConstr.t Tactypes.with_bindings Ser_tactypes.delayed_open option
[@@deriving sexp]
end

let ser_wit_fun_ind_using :
  (Constrexpr.constr_expr Tactypes.with_bindings option,
   Genintern.glob_constr_and_expr Tactypes.with_bindings option,
   EConstr.t Tactypes.with_bindings Tactypes.delayed_open option)
    Ser_genarg.gen_ser =
  let open A2 in
  Ser_genarg.{
    raw_ser = sexp_of_h1;
    raw_des = h1_of_sexp;

    glb_ser = sexp_of_h2;
    glb_des = h2_of_sexp;

    top_ser = sexp_of_h3;
    top_des = h3_of_sexp;
  }

let ser_wit_fun_scheme_arg :
  (Names.variable * Libnames.qualid * Sorts.family, unit, unit)
    Ser_genarg.gen_ser =
  Ser_genarg.{
    raw_ser = sexp_of_triple Ser_names.sexp_of_variable Ser_libnames.sexp_of_qualid Ser_sorts.sexp_of_family;
    raw_des = triple_of_sexp Ser_names.variable_of_sexp Ser_libnames.qualid_of_sexp Ser_sorts.family_of_sexp;

    glb_ser = sexp_of_unit;
    glb_des = unit_of_sexp;

    top_ser = sexp_of_unit;
    top_des = unit_of_sexp;
  }

module Loc = Ser_loc
module Vernacexpr = Ser_vernacexpr

type function_fix_definition_loc_argtype = Vernacexpr.fixpoint_expr Loc.located
  [@@deriving sexp]

let ser_wit_function_fix_definition =
  Ser_genarg.mk_uniform sexp_of_function_fix_definition_loc_argtype function_fix_definition_loc_argtype_of_sexp

let ser_wit_auto_using' =
  Ser_genarg.{
    raw_ser = sexp_of_list Ser_constrexpr.sexp_of_constr_expr
  ; raw_des = list_of_sexp Ser_constrexpr.constr_expr_of_sexp

  ; glb_ser = sexp_of_list Ser_genintern.sexp_of_glob_constr_and_expr
  ; glb_des = list_of_sexp Ser_genintern.glob_constr_and_expr_of_sexp

  ; top_ser = sexp_of_list Ser_eConstr.sexp_of_constr
  ; top_des = list_of_sexp Ser_eConstr.constr_of_sexp
  }

let register () =
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_auto_using' ser_wit_auto_using';
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_constr_comma_sequence' ser_wit_auto_using';
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_with_names ser_wit_with_names;
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_fun_ind_using ser_wit_fun_ind_using;
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_fun_scheme_arg ser_wit_fun_scheme_arg;
  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_function_fix_definition ser_wit_function_fix_definition;
  ()

let _ = register ()