printer.ml 18.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13

open Format
open Pp
14

15
open Wstdlib
16 17 18 19 20 21 22 23 24 25 26
open Ident
open Ty
open Term
open Decl
open Theory
open Task

(** Register printers *)

type prelude = string list
type prelude_map = prelude Mid.t
27 28
type interface = string list
type interface_map = interface Mid.t
29
type blacklist = string list
30

31
type 'a pp = Pp.formatter -> 'a -> unit
32

33 34
type printer_mapping = {
  lsymbol_m     : string -> Term.lsymbol;
35
  vc_term_loc   : Loc.position option;
36
  queried_terms : Term.term Mstr.t;
37
  list_projections: Ident.ident Mstr.t;
DAILLER Sylvain's avatar
DAILLER Sylvain committed
38
  list_fields: Ident.ident Mstr.t;
39
  list_records: ((string * string) list) Mstr.t;
40
  noarg_constructors: string list;
41
  set_str: Sattr.t Mstr.t
42 43
}

44 45 46 47 48
type printer_args = {
  env        : Env.env;
  prelude    : prelude;
  th_prelude : prelude_map;
  blacklist  : blacklist;
49
  mutable printer_mapping : printer_mapping;
50 51 52
}

type printer = printer_args -> ?old:in_channel -> task pp
53

54
type reg_printer = Pp.formatted * printer
55

56
let printers : reg_printer Hstr.t = Hstr.create 17
57 58 59 60

exception KnownPrinter of string
exception UnknownPrinter of string

61 62
let get_default_printer_mapping = {
  lsymbol_m = (function _ -> raise Not_found);
63
  vc_term_loc = None;
64
  queried_terms = Mstr.empty;
65
  list_projections = Mstr.empty;
DAILLER Sylvain's avatar
DAILLER Sylvain committed
66
  list_fields = Mstr.empty;
67
  list_records = Mstr.empty;
68
  noarg_constructors = [];
69
  set_str = Mstr.empty
70 71
}

72
let register_printer ~desc s p =
73 74
  if Hstr.mem printers s then raise (KnownPrinter s);
  Hstr.replace printers s (desc, p)
75 76

let lookup_printer s =
77
  try snd (Hstr.find printers s)
78 79
  with Not_found -> raise (UnknownPrinter s)

80 81
let list_printers () =
  Hstr.fold (fun k (desc,_) acc -> (k,desc)::acc) printers []
82

Andrei Paskevich's avatar
Andrei Paskevich committed
83 84
let () = register_printer
  ~desc:"Dummy@ printer@ with@ no@ output@ (used@ for@ debugging)." "(null)"
85
  (fun _ ?old:_ _ _ -> ())
86

87 88
(** Syntax substitutions *)

89
(*
90 91
let opt_search_forward re s pos =
  try Some (Str.search_forward re s pos) with Not_found -> None
92
*)
93

94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
(* specialized version of opt_search_forward, searching for strings
   matching '%' [tv]? [0-9]+ [search_forward s pos] search from
   starting position [pos], in the string [s], and returns either None
   if no substrings match, or [Some(b,e)] if the substring between
   positions [b] included and [e] excluded matches (without the leading '%').
*)

let is_digit ch = match ch with '0'..'9' -> true | _ -> false

let opt_search_forward s pos =
  let l = String.length s in
  let b = ref pos in
  let i = ref pos in
  try
    while !i < l-1 do
      if s.[!i] = '%' then begin
        incr i;
        b := !i;
        begin match s.[!i] with
        | 't' | 'v' -> incr i
        | _ -> ()
        end;
        let e = !i in
        while !i < l && is_digit s.[!i] do incr i done;
        if !i > e then raise Exit
      end;
      incr i
    done;
    None
  with Exit -> Some(!b,!i)

Clément Fumex's avatar
Clément Fumex committed
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147
let opt_search_forward_literal_format s pos =
  let l = String.length s in
  let b = ref pos in
  let i = ref pos in
  try
    while !i < l-1 do
      if s.[!i] = '%' then begin
        incr i;
        b := !i;
        begin match s.[!i] with
        | 's' | 'e' | 'm' -> incr i; (* float literals *)
        | _ -> ()
        end;
        while !i < l && is_digit s.[!i] do incr i done;
        begin match s.[!i] with
        | 'b' | 'x' | 'o' | 'd' -> incr i; raise Exit
        | _ -> ()
        end;
      end;
      incr i
    done;
    None
  with Exit -> Some(!b,!i)
