pretty.ml 17.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Format
open Pp
open Util
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
26
open Decl
27
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
28
open Task
29

30
let iprinter,tprinter,lprinter,pprinter =
31 32
  let bl = ["theory"; "type"; "logic"; "inductive"; "meta";
            "axiom"; "lemma"; "goal"; "use"; "clone"; "prop";
33 34 35 36 37
            "namespace"; "import"; "export"; "end";
            "forall"; "exists"; "and"; "or"; "not";
            "true"; "false"; "if"; "then"; "else";
            "let"; "in"; "match"; "with"; "as"; "epsilon" ]
  in
38 39 40 41 42
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
  let usanitize = sanitizer char_to_ualpha char_to_alnumus in
  create_ident_printer bl ~sanitizer:isanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
Andrei Paskevich's avatar
Andrei Paskevich committed
43
  create_ident_printer bl ~sanitizer:isanitize,
44 45 46 47 48 49
  create_ident_printer bl ~sanitizer:usanitize

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
  forget_all lprinter;
50
  forget_all pprinter
51

52
let tv_set = ref Sid.empty
53

54 55
(* type variables always start with a quote *)
let print_tv fmt tv =
56
  tv_set := Sid.add tv.tv_name !tv_set;
57 58
  let sanitizer n = "'" ^ n in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer tv.tv_name)
59

60 61 62 63 64 65
let forget_tvs () =
  Sid.iter (forget_id iprinter) !tv_set;
  tv_set := Sid.empty

(* logic variables always start with a lower case letter *)
let print_vs fmt vs =
66 67
  let sanitizer = String.uncapitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
68

69
let forget_var vs = forget_id iprinter vs.vs_name
70

71 72
(* theory names always start with an upper case letter *)
let print_th fmt th =
73 74
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)
75

76 77
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)
78

79
let print_ls fmt ls =
80 81 82 83 84
  fprintf fmt "%s" (id_unique lprinter ls.ls_name)

let print_cs fmt ls =
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique lprinter ~sanitizer ls.ls_name)
85

86
let print_pr fmt pr =
87
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
88 89 90

(** Types *)

91
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
92

93
let rec print_ty_node inn fmt ty = match ty.ty_node with
94
  | Tyvar v -> print_tv fmt v
Andrei Paskevich's avatar
Andrei Paskevich committed
95 96
  | Tyapp (ts, tl) when is_ts_tuple ts -> fprintf fmt "(%a)"
      (print_list comma (print_ty_node false)) tl
97
  | Tyapp (ts, []) -> print_ts fmt ts
98 99 100 101
  | Tyapp (ts, tl) -> fprintf fmt (protect_on inn "%a@ %a")
      print_ts ts (print_list space (print_ty_node true)) tl

let print_ty = print_ty_node false
102 103 104 105 106 107 108 109 110 111

let print_const fmt = function
  | ConstInt s -> fprintf fmt "%s" s
  | ConstReal (RConstDecimal (i,f,None)) -> fprintf fmt "%s.%s" i f
  | ConstReal (RConstDecimal (i,f,Some e)) -> fprintf fmt "%s.%se%s" i f e
  | ConstReal (RConstHexa (i,f,e)) -> fprintf fmt "0x%s.%sp%s" i f e

(* can the type of a value be derived from the type of the arguments? *)
let unambig_fs fs =
  let rec lookup v ty = match ty.ty_node with
112
    | Tyvar u when tv_equal u v -> true
113 114 115 116 117 118 119 120 121 122 123
    | _ -> ty_any (lookup v) ty
  in
  let lookup v = List.exists (lookup v) fs.ls_args in
  let rec inspect ty = match ty.ty_node with
    | Tyvar u when not (lookup u) -> false
    | _ -> ty_all inspect ty
  in
  inspect (of_option fs.ls_value)

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
let rec print_pat_node pri fmt p = match p.pat_node with
  | Pwild ->
      fprintf fmt "_"
  | Pvar v ->
      print_vs fmt v
  | Pas (p, v) ->
      fprintf fmt (protect_on (pri > 1) "%a as %a")
        (print_pat_node 1) p print_vs v
  | Por (p, q) ->
      fprintf fmt (protect_on (pri > 0) "%a | %a")
        (print_pat_node 0) p (print_pat_node 0) q
  | Papp (cs, pl) when is_fs_tuple cs ->
      fprintf fmt (protect_on (pri > 0) "%a")
        (print_list comma (print_pat_node 1)) pl
  | Papp (cs, []) ->
      print_cs fmt cs
  | Papp (cs, pl) ->
      fprintf fmt (protect_on (pri > 1) "%a@ %a")
        print_cs cs (print_list space (print_pat_node 2)) pl

