mlw_pretty.ml 17.2 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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 16 17 18 19
open Ident
open Ty
open Term
open Pretty
open Mlw_ty
20
open Mlw_ty.T
21 22 23
open Mlw_expr
open Mlw_decl

24
let debug_print_labels = Debug.register_info_flag "print_labels"
Andrei Paskevich's avatar
Andrei Paskevich committed
25
  ~desc:"Print@ labels@ of@ identifiers@ and@ expressions."
26
let debug_print_locs = Debug.register_info_flag "print_locs"
Andrei Paskevich's avatar
Andrei Paskevich committed
27
  ~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
28
let debug_print_reg_types = Debug.register_info_flag "print_reg_types"
Andrei Paskevich's avatar
Andrei Paskevich committed
29
  ~desc:"Print@ types@ of@ regions@ (mutable@ fields)."
30

Andrei Paskevich's avatar
Andrei Paskevich committed
31 32 33 34
let iprinter =
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  create_ident_printer [] ~sanitizer:isanitize

35 36 37 38 39 40 41 42
let rprinter =
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  create_ident_printer [] ~sanitizer:isanitize

let forget_regs () = Ident.forget_all rprinter
let forget_tvs_regs () = Ident.forget_all rprinter; forget_tvs ()
let forget_all () = Ident.forget_all rprinter; forget_all ()

Andrei Paskevich's avatar
Andrei Paskevich committed
43 44 45 46 47 48 49 50 51
(* Labels and locs - copied from Pretty *)

let print_labels = print_iter1 Slab.iter space print_label

let print_ident_labels fmt id =
  if Debug.test_flag debug_print_labels &&
      not (Slab.is_empty id.id_label) then
    fprintf fmt "@ %a" print_labels id.id_label;
  if Debug.test_flag debug_print_locs then
52
    Opt.iter (fprintf fmt "@ %a" print_loc) id.id_loc
Andrei Paskevich's avatar
Andrei Paskevich committed
53 54 55

(* identifiers *)

56
let print_reg fmt reg =
57
  fprintf fmt "%s" (id_unique rprinter reg.reg_name)
58 59

let print_pv fmt pv =
60
  fprintf fmt "%s%a" (if pv.pv_ghost then "?" else "")
61 62 63 64
    print_vs pv.pv_vs

let forget_pv pv = forget_var pv.pv_vs

Andrei Paskevich's avatar
Andrei Paskevich committed
65 66 67 68 69 70
let print_name fmt id =
  fprintf fmt "%s%a" (id_unique iprinter id) print_ident_labels id

let print_xs fmt xs = print_name fmt xs.xs_name

let print_ps fmt ps =
71
  fprintf fmt "%s%a" (if ps.ps_ghost then "?" else "")
Andrei Paskevich's avatar
Andrei Paskevich committed
72 73 74 75
    print_name ps.ps_name

let forget_ps ps = forget_id iprinter ps.ps_name

76
let print_its fmt ts = print_ts fmt ts.its_ts
77 78 79 80 81

(** Types *)

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

82 83 84 85 86 87
let rec print_ity_node s inn fmt ity = match ity.ity_node with
  | Ityvar v ->
      begin match Mtv.find_opt v s.ity_subst_tv with
        | Some ity -> print_ity_node ity_subst_empty inn fmt ity
        | None     -> print_tv fmt v
      end
88
  | Itypur (ts,tl) when is_ts_tuple ts -> fprintf fmt "(%a)"
89
      (print_list comma (print_ity_node s false)) tl
90 91
  | Itypur (ts,[]) -> print_ts fmt ts
  | Itypur (ts,tl) -> fprintf fmt (protect_on inn "%a@ %a")
92
      print_ts ts (print_list space (print_ity_node s true)) tl
93
  | Ityapp (ts,[],rl) -> fprintf fmt (protect_on inn "%a@ <%a>")
94 95
      print_its ts (print_list comma print_regty)
      (List.map (fun r -> Mreg.find_def r r s.ity_subst_reg) rl)
96
  | Ityapp (ts,tl,rl) -> fprintf fmt (protect_on inn "%a@ <%a>@ %a")
97 98 99
      print_its ts (print_list comma print_regty)
      (List.map (fun r -> Mreg.find_def r r s.ity_subst_reg) rl)
      (print_list space (print_ity_node s true)) tl
