why3.ml 12.2 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

20 21 22 23 24 25
open Format
open Pp
open Util
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
26
open Decl
27 28
open Driver

29
let iprinter,tprinter,lprinter,pprinter =
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
  let bl = ["theory"; "type"; "logic"; "inductive";
            "axiom"; "lemma"; "goal"; "use"; "clone";
            "namespace"; "import"; "export"; "end";
            "forall"; "exists"; "and"; "or"; "not";
            "true"; "false"; "if"; "then"; "else";
            "let"; "in"; "match"; "with"; "as"; "epsilon" ]
  in
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
  let usanitize = sanitizer char_to_ualpha char_to_alnumus in
  create_ident_printer bl ~sanitizer:isanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
  create_ident_printer bl ~sanitizer:lsanitize,
  create_ident_printer bl ~sanitizer:usanitize

let forget_all () =
  forget_all iprinter;
  forget_all tprinter;
  forget_all lprinter;
Andrei Paskevich's avatar
Andrei Paskevich committed
49
  forget_all pprinter
50 51 52 53 54

let tv_set = ref Sid.empty

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

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 =
65 66
  let sanitizer = String.uncapitalize in
  fprintf fmt "%s" (id_unique iprinter ~sanitizer vs.vs_name)
67 68 69 70 71 72 73

let forget_var vs = forget_id iprinter vs.vs_name

let print_ts fmt ts =
  fprintf fmt "%s" (id_unique tprinter ts.ts_name)

let print_ls fmt ls =
74 75 76 77 78
  fprintf fmt "%s" (id_unique lprinter ls.ls_name)

let print_cs fmt ls =
  let sanitizer = String.capitalize in
  fprintf fmt "%s" (id_unique lprinter ~sanitizer ls.ls_name)
79 80

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

(** Types *)

let rec ns_comma fmt () = fprintf fmt ",@,"

87
let rec print_ty drv fmt ty = match ty.ty_node with
88
  | Tyvar v -> print_tv fmt v
89
  | Tyapp (ts, tl) ->
90
    begin match drv ts.ts_name with
91 92 93 94 95 96 97 98 99
      | Syntax s -> syntax_arguments s (print_ty drv) fmt tl
      | _ ->
        begin match tl with
          | []  -> print_ts fmt ts
          | [t] -> fprintf fmt "%a@ %a" (print_ty drv) t print_ts ts
          | l   -> fprintf fmt "(%a)@ %a"
                     (print_list ns_comma (print_ty drv)) l print_ts ts
        end
    end
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 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
    | Tyvar u when u == v -> true
    | _ -> 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
  inspect (of_option fs.ls_value)

(** Patterns, terms, and formulas *)

let lparen_l fmt () = fprintf fmt "@ ("
let lparen_r fmt () = fprintf fmt "(@,"
let print_paren_l fmt x = print_list_delim lparen_l rparen comma fmt x
let print_paren_r fmt x = print_list_delim lparen_r rparen comma fmt x

121
let rec print_pat drv fmt p = match p.pat_node with
122 123
  | Pwild -> fprintf fmt "_"
  | Pvar v -> print_vs fmt v
124
  | Pas (p,v) -> fprintf fmt "%a as %a" (print_pat drv) p print_vs v
125
  | Papp (cs,pl) ->
126
    begin match drv cs.ls_name with
127 128
      | Syntax s -> syntax_arguments s (print_pat drv) fmt pl
      | _ -> fprintf fmt "%a%a"
129
          print_cs cs (print_paren_r (print_pat drv)) pl
130
    end
131

132 133
let print_vsty drv fmt v =
  fprintf fmt "%a:@,%a" print_vs v (print_ty drv) v.vs_ty
134 135 136 137 138 139 140 141 142 143 144 145 146 147 148

let print_quant fmt = function
  | Fforall -> fprintf fmt "forall"
  | Fexists -> fprintf fmt "exists"

let print_binop fmt = function
  | Fand -> fprintf fmt "and"
  | For -> fprintf fmt "or"
  | Fimplies -> fprintf fmt "->"
  | Fiff -> fprintf fmt "<->"

let print_label fmt l = fprintf fmt "\"%s\"" l

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

149 150 151 152 153 154
let rec print_term drv fmt t = print_lrterm false false drv fmt t
and     print_fmla drv fmt f = print_lrfmla false false drv fmt f
and print_opl_term drv fmt t = print_lrterm true  false drv fmt t
and print_opl_fmla drv fmt f = print_lrfmla true  false drv fmt f
and print_opr_term drv fmt t = print_lrterm false true  drv fmt t
and print_opr_fmla drv fmt f = print_lrfmla false true  drv fmt f
155

