alt_ergo.ml 12.7 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
(*    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
headers  
Jean-Christophe Filliâtre committed
19

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

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

31
let meta_ac = Theory.register_meta "AC" [Theory.MTlsymbol]
32

33
let ident_printer =
34
  let bls = [
35
    "ac"; "and"; "array"; "as"; "axiom"; "bool"; "distinct"; "else"; "exists";
36 37 38
    "false"; "forall"; "function"; "goal"; "if"; "int"; "bitv";
    "logic"; "not"; "or"; "parameter"; "predicate";
    "prop"; "real"; "then"; "true"; "type"; "unit"; "void";
39
    "select"; "store";
40
  ]
41
  in
42
  let san = sanitizer char_to_alpha char_to_alnumus in
43
  create_ident_printer bls ~sanitizer:san
44 45

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

48 49
let forget_var v = forget_id ident_printer v.vs_name

50 51 52 53 54 55 56 57 58
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

59
type info = {
60
  info_syn : syntax_map;
61
  info_ac  : Sls.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
62 63 64
  info_csm : lsymbol list Mls.t;
  info_pjs : Sls.t;
  info_axs : Spr.t;
65 66 67
}

let rec print_type info fmt ty = match ty.ty_node with
68
  | Tyvar id ->
69
      print_tvsymbol fmt id
70
  | Tyapp (ts, tl) -> begin match query_syntax info.info_syn ts.ts_name with
71 72
      | Some s -> syntax_arguments s (print_type info) fmt tl
      | None -> fprintf fmt "%a%a" (print_tyapp info) tl print_ident ts.ts_name
73 74
    end

75
and print_tyapp info fmt = function
76
  | [] -> ()
77 78
  | [ty] -> fprintf fmt "%a " (print_type info) ty
  | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
79

80
let rec print_term info fmt t = match t.t_node with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
81
  | Tconst c ->
82 83 84 85 86 87 88 89 90 91 92 93 94
      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
95
  | Tvar { vs_name = id } ->
96
      print_ident fmt id
97
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
98
      | Some s -> syntax_arguments s (print_term info) fmt tl
Andrei Paskevich's avatar
Andrei Paskevich committed
99 100 101 102 103 104 105 106 107
      | 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
108
    end
109
  | Tlet _ -> unsupportedTerm t
110
      "alt-ergo : you must eliminate let in term"
111
  | Tif _ -> unsupportedTerm t
112
      "alt-ergo : you must eliminate if_then_else"
113
  | Tcase _ -> unsupportedTerm t
114
      "alt-ergo : you must eliminate match"
115
  | Teps _ -> unsupportedTerm t
116
      "alt-ergo : you must eliminate epsilon"
117
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
118

119
and print_tapp info fmt = function
120
  | [] -> ()
121
  | tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
122

123 124
let rec print_fmla info fmt f = match f.t_node with
  | Tapp ({ ls_name = id }, []) ->
125
      print_ident fmt id
126
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
127
      | Some s -> syntax_arguments s (print_term info) fmt tl
128
      | None -> fprintf fmt "%a(%a)" print_ident ls.ls_name
129
                    (print_list comma (print_term info)) tl
130
    end
131 132
  | Tquant (q, fq) ->
      let vl, tl, f = t_open_quant fq in
133 134
      let q, tl = match q with
        | Tforall -> "forall", tl
135
        | Texists -> "exists", [] (* Alt-ergo has no triggers for exists *)
136
      in
137
      let forall fmt v =
138
        fprintf fmt "%s %a:%a" q print_ident v.vs_name (print_type info) v.vs_ty
139
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
140
      fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
141
        (print_triggers info) tl (print_fmla info) f;
142
      List.iter forget_var vl
143
  | Tbinop (Tand, f1, f2) ->
144
      fprintf fmt "(%a and@ %a)" (print_fmla info) f1 (print_fmla info) f2
145
  | Tbinop (Tor, f1, f2) ->
146
      fprintf fmt "(%a or@ %a)" (print_fmla info) f1 (print_fmla info) f2
147
  | Tbinop (Timplies, f1, f2) ->
148
      fprintf fmt "(%a ->@ %a)" (print_fmla info) f1 (print_fmla info) f2
149
  | Tbinop (Tiff, f1, f2) ->
150
      fprintf fmt "(%a <->@ %a)" (print_fmla info) f1 (print_fmla info) f2
151
  | Tnot f ->
152
      fprintf fmt "(not %a)" (print_fmla info) f
153
  | Ttrue ->
154
      fprintf fmt "true"
155
  | Tfalse ->
156
      fprintf fmt "false"
157
  | Tif (f1, f2, f3) ->
158
      fprintf fmt "((%a and@ %a)@ or@ (not@ %a and@ %a))"
159
        (print_fmla info) f1 (print_fmla info) f2 (print_fmla info)
160
        f1 (print_fmla info) f3
161
  | Tlet _ -> unsupportedTerm f
162
      "alt-ergo : you must eliminate let in formula"
163
  | Tcase _ -> unsupportedTerm f
164
      "alt-ergo : you must eliminate match"
165
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
166

167 168
and print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)
169

170
and print_triggers info fmt tl =
171
  let filter = function