148

Clément Fumex's avatar
Clément Fumex committed
149
let global_substitute_fmt search_fun repl_fun text fmt =
150 151
  let len = String.length text in
  let rec replace start =
Clément Fumex's avatar
Clément Fumex committed
152
    match search_fun text start with
153 154 155 156 157 158
    | None ->
      pp_print_string fmt (String.sub text start (len - start))
    | Some(pos,end_pos) ->
      pp_print_string fmt (String.sub text start (pos - start - 1));
      repl_fun text pos end_pos fmt;
      replace end_pos
159
  in
160
  replace 0
161

Clément Fumex's avatar
Clément Fumex committed
162
let iter_group search_fun iter_fun text =
163 164 165
  let rec iter start last_was_empty =
    let startpos = if last_was_empty then start + 1 else start in
    if startpos < String.length text then
Clément Fumex's avatar
Clément Fumex committed
166
      match search_fun text startpos with
167
      | None -> ()
168 169
      | Some (pos,end_pos) ->
          iter_fun text pos end_pos;
170 171 172 173 174 175 176
          iter end_pos (end_pos = pos)
  in
  iter 0 false

exception BadSyntaxIndex of int
exception BadSyntaxArity of int * int

177 178 179
let int_of_string s =
  try int_of_string s
  with _ ->
180
    Format.eprintf "bad argument for int_of_string: %s@." s;
181 182
    assert false

183
let check_syntax s len =
184 185
  let arg s b e =
    let i = int_of_string (String.sub s b (e-b)) in
186 187
    if i <= 0 then raise (BadSyntaxIndex i);
    if i > len then raise (BadSyntaxArity (len,i));
188
    ()
189
  in
Clément Fumex's avatar
Clément Fumex committed
190
  iter_group opt_search_forward arg s
191

192
let check_syntax_logic ls s =
193 194 195
  let len = List.length ls.ls_args in
  let ret = ls.ls_value <> None in
  let nfv = Stv.cardinal (ls_ty_freevars ls) in
196 197 198
  let arg s b e =
    if s.[b] = 't' then begin
      let grp = String.sub s (b+1) (e-b-1) in
199 200
      let i = int_of_string grp in
      if i < 0 || (not ret && i = 0) then raise (BadSyntaxIndex i);
201
      if i > len then raise (BadSyntaxArity (len,i))
202 203
    end else if s.[b] = 'v' then begin
      let grp = String.sub s (b+1) (e-b-1) in
204 205 206
      let i = int_of_string grp in
      if i < 0 || i >= nfv then raise (BadSyntaxIndex i)
    end else begin
207
      let grp = String.sub s b (e-b) in
208 209 210
      let i = int_of_string grp in
      if i <= 0 then raise (BadSyntaxIndex i);
      if i > len then raise (BadSyntaxArity (len,i));
211
    end
212
  in
Clément Fumex's avatar
Clément Fumex committed
213 214 215 216 217 218 219 220 221 222 223
  iter_group opt_search_forward arg s

let check_syntax_literal _ts s =
  let count = ref 0 in
  let arg _s _b _e =
    incr count;
  (* nothing else to check ?! *)
  in
  iter_group opt_search_forward_literal_format arg s
  (* if !count <> 1 then *)
    (* raise (BadSyntaxArity (1,!count)) *)
224

225
let syntax_arguments_prec s print pl fmt l =
226
  let args = Array.of_list l in
227 228
  let precs = Array.of_list pl in
  let lp = Array.length precs in
229 230
  let repl_fun s b e fmt =
    let i = int_of_string (String.sub s b (e-b)) in
231 232 233 234 235
    let p =
      if i < lp then precs.(i)
      else if lp = 0 then 0
      else precs.(0) - 1 in
    print p fmt args.(i-1) in
Clément Fumex's avatar
Clément Fumex committed
236
  global_substitute_fmt opt_search_forward repl_fun s fmt
