Source file includemod_errorprinter.ml

(**************************************************************************)
(*                                                                        *)
(*                                 OCaml                                  *)
(*                                                                        *)
(*             Florian Angeletti, projet Cambium, Inria Paris             *)
(*                                                                        *)
(*   Copyright 2021 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.          *)
(*                                                                        *)
(**************************************************************************)

module Style = Misc.Style
module Fmt = Format_doc

module Context = struct
  type pos =
    | Module of Ident.t
    | Modtype of Ident.t
    | Arg of Types.functor_parameter
    | Body of Types.functor_parameter

  let path_of_context = function
      Module id :: rem ->
        let rec subm path = function
          | [] -> path
          | Module id :: rem -> subm (Path.Pdot (path, Ident.name id)) rem
          | _ -> assert false
        in subm (Path.Pident id) rem
    | _ -> assert false


  let rec context ppf = function
      Module id :: rem ->
        Fmt.fprintf ppf "@[<2>module %a%a@]" Printtyp.ident id args rem
    | Modtype id :: rem ->
        Fmt.fprintf ppf "@[<2>module type %a =@ %a@]"
          Printtyp.ident id context_mty rem
    | Body x :: rem ->
        Fmt.fprintf ppf "functor (%s) ->@ %a" (argname x) context_mty rem
    | Arg x :: rem ->
        Fmt.fprintf ppf "functor (%s : %a) -> ..."
          (argname x) context_mty rem
    | [] ->
        Fmt.fprintf ppf "<here>"
  and context_mty ppf = function
      (Module _ | Modtype _) :: _ as rem ->
        Fmt.fprintf ppf "@[<2>sig@ %a@;<1 -2>end@]" context rem
    | cxt -> context ppf cxt
  and args ppf = function
      Body x :: rem ->
        Fmt.fprintf ppf "(%s)%a" (argname x) args rem
    | Arg x :: rem ->
        Fmt.fprintf ppf "(%s :@ %a) : ..." (argname  x) context_mty rem
    | cxt ->
        Fmt.fprintf ppf " :@ %a" context_mty cxt
  and argname = function
    | Types.Unit -> ""
    | Types.Named (None, _, _) -> "_"
    | Types.Named (Some id, _, _) -> Ident.name id

  (* Use deprecated_printer to defer path printing until render time.
     This ensures the naming context is queried after reset_naming_context()
     is called in wrap_printing_env, matching the old thunk-based behavior. *)
  let alt_pp ppf cxt =
    if cxt = [] then () else
    if List.for_all (function Module _ -> true | _ -> false) cxt then
      Fmt.fprintf ppf "in module %t,"
        (fun ppf -> Fmt.deprecated_printer (fun fmt ->
          Format.fprintf fmt "%a"
            (Fmt.compat (Style.as_inline_code Printtyp.path))
            (path_of_context cxt)
        ) ppf)
    else
      Fmt.fprintf ppf "@[<hv 2>at position@ %a,@]"
        (Style.as_inline_code context) cxt

  let pp ppf cxt =
    if cxt = [] then () else
    if List.for_all (function Module _ -> true | _ -> false) cxt then
      Fmt.fprintf ppf "In module %t:@ "
        (fun ppf -> Fmt.deprecated_printer (fun fmt ->
          Format.fprintf fmt "%a"
            (Fmt.compat (Style.as_inline_code Printtyp.path))
            (path_of_context cxt)
        ) ppf)
    else
      Fmt.fprintf ppf "@[<hv 2>At position@ %a@]@ "
        (Style.as_inline_code context) cxt
end

module Illegal_permutation = struct
  (** Extraction of information in case of illegal permutation
      in a module type *)

  (** When examining coercions, we only have runtime component indices,
      we use thus a limited version of {!pos}. *)
  type coerce_pos =
    | Item of int
    | InArg
    | InBody

  let either f x g y = match f x with
    | None -> g y
    | Some _ as v -> v

  (** We extract a lone transposition from a full tree of permutations. *)
  let rec transposition_under path (coerc:Typedtree.module_coercion) =
    match coerc with
    | Tcoerce_structure { pos_cc_list; _ } ->
        either
          (not_fixpoint path 0) pos_cc_list
          (first_non_id path 0) pos_cc_list
    | Tcoerce_functor(arg,res) ->
        either
          (transposition_under (InArg::path)) arg
          (transposition_under (InBody::path)) res
    | Tcoerce_none -> None
    | Tcoerce_alias _ | Tcoerce_primitive _ ->
        (* these coercions are not inversible, and raise an error earlier when
           checking for module type equivalence *)
        assert false
  (* we search the first point which is not invariant at the current level *)
  and not_fixpoint path pos = function
    | [] -> None
    | (n, _) :: q ->
        if n = pos then
          not_fixpoint path (pos+1) q
        else
          Some(List.rev path, pos, n)
  (* we search the first item with a non-identity inner coercion *)
  and first_non_id path pos = function
    | [] -> None
    | (_, Typedtree.Tcoerce_none) :: q -> first_non_id path (pos + 1) q
    | (_,c) :: q ->
        either
          (transposition_under (Item pos :: path)) c
          (first_non_id path (pos + 1)) q

  let transposition c =
    match transposition_under [] c with
    | None -> raise Not_found
    | Some x -> x

  let rec runtime_item k = function
    | [] -> raise Not_found
    | item :: q ->
        if not(Includemod.is_runtime_component item) then
          runtime_item k q
        else if k = 0 then
          item
        else
          runtime_item (k-1) q

  (* Find module type at position [path] and convert the [coerce_pos] path to
     a [pos] path *)
  let rec find env ctx path (mt:Types.module_type) =
    match Mtype.scrape_alias env mt, path with
    | Mty_signature s , [] -> List.rev ctx, s
    | Mty_signature s, Item k :: q ->
        begin match runtime_item k s with
        | Sig_module (id, _, md,_,_) ->
            find env (Context.Module id :: ctx) q md.md_type
        | _ -> raise Not_found
        end
    | Mty_functor(Named (_,mt,_) as arg,_,_), InArg :: q ->
        find env (Context.Arg arg :: ctx) q mt
    | Mty_functor(arg, mt,_), InBody :: q ->
        find env (Context.Body arg :: ctx) q mt
    | _ -> raise Not_found

  let find env path mt = find env [] path mt
  let item mt k = Includemod.item_ident_name (runtime_item k mt)

  let pp_item ppf (id,_,kind) =
    Fmt.fprintf ppf "%s %a"
      (Includemod.kind_of_field_desc kind)
      Style.inline_code (Ident.name id)

  let pp ctx_printer env ppf (mty,c) =
    try
      let p, k, l = transposition c in
      let ctx, mt = find env p mty in
      Fmt.fprintf ppf
        "@[<hv 2>Illegal permutation of runtime components in a module type.@ \
         @[For example,@ %a@]@ @[the %a@ and the %a are not in the same order@ \
         in the expected and actual module types.@]@]"
        ctx_printer ctx pp_item (item mt k) pp_item (item mt l)
    with Not_found -> (* this should not happen *)
      Fmt.fprintf ppf
        "Illegal permutation of runtime components in a module type."

