forked from rocq-archive/coq-serapi
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathser_declarations.mli
110 lines (85 loc) · 4.34 KB
/
ser_declarations.mli
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
(************************************************************************)
(* 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-2017 MINES ParisTech *)
(* Written by: Emilio J. Gallego Arias *)
(************************************************************************)
(* Status: Very Experimental *)
(************************************************************************)
open Sexplib
type template_arity = Declarations.template_arity
val template_arity_of_sexp : Sexp.t -> template_arity
val sexp_of_template_arity : template_arity -> Sexp.t
type ('a, 'b) declaration_arity = ('a, 'b) Declarations.declaration_arity
val declaration_arity_of_sexp :
(Sexp.t -> 'a) ->
(Sexp.t -> 'b) ->
Sexp.t -> ('a, 'b) declaration_arity
val sexp_of_declaration_arity :
('a -> Sexp.t) ->
('b -> Sexp.t) ->
('a, 'b) declaration_arity -> Sexp.t
type recarg = Declarations.recarg
val recarg_of_sexp : Sexp.t -> recarg
val sexp_of_recarg : recarg -> Sexp.t
type wf_paths = recarg Rtree.t
val wf_paths_of_sexp : Sexp.t -> wf_paths
val sexp_of_wf_paths : wf_paths -> Sexp.t
type regular_inductive_arity = Declarations.regular_inductive_arity
val regular_inductive_arity_of_sexp : Sexp.t -> regular_inductive_arity
val sexp_of_regular_inductive_arity : regular_inductive_arity -> Sexp.t
type inductive_arity = Declarations.inductive_arity
val inductive_arity_of_sexp : Sexp.t -> inductive_arity
val sexp_of_inductive_arity : inductive_arity -> Sexp.t
type one_inductive_body = Declarations.one_inductive_body
val one_inductive_body_of_sexp : Sexp.t -> one_inductive_body
val sexp_of_one_inductive_body : one_inductive_body -> Sexp.t
(* type set_predicativity = Declarations.set_predicativity
* val set_predicativity_of_sexp : Sexp.t -> set_predicativity
* val sexp_of_set_predicativity : set_predicativity -> Sexp.t *)
(* type engagement = Declarations.engagement
* val engagement_of_sexp : Sexp.t -> engagement
* val sexp_of_engagement : engagement -> Sexp.t *)
type typing_flags = Declarations.typing_flags
val typing_flags_of_sexp : Sexp.t -> typing_flags
val sexp_of_typing_flags : typing_flags -> Sexp.t
type inline = Declarations.inline
val sexp_of_inline : inline -> Sexp.t
val inline_of_sexp : Sexp.t -> inline
(* type work_list = Declarations.work_list *)
(* type abstr_info = Declarations.abstr_info = {
* abstr_ctx : Constr.named_context;
* abstr_subst : Univ.Instance.t;
* abstr_uctx : Univ.AbstractContext.t;
* }
*
* type cooking_info = Declarations.cooking_info
* val sexp_of_cooking_info : cooking_info -> Sexp.t
* val cooking_info_of_sexp : Sexp.t -> cooking_info *)
type constant_body = Declarations.constant_body
[@@deriving sexp,yojson,hash,compare]
(* type record_body = Declarations.record_body
* val record_body_of_sexp : Sexp.t -> record_body
* val sexp_of_record_body : record_body -> Sexp.t *)
type recursivity_kind = Declarations.recursivity_kind
val recursivity_kind_of_sexp : Sexp.t -> recursivity_kind
val sexp_of_recursivity_kind : recursivity_kind -> Sexp.t
val recursivity_kind_of_yojson : Yojson.Safe.t -> (recursivity_kind, string) Result.result
val recursivity_kind_to_yojson : recursivity_kind -> Yojson.Safe.t
type mutual_inductive_body = Declarations.mutual_inductive_body
[@@deriving sexp,yojson,hash,compare]
type 'a module_alg_expr = 'a Declarations.module_alg_expr
val sexp_of_module_alg_expr : ('a -> Sexp.t) -> 'a module_alg_expr -> Sexp.t
val module_alg_expr_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a module_alg_expr
type structure_body = Declarations.structure_body
[@@deriving sexp,yojson,hash,compare]
type module_body = Declarations.module_body
[@@deriving sexp,yojson,hash,compare]
type module_type_body = Declarations.module_type_body
[@@deriving sexp,yojson,hash,compare]