Source file print.ml

(* This file is part of the Catala compiler, a specification language for tax
   and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
   Denis Merigoux <denis.merigoux@inria.fr>

   Licensed under the Apache License, Version 2.0 (the "License"); you may not
   use this file except in compliance with the License. You may obtain a copy of
   the License at

   http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
   WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
   License for the specific language governing permissions and limitations under
   the License. *)

open Catala_utils
open Definitions

let typ_needs_parens (ty : typ) : bool =
  match Mark.remove ty with TArrow _ | TArray _ -> true | _ -> false

let uid_list (fmt : Format.formatter) (infos : Uid.MarkedString.info list) :
    unit =
  Format.pp_print_list
    ~pp_sep:(fun fmt () -> Format.pp_print_char fmt '.')
    (fun fmt info ->
      Format.fprintf fmt
        (if String.begins_with_uppercase (Mark.remove info) then "@{<red>%s@}"
         else "%s")
        (Uid.MarkedString.to_string info))
    fmt infos

let with_color f color fmt x =
  (* equivalent to [Format.fprintf fmt "@{<color>%s@}" s] *)
  Format.pp_open_stag fmt Ocolor_format.(Ocolor_style_tag (Fg (C4 color)));
  f fmt x;
  Format.pp_close_stag fmt ()

let pp_color_string = with_color Format.pp_print_string
let pp_color_uchar fmt = with_color (fun fmt -> Format.pp_print_as fmt 1) fmt

(* Cyclic list used to choose nested paren colors *)
let rec colors =
  let open Ocolor_types in
  blue :: cyan :: green :: yellow :: red :: magenta :: colors

let keyword (fmt : Format.formatter) (s : string) : unit =
  pp_color_string Ocolor_types.hi_magenta fmt s

let base_type (fmt : Format.formatter) (s : string) : unit =
  pp_color_string Ocolor_types.yellow fmt s

let punctuation (fmt : Format.formatter) (s : string) : unit =
  pp_color_uchar Ocolor_types.cyan fmt s

let op_style (fmt : Format.formatter) (s : string) : unit =
  pp_color_uchar Ocolor_types.green fmt s

let literal_op_style (fmt : Format.formatter) (s : string) : unit =
  with_color
    (fun fmt -> Format.pp_print_as fmt (String.width s))
    Ocolor_types.green fmt s

let lit_style (fmt : Format.formatter) (s : string) : unit =
  pp_color_string Ocolor_types.yellow fmt s

let lit_uchar_style (fmt : Format.formatter) (s : string) : unit =
  pp_color_uchar Ocolor_types.yellow fmt s

let tlit (fmt : Format.formatter) (l : typ_lit) : unit =
  base_type fmt
    (match l with
    | TUnit -> "unit"
    | TBool -> "bool"
    | TInt -> "integer"
    | TRat -> "decimal"
    | TMoney -> "money"
    | TDuration -> "duration"
    | TDate -> "date"
    | TPos -> "code_location")

let location (type a) (fmt : Format.formatter) (l : a glocation) : unit =
  match l with
  | DesugaredScopeVar { name; _ } -> ScopeVar.format fmt (Mark.remove name)
  | ScopelangScopeVar { name; _ } -> ScopeVar.format fmt (Mark.remove name)
  | ToplevelVar { name; _ } -> TopdefName.format fmt (Mark.remove name)

let external_ref fmt er =
  match Mark.remove er with
  | External_value v -> TopdefName.format fmt v
  | External_scope s -> ScopeName.format fmt s

let attr ppf = function
  | Pos.Law_pos _ -> ()
  | Src (path, value, _pos) ->
    Format.fprintf ppf "#[%a"
      (Format.pp_print_list
         ~pp_sep:(fun ppf () -> Format.pp_print_char ppf '.')
         Format.pp_print_string)
      (Mark.remove path);
    (match value with
    | Unit -> ()
    | String (str, _) -> Format.fprintf ppf " = %S" str
    | _ -> Format.fprintf ppf " = <expr>");
    Format.fprintf ppf "]@ "
  | DebugPrint { label } ->
    Format.fprintf ppf "#[debug.print%a]@ "
      (fun ppf -> function
        | None -> () | Some label -> Format.fprintf ppf " = %S" label)
      label
  | Test -> Format.fprintf ppf "#[test]@ "
  | ErrorMessage s -> Format.fprintf ppf "#[error.message = %S]@ " s
  | ImplicitPosArg -> Format.fprintf ppf "#[implicit_position_argument]@ "
  | JsonPayload s -> Format.fprintf ppf "#[json = %S]@ " s
  | _ -> Format.fprintf ppf "#[?]@ "

let attrs ppf x = List.iter (attr ppf) (Pos.attrs x)

let tvar ppf tv =
  let name = Bindlib.name_of tv in
  let name =
    if name.[0] = '\'' then
      let num = String.sub name 1 (String.length name - 1) in
      if num = "1" then "any type" else "any type (" ^ num ^ ")"
    else name
  in
  Format.fprintf ppf "@{<bold;yellow><%s%s>@}" name
    (if Global.options.debug then "_" ^ string_of_int (Bindlib.uid_of tv)
     else "")

let rec typ_gen :
    colors:Ocolor_types.color4 list ->
    Bindlib.ctxt ->
    Format.formatter ->
    typ ->
    unit =
 fun ~colors bctx fmt ty ->
  let typ_gen ?(colors = colors) ?(bctx = bctx) () = typ_gen ~colors bctx in
  let typ_with_parens ?(colors = colors) (fmt : Format.formatter) t =
    if typ_needs_parens t then (
      Format.pp_open_hvbox fmt 1;
      pp_color_string (List.hd colors) fmt "(";
      typ_gen ~colors:(List.tl colors) () fmt t;
      Format.pp_close_box fmt ();
      pp_color_string (List.hd colors) fmt ")")
    else typ_gen ~colors () fmt t
  in
  attrs fmt (Mark.get ty);
  match Mark.remove ty with
  | TLit l -> tlit fmt l
  | TTuple ts ->
    Format.pp_open_hvbox fmt 1;
    pp_color_string (List.hd colors) fmt "(";
    (Format.pp_print_list
       ~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " op_style ",")
       (typ_gen ~colors:(List.tl colors) ()))
      fmt ts;
    Format.pp_close_box fmt ();
    pp_color_string (List.hd colors) fmt ")"
  | TStruct s -> StructName.format fmt s
  | TEnum e -> Format.fprintf fmt "@[<hov 2>%a@]" EnumName.format e
  | TAbstract e -> Format.fprintf fmt "@[<hov 2>%a@]" AbstractType.format e
  | TOption t ->
    Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "optional of" (typ_gen ())
      t
  | TArrow ([t1], t2) ->
    Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" (typ_with_parens ~colors) t1
      op_style "→" (typ_gen ()) t2
  | TArrow (t1, t2) ->
    Format.fprintf fmt "@[<hov 2>%a%a%a@ %a@ %a@]"
      (pp_color_string (List.hd colors))
      "("
      (Format.pp_print_list
         ~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " op_style ",")
         (typ_with_parens ~colors:(List.tl colors)))
      t1
      (pp_color_string (List.hd colors))
      ")" op_style "→"
      (typ_gen ~colors:(List.tl colors) ())
      t2
  | TArray t1 ->
    Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "list of" (typ_gen ()) t1
  | TDefault t1 ->
    punctuation fmt "⟪";
    typ_gen () fmt t1;
    punctuation fmt "⟫"
  | TVar tv -> tvar fmt tv
  | TForAll tb ->
    let tvs, ty, bctx = Bindlib.unmbind_in bctx tb in
    if Global.options.debug then
      Format.fprintf fmt "∀ %a .@ "
        (Format.pp_print_seq ~pp_sep:Format.pp_print_space tvar)
        (Array.to_seq tvs);
    typ_gen ~bctx () fmt ty
  | TClosureEnv -> base_type fmt "closure_env"
  | TError -> base_type fmt "error"

