blob: 95b322e4e24b93a2d18cfabf38562fb17e3b4d56 (
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
|
(* $Id$ *)
open Names
open Generic
open Term
open Reduction
open Constant
open Inductive
open Typing
type implicits =
| Impl_auto of int list
| Impl_manual of int list
| No_impl
let implicit_args = ref false
let auto_implicits ty =
if !implicit_args then
let genv = unsafe_env_of_env (Global.env()) in
Impl_auto (poly_args genv ty)
else
No_impl
(* Constants. *)
let constants_table = ref Spmap.empty
let declare_constant_implicits sp =
let cb = Global.lookup_constant sp in
let imps = auto_implicits cb.const_type.body in
constants_table := Spmap.add sp imps !constants_table
let declare_constant_manual_implicits sp imps =
constants_table := Spmap.add sp (Impl_manual imps) !constants_table
let constant_implicits sp =
Spmap.find sp !constants_table
(* Inductives and constructors. Their implicit arguments are stored
in an array, indexed by the inductive number, of pairs $(i,v)$ where
$i$ are the implicit arguments of the inductive and $v$ the array of
implicit arguments of the constructors. *)
let inductives_table = ref Spmap.empty
let declare_inductive_implicits sp =
let mib = Global.lookup_mind sp in
let imps_one_inductive mip =
(auto_implicits mip.mind_arity.body,
let (_,lc) = decomp_all_DLAMV_name mip.mind_lc in
Array.map auto_implicits lc)
in
let imps = Array.map imps_one_inductive mib.mind_packets in
inductives_table := Spmap.add sp imps !inductives_table
let inductive_implicits (sp,i) =
let imps = Spmap.find sp !inductives_table in
fst imps.(i)
let constructor_implicits ((sp,i),j) =
let imps = Spmap.find sp !inductives_table in
(snd imps.(i)).(pred j)
(* Registration as global tables and roolback. *)
type frozen = implicits Spmap.t
let init () =
constants_table := Spmap.empty
let freeze () =
!constants_table
let unfreeze ct =
constants_table := ct
let _ =
Summary.declare_summary "names"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
Summary.init_function = init }
let rollback f x =
let fs = freeze () in
try f x with e -> begin unfreeze fs; raise e end
|