let print_pat = print_pat_node 0
145

146 147
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
148 149 150 151 152 153 154 155 156 157 158

let print_quant fmt = function
  | Fforall -> fprintf fmt "forall"
  | Fexists -> fprintf fmt "exists"

let print_binop fmt = function
  | Fand -> fprintf fmt "and"
  | For -> fprintf fmt "or"
  | Fimplies -> fprintf fmt "->"
  | Fiff -> fprintf fmt "<->"

159 160 161 162 163
let prio_binop = function
  | Fand -> 3
  | For -> 2
  | Fimplies -> 1
  | Fiff -> 1
164

165
let print_label fmt l = fprintf fmt "\"%s\"" l
166

167 168
let rec print_term fmt t = print_lterm 0 fmt t
and     print_fmla fmt f = print_lfmla 0 fmt f
169

170 171 172 173
and print_lterm pri fmt t = match t.t_label with
  | [] -> print_tnode pri fmt t
  | ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
      (print_list space print_label) ll (print_tnode 0) t
174

175 176 177 178
and print_lfmla pri fmt f = match f.f_label with
  | [] -> print_fnode pri fmt f
  | ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
      (print_list space print_label) ll (print_fnode 0) f
179

180
and print_tnode pri fmt t = match t.t_node with
181 182 183
  | Tbvar _ ->
      assert false
  | Tvar v ->
184
      print_vs fmt v
185 186
  | Tconst c ->
      print_const fmt c
Andrei Paskevich's avatar
Andrei Paskevich committed
187 188
  | Tapp (fs, tl) when is_fs_tuple fs ->
      fprintf fmt "(%a)" (print_list comma print_term) tl
189 190 191 192 193
  | Tapp (fs, []) when unambig_fs fs ->
      print_ls fmt fs
  | Tapp (fs, []) ->
      fprintf fmt (protect_on (pri > 0) "%a:%a")
        print_ls fs print_ty t.t_ty
194
  | Tapp (fs, tl) when unambig_fs fs ->
195 196
      fprintf fmt (protect_on (pri > 4) "%a@ %a")
        print_ls fs (print_list space (print_lterm 5)) tl
197
  | Tapp (fs, tl) ->
198 199 200
      fprintf fmt (protect_on (pri > 0) "%a@ %a:%a")
        print_ls fs (print_list space (print_lterm 5)) tl
          print_ty t.t_ty
201
  | Tif (f,t1,t2) ->
202 203
      fprintf fmt (protect_on (pri > 0) "if %a@ then %a@ else %a")
        print_fmla f print_term t1 print_term t2
204 205
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
206 207
      fprintf fmt (protect_on (pri > 0) "let %a =@ %a in@ %a")
        print_vs v (print_lterm 4) t1 print_term t2;
208
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
209
  | Tcase (t1,bl) ->
210
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
211
        print_term t1 (print_list newline print_tbranch) bl
212 213
  | Teps fb ->
      let v,f = f_open_bound fb in
214 215
      fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
        print_vsty v print_fmla f;
216
      forget_var v
217

218
and print_fnode pri fmt f = match f.f_node with
219
  | Fapp (ps,[t1;t2]) when ps = ps_equ ->
220 221 222 223
      fprintf fmt (protect_on (pri > 4) "%a =@ %a")
        (print_lterm 4) t1 (print_lterm 4) t2
  | Fapp (ps,[]) ->
      print_ls fmt ps
224
  | Fapp (ps,tl) ->
225 226
      fprintf fmt (protect_on (pri > 4) "%a@ %a")
        print_ls ps (print_list space (print_lterm 5)) tl
