why3printer.ml 13 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

Francois Bobot's avatar
Francois Bobot committed
20 21
(** Why3 printer *)

22 23 24 25 26 27
open Format
open Pp
open Util
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
28
open Decl
29
open Printer
30
open Theory
31

32
let iprinter,tprinter,pprinter =
Andrei Paskevich's avatar
Andrei Paskevich committed
33 34
  let bl = ["theory"; "type"; "function"; "predicate"; "inductive";
            "axiom"; "lemma"; "goal"; "use"; "clone"; "prop"; "meta";
35
            "namespace"; "import"; "export"; "end";
Andrei Paskevich's avatar
Andrei Paskevich committed
36 37
            "forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
            "let"; "in"; "match"; "with"; "as"; "epsilon" ] in
38 39 40 41
  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,
42
  create_ident_printer bl ~sanitizer:isanitize
43 44 45 46

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
Andrei Paskevich's avatar
Andrei Paskevich committed
47
  forget_all pprinter
48 49 50 51 52

let tv_set = ref Sid.empty

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

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 =
63 64
  let sanitizer = String.uncapitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
65 66 67

let forget_var vs = forget_id iprinter vs.vs_name

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

73 74 75 76
let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)

let print_ls fmt ls =
77
  fprintf fmt "%s" (id_unique iprinter ls.ls_name)
78 79 80

let print_cs fmt ls =
  let sanitizer = String.capitalize in
81
  fprintf fmt "%s" (id_unique iprinter ~sanitizer ls.ls_name)
82 83

let print_pr fmt pr =
84
  fprintf fmt "%s" (id_unique pprinter pr.pr_name)
85

86 87 88
(* info *)

type info = {
Andrei Paskevich's avatar
Andrei Paskevich committed
89
  info_syn : string Mid.t;
90 91 92
  info_rem : Sid.t;
}

93 94 95 96 97 98 99 100
let info = ref {
  info_syn = Mid.empty;
  info_rem = Sid.empty
}

let query_syntax id = query_syntax !info.info_syn id
let query_remove id = Sid.mem id !info.info_rem

101 102
(** Types *)

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

105
let rec print_ty_node inn fmt ty = match ty.ty_node with
106
  | Tyvar v -> print_tv fmt v
107 108 109 110 111 112 113 114
  | 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
115

116
let print_ty = print_ty_node false
117

