alt_ergo.ml 8.48 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
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
29
30
let ident_printer = 
  let bls = ["let"; "forall"; "exists"; "and"; "or"] in
  let san = sanitizer char_to_alpha char_to_alnumus in
31
  create_ident_printer bls ~sanitizer:san
32
33

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

Francois Bobot's avatar
Francois Bobot committed
36
37
38
39
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
40

41
42
let forget_var v = forget_id ident_printer v.vs_name

43
let rec print_type drv fmt ty = match ty.ty_node with
44
  | Tyvar id -> 
45
      print_tvsymbols fmt id
46
  | Tyapp (ts, tl) -> 
47
      match drv ts.ts_name with
48
49
50
51
52
53
54
55
56
57
        | Driver.Remove -> assert false (* Mettre une erreur *)
        | Driver.Syntax s ->
            Driver.syntax_arguments s (print_type drv) fmt tl
        | Driver.Tag _ -> 
            begin
              match ty.ty_node with
                | Tyvar _ -> assert false
                | Tyapp (ts,[]) -> 
                    print_ident fmt ts.ts_name
                | Tyapp (ts, [ty]) -> 
58
59
                    fprintf fmt "%a %a" (print_type drv) 
                      ty print_ident ts.ts_name
60
61
                | Tyapp (ts, tyl) ->
                    fprintf fmt "(%a) %a" 
62
63
	              (print_list comma (print_type drv)) 
                      tyl print_ident ts.ts_name
64
            end
65
let rec print_term drv fmt t = match t.t_node with
66
67
  | Tbvar _ -> 
      assert false
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
68
69
  | Tconst c ->
      Pretty.print_const fmt c
70
  | Tvar { vs_name = id } ->
71
72
      print_ident fmt id
  | Tapp (ls, tl) ->
73
      begin      
74
        match drv ls.ls_name with
75
76
77
          | Driver.Remove -> assert false (* Mettre une erreur *)
          | Driver.Syntax s ->
              Driver.syntax_arguments s (print_term drv) fmt tl
78
79
80
81
          | Driver.Tag _ ->
              match tl with
                | [] -> print_ident fmt ls.ls_name
                | tl ->
82
83
84
              fprintf fmt "%a(%a)" 
	        print_ident ls.ls_name (print_list comma (print_term drv)) tl
      end
85
86
87
  | Tlet (t1, tb) ->
      let v, t2 = t_open_bound tb in
      fprintf fmt "@[(let %a = %a@ in %a)@]" print_ident v.vs_name
88
        (print_term drv) t1 (print_term drv) t2;
89
      forget_var v
90
91
  | Tif _ ->
      assert false
92
93
94
95
96
  | Tcase _ ->
      assert false
  | Teps _ ->
      assert false

97
let rec print_fmla drv fmt f = match f.f_node with
98
99
100
  | Fapp ({ ls_name = id }, []) ->
      print_ident fmt id
  | Fapp (ls, tl) ->
101
      begin      
102
        match drv ls.ls_name with
103
104
105
106
107
108
109
          | Driver.Remove -> assert false (* Mettre une erreur *)
          | Driver.Syntax s ->
              Driver.syntax_arguments s (print_term drv) fmt tl
          | Driver.Tag _ -> 
              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
110
111
  | Fquant (q, fq) ->
      let q = match q with Fforall -> "forall" | Fexists -> "exists" in
112
113
      let vl, tl, f = f_open_quant fq in
      let forall fmt v = 
114
	fprintf fmt "%s %a:%a" q print_ident v.vs_name (print_type drv) v.vs_ty
115
      in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116
117
      fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
        (print_triggers drv) tl (print_fmla drv) f;
118
      List.iter forget_var vl
