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
135
136
|
(* $Id$ *)
open Names
open Generic
open Term
open Reduction
open Declarations
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 =
let genv = Global.env() in
Impl_auto (poly_args genv Evd.empty ty)
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 (body_of_type cb.const_type) 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 =
try Spmap.find sp !constants_table with Not_found -> No_impl
let constant_implicits_list sp =
list_of_implicits (constant_implicits sp)
(* 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 (mind_user_arity mip),
Array.map (fun c -> auto_implicits c) (mind_user_lc mip))
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) =
try
let imps = Spmap.find sp !inductives_table in fst imps.(i)
with Not_found ->
No_impl
let constructor_implicits ((sp,i),j) =
try
let imps = Spmap.find sp !inductives_table in (snd imps.(i)).(pred j)
with Not_found ->
No_impl
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)
(* Variables. *)
let var_table = ref Idmap.empty
let declare_var_implicits id =
let (_,ty) = Global.lookup_var id in
let imps = auto_implicits (body_of_type ty) in
var_table := Idmap.add id imps !var_table
let implicits_of_var id =
list_of_implicits (try Idmap.find id !var_table with Not_found -> No_impl)
(* Registration as global tables and roolback. *)
type frozen_t = bool
* 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 () =
(!implicit_args,!constants_table, !inductives_table, !var_table)
let unfreeze (imps,ct,it,vt) =
implicit_args := imps;
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
|