let typ ?(colors = colors) fmt ty = typ_gen ~colors Bindlib.empty_ctxt fmt ty

let lit (fmt : Format.formatter) (l : lit) : unit =
  match l with
  | LBool b -> lit_style fmt (string_of_bool b)
  | LInt i -> lit_style fmt (Catala_runtime.integer_to_string i)
  | LUnit -> lit_style fmt "()"
  | LRat i ->
    lit_style fmt
      (Catala_runtime.decimal_to_string
         ~max_prec_digits:Global.options.max_prec_digits i)
  | LMoney e ->
    lit_style fmt (Format.asprintf "¤%s" (Catala_runtime.money_to_string e))
  | LDate d -> lit_style fmt ("|" ^ Catala_runtime.date_to_string d ^ "|")
  | LDuration d -> lit_style fmt (Catala_runtime.duration_to_string d)

let tag (fmt : Format.formatter) (entry : tag) : unit =
  match entry with
  | LocalVarDef { name } -> Format.fprintf fmt "LocalVarDef(%s)" name
  | LocalTupDef { names } ->
    Format.fprintf fmt "LocalTupDef(%a)"
      Format.(
        pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ",") pp_print_string)
      names
  | ScopeVarDef { var; _ } ->
    Format.fprintf fmt "ScopeVarDef(%s)" (ScopeVar.to_string var)
  | ScopeCall scope ->
    Format.fprintf fmt "ScopeCall(%a)" ScopeName.format_original scope
  | FunCall f -> Format.fprintf fmt "FunCall(%a)" TopdefName.format_original f
  | BranchingCondition -> Format.fprintf fmt "BranchingCondition"
  | Branching None -> Format.fprintf fmt "IfBranching"
  | Branching (Some cstr) -> Format.fprintf fmt "MatchBranching(%s)" cstr
  | Exception { label = Some (lbl, _); cons_pos = _ } ->
    Format.fprintf fmt "Exception(%s)" lbl
  | Exception { label = None; cons_pos = _ } -> Format.fprintf fmt "Exception"
  | Assertion -> Format.fprintf fmt "Assertion"

let tag_to_runtime (k : tag) =
  match k with
  | ScopeCall _ -> "ScopeCall"
  | ScopeVarDef _ -> "ScopeVarDef"
  | LocalVarDef _ -> "LocalVarDef"
  | LocalTupDef _ -> "LocalTupDef"
  | FunCall _ -> "FunCall"
  | BranchingCondition -> "BranchingCondition"
  | Branching None -> "IfBranching"
  | Branching (Some _) -> "MatchBranching"
  | Assertion -> "Assertion"
  | Exception _ -> "Exception"

let operator_to_string : type a. a Op.t -> string =
  let open Op in
  function
  | Not -> "not"
  | Length -> "length"
  | ToInt -> "to_int"
  | ToInt_rat -> "to_int_rat"
  | ToInt_mon -> "to_int_mon"
  | ToRat -> "to_rat"
  | ToRat_int -> "to_rat_int"
  | ToRat_mon -> "to_rat_mon"
  | ToMoney -> "to_mon"
  | ToMoney_rat -> "to_mon_rat"
  | ToMoney_int -> "to_mon_int"
  | Round -> "round"
  | Round_rat -> "round_rat"
  | Round_mon -> "round_mon"
  | Tag t -> Format.asprintf "#{%a}" tag t
  | Minus -> "-"
  | Minus_int -> "-!"
  | Minus_rat -> "-."
  | Minus_mon -> "-$"
  | Minus_dur -> "-^"
  | And -> "&&"
  | Or -> "||"
  | Xor -> "xor"
  | Eq -> "="
  | Map -> "map"
  | Map2 -> "map2"
  | Reduce -> "reduce"
  | Concat -> "++"
  | Filter -> "filter"
  | Find -> "find"
  | Sort `Asc -> "sort_increasing"
  | Sort `Desc -> "sort_decreasing"
  | Add -> "+"
  | Add_int_int -> "+!"
  | Add_rat_rat -> "+."
  | Add_mon_mon -> "+$"
  | Add_dat_dur AbortOnRound -> "+@"
  | Add_dat_dur RoundUp -> "+@u"
  | Add_dat_dur RoundDown -> "+@d"
  | Add_dur_dur -> "+^"
  | Sub -> "-"
  | Sub_int_int -> "-!"
  | Sub_rat_rat -> "-."
  | Sub_mon_mon -> "-$"
  | Sub_dat_dat -> "-@"
  | Sub_dat_dur AbortOnRound -> "-@"
  | Sub_dat_dur RoundUp -> "-@^u"
  | Sub_dat_dur RoundDown -> "-@d"
  | Sub_dur_dur -> "-^"
  | Mult -> "*"
  | Mult_int_int -> "*!"
  | Mult_rat_rat -> "*."
  | Mult_mon_int -> "*$!"
  | Mult_mon_rat -> "*$."
  | Mult_dur_int -> "*^"
  | Div -> "/"
  | Div_int_int -> "/!"
  | Div_rat_rat -> "/."
  | Div_mon_mon -> "/$"
  | Div_mon_int -> "/$!"
  | Div_mon_rat -> "/$."
  | Div_dur_dur -> "/^"
  | Lt -> "<"
  | Lte -> "<="
  | Gt -> ">"
  | Gte -> ">="
  | Fold -> "fold"
  | HandleExceptions -> "handle_exceptions"
  | ToClosureEnv -> "to_closure_env"
  | FromClosureEnv -> "from_closure_env"
  | ArrayAccess n -> Printf.sprintf "o_array_nth(%d)" n
  | ConstructorCheck (e, c) ->
    Printf.sprintf "o_is(%s.%s)" (EnumName.to_string e)
      (EnumConstructor.to_string c)
  | ValueFromJson (_ty, json) -> Printf.sprintf "json[%s]" json
  | DebugPrint s -> Printf.sprintf "debug_print(\"%s\")" s

let operator_to_shorter_string : type a. a Op.t -> string =
  let open Op in
  function
  | Not -> "not"
  | Length -> "length"
  | ToInt | ToInt_rat | ToInt_mon -> "to_int"
  | ToRat_int | ToRat_mon | ToRat -> "to_rat"
  | ToMoney_rat | ToMoney_int | ToMoney -> "to_mon"
  | Round_rat | Round_mon | Round -> "round"
  | Tag _ -> "#"
  | Minus_int | Minus_rat | Minus_mon | Minus_dur | Minus -> "-"
  | And -> "&&"
  | Or -> "||"
  | Xor -> "xor"
  | Eq -> "="
  | Map -> "map"
  | Map2 -> "map2"
  | Reduce -> "reduce"
  | Concat -> "++"
  | Filter -> "filter"
  | Find -> "find"
  | Sort `Asc -> "sort_up"
  | Sort `Desc -> "sort_down"
  | Add_int_int | Add_rat_rat | Add_mon_mon | Add_dat_dur _ | Add_dur_dur | Add
    ->
    "+"
  | Sub_int_int | Sub_rat_rat | Sub_mon_mon | Sub_dat_dat | Sub_dat_dur _
  | Sub_dur_dur | Sub ->
    "-"
  | Mult_int_int | Mult_rat_rat | Mult_mon_int | Mult_mon_rat | Mult_dur_int
  | Mult ->
    "*"
  | Div_int_int | Div_rat_rat | Div_mon_mon | Div_mon_int | Div_mon_rat
  | Div_dur_dur | Div ->
    "/"
  | Lt -> "<"
  | Lte -> "≤"
  | Gt -> ">"
  | Gte -> "≥"
  | Fold -> "fold"
  | HandleExceptions -> "handle_exceptions"
  | ToClosureEnv -> "to_closure_env"
  | FromClosureEnv -> "from_closure_env"
  | ArrayAccess n -> Printf.sprintf "nth(%d)" n
  | ConstructorCheck (_, c) ->
    Printf.sprintf "is_%s" (EnumConstructor.to_string c)
  | ValueFromJson (_ty, json) -> Printf.sprintf "json[%s]" json
  | DebugPrint s -> Printf.sprintf "debug_print(\"%s\")" s