119
  | Fbinop (Fand, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
120
      fprintf fmt "(%a and@ %a)" (print_fmla drv) f1 (print_fmla drv) f2
121
  | Fbinop (For, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
122
      fprintf fmt "(%a or@ %a)" (print_fmla drv) f1 (print_fmla drv) f2
123
  | Fbinop (Fimplies, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
124
      fprintf fmt "(%a ->@ %a)" (print_fmla drv) f1 (print_fmla drv) f2
125
  | Fbinop (Fiff, f1, f2) ->
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
126
      fprintf fmt "(%a <->@ %a)" (print_fmla drv) f1 (print_fmla drv) f2
127
  | Fnot f ->
128
      fprintf fmt "(not %a)" (print_fmla drv) f
129
130
131
132
133
134
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fif (f1, f2, f3) ->
      fprintf fmt "((%a and %a) or (not %a and %a))"
135
136
	(print_fmla drv) f1 (print_fmla drv) f2 (print_fmla drv)
        f1 (print_fmla drv) f3
137
138
139
140
141
  | Flet _ ->
      assert false
  | Fcase _ ->
      assert false

142
and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
143

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
144
145
146
and print_triggers drv fmt tl =
  if tl = [] then () else fprintf fmt "@ [%a]"
    (print_list alt (print_list comma (print_expr drv))) tl
147

148
149
let print_logic_binder drv fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type drv) v.vs_ty
150

151
let print_type_decl drv fmt = function
152
  | ts, Tabstract ->
153
      begin
154
        match drv ts.ts_name with
155
          | Driver.Remove | Driver.Syntax _ -> false
156
157
158
          | Driver.Tag _ -> 
              match ts.ts_args with
                | [] -> fprintf fmt "type %a" print_ident ts.ts_name; true
159
                | _  -> fprintf fmt "type (%a) %a" 
160
161
                    (print_list comma print_tvsymbols) ts.ts_args  
                      print_ident ts.ts_name; true
162
      end
163
164
165
  | _, Talgebraic _ ->
      assert false

166
let ac_th = ["algebra";"AC"]
167

Andrei Paskevich's avatar
Andrei Paskevich committed
168
let print_logic_decl drv task fmt (ls,ld) =
169
  match drv ls.ls_name with
170
171
172
173
    | Driver.Remove | Driver.Syntax _ -> false
    | Driver.Tag s ->
        begin match ld with
          | None ->
Andrei Paskevich's avatar
Andrei Paskevich committed
174
              let sac = if Util.Sstr.mem "AC" s then "ac " else "" in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
175
              fprintf fmt "@[<hov 2>logic %s%a : %a%s%a@]@\n"
176
177
                sac print_ident ls.ls_name
                (print_list comma (print_type drv)) ls.ls_args 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
178
		(if ls.ls_args = [] then "" else " -> ")
179
                (print_option_or_default "prop" (print_type drv)) ls.ls_value
180
          | Some ld ->
181
              let vl,e = open_ls_defn ld in
182
183
              begin match e with
                | Term t ->
Francois Bobot's avatar
Francois Bobot committed
184
                    (* TODO AC? *)
185
186
187
188
189
190
                    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 ->
191
                    fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]"
Francois Bobot's avatar
Francois Bobot committed
192
	              print_ident ls.ls_name 
193
194
195
196
197
198
199
                      (print_list comma (print_logic_binder drv)) vl 
                      (print_fmla drv) f
              end;
              List.iter forget_var vl
        end;
        true
  
Andrei Paskevich's avatar
Andrei Paskevich committed
200
let print_decl drv task fmt d = match d.d_node with
201
  | Dtype dl ->
202
      print_list_opt newline (print_type_decl drv) fmt dl
203
  | Dlogic dl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
204
      print_list_opt newline (print_logic_decl drv task) fmt dl
205
  | Dind _ -> assert false (* TODO *)
206
  | Dprop (Paxiom, pr, _) when
207
      drv pr.pr_name = Driver.Remove -> false
208
  | Dprop (Paxiom, pr, f) ->
209
      fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n" 
210
        print_ident pr.pr_name (print_fmla drv) f; true
211
  | Dprop (Pgoal, pr, f) ->
212
      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
213
        print_ident pr.pr_name (print_fmla drv) f; true
214
  | Dprop (Plemma, _, _) ->
215
216
      assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
217
218
let print_context drv fmt task = 
  let decls = Task.task_decls task in
219
  ignore (print_list_opt (add_flush newline2) (print_decl drv task) fmt decls)
220

221
let () = Driver.register_printer "alt-ergo" 
Andrei Paskevich's avatar
Andrei Paskevich committed
222
  (fun drv fmt task -> 
223
     forget_all ident_printer;
Andrei Paskevich's avatar
Andrei Paskevich committed
224
     print_context drv fmt task)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
225

Andrei Paskevich's avatar
Andrei Paskevich committed
226
227
let print_goal drv fmt (id, f, task) =
  print_context drv fmt task;
228
  fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla drv) f