118 119 120
(* 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
121
    | Tyvar u when tv_equal u v -> true
122 123 124 125 126 127 128
    | _ -> 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
129
  option_apply true inspect fs.ls_value
130 131 132

(** Patterns, terms, and formulas *)

Andrei Paskevich's avatar
Andrei Paskevich committed
133 134 135 136 137 138 139 140 141 142 143 144 145
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
146 147
      | None -> begin match pl with
          | [] -> print_cs fmt cs
Andrei Paskevich's avatar
Andrei Paskevich committed
148 149
          | pl -> fprintf fmt (protect_on (pri > 1) "%a@ %a")
              print_cs cs (print_list space (print_pat_node 2)) pl
150 151
          end
      end
152

Andrei Paskevich's avatar
Andrei Paskevich committed
153
let print_pat = print_pat_node 0
154

155 156
let print_vsty fmt v =
  fprintf fmt "%a:@,%a" print_vs v print_ty v.vs_ty
157

158 159 160
let print_const = Pretty.print_const
let print_quant = Pretty.print_quant
let print_binop = Pretty.print_binop
161

162
let prio_binop = function
163 164 165 166
  | Tand -> 3
  | Tor -> 2
  | Timplies -> 1
  | Tiff -> 1
167

168
let print_label = Pretty.print_label
169

170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
let rec print_term fmt t = print_lterm 0 fmt t

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

and print_tapp pri fs fmt tl =
  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
        | tl -> fprintf fmt (protect_on (pri > 4) "%a@ %a")
            print_ls fs (print_list space (print_lterm 5)) tl
        end

and print_tnode pri fmt t = match t.t_node with
187 188 189
  | Tvar v ->
      print_vs fmt v
  | Tconst c ->
190 191 192 193 194
      print_const fmt c
  | Tapp (fs, tl) when unambig_fs fs ->
      print_tapp pri fs fmt tl
  | Tapp (fs, tl) ->
      fprintf fmt (protect_on (pri > 0) "%a:%a")
195
        (print_tapp 0 fs) tl print_ty (t_type t)
196
  | Tif (f,t1,t2) ->
197
      fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
198
        print_term f print_term t1 print_term t2
199 200
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
201
      fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
202
        print_vs v (print_lterm 4) t1 print_term t2;
203
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
204
  | Tcase (t1,bl) ->
205
      fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
206
        print_term t1 (print_list newline print_tbranch) bl
207
  | Teps fb ->
208
      let v,f = t_open_bound fb in
209
      fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
210
        print_vsty v print_term f;
211
      forget_var v
212 213
  | Tquant (q,fq) ->
      let vl,tl,f = t_open_quant fq in
214
      fprintf fmt (protect_on (pri > 0) "%a %a%a.@ %a") print_quant q
215
        (print_list comma print_vsty) vl print_tl tl print_term f;
216
      List.iter forget_var vl
217
  | Tbinop (b,f1,f2) ->
218 219
      let p = prio_binop b in
      fprintf fmt (protect_on (pri > p) "%a %a@ %a")
220
        (print_lterm (p + 1)) f1 print_binop b (print_lterm p) f2
221
  | Tnot f ->
222 223 224 225 226
      fprintf fmt (protect_on (pri > 4) "not %a") (print_lterm 4) f
  | Ttrue ->
      fprintf fmt "true"
  | Tfalse ->
      fprintf fmt "false"
227 228

and print_tbranch fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
229 230 231
  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
232

233
and print_tl fmt tl =
234
  if tl = [] then () else fprintf fmt "@ [%a]"
235
    (print_list alt (print_list comma print_term)) tl
236 237 238

(** Declarations *)

239 240 241
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
242

243 244 245
let print_constr fmt cs =
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
    (print_list nothing print_ty_arg) cs.ls_args
246

247 248 249 250 251 252 253
let print_constr ty fmt cs =
  let ty_val = of_option cs.ls_value in
  let m = ty_match Mtv.empty ty_val ty in
  let tl = List.map (ty_inst m) cs.ls_args in
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
    (print_list nothing print_ty_arg) tl

254
let print_type_decl fst fmt (ts,def) = match def with
255 256
  | Tabstract -> begin match ts.ts_def with
      | None ->
257 258
          fprintf fmt "@[<hov 2>%s %a%a@]@\n@\n"
            (if fst then "type" else "with") print_ts ts
259
            (print_list nothing print_tv_arg) ts.ts_args
260
      | Some ty ->
261 262
          fprintf fmt "@[<hov 2>%s %a%a =@ %a@]@\n@\n"
            (if fst then "type" else "with") print_ts ts
263
            (print_list nothing print_tv_arg) ts.ts_args print_ty ty
264 265
      end
  | Talgebraic csl ->
266
      let ty = ty_app ts (List.map ty_var ts.ts_args) in
267 268 269
      fprintf fmt "@[<hov 2>%s %a%a =@\n@[<hov>%a@]@]@\n@\n"
        (if fst then "type" else "with") print_ts ts
        (print_list nothing print_tv_arg) ts.ts_args
270
        (print_list newline (print_constr ty)) csl
271

272
let print_type_decl first fmt d =
273
  if not (query_remove (fst d).ts_name) then
274
    (print_type_decl first fmt d; forget_tvs ())
275

276
let print_ls_type fmt = fprintf fmt " :@ %a" print_ty
277

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

280
let print_logic_decl fst fmt (ls,ld) = match ld with
281 282
  | Some ld ->
      let vl,e = open_ls_defn ld in
283
      fprintf fmt "@[<hov 2>%s %a%a%a =@ %a@]@\n@\n"
Andrei Paskevich's avatar
Andrei Paskevich committed
284
        (if fst then ls_kind ls else "with") print_ls ls
285
        (print_list nothing print_vs_arg) vl
286
        (print_option print_ls_type) ls.ls_value print_term e;
287 288
      List.iter forget_var vl
  | None ->
289
      fprintf fmt "@[<hov 2>%s %a%a%a@]@\n@\n"
Andrei Paskevich's avatar
Andrei Paskevich committed
290
        (if fst then ls_kind ls else "with") print_ls ls
291
        (print_list nothing print_ty_arg) ls.ls_args
292
        (print_option print_ls_type) ls.ls_value
293

294
let print_logic_decl first fmt d =
295
  if not (query_remove (fst d).ls_name) then
296
    (print_logic_decl first fmt d; forget_tvs ())
297

298
let print_ind fmt (pr,f) =
299
  fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr print_term f
300

301 302 303 304
let print_ind_decl fst fmt (ps,bl) =
  fprintf fmt "@[<hov 2>%s %a%a =@ @[<hov>%a@]@]@\n@\n"
    (if fst then "inductive" else "with") print_ls ps
    (print_list nothing print_ty_arg) ps.ls_args
305
    (print_list newline print_ind) bl
306

307
let print_ind_decl first fmt d =
308
  if not (query_remove (fst d).ls_name) then
309
    (print_ind_decl first fmt d; forget_tvs ())
310

311
let print_pkind = Pretty.print_pkind
312

313
let print_prop_decl fmt (k,pr,f) =
314
  fprintf fmt "@[<hov 2>%a %a : %a@]@\n@\n" print_pkind k
315
    print_pr pr print_term f
316

317 318 319
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 ()
320

321 322 323 324 325 326
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

327
let print_decl fmt d = match d.d_node with
328 329 330
  | Dtype tl  -> print_list_next nothing print_type_decl fmt tl
  | Dlogic ll -> print_list_next nothing print_logic_decl fmt ll
  | Dind il   -> print_list_next nothing print_ind_decl fmt il
331
  | Dprop p   -> print_prop_decl fmt p
332

333 334 335 336
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) =
Andrei Paskevich's avatar
Andrei Paskevich committed
337
  fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
