aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_typing.ml
blob: 7794f19be0d176e9b7f619881fb36174afb322d4 (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
(************************************************************************)
(*  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 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 option * delta_resolver * Univ.constraints

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.typ_expr with
  | NoFunctor _ -> mtb.typ_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.union_constraints

let rec check_with_def env struc (idl,c) 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',cst = match cb.const_body with
	| Undef _ | OpaqueDef _ ->
	  let j,cst1 = Typeops.infer env' c in
	  let typ = Typeops.type_of_constant_type env' cb.const_type in
	  let cst2 = Reduction.conv_leq env' j.uj_type typ in
	  let cst = Future.force cb.const_constraints +++ cst1 +++ cst2 in
	  j.uj_val,cst
	| Def cs ->
	  let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
	  let cst = Future.force cb.const_constraints +++ cst1 in
          c, cst
      in
      let def = Def (Lazyconstr.from_val c') in
      let cb' =
	{ cb with
	  const_body = def;
	  const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
	  const_constraints = Future.from_val cst }
      in
      before@(lab,SFBconst(cb'))::after, c', cst
    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) (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
              Subtyping.check_subtypes env' mtb_mp1 mtb_old
                +++ old.mod_constraints
	    with Failure _ -> 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.empty_constraint
      | _ -> error_generative_module_expected lab
      end
  with
  | Not_found -> error_no_such_label lab
  | Reduction.NotConvertible -> error_incorrect_with_constraint lab

let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg

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 alg' = mk_alg_with alg (WithDef (idl,c')) in
    (NoFunctor struc'),alg',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
    let alg' = mk_alg_with alg wd in
    (NoFunctor struc'),alg',reso', cst+++cst'

let mk_alg_app mpo alg arg = match mpo, alg with
  | Some _, Some alg -> Some (MEapply (alg,arg))
  | _ -> None

(** 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.
      It is never None when translating to a module, but for module type
      it could not be contain [SEBapply] or [SEBfunctor].
*)

let rec translate_mse env mpo inl = function
  |MEident mp1 ->
    let sign,reso = match mpo with
      |Some mp ->
        let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in
        mb.mod_type, mb.mod_delta
      |None ->
        let mtb = lookup_modtype mp1 env in
        mtb.typ_expr, mtb.typ_delta
    in
    sign,Some (MEident mp1),reso,Univ.empty_constraint
  |MEapply (fe,mp1) ->
    translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
  |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

and 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', cst1 +++ cst2

let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
  | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
  | _ -> None

let rec translate_mse_funct env mpo inl mse = function
  |[] ->
    let sign,alg,reso,cst = translate_mse env mpo inl mse in
    sign, Option.map (fun a -> NoFunctor a) 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' = mk_alg_funct mpo mbid mtb alg in
    MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.typ_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 =
    { typ_mp = mp_from_mexpr mte;
      typ_expr = sign;
      typ_expr_alg = None;
      typ_constraints = cst;
      typ_delta = reso }
  in
  let mtb' = subst_modtype_and_resolver mtb mp in
  { mtb' with typ_expr_alg = alg }

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

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
    { mod_mp = mp;
      mod_expr = impl;
      mod_type = sign;
      mod_type_alg = None;
      mod_constraints = cst;
      mod_delta = reso;
      mod_retroknowledge = [] }
  |Some (params_mte,inl) ->
    let res_mtb = translate_modtype env mp inl params_mte in
    let auto_mtb = {
      typ_mp = mp;
      typ_expr = sign;
      typ_expr_alg = None;
      typ_constraints = Univ.empty_constraint;
      typ_delta = 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
    { mod_mp = mp;
      mod_expr = impl;
      mod_type = res_mtb.typ_expr;
      mod_type_alg = res_mtb.typ_expr_alg;
      mod_constraints = cst +++ cst';
      mod_delta = res_mtb.typ_delta;
      mod_retroknowledge = [] }

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 t = 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 t restype

let rec translate_mse_incl 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,None,mb.mod_delta,Univ.empty_constraint
  |MEapply (fe,arg) ->
    let ftrans = translate_mse_incl env mp inl fe in
    translate_apply env inl ftrans arg (fun _ _ -> None)
  |_ -> Modops.error_higher_order_include ()