237

238 239 240
let syntax_arguments s print fmt l =
  syntax_arguments_prec s (fun _ f a -> print f a) [] fmt l

241 242 243 244 245 246 247
(* return the type arguments of a symbol application, sorted according
   to their (formal) names *)
let get_type_arguments t = match t.t_node with
  | Tapp (ls, tl) ->
      let m = oty_match Mtv.empty ls.ls_value t.t_ty in
      let m = List.fold_left2
        (fun m ty t -> oty_match m (Some ty) t.t_ty) m ls.ls_args tl in
248 249 250
      let name tv = Mstr.add tv.tv_name.id_string in
      let m = Mtv.fold name m Mstr.empty in
      Array.of_list (Mstr.values m)
251 252 253
  | _ ->
      [||]

254 255
let gen_syntax_arguments_typed_prec
      ty_of tys_of s print_arg print_type t pl fmt l =
256
  let args = Array.of_list l in
257 258
  let precs = Array.of_list pl in
  let lp = Array.length precs in
259 260 261
  let repl_fun s b e fmt =
    if s.[b] = 't' then
      let grp = String.sub s (b+1) (e-b-1) in
262 263
      let i = int_of_string grp in
      if i = 0
264 265
      then print_type fmt (ty_of t)
      else print_type fmt (ty_of args.(i-1))
266 267
    else if s.[b] = 'v' then
      let grp = String.sub s (b+1) (e-b-1) in
268
      let m = tys_of t in
269
      print_type fmt m.(int_of_string grp)
270
    else
271
      let grp = String.sub s b (e-b) in
272
      let i = int_of_string grp in
273 274 275 276 277
      let p =
        if i < lp then precs.(i)
        else if lp = 0 then 0
        else precs.(0) - 1 in
      print_arg p fmt args.(i-1) in
Clément Fumex's avatar
Clément Fumex committed
278
  global_substitute_fmt opt_search_forward repl_fun s fmt
279

280 281 282 283 284
let syntax_arguments_typed_prec =
  gen_syntax_arguments_typed_prec t_type get_type_arguments

let syntax_arguments_typed s print_arg print_type t fmt l =
  syntax_arguments_typed_prec s (fun _ f a -> print_arg f a) print_type t [] fmt l
285

Clément Fumex's avatar
Clément Fumex committed
286 287
let syntax_range_literal s fmt c =
  let f s b e fmt =
288
    let v = c.Number.il_int in
Clément Fumex's avatar
Clément Fumex committed
289 290 291 292 293 294 295 296 297 298 299 300 301
    let base = match s.[e-1] with
      | 'x' -> 16
      | 'd' -> 10
      | 'o' -> 8
      | 'b' -> 2
      | _ -> assert false
    in
    let digits =
      if e > b + 1 then
        Some (int_of_string (String.sub s b (e-b-1)))
      else
        None
    in
302
    if base = 10 then begin
303 304
        if BigInt.lt v BigInt.zero then fprintf fmt "-";
        Number.print_in_base base digits fmt (BigInt.abs v)
305 306 307
      end
    else
      let v =
308
        if BigInt.lt v BigInt.zero then
309
          match digits with
310 311 312
          | Some d ->
              BigInt.add (BigInt.pow_int_pos base d) v
          | None -> failwith ("number of digits must be given for printing negative literals in base " ^ string_of_int base)
313 314 315
        else v
      in
      Number.print_in_base base digits fmt v
Clément Fumex's avatar
Clément Fumex committed
316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333
  in
  global_substitute_fmt opt_search_forward_literal_format f s fmt

let syntax_float_literal s fp fmt c =
  let f s b e fmt =
    let base = match s.[e-1] with
      | 'x' -> 16
      | 'd' -> 10
      | 'o' -> 8
      | 'b' -> 2
      | _ -> assert false
    in
    let digits =
      if e > b + 2 then
        Some (int_of_string (String.sub s (b+1) (e-b-2)))
      else
        None
    in
334 335
    let e,m = Number.compute_float c fp in
    let m,sg = if BigInt.lt m BigInt.zero then BigInt.abs m, BigInt.one else m, BigInt.zero in
