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
|
(************************************************************************)
(* 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: cooking.ml 10877 2008-04-30 21:58:41Z herbelin $ 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.map (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 = match cb.const_type with
| NonPolymorphicType t ->
let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
NonPolymorphicType typ
| PolymorphicArity (ctx,s) ->
let t = mkArity (ctx,Type s.poly_level) in
let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
let j = make_judge (force (Option.get body)) typ in
Typeops.make_polymorphic_if_constant_for_ind env j
in
let boxed = Cemitcodes.is_boxed cb.const_body_code in
(body, typ, cb.const_constraints, cb.const_opaque, boxed,false)
|
