typing/includecore.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$ *)
  14
  15 (* Inclusion checks for the core language *)
  16
  17 open Misc
  18 open Asttypes
  19 open Path
  20 open Types
  21 open Typedtree
  22
  23 (* Inclusion between value descriptions *)
  24
  25 exception Dont_match
  26
  27 let value_descriptions env vd1 vd2 =
  28   if Ctype.moregeneral env true vd1.val_type vd2.val_type then begin
  29     match (vd1.val_kind, vd2.val_kind) with
  30         (Val_prim p1, Val_prim p2) ->
  31           if p1 = p2 then Tcoerce_none else raise Dont_match
  32       | (Val_prim p, _) -> Tcoerce_primitive p
  33       | (_, Val_prim p) -> raise Dont_match
  34       | (_, _) -> Tcoerce_none
  35   end else
  36     raise Dont_match
  37
  38 (* Inclusion between "private" annotations *)
  39
  40 let private_flags priv1 priv2 =
  41   match (priv1, priv2) with (Private, Public) -> false | (_, _) -> true
  42
  43 (* Inclusion between manifest types (particularly for private row types) *)
  44
  45 let is_absrow env ty =
  46   match ty.desc with
  47     Tconstr(Pident id, _, _) ->
  48       begin match Ctype.expand_head env ty with
  49         {desc=Tobject _|Tvariant _} -> true
  50       | _ -> false
  51       end
  52   | _ -> false
  53
  54 let type_manifest env ty1 params1 ty2 params2 =
  55   let ty1' = Ctype.expand_head env ty1 and ty2' = Ctype.expand_head env ty2 in
  56   match ty1'.desc, ty2'.desc with
  57     Tvariant row1, Tvariant row2 when is_absrow env (Btype.row_more row2) ->
  58       let row1 = Btype.row_repr row1 and row2 = Btype.row_repr row2 in
  59       Ctype.equal env true (ty1::params1) (row2.row_more::params2) &&
  60       (match row1.row_more with {desc=Tvar|Tconstr _} -> true | _ -> false) &&
  61       let r1, r2, pairs =
  62         Ctype.merge_row_fields row1.row_fields row2.row_fields in
  63       (not row2.row_closed ||
  64        row1.row_closed && Ctype.filter_row_fields false r1 = []) &&
  65       List.for_all
  66         (fun (_,f) -> match Btype.row_field_repr f with
  67           Rabsent | Reither _ -> true | Rpresent _ -> false)
  68         r2 &&
  69       let to_equal = ref (List.combine params1 params2) in
  70       List.for_all
  71         (fun (_, f1, f2) ->
  72           match Btype.row_field_repr f1, Btype.row_field_repr f2 with
  73             Rpresent(Some t1),
  74             (Rpresent(Some t2) | Reither(false, [t2], _, _)) ->
  75               to_equal := (t1,t2) :: !to_equal; true
  76           | Rpresent None, (Rpresent None | Reither(true, [], _, _)) -> true
  77           | Reither(c1,tl1,_,_), Reither(c2,tl2,_,_)
  78             when List.length tl1 = List.length tl2 && c1 = c2 ->
  79               to_equal := List.combine tl1 tl2 @ !to_equal; true
  80           | Rabsent, (Reither _ | Rabsent) -> true
  81           | _ -> false)
  82         pairs &&
  83       let tl1, tl2 = List.split !to_equal in
  84       Ctype.equal env true tl1 tl2
  85   | Tobject (fi1, _), Tobject (fi2, _)
  86     when is_absrow env (snd(Ctype.flatten_fields fi2)) ->
  87       let (fields2,rest2) = Ctype.flatten_fields fi2 in
  88       Ctype.equal env true (ty1::params1) (rest2::params2) &&
  89       let (fields1,rest1) = Ctype.flatten_fields fi1 in
  90       (match rest1 with {desc=Tnil|Tvar|Tconstr _} -> true | _ -> false) &&
  91       let pairs, miss1, miss2 = Ctype.associate_fields fields1 fields2 in
  92       miss2 = [] &&
  93       let tl1, tl2 =
  94         List.split (List.map (fun (_,_,t1,_,t2) -> t1, t2) pairs) in
  95       Ctype.equal env true (params1 @ tl1) (params2 @ tl2)
  96   | _ ->
  97       Ctype.equal env true (ty1 :: params1) (ty2 :: params2)
  98
  99 (* Inclusion between type declarations *)
 100
 101 let type_declarations env id decl1 decl2 =
 102   decl1.type_arity = decl2.type_arity &&
 103   begin match (decl1.type_kind, decl2.type_kind) with
 104       (_, Type_abstract) -> true
 105     | (Type_variant (cstrs1, priv1), Type_variant (cstrs2, priv2)) ->
 106         private_flags priv1 priv2 &&
 107         Misc.for_all2
 108           (fun (cstr1, arg1) (cstr2, arg2) ->
 109             cstr1 = cstr2 &&
 110             Misc.for_all2
 111               (fun ty1 ty2 ->
 112                 Ctype.equal env true (ty1::decl1.type_params)
 113                                      (ty2::decl2.type_params))
 114               arg1 arg2)
 115           cstrs1 cstrs2
 116     | (Type_record(labels1,rep1,priv1), Type_record(labels2,rep2,priv2)) ->
 117         private_flags priv1 priv2 &&
 118         rep1 = rep2 &&
 119         Misc.for_all2
 120           (fun (lbl1, mut1, ty1) (lbl2, mut2, ty2) ->
 121             lbl1 = lbl2 && mut1 = mut2 &&
 122             Ctype.equal env true (ty1::decl1.type_params)
 123                                  (ty2::decl2.type_params))
 124           labels1 labels2
 125     | (_, _) -> false
 126   end &&
 127   begin match (decl1.type_manifest, decl2.type_manifest) with
 128       (_, None) ->
 129         Ctype.equal env true decl1.type_params decl2.type_params
 130     | (Some ty1, Some ty2) ->
 131         type_manifest env ty1 decl1.type_params ty2 decl2.type_params
 132     | (None, Some ty2) ->
 133         let ty1 =
 134           Btype.newgenty (Tconstr(Pident id, decl2.type_params, ref Mnil))
 135         in
 136         Ctype.equal env true decl1.type_params decl2.type_params &&
 137         Ctype.equal env false [ty1] [ty2]
 138   end &&
 139   if match decl2.type_kind with
 140   | Type_record(_,_,priv) | Type_variant(_,priv) -> priv = Private
 141   | Type_abstract ->
 142       match decl2.type_manifest with None -> true
 143       | Some ty -> Btype.has_constr_row (Ctype.expand_head env ty)
 144   then
 145     List.for_all2
 146       (fun (co1,cn1,ct1) (co2,cn2,ct2) -> (not co1 || co2) && (not cn1 || cn2))
 147       decl1.type_variance decl2.type_variance
 148   else true
 149
 150 (* Inclusion between exception declarations *)
 151
 152 let exception_declarations env ed1 ed2 =
 153   Misc.for_all2 (fun ty1 ty2 -> Ctype.equal env false [ty1] [ty2]) ed1 ed2
 154
 155 (* Inclusion between class types *)
 156 let encode_val (mut, ty) rem =
 157   begin match mut with
 158     Asttypes.Mutable   -> Predef.type_unit
 159   | Asttypes.Immutable -> Btype.newgenty Tvar
 160   end
 161   ::ty::rem
 162
 163 let meths meths1 meths2 =
 164   Meths.fold
 165     (fun nam t2 (ml1, ml2) ->
 166        (begin try
 167           Meths.find nam meths1 :: ml1
 168         with Not_found ->
 169           ml1
 170         end,
 171         t2 :: ml2))
 172     meths2 ([], [])
 173
 174 let vars vars1 vars2 =
 175   Vars.fold
 176     (fun lab v2 (vl1, vl2) ->
 177        (begin try
 178           encode_val (Vars.find lab vars1) vl1
 179         with Not_found ->
 180           vl1
 181         end,
 182         encode_val v2 vl2))
 183     vars2 ([], [])