(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
(*            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.               *)
(*                                                                     *)
(***********************************************************************)

(* $Id$ *)

(* Inclusion checks for the module language *)

open Misc
open Path
open Types
open Typedtree

type error =
    Missing_field of Ident.t
  | Value_descriptions of Ident.t * value_description * value_description
  | Type_declarations of Ident.t * type_declaration * type_declaration
  | Exception_declarations of
      Ident.t * exception_declaration * exception_declaration
  | Module_types of module_type * module_type
  | Modtype_infos of Ident.t * modtype_declaration * modtype_declaration
  | Modtype_permutation
  | Interface_mismatch of string * string
  | Class_type_declarations of
      Ident.t * cltype_declaration * cltype_declaration *
      Ctype.class_match_failure list
  | Class_declarations of
      Ident.t * class_declaration * class_declaration *
      Ctype.class_match_failure list

exception Error of error list

(* All functions "blah env x1 x2" check that x1 is included in x2,
   i.e. that x1 is the type of an implementation that fulfills the
   specification x2. If not, Error is raised with a backtrace of the error. *)

(* Inclusion between value descriptions *)

let value_descriptions env subst id vd1 vd2 =
  let vd2 = Subst.value_description subst vd2 in
  try
    Includecore.value_descriptions env vd1 vd2
  with Includecore.Dont_match ->
    raise(Error[Value_descriptions(id, vd1, vd2)])

(* Inclusion between type declarations *)

let type_declarations env subst id decl1 decl2 =
  let decl2 = Subst.type_declaration subst decl2 in
  if Includecore.type_declarations env id decl1 decl2
  then ()
  else raise(Error[Type_declarations(id, decl1, decl2)])

(* Inclusion between exception declarations *)

let exception_declarations env subst id decl1 decl2 =
  let decl2 = Subst.exception_declaration subst decl2 in
  if Includecore.exception_declarations env decl1 decl2
  then ()
  else raise(Error[Exception_declarations(id, decl1, decl2)])

(* Inclusion between class declarations *)

let class_type_declarations env subst id decl1 decl2 =
  let decl2 = Subst.cltype_declaration subst decl2 in
  match Includeclass.class_type_declarations env decl1 decl2 with
    []     -> ()
  | reason -> raise(Error[Class_type_declarations(id, decl1, decl2, reason)])

let class_declarations env subst id decl1 decl2 =
  let decl2 = Subst.class_declaration subst decl2 in
  match Includeclass.class_declarations env decl1 decl2 with
    []     -> ()
  | reason -> raise(Error[Class_declarations(id, decl1, decl2, reason)])

(* Expand a module type identifier when possible *)

exception Dont_match

let expand_module_path env path =
  try
    Env.find_modtype_expansion path env
  with Not_found ->
    raise Dont_match

(* Extract name, kind and ident from a signature item *)

type field_desc =
    Field_value of string
  | Field_type of string
  | Field_exception of string
  | Field_module of string
  | Field_modtype of string
  | Field_class of string
  | Field_classtype of string

let item_ident_name = function
    Tsig_value(id, _) -> (id, Field_value(Ident.name id))
  | Tsig_type(id, _) -> (id, Field_type(Ident.name id))
  | Tsig_exception(id, _) -> (id, Field_exception(Ident.name id))
  | Tsig_module(id, _) -> (id, Field_module(Ident.name id))
  | Tsig_modtype(id, _) -> (id, Field_modtype(Ident.name id))
  | Tsig_class(id, _) -> (id, Field_class(Ident.name id))
  | Tsig_cltype(id, _) -> (id, Field_classtype(Ident.name id))

(* Simplify a structure coercion *)

let simplify_structure_coercion cc =
  let pos = ref 0 in
  try
    List.iter
      (fun (n, c) ->
        if n <> !pos || c <> Tcoerce_none then raise Exit;
        incr pos)
      cc;
    Tcoerce_none
  with Exit ->
    Tcoerce_structure cc

(* Inclusion between module types. 
   Return the restriction that transforms a value of the smaller type
   into a value of the bigger type. *)

let rec modtypes env subst mty1 mty2 =
  try
    try_modtypes env subst mty1 mty2
  with 
    Dont_match ->
      raise(Error[Module_types(mty1, Subst.modtype subst mty2)])
  | Error reasons ->
      raise(Error(Module_types(mty1, Subst.modtype subst mty2) :: reasons))

and try_modtypes env subst mty1 mty2 =
  match (mty1, mty2) with
    (_, Tmty_ident p2) ->
      try_modtypes2 env mty1 (Subst.modtype subst mty2)
  | (Tmty_ident p1, _) ->
      try_modtypes env subst (expand_module_path env p1) mty2
  | (Tmty_signature sig1, Tmty_signature sig2) ->
      signatures env subst sig1 sig2
  | (Tmty_functor(param1, arg1, res1), Tmty_functor(param2, arg2, res2)) ->
      let cc_arg =
        modtypes env Subst.identity (Subst.modtype subst arg2) arg1
      in
      let cc_res =
        modtypes (Env.add_module param1 arg1 env)
          (Subst.add_module param2 (Pident param1) subst) res1 res2
      in
      begin match (cc_arg, cc_res) with
          (Tcoerce_none, Tcoerce_none) -> Tcoerce_none
        | _ -> Tcoerce_functor(cc_arg, cc_res)
      end
  | (_, _) ->
      raise Dont_match

and try_modtypes2 env mty1 mty2 =
  (* mty2 is an identifier *)
  match (mty1, mty2) with
    (Tmty_ident p1, Tmty_ident p2) when Path.same p1 p2 ->
      Tcoerce_none
  | (_, Tmty_ident p2) ->
      try_modtypes env Subst.identity mty1 (expand_module_path env p2)
  | (_, _) ->
      assert false

(* Inclusion between signatures *)

and signatures env subst sig1 sig2 =
  (* Environment used to check inclusion of components *)
  let new_env =
    Env.add_signature sig1 env in
  (* Build a table of the components of sig1, along with their positions.
     The table is indexed by kind and name of component *)
  let rec build_component_table pos tbl = function
      [] -> tbl
    | item :: rem ->
        let (id, name) = item_ident_name item in
        let nextpos =
          match item with
            Tsig_value(_,{val_kind = Val_prim _})
          | Tsig_type(_,_)
          | Tsig_modtype(_,_)
          | Tsig_cltype(_,_) -> pos
          | Tsig_value(_,_)
          | Tsig_exception(_,_)
          | Tsig_module(_,_)
          | Tsig_class(_, _) -> pos+1 in
        build_component_table nextpos
                              (Tbl.add name (id, item, pos) tbl) rem in
  let comps1 =
    build_component_table 0 Tbl.empty sig1 in
  (* Pair each component of sig2 with a component of sig1,
     identifying the names along the way.
     Return a coercion list indicating, for all run-time components
     of sig2, the position of the matching run-time components of sig1
     and the coercion to be applied to it. *)
  let rec pair_components subst paired unpaired = function
      [] ->
        begin match unpaired with
            [] -> signature_components new_env subst (List.rev paired)
          | _  -> raise(Error unpaired)
        end
    | item2 :: rem ->
        let (id2, name2) = item_ident_name item2 in
        begin try
          let (id1, item1, pos1) = Tbl.find name2 comps1 in
          let new_subst =
            match item2 with
              Tsig_type _ ->
                Subst.add_type id2 (Pident id1) subst
            | Tsig_module _ ->
                Subst.add_module id2 (Pident id1) subst
            | Tsig_modtype _ ->
                Subst.add_modtype id2 (Tmty_ident (Pident id1)) subst
            | Tsig_value _ | Tsig_exception _ | Tsig_class _ | Tsig_cltype _ ->
                subst
          in
          pair_components new_subst
            ((item1, item2, pos1) :: paired) unpaired rem
        with Not_found ->
          pair_components subst paired (Missing_field id2 :: unpaired) rem
        end in
  (* Do the pairing and checking, and return the final coercion *)
  simplify_structure_coercion(pair_components subst [] [] sig2)

(* Inclusion between signature components *)

and signature_components env subst = function
    [] -> []
  | (Tsig_value(id1, valdecl1), Tsig_value(id2, valdecl2), pos) :: rem ->
      let cc = value_descriptions env subst id1 valdecl1 valdecl2 in
      begin match valdecl2.val_kind with
        Val_prim p -> signature_components env subst rem
      | _ -> (pos, cc) :: signature_components env subst rem
      end
  | (Tsig_type(id1, tydecl1), Tsig_type(id2, tydecl2), pos) :: rem ->
      type_declarations env subst id1 tydecl1 tydecl2;
      signature_components env subst rem
  | (Tsig_exception(id1, excdecl1), Tsig_exception(id2, excdecl2), pos)
    :: rem ->
      exception_declarations env subst id1 excdecl1 excdecl2;
      (pos, Tcoerce_none) :: signature_components env subst rem
  | (Tsig_module(id1, mty1), Tsig_module(id2, mty2), pos) :: rem ->
      let cc =
        modtypes env subst (Mtype.strengthen env mty1 (Pident id1)) mty2 in
      (pos, cc) :: signature_components env subst rem
  | (Tsig_modtype(id1, info1), Tsig_modtype(id2, info2), pos) :: rem ->
      modtype_infos env subst id1 info1 info2;
      signature_components env subst rem
  | (Tsig_class(id1, decl1), Tsig_class(id2, decl2), pos) :: rem ->
      class_declarations env subst id1 decl1 decl2;
      (pos, Tcoerce_none) :: signature_components env subst rem
  | (Tsig_cltype(id1, info1), Tsig_cltype(id2, info2), pos) :: rem ->
      class_type_declarations env subst id1 info1 info2;
      signature_components env subst rem
  | _ ->
      assert false

(* Inclusion between module type specifications *)

and modtype_infos env subst id info1 info2 =
  let info2 = Subst.modtype_declaration subst info2 in
  try
    match (info1, info2) with
      (Tmodtype_abstract, Tmodtype_abstract) -> ()
    | (Tmodtype_manifest mty1, Tmodtype_abstract) -> ()
    | (Tmodtype_manifest mty1, Tmodtype_manifest mty2) ->
        check_modtype_equiv env mty1 mty2
    | (Tmodtype_abstract, Tmodtype_manifest mty2) ->
        check_modtype_equiv env (Tmty_ident(Pident id)) mty2
  with Error reasons ->
    raise(Error(Modtype_infos(id, info1, info2) :: reasons))

and check_modtype_equiv env mty1 mty2 =
  match
    (modtypes env Subst.identity mty1 mty2,
     modtypes env Subst.identity mty2 mty1)
  with
    (Tcoerce_none, Tcoerce_none) -> ()
  | (_, _) -> raise(Error [Modtype_permutation])

(* Simplified inclusion check between module types *)

let check_modtype_inclusion env mty1 mty2 =
  try
    ignore(modtypes env Subst.identity mty1 mty2)
  with Error reasons ->
    raise Not_found

let _ = Env.check_modtype_inclusion := check_modtype_inclusion

(* Check that an implementation of a compilation unit meets its
   interface. *)

let compunit impl_name impl_sig intf_name intf_sig =
  try
    signatures Env.initial Subst.identity impl_sig intf_sig
  with Error reasons ->
    raise(Error(Interface_mismatch(impl_name, intf_name) :: reasons))

(* Hide the substitution parameter to the outside world *)

let modtypes env mty1 mty2 = modtypes env Subst.identity mty1 mty2
let signatures env sig1 sig2 = signatures env Subst.identity sig1 sig2
let type_declarations env id decl1 decl2 =
  type_declarations env Subst.identity id decl1 decl2

(* Error report *)

open Format
open Printtyp

let include_err ppf = function
  | Missing_field id ->
      fprintf ppf "The field `%a' is required but not provided" ident id
  | Value_descriptions(id, d1, d2) ->
      fprintf ppf
       "@[<hv 2>Values do not match:@ \
        %a@;<1 -2>is not included in@ %a@]"
       (value_description id) d1 (value_description id) d2
  | Type_declarations(id, d1, d2) ->
      fprintf ppf
       "@[<hv 2>Type declarations do not match:@ \
        %a@;<1 -2>is not included in@ %a@]"
       (type_declaration id) d1
       (type_declaration id) d2
  | Exception_declarations(id, d1, d2) ->
      fprintf ppf
       "@[<hv 2>Exception declarations do not match:@ \
        %a@;<1 -2>is not included in@ %a@]"
      (exception_declaration id) d1
      (exception_declaration id) d2
  | Module_types(mty1, mty2)->
      fprintf ppf
       "@[<hv 2>Modules do not match:@ \
        %a@;<1 -2>is not included in@ %a@]"
      modtype mty1
      modtype mty2
  | Modtype_infos(id, d1, d2) ->
      fprintf ppf
       "@[<hv 2>Module type declarations do not match:@ \
        %a@;<1 -2>is not included in@ %a@]"
      (modtype_declaration id) d1
      (modtype_declaration id) d2
  | Modtype_permutation ->
      fprintf ppf "Illegal permutation of structure fields"
  | Interface_mismatch(impl_name, intf_name) ->
      fprintf ppf "@[The implementation %s@ does not match the interface %s:" 
       impl_name intf_name
  | Class_type_declarations(id, d1, d2, reason) ->
      fprintf ppf
       "@[<hv 2>Class type declarations do not match:@ \
        %a@;<1 -2>is not included in@ %a@]@ %a"
      (Printtyp.cltype_declaration id) d1
      (Printtyp.cltype_declaration id) d2
      Includeclass.report_error reason
  | Class_declarations(id, d1, d2, reason) ->
      fprintf ppf
       "@[<hv 2>Class declarations do not match:@ \
        %a@;<1 -2>is not included in@ %a@]@ %a"
      (Printtyp.class_declaration id) d1
      (Printtyp.class_declaration id) d2
      Includeclass.report_error reason

let report_error ppf = function
  |  [] -> ()
  | err :: errs ->
      let print_errs ppf errs =
         List.iter (fun err -> fprintf ppf "@ %a" include_err err) errs in
      fprintf ppf "@[<v>%a%a@]" include_err err print_errs errs