forked from rocq-archive/coq-serapi
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ser_constrexpr.ml
162 lines (126 loc) · 5.44 KB
/
ser_constrexpr.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
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(************************************************************************)
(* Coq serialization API/Plugin *)
(* Copyright 2016-2017 MINES ParisTech *)
(************************************************************************)
(* Status: Very Experimental *)
(************************************************************************)
open Ppx_hash_lib.Std.Hash.Builtin
open Ppx_compare_lib.Builtin
let hash_fold_array = Ppx_hash_lib.Std.Hash.Builtin.hash_fold_array_frozen
open Sexplib.Std
module Loc = Ser_loc
module CAst = Ser_cAst
module Names = Ser_names
module Constr = Ser_constr
module UState = Ser_uState
module Namegen = Ser_namegen
module Pattern = Ser_pattern
module Evar_kinds = Ser_evar_kinds
module Genarg = Ser_genarg
module Libnames = Ser_libnames
module Glob_term = Ser_glob_term
module NumTok = Ser_numTok
module Univ = Ser_univ
type sort_name_expr =
[%import: Constrexpr.sort_name_expr]
[@@deriving sexp,yojson,hash,compare]
type univ_level_expr =
[%import: Constrexpr.univ_level_expr]
[@@deriving sexp,yojson,hash,compare]
type sort_expr =
[%import: Constrexpr.sort_expr]
[@@deriving sexp,yojson,hash,compare]
type univ_constraint_expr =
[%import: Constrexpr.univ_constraint_expr]
[@@deriving sexp,yojson,hash,compare]
type instance_expr =
[%import: Constrexpr.instance_expr]
[@@deriving sexp,yojson,hash,compare]
type 'a or_by_notation_r =
[%import: 'a Constrexpr.or_by_notation_r]
[@@deriving sexp,yojson,hash,compare]
type 'a or_by_notation =
[%import: 'a Constrexpr.or_by_notation]
[@@deriving sexp,yojson,hash,compare]
type universe_decl_expr =
[%import: Constrexpr.universe_decl_expr]
[@@deriving sexp,yojson,hash,compare]
type ident_decl =
[%import: Constrexpr.ident_decl]
[@@deriving sexp,yojson,hash,compare]
type cumul_univ_decl_expr =
[%import: Constrexpr.cumul_univ_decl_expr]
[@@deriving sexp,yojson,hash,compare]
type cumul_ident_decl =
[%import: Constrexpr.cumul_ident_decl]
[@@deriving sexp,yojson,hash,compare]
type name_decl =
[%import: Constrexpr.name_decl]
[@@deriving sexp,yojson,hash,compare]
type notation_entry =
[%import: Constrexpr.notation_entry]
[@@deriving sexp,yojson,hash,compare]
type entry_level =
[%import: Constrexpr.entry_level]
[@@deriving sexp,yojson]
type entry_relative_level =
[%import: Constrexpr.entry_relative_level]
[@@deriving sexp,yojson]
type notation_entry_level =
[%import: Constrexpr.notation_entry_level]
[@@deriving sexp,yojson]
type notation_key =
[%import: Constrexpr.notation_key]
[@@deriving sexp,yojson,hash,compare]
type notation = [%import: Constrexpr.notation]
[@@deriving sexp,yojson,hash,compare]
type explicitation = [%import: Constrexpr.explicitation]
[@@deriving sexp,yojson,hash,compare]
type binder_kind = [%import: Constrexpr.binder_kind]
[@@deriving sexp,yojson,hash,compare]
type explicit_flag = [%import: Constrexpr.explicit_flag]
[@@deriving sexp,yojson,hash,compare]
(* type abstraction_kind = [%import: Constrexpr.abstraction_kind]
* [@@deriving sexp,yojson] *)
(* type proj_flag = [%import: Constrexpr.proj_flag]
* [@@deriving sexp,yojson] *)
(* type raw_numeral = [%import: Constrexpr.raw_numeral]
* [@@deriving sexp,yojson] *)
(* type sign = [%import: Constrexpr.sign]
* [@@deriving sexp,yojson] *)
type prim_token = [%import: Constrexpr.prim_token]
[@@deriving sexp,yojson,hash,compare]
type notation_with_optional_scope =
[%import: Constrexpr.notation_with_optional_scope]
[@@deriving sexp,yojson,hash,compare]
type cases_pattern_expr_r = [%import: Constrexpr.cases_pattern_expr_r]
and cases_pattern_expr = [%import: Constrexpr.cases_pattern_expr]
and kinded_cases_pattern_expr = [%import: Constrexpr.kinded_cases_pattern_expr]
and cases_pattern_notation_substitution = [%import: Constrexpr.cases_pattern_notation_substitution]
and constr_expr_r = [%import: Constrexpr.constr_expr_r]
and constr_expr = [%import: Constrexpr.constr_expr]
and case_expr = [%import: Constrexpr.case_expr]
and branch_expr = [%import: Constrexpr.branch_expr]
and fix_expr = [%import: Constrexpr.fix_expr]
and cofix_expr = [%import: Constrexpr.cofix_expr]
and recursion_order_expr_r = [%import: Constrexpr.recursion_order_expr_r]
and recursion_order_expr = [%import: Constrexpr.recursion_order_expr]
and local_binder_expr = [%import: Constrexpr.local_binder_expr]
and constr_notation_substitution = [%import: Constrexpr.constr_notation_substitution]
[@@deriving sexp,yojson,hash,compare]
type constr_pattern_expr = [%import: Constrexpr.constr_pattern_expr]
[@@deriving sexp,yojson,hash,compare]
type with_declaration_ast =
[%import: Constrexpr.with_declaration_ast]
[@@deriving sexp,yojson,hash,compare]
type module_ast_r = [%import: Constrexpr.module_ast_r]
and module_ast =
[%import: Constrexpr.module_ast]
[@@deriving sexp,yojson,hash,compare]