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
|
open Names
open Cic
(* Environments *)
type globals = {
env_constants : constant_body Cmap_env.t;
env_inductives : mutual_inductive_body Mindmap_env.t;
env_inductives_eq : KerName.t KNmap.t;
env_modules : module_body MPmap.t;
env_modtypes : module_type_body MPmap.t}
type stratification = {
env_universes : Univ.universes;
env_engagement : engagement;
}
type env = {
env_globals : globals;
env_rel_context : rel_context;
env_stratification : stratification;
env_imports : Cic.vodigest MPmap.t;
env_conv_oracle : Cic.oracle;
}
val empty_env : env
(* Engagement *)
val engagement : env -> Cic.engagement
val set_engagement : Cic.engagement -> env -> env
(** Oracle *)
val set_oracle : env -> Cic.oracle -> env
(* Digests *)
val add_digest : env -> DirPath.t -> Cic.vodigest -> env
val lookup_digest : env -> DirPath.t -> Cic.vodigest
(* de Bruijn variables *)
val rel_context : env -> rel_context
val lookup_rel : int -> env -> rel_declaration
val push_rel : rel_declaration -> env -> env
val push_rel_context : rel_context -> env -> env
val push_rec_types : Name.t array * constr array * 'a -> env -> env
(* Universes *)
val universes : env -> Univ.universes
val add_constraints : Univ.constraints -> env -> env
val push_context : ?strict:bool -> Univ.universe_context -> env -> env
val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
val check_constraints : Univ.constraints -> env -> bool
(* Constants *)
val lookup_constant : Constant.t -> env -> Cic.constant_body
val add_constant : Constant.t -> Cic.constant_body -> env -> env
val constant_type : env -> Constant.t puniverses -> constr Univ.constrained
type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
val constant_value : env -> Constant.t puniverses -> constr
val evaluable_constant : Constant.t -> env -> bool
(** NB: here in the checker we check the inferred info (npars, label) *)
val lookup_projection : Projection.t -> env -> constr
(* Inductives *)
val mind_equiv : env -> inductive -> inductive -> bool
val lookup_mind :
MutInd.t -> env -> Cic.mutual_inductive_body
val add_mind :
MutInd.t -> Cic.mutual_inductive_body -> env -> env
(* Modules *)
val add_modtype :
ModPath.t -> Cic.module_type_body -> env -> env
val shallow_add_module :
ModPath.t -> Cic.module_body -> env -> env
val shallow_remove_module : ModPath.t -> env -> env
val lookup_module : ModPath.t -> env -> Cic.module_body
val lookup_modtype : ModPath.t -> env -> Cic.module_type_body
|
