alt_ergo.ml 8.54 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.                  *)
(*                                                                        *)
(**************************************************************************)
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
19

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

29
let ident_printer = 
30
31
32
33
34
35
36
  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
37
  let san = sanitizer char_to_alpha char_to_alnumus in
38
  create_ident_printer bls ~sanitizer:san
39
40

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

Francois Bobot's avatar
Francois Bobot committed
43
44
45
46
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
47

48
49
let forget_var v = forget_id ident_printer v.vs_name

50
let rec print_type drv fmt ty = match ty.ty_node with
51
  | Tyvar id -> 
52
      print_tvsymbols fmt id
53
  | Tyapp (ts, tl) -> begin match Driver.query_syntax drv ts.ts_name with
54
55
56
57
58
59
60
61
62
      | 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

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

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
130
and print_triggers drv fmt tl =
131
  let filter = function 
132
133
    | Term _ -> true 
    | Fmla {f_node = Fapp (ps,_)} -> not (ls_equal ps ps_equ)
134
135
    | _ -> false in
  let tl = List.map (List.filter filter)
136
    tl in
137
  let tl = List.filter (function [] -> false | _::_ -> true) tl in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
138
139
  if tl = [] then () else fprintf fmt "@ [%a]"
    (print_list alt (print_list comma (print_expr drv))) tl
140

141
142
let print_logic_binder drv fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type drv) v.vs_ty
143

144
145
let print_type_decl fmt ts = match ts.ts_args with
  | [] -> fprintf fmt "type %a" print_ident ts.ts_name
146
  | [tv] -> fprintf fmt "type %a %a" print_tvsymbols tv print_ident ts.ts_name
147
148
149
  | tl -> fprintf fmt "type (%a) %a" 
      (print_list comma print_tvsymbols) tl print_ident ts.ts_name

150
let print_type_decl drv fmt = function
151
  | ts, Tabstract when Driver.query_remove drv ts.ts_name -> false
152
  | ts, Tabstract -> print_type_decl fmt ts; true
153
154
  | _, Talgebraic _ -> unsupported 
      "alt-ergo : algebraic datatype are not supported"
155

156
let ac_th = ["algebra";"AC"]
157

158
let print_logic_decl drv fmt (ls,ld) =
159
  let tags = Driver.query_tags drv ls.ls_name in
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
  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
183
        end;
184
185
186
        List.iter forget_var vl

let print_logic_decl drv fmt d =
187
188
  if Driver.query_remove drv (fst d).ls_name then
    false else (print_logic_decl drv fmt d; true)
189
190

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

207
let print_decl drv fmt = catch_unsupportedDecl (print_decl drv fmt)
208

209
let print_task drv fmt task = 
210
  Driver.print_full_prelude drv task fmt;
Andrei Paskevich's avatar
Andrei Paskevich committed
211
  let decls = Task.task_decls task in
212
  ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls)
213

214
let () = register_printer "alt-ergo" 
Andrei Paskevich's avatar
Andrei Paskevich committed
215
  (fun drv fmt task -> 
216
     forget_all ident_printer;
217
     print_task drv fmt task)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
218

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