100 101

and print_regty fmt reg =
102 103
  if Debug.test_noflag debug_print_reg_types then print_reg fmt reg
  else fprintf fmt "@[%a:@,%a@]" print_reg reg print_ity reg.reg_ity
104

105
and print_ity fmt ity = print_ity_node ity_subst_empty false fmt ity
106 107 108 109 110

let print_reg_opt fmt = function
  | Some r -> fprintf fmt "<%a>" print_regty r
  | None -> ()

Andrei Paskevich's avatar
Andrei Paskevich committed
111 112 113 114 115 116
let print_effect fmt eff =
  let print_xs s xs = fprintf fmt "{%s %a}@ " s print_xs xs in
  let print_reg s r = fprintf fmt "{%s %a}@ " s print_regty r in
  let print_reset r = function
    | None -> print_reg "fresh" r
    | Some u ->
117
        fprintf fmt "{refresh %a@ under %a}@ " print_regty r print_regty u
Andrei Paskevich's avatar
Andrei Paskevich committed
118 119 120 121 122 123 124
  in
  Sreg.iter (print_reg "write") eff.eff_writes;
  Sexn.iter (print_xs  "raise") eff.eff_raises;
  Sreg.iter (print_reg "ghost write") eff.eff_ghostw;
  Sexn.iter (print_xs  "ghost raise") eff.eff_ghostx;
  Mreg.iter print_reset eff.eff_resets

125
let rec print_aty fmt aty =
126
  let print_arg fmt pv = fprintf fmt "%a ->@ " print_ity pv.pv_ity in
127 128
  fprintf fmt "%a%a%a" (print_list nothing print_arg) aty.aty_args
    print_effect aty.aty_spec.c_effect print_vty aty.aty_result
Andrei Paskevich's avatar
Andrei Paskevich committed
129 130

and print_vty fmt = function
131
  | VTarrow aty -> print_aty fmt aty
132
  | VTvalue ity -> print_ity fmt ity
Andrei Paskevich's avatar
Andrei Paskevich committed
133

134
let print_pvty fmt pv = fprintf fmt "@[%a:@,%a@]"
135
  print_pv pv print_ity pv.pv_ity
Andrei Paskevich's avatar
Andrei Paskevich committed
136 137 138 139 140 141

let print_psty fmt ps =
  let print_tvs fmt tvs = if not (Stv.is_empty tvs) then
    fprintf fmt "[%a]@ " (print_list comma print_tv) (Stv.elements tvs) in
  let print_regs fmt regs = if not (Sreg.is_empty regs) then
    fprintf fmt "<%a>@ " (print_list comma print_regty) (Sreg.elements regs) in
142
  let vars = aty_vars ps.ps_aty in
143
  fprintf fmt "@[%a :@ %a%a%a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
144
    print_ps ps
145
    print_tvs (Mtv.set_diff vars.vars_tv ps.ps_subst.ity_subst_tv)
Andrei Paskevich's avatar
Andrei Paskevich committed
146
    print_regs (Mreg.set_diff vars.vars_reg ps.ps_subst.ity_subst_reg)
147
    print_aty ps.ps_aty
Andrei Paskevich's avatar
Andrei Paskevich committed
148

149 150 151 152
(* specification *)

let print_post fmt post =
  let vs,f = open_post post in
153
  fprintf fmt "@[%a ->@ %a@]" print_vs vs print_term f;
154
  Pretty.forget_var vs
155 156 157 158 159 160 161 162 163 164

let print_lv fmt = function
  | LetV pv -> print_pvty fmt pv
  | LetA ps -> print_psty fmt ps

let forget_lv = function
  | LetV pv -> forget_pv pv
  | LetA ps -> forget_ps ps

let rec print_type_v fmt = function
165
  | VTvalue ity -> print_ity fmt ity
166
  | VTarrow aty ->
167
      let print_arg fmt pv = fprintf fmt "@[(%a)@] ->@ " print_pvty pv in
168
      fprintf fmt "%a%a"
169 170 171
        (print_list nothing print_arg) aty.aty_args
        (print_type_c aty.aty_spec) aty.aty_result;
      List.iter forget_pv aty.aty_args
172

