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
|
(* $Id$ *)
open Util
open Names
open Constant
open Inductive
open Libobject
open Lib
open Impargs
(* Variables. *)
let cache_variable (_,obj) =
Global.push_var obj
let load_variable _ =
anomaly "we shouldn't load a variable"
let open_variable _ =
anomaly "we shouldn't open a variable"
let specification_variable _ =
anomaly "we shouldn't extract the specification of a variable"
let (in_variable, out_variable) =
let od = {
cache_function = cache_variable;
load_function = load_variable;
open_function = open_variable;
specification_function = specification_variable } in
declare_object ("Variable", od)
let declare_variable id c =
let obj = (id,c) in
Global.push_var obj;
let _ = add_leaf id CCI (in_variable obj) in
()
(* Parameters. *)
let cache_parameter (sp,c) =
Global.add_parameter sp c;
Nametab.push (basename sp) sp
let open_parameter (sp,_) =
Nametab.push (basename sp) sp
let specification_parameter obj = obj
let (in_parameter, out_parameter) =
let od = {
cache_function = cache_parameter;
load_function = (fun _ -> ());
open_function = open_parameter;
specification_function = specification_parameter } in
declare_object ("Parameter", od)
let declare_parameter id c =
let sp = add_leaf id CCI (in_parameter c) in
Global.add_parameter sp c;
Nametab.push (basename sp) sp
(* Constants. *)
let cache_constant (sp,ce) =
Global.add_constant sp ce;
Nametab.push (basename sp) sp;
declare_constant_implicits sp
let open_constant (sp,_) =
Nametab.push (basename sp) sp;
declare_constant_implicits sp
let specification_constant obj = obj
let (in_constant, out_constant) =
let od = {
cache_function = cache_constant;
load_function = (fun _ -> ());
open_function = open_constant;
specification_function = specification_constant } in
declare_object ("Constant", od)
let declare_constant id ce =
let sp = add_leaf id CCI (in_constant ce) in
Global.add_constant sp ce;
Nametab.push (basename sp) sp;
declare_constant_implicits sp
(* Inductives. *)
let push_inductive_names sp mie =
List.iter
(fun (id,_,cnames,_) ->
Nametab.push id sp;
List.iter (fun x -> Nametab.push x sp) cnames)
mie.mind_entry_inds
let cache_inductive (sp,mie) =
Global.add_mind sp mie;
push_inductive_names sp mie;
declare_inductive_implicits sp
let open_inductive (sp,mie) =
push_inductive_names sp mie;
declare_inductive_implicits sp
let specification_inductive obj = obj
let (in_inductive, out_inductive) =
let od = {
cache_function = cache_inductive;
load_function = (fun _ -> ());
open_function = open_inductive;
specification_function = specification_inductive } in
declare_object ("Inductive", od)
let declare_mind mie =
let id = match mie.mind_entry_inds with
| (id,_,_,_)::_ -> id
| [] -> anomaly "cannot declare an empty list of inductives"
in
let sp = add_leaf id CCI (in_inductive mie) in
Global.add_mind sp mie;
push_inductive_names sp mie;
declare_inductive_implicits sp
|
