alt_ergo.ml 13.9 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
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.                  *)
(*                                                                        *)
(**************************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
20

Francois Bobot's avatar
Francois Bobot committed
21 22
(** Alt-ergo printer *)

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

32
let meta_ac = Theory.register_meta "AC" [Theory.MTlsymbol]
33 34
let meta_printer_option =
  Theory.register_meta "printer_option" [Theory.MTstring]
35 36 37 38 39 40 41 42 43

type info = {
  info_syn : syntax_map;
  info_ac  : Sls.t;
  info_show_labels : bool;
  info_csm : lsymbol list Mls.t;
  info_pjs : Sls.t;
  info_axs : Spr.t;
}
44

45
let ident_printer =
46
  let bls = [
47
    "ac"; "and"; "array"; "as"; "axiom"; "bool"; "distinct"; "else"; "exists";
48 49 50
    "false"; "forall"; "function"; "goal"; "if"; "int"; "bitv";
    "logic"; "not"; "or"; "parameter"; "predicate";
    "prop"; "real"; "then"; "true"; "type"; "unit"; "void";
51
    "select"; "store";
52
  ]
53
  in
54
  let san = sanitizer char_to_alpha char_to_alnumus in
55
  create_ident_printer bls ~sanitizer:san
56 57

let print_ident fmt id =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
58
  fprintf fmt "%s" (id_unique ident_printer id)
59

60 61 62
let print_label fmt l =
  fprintf fmt "\"%s\"" l.lab_string

63 64
let print_ident_label info fmt id =
  if info.info_show_labels then
65 66 67 68 69 70
    fprintf fmt "%s %a"
      (id_unique ident_printer id)
      (print_list space print_label) (Slab.elements id.id_label)
  else
    print_ident fmt id

71 72
let forget_var v = forget_id ident_printer v.vs_name

73 74 75 76 77 78 79 80 81
let tv_printer =
  let san = sanitizer char_to_lalpha char_to_alnumus in
  create_ident_printer [] ~sanitizer:san

let print_tvsymbol fmt tv =
  fprintf fmt "'%s" (id_unique tv_printer tv.tv_name)

let forget_tvs () = forget_all tv_printer

82
let rec print_type info fmt ty = match ty.ty_node with
83
  | Tyvar id ->
84
      print_tvsymbol fmt id
85
  | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
86 87
      | Some s -> syntax_arguments s (print_type info) fmt tl
      | None -> fprintf fmt "%a%a" (print_tyapp info) tl print_ident ts.ts_name
88 89
    end

90
and print_tyapp info fmt = function
91
  | [] -> ()
92 93
  | [ty] -> fprintf fmt "%a " (print_type info) ty
  | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
94

95
let rec print_term info fmt t = match t.t_node with
96
  | Tconst c ->
97 98 99 100 101 102 103 104 105 106 107 108 109
      let number_format = {
          Print_number.long_int_support = true;
          Print_number.dec_int_support = Print_number.Number_default;
          Print_number.hex_int_support = Print_number.Number_unsupported;
          Print_number.oct_int_support = Print_number.Number_unsupported;
          Print_number.bin_int_support = Print_number.Number_unsupported;
          Print_number.def_int_support = Print_number.Number_unsupported;
          Print_number.dec_real_support = Print_number.Number_default;
          Print_number.hex_real_support = Print_number.Number_default;
          Print_number.frac_real_support = Print_number.Number_unsupported;
          Print_number.def_real_support = Print_number.Number_unsupported;
        } in
      Print_number.print number_format fmt c
110
  | Tvar { vs_name = id } ->
111
      print_ident fmt id
112
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
113
      | Some s -> syntax_arguments s (print_term info) fmt tl
114 115 116 117 118 119 120 121 122
      | None when Mls.mem ls info.info_csm ->
          let print_field fmt ({ls_name = id},t) =
            fprintf fmt "%a =@ %a" print_ident id (print_term info) t in
          fprintf fmt "{@ %a@ }" (print_list semi print_field)
            (List.combine (Mls.find ls info.info_csm) tl)
      | None when Sls.mem ls info.info_pjs ->
          fprintf fmt "%a.%a" (print_tapp info) tl print_ident ls.ls_name
      | None ->
          fprintf fmt "%a%a" print_ident ls.ls_name (print_tapp info) tl
123
    end
124
  | Tlet _ -> unsupportedTerm t
125
      "alt-ergo : you must eliminate let in term"
126
  | Tif _ -> unsupportedTerm t
127
      "alt-ergo : you must eliminate if_then_else"
128
  | Tcase _ -> unsupportedTerm t
129
      "alt-ergo : you must eliminate match"
130
  | Teps _ -> unsupportedTerm t
131
      "alt-ergo : you must eliminate epsilon"
132
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
133

134
and print_tapp info fmt = function
135
  | [] -> ()
136
  | tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
137

138
let rec print_fmla info fmt f =
139
  if info.info_show_labels then
140 141 142 143 144 145 146 147 148 149
    match Slab.elements f.t_label with
      | [] -> print_fmla_node info fmt f
      | l ->
        fprintf fmt "(%a : %a)"
          (print_list colon print_label) l
          (print_fmla_node info) f
  else
    print_fmla_node info fmt f

and print_fmla_node info fmt f = match f.t_node with
150
  | Tapp ({ ls_name = id }, []) ->
151
      print_ident fmt id
152
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
153
      | Some s -> syntax_arguments s (print_term info) fmt tl
154
      | None -> fprintf fmt "%a(%a)" print_ident ls.ls_name
155
                    (print_list comma (print_term info)) tl
156
    end
157 158
  | Tquant (q, fq) ->
      let vl, tl, f = t_open_quant fq in
159 160
      let q, tl = match q with
        | Tforall -> "forall", tl
161
        | Texists -> "exists", [] (* Alt-ergo has no triggers for exists *)
162
      in
163
      let forall fmt v =
164 165
        fprintf fmt "%s %a:%a" q (print_ident_label info) v.vs_name
          (print_type info) v.vs_ty
166
      in
167
      fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
168
        (print_triggers info) tl (print_fmla info) f;
169
      List.iter forget_var vl
170
  | Tbinop (Tand, f1, f2) ->
171
      fprintf fmt "(%a and@ %a)" (print_fmla info) f1 (print_fmla info) f2
172
  | Tbinop (Tor, f1, f2) ->
173
      fprintf fmt "(%a or@ %a)" (print_fmla info) f1 (print_fmla info) f2
174
  | Tbinop (Timplies, f1, f2) ->
175
      fprintf fmt "(%a ->@ %a)" (print_fmla info) f1 (print_fmla info) f2
176
  | Tbinop (Tiff, f1, f2) ->
177
      fprintf fmt "(%a <->@ %a)" (print_fmla info) f1 (print_fmla info) f2
178
  | Tnot f ->
179
      fprintf fmt "(not %a)" (print_fmla info) f
180
  | Ttrue ->
181
      fprintf fmt "true"
182
  | Tfalse ->
183
      fprintf fmt "false"
184
  | Tif (f1, f2, f3) ->
185
      fprintf fmt "((%a and@ %a)@ or@ (not@ %a and@ %a))"
186
        (print_fmla info) f1 (print_fmla info) f2 (print_fmla info)
187
        f1 (print_fmla info) f3
188
  | Tlet _ -> unsupportedTerm f
189
      "alt-ergo: you must eliminate let in formula"
190
  | Tcase _ -> unsupportedTerm f
191
      "alt-ergo: you must eliminate match"
192
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
193

194 195
and print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
196

197
and print_triggers info fmt tl =
198
  let filter = function
199 200
    | { t_ty = Some _ } -> true
    | { t_node = Tapp (ps,_) } -> not (ls_equal ps ps_equ)
201
    | _ -> false in
202
  let tl = List.map (List.filter filter) tl in
203
  let tl = List.filter (function [] -> false | _::_ -> true) tl in
204
  if tl = [] then () else fprintf fmt "@ [%a]"
205
    (print_list alt (print_list comma (print_expr info))) tl
206

207 208
let print_logic_binder info fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty
209

210
let print_type_decl fmt ts = match ts.ts_args with
211
  | [] -> fprintf fmt "type %a"
212
      print_ident ts.ts_name
213
  | [tv] -> fprintf fmt "type %a %a"
214
      print_tvsymbol tv print_ident ts.ts_name
215
  | tl -> fprintf fmt "type (%a) %a"
216
      (print_list comma print_tvsymbol) tl print_ident ts.ts_name
217

218 219
let print_enum_decl fmt ts csl =
  let print_cs fmt (ls,_) = print_ident fmt ls.ls_name in
220 221
  fprintf fmt "@[<hov 2>type %a =@ %a@]@\n@\n" print_ident ts.ts_name
    (print_list alt2 print_cs) csl
222

223 224 225 226 227 228
let print_ty_decl info fmt ts =
  if Mid.mem ts.ts_name info.info_syn then () else
  (fprintf fmt "%a@\n@\n" print_type_decl ts; forget_tvs ())

let print_data_decl info fmt = function
  | ts, csl (* monomorphic enumeration *)
229 230
    when ts.ts_args = [] && List.for_all (fun (_,l) -> l = []) csl ->
      print_enum_decl fmt ts csl
231
  | ts, [cs,_] (* non-recursive records *)
232 233 234 235 236 237 238
    when Mls.mem cs info.info_csm ->
      let pjl = Mls.find cs info.info_csm in
      let print_field fmt ls =
        fprintf fmt "%a@ :@ %a" print_ident ls.ls_name
          (print_type info) (Util.of_option ls.ls_value) in
      fprintf fmt "%a@ =@ {@ %a@ }@\n@\n" print_type_decl ts
        (print_list semi print_field) pjl
239
  | _, _ -> unsupported
240
      "alt-ergo : algebraic datatype are not supported"
241

242 243 244 245 246 247 248 249
let print_param_decl info fmt ls =
  let sac = if Sls.mem ls info.info_ac then "ac " else "" in
  fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n@\n"
    sac print_ident ls.ls_name
    (print_list comma (print_type info)) ls.ls_args
    (if ls.ls_args = [] then "" else " -> ")
    (print_option_or_default "prop" (print_type info)) ls.ls_value

Andrei Paskevich's avatar
Andrei Paskevich committed
250 251 252 253
let print_param_decl info fmt ls =
  if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
    then () else (print_param_decl info fmt ls; forget_tvs ())

254 255 256 257 258 259 260 261 262 263
let print_logic_decl info fmt ls ld =
  let vl,e = open_ls_defn ld in
  begin match e.t_ty with
    | Some _ ->
        (* TODO AC? *)
        fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n@\n"
          print_ident ls.ls_name
          (print_list comma (print_logic_binder info)) vl
          (print_type info) (Util.of_option ls.ls_value)
          (print_term info) e
264
    | None ->
265 266 267 268 269 270
        fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]@\n@\n"
          print_ident ls.ls_name
          (print_list comma (print_logic_binder info)) vl
          (print_fmla info) e
  end;
  List.iter forget_var vl
