File: environ.mli

package info (click to toggle)
coq-doc 8.2pl1-1
  • links: PTS, VCS
  • area: non-free
  • in suites: squeeze
  • size: 19,240 kB
  • ctags: 22,737
  • sloc: ml: 132,933; ansic: 1,960; sh: 1,366; lisp: 456; makefile: 327
file content (77 lines) | stat: -rw-r--r-- 2,686 bytes parent folder | download | duplicates (2)
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
open Names
open Term

(* Environments *)

type globals = {
  env_constants : Declarations.constant_body Cmap.t;
  env_inductives : Declarations.mutual_inductive_body KNmap.t;
  env_modules : Declarations.module_body MPmap.t;
  env_modtypes : Declarations.module_type_body MPmap.t;
  env_alias : module_path MPmap.t;
}
type stratification = {
  env_universes : Univ.universes;
  env_engagement : Declarations.engagement option;
}
type env = {
  env_globals : globals;
  env_named_context : named_context;
  env_rel_context : rel_context;
  env_stratification : stratification;
  env_imports : Digest.t MPmap.t;
}
val empty_env : env

(* Engagement *)
val engagement : env -> Declarations.engagement option
val set_engagement : Declarations.engagement -> env -> env

(* Digests *)
val add_digest : env -> dir_path -> Digest.t -> env
val lookup_digest : env -> dir_path -> Digest.t

(* 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 array * constr array * 'a -> env -> env

(* Named variables *)
val named_context : env -> named_context
val push_named : named_declaration -> env -> env
val lookup_named : identifier -> env -> named_declaration
val named_type : identifier -> env -> constr

(* Universes *)
val universes : env -> Univ.universes
val add_constraints : Univ.constraints -> env -> env

(* Constants *)
val lookup_constant : constant -> env -> Declarations.constant_body
val add_constant : constant -> Declarations.constant_body -> env -> env
val constant_type : env -> constant -> Declarations.constant_type
type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
val constant_value : env -> constant -> constr
val constant_opt_value : env -> constant -> constr option
val evaluable_constant : constant -> env -> bool

(* Inductives *)
val lookup_mind :
  mutual_inductive -> env -> Declarations.mutual_inductive_body
val scrape_mind : env -> mutual_inductive -> mutual_inductive
val add_mind :
  mutual_inductive -> Declarations.mutual_inductive_body -> env -> env
val mind_equiv : env -> inductive -> inductive -> bool

(* Modules *)
val add_modtype :
  module_path -> Declarations.module_type_body -> env -> env
val shallow_add_module :
  module_path -> Declarations.module_body -> env -> env
val register_alias : module_path -> module_path -> env -> env
val scrape_alias : module_path -> env -> module_path
val lookup_module : module_path -> env -> Declarations.module_body
val lookup_modtype : module_path -> env -> Declarations.module_type_body