aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_typing.ml
blob: c7f3e5c51bceca95c9ad024b01a5ef7a8e888486 (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
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
   the Coq module system *)

(* This module provides the main functions for type-checking module
   declarations *)

open Util
open Names
open Declarations
open Entries
open Environ
open Modops
open Mod_subst

type 'alg translation =
  module_signature * 'alg * delta_resolver * Univ.ContextSet.t

let rec mp_from_mexpr = function
  | MEident mp -> mp
  | MEapply (expr,_) -> mp_from_mexpr expr
  | MEwith (expr,_) -> mp_from_mexpr expr

let is_modular = function
  | SFBmodule _ | SFBmodtype _ -> true
  | SFBconst _ | SFBmind _ -> false

(** Split a [structure_body] at some label corresponding to
    a modular definition or not. *)

let split_struc k m struc =
  let rec split rev_before = function
    | [] -> raise Not_found
    | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) ->
      List.rev rev_before,b,after
    | h::tail -> split (h::rev_before) tail
  in split [] struc

let discr_resolver mtb = match mtb.mod_type with
  | NoFunctor _ -> mtb.mod_delta
  | MoreFunctor _ -> empty_delta_resolver

let rec rebuild_mp mp l =
  match l with
  | []-> mp
  | i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r

let (+++) = Univ.ContextSet.union