156 157
and print_lrterm opl opr drv fmt t = match t.t_label with
  | [] -> print_tnode opl opr drv fmt t
158
  | ll -> fprintf fmt "(%a %a)"
159
      (print_list space print_label) ll (print_tnode false false drv) t
160

161 162
and print_lrfmla opl opr drv fmt f = match f.f_label with
  | [] -> print_fnode opl opr drv fmt f
163
  | ll -> fprintf fmt "(%a %a)"
164
      (print_list space print_label) ll (print_fnode false false drv) f
165

166
and print_tnode opl opr drv fmt t = match t.t_node with
167 168 169 170 171
  | Tbvar _ ->
      assert false
  | Tvar v ->
      print_vs fmt v
  | Tconst c ->
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
172
      Pretty.print_const fmt c
173 174 175
  | Tif (f,t1,t2) ->
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
        (print_fmla drv) f (print_term drv) t1 (print_opl_term drv) t2
176 177 178
  | Tlet (t1,tb) ->
      let v,t2 = t_open_bound tb in
      fprintf fmt (protect_on opr "let %a =@ %a in@ %a")
179
        print_vs v (print_opl_term drv) t1 (print_opl_term drv) t2;
180
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
181
  | Tcase (tl,bl) ->
182
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
Andrei Paskevich's avatar
Andrei Paskevich committed
183 184
        (print_list comma (print_term drv)) tl
        (print_list newline (print_tbranch drv)) bl
185 186
  | Teps fb ->
      let v,f = f_open_bound fb in
Andrei Paskevich's avatar
Andrei Paskevich committed
187
      fprintf fmt (protect_on opr "epsilon %a.@ %a")
188
        (print_vsty drv) v (print_opl_fmla drv) f;
189
      forget_var v
190
  | Tapp (fs, tl) ->
191
    begin match drv fs.ls_name with
192 193 194 195 196 197 198
      | Syntax s -> syntax_arguments s (print_term drv) fmt tl
      | _ -> if unambig_fs fs
          then fprintf fmt "%a%a" print_ls fs
            (print_paren_r (print_term drv)) tl
          else fprintf fmt (protect_on opl "%a%a:%a") print_ls fs
            (print_paren_r (print_term drv)) tl (print_ty drv) t.t_ty
    end
199

200
and print_fnode opl opr drv fmt f = match f.f_node with
201 202 203
  | Fquant (q,fq) ->
      let vl,tl,f = f_open_quant fq in
      fprintf fmt (protect_on opr "%a %a%a.@ %a") print_quant q
204 205
        (print_list comma (print_vsty drv)) vl
        (print_tl drv) tl (print_fmla drv) f;
206 207 208 209 210 211 212
      List.iter forget_var vl
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fbinop (b,f1,f2) ->
      fprintf fmt (protect_on (opl || opr) "%a %a@ %a")
213
        (print_opr_fmla drv) f1 print_binop b (print_opl_fmla drv) f2
214
  | Fnot f ->
215
      fprintf fmt (protect_on opr "not %a") (print_opl_fmla drv) f
216 217 218
  | Fif (f1,f2,f3) ->
      fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
        (print_fmla drv) f1 (print_fmla drv) f2 (print_opl_fmla drv) f3
219 220 221
  | Flet (t,f) ->
      let v,f = f_open_bound f in
      fprintf fmt (protect_on opr "let %a =@ %a in@ %a")
222
        print_vs v (print_opl_term drv) t (print_opl_fmla drv) f;
223
      forget_var v
Andrei Paskevich's avatar
Andrei Paskevich committed
224 225 226
  | Fcase (tl,bl) ->
      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
        (print_list comma (print_term drv)) tl
227
        (print_list newline (print_fbranch drv)) bl
228
  | Fapp (ps, tl) ->
229
    begin match drv ps.ls_name with
230 231 232 233
      | Syntax s -> syntax_arguments s (print_term drv) fmt tl
      | _ -> fprintf fmt "%a%a" print_ls ps
            (print_paren_r (print_term drv)) tl
    end
234

235
and print_tbranch drv fmt br =
236
  let pl,t = t_open_branch br in
Andrei Paskevich's avatar
Andrei Paskevich committed
237 238
  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
    (print_list comma (print_pat drv)) pl (print_term drv) t;
239
  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
240

241
and print_fbranch drv fmt br =
242
  let pl,f = f_open_branch br in
Andrei Paskevich's avatar
Andrei Paskevich committed
243 244
  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
    (print_list comma (print_pat drv)) pl (print_fmla drv) f;
245
  Svs.iter forget_var (List.fold_left pat_freevars Svs.empty pl)
246