271

272
let print_logic_decl info fmt (ls,ld) =
273 274
  if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
    then () else (print_logic_decl info fmt ls ld; forget_tvs ())
275 276 277 278 279 280 281 282 283 284 285

let print_prop_decl info fmt k pr f = match k with
  | Paxiom ->
      fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n@\n"
        print_ident pr.pr_name (print_fmla info) f
  | Pgoal ->
      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
        print_ident pr.pr_name (print_fmla info) f
  | Plemma| Pskip -> assert false

let print_prop_decl info fmt k pr f =
286 287
  if Mid.mem pr.pr_name info.info_syn || Spr.mem pr info.info_axs
    then () else (print_prop_decl info fmt k pr f; forget_tvs ())
288

289
let print_decl info fmt d = match d.d_node with
290 291 292 293 294 295
  | Dtype ts ->
      print_ty_decl info fmt ts
  | Ddata dl ->
      print_list nothing (print_data_decl info) fmt dl
  | Dparam ls ->
      print_param_decl info fmt ls
296
  | Dlogic dl ->
297
      print_list nothing (print_logic_decl info) fmt dl
298
  | Dind _ -> unsupportedDecl d
299
      "alt-ergo: inductive definitions are not supported"
300
  | Dprop (k,pr,f) -> print_prop_decl info fmt k pr f
