aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/declareops.ml
blob: 0e4b80495ebc3965d8d0946128b3aaea774f218f (plain)
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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
(************************************************************************)
(*  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        *)
(************************************************************************)

open Declarations
open Mod_subst
open Util

(** Operations concernings types in [Declarations] :
    [constant_body], [mutual_inductive_body], [module_body] ... *)

(** {6 Constants } *)

let body_of_constant cb = match cb.const_body with
  | Undef _ -> None
  | Def c -> Some (force_constr c)
  | OpaqueDef o -> Some (Opaqueproof.force_proof o)

let constraints_of_constant cb = Univ.Constraint.union 
  (Univ.UContext.constraints (Future.force cb.const_universes))
  (match cb.const_body with
  | Undef _ -> Univ.empty_constraint
  | Def c -> Univ.empty_constraint
  | OpaqueDef o -> Opaqueproof.force_constraints o)

let constant_has_body cb = match cb.const_body with
  | Undef _ -> false
  | Def _ | OpaqueDef _ -> true

let is_opaque cb = match cb.const_body with
  | OpaqueDef _ -> true
  | Undef _ | Def _ -> false

(** {7 Constant substitutions } *)

let subst_rel_declaration sub (id,copt,t as x) =
  let copt' = Option.smartmap (subst_mps sub) copt in
  let t' = subst_mps sub t in
  if copt == copt' && t == t' then x else (id,copt',t')

let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)

(* let subst_const_type sub arity = match arity with *)
(*   | NonPolymorphicType s -> *)
(*     let s' = subst_mps sub s in *)
(*     if s==s' then arity else NonPolymorphicType s' *)
(*   | PolymorphicArity (ctx,s) -> *)
(*     let ctx' = subst_rel_context sub ctx in *)
(*     if ctx==ctx' then arity else PolymorphicArity (ctx',s) *)

let subst_const_type sub arity =
  if is_empty_subst sub then arity
  else subst_mps sub arity

(** No need here to check for physical equality after substitution,
    at least for Def due to the delayed substitution [subst_constr_subst]. *)
let subst_const_def sub def = match def with
  | Undef _ -> def
  | Def c -> Def (subst_constr sub c)
  | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o)

let subst_const_proj sub pb =
  { pb with proj_ind = subst_mind sub pb.proj_ind;
    proj_type = subst_mps sub pb.proj_type;
    proj_body = subst_const_type sub pb.proj_body }

let subst_const_body sub cb =
  assert (List.is_empty cb.const_hyps); (* we're outside sections *)
  if is_empty_subst sub then cb
  else
    let body' = subst_const_def sub cb.const_body in
    let type' = subst_const_type sub cb.const_type in
    let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in
    if body' == cb.const_body && type' == cb.const_type
      && proj' == cb.const_proj then cb
    else
      { const_hyps = [];
        const_body = body';
        const_type = type';
        const_proj = proj';
        const_body_code =
          Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
        const_polymorphic = cb.const_polymorphic;
        const_universes = cb.const_universes;
        const_inline_code = cb.const_inline_code }

(** {7 Hash-consing of constants } *)

(** This hash-consing is currently quite partial : we only
    share internal fields (e.g. constr), and not the records
    themselves. But would it really bring substantial gains ? *)

let hcons_rel_decl ((n,oc,t) as d) =
  let n' = Names.Name.hcons n
  and oc' = Option.smartmap Term.hcons_constr oc
  and t' = Term.hcons_types t
  in if n' == n && oc' == oc && t' == t then d else (n',oc',t')

let hcons_rel_context l = List.smartmap hcons_rel_decl l

let hcons_const_type t = Term.hcons_constr t

let hcons_const_def = function
  | Undef inl -> Undef inl
  | Def l_constr ->
    let constr = force_constr l_constr in
    Def (from_val (Term.hcons_constr constr))
  | OpaqueDef _ as x -> x (* hashconsed when turned indirect *)

let hcons_const_body cb =
  { cb with
    const_body = hcons_const_def cb.const_body;
    const_type = hcons_const_type cb.const_type;
    const_universes =
      if Future.is_val cb.const_universes then
        Future.from_val
          (Univ.hcons_universe_context (Future.force cb.const_universes))
      else (* FIXME: Why not? *) cb.const_universes }

(** {6 Inductive types } *)

let eq_recarg r1 r2 = match r1, r2 with
| Norec, Norec -> true
| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
| _ -> false

let subst_recarg sub r = match r with
  | Norec -> r
  | Mrec (kn,i) ->
    let kn' = subst_mind sub kn in
    if kn==kn' then r else Mrec (kn',i)
  | Imbr (kn,i) ->
    let kn' = subst_mind sub kn in
    if kn==kn' then r else Imbr (kn',i)

let mk_norec = Rtree.mk_node Norec [||]

let mk_paths r recargs =
  Rtree.mk_node r
    (Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs)

let dest_recarg p = fst (Rtree.dest_node p)

(* dest_subterms returns the sizes of each argument of each constructor of
   an inductive object of size [p]. This should never be done for Norec,
   because the number of sons does not correspond to the number of
   constructors.
 *)
let dest_subterms p =
  let (ra,cstrs) = Rtree.dest_node p in
  assert (match ra with Norec -> false | _ -> true);
  Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs

let recarg_length p j =
  let (_,cstrs) = Rtree.dest_node p in
  Array.length (snd (Rtree.dest_node cstrs.(j-1)))

let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p

(** {7 Substitution of inductive declarations } *)

