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
|
(* $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 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 mconstr_implicits mc =
let (sp, i, j, _) = destMutConstruct mc in
list_of_implicits (constructor_implicits ((sp,i),j))
let mind_implicits m =
let (sp,i,_) = destMutInd m in
list_of_implicits (inductive_implicits (sp,i))
let implicits_of_var kind id =
failwith "TODO: implicits of vars"
(* 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 "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
|
