alt_ergo.ml 8.46 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)
19
open Register
20
21
22
23
24
open Format
open Pp
open Ident
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
25
26
open Decl
open Task
27

28
let ident_printer = 
29
30
31
32
33
34
35
  let bls = [
    "ac"; "and"; "array"; "as"; "axiom"; "bool"; "else"; "exists";
    "false"; "forall"; "function"; "goal"; "if"; "int"; "bitv";
    "logic"; "not"; "or"; "parameter"; "predicate";
    "prop"; "real"; "then"; "true"; "type"; "unit"; "void";
  ] 
  in
36
  let san = sanitizer char_to_alpha char_to_alnumus in
37
  create_ident_printer bls ~sanitizer:san
38
39

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

Francois Bobot's avatar
Francois Bobot committed
42
43
44
45
let print_tvsymbols fmt tv =
  let sanitize n = "'" ^ n in
  let n = id_unique ident_printer ~sanitizer:sanitize tv.tv_name in
  fprintf fmt "%s" n
46

47
48
let forget_var v = forget_id ident_printer v.vs_name

49
let rec print_type drv fmt ty = match ty.ty_node with
50
  | Tyvar id -> 
51
      print_tvsymbols fmt id
52
  | Tyapp (ts, tl) -> begin match Driver.query_syntax drv ts.ts_name with
53
54
55
56
57
58
59
60
61
      | Some s -> Driver.syntax_arguments s (print_type drv) fmt tl
      | None -> fprintf fmt "%a%a" (print_tyapp drv) tl print_ident ts.ts_name
    end

and print_tyapp drv fmt = function
  | [] -> ()
  | [ty] -> fprintf fmt "%a " (print_type drv) ty
  | tl -> fprintf fmt "(%a) " (print_list comma (print_type drv)) tl

62
let rec print_term drv fmt t = match t.t_node with
63
64
  | Tbvar _ -> 
      assert false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
65
66
  | Tconst c ->
      Pretty.print_const fmt c
67
  | Tvar { vs_name = id } ->
68
      print_ident fmt id
69
  | Tapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
70
71
72
      | Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
      | None -> fprintf fmt "%a%a" print_ident ls.ls_name (print_tapp drv) tl
    end
73
74
75
76
77
78
79
80
  | Tlet _ -> unsupportedExpression (Term t)
      "alt-ergo : you must eliminate let in term"
  | Tif _ -> unsupportedExpression (Term t) 
      "alt-ergo : you must eliminate if_then_else"
  | Tcase _ -> unsupportedExpression (Term t) 
      "alt-ergo : you must eliminate match"
  | Teps _ -> unsupportedExpression (Term t) 
      "alt-ergo : you must eliminate epsilon"
81

82
83
84
85
and print_tapp drv fmt = function
  | [] -> ()
  | tl -> fprintf fmt "(%a)" (print_list comma (print_term drv)) tl

86
let rec print_fmla drv fmt f = match f.f_node with
87
88
  | Fapp ({ ls_name = id }, []) ->
      print_ident fmt id
89
  | Fapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
90
91
92
93
      | Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
      | None -> fprintf fmt "%a(%a)" print_ident ls.ls_name 
                    (print_list comma (print_term drv)) tl
    end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94
95
  | Fquant (q, fq) ->
      let q = match q with Fforall -> "forall" | Fexists -> "exists" in
96
97
      let vl, tl, f = f_open_quant fq in
      let forall fmt v = 
98
	fprintf fmt "%s %a:%a" q print_ident v.vs_name (print_type drv) v.vs_ty
99
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
100
101
      fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
        (print_triggers drv) tl (print_fmla drv) f;
102
      List.iter forget_var vl