(* OLD POLYMORPHISM *)
(* let subst_indarity sub ar = match ar with *)
(*   | Monomorphic s -> *)
(*     let uar' = subst_mps sub s.mind_user_arity in *)
(*     if uar' == s.mind_user_arity then ar *)
(*     else Monomorphic { mind_user_arity = uar'; mind_sort = s.mind_sort } *)
(*   | Polymorphic _ -> ar *)

(* let subst_mind_packet sub mip = *)
(*   let { mind_nf_lc = nf; *)
(*         mind_user_lc = user; *)
(*         mind_arity_ctxt = ctxt; *)
(*         mind_arity = ar; *)
(*         mind_recargs = ra } = mip *)
(*   in *)
(*   let nf' = Array.smartmap (subst_mps sub) nf in *)
(*   let user' = *)
(*     (\* maintain sharing of [mind_user_lc] and [mind_nf_lc] *\) *)
(*     if user==nf then nf' *)
(*     else Array.smartmap (subst_mps sub) user *)
(*   in *)
(*   let ctxt' = subst_rel_context sub ctxt in *)
(*   let ar' = subst_indarity sub ar in *)
(*   let ra' = subst_wf_paths sub ra in *)
(*   if nf==nf' && user==user' && ctxt==ctxt' && ar==ar' && ra==ra' *)
(*   then mip *)
(*   else *)
(*     { mip with *)
(*       mind_nf_lc = nf'; *)
(*       mind_user_lc = user'; *)
(*       mind_arity_ctxt = ctxt'; *)
(*       mind_arity = ar'; *)
(*       mind_recargs = ra' } *)

(* let subst_mind sub mib = *)
(*   assert (List.is_empty mib.mind_hyps); (\* we're outside sections *\) *)
(*   if is_empty_subst sub then mib *)
(*   else *)
(*     let params = mib.mind_params_ctxt in *)
(*     let params' = Context.map_rel_context (subst_mps sub) params in *)
(*     let packets = mib.mind_packets in *)
(*     let packets' = Array.smartmap (subst_mind_packet sub) packets in *)
(*     if params==params' && packets==packets' then mib *)
(*     else *)
(*       { mib with *)
(*         mind_params_ctxt = params'; *)
(*         mind_packets = packets'; *)
(*         mind_native_name = ref NotLinked } *)

(* (\** {6 Hash-consing of inductive declarations } *\) *)

(* (\** Just as for constants, this hash-consing is quite partial *\) *)

(* let hcons_indarity = function *)
(*   | Monomorphic a -> *)
(*     Monomorphic *)
(*       { mind_user_arity = Term.hcons_constr a.mind_user_arity; *)
(*         mind_sort = Term.hcons_sorts a.mind_sort } *)
(*   | Polymorphic a -> Polymorphic (hcons_polyarity a) *)

(** Substitution of inductive declarations *)

let subst_indarity sub s =
  { mind_user_arity = subst_mps sub s.mind_user_arity;
    mind_sort = s.mind_sort;
  }

let subst_mind_packet sub mbp =
  { mind_consnames = mbp.mind_consnames;
    mind_consnrealdecls = mbp.mind_consnrealdecls;
    mind_consnrealargs = mbp.mind_consnrealargs;
    mind_typename = mbp.mind_typename;
    mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
    mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
    mind_arity = subst_indarity sub mbp.mind_arity;
    mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
    mind_nrealargs = mbp.mind_nrealargs;
    mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
    mind_kelim = mbp.mind_kelim;
    mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
    mind_nb_constant = mbp.mind_nb_constant;
    mind_nb_args = mbp.mind_nb_args;
    mind_reloc_tbl = mbp.mind_reloc_tbl }

let subst_mind_body sub mib =
  { mind_record = mib.mind_record ;
    mind_finite = mib.mind_finite ;
    mind_ntypes = mib.mind_ntypes ;
    mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
    mind_nparams = mib.mind_nparams;
    mind_nparams_rec = mib.mind_nparams_rec;
    mind_params_ctxt =
      Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt;
    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
    mind_polymorphic = mib.mind_polymorphic;
    mind_universes = mib.mind_universes }

(** Hash-consing of inductive declarations *)

let hcons_indarity a =
  { mind_user_arity = Term.hcons_constr a.mind_user_arity;
    mind_sort = Term.hcons_sorts a.mind_sort }

let hcons_mind_packet oib =
  let user = Array.smartmap Term.hcons_types oib.mind_user_lc in
  let nf = Array.smartmap Term.hcons_types oib.mind_nf_lc in
  (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *)
  let nf = if Array.equal (==) user nf then user else nf in
  { oib with
    mind_typename = Names.Id.hcons oib.mind_typename;
    mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
    mind_arity = hcons_indarity oib.mind_arity;
    mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames;
    mind_user_lc = user;
    mind_nf_lc = nf }

let hcons_mind mib =
  { mib with
    mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
    mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
    mind_universes = Univ.hcons_universe_context mib.mind_universes }

(** {6 Stm machinery } *)

let join_constant_body cb =
  ignore(Future.join cb.const_universes);
  match cb.const_body with
  | OpaqueDef o -> Opaqueproof.join_opaque o
  | _ -> ()

let string_of_side_effect = function
  | SEsubproof (c,_) -> Names.string_of_con c
  | SEscheme (cl,_) ->
      String.concat ", " (List.map (fun (_,c,_) -> Names.string_of_con c) cl)
type side_effects = side_effect list
let no_seff = ([] : side_effects)
let iter_side_effects f l = List.iter f (List.rev l)
let fold_side_effects f a l = List.fold_left f a l
let uniquize_side_effects l = l (** FIXME: there is something dubious here *)
let union_side_effects l1 l2 = l1 @ l2
let flatten_side_effects l = List.flatten l
let side_effects_of_list l = l
let cons_side_effects x l = x :: l
let side_effects_is_empty = List.is_empty