alt_ergo.ml 8.64 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 25 26

open Format
open Pp
open Ident
open Ty
open Term
open Theory

27 28 29
let ident_printer = 
  let bls = ["let"; "forall"; "exists"; "and"; "or"] in
  let san = sanitizer char_to_alpha char_to_alnumus in
30
  create_ident_printer bls ~sanitizer:san
31 32

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

35 36
let forget_var v = forget_id ident_printer v.vs_name

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

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

131 132 133
and print_trigger drv fmt = function
  | TrTerm t -> (print_term drv) fmt t
  | TrFmla f -> (print_fmla drv) fmt f
134

135
and print_triggers drv fmt tl = print_list comma (print_trigger drv) fmt tl
136 137


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

141
let print_type_decl drv fmt = function
142
  | ts, Tabstract ->
143 144
      begin
        match Driver.query_ident drv ts.ts_name with
145 146
          | Driver.Remove | Driver.Syntax _ -> false
          | Driver.Tag _ -> fprintf fmt "type %a" print_ident ts.ts_name; true
147
      end
148 149 150
  | _, Talgebraic _ ->
      assert false

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

153
let print_logic_decl drv ctxt fmt = function
Francois Bobot's avatar
Francois Bobot committed
154
  | Lfunction (ls, def) ->
155 156
      begin
        match Driver.query_ident drv ls.ls_name with
157
          | Driver.Remove | Driver.Syntax _ -> false
Francois Bobot's avatar
Francois Bobot committed
158
          | Driver.Tag s ->
159 160
              let sac = if Snm.mem "AC" s then "ac " else "" in
              let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
Francois Bobot's avatar
Francois Bobot committed
161 162 163 164 165 166 167 168 169 170 171 172 173 174 175
              match def with
                | None ->
                    let tyl = ls.ls_args in
                    fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
                      sac
                      print_ident ls.ls_name
	              (print_list comma (print_type drv)) tyl (print_type drv) ty;
                    true
                | Some defn ->
                    let id = ls.ls_name in
                    let _, vl, t = open_fs_defn defn in
                    (* TODO AC? *)
                    fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" print_ident id
                      (print_list comma (print_logic_binder drv)) vl (print_type drv) ty (print_term drv) t;
                    List.iter forget_var vl;true
176
      end
Francois Bobot's avatar
Francois Bobot committed
177
  | Lpredicate (ls, def) ->
178 179
      begin
        match Driver.query_ident drv ls.ls_name with
180
          | Driver.Remove | Driver.Syntax _ -> false
Francois Bobot's avatar
Francois Bobot committed
181 182 183 184 185 186 187 188 189 190 191 192
          | Driver.Tag _ -> 
              match def with
                | None ->
                    fprintf fmt "@[<hov 2>logic %a : %a -> prop@]"
	              print_ident ls.ls_name (print_list comma (print_type drv)) ls.ls_args;
                    true
                | Some fd -> 
                    let _,vl,f = open_ps_defn fd in
                    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;
                    true
193
      end
194

195
let print_decl drv ctxt fmt d = match d.d_node with
196
  | Dtype dl ->
197
      print_list_opt newline (print_type_decl drv) fmt dl
198
  | Dlogic dl ->
199
      print_list_opt newline (print_logic_decl drv ctxt) fmt dl
200 201
  | Dind _ -> assert false (* TODO *)
  | Dprop (Paxiom, pr) when
202
      Driver.query_ident drv pr.pr_name = Driver.Remove -> false
203 204
  | Dprop (Paxiom, pr) ->
      fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n" 
205
        print_ident pr.pr_name (print_fmla drv) pr.pr_fmla; true
206 207
  | Dprop (Pgoal, pr) ->
      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
208
        print_ident pr.pr_name (print_fmla drv) pr.pr_fmla; true
209
  | Dprop (Plemma, _) ->
210
      assert false
211
  | Duse _ | Dclone _ -> false
212

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
213
let print_context drv fmt ctxt = 
214
  let decls = Context.get_decls ctxt in
215
  ignore (print_list_opt newline2 (print_decl drv ctxt) fmt decls)
216

217 218 219 220
let () = Driver.register_printer "alt-ergo" 
  (fun drv fmt ctxt -> 
     forget_all ident_printer;
     print_context drv fmt ctxt)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
221

222 223 224
let print_goal drv fmt (id, f, ctxt) =
  print_context drv fmt ctxt;
  fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla drv) f