let negated_op_to_string : type a. a Op.t -> string = function
  | Xor -> "="
  | Eq -> "≠"
  | Lt -> "≮"
  | Lte -> "≰"
  | Gt -> "≯"
  | Gte -> "≱"
  | _ -> invalid_arg "negated_op_to_string"

let negated_op ppf op = literal_op_style ppf (negated_op_to_string op)

let operator : type a. ?debug:bool -> Format.formatter -> a operator -> unit =
 fun ?(debug = true) fmt op ->
  let open Op in
  match op with
  | Tag t -> Format.fprintf fmt "@{<blue>#{@}%a@{<blue>}@}" tag t
  | op ->
    literal_op_style fmt
      (if debug then operator_to_string op else operator_to_shorter_string op)

let runtime_error ppf err =
  Format.fprintf ppf "@{<red>%s@}" (Catala_runtime.error_to_string err)

let var_debug fmt v =
  Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)

let var fmt v = Format.pp_print_string fmt (Bindlib.name_of v)

(* Define precedence levels for auto parentheses *)
module Precedence = struct
  type op = Xor | And | Or | Comp | Mul | Div | Add | Sub

  type t =
    | Contained
      (* No parens needed, the term has unambiguous beginning and end *)
    | Op of op
    | App (* Function application, right-associative *)
    | Abs (* lambda, *)
    | Inj (* constructor application *)
    | Dot (* *)

  let expr : type a. (a, 't) gexpr -> t =
   fun e ->
    match Mark.remove e with
    | ELit _ -> Contained (* Todo: unop if < 0 *)
    | EAppOp { op; _ } -> (
      match Mark.remove op with
      | Not | Length | Tag _ | Minus | Minus_int | Minus_rat | Minus_mon
      | Minus_dur | ToInt | ToInt_rat | ToInt_mon | ToRat | ToRat_int
      | ToRat_mon | ToMoney | ToMoney_int | ToMoney_rat | Round | Round_rat
      | Round_mon ->
        App
      | And -> Op And
      | Or -> Op Or
      | Xor -> Op Xor
      | Eq -> Op Comp
      | Lt -> Op Comp
      | Lte -> Op Comp
      | Gt -> Op Comp
      | Gte -> Op Comp
      | Add | Add_int_int | Add_rat_rat | Add_mon_mon | Add_dat_dur _
      | Add_dur_dur ->
        Op Add
      | Sub | Sub_int_int | Sub_rat_rat | Sub_mon_mon | Sub_dat_dat
      | Sub_dat_dur _ | Sub_dur_dur ->
        Op Sub
      | Mult | Mult_int_int | Mult_rat_rat | Mult_mon_int | Mult_mon_rat
      | Mult_dur_int ->
        Op Mul
      | Div | Div_int_int | Div_rat_rat | Div_mon_int | Div_mon_rat
      | Div_mon_mon | Div_dur_dur ->
        Op Div
      | HandleExceptions | Map | Map2 | Concat | Filter | Find | Reduce | Fold
      | Sort _ | ToClosureEnv | FromClosureEnv | ArrayAccess _
      | ConstructorCheck _ | DebugPrint _ ->
        App
      | ValueFromJson _ -> Contained)
    | EApp _ -> App
    | EArray _ -> Contained
    | EVar _ -> Contained
    | EExternal _ -> Contained
    | EAbs _ -> Abs
    | EIfThenElse _ -> Contained
    | EStruct _ -> Contained
    | EInj { e = ELit LUnit, _; _ } -> Contained
    | EInj _ -> Inj
    | EMatch _ -> App
    | ETuple _ -> Contained
    | ETupleAccess _ -> Dot
    | ELocation _ -> Contained
    | EScopeCall _ -> App
    | EDStructAmend _ -> App
    | EDStructAccess _ | EStructAccess _ -> Dot
    | EAssert _ -> App
    | EFatalError _ -> App
    | EFatalError_pos _ -> App
    | EDefault _ -> Contained
    | EPureDefault _ -> Contained
    | EEmpty -> Contained
    | EErrorOnEmpty _ -> App
    | EPos _ -> Contained
    | ECustom _ -> Contained
    | EBad -> Contained

  let needs_parens ~context ?(rhs = false) e =
    match expr context, expr e with
    | _, Contained -> false
    | Dot, Dot -> rhs
    | _, Dot -> false
    | Dot, _ -> true
    | Inj, _ -> true
    | _, Inj -> false
    | App, App -> not rhs
    | App, Op _ -> true
    | App, Abs -> true
    | Abs, _ -> false
    | Op a, Op b -> (
      match a, b with
      | _, Xor -> true
      | And, And | Or, Or -> false
      | And, Or | Or, And -> true
      | (And | Or | Xor), _ -> false
      | _, (And | Or | Comp) -> true
      | Comp, _ -> false
      | Add, (Add | Sub) -> false
      | Sub, (Add | Sub) -> rhs
      | (Add | Sub), (Mul | Div) -> false
      | (Mul | Div), (Add | Sub) -> true
      | Mul, (Mul | Div) -> false
      | Div, (Mul | Div) -> rhs)
    | Op Comp, App -> false
    | Op _, App -> not rhs
    | Op _, _ -> true
    | Contained, _ -> false
end

module type EXPR_PARAM = sig
  val bypass : Format.formatter -> ('a, 't) gexpr -> bool
  val operator : Format.formatter -> 'a operator -> unit
  val var : Format.formatter -> ('a, 't) gexpr Var.t -> unit
  val lit : Format.formatter -> lit -> unit
  val pre_map : ('a, 't) gexpr -> ('a, 't) gexpr
end

module ExprGen (C : EXPR_PARAM) = struct
  let rec expr_aux : type a t.
      Bindlib.ctxt ->
      Ocolor_types.color4 list ->
      Format.formatter ->
      (a, t) gexpr ->
      unit =
   fun bnd_ctx colors fmt e ->
    attrs fmt
      (match Mark.get e with
      | Untyped { pos } | Typed { pos; _ } | Custom { pos; _ } -> pos);
    (* Uncomment for type annotations everywhere *)
    (* (fun f ->
     *    match Mark.get e with
     *    | Typed {ty; _} ->
     *      Format.fprintf fmt "@[<hv 1>(%a:@ %a)@]"
     *        f e
     *        (typ ~colors) ty
     *    | _ -> f fmt e)
     * @@ fun fmt e -> *)
    let exprb bnd_ctx colors e = expr_aux bnd_ctx colors e in
    let exprc colors e = exprb bnd_ctx colors e in
    let expr e = exprc colors e in
    let var = C.var in
    let operator = C.operator in
    let e = C.pre_map e in
    let paren ?(context = e) ~rhs ?(colors = colors) expr fmt e1 =
      if Precedence.needs_parens ~rhs ~context (C.pre_map e1) then (
        Format.pp_open_hvbox fmt 1;
        pp_color_string (List.hd colors) fmt "(";
        expr (List.tl colors) fmt e1;
        Format.pp_close_box fmt ();
        pp_color_string (List.hd colors) fmt ")")
      else expr colors fmt e1
    in
    let default_punct = with_color (fun fmt -> Format.pp_print_as fmt 1) in
    let lhs ?(colors = colors) ex = paren ~colors ~rhs:false ex in
    let rhs ex = paren ~rhs:true ex in
    if C.bypass fmt e then ()
    else
      match Mark.remove e with
      | EVar v -> var fmt v
      | EExternal { name } -> external_ref fmt name
      | ETuple es ->
        Format.fprintf fmt "@[<hov 1>%a%a%a@]"
          (pp_color_string (List.hd colors))
          "("
          (Format.pp_print_list
             ~pp_sep:(fun fmt () ->
               Format.fprintf fmt "%a@ " (pp_color_string (List.hd colors)) ",")
             (fun fmt e -> lhs ~colors:(List.tl colors) exprc fmt e))
          es
          (pp_color_string (List.hd colors))
          ")"
      | EArray es ->
        Format.fprintf fmt "@[<hv 2>%a@,@[<hov>%a@]@;<0 -2>%a@]" punctuation "["
          (Format.pp_print_list
             ~pp_sep:(fun fmt () -> Format.fprintf fmt ";@ ")
             (fun fmt e -> lhs exprc fmt e))
          es punctuation "]"
      | ETupleAccess { e; index; _ } ->
        lhs exprc fmt e;
        punctuation fmt ".";
        Format.pp_print_int fmt index
      | ELit l -> C.lit fmt l
      | EApp { f = EAbs _, _; _ } ->
        let rec pr bnd_ctx colors fmt = function
          | EApp { f = EAbs { binder; pos = _; tys }, _; args; _ }, _ ->
            let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in
            let xs_tau = List.mapi (fun i tau -> xs.(i), tau) tys in
            let xs_tau_arg =
              let rec aux xs_tau args =
                match xs_tau, args with
                | (x, tau) :: xs_tau, arg :: args ->
                  (x, tau, arg) :: aux xs_tau args
                | [], [] -> []
                | (x, tau) :: xs_tau, [] ->
                  (x, tau, (EVar (Var.make "XXX"), Mark.get e))
                  :: aux xs_tau args
                | [], arg :: args ->
                  (Var.make "XXX", (TLit TUnit, Pos.void), arg)
                  :: aux xs_tau args
              in
              aux xs_tau args
            in
            Format.pp_print_list
              (fun fmt (x, tau, arg) ->
                Format.fprintf fmt
                  "@[<hv 2>@[<hov 4>%a %a %a@ %a@ %a@]@ %a@;<1 -2>%a@]" keyword
                  "let" var x punctuation ":" (typ ~colors) tau punctuation "="
                  (exprc colors) arg keyword "in")
              fmt xs_tau_arg;
            Format.pp_print_cut fmt ();
            rhs (pr bnd_ctx) fmt body
          | e -> rhs (exprb bnd_ctx) fmt e
        in
        Format.pp_open_vbox fmt 0;
        pr bnd_ctx colors fmt e;
        Format.pp_close_box fmt ()
      | EAbs { binder; pos = _; tys } ->
        let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in
        let expr = exprb bnd_ctx in
        let xs_tau =
          List.mapi
            (fun i tau ->
              ( (if i < Array.length xs then xs.(i) else Var.make "[MISSING ARG]"),
                tau ))
            tys
        in
        Format.fprintf fmt "@[<hv 0>%a @[<hv 2>%a@]@ @]%a@ %a" punctuation "λ"
          (Format.pp_print_list ~pp_sep:Format.pp_print_space
             (fun fmt (x, tau) ->
               match tau with
               | TLit TUnit, _ ->
                 punctuation fmt "(";
                 punctuation fmt ")"
               | _ ->
                 punctuation fmt "(";
                 Format.pp_open_hvbox fmt 2;
                 var fmt x;
                 punctuation fmt ":";
                 Format.pp_print_space fmt ();
                 typ ~colors fmt tau;
                 Format.pp_close_box fmt ();
                 punctuation fmt ")"))
          xs_tau punctuation "→" (rhs expr) body
      | EAppOp { op = ((Map | Filter) as op), _; args = [arg1; arg2]; _ } ->
        Format.fprintf fmt "@[<hv 2>%a %a@ %a@]" operator op (lhs exprc) arg1
          (rhs exprc) arg2
      | EAppOp { op = Not, _; args = [e]; _ } -> (
        match e with
        | EAppOp { op = Not, _; args = [arg1]; _ }, _ -> expr fmt arg1
        | ( EAppOp
              {
                op = ((Eq | Lt | Lte | Gt | Gte | Xor) as op), _;
                args = [arg1; arg2];
                _;
              },
            _ ) ->
          Format.fprintf fmt "@[<hv 2>%a %a@ %a@]"
            (paren ~context:e ~colors ~rhs:false exprc)
            arg1 negated_op op
            (paren ~context:e ~colors ~rhs:false exprc)
            arg2
        | e -> Format.fprintf fmt "@[<hv 2>%a@ %a@]" operator Not (rhs exprc) e)
      | EAppOp { op = (Tag _ as op), _; args = [arg1]; _ } ->
        Format.fprintf fmt "@[<hv 0>%a@ %a@]" operator op (rhs exprc) arg1
      | EAppOp { op = op0, _; args = [_; _]; _ } ->
        let prec = Precedence.expr e in
        let rec pr colors fmt = function
          (* Flatten sequences of the same associative op *)
          | EAppOp { op = op, _; args = [arg1; arg2]; _ }, _ when op = op0 -> (
            (match prec with
            | Op (And | Or | Mul | Add | Div | Sub) -> lhs pr fmt arg1
            | _ -> lhs exprc fmt arg1);
            Format.pp_print_space fmt ();
            operator fmt op;
            Format.pp_print_char fmt ' ';
            match prec with
            | Op (And | Or | Mul | Add) -> rhs pr fmt arg2
            | _ -> rhs exprc fmt arg2)
          | e -> exprc colors fmt e
        in
        Format.pp_open_hvbox fmt 0;
        pr colors fmt e;
        Format.pp_close_box fmt ()
      | EAppOp { op = op, _; args = [arg1]; _ } ->
        Format.fprintf fmt "@[<hv 2>%a@ %a@]" operator op (rhs exprc) arg1
      | EAppOp { op = op, _; args; _ } ->
        Format.fprintf fmt "@[<hv 2>%a@ %a@]" operator op
          (Format.pp_print_list
             ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
             (rhs exprc))
          args
      | EApp { f; args; _ } ->
        Format.fprintf fmt "@[<hv 2>%a@ %a@]" (lhs exprc) f
          (Format.pp_print_list
             ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
             (rhs exprc))
          args
      | EIfThenElse _ ->
        let rec pr els fmt = function
          | EIfThenElse { cond; etrue; efalse }, _ ->
            Format.fprintf fmt "@[<hv 2>@[<hv 2>%a@ %a@;<1 -2>%a@]@ %a@]@ %a"
              keyword
              (if els then "else if" else "if")
              expr cond keyword "then" expr etrue (pr true) efalse
          | e ->
            Format.fprintf fmt "@[<hv 2>%a@ %a@]" keyword "else" (rhs exprc) e
        in
        Format.pp_open_hvbox fmt 0;
        pr false fmt e;
        Format.pp_close_box fmt ()
      | EDefault { excepts; just; cons } ->
        if List.length excepts = 0 then
          Format.fprintf fmt "@[<hv 1>%a%a@ %a %a%a@]"
            (default_punct (List.hd colors))
            "⟨"
            (exprc (List.tl colors))
            just
            (default_punct (List.hd colors))
            "⊢"
            (exprc (List.tl colors))
            cons
            (default_punct (List.hd colors))
            "⟩"
        else
          Format.fprintf fmt
            "@[<hv 0>@[<hov 2>%a %a@]@ @[<hov 2>%a %a@ %a %a@] %a@]"
            (default_punct (List.hd colors))
            "⟨"
            (Format.pp_print_list
               ~pp_sep:(fun fmt () ->
                 Format.fprintf fmt "%a@ " (default_punct (List.hd colors)) ",")
               (lhs ~colors:(List.tl colors) exprc))
            excepts
            (default_punct (List.hd colors))
            "|"
            (exprc (List.tl colors))
            just
            (default_punct (List.hd colors))
            "⊢"
            (exprc (List.tl colors))
            cons
            (default_punct (List.hd colors))
            "⟩"
      | EPureDefault e ->
        Format.fprintf fmt "%a%a%a"
          (default_punct (List.hd colors))
          "⟨" expr e
          (default_punct (List.hd colors))
          "⟩"
      | EEmpty -> lit_uchar_style fmt "∅"
      | EErrorOnEmpty e' ->
        Format.fprintf fmt "@[<hov 2>%a@ %a@]" literal_op_style "error_empty"
          (rhs exprc) e'
      | EPos p ->
        Message.link () fmt
          ~target:
            (Message.file_url (Pos.get_file p) ~line:(Pos.get_start_line p)
               ~column:(Pos.get_start_column p))
          ("<" ^ Pos.to_string_shorter p ^ ">")
      | EAssert e' ->
        Format.fprintf fmt "@[<hov 2>%a@ %a@]" keyword "assert" (rhs exprc) e'
      | EFatalError error ->
        Format.fprintf fmt "@[<hov 2>%a@ @{<red>%s@}@]" keyword "error"
          (Catala_runtime.error_to_string error)
      | EFatalError_pos { error; _ } ->
        Format.fprintf fmt "@[<hov 2>%a@ @{<red>%s@}@]" keyword "error"
          (Catala_runtime.error_to_string error)
      | ELocation loc -> location fmt loc
      | EDStructAccess { e; field; _ } ->
        Format.fprintf fmt "@[<hv 2>%a%a@,%a%a%a@]" (lhs exprc) e punctuation
          "." punctuation "\"" MarkedIdent.format field punctuation "\""
      | EDStructAmend { e; fields; _ } ->
        Format.fprintf fmt "@[<hv 2>@[<hov>%a %a@ with@]@ %a@;<1 -2>%a@]"
          punctuation "{" (lhs exprc) e
          (MarkedIdent.Map.format_bindings ~pp_sep:Format.pp_print_space
             (fun fmt pp_field_name field_expr ->
               Format.fprintf fmt "@[<hv 2>%t %a@ %a%a@]" pp_field_name
                 punctuation "=" (lhs exprc) field_expr punctuation ";"))
          fields punctuation "}"
      | EStruct { name; fields } ->
        if StructField.Map.is_empty fields then (
          punctuation fmt "{";
          StructName.format fmt name;
          punctuation fmt "}")
        else
          Format.fprintf fmt "@[<hv 2>%a %a@ %a@;<1 -2>%a@]" punctuation "{"
            StructName.format name
            (StructField.Map.format_bindings ~pp_sep:Format.pp_print_space
               (fun fmt pp_field_name field_expr ->
                 Format.fprintf fmt "@[<hv 2>%t %a@ %a%a@]" pp_field_name
                   punctuation "=" (lhs exprc) field_expr punctuation ";"))
            fields punctuation "}"
      | EStructAccess { e; field; _ } ->
        Format.fprintf fmt "@[<hv 2>%a%a@,%a@]" (lhs exprc) e punctuation "."
          StructField.format field
      | EInj { e = ELit LUnit, _; cons; _ } ->
        Format.fprintf fmt "@[<hv 2>%a@]" EnumConstructor.format cons
      | EInj { e; cons; _ } ->
        Format.fprintf fmt "@[<hv 2>%a@ %a@]" EnumConstructor.format cons
          (paren ~rhs:false exprc) e
      | EMatch { e; cases; _ } ->
        Format.fprintf fmt "@[<v 0>@[<hv 2>%a@ %a@;<1 -2>%a@]@ %a@]" keyword
          "match" (lhs exprc) e keyword "with"
          (EnumConstructor.Map.format_bindings
             (fun fmt pp_cons_name case_expr ->
               match case_expr with
               | EAbs { binder; tys; _ }, _ ->
                 let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in
                 let expr = exprb bnd_ctx in
                 let pp_args fmt =
                   match tys with
                   | [(TLit TUnit, _)] -> ()
                   | _ ->
                     Format.pp_print_seq ~pp_sep:Format.pp_print_space var fmt
                       (Array.to_seq xs);
                     Format.pp_print_space fmt ()
                 in
                 Format.fprintf fmt "@[<hov 2>%a %t@ %t%a@ %a@]" punctuation "|"
                   pp_cons_name pp_args punctuation "→" (rhs expr) body
               | e ->
                 Format.fprintf fmt "@[<hov 2>%a %t@ %a@ %a@]" punctuation "|"
                   pp_cons_name punctuation "→" (rhs exprc) e))
          cases
      | EScopeCall { scope; args } ->
        Format.pp_open_hovbox fmt 2;
        ScopeName.format fmt scope;
        Format.pp_print_space fmt ();
        keyword fmt "of";
        Format.pp_print_space fmt ();
        Format.pp_open_hvbox fmt 2;
        punctuation fmt "{";
        ScopeVar.Map.format_bindings
          ~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ";")
          (fun fmt pp_field_name (_, field_expr) ->
            Format.fprintf fmt "%a%t%a%a@ %a" punctuation "\"" pp_field_name
              punctuation "\"" punctuation "=" (rhs exprc) field_expr)
          fmt args;
        Format.pp_close_box fmt ();
        punctuation fmt "}";
        Format.pp_close_box fmt ()
      | ECustom { obj; targs = []; tret = TAbstract tid, _ } ->
        let module E =
          (val Catala_runtime.lookup_type
                 ( Uid.Module.to_string
                     (Option.get (Uid.Path.last_member (AbstractType.path tid))),
                   AbstractType.base tid ))
        in
        Catala_runtime.Value.format fmt
          (Catala_runtime.Value.V (E.rtype, Obj.obj obj))
      | ECustom _ -> Format.pp_print_string fmt "<obj>"
      | EBad -> Format.pp_print_string fmt "<bad>"

  let expr ppf e = expr_aux Bindlib.empty_ctxt colors ppf e
