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
130
131
132
133
134
|
(* $Id$ *)
open Names
open Generic
open Term
open Reduction
open Constant
open Inductive
type implicits =
| Impl_auto of int list
| Impl_manual of int list
| No_impl
let implicit_args = ref false
let make_implicit_args flag = implicit_args := flag
let is_implicit_args () = !implicit_args
let implicitely f x =
let oimplicit = !implicit_args in
try
implicit_args := true;
let rslt = f x in
implicit_args := oimplicit;
rslt
with e -> begin
implicit_args := oimplicit;
raise e
end
let auto_implicits ty =
if !implicit_args then
let genv = Global.env() in
Impl_auto (poly_args genv Evd.empty ty)
else
No_impl
let list_of_implicits = function
| Impl_auto l -> l
| Impl_manual l -> l
| 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)
let constructor_implicits_list constr_sp =
list_of_implicits (constructor_implicits constr_sp)
let inductive_implicits_list ind_sp =
list_of_implicits (inductive_implicits ind_sp)
let constant_implicits_list sp =
list_of_implicits (constant_implicits sp)
(* Variables. *)
let var_table = ref Idmap.empty
let declare_var_implicits id =
let (_,ty) = Global.lookup_var id in
let imps = auto_implicits ty.body in
var_table := Idmap.add id imps !var_table
let implicits_of_var _ id =
list_of_implicits (Idmap.find id !var_table)
(* Registration as global tables and roolback. *)
type frozen_t = implicits Spmap.t
* (implicits * implicits array) array Spmap.t
* implicits Idmap.t
let init () =
constants_table := Spmap.empty;
inductives_table := Spmap.empty;
var_table := Idmap.empty
let freeze () =
!constants_table, !inductives_table, !var_table
let unfreeze (ct,it,vt) =
constants_table := ct;
inductives_table := it;
var_table := vt
let _ =
Summary.declare_summary "implicits"
{ 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
|