227 228
  | Fquant (q,fq) ->
      let vl,tl,f = f_open_quant fq in
229
      fprintf fmt (protect_on (pri > 0) "%a %a%a.@ %a") print_quant q
230 231
        (print_list comma print_vsty) vl print_tl tl print_fmla f;
      List.iter forget_var vl
232 233 234 235 236
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fbinop (b,f1,f2) ->
237 238 239
      let p = prio_binop b in
      fprintf fmt (protect_on (pri > p) "%a %a@ %a")
        (print_lfmla (p + 1)) f1 print_binop b (print_lfmla p) f2
240
  | Fnot f ->
241
      fprintf fmt (protect_on (pri > 4) "not %a") (print_lfmla 4) f
242
  | Fif (f1,f2,f3) ->
243 244
      fprintf fmt (protect_on (pri > 0) "if %a@ then %a@ else %a")
        print_fmla f1 print_fmla f2 print_fmla f3
245 246
  | Flet (t,f) ->
      let v,f = f_open_bound f in
247 248
      fprintf fmt (protect_on (pri > 0) "let %a =@ %a in@ %a")
        print_vs v (print_lterm 4) t print_fmla f;
249
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
250
  | Fcase (t,bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
251
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
252
        print_term t (print_list newline print_fbranch) bl
253

254
and print_tbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
255 256 257
  let p,t = t_open_branch br in
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_term t;
  Svs.iter forget_var p.pat_vars
258

259
and print_fbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
260 261 262
  let p,f = f_open_branch br in
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_fmla f;
  Svs.iter forget_var p.pat_vars
263

264
and print_tl fmt tl =
265
  if tl = [] then () else fprintf fmt "@ [%a]"
266
    (print_list alt (print_list comma print_expr)) tl
267

268
and print_expr fmt = e_apply (print_term fmt) (print_fmla fmt)
269 270 271

(** Declarations *)

272 273 274 275
let print_tv_arg fmt tv = fprintf fmt "@ %a" print_tv tv
let print_ty_arg fmt ty = fprintf fmt "@ %a" (print_ty_node true) ty
let print_vs_arg fmt vs = fprintf fmt "@ (%a)" print_vsty vs

276
let print_constr fmt cs =
277
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
278
    (print_list nothing print_ty_arg) cs.ls_args
279

280
let print_type_decl fmt (ts,def) = match def with
281 282
  | Tabstract -> begin match ts.ts_def with
      | None ->
283 284
          fprintf fmt "@[<hov 2>type %a%a@]" print_ts ts
            (print_list nothing print_tv_arg) ts.ts_args
285
      | Some ty ->
286 287
          fprintf fmt "@[<hov 2>type %a%a =@ %a@]" print_ts ts
            (print_list nothing print_tv_arg) ts.ts_args print_ty ty
288 289
      end
  | Talgebraic csl ->
290 291
      fprintf fmt "@[<hov 2>type %a%a =@\n@[<hov>%a@]@]"
        print_ts ts (print_list nothing print_tv_arg) ts.ts_args
292
        (print_list newline print_constr) csl
293

294
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
295

296
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
297

298 299 300 301
let print_logic_decl fmt (ls,ld) = match ld with
  | Some ld ->
      let vl,e = open_ls_defn ld in
      fprintf fmt "@[<hov 2>logic %a%a%a =@ %a@]"
302
        print_ls ls (print_list nothing print_vs_arg) vl
303 304 305 306
        (print_option print_ls_type) ls.ls_value print_expr e;
      List.iter forget_var vl
  | None ->
      fprintf fmt "@[<hov 2>logic %a%a%a@]"
307
        print_ls ls (print_list nothing print_ty_arg) ls.ls_args
308 309 310
        (print_option print_ls_type) ls.ls_value

let print_logic_decl fmt d = print_logic_decl fmt d; forget_tvs ()
311

312 313
let print_ind fmt (pr,f) =
  fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr print_fmla f
314

315
let print_ind_decl fmt (ps,bl) =
316
  fprintf fmt "@[<hov 2>inductive %a%a =@ @[<hov>%a@]@]"
317
    print_ls ps (print_list nothing print_ty_arg) ps.ls_args
318
    (print_list newline print_ind) bl;
319
  forget_tvs ()
320

321 322 323 324 325 326 327
let sprint_pkind = function
  | Paxiom -> "axiom"
  | Plemma -> "lemma"
  | Pgoal  -> "goal"
  | Pskip  -> "skip"

let print_pkind fmt k = pp_print_string fmt (sprint_pkind k)
328

329 330 331 332 333
let print_prop_decl fmt (k,pr,f) =
  fprintf fmt "@[<hov 2>%a %a : %a@]" print_pkind k
    print_pr pr print_fmla f;
  forget_tvs ()

334 335 336 337 338 339
let print_decl fmt d = match d.d_node with
  | Dtype tl  -> print_list newline print_type_decl fmt tl
  | Dlogic ll -> print_list newline print_logic_decl fmt ll
  | Dind il   -> print_list newline print_ind_decl fmt il
  | Dprop p   -> print_prop_decl fmt p

340 341 342 343 344 345 346 347
let print_inst_ts fmt (ts1,ts2) =
  fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2

let print_inst_ls fmt (ls1,ls2) =
  fprintf fmt "logic %a = %a" print_ls ls1 print_ls ls2

let print_inst_pr fmt (pr1,pr2) =
  fprintf fmt "prop %a = %a" print_pr pr1 print_pr pr2
348

349
let print_meta_arg fmt = function
350 351 352 353 354
  | MAts ts -> fprintf fmt "type %a" print_ts ts
  | MAls ls -> fprintf fmt "logic %a" print_ls ls
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
355 356 357

let print_tdecl fmt td = match td.td_node with
  | Decl d ->
Andrei Paskevich's avatar
Andrei Paskevich committed
358
      print_decl fmt d
359
  | Use th ->
360
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
361 362 363
  | Clone (th,tm,lm,pm)
    when Mts.is_empty tm && Mls.is_empty lm && Mpr.is_empty pm ->
      fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
364 365 366 367
  | Clone (th,tm,lm,pm) ->
      let tm = Mts.fold (fun x y a -> (x,y)::a) tm [] in
      let lm = Mls.fold (fun x y a -> (x,y)::a) lm [] in
      let pm = Mpr.fold (fun x y a -> (x,y)::a) pm [] in
368
      fprintf fmt "@[<hov 2>(* clone %a with %a,@ %a,@ %a *)@]"
369 370 371
        print_th th (print_list comma print_inst_ts) tm
                    (print_list comma print_inst_ls) lm
                    (print_list comma print_inst_pr) pm
372 373
  | Meta (t,al) ->
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
374
        t (print_list comma print_meta_arg) al
375 376 377 378

let print_theory fmt th =
  fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
    print_th th (print_list newline2 print_tdecl) th.th_decls
379

380
let print_task fmt task =
381 382
  fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
    (print_list newline2 print_tdecl) (task_tdecls task)
383

384 385
module NsTree = struct
  type t =
386
    | Namespace of string * namespace * known_map
387 388
    | Leaf      of string

389 390
  let contents ns kn =
    let add_ns s ns acc = Namespace (s, ns, kn) :: acc in
391
    let add_pr s p  acc =
392 393
      let k, _ = find_prop_decl kn p in
      Leaf (sprint_pkind k ^ " " ^ s) :: acc in
394 395 396 397 398 399 400 401 402 403 404 405 406 407
    let add_ls s ls acc =
      if s = "infix ="  && ls_equal ls ps_equ then acc else
      if s = "infix <>" && ls_equal ls ps_neq then acc else
        Leaf ("logic " ^ s) :: acc
    in
    let add_ts s ts acc =
      if s = "int"  && ts_equal ts ts_int  then acc else
      if s = "real" && ts_equal ts ts_real then acc else
        Leaf ("type " ^ s) :: acc
    in
    let acc = Mnm.fold add_ns ns.ns_ns []  in
    let acc = Mnm.fold add_pr ns.ns_pr acc in
    let acc = Mnm.fold add_ls ns.ns_ls acc in
    let acc = Mnm.fold add_ts ns.ns_ts acc in acc
408 409

  let decomp = function
410 411
    | Namespace (s,ns,kn) -> s, contents ns kn
    | Leaf s              -> s, []
412 413
end

414
let print_namespace fmt name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
415
  let module P = Print_tree.Make(NsTree) in
416
  fprintf fmt "@[<hov>%a@]@." P.print
417
    (NsTree.Namespace (name, th.th_export, th.th_known))
418

419 420 421 422 423 424 425 426 427 428 429 430
(* Exception reporting *)

let () = Exn_printer.register
  begin fun fmt exn -> match exn with
  | Ty.TypeMismatch (t1,t2) ->
      fprintf fmt "Type mismatch between %a and %a"
        print_ty t1 print_ty t2
  | Ty.BadTypeArity (ts, ts_arg, app_arg) ->
      fprintf fmt "Bad type arity: type symbol %a must be applied \
                   to %i arguments, but is applied to %i"
        print_ts ts ts_arg app_arg
  | Ty.DuplicateTypeVar tv ->
431 432 433
      fprintf fmt "Type variable %a is used twice" print_tv tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" print_tv tv
434 435 436 437 438 439
  | Term.BadArity (ls, ls_arg, app_arg) ->
      fprintf fmt "Bad arity: symbol %a must be applied \
                   to %i arguments, but is applied to %i"
        print_ls ls ls_arg app_arg
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" print_vsty vs
Andrei Paskevich's avatar
Andrei Paskevich committed
440 441
  | Term.UncoveredVar vs ->
      fprintf fmt "Variable %a uncovered in \"or\"-pattern" print_vsty vs
442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471
  | Term.FunctionSymbolExpected ls ->
      fprintf fmt "Not a function symbol: %a" print_ls ls
  | Term.PredicateSymbolExpected ls ->
      fprintf fmt "Not a predicate symbol: %a" print_ls ls
  | Term.NoMatch ->
      fprintf fmt "Uncatched Term.NoMatch exception: [tf]_match failed"
  | Pattern.ConstructorExpected ls ->
      fprintf fmt "The symbol %a is not a constructor"
        print_ls ls
  | Pattern.NonExhaustive pl ->
      fprintf fmt "Non-exhaustive pattern list:@\n@[<hov 2>%a@]"
        (print_list newline print_pat) pl
  | Decl.IllegalTypeAlias ts ->
      fprintf fmt
        "Type symbol %a is a type alias and cannot be declared as algebraic"
        print_ts ts
  | Decl.InvalidIndDecl (_ls, pr) ->
      fprintf fmt "Ill-formed clause %a in inductive predicate declaration"
        print_pr pr
  | Decl.TooSpecificIndDecl (_ls, pr, t) ->
      fprintf fmt "Clause %a in inductive predicate declaration \
          has too type-specific conclusion %a"
        print_pr pr print_term t
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
      fprintf fmt "Clause %a in inductive predicate declaration \
          contains a negative occurrence of dependent symbol %a"
        print_pr pr print_ls ls1
  | Decl.BadLogicDecl (id1,id2) ->
      fprintf fmt "Ill-formed definition: idents %s and %s are different"
        id1.id_string id2.id_string
472 473
  | Decl.UnboundVar vs ->
      fprintf fmt "Unbound variable: %a" print_vsty vs
474 475 476 477
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
478 479 480 481
  | Decl.EmptyAlgDecl ts ->
      fprintf fmt "Algebraic type %a has no constructors" print_ts ts
  | Decl.EmptyIndDecl ls ->
      fprintf fmt "Inductive predicate %a has no constructors" print_ls ls
482 483 484 485 486 487 488 489 490 491 492 493 494 495
  | Decl.KnownIdent id ->
      fprintf fmt "Ident %s is already declared" id.id_string
  | Decl.UnknownIdent id ->
      fprintf fmt "Ident %s is not yet declared" id.id_string
  | Decl.RedeclaredIdent id ->
      fprintf fmt "Ident %s is already declared, with a different declaration"
        id.id_string
  | Decl.NonExhaustiveExpr (pl, e) ->
      fprintf fmt
        "Non-exhaustive pattern list:@\n@[<hov 2>%a@]@\nin expression %a"
        (print_list newline print_pat) pl print_expr e
  | _ -> raise exn
  end