end

module ExprConciseParam = struct
  let bypass _ _ = false
  let operator o = operator ~debug:false o
  let var = var
  let lit = lit

  let rec pre_map : type a. (a, 't) gexpr -> (a, 't) gexpr = function
    | EAppOp { op = Tag _, _; args = [e]; _ }, _ -> pre_map e
    | e -> e
end

module ExprConcise = ExprGen (ExprConciseParam)

module ExprDebugParam = struct
  let bypass _ _ = false
  let operator o = operator ~debug:true o
  let var = var_debug
  let lit = lit
  let pre_map e = e
end

module ExprDebug = ExprGen (ExprDebugParam)

let expr ?(debug = Global.options.debug) () ppf e =
  if debug then ExprDebug.expr ppf e else ExprConcise.expr ppf e

let scope_let_kind ?debug:(_debug = true) fmt k =
  match k with
  | DestructuringInputStruct -> keyword fmt "get"
  | ScopeVarDefinition -> keyword fmt "set"
  | CallingSubScope -> keyword fmt "call"
  | DestructuringSubScopeResults -> keyword fmt "sub_get"
  | Assertion -> keyword fmt "assert"

let typ = typ ?colors:None

let[@ocamlformat "disable"]
  scope_body_expr ?(debug = false) fmt b : unit =
  let print_scope_let x sl =
    Format.fprintf fmt
      "@[<hv 2>@[<hov 4>%a %a %a %a@ %a@ %a@]@ %a@;<1 -2>%a@]@,"
      keyword "let"
      (scope_let_kind ~debug) sl.scope_let_kind
      (if debug then var_debug else var) x
      punctuation ":"
      typ sl.scope_let_typ
      punctuation "="
      (expr ~debug ()) sl.scope_let_expr
      keyword "in"
  in
  let last = BoundList.iter ~f:print_scope_let b in
  Format.fprintf fmt "%a %a" keyword "return" (expr ~debug ()) last

