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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Created by Jean-Christophe Filliâtre out of V6.3 file constants.ml
as part of the rebuilding of Coq around a purely functional
abstract type-checker, Nov 1999 *)
(* This module implements kernel-level discharching of local
declarations over global constants and inductive types *)
open Errors
open Util
open Names
open Term
open Sign
open Declarations
open Environ
(*s Cooking the constants. *)
type work_list = identifier array Cmap.t * identifier array Mindmap.t
let pop_dirpath p = match repr_dirpath p with
| [] -> anomaly "dirpath_prefix: empty dirpath"
| _::l -> make_dirpath l
let pop_mind kn =
let (mp,dir,l) = Names.repr_mind kn in
Names.make_mind mp (pop_dirpath dir) l
let pop_con con =
let (mp,dir,l) = Names.repr_con con in
Names.make_con mp (pop_dirpath 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_mind kn,i), Mindmap.find kn knl
| ConstructRef ((kn,i),j) ->
mkConstruct ((pop_mind kn,i),j), Mindmap.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, Mindmap.empty)
let is_empty_modlist (cm, mm) =
Cmap.is_empty cm && Mindmap.is_empty mm
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 is_empty_modlist modlist then c
else 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 = function
| Undef inl -> Undef inl
| Def cs -> Def (Declarations.from_val (f (Declarations.force cs)))
| OpaqueDef lc ->
OpaqueDef (Declarations.opaque_from_val (f (Declarations.force_opaque lc)))
let constr_of_def = function
| Undef _ -> assert false
| Def cs -> Declarations.force cs
| OpaqueDef lc -> Declarations.force_opaque lc
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 const_hyps =
Sign.fold_named_context (fun (h,_,_) hyps ->
List.filter (fun (id,_,_) -> not (id_eq id h)) hyps)
hyps ~init:cb.const_hyps 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 (constr_of_def body) typ in
Typeops.make_polymorphic_if_constant_for_ind env j
in
(body, typ, cb.const_constraints, const_hyps)
|