103
  | Fbinop (Fand, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
104
      fprintf fmt "(%a and@ %a)" (print_fmla drv) f1 (print_fmla drv) f2
105
  | Fbinop (For, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
106
      fprintf fmt "(%a or@ %a)" (print_fmla drv) f1 (print_fmla drv) f2
107
  | Fbinop (Fimplies, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
108
      fprintf fmt "(%a ->@ %a)" (print_fmla drv) f1 (print_fmla drv) f2
109
  | Fbinop (Fiff, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
110
      fprintf fmt "(%a <->@ %a)" (print_fmla drv) f1 (print_fmla drv) f2
111
  | Fnot f ->
112
      fprintf fmt "(not %a)" (print_fmla drv) f
113
114
115
116
117
118
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fif (f1, f2, f3) ->
      fprintf fmt "((%a and %a) or (not %a and %a))"
119
120
	(print_fmla drv) f1 (print_fmla drv) f2 (print_fmla drv)
        f1 (print_fmla drv) f3
121
122
123
124
125
  | Flet _ -> unsupportedExpression (Fmla f)
      "alt-ergo : you must eliminate let in formula"
  | Fcase _ -> unsupportedExpression (Fmla f) 
      "alt-ergo : you must eliminate match"
  
126

127
and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
128

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
129
and print_triggers drv fmt tl =
130
131
  let tl = List.map (List.filter (function Term _ -> true | Fmla _ -> false))
    tl in
132
  let tl = List.filter (function [] -> false | _::_ -> true) tl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
133
134
  if tl = [] then () else fprintf fmt "@ [%a]"
    (print_list alt (print_list comma (print_expr drv))) tl
135

136
137
let print_logic_binder drv fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type drv) v.vs_ty
138

139
140
141
142
143
let print_type_decl fmt ts = match ts.ts_args with
  | [] -> fprintf fmt "type %a" print_ident ts.ts_name
  | tl -> fprintf fmt "type (%a) %a" 
      (print_list comma print_tvsymbols) tl print_ident ts.ts_name

144
let print_type_decl drv fmt = function
145
  | ts, Tabstract when Driver.query_remove drv ts.ts_name -> false
146
  | ts, Tabstract -> print_type_decl fmt ts; true
147
148
  | _, Talgebraic _ -> unsupported 
      "alt-ergo : algebraic datatype are not supported"
149

150
let ac_th = ["algebra";"AC"]
151

152
let print_logic_decl drv fmt (ls,ld) =
153
  let tags = Driver.query_tags drv ls.ls_name in
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
  match ld with
    | None ->
        let sac = if Util.Sstr.mem "AC" tags then "ac " else "" in
        fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n"
          sac print_ident ls.ls_name
          (print_list comma (print_type drv)) ls.ls_args 
          (if ls.ls_args = [] then "" else " -> ")
          (print_option_or_default "prop" (print_type drv)) ls.ls_value
    | Some ld ->
        let vl,e = open_ls_defn ld in
        begin match e with
          | Term t ->
              (* TODO AC? *)
              fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" 
                print_ident ls.ls_name
                (print_list comma (print_logic_binder drv)) vl 
                (print_type drv) (Util.of_option ls.ls_value) 
                (print_term drv) t
          | Fmla f ->
              fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]"
                print_ident ls.ls_name 
                (print_list comma (print_logic_binder drv)) vl 
                (print_fmla drv) f
177
        end;
178
179
180
        List.iter forget_var vl

let print_logic_decl drv fmt d =
181
182
  if Driver.query_remove drv (fst d).ls_name then
    false else (print_logic_decl drv fmt d; true)
183
184

let print_decl drv fmt d = match d.d_node with
185
  | Dtype dl ->
186
      print_list_opt newline (print_type_decl drv) fmt dl
187
  | Dlogic dl ->
188
      print_list_opt newline (print_logic_decl drv) fmt dl
189
190
  | Dind _ -> unsupportedDeclaration d 
      "alt-ergo : inductive definition are not supported"
191
  | Dprop (Paxiom, pr, _) when Driver.query_remove drv pr.pr_name -> false
192
  | Dprop (Paxiom, pr, f) ->
193
      fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n" 
194
        print_ident pr.pr_name (print_fmla drv) f; true
195
  | Dprop (Pgoal, pr, f) ->
196
      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
197
        print_ident pr.pr_name (print_fmla drv) f; true
198
  | Dprop (Plemma, _, _) ->
199
200
      assert false

201
202
let print_decl drv fmt = catch_unsupportedDeclaration (print_decl drv fmt)

203
let print_task drv fmt task = 
204
  Driver.print_full_prelude drv task fmt;
Andrei Paskevich's avatar
Andrei Paskevich committed
205
  let decls = Task.task_decls task in
206
  ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls)
207

208
let () = register_printer "alt-ergo" 
Andrei Paskevich's avatar
Andrei Paskevich committed
209
  (fun drv fmt task -> 
210
     forget_all ident_printer;
211
     print_task drv fmt task)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
212

Andrei Paskevich's avatar
Andrei Paskevich committed
213
let print_goal drv fmt (id, f, task) =
214
  print_task drv fmt task;
215
  fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla drv) f
216