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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
open Names
open Constr
open Univ
open UVars
open Environ
(** {6 Typing functions (not yet tagged as safe) }
They return unsafe judgments that are "in context" of a set of
(local) universe variables (the ones that appear in the term) and
associated constraints. In case of polymorphic definitions, these
variables and constraints will be generalized.
When typechecking a term it may be updated to fix relevance marks.
Do not discard the result. *)
val infer : env -> constr -> unsafe_judgment
val infer_type : env -> types -> unsafe_type_judgment
val check_context :
env -> Constr.rel_context -> env * Constr.rel_context
(** {6 Basic operations of the typing machine. } *)
(** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j]
returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *)
val assumption_of_judgment : env -> unsafe_judgment -> Sorts.relevance
val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment
(** {6 Type of sorts. } *)
val type1 : types
val type_of_sort : Sorts.t -> types
val judge_of_prop : unsafe_judgment
val judge_of_set : unsafe_judgment
val judge_of_type : Universe.t -> unsafe_judgment
(** {6 Type of a bound variable. } *)
val type_of_relative : env -> int -> types
val judge_of_relative : env -> int -> unsafe_judgment
(** {6 Type of variables } *)
val type_of_variable : env -> variable -> types
val judge_of_variable : env -> variable -> unsafe_judgment
(** {6 type of a constant } *)
val type_of_constant_in : env -> pconstant -> types
val judge_of_constant : env -> pconstant -> unsafe_judgment
(** {6 type of an applied projection } *)
val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment
(** {6 Type of application. } *)
val judge_of_apply :
env -> unsafe_judgment -> unsafe_judgment array
-> unsafe_judgment
(** {6 Type of an abstraction. } *)
(* val judge_of_abstraction : *)
(* env -> Name.t -> unsafe_type_judgment -> unsafe_judgment *)
(* -> unsafe_judgment *)
(** {6 Type of a product. } *)
val sort_of_product : env -> Sorts.t -> Sorts.t -> Sorts.t
val type_of_product : env -> Name.t binder_annot -> Sorts.t -> Sorts.t -> types
(* val judge_of_product : *)
(* env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment *)
(* -> unsafe_judgment *)
(** s Type of a let in. *)
(* val judge_of_letin : *)
(* env -> Name.t -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment *)
(* -> unsafe_judgment *)
(** {6 Type of a cast. } *)
val judge_of_cast :
env -> unsafe_judgment -> cast_kind -> unsafe_type_judgment ->
unsafe_judgment
(** {6 Inductive types. } *)
val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment
val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment
(** {6 Type of global references. } *)
val type_of_global_in_context : env -> GlobRef.t -> types * UVars.AbstractContext.t
(** Returns the type of the global reference, by creating a fresh
instance of polymorphic references and computing their
instantiated universe context. The type should not be used
without pushing it's universe context in the environmnent of
usage. For non-universe-polymorphic constants, it does not
matter. *)
(** {6 Miscellaneous. } *)
(** Check that hyps are included in env and fails with error otherwise *)
val check_hyps_inclusion : env -> ?evars:CClosure.evar_handler ->
GlobRef.t -> Constr.named_context -> unit
(** Types for primitives *)
val type_of_int : env -> types
val judge_of_int : env -> Uint63.t -> unsafe_judgment
val type_of_float : env -> types
val judge_of_float : env -> Float64.t -> unsafe_judgment
val type_of_string : env -> types
val judge_of_string : env -> Pstring.t -> unsafe_judgment
val type_of_array : env -> UVars.Instance.t -> types
val judge_of_array : env -> UVars.Instance.t -> unsafe_judgment array -> unsafe_judgment -> unsafe_judgment
val type_of_prim_type : env -> UVars.Instance.t -> 'a CPrimitives.prim_type -> types
val type_of_prim : env -> UVars.Instance.t -> CPrimitives.t -> types
val type_of_prim_or_type : env -> UVars.Instance.t -> CPrimitives.op_or_type -> types
val warn_bad_relevance_name : string
(** Allow the checker to make this warning into an error. *)
val bad_relevance_warning : CWarnings.warning
(** Also used by the pretyper to define a message which uses the evar map. *)
type ('constr,'types, 'r) bad_relevance =
| BadRelevanceBinder of 'r * ('constr,'types,'r) Context.Rel.Declaration.pt
| BadRelevanceCase of 'r * 'constr
val bad_relevance_msg : (env * (constr,types,Sorts.relevance) bad_relevance) CWarnings.msg
(** Used by the higher layers to register a nicer printer than the default. *)
val should_invert_case : env -> Sorts.relevance -> case_info -> bool
(** Matches must be annotated with the indices when going from SProp to non SProp
(implies 1 or 0 constructors). *)
|
