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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Util
open Pp
open Names
open Term
open Typeops
open Libobject
open Library
open Classops
let nbimpl = ref 0
let nbpathc = ref 0
let nbcoer = ref 0
let nbstruc = ref 0
let nbimplstruc = ref 0
let compter = ref false
(*s Une structure S est un type inductif non récursif à un seul
constructeur (de nom par défaut Build_S) *)
(* Table des structures: le nom de la structure (un [inductive]) donne
le nom du constructeur, le nombre de paramètres et pour chaque
argument réels du constructeur, le noms de la projection
correspondante, si valide *)
type struc_typ = {
s_CONST : identifier;
s_PARAM : int;
s_PROJ : constant option list }
let structure_table = (ref [] : (inductive * struc_typ) list ref)
let cache_structure (_,x) = structure_table := x :: (!structure_table)
let (inStruc,outStruc) =
declare_object
("STRUCTURE", {
load_function = (fun _ -> ());
cache_function = cache_structure;
open_function = cache_structure;
export_function = (function x -> Some x)
})
let add_new_struc (s,c,n,l) =
Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
let find_structure indsp = List.assoc indsp !structure_table
(*s Un "object" est une fonction construisant une instance d'une structure *)
(* Table des definitions "object" : pour chaque object c,
c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n)
avec ti = (ci ui1...uir)
Pour tout ci, et Li, la ième projection de la structure R (si
définie), on déclare une "coercion"
o_DEF = c
o_TABS = B1...Bk
o_PARAMS = a1...am
o_TCOMP = ui1...uir
*)
type obj_typ = {
o_DEF : constr;
o_TABS : constr list; (* dans l'ordre *)
o_TPARAMS : constr list; (* dans l'ordre *)
o_TCOMPS : constr list } (* dans l'ordre *)
let object_table =
(ref [] : ((global_reference * global_reference) * obj_typ) list ref)
let cache_object (_,x) = object_table := x :: (!object_table)
let (inObjDef, outObjDef) =
declare_object
("OBJDEF", {
load_function = (fun _ -> ());
open_function = cache_object;
cache_function = cache_object;
export_function = (function x -> Some x)
})
let add_new_objdef (o,c,la,lp,l) =
try
let _ = List.assoc o !object_table in ()
with Not_found ->
Lib.add_anonymous_leaf
(inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l}))
let cache_objdef1 (_,sp) = ()
let (inObjDef1, outObjDef1) =
declare_object
("OBJDEF1", {
load_function = (fun _ -> ());
open_function = cache_objdef1;
cache_function = cache_objdef1;
export_function = (function x -> Some x)
})
let objdef_info o = List.assoc o !object_table
let freeze () = !structure_table, !object_table
let unfreeze (s,o) = structure_table := s; object_table := o
let init () = structure_table := []; object_table:=[]
let _ = init()
let _ =
Summary.declare_summary "objdefs"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = init;
Summary.survive_section = false }
|