Clément Fumex's avatar
Clément Fumex committed
336
    match s.[b] with
337
    | 's' -> Number.print_in_base base digits fmt sg
Clément Fumex's avatar
Clément Fumex committed
338 339 340 341 342 343
    | 'e' -> Number.print_in_base base digits fmt e
    | 'm' -> Number.print_in_base base digits fmt m
    | _ -> assert false
  in
  global_substitute_fmt opt_search_forward_literal_format f s fmt

344 345
(** {2 use printers} *)

346
let print_prelude fmt pl =
347 348
  let println fmt s = fprintf fmt "%s@\n" s in
  print_list nothing println fmt pl
349

350 351
let print_interface = print_prelude

352
let print_prelude_of_theories th_used fmt pm =
353 354 355 356 357
  let ht = Hid.create 5 in
  List.iter (fun { th_name = id } ->
    if not (Hid.mem ht id) then begin
      print_prelude fmt (Mid.find_def [] id pm);
      Hid.add ht id () end) th_used
358

359 360
let print_th_prelude task fmt pm =
  let th_used = task_fold (fun acc -> function
361
    | { td_node = Use th | Clone (th,_) } -> th::acc
362 363
    | _ -> acc) [] task
  in
364 365
  print_prelude_of_theories th_used fmt pm

366
(*
367
let print_prelude_for_theory th fmt pm =
368 369 370 371
  let rec get_th_used acc th = List.fold_left (fun acc -> function
    | { td_node = Use th } -> th :: get_th_used acc th
    | { td_node = Clone (th,_) } -> th::acc
    | _ -> acc) acc th.th_decls
372
  in
373
  let th_used = List.rev (get_th_used [] th) in
374
  print_prelude_of_theories th_used fmt pm
375
*)
376

377 378
exception KnownTypeSyntax of tysymbol
exception KnownLogicSyntax of lsymbol
379 380
exception TooManyTypeOverride of tysymbol
exception TooManyLogicOverride of lsymbol
381

382
let meta_syntax_type = register_meta "syntax_type" [MTtysymbol; MTstring; MTint]
Andrei Paskevich's avatar
Andrei Paskevich committed
383
  ~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ type@ symbol.@ \
384 385
         Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax type'@ rule."

386
let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring; MTint]
Andrei Paskevich's avatar
Andrei Paskevich committed
387 388
  ~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ function/predicate@ \
         symbol.@ \
389
         Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax function'@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
390
         or@ 'syntax predicate'@ rules."
391

Clément Fumex's avatar
Clément Fumex committed
392 393 394 395 396
let meta_syntax_literal = register_meta "syntax_literal" [MTtysymbol; MTstring; MTint]
  ~desc:"Specify@ the@ syntax@ used@ to@ pretty-print@ a@ range@ literal.@ \
         Can@ be@ specified@ in@ the@ driver@ with@ the@ 'syntax literal'@ \
         rules."

Andrei Paskevich's avatar
Andrei Paskevich committed
397
let meta_remove_prop = register_meta "remove_prop" [MTprsymbol]
398 399
    ~desc:"Remove@ a@ logical@ proposition@ from@ proof@ obligations.@ \
           Can@ be@ specified@ in@ the@ driver@ with@ the@ 'remove prop'@ rule."
400

Andrei Paskevich's avatar
Andrei Paskevich committed
401 402 403
let meta_remove_type = register_meta "remove_type" [MTtysymbol]
  ~desc:"Remove@ a@ type@ symbol@ from@ proof@ obligations.@ \
         Used@ in@ bisection."
404

Andrei Paskevich's avatar
Andrei Paskevich committed
405 406 407
let meta_remove_logic = register_meta "remove_logic" [MTlsymbol]
  ~desc:"Remove@ a@ function/predicate@ symbol@ from@ proof@ obligations.@ \
         Used@ in@ bisection."
408

Andrei Paskevich's avatar
Andrei Paskevich committed
409
let meta_realized_theory = register_meta "realized_theory" [MTstring; MTstring]
Andrei Paskevich's avatar
Andrei Paskevich committed
410
  ~desc:"Specify@ that@ a@ Why3@ theory@ is@ realized@ as@ a@ module@ \
Andrei Paskevich's avatar
Andrei Paskevich committed
411
         in@ an@ ITP."
