why3printer.ml 14.3 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
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  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

Francois Bobot's avatar
Francois Bobot committed
12 13
(** Why3 printer *)

14 15 16 17 18
open Format
open Pp
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
19
open Decl
20
open Printer
21
open Theory
22

23
let iprinter,aprinter,tprinter,pprinter =
Andrei Paskevich's avatar
Andrei Paskevich committed
24 25
  let bl = ["theory"; "type"; "function"; "predicate"; "inductive";
            "axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
26
            "scope"; "import"; "export"; "end";
Andrei Paskevich's avatar
Andrei Paskevich committed
27 28
            "forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
            "let"; "in"; "match"; "with"; "as"; "epsilon" ] in
29 30 31 32
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
  create_ident_printer bl ~sanitizer:isanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
33
  create_ident_printer bl ~sanitizer:lsanitize,
34
  create_ident_printer bl ~sanitizer:isanitize
35

36 37 38
let forget_tvs () =
  forget_all aprinter

MARCHE Claude's avatar
MARCHE Claude committed
39
let _forget_all () =
40
  forget_all iprinter;
41
  forget_all aprinter;
42
  forget_all tprinter;
Andrei Paskevich's avatar
Andrei Paskevich committed
43
  forget_all pprinter
44 45 46

(* type variables always start with a quote *)
let print_tv fmt tv =
47
  fprintf fmt "'%s" (id_unique aprinter tv.tv_name)
48 49 50

(* logic variables always start with a lower case letter *)
let print_vs fmt vs =
51
  let sanitizer = Strings.uncapitalize in
52
  fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
53 54 55

let forget_var vs = forget_id iprinter vs.vs_name

56 57
(* theory names always start with an upper case letter *)
let print_th fmt th =
58
  let sanitizer = Strings.capitalize in
59 60
  fprintf fmt "%s" (id_unique iprinter ~sanitizer th.th_name)

61 62 63 64
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)

let print_ls fmt ls =
65
  fprintf fmt "%s" (id_unique iprinter ls.ls_name)
66 67

let print_cs fmt ls =
68
  let sanitizer = Strings.capitalize in
69
  fprintf fmt "%s" (id_unique iprinter ~sanitizer ls.ls_name)
70 71

let print_pr fmt pr =
72
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
73

74 75
(* info *)

76
type info = { info_syn : syntax_map }
77

78
let info = ref { info_syn = Mid.empty }
79 80

let query_syntax id = query_syntax !info.info_syn id
81
let query_remove id = Mid.mem id !info.info_syn
82

83 84
(** Types *)

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

87
let rec print_ty_node inn fmt ty = match ty.ty_node with
88
  | Tyvar v -> print_tv fmt v
89 90 91 92 93 94 95 96
  | Tyapp (ts, tl) -> begin match query_syntax ts.ts_name with
      | Some s -> syntax_arguments s (print_ty_node false) fmt tl
      | None -> begin match tl with
          | [] -> print_ts fmt ts
          | tl -> fprintf fmt (protect_on inn "%a@ %a")
              print_ts ts (print_list space (print_ty_node true)) tl
          end
      end
97

98
let print_ty = print_ty_node false
99

100 101 102
(* 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
103
    | Tyvar u when tv_equal u v -> true
104 105 106 107 108 109 110
    | _ -> 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
111
  Opt.fold (fun _ -> inspect) true fs.ls_value
112 113 114

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
115 116 117 118 119 120 121 122 123 124 125 126 127
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) -> begin match query_syntax cs.ls_name with
      | Some s -> syntax_arguments s (print_pat_node 0) fmt pl
128 129
      | None -> begin match pl with
          | [] -> print_cs fmt cs
Andrei Paskevich's avatar
Andrei Paskevich committed
130 131
          | pl -> fprintf fmt (protect_on (pri > 1) "%a@ %a")
              print_cs cs (print_list space (print_pat_node 2)) pl
132 133
          end
      end
134

Andrei Paskevich's avatar
Andrei Paskevich committed
135
let print_pat = print_pat_node 0
136

137 138
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
139

140 141
let print_quant = Pretty.print_quant
let print_binop = Pretty.print_binop
142

143
let prio_binop = function
144 145 146 147
  | Tand -> 3
  | Tor -> 2
  | Timplies -> 1
  | Tiff -> 1
148

Andrei Paskevich's avatar
Andrei Paskevich committed
149 150
let print_attr = Pretty.print_attr
let print_attrs = print_iter1 Sattr.iter space print_attr
151

