why3printer.ml 16.4 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   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
open Args_wrapper
Sylvain Dailler's avatar
Sylvain Dailler committed
24

25 26 27 28 29 30 31
(* Labels and locations can be printed by setting the appropriate flags *)
let debug_print_labels = Debug.register_info_flag "print_labels"
  ~desc:"Print@ labels@ of@ identifiers@ and@ expressions."

let debug_print_locs = Debug.register_info_flag "print_locs"
  ~desc:"Print@ locations@ of@ identifiers@ and@ expressions."

32
let id_unique tables id = id_unique tables.printer id
Sylvain Dailler's avatar
Sylvain Dailler committed
33 34

(*
35 36 37
let forget_tvs () =
  forget_all aprinter

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

(* type variables always start with a quote *)
Sylvain Dailler's avatar
Sylvain Dailler committed
46 47
let print_tv tables fmt tv =
  fprintf fmt "'%s" (id_unique tables tv.tv_name)
48 49

(* logic variables always start with a lower case letter *)
Sylvain Dailler's avatar
Sylvain Dailler committed
50 51
let print_vs tables fmt vs =
  fprintf fmt "%s" (id_unique tables vs.vs_name)
52

Sylvain Dailler's avatar
Sylvain Dailler committed
53
(*
54
let forget_var vs = forget_id iprinter vs.vs_name
Sylvain Dailler's avatar
Sylvain Dailler committed
55
*)
56

57
(* theory names always start with an upper case letter *)
Sylvain Dailler's avatar
Sylvain Dailler committed
58 59
let print_th tables fmt th =
  fprintf fmt "%s" (id_unique tables th.th_name)
60

Sylvain Dailler's avatar
Sylvain Dailler committed
61 62
let print_ts tables fmt ts =
  fprintf fmt "%s" (id_unique tables ts.ts_name)
63

Sylvain Dailler's avatar
Sylvain Dailler committed
64 65
let print_ls tables fmt ls =
  fprintf fmt "%s" (id_unique tables ls.ls_name)
66

Sylvain Dailler's avatar
Sylvain Dailler committed
67 68
let print_cs tables fmt ls =
  fprintf fmt "%s" (id_unique tables ls.ls_name)
69

Sylvain Dailler's avatar
Sylvain Dailler committed
70 71
let print_pr tables fmt pr =
  fprintf fmt "%s" (id_unique tables pr.pr_name)
72

73 74
(* info *)

75
type info = { info_syn : syntax_map ; itp : bool; }
76

77
let info = ref { info_syn = Mid.empty ; itp = false ; }
78 79

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

82 83
(** Types *)

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

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

97
let print_ty = print_ty_node false
98

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

(** Patterns, terms, and formulas *)

Sylvain Dailler's avatar
Sylvain Dailler committed
114
let rec print_pat_node pri tables fmt p = match p.pat_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
115 116 117
  | Pwild ->
      fprintf fmt "_"
  | Pvar v ->
Sylvain Dailler's avatar
Sylvain Dailler committed
118
      print_vs tables fmt v
Andrei Paskevich's avatar
Andrei Paskevich committed
119 120
  | Pas (p, v) ->
      fprintf fmt (protect_on (pri > 1) "%a as %a")
Sylvain Dailler's avatar
Sylvain Dailler committed
121
        (print_pat_node 1 tables) p (print_vs tables) v
Andrei Paskevich's avatar
Andrei Paskevich committed
122 123
  | Por (p, q) ->
      fprintf fmt (protect_on (pri > 0) "%a | %a")
Sylvain Dailler's avatar
Sylvain Dailler committed
124
        (print_pat_node 0 tables) p (print_pat_node 0 tables) q
Andrei Paskevich's avatar
Andrei Paskevich committed
125
  | Papp (cs, pl) -> begin match query_syntax cs.ls_name with
Sylvain Dailler's avatar
Sylvain Dailler committed
126
      | Some s -> syntax_arguments s (print_pat_node 0 tables) fmt pl
127
      | None -> begin match pl with
Sylvain Dailler's avatar
Sylvain Dailler committed
128
          | [] -> print_cs tables fmt cs
Andrei Paskevich's avatar
Andrei Paskevich committed
129
          | pl -> fprintf fmt (protect_on (pri > 1) "%a@ %a")
Sylvain Dailler's avatar
Sylvain Dailler committed
130
              (print_cs tables) cs (print_list space (print_pat_node 2 tables)) pl
131 132
          end
      end
133

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

Sylvain Dailler's avatar
Sylvain Dailler committed
136 137
let print_vsty tables fmt v =
  fprintf fmt "%a:@,%a" (print_vs tables) v (print_ty tables) v.vs_ty
138

139 140 141
let print_const = Pretty.print_const
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

149
let print_label = Pretty.print_label
150
let print_labels = print_iter1 Slab.iter space print_label
151

152
let print_ident_labels fmt id =
153 154 155 156 157 158 159 160
  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
    Opt.iter (fprintf fmt "@ %a" Pretty.print_loc) id.id_loc

(*  if not (Slab.is_empty id.id_label) then
    fprintf fmt "@ %a" print_labels id.id_label*)
161

Sylvain Dailler's avatar
Sylvain Dailler committed
162
let rec print_term tables fmt t = print_lterm 0 tables fmt t
163

Sylvain Dailler's avatar
Sylvain Dailler committed
164
and print_lterm pri tables fmt t =
165 166
  if (Slab.is_empty t.t_label || not (Debug.test_flag debug_print_labels)) then
    print_tnode pri tables fmt t
167
  else fprintf fmt (protect_on (pri > 0) "%a %a")
Sylvain Dailler's avatar
Sylvain Dailler committed
168
      print_labels t.t_label (print_tnode 0 tables) t
169

Sylvain Dailler's avatar
Sylvain Dailler committed
170
and print_app pri fs tables fmt tl =
171
  match query_syntax fs.ls_name with
Sylvain Dailler's avatar
Sylvain Dailler committed
172
    | Some s -> syntax_arguments s (print_term tables) fmt tl
173
    | None -> begin match tl with
Sylvain Dailler's avatar
Sylvain Dailler committed
174
        | [] -> print_ls tables fmt fs
175
        | tl -> fprintf fmt (protect_on (pri > 5) "%a@ %a")
Sylvain Dailler's avatar
Sylvain Dailler committed
176
            (print_ls tables) fs (print_list space (print_lterm 6 tables)) tl
177 178
        end

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

Sylvain Dailler's avatar
Sylvain Dailler committed
225
and print_tbranch tables fmt br =
Andrei Paskevich's avatar
Andrei Paskevich committed
226
  let p,t = t_open_branch br in
Sylvain Dailler's avatar
Sylvain Dailler committed
227
  fprintf fmt "@[<hov 4>| %a ->@ %a@]" (print_pat tables) p (print_term tables) t
228

Sylvain Dailler's avatar
Sylvain Dailler committed
229
and print_tl tables fmt tl =
230
  if tl = [] then () else fprintf fmt "@ [%a]"
Sylvain Dailler's avatar
Sylvain Dailler committed
231
    (print_list alt (print_list comma (print_term tables))) tl
232 233 234

(** Declarations *)

Sylvain Dailler's avatar
Sylvain Dailler committed
235 236 237
let print_tv_arg tables fmt tv = fprintf fmt "@ %a" (print_tv tables) tv
let print_ty_arg tables fmt ty = fprintf fmt "@ %a" (print_ty_node true tables) ty
let print_vs_arg tables fmt vs = fprintf fmt "@ (%a)" (print_vsty tables) vs
238

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

Sylvain Dailler's avatar
Sylvain Dailler committed
250
let print_type_decl tables fmt ts = match ts.ts_def with
251
  | None ->
252
      fprintf fmt "@[<hov 2>type %a%a%a@]@\n"
Sylvain Dailler's avatar
Sylvain Dailler committed
253 254
        (print_ts tables) ts print_ident_labels ts.ts_name
        (print_list nothing (print_tv_arg tables)) ts.ts_args
255
  | Some ty ->
256
      fprintf fmt "@[<hov 2>type %a%a%a =@ %a@]@\n"
Sylvain Dailler's avatar
Sylvain Dailler committed
257 258
        (print_ts tables) ts print_ident_labels ts.ts_name
        (print_list nothing (print_tv_arg tables)) ts.ts_args (print_ty tables) ty
259

Sylvain Dailler's avatar
Sylvain Dailler committed
260
let print_type_decl tables fmt ts =
261
  if not (query_remove ts.ts_name) then
Sylvain Dailler's avatar
Sylvain Dailler committed
262
    (print_type_decl tables fmt ts)
263

Sylvain Dailler's avatar
Sylvain Dailler committed
264
let print_data_decl fst tables fmt (ts,csl) =
265
  fprintf fmt "@[<hov 2>%s %a%a%a =@\n@[<hov>%a@]@]@\n"
Sylvain Dailler's avatar
Sylvain Dailler committed
266
    (if fst then "type" else "with") (print_ts tables) ts
267
    print_ident_labels ts.ts_name
Sylvain Dailler's avatar
Sylvain Dailler committed
268 269
    (print_list nothing (print_tv_arg tables)) ts.ts_args
    (print_list newline (print_constr tables)) csl
270

Sylvain Dailler's avatar
Sylvain Dailler committed
271
let print_data_decl first tables fmt d =
272
  if not (query_remove (fst d).ts_name) then
Sylvain Dailler's avatar
Sylvain Dailler committed
273
    (print_data_decl first tables fmt d)
274

Sylvain Dailler's avatar
Sylvain Dailler committed
275
let print_ls_type tables fmt = fprintf fmt " :@ %a" (print_ty tables)
276

277 278 279 280 281 282
let print_ls_kind ~fst fmt ls =
  if not !info.itp then
    fprintf fmt "%s "
            (if fst then
               if ls.ls_value = None then "predicate" else "function"
             else "with")
Andrei Paskevich's avatar
Andrei Paskevich committed
283

Sylvain Dailler's avatar
Sylvain Dailler committed
284
let print_param_decl tables fmt ls =
285
  fprintf fmt "@[<hov 2>%a%a%a%a%a@]@\n"
Sylvain Dailler's avatar
Sylvain Dailler committed
286
    (print_ls_kind ~fst:true) ls (print_ls tables) ls
287
    print_ident_labels ls.ls_name
Sylvain Dailler's avatar
Sylvain Dailler committed
288 289
    (print_list nothing (print_ty_arg tables)) ls.ls_args
    (print_option (print_ls_type tables)) ls.ls_value
290

Sylvain Dailler's avatar
Sylvain Dailler committed
291
let print_param_decl tables fmt ls =
292
  if not (query_remove ls.ls_name) then
Sylvain Dailler's avatar
Sylvain Dailler committed
293
    (print_param_decl tables fmt ls)
294

Sylvain Dailler's avatar
Sylvain Dailler committed
295
let print_logic_decl fst tables fmt (ls,ld) =
296
  let vl,e = open_ls_defn ld in
297
  fprintf fmt "@[<hov 2>%a%a%a%a%a =@ %a@]@\n"
Sylvain Dailler's avatar
Sylvain Dailler committed
298
    (print_ls_kind ~fst) ls (print_ls tables) ls
299
    print_ident_labels ls.ls_name
Sylvain Dailler's avatar
Sylvain Dailler committed
300 301
    (print_list nothing (print_vs_arg tables)) vl
    (print_option (print_ls_type tables)) ls.ls_value (print_term tables) e
302

Sylvain Dailler's avatar
Sylvain Dailler committed
303
let print_logic_decl first tables fmt d =
304
  if not (query_remove (fst d).ls_name) then
Sylvain Dailler's avatar
Sylvain Dailler committed
305
    (print_logic_decl first tables fmt d)
306

Sylvain Dailler's avatar
Sylvain Dailler committed
307
let print_ind tables fmt (pr,f) =
308
  fprintf fmt "@[<hov 4>| %a%a :@ %a@]"
Sylvain Dailler's avatar
Sylvain Dailler committed
309
    (print_pr tables) pr print_ident_labels pr.pr_name (print_term tables) f
310

311 312 313 314
let ind_sign = function
  | Ind   -> "inductive"
  | Coind -> "coinductive"

Sylvain Dailler's avatar
Sylvain Dailler committed
315
let print_ind_decl s fst tables fmt (ps,bl) =
316
  fprintf fmt "@[<hov 2>%s %a%a%a =@ @[<hov>%a@]@]@\n"
Sylvain Dailler's avatar
Sylvain Dailler committed
317
    (if fst then ind_sign s else "with") (print_ls tables) ps
318
    print_ident_labels ps.ls_name
Sylvain Dailler's avatar
Sylvain Dailler committed
319 320
    (print_list nothing (print_ty_arg tables)) ps.ls_args
    (print_list newline (print_ind tables)) bl
321

Sylvain Dailler's avatar
Sylvain Dailler committed
322
let print_ind_decl s first tables fmt d =
323
  if not (query_remove (fst d).ls_name) then
Sylvain Dailler's avatar
Sylvain Dailler committed
324
    (print_ind_decl s first tables fmt d)
325

326 327
let print_pkind fmt k =
  if not !info.itp then fprintf fmt "%a " Pretty.print_pkind k
328

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

Sylvain Dailler's avatar
Sylvain Dailler committed
333
let print_prop_decl tables fmt (k,pr,f) = match k with
334
  | Paxiom when query_remove pr.pr_name -> ()
Sylvain Dailler's avatar
Sylvain Dailler committed
335
  | _ -> print_prop_decl tables fmt (k,pr,f)
336

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

Sylvain Dailler's avatar
Sylvain Dailler committed
343 344 345 346 347 348 349
let print_decl tables fmt d = match d.d_node with
  | Dtype ts  -> print_type_decl tables fmt ts
  | Ddata tl  -> print_list_next nothing (fun f -> print_data_decl f tables) fmt tl
  | Dparam ls -> print_param_decl tables fmt ls
  | Dlogic ll -> print_list_next nothing (fun f -> print_logic_decl f tables) fmt ll
  | Dind (s, il) -> print_list_next nothing (fun u -> print_ind_decl s u tables) fmt il
  | Dprop p   -> print_prop_decl tables fmt p
350

Sylvain Dailler's avatar
Sylvain Dailler committed
351 352
let print_inst_ts tables fmt (ts1,ts2) =
  fprintf fmt "type %a = %a" (print_ts tables) ts1 (print_ts tables) ts2
353

Sylvain Dailler's avatar
Sylvain Dailler committed
354
let print_inst_ls tables fmt (ls1,ls2) =
355
  fprintf fmt "%a%a = %a"
Sylvain Dailler's avatar
Sylvain Dailler committed
356
          (print_ls_kind ~fst:true) ls1 (print_ls tables) ls1 (print_ls tables) ls2
357

Sylvain Dailler's avatar
Sylvain Dailler committed
358 359
let print_inst_pr tables fmt (pr1,pr2) =
  fprintf fmt "prop %a = %a" (print_pr tables) pr1 (print_pr tables) pr2
360

Sylvain Dailler's avatar
Sylvain Dailler committed
361 362 363 364 365
let print_meta_arg tables fmt = function
  | MAty ty -> fprintf fmt "type %a" (print_ty tables) ty
  | MAts ts -> fprintf fmt "type %a" (print_ts tables) ts
  | MAls ls -> fprintf fmt "%a%a" (print_ls_kind ~fst:true) ls (print_ls tables) ls
  | MApr pr -> fprintf fmt "prop %a" (print_pr tables) pr
366 367
  | MAstr s -> fprintf fmt "\"%s\"" s
  | MAint i -> fprintf fmt "%d" i
368

Sylvain Dailler's avatar
Sylvain Dailler committed
369 370
let print_qt tables fmt th =
  if th.th_path = [] then print_th tables fmt th else
371 372
  fprintf fmt "%a.%a"
    (print_list (constant_string ".") string) th.th_path
Sylvain Dailler's avatar
Sylvain Dailler committed
373
    (print_th tables) th
374

Sylvain Dailler's avatar
Sylvain Dailler committed
375
let print_tdecl tables fmt td = match td.td_node with
376
  | Decl d ->
Sylvain Dailler's avatar
Sylvain Dailler committed
377
      fprintf fmt "%a@\n" (print_decl tables) d
378
  | Use th ->
Sylvain Dailler's avatar
Sylvain Dailler committed
379
      fprintf fmt "@[<hov 2>(* use %a *)@]@\n@\n" (print_qt tables) th
380
  | Clone (th,sm) when is_empty_sm sm ->
Sylvain Dailler's avatar
Sylvain Dailler committed
381
      fprintf fmt "@[<hov 2>(* use %a *)@]@\n@\n" (print_qt tables) th
382 383 384 385
  | 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
386
      fprintf fmt "@[<hov 2>(* clone %a with %a,@ %a,@ %a *)@]@\n@\n"
Sylvain Dailler's avatar
Sylvain Dailler committed
387 388 389
        (print_qt tables) th (print_list comma (print_inst_ts tables)) tm
                    (print_list comma (print_inst_ls tables)) lm
                    (print_list comma (print_inst_pr tables)) pm
390
  | Meta (m,al) ->
391
      fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
Sylvain Dailler's avatar
Sylvain Dailler committed
392
        m.meta_name (print_list comma (print_meta_arg tables)) al
393

Sylvain Dailler's avatar
Sylvain Dailler committed
394 395 396 397 398 399
let print_tdecls tables =
  let print_tdecl sm tables fmt td =
    info := {info_syn = sm; itp = false}; print_tdecl tables fmt td; sm, [] in
  let print_tdecl tables = Printer.sprint_tdecl (fun sm -> print_tdecl sm tables) in
  let print_tdecl tables task acc = print_tdecl tables task.Task.task_decl acc in
  Discriminate.on_syntax_map (fun sm -> Trans.fold (print_tdecl tables) (sm,[]))
400

Sylvain Dailler's avatar
Sylvain Dailler committed
401 402
(* TODO print_task and print_sequent recompute a table every time they are called.
    Do we want that? *)
403
let print_task args ?old:_ fmt task =
404 405
  (* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
  (* forget_all (); *)
Sylvain Dailler's avatar
Sylvain Dailler committed
406
  let tables = build_name_tables task in
407
  print_prelude fmt args.prelude;
408
  fprintf fmt "theory Task@\n";
409
  print_th_prelude task fmt args.th_prelude;
410 411 412
  let rec print = function
    | x :: r -> print r; Pp.string fmt x
    | [] -> () in
Sylvain Dailler's avatar
Sylvain Dailler committed
413
  print (snd (Trans.apply (print_tdecls tables) task));
414
  fprintf fmt "end@."
415

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

419
let print_sequent _args ?old:_ fmt =
420 421 422 423 424 425
  Trans.apply
    (Printer.on_syntax_map
       (fun sm ->
        info := {info_syn = sm; itp = true};
        Trans.store
          (fun task ->
426 427 428
(*
          let task = Trans.apply (Trans.goal Introduction.intros) task in
*)
429
           (* print_th_prelude task fmt args.th_prelude; *)
Sylvain Dailler's avatar
Sylvain Dailler committed
430
           let tables = build_name_tables task in
431 432
           let ut = Task.used_symbols (Task.used_theories task) in
           let ld = Task.local_decls task ut in
MARCHE Claude's avatar
MARCHE Claude committed
433
           fprintf fmt "@[<v 0>%a@]"
Sylvain Dailler's avatar
Sylvain Dailler committed
434
                   (Pp.print_list Pp.newline (print_decl tables)) ld)))
435 436 437 438


let () = register_printer "why3_itp" print_sequent
  ~desc:"Print@ the@ goal@ in@ a@ format@ dedicated@ to@ ITP."
439 440 441 442 443


(** *)


Sylvain Dailler's avatar
Sylvain Dailler committed
444
(*
445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464
let build_name_tables task : name_tables =
(*
  TODO:
   - simply use [km = Task.task_known task] as the set of identifiers
     to insert in the tables
   - only one printer (do not attempt te rebuild qualified idents)
   - use syntax_map from why3_itp driver
   - to build the namespace, do a match on the decl associated with the id
      in [km]
  | Dtype  -> tysymbol
  | Ddata | Dparam | Dlogic | Dind  -> lsymbol
  | Dprop  -> prsymbol

  TODO: use the result of this function in
    - a new variant of a printer in this file
    - use the namespace to type the terms
      (change the code in parser/typing.ml to use namespace
      instead of theory_uc)

*)
Sylvain Dailler's avatar
Sylvain Dailler committed
465
*)