let scope_body ?(debug = false) fmt (n, l) : unit =
  let {
    scope_body_input_struct;
    scope_body_output_struct;
    scope_body_expr = body;
    scope_body_visibility = _vis;
  } =
    l
  in

  let input_typ = TStruct scope_body_input_struct, Pos.void in
  let output_typ = TStruct scope_body_output_struct, Pos.void in

  let x, body = Bindlib.unbind body in

  let () =
    Format.pp_open_vbox fmt 2;
    let () =
      Format.pp_open_hvbox fmt 2;
      let () =
        Format.pp_open_hovbox fmt 4;
        keyword fmt "let scope";
        Format.fprintf fmt "@ @{<hi_magenta>%s@}@]" n
      in
      Format.pp_print_space fmt ();
      punctuation fmt "(";
      let () =
        Format.pp_open_hvbox fmt 2;
        (if debug then var_debug else var) fmt x;
        punctuation fmt ":";
        Format.pp_print_space fmt ();
        typ fmt input_typ;
        punctuation fmt ")";
        Format.pp_close_box fmt ()
      in
      Format.pp_print_cut fmt ();
      punctuation fmt ":";
      Format.pp_print_string fmt " ";
      let () =
        Format.pp_open_hvbox fmt 2;
        typ fmt output_typ;
        Format.pp_close_box fmt ()
      in
      Format.pp_print_space fmt ();
      punctuation fmt "=";
      Format.pp_close_box fmt ()
    in

    Format.pp_print_cut fmt ();

    scope_body_expr ~debug fmt body;
    Format.pp_close_box fmt ()
  in
  ()