247
and print_tl drv fmt tl =
248
  if tl = [] then () else fprintf fmt "@ [%a]"
249
    (print_list alt (print_list comma (print_expr drv))) tl
250

251
and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
252 253 254

(** Declarations *)

255
let print_constr drv fmt cs =
256
  fprintf fmt "@[<hov 4>| %a%a@]" print_cs cs
257
    (print_paren_l (print_ty drv)) cs.ls_args
258 259 260 261 262 263

let print_ty_args fmt = function
  | [] -> ()
  | [tv] -> fprintf fmt " %a" print_tv tv
  | l -> fprintf fmt " (%a)" (print_list ns_comma print_tv) l

264
let print_type_decl drv fmt (ts,def) = match def with
265 266
  | Tabstract -> begin match ts.ts_def with
      | None ->
267
          fprintf fmt "@[<hov 2>type%a %a@]@\n@\n"
268 269
            print_ty_args ts.ts_args print_ts ts
      | Some ty ->
270
          fprintf fmt "@[<hov 2>type%a %a =@ %a@]@\n@\n"
271
            print_ty_args ts.ts_args print_ts ts (print_ty drv) ty
272 273
      end
  | Talgebraic csl ->
274
      fprintf fmt "@[<hov 2>type%a %a =@\n@[<hov>%a@]@]@\n@\n"
275
        print_ty_args ts.ts_args print_ts ts
276
        (print_list newline (print_constr drv)) csl
277

278
let print_type_decl drv fmt d =
279
  match drv (fst d).ts_name with
280 281
    | Syntax _ -> ()
    | _ -> print_type_decl drv fmt d; forget_tvs ()
282

283
let print_ls_type drv fmt = fprintf fmt " :@ %a" (print_ty drv)
284

285 286 287 288 289 290 291 292 293 294 295 296
let print_logic_decl drv fmt (ls,ld) = match ld with
  | Some ld ->
      let vl,e = open_ls_defn ld in
      fprintf fmt "@[<hov 2>logic %a%a%a =@ %a@]@\n@\n"
        print_ls ls (print_paren_l (print_vsty drv)) vl
        (print_option (print_ls_type drv)) ls.ls_value
        (print_expr drv) e;
      List.iter forget_var vl
  | None ->
      fprintf fmt "@[<hov 2>logic %a%a%a@]@\n@\n"
        print_ls ls (print_paren_l (print_ty drv)) ls.ls_args
        (print_option (print_ls_type drv)) ls.ls_value
297 298

let print_logic_decl drv fmt d =
299
  match drv (fst d).ls_name with
300 301
    | Syntax _ -> ()
    | _ -> print_logic_decl drv fmt d; forget_tvs ()
302

303 304
let print_ind drv fmt (pr,f) =
  fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr (print_fmla drv) f
305

306
let print_ind_decl drv fmt (ps,bl) =
307
  fprintf fmt "@[<hov 2>inductive %a%a =@ @[<hov>%a@]@]@\n@\n"
308
     print_ls ps (print_paren_l (print_ty drv)) ps.ls_args
309 310 311
     (print_list newline (print_ind drv)) bl

let print_ind_decl drv fmt d =
312
  match drv (fst d).ls_name with
313 314
    | Syntax _ -> ()
    | _ -> print_ind_decl drv fmt d; forget_tvs ()
315 316 317 318 319 320

let print_pkind fmt = function
  | Paxiom -> fprintf fmt "axiom"
  | Plemma -> fprintf fmt "lemma"
  | Pgoal  -> fprintf fmt "goal"

321
let print_prop_decl drv fmt (k,pr,f) =
322 323 324 325
  fprintf fmt "@[<hov 2>%a %a : %a@]@\n@\n" print_pkind k
    print_pr pr (print_fmla drv) f

let print_prop_decl drv fmt (k,pr,f) =
326
  match k, drv pr.pr_name with
327 328
    | Paxiom, Remove -> ()
    | _ -> print_prop_decl drv fmt (k,pr,f); forget_tvs ()
329

330
let print_decl drv fmt d = match d.d_node with
331 332 333
  | Dtype tl  -> print_list nothing (print_type_decl drv) fmt tl
  | Dlogic ll -> print_list nothing (print_logic_decl drv) fmt ll
  | Dind il   -> print_list nothing (print_ind_decl drv) fmt il
334
  | Dprop p -> print_prop_decl drv fmt p
335

336
let print_decls drv fmt dl =
337
  fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl drv)) dl
338

Andrei Paskevich's avatar
Andrei Paskevich committed
339 340
let print_context drv fmt task =
  forget_all (); print_decls drv fmt (Task.task_decls task)
341 342

let () = register_printer "why3" print_context
343