173
and print_type_c spec fmt vty =
174
  fprintf fmt "{ %a }@ %a%a@ { %a }"
175 176 177 178
    print_term spec.c_pre
    print_effect spec.c_effect
    print_type_v vty
    print_post spec.c_post
179
    (* TODO: print_xpost *)
Andrei Paskevich's avatar
Andrei Paskevich committed
180

181 182
let print_invariant fmt f =
  fprintf fmt "invariant@ { %a }@ " Pretty.print_term f
Andrei Paskevich's avatar
Andrei Paskevich committed
183 184 185 186 187

let print_variant fmt varl =
  let print_rel fmt = function
    | Some ps -> fprintf fmt "@ [%a]" Pretty.print_ls ps
    | None -> () in
188
  let print_var fmt (t, ps) =
Andrei Paskevich's avatar
Andrei Paskevich committed
189 190 191
    fprintf fmt " %a%a" Pretty.print_term t print_rel ps in
  fprintf fmt "variant@ {%a }@ " (print_list comma print_var) varl

192 193 194 195
let print_invariant fmt f = match f.t_node with
  | Ttrue -> ()
  | _ -> print_invariant fmt f

Andrei Paskevich's avatar
Andrei Paskevich committed
196 197 198 199
let print_variant fmt = function
  | [] -> ()
  | varl -> print_variant fmt varl

Andrei Paskevich's avatar
Andrei Paskevich committed
200 201
(* expressions *)

202 203
let print_ppat fmt ppat = print_pat fmt ppat.ppat_pattern

204 205 206 207 208
let print_ak fmt = function
  | Aassert -> fprintf fmt "assert"
  | Aassume -> fprintf fmt "assume"
  | Acheck  -> fprintf fmt "check"

209 210 211 212 213 214
let print_list_next sep print fmt = function
  | [] -> ()
  | [x] -> print true fmt x
  | x :: r -> print true fmt x; sep fmt ();
      print_list sep (print false) fmt r

215
let is_letrec = function
216
  | [fd] -> fd.fun_lambda.l_spec.c_letrec <> 0
217 218
  | _ -> true

Andrei Paskevich's avatar
Andrei Paskevich committed
219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255
let rec print_expr fmt e = print_lexpr 0 fmt e

and print_lexpr pri fmt e =
  let print_elab pri fmt e =
    if Debug.test_flag debug_print_labels && not (Slab.is_empty e.e_label)
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
      print_labels e.e_label (print_enode 0) e
    else print_enode pri fmt e in
  let print_eloc pri fmt e =
    if Debug.test_flag debug_print_locs && e.e_loc <> None
    then fprintf fmt (protect_on (pri > 0) "@[<hov 0>%a@ %a@]")
      (print_option print_loc) e.e_loc (print_elab 0) e
    else print_elab pri fmt e in
  print_eloc pri fmt e

(*
and print_app pri ls fmt tl = match extract_op ls, tl with
  | _, [] ->
      print_ls fmt ls
  | Some s, [t1] when tight_op s ->
      fprintf fmt (protect_on (pri > 7) "%s%a")
        s (print_lterm 7) t1
  | Some s, [t1] ->
      fprintf fmt (protect_on (pri > 4) "%s %a")
        s (print_lterm 5) t1
  | Some s, [t1;t2] ->
      fprintf fmt (protect_on (pri > 4) "@[<hov 1>%a %s@ %a@]")
        (print_lterm 5) t1 s (print_lterm 5) t2
  | _, [t1;t2] when ls.ls_name.id_string = "mixfix []" ->
      fprintf fmt (protect_on (pri > 6) "%a[%a]")
        (print_lterm 6) t1 print_term t2
  | _, [t1;t2;t3] when ls.ls_name.id_string = "mixfix [<-]" ->
      fprintf fmt (protect_on (pri > 6) "%a[%a <- %a]")
        (print_lterm 6) t1 (print_lterm 5) t2 (print_lterm 5) t3
  | _, tl ->
      fprintf fmt (protect_on (pri > 5) "@[<hov 1>%a@ %a@]")
        print_ls ls (print_list space (print_lterm 6)) tl
256
*)
257