338 339 340

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

let print_meta_arg fmt = function
343
  | MAty ty -> fprintf fmt "type %a" print_ty ty
344
  | MAts ts -> fprintf fmt "type %a" print_ts ts
Andrei Paskevich's avatar
Andrei Paskevich committed
345
  | MAls ls -> fprintf fmt "%s %a" (ls_kind ls) print_ls ls
346 347 348
  | MApr pr -> fprintf fmt "prop %a" print_pr pr
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
349

350 351 352
let print_tdecl fmt td = match td.td_node with
  | Decl d ->
      print_decl fmt d
353
  | Use th ->
354
      fprintf fmt "@[<hov 2>(* use %a *)@]@\n@\n" print_th th
355
  | Clone (th,sm) when is_empty_sm sm ->
356
      fprintf fmt "@[<hov 2>(* use %a *)@]@\n@\n" print_th th
357 358 359 360
  | Clone (th,sm) ->
      let tm = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ts [] in
      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
361
      fprintf fmt "@[<hov 2>(* clone %a with %a,@ %a,@ %a *)@]@\n@\n"
362 363 364
        print_th th (print_list comma print_inst_ts) tm
                    (print_list comma print_inst_ls) lm
                    (print_list comma print_inst_pr) pm
365
  | Meta (m,al) ->
366
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
367
        m.meta_name (print_list comma print_meta_arg) al
368

MARCHE Claude's avatar
MARCHE Claude committed
369
let print_task _env pr thpr ?old:_ fmt task =
370 371 372
  forget_all ();
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
Andrei Paskevich's avatar
Andrei Paskevich committed
373 374 375
  info := {
    info_syn = get_syntax_map task;
    info_rem = get_remove_set task };
376
  fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
377
    (print_list nothing print_tdecl) (Task.task_tdecls task)
378

379
let () = register_printer "why3" print_task
380