412

413 414
let check_syntax_type ts s = check_syntax s (List.length ts.ts_args)

415
let syntax_type ts s b =
416
  check_syntax_type ts s;
417
  create_meta meta_syntax_type [MAts ts; MAstr s; MAint (if b then 1 else 0)]
418

419
let syntax_logic ls s b =
420
  check_syntax_logic ls s;
421
  create_meta meta_syntax_logic [MAls ls; MAstr s; MAint (if b then 1 else 0)]
422

Clément Fumex's avatar
Clément Fumex committed
423 424 425 426
let syntax_literal ts s b =
  check_syntax_literal ts s;
  create_meta meta_syntax_literal [MAts ts; MAstr s; MAint (if b then 1 else 0)]

427 428
let remove_prop pr =
  create_meta meta_remove_prop [MApr pr]
429

430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447
type syntax_map = (string * int) Mid.t

let change_override e e' rs ov = function
  | None         -> Some (rs,ov)
  | Some (_,0)   ->
    begin match ov with
      | 0 -> raise e
      | 1 -> Some (rs, 2)
      | _ -> assert false
    end
  | Some (rs',1) ->
    begin match ov with
      | 0 -> Some (rs',2)
      | 1 -> raise e'
      | _ -> assert false
    end
  | Some (_,2)   -> raise e'
  | _            -> assert false
448 449

let sm_add_ts sm = function
450 451 452 453
  | [MAts ts; MAstr rs; MAint ov] ->
    Mid.change
      (change_override (KnownTypeSyntax ts) (TooManyTypeOverride ts)
         rs ov) ts.ts_name sm
454 455 456
  | _ -> assert false

let sm_add_ls sm = function
457 458 459 460
  | [MAls ls; MAstr rs; MAint ov] ->
    Mid.change
      (change_override (KnownLogicSyntax ls) (TooManyLogicOverride ls)
         rs ov) ls.ls_name sm
461 462 463
  | _ -> assert false

let sm_add_pr sm = function
464
  | [MApr pr] -> Mid.add pr.pr_name ("",0) sm
465 466 467 468 469 470 471 472 473
  | _ -> assert false

let get_syntax_map task =
  let sm = Mid.empty in
  let sm = Task.on_meta meta_syntax_type sm_add_ts sm task in
  let sm = Task.on_meta meta_syntax_logic sm_add_ls sm task in
  let sm = Task.on_meta meta_remove_prop sm_add_pr sm task in
  sm

Clément Fumex's avatar
Clément Fumex committed
474 475 476
let get_rliteral_map task =
  Task.on_meta meta_syntax_literal sm_add_ts Mid.empty task

477
let add_syntax_map td sm = match td.td_node with
Clément Fumex's avatar
Clément Fumex committed
478 479 480 481 482 483
  | Meta (m, args) when meta_equal m meta_syntax_type ->
      sm_add_ts sm args
  | Meta (m, args) when meta_equal m meta_syntax_logic ->
      sm_add_ls sm args
  | Meta (m, args) when meta_equal m meta_remove_prop ->
      sm_add_pr sm args
484
  | _ -> sm
485

Clément Fumex's avatar
Clément Fumex committed
486 487 488 489
let add_rliteral_map td sm = match td.td_node with
  | Meta (m, args) when meta_equal m meta_syntax_literal ->
      sm_add_ts sm args
  | _ -> sm
490

491 492
let query_syntax sm id =
  try Some (fst (Mid.find id sm)) with Not_found -> None
493

494
let on_syntax_map fn =
495 496 497 498 499 500 501
  Trans.on_meta meta_syntax_type (fun sts ->
  Trans.on_meta meta_syntax_logic (fun sls ->
  Trans.on_meta meta_remove_prop (fun spr ->
    let sm = Mid.empty in
    let sm = List.fold_left sm_add_ts sm sts in
    let sm = List.fold_left sm_add_ls sm sls in
    let sm = List.fold_left sm_add_pr sm spr in
502
    fn sm)))
503

504
let sprint_tdecl (fn : 'a -> Format.formatter -> tdecl -> 'a * string list) =
505
  let buf = Buffer.create 2048 in
506
  let fmt = Format.formatter_of_buffer buf in
507
  fun td (acc,strl) ->
508
    Buffer.reset buf;
509
    let acc, urg = fn acc fmt td in
510
    Format.pp_print_flush fmt ();
511
    acc, Buffer.contents buf :: List.rev_append urg strl
512

513
let sprint_decl (fn : 'a -> Format.formatter -> decl -> 'a * string list) =
514
  let buf = Buffer.create 2048 in
515
  let fmt = Format.formatter_of_buffer buf in
516
  fun td (acc,strl) -> match td.td_node with
517 518
    | Decl d ->
        Buffer.reset buf;
519
        let acc, urg = fn acc fmt d in
520
        Format.pp_print_flush fmt ();
521
        acc, Buffer.contents buf :: List.rev_append urg strl
522
    | _ -> acc, strl
523

524 525 526
(** {2 exceptions to use in transformations and printers} *)

exception UnsupportedType of ty   * string
527
exception UnsupportedTerm of term * string
528
exception UnsupportedPattern of pattern * string
529 530 531 532 533 534 535
exception UnsupportedDecl of decl * string
exception NotImplemented  of        string
exception Unsupported     of        string

(** {3 functions that catch inner error} *)

let unsupportedType e s = raise (UnsupportedType (e,s))
536
let unsupportedTerm e s = raise (UnsupportedTerm (e,s))
537
let unsupportedPattern p s = raise (UnsupportedPattern (p,s))
538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555
let unsupportedDecl e s = raise (UnsupportedDecl (e,s))
let notImplemented    s = raise (NotImplemented s)
let unsupported       s = raise (Unsupported s)

let catch_unsupportedType f e =
  try f e with Unsupported s -> unsupportedType e s

let catch_unsupportedTerm f e =
  try f e with Unsupported s -> unsupportedTerm e s

let catch_unsupportedDecl f e =
  try f e with Unsupported s -> unsupportedDecl e s

let () = Exn_printer.register (fun fmt exn -> match exn with
  | KnownPrinter s ->
      fprintf fmt "Printer '%s' is already registered" s
  | UnknownPrinter s ->
      fprintf fmt "Unknown printer '%s'" s
556 557 558 559 560 561
  | KnownTypeSyntax ts ->
      fprintf fmt "Syntax for type symbol %a is already defined"
        Pretty.print_ts ts
  | KnownLogicSyntax ls ->
      fprintf fmt "Syntax for logical symbol %a is already defined"
        Pretty.print_ls ls
562 563 564 565 566 567
  | TooManyTypeOverride ts ->
      fprintf fmt "Too many syntax overriding for type symbol %a"
        Pretty.print_ts ts
  | TooManyLogicOverride ls ->
      fprintf fmt "Too many syntax overriding for logic symbol %a"
        Pretty.print_ls ls
568 569 570 571 572
  | BadSyntaxIndex i ->
      fprintf fmt "Bad argument index %d, must start with 1" i
  | BadSyntaxArity (i1,i2) ->
      fprintf fmt "Bad argument index %d, must end with %d" i2 i1
  | Unsupported s ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
573
      fprintf fmt "@[<hov 3> Uncaught exception 'Unsupported %s'@]" s
574
  | UnsupportedType (e,s) ->
575
      fprintf fmt "@[@[<hov 3> This type isn't supported:@\n%a@]@\n %s@]"
576
        Pretty.print_ty e s
577
  | UnsupportedTerm (e,s) ->
578
      fprintf fmt "@[@[<hov 3> This expression isn't supported:@\n%a@]@\n %s@]"
579
        Pretty.print_term e s
580 581 582
  | UnsupportedPattern (p,s) ->
      fprintf fmt "@[@[<hov 3> This pattern isn't supported:@\n%a@]@\n %s@]"
        Pretty.print_pat p s
583
  | UnsupportedDecl (d,s) ->
584
      fprintf fmt "@[@[<hov 3> This declaration isn't supported:@\n%a@]@\n %s@]"
585 586 587 588
        Pretty.print_decl d s
  | NotImplemented (s) ->
      fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]" s
  | e -> raise e)