blob: 335ca1057f3807ba0fffbfed6cf586ffaffc3af6 (
plain)
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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
open Names
open Constr
open Declarations
(** The type of environments. *)
type link_info =
| Linked of string
| LinkedInteractive of string
| NotLinked
type key = int CEphemeron.key option ref
type constant_key = constant_body * (link_info ref * key)
type mind_key = mutual_inductive_body * link_info ref
type globals = {
env_constants : constant_key Cmap_env.t;
env_inductives : mind_key Mindmap_env.t;
env_modules : module_body MPmap.t;
env_modtypes : module_type_body MPmap.t}
type stratification = {
env_universes : UGraph.t;
env_engagement : engagement
}
type lazy_val
val force_lazy_val : lazy_val -> (values * Id.Set.t) option
val dummy_lazy_val : unit -> lazy_val
val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit
type named_context_val = private {
env_named_ctx : Context.Named.t;
env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t;
}
type rel_context_val = private {
env_rel_ctx : Context.Rel.t;
env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t;
}
type env = {
env_globals : globals;
env_named_context : named_context_val;
env_rel_context : rel_context_val;
env_nb_rel : int;
env_stratification : stratification;
env_typing_flags : typing_flags;
retroknowledge : Retroknowledge.retroknowledge;
indirect_pterms : Opaqueproof.opaquetab;
}
val empty_named_context_val : named_context_val
val empty_env : env
(** Rel context *)
val empty_rel_context_val : rel_context_val
val push_rel_context_val :
Context.Rel.Declaration.t -> rel_context_val -> rel_context_val
val match_rel_context_val :
rel_context_val -> (Context.Rel.Declaration.t * lazy_val * rel_context_val) option
val nb_rel : env -> int
val push_rel : Context.Rel.Declaration.t -> env -> env
val lookup_rel : int -> env -> Context.Rel.Declaration.t
val lookup_rel_val : int -> env -> lazy_val
val env_of_rel : int -> env -> env
(** Named context *)
val push_named_context_val :
Context.Named.Declaration.t -> named_context_val -> named_context_val
val push_named_context_val_val :
Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val
val match_named_context_val :
named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option
val map_named_val :
(constr -> constr) -> named_context_val -> named_context_val
val push_named : Context.Named.Declaration.t -> env -> env
val lookup_named : Id.t -> env -> Context.Named.Declaration.t
val lookup_named_val : Id.t -> env -> lazy_val
val env_of_named : Id.t -> env -> env
(** Global constants *)
val lookup_constant_key : Constant.t -> env -> constant_key
val lookup_constant : Constant.t -> env -> constant_body
(** Mutual Inductives *)
val lookup_mind_key : MutInd.t -> env -> mind_key
val lookup_mind : MutInd.t -> env -> mutual_inductive_body
|
