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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(** A structure S is a non recursive inductive type with a single
constructor *)
module Structure : sig
(** A projection to a structure field *)
type projection = {
proj_name : Names.Name.t; (** field name *)
proj_true : bool; (** false for primitive records *)
proj_canonical : bool; (** false = not to be used for CS inference *)
proj_body : Names.Constant.t option; (** the projection function *)
}
type t = {
name : Names.inductive;
projections : projection list;
nparams : int;
}
val make : Environ.env -> Names.inductive -> projection list -> t
val register : t -> unit
val subst : Mod_subst.substitution -> t -> t
(** refreshes nparams, e.g. after section discharging *)
val rebuild : Environ.env -> t -> t
(** [find isp] returns the Structure.t associated to the
inductive path [isp] if it corresponds to a structure, otherwise
it fails with [Not_found] *)
val find : Names.inductive -> t
(** raise [Not_found] if not a structure projection *)
val find_from_projection : Names.Constant.t -> t
(** [lookup_projections isp] returns the projections associated to the
inductive path [isp] if it corresponds to a structure, otherwise
it fails with [Not_found] *)
val find_projections : Names.inductive -> Names.Constant.t option list
(** raise [Not_found] if not a projection *)
val projection_nparams : Names.Constant.t -> int
val is_projection : Names.Constant.t -> bool
end
(** A canonical instance declares "canonical" conversion hints between
the effective components of a structure and the projections of the
structure *)
module Instance : sig
type t
(** Process a record instance, checkig it can be registered as canonical.
The record type must be declared as a canonical Structure.t beforehand. *)
val make : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> t
(** Register an instance as canonical *)
val register : warn:bool -> Environ.env -> Evd.evar_map -> t -> unit
val subst : Mod_subst.substitution -> t -> t
val repr : t -> Names.GlobRef.t
end
(** A ValuePattern.t characterizes the form of a component of canonical
instance and is used to query the data base of canonical instances *)
module ValuePattern : sig
type t =
| Const_cs of Names.GlobRef.t
| Proj_cs of Names.Projection.Repr.t
| Prod_cs
| Sort_cs of Sorts.family
| Default_cs
val equal : Environ.env -> t -> t -> bool
val compare : t -> t -> int
val print : t -> Pp.t
(** Return the form of the component of a canonical structure *)
val of_constr : Environ.env -> Constr.t -> t * int option * Constr.t list
end
(** The canonical solution of a problem (proj,val) is a global
[constant = fun abs : abstractions_ty => body] and
[body = RecodConstructor params canon_values] and the canonical value
corresponding to val is [val cvalue_arguments].
It is possible that val is one of the [abs] abstractions, eg [Default_cs],
and in that case [cvalue_abstraction = Some i] *)
module CanonicalSolution : sig
type t = {
constant : EConstr.t;
abstractions_ty : EConstr.t list;
body : EConstr.t;
nparams : int;
params : EConstr.t list;
cvalue_abstraction : int option;
cvalue_arguments : EConstr.t list;
}
(** [find (p,v)] returns a s such that p s = v.
The solution s gets a fresh universe instance and is decomposed into
bits for consumption by evarconv. Can raise [Not_found] on failure *)
val find :
Environ.env -> Evd.evar_map -> (Names.GlobRef.t * ValuePattern.t) ->
Evd.evar_map * t
(** [is_open_canonical_projection env sigma t] is true if t is a FieldName
applied to term which is not a constructor. Used by evarconv not to
unfold too much and lose a projection too early *)
val is_open_canonical_projection :
Environ.env -> Evd.evar_map -> EConstr.t -> bool
end
(** Low level access to the Canonical Structure database *)
module CSTable : sig
type entry = {
projection : Names.GlobRef.t;
value : ValuePattern.t;
solution : Names.GlobRef.t;
}
(** [all] returns the list of tuples { p ; v ; s }
Note: p s = v *)
val entries : unit -> entry list
(** [entries_for p] returns the list of canonical entries that have
p as their FieldName *)
val entries_for : projection:Names.GlobRef.t -> entry list
end
(** Some extra info for structures which are primitive records *)
module PrimitiveProjections : sig
(** Sets up the mapping from constants to primitive projections *)
val register : Names.Projection.Repr.t -> Names.Constant.t -> unit
val mem : Names.Constant.t -> bool
val find_opt : Names.Constant.t -> Names.Projection.Repr.t option
end
|
