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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
open Pp
open Util
open Names
open Term
open Sign
open Declarations
open Environ
open Reduction
(*s Cooking the constants. *)
type work_list = identifier array Cmap.t * identifier array KNmap.t
let dirpath_prefix p = match repr_dirpath p with
| [] -> anomaly "dirpath_prefix: empty dirpath"
| _::l -> make_dirpath l
let pop_kn kn =
let (mp,dir,l) = Names.repr_kn kn in
Names.make_kn mp (dirpath_prefix dir) l
let pop_con con =
let (mp,dir,l) = Names.repr_con con in
Names.make_con mp (dirpath_prefix dir) l
type my_global_reference =
| ConstRef of constant
| IndRef of inductive
| ConstructRef of constructor
let cache = (Hashtbl.create 13 : (my_global_reference, constr) Hashtbl.t)
let clear_cooking_sharing () = Hashtbl.clear cache
let share r (cstl,knl) =
try Hashtbl.find cache r
with Not_found ->
let f,l =
match r with
| IndRef (kn,i) ->
mkInd (pop_kn kn,i), KNmap.find kn knl
| ConstructRef ((kn,i),j) ->
mkConstruct ((pop_kn kn,i),j), KNmap.find kn knl
| ConstRef cst ->
mkConst (pop_con cst), Cmap.find cst cstl in
let c = mkApp (f, Array.map mkVar l) in
Hashtbl.add cache r c;
(* has raised Not_found if not in work_list *)
c
let update_case_info ci modlist =
try
let ind, n =
match kind_of_term (share (IndRef ci.ci_ind) modlist) with
| App (f,l) -> (destInd f, Array.length l)
| Ind ind -> ind, 0
| _ -> assert false in
{ ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
with Not_found ->
ci
let empty_modlist = (Cmap.empty, KNmap.empty)
let expmod_constr modlist c =
let rec substrec c =
match kind_of_term c with
| Case (ci,p,t,br) ->
map_constr substrec (mkCase (update_case_info ci modlist,p,t,br))
| Ind ind ->
(try
share (IndRef ind) modlist
with
| Not_found -> map_constr substrec c)
| Construct cstr ->
(try
share (ConstructRef cstr) modlist
with
| Not_found -> map_constr substrec c)
| Const cst ->
(try
share (ConstRef cst) modlist
with
| Not_found -> map_constr substrec c)
| _ -> map_constr substrec c
in
if modlist = empty_modlist then c
else under_outer_cast nf_betaiota (substrec c)
let abstract_constant_type =
List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c)
let abstract_constant_body =
List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
type recipe = {
d_from : constant_body;
d_abstract : named_context;
d_modlist : work_list }
let on_body f =
option_app (fun c -> Declarations.from_val (f (Declarations.force c)))
let cook_constant env r =
let cb = r.d_from in
let hyps = Sign.map_named_context (expmod_constr r.d_modlist) r.d_abstract in
let body =
on_body (fun c ->
abstract_constant_body (expmod_constr r.d_modlist c) hyps)
cb.const_body in
let typ =
abstract_constant_type (expmod_constr r.d_modlist cb.const_type) hyps in
let boxed = Cemitcodes.is_boxed cb.const_body_code in
(body, typ, cb.const_constraints, cb.const_opaque, boxed)
|