let enum
    ?debug:(_ = false)
    fmt
    (pp_name : Format.formatter -> unit)
    name
    (c : typ EnumConstructor.Map.t) =
  attrs fmt (Mark.get (EnumName.get_info name));
  Format.fprintf fmt "@[<v 2>%a %t %a@ %a@]@," keyword "type" pp_name
    punctuation "="
    (EnumConstructor.Map.format_bindings_i ~pp_sep:Format.pp_print_space
       (fun fmt pp_n n ty ->
         Format.fprintf fmt "@[<hov2>%a %a%t%a@]" punctuation "|" attrs
           (Mark.get (EnumConstructor.get_info n))
           pp_n
           (fun ppf -> function
             | TLit TUnit, _ -> ()
             | ty -> Format.fprintf ppf " %a %a" keyword "of" typ ty)
           ty))
    c

let struct_
    ?debug:(_ = false)
    fmt
    (pp_name : Format.formatter -> unit)
    name
    (c : typ StructField.Map.t) =
  attrs fmt (Mark.get (StructName.get_info name));
  Format.fprintf fmt "@[<hv 2>%a %t %a %a@ %a@;<1 -2>%a@]@," keyword "type"
    pp_name punctuation "=" punctuation "{"
    (StructField.Map.format_bindings_i ~pp_sep:Format.pp_print_space
       (fun fmt pp_n n ty ->
         Format.fprintf fmt "@[<hov 0>%a@[<h 2>%t%a %a%a@]@]" attrs
           (Mark.get (StructField.get_info n))
           pp_n keyword ":" typ ty punctuation ";"))
    c punctuation "}"

let decl_ctx ?(debug = false) (fmt : Format.formatter) (ctx : decl_ctx) : unit =
  let { ctx_enums; ctx_structs; _ } = ctx in
  Format.fprintf fmt "@[<v>%a@,%a@,@]"
    (EnumName.Map.format_bindings_i (enum ~debug))
    (EnumName.Map.filter
       (fun ename _ -> EnumName.path ename = [])
       (* Remove the Optional type, which is necessarily the first in the ctx *)
       (EnumName.Map.remove
          (fst (EnumName.Map.min_binding ctx_enums))
          ctx_enums))
    (StructName.Map.format_bindings_i (struct_ ~debug))
    (StructName.Map.filter
       (fun sname _ -> StructName.path sname = [])
       ctx_structs)

