l4/pkg/ocaml/contrib/typing/includemod.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                           Objective Caml                            *)
   4 (*                                                                     *)
   5 (*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
   6 (*                                                                     *)
   7 (*  Copyright 1996 Institut National de Recherche en Informatique et   *)
   8 (*  en Automatique.  All rights reserved.  This file is distributed    *)
   9 (*  under the terms of the Q Public License version 1.0.               *)
  10 (*                                                                     *)
  11 (***********************************************************************)
  12
  13 (* $Id: includemod.ml 8768 2008-01-11 16:13:18Z doligez $ *)
  14
  15 (* Inclusion checks for the module language *)
  16
  17 open Misc
  18 open Path
  19 open Types
  20 open Typedtree
  21
  22 type error =
  23     Missing_field of Ident.t
  24   | Value_descriptions of Ident.t * value_description * value_description
  25   | Type_declarations of Ident.t * type_declaration * type_declaration
  26   | Exception_declarations of
  27       Ident.t * exception_declaration * exception_declaration
  28   | Module_types of module_type * module_type
  29   | Modtype_infos of Ident.t * modtype_declaration * modtype_declaration
  30   | Modtype_permutation
  31   | Interface_mismatch of string * string
  32   | Class_type_declarations of
  33       Ident.t * cltype_declaration * cltype_declaration *
  34       Ctype.class_match_failure list
  35   | Class_declarations of
  36       Ident.t * class_declaration * class_declaration *
  37       Ctype.class_match_failure list
  38   | Unbound_modtype_path of Path.t
  39
  40 exception Error of error list
  41
  42 (* All functions "blah env x1 x2" check that x1 is included in x2,
  43    i.e. that x1 is the type of an implementation that fulfills the
  44    specification x2. If not, Error is raised with a backtrace of the error. *)
  45
  46 (* Inclusion between value descriptions *)
  47
  48 let value_descriptions env subst id vd1 vd2 =
  49   let vd2 = Subst.value_description subst vd2 in
  50   try
  51     Includecore.value_descriptions env vd1 vd2
  52   with Includecore.Dont_match ->
  53     raise(Error[Value_descriptions(id, vd1, vd2)])
  54
  55 (* Inclusion between type declarations *)
  56
  57 let type_declarations env subst id decl1 decl2 =
  58   let decl2 = Subst.type_declaration subst decl2 in
  59   if Includecore.type_declarations env id decl1 decl2
  60   then ()
  61   else raise(Error[Type_declarations(id, decl1, decl2)])
  62
  63 (* Inclusion between exception declarations *)
  64
  65 let exception_declarations env subst id decl1 decl2 =
  66   let decl2 = Subst.exception_declaration subst decl2 in
  67   if Includecore.exception_declarations env decl1 decl2
  68   then ()
  69   else raise(Error[Exception_declarations(id, decl1, decl2)])
  70
  71 (* Inclusion between class declarations *)
  72
  73 let class_type_declarations env subst id decl1 decl2 =
  74   let decl2 = Subst.cltype_declaration subst decl2 in
  75   match Includeclass.class_type_declarations env decl1 decl2 with
  76     []     -> ()
  77   | reason -> raise(Error[Class_type_declarations(id, decl1, decl2, reason)])
  78
  79 let class_declarations env subst id decl1 decl2 =
  80   let decl2 = Subst.class_declaration subst decl2 in
  81   match Includeclass.class_declarations env decl1 decl2 with
  82     []     -> ()
  83   | reason -> raise(Error[Class_declarations(id, decl1, decl2, reason)])
  84
  85 (* Expand a module type identifier when possible *)
  86
  87 exception Dont_match
  88
  89 let expand_module_path env path =
  90   try
  91     Env.find_modtype_expansion path env
  92   with Not_found ->
  93     raise(Error[Unbound_modtype_path path])
  94
  95 (* Extract name, kind and ident from a signature item *)
  96
  97 type field_desc =
  98     Field_value of string
  99   | Field_type of string
 100   | Field_exception of string
 101   | Field_module of string
 102   | Field_modtype of string
 103   | Field_class of string
 104   | Field_classtype of string
 105
 106 let item_ident_name = function
 107     Tsig_value(id, _) -> (id, Field_value(Ident.name id))
 108   | Tsig_type(id, _, _) -> (id, Field_type(Ident.name id))
 109   | Tsig_exception(id, _) -> (id, Field_exception(Ident.name id))
 110   | Tsig_module(id, _, _) -> (id, Field_module(Ident.name id))
 111   | Tsig_modtype(id, _) -> (id, Field_modtype(Ident.name id))
 112   | Tsig_class(id, _, _) -> (id, Field_class(Ident.name id))
 113   | Tsig_cltype(id, _, _) -> (id, Field_classtype(Ident.name id))
 114
 115 (* Simplify a structure coercion *)
 116
 117 let simplify_structure_coercion cc =
 118   let rec is_identity_coercion pos = function
 119   | [] ->
 120       true
 121   | (n, c) :: rem ->
 122       n = pos && c = Tcoerce_none && is_identity_coercion (pos + 1) rem in
 123   if is_identity_coercion 0 cc
 124   then Tcoerce_none
 125   else Tcoerce_structure cc
 126
 127 (* Inclusion between module types.
 128    Return the restriction that transforms a value of the smaller type
 129    into a value of the bigger type. *)
 130
 131 let rec modtypes env subst mty1 mty2 =
 132   try
 133     try_modtypes env subst mty1 mty2
 134   with
 135     Dont_match ->
 136       raise(Error[Module_types(mty1, Subst.modtype subst mty2)])
 137   | Error reasons ->
 138       raise(Error(Module_types(mty1, Subst.modtype subst mty2) :: reasons))
 139
 140 and try_modtypes env subst mty1 mty2 =
 141   match (mty1, mty2) with
 142     (_, Tmty_ident p2) ->
 143       try_modtypes2 env mty1 (Subst.modtype subst mty2)
 144   | (Tmty_ident p1, _) ->
 145       try_modtypes env subst (expand_module_path env p1) mty2
 146   | (Tmty_signature sig1, Tmty_signature sig2) ->
 147       signatures env subst sig1 sig2
 148   | (Tmty_functor(param1, arg1, res1), Tmty_functor(param2, arg2, res2)) ->
 149       let arg2' = Subst.modtype subst arg2 in
 150       let cc_arg = modtypes env Subst.identity arg2' arg1 in
 151       let cc_res =
 152         modtypes (Env.add_module param1 arg2' env)
 153           (Subst.add_module param2 (Pident param1) subst) res1 res2 in
 154       begin match (cc_arg, cc_res) with
 155           (Tcoerce_none, Tcoerce_none) -> Tcoerce_none
 156         | _ -> Tcoerce_functor(cc_arg, cc_res)
 157       end
 158   | (_, _) ->
 159       raise Dont_match
 160
 161 and try_modtypes2 env mty1 mty2 =
 162   (* mty2 is an identifier *)
 163   match (mty1, mty2) with
 164     (Tmty_ident p1, Tmty_ident p2) when Path.same p1 p2 ->
 165       Tcoerce_none
 166   | (_, Tmty_ident p2) ->
 167       try_modtypes env Subst.identity mty1 (expand_module_path env p2)
 168   | (_, _) ->
 169       assert false
 170
 171 (* Inclusion between signatures *)
 172
 173 and signatures env subst sig1 sig2 =
 174   (* Environment used to check inclusion of components *)
 175   let new_env =
 176     Env.add_signature sig1 env in
 177   (* Build a table of the components of sig1, along with their positions.
 178      The table is indexed by kind and name of component *)
 179   let rec build_component_table pos tbl = function
 180       [] -> tbl
 181     | item :: rem ->
 182         let (id, name) = item_ident_name item in
 183         let nextpos =
 184           match item with
 185             Tsig_value(_,{val_kind = Val_prim _})
 186           | Tsig_type(_,_,_)
 187           | Tsig_modtype(_,_)
 188           | Tsig_cltype(_,_,_) -> pos
 189           | Tsig_value(_,_)
 190           | Tsig_exception(_,_)
 191           | Tsig_module(_,_,_)
 192           | Tsig_class(_, _,_) -> pos+1 in
 193         build_component_table nextpos
 194                               (Tbl.add name (id, item, pos) tbl) rem in
 195   let comps1 =
 196     build_component_table 0 Tbl.empty sig1 in
 197   (* Pair each component of sig2 with a component of sig1,
 198      identifying the names along the way.
 199      Return a coercion list indicating, for all run-time components
 200      of sig2, the position of the matching run-time components of sig1
 201      and the coercion to be applied to it. *)
 202   let rec pair_components subst paired unpaired = function
 203       [] ->
 204         begin match unpaired with
 205             [] -> signature_components new_env subst (List.rev paired)
 206           | _  -> raise(Error unpaired)
 207         end
 208     | item2 :: rem ->
 209         let (id2, name2) = item_ident_name item2 in
 210         let name2, report =
 211           match item2, name2 with
 212             Tsig_type (_, {type_manifest=None}, _), Field_type s
 213             when let l = String.length s in
 214             l >= 4 && String.sub s (l-4) 4 = "#row" ->
 215               (* Do not report in case of failure,
 216                  as the main type will generate an error *)
 217               Field_type (String.sub s 0 (String.length s - 4)), false
 218           | _ -> name2, true
 219         in
 220         begin try
 221           let (id1, item1, pos1) = Tbl.find name2 comps1 in
 222           let new_subst =
 223             match item2 with
 224               Tsig_type _ ->
 225                 Subst.add_type id2 (Pident id1) subst
 226             | Tsig_module _ ->
 227                 Subst.add_module id2 (Pident id1) subst
 228             | Tsig_modtype _ ->
 229                 Subst.add_modtype id2 (Tmty_ident (Pident id1)) subst
 230             | Tsig_value _ | Tsig_exception _ | Tsig_class _ | Tsig_cltype _ ->
 231                 subst
 232           in
 233           pair_components new_subst
 234             ((item1, item2, pos1) :: paired) unpaired rem
 235         with Not_found ->
 236           let unpaired =
 237             if report then Missing_field id2 :: unpaired else unpaired in
 238           pair_components subst paired unpaired rem
 239         end in
 240   (* Do the pairing and checking, and return the final coercion *)
 241   simplify_structure_coercion (pair_components subst [] [] sig2)
 242
 243 (* Inclusion between signature components *)
 244
 245 and signature_components env subst = function
 246     [] -> []
 247   | (Tsig_value(id1, valdecl1), Tsig_value(id2, valdecl2), pos) :: rem ->
 248       let cc = value_descriptions env subst id1 valdecl1 valdecl2 in
 249       begin match valdecl2.val_kind with
 250         Val_prim p -> signature_components env subst rem
 251       | _ -> (pos, cc) :: signature_components env subst rem
 252       end
 253   | (Tsig_type(id1, tydecl1, _), Tsig_type(id2, tydecl2, _), pos) :: rem ->
 254       type_declarations env subst id1 tydecl1 tydecl2;
 255       signature_components env subst rem
 256   | (Tsig_exception(id1, excdecl1), Tsig_exception(id2, excdecl2), pos)
 257     :: rem ->
 258       exception_declarations env subst id1 excdecl1 excdecl2;
 259       (pos, Tcoerce_none) :: signature_components env subst rem
 260   | (Tsig_module(id1, mty1, _), Tsig_module(id2, mty2, _), pos) :: rem ->
 261       let cc =
 262         modtypes env subst (Mtype.strengthen env mty1 (Pident id1)) mty2 in
 263       (pos, cc) :: signature_components env subst rem
 264   | (Tsig_modtype(id1, info1), Tsig_modtype(id2, info2), pos) :: rem ->
 265       modtype_infos env subst id1 info1 info2;
 266       signature_components env subst rem
 267   | (Tsig_class(id1, decl1, _), Tsig_class(id2, decl2, _), pos) :: rem ->
 268       class_declarations env subst id1 decl1 decl2;
 269       (pos, Tcoerce_none) :: signature_components env subst rem
 270   | (Tsig_cltype(id1, info1, _), Tsig_cltype(id2, info2, _), pos) :: rem ->
 271       class_type_declarations env subst id1 info1 info2;
 272       signature_components env subst rem
 273   | _ ->
 274       assert false
 275
 276 (* Inclusion between module type specifications *)
 277
 278 and modtype_infos env subst id info1 info2 =
 279   let info2 = Subst.modtype_declaration subst info2 in
 280   try
 281     match (info1, info2) with
 282       (Tmodtype_abstract, Tmodtype_abstract) -> ()
 283     | (Tmodtype_manifest mty1, Tmodtype_abstract) -> ()
 284     | (Tmodtype_manifest mty1, Tmodtype_manifest mty2) ->
 285         check_modtype_equiv env mty1 mty2
 286     | (Tmodtype_abstract, Tmodtype_manifest mty2) ->
 287         check_modtype_equiv env (Tmty_ident(Pident id)) mty2
 288   with Error reasons ->
 289     raise(Error(Modtype_infos(id, info1, info2) :: reasons))
 290
 291 and check_modtype_equiv env mty1 mty2 =
 292   match
 293     (modtypes env Subst.identity mty1 mty2,
 294      modtypes env Subst.identity mty2 mty1)
 295   with
 296     (Tcoerce_none, Tcoerce_none) -> ()
 297   | (_, _) -> raise(Error [Modtype_permutation])
 298
 299 (* Simplified inclusion check between module types (for Env) *)
 300
 301 let check_modtype_inclusion env mty1 path1 mty2 =
 302   try
 303     ignore(modtypes env Subst.identity
 304                     (Mtype.strengthen env mty1 path1) mty2)
 305   with Error reasons ->
 306     raise Not_found
 307
 308 let _ = Env.check_modtype_inclusion := check_modtype_inclusion
 309
 310 (* Check that an implementation of a compilation unit meets its
 311    interface. *)
 312
 313 let compunit impl_name impl_sig intf_name intf_sig =
 314   try
 315     signatures Env.initial Subst.identity impl_sig intf_sig
 316   with Error reasons ->
 317     raise(Error(Interface_mismatch(impl_name, intf_name) :: reasons))
 318
 319 (* Hide the substitution parameter to the outside world *)
 320
 321 let modtypes env mty1 mty2 = modtypes env Subst.identity mty1 mty2
 322 let signatures env sig1 sig2 = signatures env Subst.identity sig1 sig2
 323 let type_declarations env id decl1 decl2 =
 324   type_declarations env Subst.identity id decl1 decl2
 325
 326 (* Error report *)
 327
 328 open Format
 329 open Printtyp
 330
 331 let include_err ppf = function
 332   | Missing_field id ->
 333       fprintf ppf "The field `%a' is required but not provided" ident id
 334   | Value_descriptions(id, d1, d2) ->
 335       fprintf ppf
 336        "@[<hv 2>Values do not match:@ \
 337         %a@;<1 -2>is not included in@ %a@]"
 338        (value_description id) d1 (value_description id) d2
 339   | Type_declarations(id, d1, d2) ->
 340       fprintf ppf
 341        "@[<hv 2>Type declarations do not match:@ \
 342         %a@;<1 -2>is not included in@ %a@]"
 343        (type_declaration id) d1
 344        (type_declaration id) d2
 345   | Exception_declarations(id, d1, d2) ->
 346       fprintf ppf
 347        "@[<hv 2>Exception declarations do not match:@ \
 348         %a@;<1 -2>is not included in@ %a@]"
 349       (exception_declaration id) d1
 350       (exception_declaration id) d2
 351   | Module_types(mty1, mty2)->
 352       fprintf ppf
 353        "@[<hv 2>Modules do not match:@ \
 354         %a@;<1 -2>is not included in@ %a@]"
 355       modtype mty1
 356       modtype mty2
 357   | Modtype_infos(id, d1, d2) ->
 358       fprintf ppf
 359        "@[<hv 2>Module type declarations do not match:@ \
 360         %a@;<1 -2>does not match@ %a@]"
 361       (modtype_declaration id) d1
 362       (modtype_declaration id) d2
 363   | Modtype_permutation ->
 364       fprintf ppf "Illegal permutation of structure fields"
 365   | Interface_mismatch(impl_name, intf_name) ->
 366       fprintf ppf "@[The implementation %s@ does not match the interface %s:"
 367        impl_name intf_name
 368   | Class_type_declarations(id, d1, d2, reason) ->
 369       fprintf ppf
 370        "@[<hv 2>Class type declarations do not match:@ \
 371         %a@;<1 -2>does not match@ %a@]@ %a"
 372       (Printtyp.cltype_declaration id) d1
 373       (Printtyp.cltype_declaration id) d2
 374       Includeclass.report_error reason
 375   | Class_declarations(id, d1, d2, reason) ->
 376       fprintf ppf
 377        "@[<hv 2>Class declarations do not match:@ \
 378         %a@;<1 -2>does not match@ %a@]@ %a"
 379       (Printtyp.class_declaration id) d1
 380       (Printtyp.class_declaration id) d2
 381       Includeclass.report_error reason
 382   | Unbound_modtype_path path ->
 383       fprintf ppf "Unbound module type %a" Printtyp.path path
 384
 385 let report_error ppf = function
 386   |  [] -> ()
 387   | err :: errs ->
 388       let print_errs ppf errs =
 389          List.iter (fun err -> fprintf ppf "@ %a" include_err err) errs in
 390       fprintf ppf "@[<v>%a%a@]" include_err err print_errs errs