Andrei Paskevich's avatar
Andrei Paskevich committed
258 259 260 261 262 263 264
and print_enode pri fmt e = match e.e_node with
  | Elogic t ->
      fprintf fmt "(%a)" print_term t
  | Evalue v ->
      print_pv fmt v
  | Earrow a ->
      print_ps fmt a
265
  | Eapp (e,v,_) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
266
      fprintf fmt "(%a@ %a)" (print_lexpr pri) e print_pv v
267
  | Elet ({ let_sym = LetV pv ; let_expr = e1 }, e2)
268
    when pv.pv_vs.vs_name.id_string = "_" &&
269
         ity_equal pv.pv_ity ity_unit ->
270 271
      fprintf fmt (protect_on (pri > 0) "%a;@\n%a")
        print_expr e1 print_expr e2;
272
  | Elet ({ let_sym = lv ; let_expr = e1 }, e2) ->
273
      fprintf fmt (protect_on (pri > 0) "@[<hov 2>let %a =@ %a@ in@]@\n%a")
Andrei Paskevich's avatar
Andrei Paskevich committed
274 275
        print_lv lv (print_lexpr 4) e1 print_expr e2;
      forget_lv lv
276
  | Erec (fdl, e) ->
277
      fprintf fmt (protect_on (pri > 0) "%a@ in@\n%a")
278 279
        (print_list_next newline (print_rec (is_letrec fdl))) fdl print_expr e;
      List.iter (fun fd -> forget_ps fd.fun_ps) fdl