let scope
    ?(debug : bool = false)
    (fmt : Format.formatter)
    ((n, s) : string * 'm scope_body) : unit =
  Format.pp_open_vbox fmt 0;
  scope_body ~debug fmt (n, s);
  Format.pp_close_box fmt ()

let code_item ?(debug = false) name fmt c =
  match c with
  | ScopeDef (n, b) ->
    attrs fmt (Mark.get (ScopeName.get_info n));
    scope ~debug fmt (name, b)
  | Topdef (n, ty, _vis, e) ->
    attrs fmt (Mark.get (TopdefName.get_info n));
    Format.fprintf fmt
      "@[<v 2>@[<hov 2>%a@ @{<hi_green>%s@}@ %a@ %a@ %a@]@ %a@]" keyword
      "let topval" name op_style ":" typ ty op_style "=" (expr ~debug ()) e

let code_item_list ?(debug = false) fmt c =
  Format.pp_open_vbox fmt 0;
  Format.pp_print_seq
    (fun fmt (id, item) ->
      let name = Format.asprintf "%a" (if debug then var_debug else var) id in
      code_item ~debug name fmt item;
      Format.pp_print_cut fmt ())
    fmt (BoundList.to_seq c);
  Format.pp_close_box fmt ()

let program ?(debug = false) fmt p =
  decl_ctx ~debug fmt p.decl_ctx;
  code_item_list ~debug fmt p.code_items

(* - User-facing value printer - *)

(* This function is re-exported from module [Expr], but defined here where it's
   first needed *)
let rec skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = function
  | EAppOp { op = Tag _, _; args = [e]; tys = _ }, _ -> skip_wrappers e
  | EApp { f = EAppOp { op = Tag _, _; args = [f]; _ }, _; args; tys }, m ->
    skip_wrappers (EApp { f; args; tys }, m)
  | EErrorOnEmpty e, _ -> skip_wrappers e
  | EDefault { excepts = []; just = ELit (LBool true), _; cons = e }, _ ->
    skip_wrappers e
  | EPureDefault e, _ -> skip_wrappers e
  | e -> e

module UserFacing = struct
  module V = Catala_runtime.Value

  exception Not_a_value

  let embed_option embed_value cons payload =
    let lang = Catala_runtime.Print.get_lang () in
    let constr_index =
      if EnumConstructor.equal cons ConstantNames.none_constr then 0
      else if EnumConstructor.equal cons ConstantNames.some_constr then 1
      else assert false
    in
    let name =
      match lang with
      | `En -> "Optional"
      | `Fr -> "Optionnel"
      | `Pl -> "Opcjonalny"
    in
    let constr =
     fun (index, cons, payload) ->
      let cons =
        if EnumConstructor.equal cons ConstantNames.none_constr then
          match lang with `En | `Fr -> "Absent" | `Pl -> "Nieobecny"
        else if EnumConstructor.equal cons ConstantNames.some_constr then
          match lang with
          | `En -> "Present"
          | `Fr -> "Présent"
          | `Pl -> "Obecny"
        else assert false
      in
      ( index,
        cons,
        match payload with ELit LUnit, _ -> None | e -> Some (embed_value e) )
    in
    V.V (Enum { name; constr }, (constr_index, cons, payload))

  (* this is a dumbed-down version of [Expr.embed_value] that doesn't require a
     context but won't document indexes of variant constructors correctly ; we
     go with it since those aren't necessary for printing, and [Expr] depends on
     [Print]. *)
  let rec embed_value : type a. (a, 'm) gexpr -> Catala_runtime.Value.t =
   fun e ->
    match Mark.remove e with
    | ELit LUnit -> V.V (Unit, ())
    | ELit (LBool v) -> V.V (Bool, v)
    | ELit (LInt v) -> V.V (Integer, v)
    | ELit (LMoney v) -> V.V (Money, v)
    | ELit (LRat v) -> V.V (Decimal, v)
    | ELit (LDate v) -> V.V (Date, v)
    | ELit (LDuration v) -> V.V (Duration, v)
    | EPos v ->
      V.V
        ( Position,
          {
            Catala_runtime.filename = Pos.get_file v;
            start_line = Pos.get_start_line v;
            start_column = Pos.get_start_column v;
            end_line = Pos.get_end_line v;
            end_column = Pos.get_end_column v;
            law_headings = Pos.get_law_info v;
          } )
    | EArray el -> V.V (Array embed_value, Array.of_list el)
    | ETuple [(EAbs { tys = (TClosureEnv, _) :: _; _ }, _); _] ->
      (* Closure *)
      V.V (Function, ignore)
    | ETuple el -> V.V (Tuple (List.map embed_value), el)
    | EStruct { name; fields } ->
      V.V
        ( Struct
            {
              name = StructName.original_base name;
              fields =
                List.map (fun (name, e) ->
                    StructField.original_string name, embed_value e);
            },
          StructField.Map.bindings fields )
    | EInj { name; cons; e = payload }
      when EnumName.equal name ConstantNames.option_enum ->
      embed_option embed_value cons payload
    | EInj { name; cons; e = payload } ->
      V.V
        ( Enum
            {
              name = EnumName.original_base name;
              constr =
                (fun (index, cons, payload) ->
                  ( index,
                    EnumConstructor.to_string cons,
                    match payload with
                    | ELit LUnit, _ -> None
                    | e -> Some (embed_value e) ));
            },
          (-1 (* this is fake *), cons, payload) )
    | EAbs _ -> V.V (Function, ignore (* fake *))
    | ECustom { obj; targs = []; tret = TAbstract tid, _ } -> (
      try
        let ext =
          Catala_runtime.lookup_type
            ( Uid.Module.to_string
                (Option.get (Uid.Path.last_member (AbstractType.path tid))),
              AbstractType.base tid )
        in
        let module E = (val ext) in
        V.V (E.rtype, Obj.obj obj)
      with Failure _ -> V.V (Function, obj))
    | ECustom { obj; _ } -> V.V (Function, obj)
    | _ -> raise Not_a_value

  let lit ppf lit : unit =
    with_color Catala_runtime.Value.format Ocolor_types.yellow ppf
      (embed_value (ELit lit, Untyped { pos = Pos.void }))

  let value : type a.
      ?fallback:(Format.formatter -> (a, 't) gexpr -> unit) ->
      Format.formatter ->
      (a, 't) gexpr ->
      unit =
   fun ?(fallback = fun _ _ -> invalid_arg "UserPrint.value: not a value") ppf
       e ->
    match Mark.remove e with
    | EEmpty -> Format.pp_print_string ppf "ø"
    | EExternal _ -> Format.pp_print_string ppf "<external>"
    | ELit l -> lit ppf l
    | EPos p -> Message.pp_pos ppf p
    | _ -> (
      try Catala_runtime.Value.format ppf (embed_value e)
      with Not_a_value -> fallback ppf e)

  let expr : type a. Format.formatter -> (a, 't) gexpr -> unit =
    let rec aux_value : type a t. Format.formatter -> (a, t) gexpr -> unit =
     fun ppf e -> value ~fallback ppf e
    and fallback : type a t. Format.formatter -> (a, t) gexpr -> unit =
     fun ppf e ->
      let module E = ExprGen (struct
        let bypass : type a t. Format.formatter -> (a, t) gexpr -> bool =
         fun ppf e ->
          match Mark.remove e with
          | EArray _ | ETuple _ | EStruct _ | EInj _ | EEmpty | EAbs _
          | EExternal _ ->
            aux_value ppf e;
            true
          | _ -> false

        let operator o = operator ~debug:false o
        let var = var
        let lit = lit
        let pre_map = skip_wrappers
      end) in
      E.expr ppf e
    in
    aux_value
end

let rec s_expr : type a m.
    ?pp_mark:(Format.formatter -> m mark -> unit) ->
    Format.formatter ->
    (a, m) gexpr ->
    unit =
 fun ?(pp_mark = fun _ _ -> ()) fmt e ->
  let open Format in
  let pf = fprintf in
  let pp_sep fmt () = pf fmt ",@ " in
  let s_expr = s_expr ~pp_mark in
  let ppl fmt l = pf fmt "@[<hov 2>[ %a ]@]" (pp_print_list ~pp_sep s_expr) l in
  let pp_marked_id fmt (sf, e) =
    pf fmt "@[<hov 1>%a: %a@]" MarkedIdent.format sf s_expr e
  in
  let pp_field fmt (sf, e) =
    pf fmt "@[<hov 1>%a: %a@]" StructField.format sf s_expr e
  in
  let pp_opt pp fmt = function
    | None -> pf fmt "NONE"
    | Some x -> pf fmt "SOME(%a)" pp x
  in
  pp_mark fmt (Mark.get e);
  match Mark.remove e with
  | ELit (LBool b) -> pf fmt "LitBool<%b>" b
  | ELit (LInt i) -> pf fmt "LitInt<%s>" (Z.to_string i)
  | ELit (LRat q) -> pf fmt "LitFloat<%s>" (Q.to_string q)
  | ELit (LMoney m) -> pf fmt "LitMoney<%s>" (Z.to_string m)
  | ELit LUnit -> pf fmt "LitUnit"
  | ELit (LDate d) -> pf fmt "LitDate<%a>" Dates_calc.format_date d
  | ELit (LDuration d) -> pf fmt "LitDur<%a>" Dates_calc.format_period d
  | EApp { f; args; _ } -> pf fmt "@[<hov 1>App(%a,@ %a)@]" s_expr f ppl args
  | EAppOp { op = Tag entry, m_op; args; _ } ->
    pf fmt "@[<hov 1>AppOp( Tag(%a,%s),@ %a)@]" tag entry
      (Pos.to_string_shorter m_op)
      ppl args
  | EAppOp { op; args; _ } ->
    pf fmt "@[<hov 1>AppOp( %s,@ %a)@]"
      (operator_to_string (Mark.remove op))
      ppl args
  | EArray l -> pf fmt "Array(%a)" ppl l
  | EVar v -> pf fmt "Var(%s#%d)" (Bindlib.name_of v) (Bindlib.uid_of v)
  | EAbs { binder; _ } ->
    let vars, e = Bindlib.unmbind binder in
    let vars : (a, m) gexpr list =
      Array.to_list vars |> List.map (fun v -> Mark.add (Mark.get e) (EVar v))
    in
    pf fmt "@[<hov 1>Abs(%a,@ %a)@]" ppl vars s_expr e
  | EIfThenElse { cond; etrue; efalse } ->
    pf fmt "@[<hov 1>IF(%a,@ %a,@ %a)@]" s_expr cond s_expr etrue s_expr efalse
  | EStruct { name; fields } ->
    let fields = StructField.Map.bindings fields in
    pf fmt "@[<hov 1>Struct<%a>(@[<hov 1>{ %a }@])@]" StructName.format name
      (pp_print_list ~pp_sep pp_field)
      fields
  | EInj { name; e; cons } ->
    pf fmt "@[<hov 1>Inj<%a.%a>(%a)@]" EnumName.format name
      EnumConstructor.format cons s_expr e
  | EMatch { name; e; cases } ->
    let cases = EnumConstructor.Map.bindings cases in
    let pp_case fmt (cons, e) =
      pf fmt "@[<hov 1>%a => %a@]" EnumConstructor.format cons s_expr e
    in
    pf fmt "@[<hov 1>Match<%a>(%a, @[<hov 1>{ %a }@])@]" EnumName.format name
      s_expr e
      (pp_print_list ~pp_sep pp_case)
      cases
  | ETuple t -> pf fmt "@[<hov 1>Tuple(%a)@]" ppl t
  | ETupleAccess { e; index; _ } ->
    pf fmt "@[<hov 1>TupleAccess(%d, %a)@]" index s_expr e
  | ELocation l -> pf fmt "@[<hov 1>Location(%a)@]" location l
  | EScopeCall { scope; args } ->
    let args =
      ScopeVar.Map.bindings args |> List.map (fun (v, arg) -> v, snd arg)
    in
    let pp_arg fmt (v, e) =
      pf fmt "@[<hov 1>%a : %a@]" ScopeVar.format v s_expr e
    in
    pf fmt "@[<hov 1>ScopeCall(%a, @[<hov 1>{ %a }@])@]" ScopeName.format scope
      (pp_print_list ~pp_sep pp_arg)
      args
  | EDStructAmend { name_opt; e; fields } ->
    let fields = MarkedIdent.Map.bindings fields in
    pf fmt "@[<hov 1>DStructAmend<%a>(%a, @[<hov 1>{ %a }@])@]"
      (pp_opt StructName.format) name_opt s_expr e
      (pp_print_list ~pp_sep pp_marked_id)
      fields
  | EDStructAccess { name_opt; e; field } ->
    pf fmt "@[<hov 1>DStructAccess<%a>(%a, %a)@]" (pp_opt StructName.format)
      name_opt MarkedIdent.format field s_expr e
  | EStructAccess { name; e; field } ->
    pf fmt "@[<hov 1>StructAccess<%a>(%a, %a)@]" StructName.format name
      StructField.format field s_expr e
  | EExternal { name } -> pf fmt "@[<hov 1>External<%a>@]" external_ref name
  | EAssert e -> pf fmt "@[<hov 1>Assert(%a)@]" s_expr e
  | EFatalError error ->
    pf fmt "FatalError<%s>" (Catala_runtime.error_to_string error)
  | EFatalError_pos { error; _ } ->
    pf fmt "FatalError<%s>" (Catala_runtime.error_to_string error)
  | EPos p -> pf fmt "Pos<%s>" (Pos.to_string_shorter p)
  | EDefault { excepts; just; cons } ->
    pf fmt "@[<hov 1>Default(@,%a,@ %a,@ %a)@]" ppl excepts s_expr just s_expr
      cons
  | EPureDefault e -> pf fmt "@[<hov 1>PureDefault(@,%a)@]" s_expr e
  | EEmpty -> pf fmt "Empty"
  | EErrorOnEmpty e -> pf fmt "@[<hov 1>ErrorOnEmpty(@,%a)@]" s_expr e
  | ECustom _ -> pf fmt "Custom<..>"
  | EBad -> pf fmt "Bad"

let runtime_to_pos rpos =
  let pos =
    let open Catala_runtime in
    Pos.from_info rpos.filename rpos.start_line rpos.start_column rpos.end_line
      rpos.end_column
  in
  Pos.overwrite_law_info pos rpos.law_headings

let rec trace (ppf : Format.formatter) (trace : Catala_runtime.trace) =
  Format.fprintf ppf "@[<v>%a@]"
    Format.(pp_print_list ~pp_sep:pp_print_cut trace_element)
    trace

and trace_element =
  let last_printed_pos = ref None in
  fun (ppf : Format.formatter)
    ({ kind; pos; value; sub_trace } : Catala_runtime.trace_element)
  ->
    let pp_pos ppf p =
      let rp = runtime_to_pos p in
      match !last_printed_pos with
      | None ->
        last_printed_pos := Some rp;
        (Pos.format_loc_text ~pp_file:Message.pp_pos ()) ppf (runtime_to_pos p)
      | Some rp' when rp <> rp' ->
        last_printed_pos := Some rp;
        (Pos.format_loc_text ~pp_file:Message.pp_pos ()) ppf (runtime_to_pos p)
      | _ -> ()
    in
    let open Catala_runtime in
    let open Format in
    let pp_value ppf value =
      match value with
      | None -> Format.pp_print_as ppf 1 "∅"
      | Some v -> fprintf ppf "@{<magenta>%a@}" Value.format v
    in
    let pp_sub_trace ppf =
      if sub_trace = [] then () else fprintf ppf "@ %a" trace sub_trace
    in
    match kind with
    | ScopeCall { name = scope_name; decl_pos = _ } ->
      fprintf ppf "@<1>%s Entering scope @{<cyan3>%s@}@ " "→" scope_name;
      fprintf ppf "@[<v 2>%a%t@]@ " pp_pos pos pp_sub_trace;
      fprintf ppf "@[<hov 2>@<1>%s Exiting Scope %s:@ %a@]" "←" scope_name
        pp_value value
    | ScopeVarDef { var; io } ->
      fprintf ppf "@[<hov 2>@<1>%s Scope%s variable definition %a:@ @[%a@]@]@ "
        "≔"
        (if io.io_input = Reentrant then " context"
         else if io.io_input = OnlyInput then " input"
         else "")
        lit_style var.name pp_value value;
      fprintf ppf "@[<v 2>%a%t@]" pp_pos var.decl_pos pp_sub_trace
    | LocalVarDef var_name ->
      fprintf ppf "@[<hov 2>@<1>%s Local variable %a definition:@ @[%a@]@]@ "
        "≔" lit_style var_name pp_value value;
      fprintf ppf "@[<v 2>%a%t@]" pp_pos pos pp_sub_trace
    | LocalTupDef names ->
      fprintf ppf "@[<hov 2>@<1>%s Local variables (%a) definition:@ @[%a@]@]@ "
        "≔"
        (pp_print_list ~pp_sep:(fun ppf () -> fprintf ppf ",") lit_style)
        names pp_value value;
      fprintf ppf "@[<v 2>%a%t@]" pp_pos pos pp_sub_trace
    | FunCall { name = func_name; decl_pos } ->
      fprintf ppf "@<1>%s Applying function %a@ " "→" lit_style func_name;
      fprintf ppf "@[<v 2>%a%t@]@ " pp_pos decl_pos pp_sub_trace;
      fprintf ppf "@[<hov 2>@<1>%s Function %a applied:@ @[%a@]@]" "←" lit_style
        func_name pp_value value
    | BranchingCondition ->
      fprintf ppf "@<1>%s Condition evaluated to %a@," "⊡" pp_value value;
      fprintf ppf "@[<v 2>%a%t@]" pp_pos pos pp_sub_trace
    | IfBranching ->
      fprintf ppf "@<1>%s Branch taken@ " "⊸";
      fprintf ppf "@[<v 2>%a%t@]" pp_pos pos pp_sub_trace
    | MatchBranching { constructor_name } ->
      fprintf ppf "@<1>%s Branch taken: case %a@," "⊸" lit_style
        constructor_name;
      fprintf ppf "@[<v 2>%a%t@]" pp_pos pos pp_sub_trace
    | Assertion ->
      fprintf ppf "@<1>%s Assertion@," "⊹";
      fprintf ppf "@[<v 2>%a%t@]" pp_pos pos pp_sub_trace
    | Exception { label; cons_pos } ->
      let is_fulfilled =
        match value with
        | Some (Catala_runtime.Value.V (Bool, true)) -> true
        | _ (* should only ever be true/false *) -> false
      in
      let format_decision ppf =
        if is_fulfilled then fprintf ppf "@{<green>fulfilled@}"
        else fprintf ppf "@{<brown>not fulfilled@}"
      in
      let format_label ppf =
        Option.iter (fun (lbl, _pos) -> fprintf ppf " %a" lit_style lbl) label
      in
      fprintf ppf "⊕ Definition%t %t@ " format_label format_decision;
      if is_fulfilled then (
        fprintf ppf "%a@ @<1>%s Consequence:@ " pp_pos pos "⊸";
        fprintf ppf "@[<v 2>%a%t@]" pp_pos cons_pos pp_sub_trace)
      else fprintf ppf "@[<v 2>%a%t@]" pp_pos pos pp_sub_trace
    | Error { error; locs; message } ->
      fprintf ppf "@{<red;bold>@<1>%s Error: %s%t@}" "⨉"
        (Catala_runtime.error_message error) (fun ppf ->
          match message with
          | Some message -> Format.fprintf ppf " (%s)" message
          | None -> ());
      fprintf ppf "%a" pp_pos pos;
      if locs = [] then ()
      else begin
        pp_print_cut ppf ();
        fprintf ppf "@[<v 2>Related locations:@ %a@]"
          (pp_print_list ~pp_sep:pp_print_cut pp_pos)
          locs
      end;
      pp_sub_trace ppf