end



module Err = Includemod.Error

let is_big p =
  let size = !Clflags.error_size in
  let format_p ppf = Fmt.Doc.format ppf (Fmt.doc_printf "%t" p) in
  size > 0 && Misc.is_print_longer_than size format_p

let show_loc msg ppf loc =
  let pos = loc.Location.loc_start in
  if List.mem pos.Lexing.pos_fname [""; "_none_"; "//toplevel//"] then ()
  else Fmt.fprintf ppf "@\n@[<2>%a:@ %s@]"
    (Location.Doc.loc ~capitalize_first:true) loc msg

let show_locs ppf (loc1, loc2) =
  show_loc "Expected declaration" ppf loc2;
  show_loc "Actual declaration" ppf loc1


let dmodtype mty =
  let tmty = Printtyp.tree_of_modtype ~abbrev:true mty in
  Fmt.dprintf "%a" !Oprint.out_module_type tmty

let space ppf () = Fmt.fprintf ppf "@ "


(** Checks if the error is a mode error at the leaf node, and returns the
  offending axis. *)
module Is_modal = struct
  open Err
  let rec module_type_symptom = function
    | Mode e ->
       let Mode.Value.Error (ax, _) = Mode.Value.to_simple_error e in
        Some (Mode.Value.Axis.P ax)
    | Signature s -> signature_symptom s
    | Functor _ | Invalid_module_alias _ | After_alias_expansion _ | Mt_core _
      -> None

  and signature_symptom {incompatibles} =
    List.find_map (fun (_, s) -> sigitem_symptom s)
      incompatibles

  and sigitem_symptom = function
    | Core s -> core_sigitem_symptom s
    | Module_type d -> module_type_symptom d.symptom
    | Module_type_declaration _ -> None

  and core_sigitem_symptom = function
    | Value_descriptions d -> value_mismatch d.symptom
    | Class_declarations d -> class_declaration_symptom d.symptom
    | Type_declarations _ | Extension_constructors _ | Class_type_declarations _
    | Modalities _ | Jkind_declarations _ -> None

  and class_declaration_symptom = function
    | Class_mode e ->
        let Mode.Value.Error (ax, _) = Mode.Value.to_simple_error e in
        Some (Mode.Value.Axis.P ax)
    | Class_type _ -> None

  and value_mismatch : Includecore.value_mismatch -> _ = function
    | Mode e ->
        let Mode.Value.Error (ax, _) = Mode.Value.to_simple_error e in
        Some (Mode.Value.Axis.P ax)
    | _ -> None

  and functor_param_symptom = function
    | Incompatible_params _ -> None
    | Mismatch d -> module_type_symptom d.symptom

  and functor_params_symptom = function
    | Incompatible -> None
    | Param d -> functor_param_symptom d
end

let zap_axis_to_floor
  : type a. a Mode.Value.Axis.t -> Mode.Value.l -> a
  = fun ax m ->
  match ax with
  | Comonadic ax ->
      Mode.Value.Comonadic.Per_axis.zap_to_floor ax
        (Mode.Value.proj_comonadic ax m)
  | Monadic ax ->
      Mode.Value.Monadic.Per_axis.zap_to_floor ax
        (Mode.Value.proj_monadic ax m)

let zap_axis_to_ceil
  : type a. a Mode.Value.Axis.t -> Mode.Value.r -> a
  = fun ax m ->
  match ax with
  | Comonadic ax ->
      Mode.Value.Comonadic.Per_axis.zap_to_ceil ax
        (Mode.Value.proj_comonadic ax m)
  | Monadic ax ->
      Mode.Value.Monadic.Per_axis.zap_to_ceil ax
        (Mode.Value.proj_monadic ax m)

let print_out_mode
: type a. ?in_structure:_ -> a Mode.Value.Axis.t -> a -> _ -> _
= fun ?(in_structure=false) ax mode ->
  let print = Mode.Value.Const.print_axis ax in
  if in_structure then
    fun ppf -> Fmt.fprintf ppf " (* in a structure at %a *)" print mode
  else
    fun ppf -> Fmt.fprintf ppf " @@ %a" print mode