let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
  let lab,idl = match idl with
    | [] -> assert false
    | id::idl -> Label.of_id id, idl
  in
  try
    let modular = not (List.is_empty idl) in
    let before,spec,after = split_struc lab modular struc in
    let env' = Modops.add_structure mp before equiv env in
    if List.is_empty idl then
      (* Toplevel definition *)
      let cb = match spec with
	| SFBconst cb -> cb
	| _ -> error_not_a_constant lab
      in
      (* In the spirit of subtyping.check_constant, we accept
         any implementations of parameters and opaques terms,
	 as long as they have the right type *)
      let c', univs, ctx' =
        match cb.const_universes with
        | Monomorphic_const _ ->
          (** We do not add the deferred constraints of the body in the
              environment, because they do not appear in the type of the
              definition. Any inconsistency will be raised at a later stage
              when joining the environment. *)
	  let env' = Environ.push_context ~strict:true ctx env' in
	  let c',cst = match cb.const_body with
	    | Undef _ | OpaqueDef _ ->
	      let j = Typeops.infer env' c in
	      let typ = Typeops.type_of_constant_type env' cb.const_type in
	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
						j.uj_type typ in
	      j.uj_val, cst'
	    | Def cs ->
	       let c' = Mod_subst.force_constr cs in
	         c, Reduction.infer_conv env' (Environ.universes env') c c'
	  in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
        | Polymorphic_const uctx ->
          let subst, ctx = Univ.abstract_universes ctx in
          let c = Vars.subst_univs_level_constr subst c in
          let () =
            if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
              error_incorrect_with_constraint lab
          in
          (** Terms are compared in a context with De Bruijn universe indices *)
	  let env' = Environ.push_context ~strict:false (Univ.AUContext.repr uctx) env in
	  let cst = match cb.const_body with
	    | Undef _ | OpaqueDef _ ->
	      let j = Typeops.infer env' c in
	      let typ = Typeops.type_of_constant_type env' cb.const_type in
	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
						j.uj_type typ in
	      cst'
	    | Def cs ->
	       let c' = Mod_subst.force_constr cs in
	       let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
	        cst'
	  in
	    if not (Univ.Constraint.is_empty cst) then
	      error_incorrect_with_constraint lab;
            c, Polymorphic_const ctx, Univ.ContextSet.empty
      in
      let def = Def (Mod_subst.from_val c') in
(*      let ctx' = Univ.UContext.make (newus, cst) in *)
      let cb' =
	{ cb with
	  const_body = def;
          const_universes = univs ;
	  const_body_code = Option.map Cemitcodes.from_val
                              (compile_constant_body env' cb.const_universes def) }
      in
      before@(lab,SFBconst(cb'))::after, c', ctx'
    else
      (* Definition inside a sub-module *)
      let mb = match spec with
	| SFBmodule mb -> mb
	| _ -> error_not_a_module (Label.to_string lab)
      in
      begin match mb.mod_expr with
      | Abstract ->
        let struc = Modops.destr_nofunctor mb.mod_type in
        let struc',c',cst =
          check_with_def env' struc (idl,(c,ctx)) (MPdot(mp,lab)) mb.mod_delta
        in
        let mb' = { mb with
          mod_type = NoFunctor struc';
	  mod_type_alg = None }
        in
	before@(lab,SFBmodule mb')::after, c', cst
      | _ -> error_generative_module_expected lab
      end
  with
  | Not_found -> error_no_such_label lab
  | Reduction.NotConvertible -> error_incorrect_with_constraint lab

let rec check_with_mod env struc (idl,mp1) mp equiv =
  let lab,idl = match idl with
    | [] -> assert false
    | id::idl -> Label.of_id id, idl
  in
  try
    let before,spec,after = split_struc lab true struc in
    let env' = Modops.add_structure mp before equiv env in
    let old = match spec with
      | SFBmodule mb -> mb
      | _ -> error_not_a_module (Label.to_string lab)
    in
    if List.is_empty idl then
      (* Toplevel module definition *)
      let mb_mp1 = lookup_module mp1 env in
      let mtb_mp1 = module_type_of_module mb_mp1 in
      let cst = match old.mod_expr with
	| Abstract ->
	  begin
            try
              let mtb_old = module_type_of_module old in
              let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
              Univ.ContextSet.add_constraints chk_cst old.mod_constraints
	    with Failure _ ->
              (* TODO: where can a Failure come from ??? *)
              error_incorrect_with_constraint lab
	  end
	| Algebraic (NoFunctor (MEident(mp'))) ->
	  check_modpath_equiv env' mp1 mp';
	  old.mod_constraints
	| _ -> error_generative_module_expected lab
      in
      let mp' = MPdot (mp,lab) in
      let new_mb = strengthen_and_subst_mb mb_mp1 mp' false in
      let new_mb' =
        { new_mb with
          mod_mp = mp';
          mod_expr = Algebraic (NoFunctor (MEident mp1));
          mod_constraints = cst }
      in
      let new_equiv = add_delta_resolver equiv new_mb.mod_delta in
      (* we propagate the new equality in the rest of the signature
	 with the identity substitution accompagned by the new resolver*)
      let id_subst = map_mp mp' mp' new_mb.mod_delta in
      let new_after = subst_structure id_subst after in
      before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst
    else
      (* Module definition of a sub-module *)
      let mp' = MPdot (mp,lab) in
      let old = match spec with
        | SFBmodule msb -> msb
	| _ -> error_not_a_module (Label.to_string lab)
      in
      begin match old.mod_expr with
      | Abstract ->
        let struc = destr_nofunctor old.mod_type in
	let struc',equiv',cst =
          check_with_mod env' struc (idl,mp1) mp' old.mod_delta
        in
	let new_mb =
          { old with
            mod_type = NoFunctor struc';
            mod_type_alg = None;
            mod_delta = equiv' }
        in
	let new_equiv = add_delta_resolver equiv equiv' in
	let id_subst = map_mp mp' mp' equiv' in
        let new_after = subst_structure id_subst after in
	before@(lab,SFBmodule new_mb)::new_after, new_equiv, cst
      | Algebraic (NoFunctor (MEident mp0)) ->
	let mpnew = rebuild_mp mp0 idl in
	check_modpath_equiv env' mpnew mp;
	before@(lab,spec)::after, equiv, Univ.ContextSet.empty
      | _ -> error_generative_module_expected lab
      end
  with
  | Not_found -> error_no_such_label lab
  | Reduction.NotConvertible -> error_incorrect_with_constraint lab

let check_with env mp (sign,alg,reso,cst) = function
  |WithDef(idl,c) ->
    let struc = destr_nofunctor sign in
    let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
    let wd' = WithDef (idl,(c',Univ.ContextSet.to_context cst')) in
    NoFunctor struc', MEwith (alg,wd'), reso, cst+++cst'
  |WithMod(idl,mp1) as wd ->
    let struc = destr_nofunctor sign in
    let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
    NoFunctor struc', MEwith (alg,wd), reso', cst+++cst'

let translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
  let farg_id, farg_b, fbody_b = destr_functor sign in
  let mtb = module_type_of_module (lookup_module mp1 env) in
  let cst2 = Subtyping.check_subtypes env mtb farg_b in
  let mp_delta = discr_resolver mtb in
  let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
  let subst = map_mbid farg_id mp1 mp_delta in
  let body = subst_signature subst fbody_b in
  let alg' = mkalg alg mp1 in
  let reso' = subst_codom_delta_resolver subst reso in
  body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1

(** Translation of a module struct entry :
    - We translate to a module when a [module_path] is given,
      otherwise to a module type.
    - The first output is the expanded signature
    - The second output is the algebraic expression, kept for the extraction.
*)

let mk_alg_app alg arg = MEapply (alg,arg)

let rec translate_mse env mpo inl = function
  |MEident mp1 as me ->
    let mb = match mpo with
      |Some mp -> strengthen_and_subst_mb (lookup_module mp1 env) mp false
      |None -> lookup_modtype mp1 env
    in
    mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty
  |MEapply (fe,mp1) ->
    translate_apply env inl (translate_mse env mpo inl fe) mp1 mk_alg_app
  |MEwith(me, with_decl) ->
    assert (mpo == None); (* No 'with' syntax for modules *)
    let mp = mp_from_mexpr me in
    check_with env mp (translate_mse env None inl me) with_decl

let mk_mod mp e ty cst reso =
  { mod_mp = mp;
    mod_expr = e;
    mod_type = ty;
    mod_type_alg = None;
    mod_constraints = cst;
    mod_delta = reso;
    mod_retroknowledge = [] }

let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso

let rec translate_mse_funct env mpo inl mse = function
  |[] ->
    let sign,alg,reso,cst = translate_mse env mpo inl mse in
    sign, NoFunctor alg, reso, cst
  |(mbid, ty) :: params ->
    let mp_id = MPbound mbid in
    let mtb = translate_modtype env mp_id inl ([],ty) in
    let env' = add_module_type mp_id mtb env in
    let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
    let alg' = MoreFunctor (mbid,mtb,alg) in
    MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_constraints

and translate_modtype env mp inl (params,mte) =
  let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
  let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in
  let mtb' = subst_modtype_and_resolver mtb mp in
  { mtb' with mod_type_alg = Some alg }

(** [finalize_module] :
    from an already-translated (or interactive) implementation and
    an (optional) signature entry, produces a final [module_body] *)

let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
  |None ->
    let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
    mk_mod mp impl sign cst reso
  |Some (params_mte,inl) ->
    let res_mtb = translate_modtype env mp inl params_mte in
    let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
    let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
    let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
    { res_mtb with
      mod_mp = mp;
      mod_expr = impl;
      (** cst from module body typing,
          cst' from subtyping,
          constraints from module type. *)
      mod_constraints =
        Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }

let translate_module env mp inl = function
  |MType (params,ty) ->
    let mtb = translate_modtype env mp inl (params,ty) in
    module_body_of_type mp mtb
  |MExpr (params,mse,oty) ->
    let (sg,alg,reso,cst) = translate_mse_funct env (Some mp) inl mse params in
    let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
    finalize_module env mp (sg,Some alg,reso,cst) restype

(** We now forbid any Include of functors with restricted signatures.
    Otherwise, we could end with the creation of undesired axioms
    (see #3746). Note that restricted non-functorized modules are ok,
    thanks to strengthening. *)

let rec unfunct = function
  |NoFunctor me -> me
  |MoreFunctor(_,_,me) -> unfunct me

let rec forbid_incl_signed_functor env = function
  |MEapply(fe,_) -> forbid_incl_signed_functor env fe
  |MEwith _ -> assert false (* No 'with' syntax for modules *)
  |MEident mp1 ->
    let mb = lookup_module mp1 env in
    match mb.mod_type, mb.mod_type_alg, mb.mod_expr with
    |MoreFunctor _, Some _, _ ->
      (* functor + restricted signature = error *)
      error_include_restricted_functor mp1
    |MoreFunctor _, None, Algebraic me ->
      (* functor, no signature yet, a definition which may be restricted *)
      forbid_incl_signed_functor env (unfunct me)
    |_ -> ()

let rec translate_mse_inclmod env mp inl = function
  |MEident mp1 ->
    let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
    let sign = clean_bounded_mod_expr mb.mod_type in
    sign,(),mb.mod_delta,Univ.ContextSet.empty
  |MEapply (fe,arg) ->
    let ftrans = translate_mse_inclmod env mp inl fe in
    translate_apply env inl ftrans arg (fun _ _ -> ())
  |MEwith _ -> assert false (* No 'with' syntax for modules *)

let translate_mse_incl is_mod env mp inl me =
  if is_mod then
    let () = forbid_incl_signed_functor env me in
    translate_mse_inclmod env mp inl me
  else
    let mtb = translate_modtype env mp inl ([],me) in
    let sign = clean_bounded_mod_expr mtb.mod_type in
    sign,(),mtb.mod_delta,mtb.mod_constraints