280
  | Eif (e0,e1,e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
281
      fprintf fmt (protect_on (pri > 0) "if %a then %a@ else %a")
282
        print_expr e0 print_expr e1 print_expr e2
283 284 285
  | Eassign (pl,e,r,pv) ->
      fprintf fmt (protect_on (pri > 0) "%a.%a <%a> <- %a")
        print_expr e print_ls pl.pl_ls print_regty r print_pv pv
286
  | Ecase (e0,bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
287
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
288
        print_expr e0 (print_list newline print_branch) bl
Andrei Paskevich's avatar
Andrei Paskevich committed
289 290 291 292
  | Eloop (inv,var,e) ->
      fprintf fmt "loop@ %a%a@\n@[<hov>%a@]@\nend"
        print_invariant inv print_variant var print_expr e
  | Efor (pv,(pvfrom,dir,pvto),inv,e) ->
293
      fprintf fmt "@[<hov 2>for@ %a =@ %a@ %s@ %a@ %ado@\n%a@]@\ndone"
Andrei Paskevich's avatar
Andrei Paskevich committed
294 295 296
        print_pv pv print_pv pvfrom
        (if dir = To then "to" else "downto") print_pv pvto
        print_invariant inv print_expr e
297 298
  | Eraise (xs,e) ->
      fprintf fmt "raise (%a %a)" print_xs xs print_expr e
Andrei Paskevich's avatar
Andrei Paskevich committed
299 300 301
  | Etry (e,bl) ->
      fprintf fmt "try %a with@\n@[<hov>%a@]@\nend"
        print_expr e (print_list newline print_xbranch) bl
302 303 304
  | Eabsurd ->
      fprintf fmt "absurd"
  | Eassert (ak,f) ->
305
      fprintf fmt "%a { %a }" print_ak ak print_term f
306 307 308
  | Eabstr (e,spec) ->
    (* TODO: print_spec *)
      fprintf fmt "abstract %a@ { %a }" print_expr e print_post spec.c_post
309 310
  | Eghost e ->
      fprintf fmt "ghost@ %a" print_expr e
311 312
  | Eany spec ->
      fprintf fmt "any@ %a" (print_type_c spec) e.e_vty
313

314 315
and print_branch fmt ({ ppat_pattern = p }, e) =
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_expr e;
Andrei Paskevich's avatar
Andrei Paskevich committed
316
  Svs.iter forget_var p.pat_vars
317

Andrei Paskevich's avatar
Andrei Paskevich committed
318 319 320 321
and print_xbranch fmt (xs, pv, e) =
  fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" print_xs xs print_pv pv print_expr e;
  forget_pv pv

322
and print_rec lr fst fmt { fun_ps = ps ; fun_lambda = lam } =
323 324
  let print_arg fmt pv = fprintf fmt "@[(%a)@]" print_pvty pv in
  fprintf fmt "@[<hov 2>%s (%a)@ %a =@\n{ %a }@\n%a%a@\n{ %a }@]"
325
    (if fst then if lr then "let rec" else "let" else "with")
326 327
    print_psty ps
    (print_list space print_arg) lam.l_args
328 329
    print_term lam.l_spec.c_pre
    print_variant lam.l_spec.c_variant
330
    print_expr lam.l_expr
331 332
    print_post lam.l_spec.c_post
    (* TODO: print_spec *)
333

334
(*
Andrei Paskevich's avatar
Andrei Paskevich committed
335 336 337 338
and print_tl fmt tl =
  if tl = [] then () else fprintf fmt "@ [%a]"
    (print_list alt (print_list comma print_term)) tl
*)
339 340 341 342

(** Type declarations *)

let print_tv_arg fmt tv = fprintf fmt "@ %a" print_tv tv
343 344 345

let print_ty_arg fmt ty =
  fprintf fmt "@ %a" (print_ity_node ity_subst_empty true) ty
346 347

let print_constr fmt (cs,pjl) =
348
  let print_pj fmt (fd,pj) = match pj with
349
    | Some { pl_ls = ls } ->
350
        fprintf fmt "@ (%s%s%a%a:@,%a)"
351 352 353 354
          (if fd.fd_ghost then "ghost " else "")
          (if fd.fd_mut <> None then "mutable " else "")
          print_ls ls print_reg_opt fd.fd_mut print_ity fd.fd_ity
    | None when fd.fd_ghost || fd.fd_mut <> None ->
355
        fprintf fmt "@ (%s%s%a@ %a)"
356 357 358
          (if fd.fd_ghost then "ghost" else "")
          (if fd.fd_mut <> None then "mutable " else "")
          print_reg_opt fd.fd_mut print_ity fd.fd_ity
359
    | None ->
360
        print_ty_arg fmt fd.fd_ity
361
  in
362 363 364
  fprintf fmt "@[<hov 4>| %a%a%a@]" print_cs cs.pl_ls
    print_ident_labels cs.pl_ls.ls_name
    (print_list nothing print_pj)
365
    (List.map2 (fun fd pj -> (fd,pj)) cs.pl_args pjl)
366

367 368 369 370 371 372
let print_head fst fmt ts =
  fprintf fmt "%s %s%s%a%a <%a>%a"
    (if fst then "type" else "with")
    (if ts.its_abst then "abstract " else "")
    (if ts.its_priv then "private " else "")
    print_its ts
373
    print_ident_labels ts.its_ts.ts_name
374
    (print_list comma print_regty) ts.its_regs
375
    (print_list nothing print_tv_arg) ts.its_ts.ts_args
376 377 378 379 380 381 382 383 384 385

let print_ty_decl fmt ts = match ts.its_def with
  | None ->
      fprintf fmt "@[<hov 2>%a@]" (print_head true) ts
  | Some ty ->
      fprintf fmt "@[<hov 2>%a =@ %a@]" (print_head true) ts print_ity ty

let print_ty_decl fmt ts =
  print_ty_decl fmt ts; forget_tvs_regs ()

386 387 388 389 390 391
let print_data_decl fst fmt (ts,csl,inv) =
  let print_inv fmt inv = if ts.its_inv then
    fprintf fmt "@ invariant { %a }" print_post inv else () in
  fprintf fmt "@[<hov 2>%a =@ %a%a@]"
    (print_head fst) ts (print_list newline print_constr) csl
    print_inv inv;
392
  forget_tvs_regs ()
393

394 395
let print_val_decl fmt lv =
  let vty = match lv with
396
    | LetV pv -> VTvalue pv.pv_ity | LetA ps -> VTarrow ps.ps_aty in
397
  fprintf fmt "@[<hov 2>val (%a) :@ %a@]" print_lv lv print_type_v vty;
398 399
  (* FIXME: forget only generalized regions *)
  match lv with LetA _ -> forget_tvs_regs () | _ -> ()
400

401
let print_let_decl fmt { let_sym = lv ; let_expr = e } =
402
  fprintf fmt "@[<hov 2>let %a =@ %a@]" print_lv lv print_expr e;
403 404
  (* FIXME: forget only generalized regions *)
  match lv with LetA _ -> forget_tvs_regs () | _ -> ()
405

406 407
let print_rec_decl lr fst fmt fd =
  print_rec lr fst fmt fd;
408 409
  forget_tvs_regs ()

410 411 412 413
let print_exn_decl fmt xs =
  fprintf fmt "@[<hov 2>exception %a of@ %a@]"
    print_xs xs print_ity xs.xs_ity

414
(* Declarations *)
415 416

let print_pdecl fmt d = match d.pd_node with
417 418
  | PDtype ts -> print_ty_decl fmt ts
  | PDdata tl -> print_list_next newline print_data_decl fmt tl
419
  | PDval  vd -> print_val_decl fmt vd
420
  | PDlet  ld -> print_let_decl fmt ld
421
  | PDrec fdl ->
422
      print_list_next newline (print_rec_decl (is_letrec fdl)) fmt fdl
423
  | PDexn  xs -> print_exn_decl fmt xs
424

425 426 427 428
(* Print exceptions *)

let () = Exn_printer.register
  begin fun fmt exn -> match exn with
429
  | Mlw_ty.BadItyArity (ts, app_arg) ->
430 431
      fprintf fmt "Bad type arity: type symbol %a must be applied \
                   to %i arguments, but is applied to %i"
432 433
        print_its ts (List.length ts.its_ts.ts_args) app_arg
  | Mlw_ty.BadRegArity (ts, app_arg) ->
434 435
      fprintf fmt "Bad region arity: type symbol %a must be applied \
                   to %i regions, but is applied to %i"
436
        print_its ts (List.length ts.its_regs) app_arg
437
  | Mlw_ty.DuplicateRegion r ->
438
      fprintf fmt "Region %a is used twice" print_reg r
439
  | Mlw_ty.UnboundRegion r ->
440
      fprintf fmt "Unbound region %a" print_reg r
441 442 443
  | Mlw_ty.UnboundException xs ->
      fprintf fmt "This function raises %a but does not \
        specify a post-condition for it" print_xs xs
444 445
  | Mlw_ty.RegionMismatch (r1,r2,s) ->
      let r1 = Mreg.find_def r1 r1 s.ity_subst_reg in
446 447
      fprintf fmt "Region mismatch between %a and %a"
        print_regty r1 print_regty r2
448
  | Mlw_ty.TypeMismatch (t1,t2,s) ->
449
      fprintf fmt "Type mismatch between %a and %a"
450
        (print_ity_node s false) t1 print_ity t2
451 452 453 454 455 456
  | Mlw_ty.PolymorphicException (id,_ity) ->
      fprintf fmt "Exception %s has a polymorphic type" id.id_string
  | Mlw_ty.MutableException (id,_ity) ->
      fprintf fmt "The type of exception %s has mutable components" id.id_string
  | Mlw_ty.IllegalAlias _reg ->
      fprintf fmt "This application creates an illegal alias"
457 458 459
  | Mlw_ty.IllegalCompar (tv,_ity) ->
      fprintf fmt "This application instantiates \
          a non-opaque type parameter %a with a program type" print_tv tv
460 461 462
  | Mlw_ty.GhostDiverg ->
      fprintf fmt "This ghost expression contains potentially \
        non-terminating loops or function calls"
Andrei Paskevich's avatar
Andrei Paskevich committed
463
  | Mlw_expr.RdOnlyPLS _ls ->
464 465
      fprintf fmt "Cannot construct or modify values of a private type"
  | Mlw_expr.HiddenPLS pl ->
466
      fprintf fmt "'%a' is a constructor/field of an abstract type \
467
        and cannot be used in a program" print_ls pl.pl_ls;
468
  | Mlw_expr.StaleRegion (_e, id) ->
469 470 471 472 473 474 475 476
      fprintf fmt "This expression prohibits further \
        usage of variable %s" id.id_string
  | Mlw_expr.ValueExpected _e ->
      fprintf fmt "This expression is not a first-order value"
  | Mlw_expr.ArrowExpected _e ->
      fprintf fmt "This expression is not a function and cannot be applied"
  | Mlw_expr.Immutable _e ->
      fprintf fmt "Mutable expression expected"
477 478
  | Mlw_decl.NonupdatableType ity ->
      fprintf fmt "Cannot update values of type @[%a@]" print_ity ity
479 480
  | _ -> raise exn
  end