Andrei Paskevich's avatar
Andrei Paskevich committed
152 153 154
let print_ident_attrs fmt id =
  if not (Sattr.is_empty id.id_attrs) then
    fprintf fmt "@ %a" print_attrs id.id_attrs
155

156 157
let rec print_term fmt t = print_lterm 0 fmt t

158
and print_lterm pri fmt t =
Andrei Paskevich's avatar
Andrei Paskevich committed
159
  if Sattr.is_empty t.t_attrs then print_tnode pri fmt t
160
  else fprintf fmt (protect_on (pri > 0) "%a %a")
Andrei Paskevich's avatar
Andrei Paskevich committed
161
      print_attrs t.t_attrs (print_tnode 0) t
162

163
and print_app pri fs fmt tl =
164 165 166 167
  match query_syntax fs.ls_name with
    | Some s -> syntax_arguments s print_term fmt tl
    | None -> begin match tl with
        | [] -> print_ls fmt fs
168 169
        | tl -> fprintf fmt (protect_on (pri > 5) "%a@ %a")
            print_ls fs (print_list space (print_lterm 6)) tl
170 171 172
        end

and print_tnode pri fmt t = match t.t_node with
173 174 175
  | Tvar v ->
      print_vs fmt v
  | Tconst c ->
Clément Fumex's avatar
Clément Fumex committed
176
      Number.print_constant fmt c
177
  | Tapp (fs, tl) when unambig_fs fs ->
178
      print_app pri fs fmt tl
179 180
  | Tapp (fs, tl) ->
      fprintf fmt (protect_on (pri > 0) "%a:%a")
181
        (print_app 5 fs) tl print_ty (t_type t)
182
  | Tif (f,t1,t2) ->
183
      fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
184
        print_term f print_term t1 print_term t2
185 186
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
187
      fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
188
        print_vs v (print_lterm 4) t1 print_term t2;
189
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
190
  | Tcase (t1,bl) ->
191
      fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
192
        print_term t1 (print_list newline print_tbranch) bl
193
  | Teps fb ->
194 195 196 197 198 199 200
      let vl,tl,e = t_open_lambda t in
      if vl = [] then begin
        let v,f = t_open_bound fb in
        fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
          print_vsty v print_term f;
        forget_var v
      end else begin
Andrei Paskevich's avatar
Andrei Paskevich committed
201
        fprintf fmt (protect_on (pri > 0) "fun %a%a ->@ %a")
202 203 204
          (print_list comma print_vsty) vl print_tl tl print_term e;
        List.iter forget_var vl
      end
205 206
  | Tquant (q,fq) ->
      let vl,tl,f = t_open_quant fq in
207
      fprintf fmt (protect_on (pri > 0) "%a %a%a.@ %a") print_quant q
208
        (print_list comma print_vsty) vl print_tl tl print_term f;
209
      List.iter forget_var vl
210 211 212 213
  | Ttrue ->
      fprintf fmt "true"
  | Tfalse ->
      fprintf fmt "false"