301

302
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
303

304 305 306 307 308 309 310 311
let add_projection (csm,pjs,axs) = function
  | [Theory.MAls ls; Theory.MAls cs; Theory.MAint ind; Theory.MApr pr] ->
      let csm = try Array.set (Mls.find cs csm) ind ls; csm
      with Not_found ->
        Mls.add cs (Array.make (List.length cs.ls_args) ls) csm in
      csm, Sls.add ls pjs, Spr.add pr axs
  | _ -> assert false

312 313 314 315
let check_showlabels acc l =
  match l with
    | [Theory.MAstr s] ->
      begin match s with
316 317
        | "show_labels" -> true
        | _ -> acc
318 319 320 321
      end
    | _ -> assert false

(*
322
let print_task_old pr thpr fmt task =
323 324
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
325 326
  let csm,pjs,axs = Task.on_meta Eliminate_algebraic.meta_proj
    add_projection (Mls.empty,Sls.empty,Spr.empty) task in
327
  let info = {
328
    info_syn = get_syntax_map task;
329
    info_ac  = Task.on_tagged_ls meta_ac task;
330 331
    info_show_labels =
      Task.on_meta meta_printer_option check_showlabels false task;
332 333 334
    info_csm = Mls.map Array.to_list csm;
    info_pjs = pjs;
    info_axs = axs;
335
  } in
Andrei Paskevich's avatar
Andrei Paskevich committed
336
  let decls = Task.task_decls task in
337
  fprintf fmt "%a@." (print_list nothing (print_decl info)) decls
338

339
let () = register_printer "alt-ergo-old"
340
  (fun _env pr thpr ?old:_ fmt task ->
341
     forget_all ident_printer;
342
     print_task_old pr thpr fmt task)
343
*)
344 345

