ocaml/typing/includecore.ml

(***********************************************************************)
(*                                                                     *)
(*                                OCaml                                *)
(*                                                                     *)
(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
(*                                                                     *)
(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
(*  en Automatique.  All rights reserved.  This file is distributed    *)
(*  under the terms of the Q Public License version 1.0.               *)
(*                                                                     *)
(***********************************************************************)

(* Inclusion checks for the core language *)

open Asttypes
open Path
open Types
open Typedtree

(* Inclusion between value descriptions *)

exception Dont_match

let value_descriptions env vd1 vd2 =
  if Ctype.moregeneral env true vd1.val_type vd2.val_type then begin
    match (vd1.val_kind, vd2.val_kind) with
        (Val_prim p1, Val_prim p2) ->
          if p1 = p2 then Tcoerce_none else raise Dont_match
      | (Val_prim p, _) ->
          let pc = {pc_desc = p; pc_type = vd2.val_type;
                  pc_env = env; pc_loc = vd1.val_loc; } in
          Tcoerce_primitive pc
      | (_, Val_prim p) -> raise Dont_match
      | (_, _) -> Tcoerce_none
  end else
    raise Dont_match

(* Inclusion between "private" annotations *)

let private_flags decl1 decl2 =
  match decl1.type_private, decl2.type_private with
  | Private, Public ->
      decl2.type_kind = Type_abstract &&
      (decl2.type_manifest = None || decl1.type_kind <> Type_abstract)
  | _, _ -> true

(* Inclusion between manifest types (particularly for private row types) *)

let is_absrow env ty =
  match ty.desc with
    Tconstr(Pident id, _, _) ->
      begin match Ctype.expand_head env ty with
        {desc=Tobject _|Tvariant _} -> true
      | _ -> false
      end
  | _ -> false

let type_manifest env ty1 params1 ty2 params2 priv2 =
  let ty1' = Ctype.expand_head env ty1 and ty2' = Ctype.expand_head env ty2 in
  match ty1'.desc, ty2'.desc with
    Tvariant row1, Tvariant row2 when is_absrow env (Btype.row_more row2) ->
      let row1 = Btype.row_repr row1 and row2 = Btype.row_repr row2 in
      Ctype.equal env true (ty1::params1) (row2.row_more::params2) &&
      begin match row1.row_more with
        {desc=Tvar _|Tconstr _|Tnil} -> true
      | _ -> false
      end &&
      let r1, r2, pairs =
        Ctype.merge_row_fields row1.row_fields row2.row_fields in
      (not row2.row_closed ||
       row1.row_closed && Ctype.filter_row_fields false r1 = []) &&
      List.for_all
        (fun (_,f) -> match Btype.row_field_repr f with
          Rabsent | Reither _ -> true | Rpresent _ -> false)
        r2 &&
      let to_equal = ref (List.combine params1 params2) in
      List.for_all
        (fun (_, f1, f2) ->
          match Btype.row_field_repr f1, Btype.row_field_repr f2 with
            Rpresent(Some t1),
            (Rpresent(Some t2) | Reither(false, [t2], _, _)) ->
              to_equal := (t1,t2) :: !to_equal; true
          | Rpresent None, (Rpresent None | Reither(true, [], _, _)) -> true
          | Reither(c1,tl1,_,_), Reither(c2,tl2,_,_)
            when List.length tl1 = List.length tl2 && c1 = c2 ->
              to_equal := List.combine tl1 tl2 @ !to_equal; true
          | Rabsent, (Reither _ | Rabsent) -> true
          | _ -> false)
        pairs &&
      let tl1, tl2 = List.split !to_equal in
      Ctype.equal env true tl1 tl2
  | Tobject (fi1, _), Tobject (fi2, _)
    when is_absrow env (snd(Ctype.flatten_fields fi2)) ->
      let (fields2,rest2) = Ctype.flatten_fields fi2 in
      Ctype.equal env true (ty1::params1) (rest2::params2) &&
      let (fields1,rest1) = Ctype.flatten_fields fi1 in
      (match rest1 with {desc=Tnil|Tvar _|Tconstr _} -> true | _ -> false) &&
      let pairs, miss1, miss2 = Ctype.associate_fields fields1 fields2 in
      miss2 = [] &&
      let tl1, tl2 =
        List.split (List.map (fun (_,_,t1,_,t2) -> t1, t2) pairs) in
      Ctype.equal env true (params1 @ tl1) (params2 @ tl2)
  | _ ->
      let rec check_super ty1 =
        Ctype.equal env true (ty1 :: params1) (ty2 :: params2) ||
        priv2 = Private &&
        try check_super
              (Ctype.try_expand_once_opt env (Ctype.expand_head env ty1))
        with Ctype.Cannot_expand -> false
      in check_super ty1

(* Inclusion between type declarations *)

type type_mismatch =
    Arity
  | Privacy
  | Kind
  | Constraint
  | Manifest
  | Variance
  | Field_type of Ident.t
  | Field_mutable of Ident.t
  | Field_arity of Ident.t
  | Field_names of int * Ident.t * Ident.t
  | Field_missing of bool * Ident.t
  | Record_representation of bool

let report_type_mismatch0 first second decl ppf err =
  let pr fmt = Format.fprintf ppf fmt in
  match err with
    Arity -> pr "They have different arities"
  | Privacy -> pr "A private type would be revealed"
  | Kind -> pr "Their kinds differ"
  | Constraint -> pr "Their constraints differ"
  | Manifest -> ()
  | Variance -> pr "Their variances do not agree"
  | Field_type s ->
      pr "The types for field %s are not equal" (Ident.name s)
  | Field_mutable s ->
      pr "The mutability of field %s is different" (Ident.name s)
  | Field_arity s ->
      pr "The arities for field %s differ" (Ident.name s)
  | Field_names (n, name1, name2) ->
      pr "Fields number %i have different names, %s and %s"
        n (Ident.name name1) (Ident.name name2)
  | Field_missing (b, s) ->
      pr "The field %s is only present in %s %s"
        (Ident.name s) (if b then second else first) decl
  | Record_representation b ->
      pr "Their internal representations differ:@ %s %s %s"
        (if b then second else first) decl
        "uses unboxed float representation"

let report_type_mismatch first second decl ppf =
  List.iter
    (fun err ->
      if err = Manifest then () else
      Format.fprintf ppf "@ %a." (report_type_mismatch0 first second decl) err)

let rec compare_constructor_arguments env cstr params1 params2 arg1 arg2 =
  match arg1, arg2 with
  | Types.Cstr_tuple arg1, Types.Cstr_tuple arg2 ->
      if List.length arg1 <> List.length arg2 then [Field_arity cstr]
      else if Misc.for_all2
          (fun ty1 ty2 -> Ctype.equal env true (ty1::params1) (ty2::params2))
          (arg1) (arg2)
      then [] else [Field_type cstr]
  | Types.Cstr_record l1, Types.Cstr_record l2 ->
      compare_records env params1 params2 0 l1 l2
  | _ -> [Field_type cstr]

and compare_variants env params1 params2 n cstrs1 cstrs2 =
  match cstrs1, cstrs2 with
    [], []           -> []
  | [], c::_ -> [Field_missing (true, c.Types.cd_id)]
  | c::_, [] -> [Field_missing (false, c.Types.cd_id)]
  | {Types.cd_id=cstr1; cd_args=arg1; cd_res=ret1}::rem1,
    {Types.cd_id=cstr2; cd_args=arg2; cd_res=ret2}::rem2 ->
      if Ident.name cstr1 <> Ident.name cstr2 then
        [Field_names (n, cstr1, cstr2)]
      else match ret1, ret2 with
      | Some r1, Some r2 when not (Ctype.equal env true [r1] [r2]) ->
          [Field_type cstr1]
      | Some _, None | None, Some _ ->
          [Field_type cstr1]
      | _ ->
          let r =
            compare_constructor_arguments env cstr1
              params1 params2 arg1 arg2
          in
          if r <> [] then r
          else compare_variants env params1 params2 (n+1) rem1 rem2


and compare_records env params1 params2 n labels1 labels2 =
  match labels1, labels2 with
    [], []           -> []
  | [], l::_ -> [Field_missing (true, l.ld_id)]
  | l::_, [] -> [Field_missing (false, l.ld_id)]
  | {Types.ld_id=lab1; ld_mutable=mut1; ld_type=arg1}::rem1,
    {Types.ld_id=lab2; ld_mutable=mut2; ld_type=arg2}::rem2 ->
      if Ident.name lab1 <> Ident.name lab2
      then [Field_names (n, lab1, lab2)]
      else if mut1 <> mut2 then [Field_mutable lab1] else
      if Ctype.equal env true (arg1::params1)
                              (arg2::params2)
      then compare_records env params1 params2 (n+1) rem1 rem2
      else [Field_type lab1]

let type_declarations ?(equality = false) env name decl1 id decl2 =
  if decl1.type_arity <> decl2.type_arity then [Arity] else
  if not (private_flags decl1 decl2) then [Privacy] else
  let err = match (decl1.type_kind, decl2.type_kind) with
      (_, Type_abstract) -> []
    | (Type_variant cstrs1, Type_variant cstrs2) ->
        let mark cstrs usage name decl =
          List.iter
            (fun c ->
              Env.mark_constructor_used usage env name decl
                                        (Ident.name c.Types.cd_id))
            cstrs
        in
        let usage =
          if decl1.type_private = Private || decl2.type_private = Public
          then Env.Positive else Env.Privatize
        in
        mark cstrs1 usage name decl1;
        if equality then mark cstrs2 Env.Positive (Ident.name id) decl2;
        compare_variants env decl1.type_params decl2.type_params 1 cstrs1 cstrs2
    | (Type_record(labels1,rep1), Type_record(labels2,rep2)) ->
        let err = compare_records env decl1.type_params decl2.type_params
            1 labels1 labels2 in
        if err <> [] || rep1 = rep2 then err else
        [Record_representation (rep2 = Record_float)]
    | (Type_open, Type_open) -> []
    | (_, _) -> [Kind]
  in
  if err <> [] then err else
  let err = match (decl1.type_manifest, decl2.type_manifest) with
      (_, None) ->
        if Ctype.equal env true decl1.type_params decl2.type_params
        then [] else [Constraint]
    | (Some ty1, Some ty2) ->
        if type_manifest env ty1 decl1.type_params ty2 decl2.type_params
            decl2.type_private
        then [] else [Manifest]
    | (None, Some ty2) ->
        let ty1 =
          Btype.newgenty (Tconstr(Pident id, decl2.type_params, ref Mnil))
        in
        if Ctype.equal env true decl1.type_params decl2.type_params then
          if Ctype.equal env false [ty1] [ty2] then []
          else [Manifest]
        else [Constraint]
  in
  if err <> [] then err else
  let abstr =
    decl2.type_private = Private ||
    decl2.type_kind = Type_abstract && decl2.type_manifest = None in
  let opn = decl2.type_kind = Type_open && decl2.type_manifest = None in
  let constrained ty = not (Btype.(is_Tvar (repr ty))) in
  if List.for_all2
      (fun ty (v1,v2) ->
        let open Variance in
        let imp a b = not a || b in
        let (co1,cn1) = get_upper v1 and (co2,cn2) = get_upper v2 in
        (if abstr then (imp co1 co2 && imp cn1 cn2)
         else if opn || constrained ty then (co1 = co2 && cn1 = cn2)
         else true) &&
        let (p1,n1,i1,j1) = get_lower v1 and (p2,n2,i2,j2) = get_lower v2 in
        imp abstr (imp p2 p1 && imp n2 n1 && imp i2 i1 && imp j2 j1))
      decl2.type_params (List.combine decl1.type_variance decl2.type_variance)
  then [] else [Variance]

(* Inclusion between extension constructors *)

let extension_constructors env id ext1 ext2 =
  let usage =
    if ext1.ext_private = Private || ext2.ext_private = Public
    then Env.Positive else Env.Privatize
  in
  Env.mark_extension_used usage env ext1 (Ident.name id);
  let ty1 =
    Btype.newgenty (Tconstr(ext1.ext_type_path, ext1.ext_type_params, ref Mnil))
  in
  let ty2 =
    Btype.newgenty (Tconstr(ext2.ext_type_path, ext2.ext_type_params, ref Mnil))
  in
  if Ctype.equal env true
       (ty1 :: ext1.ext_type_params)
       (ty2 :: ext2.ext_type_params)
  then
    if compare_constructor_arguments env (Ident.create "")
        ext1.ext_type_params ext2.ext_type_params
        ext1.ext_args ext2.ext_args = [] then
      if match ext1.ext_ret_type, ext2.ext_ret_type with
          Some r1, Some r2 when not (Ctype.equal env true [r1] [r2]) -> false
        | Some _, None | None, Some _ -> false
        | _ -> true
      then
        match ext1.ext_private, ext2.ext_private with
            Private, Public -> false
          | _, _ -> true
      else false
    else false
  else false