(**************************************************************************) (* *) (* 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 GNU Lesser General Public License version 2.1, with the *) (* special exception on linking described in the file LICENSE. *) (* *) (**************************************************************************) (* Inclusion checks for the module language *) open Misc open Typedtree open Types type symptom = Missing_field of Ident.t * Location.t * string (* kind *) | Value_descriptions of Ident.t * value_description * value_description * Includecore.value_mismatch | Type_declarations of Ident.t * type_declaration * type_declaration * Includecore.type_mismatch | Extension_constructors of Ident.t * extension_constructor * extension_constructor * Includecore.extension_constructor_mismatch | Module_types of module_type * module_type | Modtype_infos of Ident.t * modtype_declaration * modtype_declaration | Modtype_permutation of Types.module_type * Typedtree.module_coercion | Interface_mismatch of string * string | Class_type_declarations of Ident.t * class_type_declaration * class_type_declaration * Ctype.class_match_failure list | Class_declarations of Ident.t * class_declaration * class_declaration * Ctype.class_match_failure list | Unbound_module_path of Path.t | Invalid_module_alias of Path.t type pos = | Module of Ident.t | Modtype of Ident.t | Arg of functor_parameter | Body of functor_parameter module Error = struct type functor_arg_descr = | Anonymous | Named of Path.t | Unit | Empty_struct (** For backward compatibility's sake, an empty struct can be implicitly converted to an unit module *) type ('a,'b) diff = {got:'a; expected:'a; symptom:'b} type 'a core_diff =('a,unit) diff let diff x y s = {got=x;expected=y; symptom=s} let sdiff x y = {got=x; expected=y; symptom=()} type core_sigitem_symptom = | Value_descriptions of (value_description, Includecore.value_mismatch) diff | Type_declarations of (type_declaration, Includecore.type_mismatch) diff | Extension_constructors of (extension_constructor, Includecore.extension_constructor_mismatch) diff | Class_type_declarations of (class_type_declaration, Ctype.class_match_failure list) diff | Class_declarations of (class_declaration, Ctype.class_match_failure list) diff type core_module_type_symptom = | Not_an_alias | Not_an_identifier | Incompatible_aliases | Abstract_module_type | Unbound_module_path of Path.t type module_type_symptom = | Mt_core of core_module_type_symptom | Signature of signature_symptom | Functor of functor_symptom | Invalid_module_alias of Path.t | After_alias_expansion of module_type_diff and module_type_diff = (module_type, module_type_symptom) diff and functor_symptom = | Params of functor_params_diff | Result of module_type_diff and ('arg,'path) functor_param_symptom = | Incompatible_params of 'arg * functor_parameter | Mismatch of module_type_diff and arg_functor_param_symptom = (functor_parameter, Ident.t) functor_param_symptom and functor_params_info = { params: functor_parameter list; res: module_type } and functor_params_diff = functor_params_info core_diff and signature_symptom = { env: Env.t; missings: signature_item list; incompatibles: (Ident.t * sigitem_symptom) list; oks: (int * module_coercion) list; leftovers: (signature_item * signature_item * int) list; } and sigitem_symptom = | Core of core_sigitem_symptom | Module_type_declaration of (modtype_declaration, module_type_declaration_symptom) diff | Module_type of module_type_diff and module_type_declaration_symptom = | Illegal_permutation of Typedtree.module_coercion | Not_greater_than of module_type_diff | Not_less_than of module_type_diff | Incomparable of {less_than:module_type_diff; greater_than: module_type_diff} type all = | In_Compilation_unit of (string, signature_symptom) diff | In_Signature of signature_symptom | In_Module_type of module_type_diff | In_Module_type_substitution of Ident.t * (Types.module_type,module_type_declaration_symptom) diff | In_Type_declaration of Ident.t * core_sigitem_symptom | In_Expansion of core_module_type_symptom let cons_arg arg params_info = { params = arg :: params_info.params; res = params_info.res } let functor_params info1 info2 = Error (Functor (Params (sdiff info1 info2))) end module Directionality = struct type mark = | Mark_both | Mark_positive | Mark_neither type pos = | Strictly_positive (** Strictly positive positions are notable for tools since they are the the case where we match a implementation definition with an interface declaration. Oherwise in the positive case we are matching declatations inside functor arguments at even level of nesting.*) | Positive | Negative (** When checking inclusion, the [Directionality.t] type tracks the subtyping direction at the syntactic level. The [posivity] field is used in the [cmt_declaration_dependencies] to distinguish between directed and undirected edges, and to avoid recording matched declarations twice. The [mark_as_used] field describes if we should record only positive use, any use (because there is no clear implementation side), or none (because we are inside an auxiliary check function.) The [in_eq] field is [true] when we are checking both directions inside of module types which allows optimizing module type equality checks. The module subtyping relation [A <: B] checks that [A.T = B.T] when [A] and [B] define a module type [T]. The relation [A.T = B.T] is equivalent to [(A.T <: B.T) and (B.T <: A.T)], but checking both recursively would lead to an exponential slowdown (see #10598 and #10616). To avoid this issue, when [in_eq] is [true], we compute a coarser relation [A << B] which is the same as [A <: B] except that module types [T] are checked only for [A.T << B.T] and not the reverse. Thus, we can implement a cheap module type equality check [A.T = B.T] by computing [(A.T << B.T) and (B.T << A.T)], avoiding the exponential slowdown described above. *) type t = { in_eq:bool; mark_as_used:mark; pos:pos; } let strictly_positive ~mark = let mark_as_used = if mark then Mark_positive else Mark_neither in { in_eq=false; pos=Strictly_positive; mark_as_used } let unknown ~mark = let mark_as_used = if mark then Mark_both else Mark_neither in { in_eq=false; pos=Positive; mark_as_used } let negate_pos = function | Positive | Strictly_positive -> Negative | Negative -> Positive let negate d = { d with pos = negate_pos d.pos } let at_most_positive = function | Strictly_positive -> Positive | Positive | Negative as non_strict -> non_strict let enter_eq d = { in_eq = true; pos = at_most_positive d.pos; mark_as_used = d.mark_as_used } let mark_as_used d = match d.mark_as_used with | Mark_neither -> false | Mark_both -> true | Mark_positive -> match d.pos with | Positive | Strictly_positive -> true | Negative -> false end module Core_inclusion = struct (* 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 ~loc env ~direction subst id vd1 vd2 = if Directionality.mark_as_used direction then Env.mark_value_used vd1.val_uid; let vd2 = Subst.value_description subst vd2 in try Ok (Includecore.value_descriptions ~loc env (Ident.name id) vd1 vd2) with Includecore.Dont_match err -> Error Error.(Core (Value_descriptions (diff vd1 vd2 err))) (* Inclusion between type declarations *) let type_declarations ~loc env ~direction subst id decl1 decl2 = let mark = Directionality.mark_as_used direction in if mark then Env.mark_type_used decl1.type_uid; let decl2 = Subst.type_declaration subst decl2 in match Includecore.type_declarations ~loc env ~mark (Ident.name id) decl1 (Path.Pident id) decl2 with | None -> Ok Tcoerce_none | Some err -> Error Error.(Core(Type_declarations (diff decl1 decl2 err))) (* Inclusion between extension constructors *) let extension_constructors ~loc env ~direction subst id ext1 ext2 = let mark = Directionality.mark_as_used direction in let ext2 = Subst.extension_constructor subst ext2 in match Includecore.extension_constructors ~loc env ~mark id ext1 ext2 with | None -> Ok Tcoerce_none | Some err -> Error Error.(Core(Extension_constructors(diff ext1 ext2 err))) (* Inclusion between class declarations *) let class_type_declarations ~loc env ~direction:_ subst _id decl1 decl2 = let decl2 = Subst.cltype_declaration subst decl2 in match Includeclass.class_type_declarations ~loc env decl1 decl2 with [] -> Ok Tcoerce_none | reason -> Error Error.(Core(Class_type_declarations(diff decl1 decl2 reason))) let class_declarations ~loc:_ env ~direction:_ subst _id decl1 decl2 = let decl2 = Subst.class_declaration subst decl2 in match Includeclass.class_declarations env decl1 decl2 with [] -> Ok Tcoerce_none | reason -> Error Error.(Core(Class_declarations(diff decl1 decl2 reason))) end (* Expand a module type identifier when possible *) let expand_modtype_path env path = match Env.find_modtype_expansion path env with | exception Not_found -> None | x -> Some x let expand_module_alias ~strengthen env path = match if strengthen then Env.find_strengthened_module ~aliasable:true path env else (Env.find_module path env).md_type with | x -> Ok x | exception Not_found -> Error (Error.Unbound_module_path path) (* Extract name, kind and ident from a signature item *) type field_kind = | Field_value | Field_type | Field_exception | Field_typext | Field_module | Field_modtype | Field_class | Field_classtype type field_desc = { name: string; kind: field_kind } let kind_of_field_desc fd = match fd.kind with | Field_value -> "value" | Field_type -> "type" | Field_exception -> "exception" | Field_typext -> "extension constructor" | Field_module -> "module" | Field_modtype -> "module type" | Field_class -> "class" | Field_classtype -> "class type" let field_desc kind id = { kind; name = Ident.name id } (** Map indexed by both field types and names. This avoids name clashes between different sorts of fields such as values and types. *) module FieldMap = Map.Make(struct type t = field_desc let compare = Stdlib.compare end) let item_ident_name = function Sig_value(id, d, _) -> (id, d.val_loc, field_desc Field_value id) | Sig_type(id, d, _, _) -> (id, d.type_loc, field_desc Field_type id ) | Sig_typext(id, d, _, _) -> let kind = if Path.same d.ext_type_path Predef.path_exn then Field_exception else Field_typext in (id, d.ext_loc, field_desc kind id) | Sig_module(id, _, d, _, _) -> (id, d.md_loc, field_desc Field_module id) | Sig_modtype(id, d, _) -> (id, d.mtd_loc, field_desc Field_modtype id) | Sig_class(id, d, _, _) -> (id, d.cty_loc, field_desc Field_class id) | Sig_class_type(id, d, _, _) -> (id, d.clty_loc, field_desc Field_classtype id) let is_runtime_component = function | Sig_value(_,{val_kind = Val_prim _}, _) | Sig_type(_,_,_,_) | Sig_module(_,Mp_absent,_,_,_) | Sig_modtype(_,_,_) | Sig_class_type(_,_,_,_) -> false | Sig_value(_,_,_) | Sig_typext(_,_,_,_) | Sig_module(_,Mp_present,_,_,_) | Sig_class(_,_,_,_) -> true (* Print a coercion *) let rec print_list pr ppf = function [] -> () | [a] -> pr ppf a | a :: l -> pr ppf a; Format.fprintf ppf ";@ "; print_list pr ppf l let print_list pr ppf l = Format.fprintf ppf "[@[%a@]]" (print_list pr) l let rec print_coercion ppf c = let pr fmt = Format.fprintf ppf fmt in match c with Tcoerce_none -> pr "id" | Tcoerce_structure (fl, nl) -> pr "@[<2>struct@ %a@ %a@]" (print_list print_coercion2) fl (print_list print_coercion3) nl | Tcoerce_functor (inp, out) -> pr "@[<2>functor@ (%a)@ (%a)@]" print_coercion inp print_coercion out | Tcoerce_primitive {pc_desc; pc_env = _; pc_type} -> pr "prim %s@ (%a)" pc_desc.Primitive.prim_name Rawprinttyp.type_expr pc_type | Tcoerce_alias (_, p, c) -> pr "@[<2>alias %a@ (%a)@]" Printtyp.path p print_coercion c and print_coercion2 ppf (n, c) = Format.fprintf ppf "@[%d,@ %a@]" n print_coercion c and print_coercion3 ppf (i, n, c) = Format.fprintf ppf "@[%s, %d,@ %a@]" (Ident.unique_name i) n print_coercion c (* Simplify a structure coercion *) let equal_module_paths env p1 subst p2 = Path.same p1 p2 || Path.same (Env.normalize_module_path None env p1) (Env.normalize_module_path None env (Subst.module_path subst p2)) let equal_modtype_paths env p1 subst p2 = Path.same p1 p2 || Path.same (Env.normalize_modtype_path env p1) (Env.normalize_modtype_path env (Subst.modtype_path subst p2)) let simplify_structure_coercion cc id_pos_list = let rec is_identity_coercion pos = function | [] -> true | (n, c) :: rem -> n = pos && c = Tcoerce_none && is_identity_coercion (pos + 1) rem in if is_identity_coercion 0 cc then Tcoerce_none else Tcoerce_structure (cc, id_pos_list) let retrieve_functor_params env mty = let rec retrieve_functor_params before env = function | Mty_ident p as res -> begin match expand_modtype_path env p with | Some mty -> retrieve_functor_params before env mty | None -> { Error.params = List.rev before; res } end | Mty_alias p as res -> begin match expand_module_alias ~strengthen:false env p with | Ok mty -> retrieve_functor_params before env mty | Error _ -> { Error.params = List.rev before; res } end | Mty_functor (p, res) -> retrieve_functor_params (p :: before) env res | Mty_signature _ as res -> { Error.params = List.rev before; res } in retrieve_functor_params [] env mty (* Inclusion between module types. Return the restriction that transforms a value of the smaller type into a value of the bigger type. *) (* When computing a signature difference, we need to distinguish between recoverable errors at the value level and unrecoverable errors at the type level that require us to stop the computation of the difference due to incoherent types. *) type 'a recoverable_error = { error: 'a; recoverable:bool } let mark_error_as_recoverable r = Result.map_error (fun error -> { error; recoverable=true}) r let mark_error_as_unrecoverable r = Result.map_error (fun error -> { error; recoverable=false}) r module Sign_diff = struct type t = { runtime_coercions: (int * Typedtree.module_coercion) list; shape_map: Shape.Map.t; deep_modifications:bool; errors: (Ident.t * Error.sigitem_symptom) list; leftovers: ((Types.signature_item as 'it) * 'it * int) list } let empty = { runtime_coercions = []; shape_map = Shape.Map.empty; deep_modifications = false; errors = []; leftovers = [] } let merge x y = { runtime_coercions = x.runtime_coercions @ y.runtime_coercions; shape_map = y.shape_map; (* the shape map is threaded the map during the difference computation, the last shape map contains all previous elements. *) deep_modifications = x.deep_modifications || y.deep_modifications; errors = x.errors @ y.errors; leftovers = x.leftovers @ y.leftovers } end (** Core type system subtyping-like relation that we want to lift at the module level. We have two relations that we want to lift: - the normal subtyping relation [<:]. - the coarse-grain consistency relation [C], which is defined by [d1 C d2] if there is an environment [E] such that [E |- d1 <: d2]. *) type 'a core_incl = loc:Location.t -> Env.t -> direction:Directionality.t -> Subst.t -> Ident.t -> 'a -> 'a -> (module_coercion, Error.sigitem_symptom) result type core_relation = { value_descriptions: Types.value_description core_incl; type_declarations: Types.type_declaration core_incl; extension_constructors: Types.extension_constructor core_incl; class_declarations: Types.class_declaration core_incl; class_type_declarations: Types.class_type_declaration core_incl; } let rec modtypes ~core ~direction ~loc env subst mty1 mty2 shape = match try_modtypes ~core ~direction ~loc env subst mty1 mty2 shape with | Ok _ as ok -> ok | Error reason -> let mty2 = Subst.modtype Make_local subst mty2 in Error Error.(diff mty1 mty2 reason) and try_modtypes ~core ~direction ~loc env subst mty1 mty2 orig_shape = match mty1, mty2 with | (Mty_alias p1, Mty_alias p2) -> if not (Env.is_aliasable p2 env) then Error (Error.Invalid_module_alias p2) else if not (equal_module_paths env p1 subst p2) then Error Error.(Mt_core Incompatible_aliases) else Ok (Tcoerce_none, orig_shape) | (Mty_alias p1, _) -> begin match Env.normalize_module_path (Some Location.none) env p1 with | exception Env.Error (Env.Missing_module (_, _, path)) -> Error Error.(Mt_core(Unbound_module_path path)) | p1 -> begin match expand_module_alias ~strengthen:false env p1 with | Error e -> Error (Error.Mt_core e) | Ok mty1 -> match strengthened_modtypes ~core ~direction ~loc ~aliasable:true env subst mty1 p1 mty2 orig_shape with | Ok _ as x -> x | Error reason -> Error (Error.After_alias_expansion reason) end end | (Mty_ident p1, Mty_ident p2) -> let p1 = Env.normalize_modtype_path env p1 in let p2 = Env.normalize_modtype_path env (Subst.modtype_path subst p2) in if Path.same p1 p2 then Ok (Tcoerce_none, orig_shape) else begin match expand_modtype_path env p1, expand_modtype_path env p2 with | Some mty1, Some mty2 -> try_modtypes ~core ~direction ~loc env subst mty1 mty2 orig_shape | None, _ | _, None -> Error (Error.Mt_core Abstract_module_type) end | (Mty_ident p1, _) -> let p1 = Env.normalize_modtype_path env p1 in begin match expand_modtype_path env p1 with | Some p1 -> try_modtypes ~core ~direction ~loc env subst p1 mty2 orig_shape | None -> Error (Error.Mt_core Abstract_module_type) end | (_, Mty_ident p2) -> let p2 = Env.normalize_modtype_path env (Subst.modtype_path subst p2) in begin match expand_modtype_path env p2 with | Some p2 -> try_modtypes ~core ~direction ~loc env subst mty1 p2 orig_shape | None -> begin match mty1 with | Mty_functor _ -> Error.functor_params (retrieve_functor_params env mty1) { params = []; res=mty2 } | _ -> Error Error.(Mt_core Not_an_identifier) end end | (Mty_signature sig1, Mty_signature sig2) -> begin match signatures ~core ~direction ~loc env subst sig1 sig2 orig_shape with | Ok _ as ok -> ok | Error e -> Error (Error.Signature e) end | Mty_functor (param1, res1), Mty_functor (param2, res2) -> let cc_arg, env, subst = let direction = Directionality.negate direction in functor_param ~core ~direction ~loc env subst param1 param2 in let var, res_shape = match Shape.decompose_abs orig_shape with | Some (var, res_shape) -> var, res_shape | None -> (* Using a fresh variable with a placeholder uid here is fine: users will never try to jump to the definition of that variable. If they try to jump to the parameter from inside the functor, they will use the variable shape that is stored in the local environment. *) let var, shape_var = Shape.fresh_var Uid.internal_not_actually_unique in var, Shape.app orig_shape ~arg:shape_var in let cc_res = modtypes ~core ~direction ~loc env subst res1 res2 res_shape in begin match cc_arg, cc_res with | Ok Tcoerce_none, Ok (Tcoerce_none, final_res_shape) -> let final_shape = if final_res_shape == res_shape then orig_shape else Shape.abs var final_res_shape in Ok (Tcoerce_none, final_shape) | Ok cc_arg, Ok (cc_res, final_res_shape) -> let final_shape = if final_res_shape == res_shape then orig_shape else Shape.abs var final_res_shape in Ok (Tcoerce_functor(cc_arg, cc_res), final_shape) | _, Error {Error.symptom = Error.Functor Error.Params res; _} -> let got = Error.cons_arg param1 res.got in let expected = Error.cons_arg param2 res.expected in Error.functor_params got expected | Error _, _ -> let params env param res = Error.cons_arg param (retrieve_functor_params env res) in Error.functor_params (params env param1 res1) (params env param2 res2) | Ok _, Error res -> Error Error.(Functor (Result res)) end | Mty_functor _, _ | _, Mty_functor _ -> Error.functor_params (retrieve_functor_params env mty1) (retrieve_functor_params env mty2) | _, Mty_alias _ -> Error (Error.Mt_core Error.Not_an_alias) (* Functor parameters *) and functor_param ~core ~direction ~loc env subst param1 param2 = match param1, param2 with | Unit, Unit -> Ok Tcoerce_none, env, subst | Named (name1, arg1), Named (name2, arg2) -> let arg2' = Subst.modtype Keep subst arg2 in let cc_arg = match modtypes ~core ~direction ~loc env Subst.identity arg2' arg1 Shape.dummy_mod with | Ok (cc, _) -> Ok cc | Error err -> Error (Error.Mismatch err) in let env, subst = equate_one_functor_param subst env arg2' name1 name2 in cc_arg, env, subst | _, _ -> Error (Error.Incompatible_params (param1, param2)), env, subst and equate_one_functor_param subst env arg2' name1 name2 = match name1, name2 with | Some id1, Some id2 -> (* two matching abstract parameters: we add one identifier to the environment and record the equality between the two identifiers in the substitution *) Env.add_module id1 Mp_present arg2' env, Subst.add_module id2 (Path.Pident id1) subst | None, Some id2 -> let id1 = Ident.rename id2 in Env.add_module id1 Mp_present arg2' env, Subst.add_module id2 (Path.Pident id1) subst | Some id1, None -> Env.add_module id1 Mp_present arg2' env, subst | None, None -> env, subst and strengthened_modtypes ~core ~direction ~loc ~aliasable env subst mty1 path1 mty2 shape = match mty1, mty2 with | Mty_ident p1, Mty_ident p2 when equal_modtype_paths env p1 subst p2 -> Ok (Tcoerce_none, shape) | _, _ -> let mty1 = Mtype.strengthen ~aliasable env mty1 path1 in modtypes ~core ~direction ~loc env subst mty1 mty2 shape and strengthened_module_decl ~core ~loc ~aliasable ~direction env subst md1 path1 md2 shape = match md1.md_type, md2.md_type with | Mty_ident p1, Mty_ident p2 when equal_modtype_paths env p1 subst p2 -> Ok (Tcoerce_none, shape) | _, _ -> let md1 = Mtype.strengthen_decl ~aliasable env md1 path1 in modtypes ~core ~direction ~loc env subst md1.md_type md2.md_type shape (* Inclusion between signatures *) and signatures ~core ~direction ~loc env subst sig1 sig2 mod_shape = (* Environment used to check inclusion of components *) let new_env = Env.add_signature sig1 (Env.in_signature true env) in (* Keep ids for module aliases *) let (id_pos_list,_) = List.fold_left (fun (l,pos) -> function Sig_module (id, Mp_present, _, _, _) -> ((id,pos,Tcoerce_none)::l , pos+1) | item -> (l, if is_runtime_component item then pos+1 else pos)) ([], 0) sig1 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 nb_exported pos tbl = function [] -> nb_exported, pos, tbl | item :: rem -> let pos, nextpos = if is_runtime_component item then pos, pos + 1 else -1, pos in match item_visibility item with | Hidden -> (* do not pair private items. *) build_component_table nb_exported nextpos tbl rem | Exported -> let (id, _loc, name) = item_ident_name item in build_component_table (nb_exported + 1) nextpos (FieldMap.add name (id, item, pos) tbl) rem in let exported_len1, runtime_len1, comps1 = build_component_table 0 0 FieldMap.empty sig1 in let exported_len2, runtime_len2 = List.fold_left (fun (el, rl) i -> let el = match item_visibility i with Hidden -> el | Exported -> el + 1 in let rl = if is_runtime_component i then rl + 1 else rl in el, rl ) (0, 0) sig2 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 ~core subst paired unpaired = function [] -> let open Sign_diff in let d = signature_components ~core ~direction ~loc env new_env subst mod_shape Shape.Map.empty (List.rev paired) in begin match unpaired, d.errors, d.runtime_coercions, d.leftovers with | [], [], cc, [] -> let shape = if not d.deep_modifications && exported_len1 = exported_len2 then mod_shape else Shape.str ?uid:mod_shape.Shape.uid d.shape_map in if runtime_len1 = runtime_len2 then (* see PR#5098 *) Ok (simplify_structure_coercion cc id_pos_list, shape) else Ok (Tcoerce_structure (cc, id_pos_list), shape) | missings, incompatibles, runtime_coercions, leftovers -> Error { Error.env=new_env; missings; incompatibles; oks=runtime_coercions; leftovers; } end | item2 :: rem -> let (id2, _loc, name2) = item_ident_name item2 in let name2, report = match item2, name2 with Sig_type (_, {type_manifest=None}, _, _), {name=s; kind=Field_type} when Btype.is_row_name s -> (* Do not report in case of failure, as the main type will generate an error *) { kind=Field_type; name=String.sub s 0 (String.length s - 4) }, false | _ -> name2, true in begin match FieldMap.find name2 comps1 with | (id1, item1, pos1) -> let new_subst = match item2 with Sig_type _ -> Subst.add_type id2 (Path.Pident id1) subst | Sig_module _ -> Subst.add_module id2 (Path.Pident id1) subst | Sig_modtype _ -> Subst.add_modtype id2 (Path.Pident id1) subst | Sig_value _ | Sig_typext _ | Sig_class _ | Sig_class_type _ -> subst in pair_components ~core new_subst ((item1, item2, pos1) :: paired) unpaired rem | exception Not_found -> let unpaired = if report then item2 :: unpaired else unpaired in pair_components ~core subst paired unpaired rem end in (* Do the pairing and checking, and return the final coercion *) pair_components ~core subst [] [] sig2 (* Inclusion between signature components *) and signature_components ~core ~direction ~loc old_env env subst orig_shape shape_map paired = match paired with | [] -> Sign_diff.{ empty with shape_map } | (sigi1, sigi2, pos) :: rem -> let shape_modified = ref false in let id, item, paired_uids, shape_map, present_at_runtime = match sigi1, sigi2 with | Sig_value(id1, valdecl1, _) ,Sig_value(_id2, valdecl2, _) -> let item = core.value_descriptions ~loc ~direction env subst id1 valdecl1 valdecl2 in let item = mark_error_as_recoverable item in let present_at_runtime = match valdecl2.val_kind with | Val_prim _ -> false | _ -> true in let shape_map = Shape.Map.add_value_proj shape_map id1 orig_shape in let paired_uids = (valdecl1.val_uid, valdecl2.val_uid) in id1, item, paired_uids, shape_map, present_at_runtime | Sig_type(id1, tydec1, _, _), Sig_type(_id2, tydec2, _, _) -> let item = core.type_declarations ~loc ~direction env subst id1 tydec1 tydec2 in let item = mark_error_as_unrecoverable item in (* Right now we don't filter hidden constructors / labels from the shape. *) let shape_map = Shape.Map.add_type_proj shape_map id1 orig_shape in id1, item, (tydec1.type_uid, tydec2.type_uid), shape_map, false | Sig_typext(id1, ext1, _, _), Sig_typext(_id2, ext2, _, _) -> let item = core.extension_constructors ~loc ~direction env subst id1 ext1 ext2 in let item = mark_error_as_unrecoverable item in let shape_map = Shape.Map.add_extcons_proj shape_map id1 orig_shape in id1, item, (ext1.ext_uid, ext2.ext_uid), shape_map, true | Sig_module(id1, pres1, mty1, _, _), Sig_module(_, pres2, mty2, _, _) -> begin let orig_shape = Shape.(proj orig_shape (Item.module_ id1)) in let item = module_declarations ~core ~direction ~loc env subst id1 mty1 mty2 orig_shape in let item, shape_map = match item with | Ok (cc, shape) -> if shape != orig_shape then shape_modified := true; let mod_shape = Shape.set_uid_if_none shape mty1.md_uid in Ok cc, Shape.Map.add_module shape_map id1 mod_shape | Error diff -> Error (Error.Module_type diff), (* We add the original shape to the map, even though there is a type error. It could still be useful for merlin. *) Shape.Map.add_module shape_map id1 orig_shape in let present_at_runtime, item = match pres1, pres2, mty1.md_type with | Mp_present, Mp_present, _ -> true, item | _, Mp_absent, _ -> false, item | Mp_absent, Mp_present, Mty_alias p1 -> true, Result.map (fun i -> Tcoerce_alias (env, p1, i)) item | Mp_absent, Mp_present, _ -> assert false in let item = mark_error_as_unrecoverable item in let paired_uids = (mty1.md_uid, mty2.md_uid) in id1, item, paired_uids, shape_map, present_at_runtime end | Sig_modtype(id1, info1, _), Sig_modtype(_id2, info2, _) -> let item = modtype_infos ~core ~direction ~loc env subst id1 info1 info2 in let shape_map = Shape.Map.add_module_type_proj shape_map id1 orig_shape in let item = mark_error_as_unrecoverable item in id1, item, (info1.mtd_uid, info2.mtd_uid), shape_map, false | Sig_class(id1, decl1, _, _), Sig_class(_id2, decl2, _, _) -> let item = core.class_declarations ~loc ~direction env subst id1 decl1 decl2 in let shape_map = Shape.Map.add_class_proj shape_map id1 orig_shape in let item = mark_error_as_unrecoverable item in id1, item, (decl1.cty_uid, decl2.cty_uid), shape_map, true | Sig_class_type(id1, info1, _, _), Sig_class_type(_id2, info2, _, _) -> let item = core.class_type_declarations ~loc ~direction env subst id1 info1 info2 in let item = mark_error_as_unrecoverable item in let shape_map = Shape.Map.add_class_type_proj shape_map id1 orig_shape in id1, item, (info1.clty_uid, info2.clty_uid), shape_map, false | _ -> assert false in let deep_modifications = !shape_modified in let first = match item with | Ok x -> begin match direction with | { Directionality.in_eq = true; pos = Negative } | { Directionality.mark_as_used = Mark_neither; _ } -> (* We do not store paired uids when checking for reverse module-type inclusion as it would introduce duplicates. *) () | { Directionality.pos; _} -> let paired_uids = let elt1, elt2 = paired_uids in match pos with | Negative -> (Cmt_format.Declaration_to_declaration, elt2, elt1) | Positive -> (Cmt_format.Declaration_to_declaration, elt1, elt2) | Strictly_positive -> (Cmt_format. Definition_to_declaration, elt1, elt2) in Cmt_format.record_declaration_dependency paired_uids end; let runtime_coercions = if present_at_runtime then [pos,x] else [] in Sign_diff.{ empty with deep_modifications; runtime_coercions } | Error { error; recoverable=_ } -> Sign_diff.{ empty with errors=[id,error]; deep_modifications } in let continue = match item with | Ok _ -> true | Error x -> x.recoverable in let rest = if continue then signature_components ~core ~direction ~loc old_env env subst orig_shape shape_map rem else Sign_diff.{ empty with leftovers=rem } in Sign_diff.merge first rest and module_declarations ~direction ~loc env subst id1 md1 md2 orig_shape = Builtin_attributes.check_alerts_inclusion ~def:md1.md_loc ~use:md2.md_loc loc md1.md_attributes md2.md_attributes (Ident.name id1); let p1 = Path.Pident id1 in if Directionality.mark_as_used direction then Env.mark_module_used md1.md_uid; strengthened_modtypes ~direction ~loc ~aliasable:true env subst md1.md_type p1 md2.md_type orig_shape (* Inclusion between module type specifications *) and modtype_infos ~core ~direction ~loc env subst id info1 info2 = Builtin_attributes.check_alerts_inclusion ~def:info1.mtd_loc ~use:info2.mtd_loc loc info1.mtd_attributes info2.mtd_attributes (Ident.name id); let info2 = Subst.modtype_declaration Keep subst info2 in let r = match (info1.mtd_type, info2.mtd_type) with (None, None) -> Ok Tcoerce_none | (Some _, None) -> Ok Tcoerce_none | (Some mty1, Some mty2) -> check_modtype_equiv ~core ~direction ~loc env mty1 mty2 | (None, Some mty2) -> let mty1 = Mty_ident(Path.Pident id) in check_modtype_equiv ~core ~direction ~loc env mty1 mty2 in match r with | Ok _ as ok -> ok | Error e -> Error Error.(Module_type_declaration (diff info1 info2 e)) and check_modtype_equiv ~core ~direction ~loc env mty1 mty2 = let nested_eq = direction.Directionality.in_eq in let direction = Directionality.enter_eq direction in let c1 = modtypes ~core ~direction ~loc env Subst.identity mty1 mty2 Shape.dummy_mod in let c2 = (* For nested module type paths, we check only one side of the equivalence: the outer module type is the one responsible for checking the other side of the equivalence. *) if nested_eq then None else let direction = Directionality.negate direction in Some ( modtypes ~core ~direction ~loc env Subst.identity mty2 mty1 Shape.dummy_mod ) in match c1, c2 with | Ok (Tcoerce_none, _), (Some Ok (Tcoerce_none, _)|None) -> Ok Tcoerce_none | Ok (c1, _), (Some Ok _ | None) -> (* Format.eprintf "@[c1 = %a@ c2 = %a@]@." print_coercion _c1 print_coercion _c2; *) Error Error.(Illegal_permutation c1) | Ok _, Some Error e -> Error Error.(Not_greater_than e) | Error e, (Some Ok _ | None) -> Error Error.(Not_less_than e) | Error less_than, Some Error greater_than -> Error Error.(Incomparable {less_than; greater_than}) (* Simplified inclusion check between module types (for Env) *) let core_inclusion = Core_inclusion.{ type_declarations; value_descriptions; extension_constructors; class_type_declarations; class_declarations; } let core_consistency = let type_declarations ~loc:_ env ~direction:_ _ _ d1 d2 = match Includecore.type_declarations_consistency env d1 d2 with | None -> Ok Tcoerce_none | Some err -> Error Error.(Core(Type_declarations (diff d1 d2 err))) in let value_descriptions ~loc:_ env ~direction:_ _ _ vd1 vd2 = match Includecore.value_descriptions_consistency env vd1 vd2 with | x -> Ok x | exception Includecore.Dont_match err -> Error Error.(Core (Value_descriptions (diff vd1 vd2 err))) in let accept ~loc:_ _env ~direction:_ _subst _id _d1 _d2 = Ok Tcoerce_none in { type_declarations; value_descriptions; class_declarations=accept; class_type_declarations=accept; extension_constructors=accept; } type explanation = Env.t * Error.all exception Error of explanation type application_name = | Anonymous_functor | Full_application_path of Longident.t | Named_leftmost_functor of Longident.t exception Apply_error of { loc : Location.t ; env : Env.t ; app_name : application_name ; mty_f : module_type ; args : (Error.functor_arg_descr * module_type) list ; } let check_modtype_inclusion_raw ~loc env mty1 path1 mty2 = let aliasable = Env.is_aliasable path1 env in let direction = Directionality.unknown ~mark:true in strengthened_modtypes ~core:core_inclusion ~direction ~loc ~aliasable env Subst.identity mty1 path1 mty2 Shape.dummy_mod |> Result.map fst let check_modtype_inclusion ~loc env mty1 path1 mty2 = match check_modtype_inclusion_raw ~loc env mty1 path1 mty2 with | Ok _ -> None | Error e -> Some (env, Error.In_Module_type e) let check_functor_application_in_path ~errors ~loc ~lid_whole_app ~f0_path ~args ~arg_path ~arg_mty ~param_mty env = match check_modtype_inclusion_raw ~loc env arg_mty arg_path param_mty with | Ok _ -> () | Error _errs -> if errors then let prepare_arg (arg_path, arg_mty) = let aliasable = Env.is_aliasable arg_path env in let smd = Mtype.strengthen ~aliasable env arg_mty arg_path in (Error.Named arg_path, smd) in let mty_f = (Env.find_module f0_path env).md_type in let args = List.map prepare_arg args in let app_name = Full_application_path lid_whole_app in raise (Apply_error {loc; env; app_name; mty_f; args}) else raise Not_found let () = Env.check_functor_application := check_functor_application_in_path (* Check that an implementation of a compilation unit meets its interface. *) let compunit env ~mark impl_name impl_sig intf_name intf_sig unit_shape = let loc = Location.in_file impl_name in let direction = Directionality.strictly_positive ~mark in match signatures ~core:core_inclusion ~direction ~loc env Subst.identity impl_sig intf_sig unit_shape with Result.Error reasons -> let cdiff = Error.In_Compilation_unit(Error.diff impl_name intf_name reasons) in raise(Error(env, cdiff)) | Ok x -> x (* Functor diffing computation: The diffing computation uses the internal typing function *) module Functor_inclusion_diff = struct module Defs = struct type left = Types.functor_parameter type right = left type eq = Typedtree.module_coercion type diff = (Types.functor_parameter, unit) Error.functor_param_symptom type state = { res: module_type option; env: Env.t; subst: Subst.t; } end open Defs module Diff = Diffing.Define(Defs) let param_name = function | Named(x,_) -> x | Unit -> None let weight: Diff.change -> _ = function | Insert _ -> 10 | Delete _ -> 10 | Change _ -> 10 | Keep (param1, param2, _) -> begin match param_name param1, param_name param2 with | None, None -> 0 | Some n1, Some n2 when String.equal (Ident.name n1) (Ident.name n2) -> 0 | Some _, Some _ -> 1 | Some _, None | None, Some _ -> 1 end let keep_expansible_param = function | Mty_ident _ | Mty_alias _ as mty -> Some mty | Mty_signature _ | Mty_functor _ -> None let lookup_expansion { env ; res ; _ } = match res with | None -> None | Some res -> match retrieve_functor_params env res with | { params = []; _ } -> None | { params; res} -> let more = Array.of_list params in Some (keep_expansible_param res, more) let expand_params state = match lookup_expansion state with | None -> state, [||] | Some (res, expansion) -> { state with res }, expansion (* Whenever we have a named parameter that doesn't match it anonymous counterpart, we add it to the typing environment because it may contain useful abbreviations, but without adding any equations *) let bind id arg state = let arg' = Subst.modtype Keep state.subst arg in let env = Env.add_module id Mp_present arg' state.env in { state with env } let rec update (d:Diff.change) st = match d with | Insert (Unit | Named (None,_)) | Delete (Unit | Named (None,_)) | Keep (Unit,_,_) | Keep (_,Unit,_) -> (* No named abstract parameters: we keep the same environment *) st, [||] | Insert (Named (Some id, arg)) | Delete (Named (Some id, arg)) -> (* one named parameter to bind *) st |> bind id arg |> expand_params | Change (delete, insert, _) -> (* Change should be delete + insert: we add both abstract parameters to the environment without equating them. *) let st, _expansion = update (Diffing.Delete delete) st in update (Diffing.Insert insert) st | Keep (Named (name1, _), Named (name2, arg2), _) -> let arg = Subst.modtype Keep st.subst arg2 in let env, subst = equate_one_functor_param st.subst st.env arg name1 name2 in expand_params { st with env; subst } let diff env (l1,res1) (l2,_) = let module Compute = Diff.Left_variadic(struct let test st mty1 mty2 = let loc = Location.none in let res, _, _ = let direction=Directionality.unknown ~mark:false in functor_param ~core:core_inclusion ~direction ~loc st.env st.subst mty1 mty2 in res let update = update let weight = weight end) in let param1 = Array.of_list l1 in let param2 = Array.of_list l2 in let state = { env; subst = Subst.identity; res = keep_expansible_param res1} in Compute.diff state param1 param2 end module Functor_app_diff = struct module I = Functor_inclusion_diff module Defs= struct type left = Error.functor_arg_descr * Types.module_type type right = Types.functor_parameter type eq = Typedtree.module_coercion type diff = (Error.functor_arg_descr, unit) Error.functor_param_symptom type state = I.Defs.state end module Diff = Diffing.Define(Defs) let weight: Diff.change -> _ = function | Insert _ -> 10 | Delete _ -> 10 | Change _ -> 10 | Keep (param1, param2, _) -> (* We assign a small penalty to named arguments with non-matching names *) begin let desc1 : Error.functor_arg_descr = fst param1 in match desc1, I.param_name param2 with | (Unit | Empty_struct | Anonymous) , None -> 0 | Named (Path.Pident n1), Some n2 when String.equal (Ident.name n1) (Ident.name n2) -> 0 | Named _, Some _ -> 1 | Named _, None | (Unit | Empty_struct | Anonymous), Some _ -> 1 end let update (d: Diff.change) (st:Defs.state) = let open Error in match d with | Insert (Unit|Named(None,_)) | Delete _ (* delete is a concrete argument, not an abstract parameter*) | Keep ((Unit,_),_,_) (* Keep(Unit,_) implies Keep(Unit,Unit) *) | Keep (_,(Unit|Named(None,_)),_) | Change (_,(Unit|Named (None,_)), _ ) -> (* no abstract parameters to add, nor any equations *) st, [||] | Insert(Named(Some param, param_ty)) | Change(_, Named(Some param, param_ty), _ ) -> (* Change is Delete + Insert: we add the Inserted parameter to the environment to track equalities with external components that the parameter might add. *) let mty = Subst.modtype Keep st.subst param_ty in let env = Env.add_module ~noalias:true param Mp_present mty st.env in I.expand_params { st with env } | Keep ((Named arg, _mty) , Named (Some param, _param), _) -> let res = Option.map (fun res -> let scope = Ctype.create_scope () in let subst = Subst.add_module param arg Subst.identity in Subst.modtype (Rescope scope) subst res ) st.res in let subst = Subst.add_module param arg st.subst in I.expand_params { st with subst; res } | Keep (((Anonymous|Empty_struct), mty), Named (Some param, _param), _) -> let mty' = Subst.modtype Keep st.subst mty in let env = Env.add_module ~noalias:true param Mp_present mty' st.env in let res = Option.map (Mtype.nondep_supertype env [param]) st.res in I.expand_params { st with env; res} let diff env ~f ~args = let {Error.params; res} = retrieve_functor_params env f in let module Compute = Diff.Right_variadic(struct let update = update let test (state:Defs.state) (arg,arg_mty) param = let loc = Location.none in let res = match (arg:Error.functor_arg_descr), param with | (Unit|Empty_struct), Unit -> Ok Tcoerce_none | Unit, Named _ | (Anonymous | Named _), Unit -> Result.Error (Error.Incompatible_params(arg,param)) | ( Anonymous | Named _ | Empty_struct ), Named (_, param) -> let direction=Directionality.unknown ~mark:false in match modtypes ~core:core_inclusion ~direction ~loc state.env state.subst arg_mty param Shape.dummy_mod with | Error mty -> Result.Error (Error.Mismatch mty) | Ok (cc, _) -> Ok cc in res let weight = weight end) in let args = Array.of_list args in let params = Array.of_list params in let state : Defs.state = { env; subst = Subst.identity; res = I.keep_expansible_param res } in Compute.diff state args params end (* Hide the context and substitution parameters to the outside world *) let modtypes_with_shape ~shape ~loc env ~mark mty1 mty2 = (* modtypes with shape is used when typing module expressions in [Typemod] *) let direction = Directionality.strictly_positive ~mark in match modtypes ~core:core_inclusion ~direction ~loc env Subst.identity mty1 mty2 shape with | Ok (cc, shape) -> cc, shape | Error reason -> raise (Error (env, Error.(In_Module_type reason))) let modtypes_consistency ~loc env mty1 mty2 = let direction = Directionality.unknown ~mark:false in match modtypes ~core:core_consistency ~direction ~loc env Subst.identity mty1 mty2 Shape.dummy_mod with | Ok _ -> () | Error reason -> raise (Error (env, Error.(In_Module_type reason))) let modtypes ~loc env ~mark mty1 mty2 = let direction = Directionality.unknown ~mark in match modtypes ~core:core_inclusion ~direction ~loc env Subst.identity mty1 mty2 Shape.dummy_mod with | Ok (cc, _) -> cc | Error reason -> raise (Error (env, Error.(In_Module_type reason))) let gen_signatures env ~direction sig1 sig2 = match signatures ~core:core_inclusion ~direction ~loc:Location.none env Subst.identity sig1 sig2 Shape.dummy_mod with | Ok (cc, _) -> cc | Error reason -> raise (Error(env,Error.(In_Signature reason))) let signatures env ~mark sig1 sig2 = let direction = Directionality.unknown ~mark in gen_signatures env ~direction sig1 sig2 let check_implementation env impl intf = let direction = Directionality.strictly_positive ~mark:true in ignore (gen_signatures env ~direction impl intf) let type_declarations ~loc env ~mark id decl1 decl2 = let direction = Directionality.unknown ~mark in match Core_inclusion.type_declarations ~loc env ~direction Subst.identity id decl1 decl2 with | Ok _ -> () | Error (Error.Core reason) -> raise (Error(env,Error.(In_Type_declaration(id,reason)))) | Error _ -> assert false let strengthened_module_decl ~loc ~aliasable env ~mark md1 path1 md2 = let direction = Directionality.unknown ~mark in match strengthened_module_decl ~core:core_inclusion ~loc ~aliasable ~direction env Subst.identity md1 path1 md2 Shape.dummy_mod with | Ok (x, _shape) -> x | Error mdiff -> raise (Error(env,Error.(In_Module_type mdiff))) let expand_module_alias ~strengthen env path = match expand_module_alias ~strengthen env path with | Ok x -> x | Result.Error _ -> raise (Error(env,In_Expansion(Error.Unbound_module_path path))) let check_modtype_equiv ~loc env id mty1 mty2 = let direction = Directionality.unknown ~mark:true in match check_modtype_equiv ~core:core_inclusion ~loc ~direction env mty1 mty2 with | Ok _ -> () | Error e -> raise (Error(env, Error.(In_Module_type_substitution (id,diff mty1 mty2 e))) )