Andrei Paskevich's avatar
Andrei Paskevich committed
172 173
    | { t_ty = Some _ } -> true
    | { t_node = Tapp (ps,_) } -> not (ls_equal ps ps_equ)
174
    | _ -> false in
175
  let tl = List.map (List.filter filter) tl in
176
  let tl = List.filter (function [] -> false | _::_ -> true) tl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
177
  if tl = [] then () else fprintf fmt "@ [%a]"
178
    (print_list alt (print_list comma (print_expr info))) tl
179

180 181
let print_logic_binder info fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty
182

183
let print_type_decl fmt ts = match ts.ts_args with
Andrei Paskevich's avatar
Andrei Paskevich committed
184
  | [] -> fprintf fmt "type %a"
185
      print_ident ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
186
  | [tv] -> fprintf fmt "type %a %a"
187
      print_tvsymbol tv print_ident ts.ts_name
Andrei Paskevich's avatar
Andrei Paskevich committed
188
  | tl -> fprintf fmt "type (%a) %a"
189
      (print_list comma print_tvsymbol) tl print_ident ts.ts_name
190

191 192
let print_enum_decl fmt ts csl =
  let print_cs fmt (ls,_) = print_ident fmt ls.ls_name in
193 194
  fprintf fmt "@[<hov 2>type %a =@ %a@]@\n@\n" print_ident ts.ts_name
    (print_list alt2 print_cs) csl
195

196 197 198 199 200 201
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 *)
202 203
    when ts.ts_args = [] && List.for_all (fun (_,l) -> l = []) csl ->
      print_enum_decl fmt ts csl
204
  | ts, [cs,_] (* non-recursive records *)
Andrei Paskevich's avatar
Andrei Paskevich committed
205 206 207 208 209 210 211
    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
212
  | _, _ -> unsupported
213
      "alt-ergo : algebraic datatype are not supported"
214

215 216 217 218 219 220 221 222
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
223 224 225 226
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 ())

227 228 229 230 231 232 233 234 235 236
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
237
    | None ->
238 239 240 241 242 243
        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
244

245
let print_logic_decl info fmt (ls,ld) =
Andrei Paskevich's avatar
Andrei Paskevich committed
246 247
  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 ())
248 249 250 251 252 253 254 255 256 257 258

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 =
Andrei Paskevich's avatar
Andrei Paskevich committed
259 260
  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 ())
261

262
let print_decl info fmt d = match d.d_node with
263 264 265 266 267 268
  | 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
269
  | Dlogic dl ->
270
      print_list nothing (print_logic_decl info) fmt dl
271
  | Dind _ -> unsupportedDecl d
272
      "alt-ergo : inductive definition are not supported"
273
  | Dprop (k,pr,f) -> print_prop_decl info fmt k pr f
274

275
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
276

277 278 279 280 281 282 283 284
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

285
let print_task_old pr thpr fmt task =
286 287
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
288 289
  let csm,pjs,axs = Task.on_meta Eliminate_algebraic.meta_proj
    add_projection (Mls.empty,Sls.empty,Spr.empty) task in
290
  let info = {
Andrei Paskevich's avatar
Andrei Paskevich committed
291
    info_syn = get_syntax_map task;
Andrei Paskevich's avatar
Andrei Paskevich committed
292
    info_ac  = Task.on_tagged_ls meta_ac task;
293 294 295
    info_csm = Mls.map Array.to_list csm;
    info_pjs = pjs;
    info_axs = axs;
Andrei Paskevich's avatar
Andrei Paskevich committed
296
  } in
Andrei Paskevich's avatar
Andrei Paskevich committed
297
  let decls = Task.task_decls task in
298
  fprintf fmt "%a@." (print_list nothing (print_decl info)) decls
299

300
let () = register_printer "alt-ergo-old"
301
  (fun _env pr thpr ?old:_ fmt task ->
302
     forget_all ident_printer;
303 304 305
     print_task_old pr thpr fmt task)

let print_decls =
Andrei Paskevich's avatar
Andrei Paskevich committed
306
  let print ac csm pjs axs sm fmt d =
307 308
    let info = {
      info_syn = sm;
Andrei Paskevich's avatar
Andrei Paskevich committed
309
      info_ac  = ac;
310
      info_csm = Mls.map Array.to_list csm;
Andrei Paskevich's avatar
Andrei Paskevich committed
311 312 313
      info_pjs = pjs;
      info_axs = axs;
    } in
314 315
    print_decl info fmt d in
  Trans.on_tagged_ls meta_ac (fun ac ->
Andrei Paskevich's avatar
Andrei Paskevich committed
316
  Trans.on_meta Eliminate_algebraic.meta_proj (fun mal ->
317 318
    let csm,pjs,axs = List.fold_left
      add_projection (Mls.empty,Sls.empty,Spr.empty) mal in
Andrei Paskevich's avatar
Andrei Paskevich committed
319
    Printer.sprint_decls (print ac csm pjs axs)))
320

321
let print_task _env pr thpr ?old:_ fmt task =
322 323 324 325 326 327 328 329
  (* 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
330

331 332 333 334 335
(*
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
*)
336