let print_decls =
346
  let print ac sl csm pjs axs sm fmt d =
347 348
    let info = {
      info_syn = sm;
349
      info_ac  = ac;
350
      info_show_labels = sl;
351
      info_csm = Mls.map Array.to_list csm;
352 353 354
      info_pjs = pjs;
      info_axs = axs;
    } in
355 356
    print_decl info fmt d in
  Trans.on_tagged_ls meta_ac (fun ac ->
357 358
  Trans.on_meta meta_printer_option (fun args ->
    let sl = List.fold_left check_showlabels false args in
359
  Trans.on_meta Eliminate_algebraic.meta_proj (fun mal ->
360 361
    let csm,pjs,axs = List.fold_left
      add_projection (Mls.empty,Sls.empty,Spr.empty) mal in
362
    Printer.sprint_decls (print ac sl csm pjs axs))))
363

364
let print_task _env pr thpr ?old:_ fmt task =
365 366 367 368 369 370 371 372
  (* In trans-based p-printing [forget_all] is a no-no *)
  (* forget_all ident_printer; *)
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
  fprintf fmt "%a@." (print_list nothing string)
    (List.rev (Trans.apply print_decls task))

let () = register_printer "alt-ergo" print_task
373

374 375 376 377 378
(*
let print_goal info fmt (id, f, task) =
  print_task info fmt task;
  fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla info) f
*)
379