let maybe_print_mode_l ~is_modal mode =
  let mode = Mode.Value.disallow_right mode in
  match is_modal with
  | None -> fun _ppf -> ()
  | Some ax ->
      let (P ax) : Mode.Value.Axis.packed = ax in
      let mode =
        mode
        (* error printing, so mutation doesn't need to be backtracked *)
        |> zap_axis_to_floor ax
      in
      print_out_mode ax mode

let maybe_print_mode_r ~is_modal mode =
  let mode = Mode.Value.disallow_left mode in
  match is_modal with
  | None -> fun _ppf -> ()
  | Some ax ->
      let (P ax) : Mode.Value.Axis.packed = ax in
      let mode = mode |> zap_axis_to_ceil ax in
      print_out_mode ax mode

let print_modes ?in_structure ax (modes : Includemod.modes) =
  let (P ax) : Mode.Value.Axis.packed = ax in
  let mode1, mode2 =
    match modes with
    | All -> assert false
    | Specific ((mode1, _), mode2) ->
        Mode.Value.disallow_right mode1, Mode.Value.disallow_left mode2
  in
  let mode1 =
    mode1
    (* error printing, so mutation doesn't need to be backtracked *)
    |> zap_axis_to_floor ax
  in
  let mode2 =
    mode2
    |> zap_axis_to_ceil ax
  in
  print_out_mode ?in_structure ax mode1, print_out_mode ?in_structure ax mode2

let maybe_print_modes ?in_structure ~is_modal (modes : Includemod.modes) =
  match is_modal with
  | None -> (fun _ppf -> ()), (fun _ppf -> ())
  | Some ax -> print_modes ?in_structure ax modes

let dthen_mode_l ~is_modal mm t =
  Fmt.dprintf "%t%t" t (maybe_print_mode_l ~is_modal mm)

let maybe_print_alloc_mode_r ~is_modal mm =
  let mm = Mode.alloc_as_value mm in
  maybe_print_mode_r ~is_modal mm

let dthen_alloc_mode_r ~is_modal mm t =
  Fmt.dprintf "%t%t" t (maybe_print_alloc_mode_r ~is_modal mm)

(**
   In order to display a list of functor arguments in a compact format,
   we introduce a notion of shorthand for functor arguments.
   The aim is to first present the lists of actual and expected types with
   shorthands:

     (X: $S1) (Y: $S2) (Z: An_existing_module_type) ...
   does not match
     (X: $T1) (Y: A_real_path) (Z: $T3) ...

   and delay the full display of the module types corresponding to $S1, $S2,
   $T1, and $T3 to the suberror message.

*)
module With_shorthand = struct

  (** A item with a potential shorthand name *)
  type 'a named = {
    item: 'a;
    name : string;
  }

  type 'a t =
    | Original of 'a (** The shorthand has been discarded *)
    | Synthetic of 'a named
    (** The shorthand is potentially useful *)

  type functor_param =
    | Unit
    | Named of (Ident.t option * Types.module_type t * Mode.Alloc.lr)

  (** Shorthand generation *)
  type kind =
    | Got
    | Expected
    | Unneeded

  type variant =
    | App
    | Inclusion

  let elide_if_app ctx s = match ctx with
    | App -> Unneeded
    | Inclusion -> s

  let make side pos =
    match side with
    | Got -> Fmt.asprintf "$S%d" pos
    | Expected -> Fmt.asprintf "$T%d" pos
    | Unneeded -> "..."

  (** Add shorthands to a patch *)
  open Diffing
  let patch ctx p =
    let add_shorthand side pos mty =
      {name = (make side pos); item = mty }
    in
    let aux i d =
      let pos = i + 1 in
      let d = match d with
        | Insert mty ->
            Insert (add_shorthand Expected pos mty)
        | Delete mty ->
            Delete (add_shorthand (elide_if_app ctx Got) pos mty)
        | Change (g, e, p) ->
            Change
              (add_shorthand Got pos g,
               add_shorthand Expected pos e, p)
        | Keep (g, e, p) ->
            Keep (add_shorthand Got pos g,
                          add_shorthand (elide_if_app ctx Expected) pos e, p)
      in
      pos, d
    in
    List.mapi aux p

  (** Shorthand computation from named item *)
  let modtype (r : _ named) = match r.item with
    | Types.Mty_ident _
    | Types.Mty_alias _
    | Types.Mty_signature []
    | Types.Mty_for_hole
    | Types.Mty_strengthen _
      -> Original r.item
    | Types.Mty_signature _ | Types.Mty_functor _
      -> Synthetic r

  let functor_param (ua : _ named) = match ua.item with
    | Types.Unit -> Unit
    | Types.Named (from, mty, mm) ->
        Named (from, modtype { ua with item = mty }, mm)

  (** Printing of arguments with shorthands *)
  let pp ppx = function
    | Original x -> ppx x
    | Synthetic s -> Fmt.dprintf "%s" s.name

  let pp_orig ppx = function
    | Original x | Synthetic { item=x; _ } -> ppx x

  let definition ~is_modal x = match functor_param x with
    | Unit -> Fmt.dprintf "()"
    | Named(_,short_mty, mm) ->
        match short_mty with
        | Original mty -> dmodtype mty |> dthen_alloc_mode_r ~is_modal mm
        | Synthetic {name; item = mty} ->
            Fmt.dprintf
              "%s@ =@ %t" name (dmodtype mty)
            |> dthen_alloc_mode_r ~is_modal mm

  let param ~is_modal x = match functor_param x with
    | Unit -> Fmt.dprintf "()"
    | Named (_, short_mty, mm) ->
        pp dmodtype short_mty
        |> dthen_alloc_mode_r ~is_modal mm

  let qualified_param ~is_modal x = match functor_param x with
    | Unit -> Fmt.dprintf "()"
    | Named (None, Original (Mty_signature []), mm) ->
        Fmt.dprintf "(sig end%t)"
          (maybe_print_alloc_mode_r ~is_modal mm)
    | Named (None, short_mty, mm) ->
        pp dmodtype short_mty
        |> dthen_alloc_mode_r ~is_modal mm
    | Named (Some p, short_mty, mm) ->
        Fmt.dprintf "(%s : %t)"
          (Ident.name p) (pp dmodtype short_mty
          |> dthen_alloc_mode_r ~is_modal mm)

  let definition_of_argument ~is_modal ua =
    let arg, mty, (mode, _locks) = ua.item in
    match (arg: Err.functor_arg_descr) with
    | Unit -> Fmt.dprintf "()"
    | Empty_struct ->
        Fmt.dprintf "(struct end%t)" (maybe_print_mode_l ~is_modal mode)
    | Named p ->
        let mty = match mty with
          | Types.Mty_strengthen (mty,q,_) when Path.same p q -> mty
          | _ -> mty
        in
        let mty = modtype { ua with item = mty } in
        Fmt.dprintf
          "%a@ :@ %t"
          Printtyp.path p
          (pp_orig dmodtype mty)
        |> dthen_mode_l ~is_modal mode
    | Anonymous ->
        let short_mty = modtype { ua with item = mty } in
        begin match short_mty with
        | Original mty -> dmodtype mty |> dthen_mode_l ~is_modal mode
        | Synthetic {name; item=mty} ->
            Fmt.dprintf "%s@ :@ %t" name (dmodtype mty)
            |> dthen_mode_l ~is_modal mode
        end

  let arg ~is_modal ua =
    let arg, mty, (mode, _locks) = ua.item in
    match (arg: Err.functor_arg_descr) with
    | Unit -> Fmt.dprintf "()"
    | Empty_struct ->
        Fmt.dprintf "(struct end%t)" (maybe_print_mode_l ~is_modal mode)
    | Named p -> fun ppf -> Printtyp.path ppf p
    | Anonymous ->
        let short_mty = modtype { ua with item=mty } in
        pp dmodtype short_mty
        |> dthen_mode_l ~is_modal mode
end


module Functor_suberror = struct
  open Err

  let param_id x = match x.With_shorthand.item with
    | Types.Named (Some _ as x,_,_) -> x
    | Types.(Unit | Named(None,_,_)) -> None

  (** Print the list of params with style *)
  let pretty_params sep proj printer patch =
    let elt (x,param) =
      let sty = Diffing.(style @@ classify x) in
      Fmt.dprintf "%a%t%a"
        Fmt.pp_open_stag (Style.Style sty)
        (printer param)
        Fmt.pp_close_stag ()
    in
    let params = List.filter_map proj @@ List.map snd patch in
    Printtyp.functor_parameters ~sep elt params

  let expected ~is_modal d =
    let extract: _ Diffing.change -> _ = function
      | Insert mty
      | Keep(_,mty,_)
      | Change (_,mty,_) as x ->
          Some (param_id mty,(x, mty))
      | Delete _ -> None
    in
    pretty_params space extract (With_shorthand.qualified_param ~is_modal) d

  let drop_inserted_suffix patch =
    let rec drop = function
      | Diffing.Insert _ :: q -> drop q
      | rest -> List.rev rest in
    drop (List.rev patch)

  let prepare_patch ~drop ~ctx patch =
    let drop_suffix x = if drop then drop_inserted_suffix x else x in
    patch |> drop_suffix |> With_shorthand.patch ctx


  module Inclusion = struct

    let got ~is_modal d =
      let extract: _ Diffing.change -> _ = function
      | Delete mty
      | Keep (mty,_,_)
      | Change (mty,_,_) as x ->
          Some (param_id mty,(x,mty))
      | Insert _ -> None
      in
      pretty_params space extract (With_shorthand.qualified_param ~is_modal) d

    let insert mty =
      Fmt.dprintf
        "An argument appears to be missing with module type@;<1 2>@[%t@]"
        (With_shorthand.definition ~is_modal:None mty)

    let delete mty =
      Fmt.dprintf
        "An extra argument is provided of module type@;<1 2>@[%t@]"
        (With_shorthand.definition ~is_modal:None mty)

      let ok x y =
        Fmt.dprintf
          "Module types %t and %t match"
          (With_shorthand.param ~is_modal:None x)
          (With_shorthand.param ~is_modal:None y)

      let diff ~is_modal g e more =
        let g = With_shorthand.definition ~is_modal g in
        let e = With_shorthand.definition ~is_modal e in
        (* Use deprecated_printer to defer evaluation of [more ()] until print
           time. This ensures that conflicts are registered by printing [g] and
           [e] before [print_explanations] is called inside [more ()]. *)
        Fmt.dprintf
          "Module types do not match:@ @[%t@]@;<1 -2>does not include@ \
           @[%t@]%t"
          g e (fun ppf ->
            Fmt.deprecated_printer (fun fmt ->
              let rdoc = ref Fmt.Doc.empty in
              (more ()) (Fmt.formatter rdoc);
              Fmt.Doc.format fmt !rdoc
            ) ppf)

      let incompatible = function
        | Types.Unit ->
            Fmt.dprintf
              "The functor was expected to be applicative at this position"
        | Types.Named _ ->
            Fmt.dprintf
              "The functor was expected to be generative at this position"

      let patch env got expected =
        Includemod.Functor_inclusion_diff.diff env got expected
        |> prepare_patch ~drop:false ~ctx:Inclusion

    end

  module App = struct

    let patch env ~f ~args =
      Includemod.Functor_app_diff.diff env ~f ~args
      |> prepare_patch ~drop:true ~ctx:App

    let got ~is_modal d =
      let extract: _ Diffing.change -> _ = function
        | Delete mty
        | Keep (mty,_,_)
        | Change (mty,_,_) as x ->
            Some (None,(x,mty))
        | Insert _ -> None
      in
      pretty_params space extract (With_shorthand.arg ~is_modal) d

    let delete mty =
      Fmt.dprintf
        "The following extra argument is provided@;<1 2>@[%t@]"
        (With_shorthand.definition_of_argument ~is_modal:None mty)

    let insert = Inclusion.insert

    let ok x y =
      let pp_orig_name = match With_shorthand.functor_param y with
        | With_shorthand.Named (_, Original mty, _) ->
            Fmt.dprintf " %t" (dmodtype mty)
        | _ -> ignore
      in
      Fmt.dprintf
        "Module %t matches the expected module type%t"
        (With_shorthand.arg ~is_modal:None x)
        pp_orig_name

    let diff ~is_modal g e more =
      let g = With_shorthand.definition_of_argument ~is_modal g in
      let e = With_shorthand.definition ~is_modal e in
      Fmt.dprintf
        "Modules do not match:@ @[%t@]@;<1 -2>\
         is not included in@ @[%t@]%t"
        g e (fun ppf ->
          Fmt.deprecated_printer (fun fmt ->
              let rdoc = ref Fmt.Doc.empty in
              (more ()) (Fmt.formatter rdoc);
              Fmt.Doc.format fmt !rdoc
            ) ppf)

    (** Specialized to avoid introducing shorthand names
        for single change difference
    *)
    let single_diff ~is_modal g e more =
      let _arg, mty1, (mode1, _) = g.With_shorthand.item in
      let mty1_with_mode = dmodtype mty1 |> dthen_mode_l ~is_modal mode1 in
      let mty2_with_mode =
        match e.With_shorthand.item with
        | Types.Unit -> Fmt.dprintf "()"
        | Types.Named(_, mty, mm) ->
            dmodtype mty |> dthen_alloc_mode_r ~is_modal mm
      in
      Fmt.dprintf
        "Modules do not match:@ @[%t@]@;<1 -2>\
         is not included in@ @[%t@]%t"
        mty1_with_mode mty2_with_mode (fun ppf ->
          Fmt.deprecated_printer (fun fmt ->
              let rdoc = ref Fmt.Doc.empty in
              (more ()) (Fmt.formatter rdoc);
              Fmt.Doc.format fmt !rdoc
            ) ppf)


    let incompatible = function
      | Unit ->
          Fmt.dprintf
            "The functor was expected to be applicative at this position"
      | Named _ | Anonymous ->
          Fmt.dprintf
            "The functor was expected to be generative at this position"
      | Empty_struct ->
          (* an empty structure can be used in both applicative and generative
             context *)
          assert false
  end

  let subcase sub ~expansion_token env (pos, diff) =
    Location.msg "%a%a%a%a@[<hv 2>%t@]%a"
      Fmt.pp_print_tab ()
      Fmt.pp_open_tbox ()
      Diffing.prefix (pos, Diffing.classify diff)
      Fmt.pp_set_tab ()
      (Printtyp.wrap_printing_env env ~error:true
         (fun () -> sub ~expansion_token env diff)
      )
     Fmt.pp_close_tbox ()

  let onlycase sub ~expansion_token env (_, diff) =
    Location.msg "%a@[<hv 2>%t@]"
      Fmt.pp_print_tab ()
      (Printtyp.wrap_printing_env env ~error:true
         (fun () -> sub ~expansion_token env diff)
      )

  let params sub ~expansion_token env l =
    let rec aux subcases = function
      | [] -> subcases
      | (_, Diffing.Keep _) as a :: q ->
          aux (subcase sub ~expansion_token env a :: subcases) q
      | a :: q ->
          List.fold_left (fun acc x ->
            (subcase sub ~expansion_token:false env x) :: acc
            )
            (subcase sub ~expansion_token env a :: subcases)
            q
    in
    match l with
    | [a] -> [onlycase sub ~expansion_token env a]
    | l -> aux [] l
end


(** Construct a linear presentation of the error tree *)

open Err

(* Context helper functions *)
let with_context ?loc ctx printer diff =
  Location.msg ?loc "%a%a" Context.pp (List.rev ctx)
    printer diff

let dwith_context ?loc ctx printer =
  Location.msg ?loc "%a%t" Context.pp (List.rev ctx) printer

let dwith_context_and_elision ?loc ctx print_diff =
  if is_big print_diff then
    Location.msg ?loc "..."
  else
    dwith_context ?loc ctx print_diff

(* Merge sub msgs into one printer *)
let coalesce msgs =
  match List.rev msgs with
  | [] -> ignore
  | before ->
      let ctx ppf =
        Fmt.pp_print_list ~pp_sep:space
          (fun ppf x -> Fmt.pp_doc ppf x.Location.txt)
          ppf before in
      ctx

let subcase_list l ppf = match l with
  | [] -> ()
  | _ :: _ ->
      let pp_msg ppf lmsg = Fmt.pp_doc ppf lmsg.Location.txt in
      Fmt.fprintf ppf "@;<1 -2>@[%a@]"
        (Fmt.pp_print_list ~pp_sep:space pp_msg)
        (List.rev l)

(* Printers for leaves *)
let core env id x =
  match x with
  | Err.Value_descriptions {symptom = Modality e} ->
      Fmt.dprintf "@[<hv>%s:@;%a@]"
        ("Modalities on " ^ (Ident.name id) ^ " do not match")
        (Includecore.report_modality_sub_error "the first" "the second") e
  | Err.Value_descriptions diff ->
      let is_modal = Is_modal.value_mismatch diff.symptom in
      let mode1, mode2 =
        maybe_print_modes ~in_structure:true ~is_modal diff.modes
      in
      Fmt.dprintf "@[<v>@[<hv>%s:@;<1 2>%a%t@ %s@;<1 2>%a%t@]%a%a%t@]"
        "Values do not match"
        !Oprint.out_sig_item
        (Printtyp.tree_of_value_description id diff.got)
        mode1
        "is not included in"
        !Oprint.out_sig_item
        (Printtyp.tree_of_value_description id diff.expected)
        mode2
        (Includecore.report_value_mismatch
           ~pp:(diff.got.val_loc, Structure_item (Value, id))
           "the first" "the second" env) diff.symptom
        show_locs (diff.got.val_loc, diff.expected.val_loc)
        Printtyp.Conflicts.print_explanations
  | Err.Modalities e ->
      Fmt.dprintf "@[<hv>%s:@;%a@]"
        ("Modalities on " ^ (Ident.name id) ^ " do not match")
        (Includecore.report_modality_sub_error "the first" "the second") e
  | Err.Type_declarations diff ->
      Fmt.dprintf "@[<v>@[<hv>%s:@;<1 2>%a@ %s@;<1 2>%a@]%a%a%t@]"
        "Type declarations do not match"
        !Oprint.out_sig_item
        (Printtyp.tree_of_type_declaration id diff.got Trec_first)
        "is not included in"
        !Oprint.out_sig_item
        (Printtyp.tree_of_type_declaration id diff.expected Trec_first)
        (Includecore.report_type_mismatch
           "the first" "the second" "declaration" env) diff.symptom
        show_locs (diff.got.type_loc, diff.expected.type_loc)
        Printtyp.Conflicts.print_explanations
  | Err.Extension_constructors diff ->
      Fmt.dprintf "@[<v>@[<hv>%s:@;<1 2>%a@ %s@;<1 2>%a@]@ %a%a%t@]"
        "Extension declarations do not match"
        !Oprint.out_sig_item
        (Printtyp.tree_of_extension_constructor id diff.got Text_first)
        "is not included in"
        !Oprint.out_sig_item
        (Printtyp.tree_of_extension_constructor id diff.expected Text_first)
        (Includecore.report_extension_constructor_mismatch
           "the first" "the second" "declaration" env) diff.symptom
        show_locs (diff.got.ext_loc, diff.expected.ext_loc)
        Printtyp.Conflicts.print_explanations
  | Err.Class_type_declarations diff ->
      Fmt.dprintf
        "@[<hv 2>Class type declarations do not match:@ \
         %a@;<1 -2>does not match@ %a@]@ %a%t"
        !Oprint.out_sig_item
        (Printtyp.tree_of_cltype_declaration id diff.got Trec_first)
        !Oprint.out_sig_item
        (Printtyp.tree_of_cltype_declaration id diff.expected Trec_first)
        (Includeclass.report_error_doc Type_scheme) diff.symptom
        Printtyp.Conflicts.print_explanations
  | Err.Class_declarations {got;expected;symptom=Class_type reason} ->
      let t1 = Printtyp.tree_of_class_declaration id got Trec_first in
      let t2 = Printtyp.tree_of_class_declaration id expected Trec_first in
      Fmt.dprintf
        "@[<hv 2>Class declarations do not match:@ \
         %a@;<1 -2>does not match@ %a@]@ %a%t"
        !Oprint.out_sig_item t1
        !Oprint.out_sig_item t2
        (Includeclass.report_error_doc Type_scheme) reason
        Printtyp.Conflicts.print_explanations
  | Err.Class_declarations {symptom=Class_mode e} ->
      Fmt.dprintf
        "@[<hv 2>Class declarations %s do not match:@ @]@ %a%t"
        (Ident.name id)
        (Includecore.report_mode_sub_error
           ~pp:(Location.none, Structure_item (Class, id))
           "first is" "second is") e
        Printtyp.Conflicts.print_explanations
  | Err.Jkind_declarations diff ->
      Fmt.dprintf "@[<v>@[<hv>%s:@;<1 2>%a@ %s@;<1 2>%a@]%a%a%t@]"
        "Kind declarations do not match"
        !Oprint.out_sig_item
        (Printtyp.tree_of_jkind_declaration id diff.got)
        "is not included in"
        !Oprint.out_sig_item
        (Printtyp.tree_of_jkind_declaration id diff.expected)
        (Includecore.report_jkind_mismatch "the first" "the second")
        diff.symptom show_locs (diff.got.jkind_loc, diff.expected.jkind_loc)
        Printtyp.Conflicts.print_explanations

let missing_field ppf item =
  let id, loc, kind =  Includemod.item_ident_name item in
  Fmt.fprintf ppf "The %s %a is required but not provided%a"
    (Includemod.kind_of_field_desc kind)
    (Style.as_inline_code Printtyp.ident) id
    (show_loc "Expected declaration") loc

let module_types ~env {Err.got=mty1; expected=mty2; modes; symptom}=
  Printtyp.wrap_printing_env ~error:true env @@ fun () ->
  let is_modal = Is_modal.module_type_symptom symptom in
  let mode1, mode2 = maybe_print_modes ~is_modal modes in
  Fmt.dprintf
    "@[<hv 2>Modules do not match:@ \
     %a%t@;<1 -2>is not included in@ %a%t@]"
    !Oprint.out_module_type (Printtyp.tree_of_modtype ~abbrev:true mty1)
    mode1
    !Oprint.out_module_type (Printtyp.tree_of_modtype ~abbrev:true mty2)
    mode2

let eq_module_types ~env ({Err.got=mty1; expected=mty2} : _ mdiff) =
  Printtyp.wrap_printing_env ~error:true env @@ fun () ->
  Fmt.dprintf
    "@[<hv 2>Module types do not match:@ \
     %a@;<1 -2>is not equal to@ %a@]"
    !Oprint.out_module_type (Printtyp.tree_of_modtype ~abbrev:true mty1)
    !Oprint.out_module_type (Printtyp.tree_of_modtype ~abbrev:true mty2)

let module_type_declarations id {Err.got=d1 ; expected=d2} =
  Fmt.dprintf
    "@[<hv 2>Module type declarations do not match:@ \
     %a@;<1 -2>does not match@ %a@]"
    !Oprint.out_sig_item (Printtyp.tree_of_modtype_declaration ~abbrev:true id d1)
    !Oprint.out_sig_item (Printtyp.tree_of_modtype_declaration ~abbrev:true id d2)

let interface_mismatch ppf (diff: _ Err.diff) =
  Fmt.fprintf ppf
    "The implementation %a@ does not match the interface %a:@ "
    Style.inline_code diff.got Style.inline_code diff.expected

let parameter_mismatch ppf (diff: _ Err.diff) =
  Fmt.fprintf ppf
    "The argument module %a@ does not match the parameter signature %a:@ "
    Style.inline_code diff.got Style.inline_code diff.expected

let compilation_unit_mismatch comparison ppf diff =
  match (comparison : Err.compilation_unit_comparison) with
  | Implementation_vs_interface -> interface_mismatch ppf diff
  | Argument_vs_parameter -> parameter_mismatch ppf diff

let core_module_type_symptom (x:Err.core_module_type_symptom)  =
  match x with
  | Not_an_alias | Not_an_identifier | Abstract_module_type
  | Incompatible_aliases ->
      if Printtyp.Conflicts.exists () then
        Some Printtyp.Conflicts.print_explanations
      else None
  | Unbound_module_path path ->
      Some(Fmt.dprintf "Unbound module %a"
             (Style.as_inline_code Printtyp.path) path
          )

(* Construct a linearized error message from the error tree *)

let rec module_type ~expansion_token ~eqmode ~env ~before ~ctx
  (diff : _ mdiff) =
  match diff.symptom with
  | Invalid_module_alias _ (* the difference is non-informative here *)
  | After_alias_expansion _ (* we print only the expanded module types *) ->
      module_type_symptom ~eqmode ~expansion_token ~env ~before ~ctx
        diff.symptom
  | Functor Params d -> (* We jump directly to the functor param error *)
      functor_params ~expansion_token ~env ~before ~ctx d
  | Mode _ -> (* jump directly to the module mode mismatch, without types *)
      module_type_symptom ~eqmode ~expansion_token ~env ~before ~ctx
        diff.symptom
  | _ ->
      let inner = if eqmode then eq_module_types ~env else module_types ~env in
      let next =
        match diff.symptom with
        | Mt_core _ ->
            (* In those cases, the refined error messages for the current error
               will at most add some minor comments on the current error.
               It is thus better to avoid eliding the current error message.
            *)
            dwith_context ctx (inner diff)
        | _ -> dwith_context_and_elision ctx (inner diff)
      in
      let before = next :: before in
      module_type_symptom ~eqmode ~expansion_token ~env ~before ~ctx
        diff.symptom

and module_type_symptom ~eqmode ~expansion_token ~env ~before ~ctx = function
  | Mt_core core ->
      begin match core_module_type_symptom core with
      | None -> before
      | Some msg -> Location.msg "%t" msg :: before
      end
  | Signature s -> signature ~expansion_token ~env ~before ~ctx s
  | Functor f -> functor_symptom ~expansion_token ~env ~before ~ctx f
  | After_alias_expansion diff ->
      module_type ~eqmode ~expansion_token ~env ~before ~ctx diff
  | Invalid_module_alias path ->
      let printer =
        Fmt.dprintf "Module %a cannot be aliased"
          (Style.as_inline_code Printtyp.path) path
      in
      dwith_context ctx printer :: before
  | Mode e ->
      let printer ppf =
        Includecore.report_mode_sub_error
          ~pp:(Location.none, Unknown) "Got" "expected" ppf e
      in
      dwith_context ctx printer :: before

and functor_params ~expansion_token ~env ~before ~ctx {got;expected;symptom} =
  let is_modal = Is_modal.functor_params_symptom symptom in
  let d = Functor_suberror.Inclusion.patch env got expected in
  let actual = Functor_suberror.Inclusion.got ~is_modal d in
  let expected = Functor_suberror.expected ~is_modal d in
  let main =
    Fmt.dprintf
      "@[<hv 2>Modules do not match:@ \
       @[functor@ %t@ -> ...@]@;<1 -2>is not included in@ \
       @[functor@ %t@ -> ...@]@]"
      actual expected
  in
  let msgs = dwith_context ctx main :: before in
  let functor_suberrors =
    if expansion_token then
      Functor_suberror.params functor_arg_diff ~expansion_token env d
    else []
  in
  functor_suberrors @ msgs

and functor_symptom ~expansion_token ~env ~before ~ctx = function
  | Result res ->
      module_type ~expansion_token ~eqmode:false ~env ~before ~ctx res
  | Params d -> functor_params ~expansion_token ~env ~before ~ctx d

and signature ~expansion_token ~env:_ ~before ~ctx sgs =
  Printtyp.wrap_printing_env ~error:true sgs.env (fun () ->
      match sgs.missings, sgs.incompatibles with
      | _ :: _ as missings, _ ->
          if expansion_token then
            let init_missings, last_missing = Misc.split_last missings in
            List.map (Location.msg "%a" missing_field) init_missings
            @ with_context ctx missing_field last_missing
            :: before
          else
            before
      | [], a :: _ -> sigitem ~expansion_token ~env:sgs.env ~before ~ctx a
      | [], [] -> assert false
    )
and sigitem ~expansion_token ~env ~before ~ctx (name,s) = match s with
  | Core c ->
      dwith_context ctx (core env name c) :: before
  | Module_type diff ->
      module_type ~expansion_token ~eqmode:false ~env ~before
        ~ctx:(Context.Module name :: ctx) diff
  | Module_type_declaration diff ->
      module_type_decl ~expansion_token ~env ~before ~ctx name diff
and module_type_decl ~expansion_token ~env ~before ~ctx id diff =
  let next =
    dwith_context_and_elision ctx (module_type_declarations id diff) in
  let before = next :: before in
  match diff.symptom with
  | Not_less_than mts ->
      let before =
        Location.msg "The first module type is not included in the second"
        :: before
      in
      module_type ~expansion_token ~eqmode:true ~before ~env
        ~ctx:(Context.Modtype id :: ctx) mts
  | Not_greater_than mts ->
      let before =
        Location.msg "The second module type is not included in the first"
        :: before in
      module_type ~expansion_token ~eqmode:true ~before ~env
        ~ctx:(Context.Modtype id :: ctx) mts
  | Incomparable mts ->
      module_type ~expansion_token ~eqmode:true ~env ~before
        ~ctx:(Context.Modtype id :: ctx) mts.less_than
  | Illegal_permutation c ->
      begin match diff.got.Types.mtd_type with
      | None -> assert false
      | Some mty ->
          with_context (Modtype id::ctx)
            (Illegal_permutation.pp Context.alt_pp env) (mty,c)
          :: before
      end

and functor_arg_diff ~expansion_token env (patch: _ Diffing.change) =
  match patch with
  | Insert mty -> Functor_suberror.Inclusion.insert mty
  | Delete mty -> Functor_suberror.Inclusion.delete mty
  | Keep (x, y, _) ->  Functor_suberror.Inclusion.ok x y
  | Change (_, _, Err.Incompatible_params (i,_)) ->
      Functor_suberror.Inclusion.incompatible i
  | Change (g, e,  Err.Mismatch mty_diff) ->
      let more () =
        subcase_list @@
        module_type_symptom ~eqmode:false ~expansion_token ~env ~before:[]
          ~ctx:[] mty_diff.symptom
      in
      let is_modal = Is_modal.module_type_symptom mty_diff.symptom in
      Functor_suberror.Inclusion.diff ~is_modal g e more

let functor_app_diff ~expansion_token env  (patch: _ Diffing.change) =
  match patch with
  | Insert mty ->  Functor_suberror.App.insert mty
  | Delete mty ->  Functor_suberror.App.delete mty
  | Keep (x, y, _) ->  Functor_suberror.App.ok x y
  | Change (_, _, Err.Incompatible_params (i,_)) ->
      Functor_suberror.App.incompatible i
  | Change (g, e,  Err.Mismatch mty_diff) ->
      let more () =
        subcase_list @@
        module_type_symptom ~eqmode:false ~expansion_token ~env ~before:[]
          ~ctx:[] mty_diff.symptom
      in
      let is_modal = Is_modal.module_type_symptom mty_diff.symptom in
      Functor_suberror.App.diff ~is_modal g e more

let module_type_subst ~env id diff =
  match diff.symptom with
  | Not_less_than mts ->
      module_type ~expansion_token:true ~eqmode:true ~before:[] ~env
        ~ctx:[Modtype id] mts
  | Not_greater_than mts ->
      module_type ~expansion_token:true ~eqmode:true ~before:[] ~env
        ~ctx:[Modtype id] mts
  | Incomparable mts ->
      module_type ~expansion_token:true ~eqmode:true ~env ~before:[]
        ~ctx:[Modtype id] mts.less_than
  | Illegal_permutation c ->
      let mty = diff.got in
      let main =
        with_context [Modtype id]
          (Illegal_permutation.pp Context.alt_pp env) (mty,c) in
      [main]

let all env = function
  | In_Compilation_unit (comparison, diff) ->
      let first =
        Location.msg "%a" (compilation_unit_mismatch comparison) diff
      in
      signature ~expansion_token:true ~env ~before:[first] ~ctx:[] diff.symptom
  | In_Type_declaration (id,reason) ->
      [Location.msg "%t" (core env id reason)]
  | In_Jkind_declaration (id,reason) ->
      [Location.msg "%t" (core env id reason)]
  | In_Module_type diff ->
      module_type ~expansion_token:true ~eqmode:false ~before:[] ~env ~ctx:[]
        diff
  | In_Module_type_substitution (id,diff) ->
      module_type_subst ~env id diff
  | In_Signature diff ->
      signature ~expansion_token:true ~before:[] ~env ~ctx:[] diff
  | In_Include_functor_signature diff ->
      signature ~expansion_token:true ~before:[] ~env ~ctx:[] diff
  | In_Expansion cmts ->
      match core_module_type_symptom cmts with
      | None -> assert false
      | Some main -> [Location.msg "%t" main]

(* General error reporting *)

let err_msgs ppf (env, err) =
  Printtyp.Conflicts.reset();
  Printtyp.wrap_printing_env ~error:true env
    (fun () -> (coalesce @@ all env err)  ppf)

let report_error_doc err =
  Location.errorf ~loc:Location.(in_file !input_name) "%a" err_msgs err

let report_apply_error_doc ~loc env (app_name, mty_f, args) =
  let d = Functor_suberror.App.patch env ~f:mty_f ~args in
  match d with
  (* We specialize the one change and one argument case to remove the
     presentation of the functor arguments *)
  | [ _,  Change (_, _, Err.Incompatible_params (i,_)) ] ->
      Location.errorf ~loc "%t" (Functor_suberror.App.incompatible i)
  | [ _, Change (g, e,  Err.Mismatch mty_diff) ] ->
      let more () =
        subcase_list @@
        module_type_symptom ~eqmode:false ~expansion_token:true ~env ~before:[]
          ~ctx:[] mty_diff.symptom
      in
      let is_modal = Is_modal.module_type_symptom mty_diff.symptom in
      Location.errorf ~loc "%t"
        (Functor_suberror.App.single_diff ~is_modal g e more)
  | _ ->
      let not_functor =
        List.for_all (function _, Diffing.Delete _ -> true | _ -> false) d
      in
      if not_functor then
        match app_name with
        | Includemod.Named_leftmost_functor lid ->
            Location.errorf ~loc
              "@[The module %a is not a functor, it cannot be applied.@]"
               (Style.as_inline_code Printtyp.longident)  lid
        | Includemod.Anonymous_functor
        | Includemod.Full_application_path _
          (* The "non-functor application in term" case is directly handled in
             [Env] and it is the only case where we have a full application
             path at hand. Thus this case of the or-pattern is currently
             unreachable and we don't try to specialize the corresponding error
             message. *) ->
            Location.errorf ~loc
              "@[This module is not a functor, it cannot be applied.@]"
      else
        let intro ppf =
          match app_name with
          | Includemod.Anonymous_functor ->
              Fmt.fprintf ppf "This functor application is ill-typed."
          | Includemod.Full_application_path lid ->
              Fmt.fprintf ppf "The functor application %a is ill-typed."
                (Style.as_inline_code Printtyp.longident) lid
          |  Includemod.Named_leftmost_functor lid ->
              Fmt.fprintf ppf
                "This application of the functor %a is ill-typed."
                 (Style.as_inline_code Printtyp.longident) lid
        in
        let actual = Functor_suberror.App.got ~is_modal:None d in
        let expected = Functor_suberror.expected ~is_modal:None d in
        let sub =
          List.rev @@
          Functor_suberror.params functor_app_diff env ~expansion_token:true d
        in
        Location.errorf ~loc ~sub
          "@[<hv>%t@ \
           These arguments:@;<1 2>@[%t@]@ \
           do not match these parameters:@;<1 2>@[functor@ %t@ -> ...@]@]"
          intro
          actual expected

let register () =
  Location.register_error_of_exn
    (function
      | Includemod.Error err -> Some (report_error_doc err)
      | Includemod.Apply_error {loc; env; app_name; mty_f; args} ->
          Some (Printtyp.wrap_printing_env env ~error:true (fun () ->
              report_apply_error_doc ~loc env (app_name, mty_f, args))
            )
      | _ -> None
    )