214
  | Tbinop (b,f1,f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
215
      let asym = Sattr.mem Term.asym_split f1.t_attrs in
216 217
      let p = prio_binop b in
      fprintf fmt (protect_on (pri > p) "%a %a@ %a")
218
        (print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
219
  | Tnot f ->
220
      fprintf fmt (protect_on (pri > 4) "not %a") (print_lterm 4) f
221 222

and print_tbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
223 224 225
  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
226

227
and print_tl fmt tl =
228
  if tl = [] then () else fprintf fmt "@ [%a]"
229
    (print_list alt (print_list comma print_term)) tl
230 231 232

(** Declarations *)

233 234 235
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
236

237 238 239 240 241 242
let print_constr fmt (cs,pjl) =
  let add_pj pj ty pjl = (pj,ty)::pjl in
  let print_pj fmt (pj,ty) = match pj with
    | Some ls -> fprintf fmt "@ (%a:@,%a)" print_ls ls print_ty ty
    | None -> print_ty_arg fmt ty
  in
243
  fprintf fmt "@[<hov 4>| %a%a%a@]" print_cs cs
Andrei Paskevich's avatar
Andrei Paskevich committed
244
    print_ident_attrs cs.ls_name
245 246
    (print_list nothing print_pj)
    (List.fold_right2 add_pj pjl cs.ls_args [])
247

248
let print_type_decl fmt ts = match ts.ts_def with
Clément Fumex's avatar
Clément Fumex committed
249
  | NoDef ->
250
      fprintf fmt "@[<hov 2>type %a%a%a@]@\n@\n"
Andrei Paskevich's avatar
Andrei Paskevich committed
251
        print_ts ts print_ident_attrs ts.ts_name
252
        (print_list nothing print_tv_arg) ts.ts_args
Clément Fumex's avatar
Clément Fumex committed
253
  | Alias ty ->
254
      fprintf fmt "@[<hov 2>type %a%a%a =@ %a@]@\n@\n"
Andrei Paskevich's avatar
Andrei Paskevich committed
255
        print_ts ts print_ident_attrs ts.ts_name
256
        (print_list nothing print_tv_arg) ts.ts_args print_ty ty
Clément Fumex's avatar
Clément Fumex committed
257 258
  | Range _ir -> (* TODO *)
      fprintf fmt "@[<hov 2>type %a%a%a =@ <range ...>@]@\n@\n"
Andrei Paskevich's avatar
Andrei Paskevich committed
259
        print_ts ts print_ident_attrs ts.ts_name
Clément Fumex's avatar
Clément Fumex committed
260 261 262
        (print_list nothing print_tv_arg) ts.ts_args
  | Float _fp -> (* TODO *)
      fprintf fmt "@[<hov 2>type %a%a%a =@ <float ...>@]@\n@\n"
Andrei Paskevich's avatar
Andrei Paskevich committed
263
        print_ts ts print_ident_attrs ts.ts_name
Clément Fumex's avatar
Clément Fumex committed
264
        (print_list nothing print_tv_arg) ts.ts_args
265 266 267 268 269 270 271 272

let print_type_decl fmt ts =
  if not (query_remove ts.ts_name) then
    (print_type_decl fmt ts; forget_tvs ())

let print_data_decl fst fmt (ts,csl) =
  fprintf fmt "@[<hov 2>%s %a%a%a =@\n@[<hov>%a@]@]@\n@\n"
    (if fst then "type" else "with") print_ts ts
Andrei Paskevich's avatar
Andrei Paskevich committed
273
    print_ident_attrs ts.ts_name
274 275 276 277
    (print_list nothing print_tv_arg) ts.ts_args
    (print_list newline print_constr) csl

let print_data_decl first fmt d =
278
  if not (query_remove (fst d).ts_name) then
279
    (print_data_decl first fmt d; forget_tvs ())
280

281
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
282

Andrei Paskevich's avatar
Andrei Paskevich committed
283 284
let ls_kind ls = if ls.ls_value = None then "predicate" else "function"

285 286 287
let print_param_decl fmt ls =
  fprintf fmt "@[<hov 2>%s %a%a%a%a@]@\n@\n"
    (ls_kind ls) print_ls ls
Andrei Paskevich's avatar
Andrei Paskevich committed
288
    print_ident_attrs ls.ls_name
289 290 291 292 293 294 295 296 297 298 299
    (print_list nothing print_ty_arg) ls.ls_args
    (print_option print_ls_type) ls.ls_value

let print_param_decl fmt ls =
  if not (query_remove ls.ls_name) then
    (print_param_decl fmt ls; forget_tvs ())

let print_logic_decl fst fmt (ls,ld) =
  let vl,e = open_ls_defn ld in
  fprintf fmt "@[<hov 2>%s %a%a%a%a =@ %a@]@\n@\n"
    (if fst then ls_kind ls else "with") print_ls ls
Andrei Paskevich's avatar
Andrei Paskevich committed
300
    print_ident_attrs ls.ls_name
301 302 303
    (print_list nothing print_vs_arg) vl
    (print_option print_ls_type) ls.ls_value print_term e;
  List.iter forget_var vl
304

305
let print_logic_decl first fmt d =
306
  if not (query_remove (fst d).ls_name) then
307
    (print_logic_decl first fmt d; forget_tvs ())
308

309
let print_ind fmt (pr,f) =
310
  fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
Andrei Paskevich's avatar
Andrei Paskevich committed
311
    print_pr pr print_ident_attrs pr.pr_name print_term f
312

313 314 315 316 317
let ind_sign = function
  | Ind   -> "inductive"
  | Coind -> "coinductive"

let print_ind_decl s fst fmt (ps,bl) =
318
  fprintf fmt "@[<hov 2>%s %a%a%a =@ @[<hov>%a@]@]@\n@\n"
319
    (if fst then ind_sign s else "with") print_ls ps
Andrei Paskevich's avatar
Andrei Paskevich committed
320
    print_ident_attrs ps.ls_name
321
    (print_list nothing print_ty_arg) ps.ls_args
322
    (print_list newline print_ind) bl
323

324
let print_ind_decl s first fmt d =
325
  if not (query_remove (fst d).ls_name) then
326
    (print_ind_decl s first fmt d; forget_tvs ())
327

328
let print_pkind = Pretty.print_pkind
329

330
let print_prop_decl fmt (k,pr,f) =
331
  fprintf fmt "@[<hov 2>%a %a%a : %a@]@\n@\n" print_pkind k
Andrei Paskevich's avatar
Andrei Paskevich committed
332
    print_pr pr print_ident_attrs pr.pr_name print_term f
333

334 335 336
let print_prop_decl fmt (k,pr,f) = match k with
  | Paxiom when query_remove pr.pr_name -> ()
  | _ -> print_prop_decl fmt (k,pr,f); forget_tvs ()
337

338 339 340 341 342 343
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

344
let print_decl fmt d = match d.d_node with
345 346 347
  | Dtype ts  -> print_type_decl fmt ts
  | Ddata tl  -> print_list_next nothing print_data_decl fmt tl
  | Dparam ls -> print_param_decl fmt ls
348
  | Dlogic ll -> print_list_next nothing print_logic_decl fmt ll
349
  | Dind (s, il) -> print_list_next nothing (print_ind_decl s) fmt il
350
  | Dprop p   -> print_prop_decl fmt p
351

352
let print_inst_ty fmt (ts1,ty2) =
353 354 355
  fprintf fmt "type %a%a = %a" print_ts ts1
    (print_list_pre space print_tv) ts1.ts_args
    print_ty ty2; forget_tvs ()
356

357 358 359
let print_inst_ts fmt (ts1,ts2) =
  fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2

360
let print_inst_ls fmt (ls1,ls2) =
Andrei Paskevich's avatar
Andrei Paskevich committed
361
  fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
362 363 364

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

let print_meta_arg fmt = function
367
  | MAty ty -> fprintf fmt "type %a" print_ty ty; forget_tvs ()
368
  | MAts ts -> fprintf fmt "type %a" print_ts ts
Andrei Paskevich's avatar
Andrei Paskevich committed
369
  | MAls ls -> fprintf fmt "%s %a" (ls_kind ls) print_ls ls
370 371 372
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
373
  | MAid id -> fprintf fmt "%s" (id_unique iprinter id)
374

375 376 377 378 379 380
let print_qt fmt th =
  if th.th_path = [] then print_th fmt th else
  fprintf fmt "%a.%a"
    (print_list (constant_string ".") string) th.th_path
    print_th th

381 382 383
let print_tdecl fmt td = match td.td_node with
  | Decl d ->
      print_decl fmt d
384
  | Use th ->
385
      fprintf fmt "@[<hov 2>(* use %a *)@]@\n@\n" print_qt th
386 387
  | Clone (th,sm) ->
      let tm = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ts [] in
388
      let ym = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ty [] in
389 390
      let lm = Mls.fold (fun x y a -> (x,y)::a) sm.sm_ls [] in
      let pm = Mpr.fold (fun x y a -> (x,y)::a) sm.sm_pr [] in
391 392 393 394 395
      fprintf fmt "@[<hov 2>(* clone %a with %a%a%a%a *)@]"
        print_qt th (print_list_suf comma print_inst_ts) tm
                    (print_list_suf comma print_inst_ty) ym
                    (print_list_suf comma print_inst_ls) lm
                    (print_list_suf comma print_inst_pr) pm
396
  | Meta (m,al) ->
397
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
398
        m.meta_name (print_list comma print_meta_arg) al
399

400
let print_tdecls =
401
  let print_tdecl sm fmt td =
402
    info := {info_syn = sm}; print_tdecl fmt td; sm, [] in
403 404 405
  let print_tdecl = Printer.sprint_tdecl print_tdecl in
  let print_tdecl task acc = print_tdecl task.Task.task_decl acc in
  Discriminate.on_syntax_map (fun sm -> Trans.fold print_tdecl (sm,[]))
406

407
let print_task args ?old:_ fmt task =
408 409
  (* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
  (* forget_all (); *)
410
  print_prelude fmt args.prelude;
411
  fprintf fmt "theory Task@\n";
412
  print_th_prelude task fmt args.th_prelude;
413 414 415 416 417
  let rec print = function
    | x :: r -> print r; Pp.string fmt x
    | [] -> () in
  print (snd (Trans.apply print_tdecls task));
  fprintf fmt "end@."
418

419
let () = register_printer "why3" print_task
420
  ~desc:"Printer@ for@ the@ logical@ format@ of@ Why3.@ Used@ for@ debugging."