gappa.ml 15.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10
(********************************************************************)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
11

Francois Bobot's avatar
Francois Bobot committed
12 13
(** Gappa printer *)

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
14 15
open Format
open Pp
16
open Printer
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
17 18 19
open Ident
open Term
open Decl
20
open Theory
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
21 22
open Task

23 24 25 26
let syntactic_transform transf =
  Trans.on_meta meta_syntax_logic (fun metas ->
    let symbols = List.fold_left (fun acc meta_arg ->
      match meta_arg with
27
      | [MAls ls; MAstr _; MAint _] -> Sls.add ls acc
28 29 30 31 32
      | _ -> assert false) Sls.empty metas in
    transf (fun ls -> Sls.mem ls symbols))

let () =
  Trans.register_transform "abstract_unknown_lsymbols"
33
    (syntactic_transform Abstraction.abstraction)
Andrei Paskevich's avatar
Andrei Paskevich committed
34 35
    ~desc:"Abstract@ applications@ of@ non-built-in@ symbols@ with@ \
      constants.@ Used@ by@ the@ Gappa@ pretty-printer.";
36 37 38
  Trans.register_transform "simplify_unknown_lsymbols"
    (syntactic_transform (fun check_ls -> Trans.goal (fun pr f ->
      [create_prop_decl Pgoal pr (Simplify_formula.fmla_cond_subst
39 40 41 42 43 44 45
        (fun t1 t2 -> match t1.t_node with
          | Tconst _ -> false
          | Tapp(_,[]) ->
            begin match t2.t_node with
            | Tconst _ | Tapp(_,[]) -> true
            | _ -> false
            end
46
          | Tapp(ls,_) -> not (check_ls ls)
47
          | _ -> true) f)
48
      ])))
Andrei Paskevich's avatar
Andrei Paskevich committed
49 50
    ~desc:"Same@ as@ simplify_trivial_quantification_in_goal,@ but@ instead@ \
      of@ substituting@ quantified@ variables,@ substitute@ applications@ \
51
      of@ non-built-in@ symbols.@ Used@ by@ the@ Gappa@ pretty-printer."
52

53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
(* patterns (TODO: add a parser and generalize it out of Gappa) *)

type pattern =
  | PatHole of int
  | PatApp of Env.pathname * string * string list * pattern list

let incremental_pat_match env holes =
  let rec aux p t =
    match p, t.t_node with
    | PatHole i, _ ->
        begin match holes.(i) with
        | None -> holes.(i) <- Some t
        | Some t' -> if not (t_equal t t') then raise Not_found
        end
    | PatApp (sp,ss,sl,pl), Tapp (ls,tl) ->
        if List.length pl <> List.length tl then raise Not_found;
Andrei Paskevich's avatar
Andrei Paskevich committed
69
        let th = Env.read_theory env sp ss in
70 71 72 73 74 75 76 77 78 79 80
        let s = ns_find_ls th.th_export sl in
        if not (ls_equal s ls) then raise Not_found;
        List.iter2 aux pl tl
    | _, _ -> raise Not_found in
  aux

let pat_match env nb_holes p t =
  let holes = Array.make nb_holes None in
  incremental_pat_match env holes p t;
  Array.map (function None -> raise Not_found | Some t -> t) holes

81 82
(* Gappa pre-compilation *)

83
type info = {
84
  info_env : Env.env;
85
  info_symbols : Sid.t;
86
  info_ops_of_rel : (string * string * string) Mls.t;
87
  info_syn : syntax_map;
88
}
89

90 91
let int_minus = ref ps_equ
let real_minus = ref ps_equ
92

93
(** lsymbol, ""/"not ", op, rev_op *)
94 95
let arith_meta = register_meta "gappa arith"
  [MTlsymbol;MTstring;MTstring;MTstring]
Andrei Paskevich's avatar
Andrei Paskevich committed
96 97 98 99 100 101 102 103
  ~desc:"Specify@ how@ to@ pretty-print@ arithmetic@ \
          operations@ in@ the@ Gappa@ format:@\n  \
    @[\
     @[<hov 2>- first@ argument:@ the@ symbol@]@\n\
     @[<hov 2>- second@ argument:@ the@ prefix@ to@ put@ before@ the@ term@]@\n\
     @[<hov 2>- third@ argument:@ the@ operator@ to@ print@]@\n\
     @[<hov 2>- fourth@ argument:@ the@ inverse@ operator@]\
    @]"
104

105
let find_th env file th =
106
  let theory = Env.read_theory env [file] th in
107 108
  fun id -> Theory.ns_find_ls theory.Theory.th_export [id]

109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
let get_info env task =
  (* unary minus for constants *)
  int_minus := find_th env "int" "Int" "prefix -";
  real_minus := find_th env "real" "Real" "prefix -";
  (* handling of inequalities *)
  let ops = on_meta arith_meta (fun acc meta_arg ->
    match meta_arg with
    | [MAls ls; MAstr s; MAstr op; MAstr rev_op] ->
        Mls.add ls (s,op,rev_op) acc
    | _ -> assert false) Mls.empty task in
  (* sets of known symbols *)
  let syn = get_syntax_map task in
  let symb = Mid.map (Util.const ()) syn in
  let symb = Mls.fold (fun ls _ acc -> Sid.add ls.ls_name acc) ops symb in
  let symb = Sid.add ps_equ.ls_name symb in
  {
125
    info_env = env;
126 127 128 129
    info_symbols = symb;
    info_ops_of_rel = ops;
    info_syn = syn;
  }
130 131

(* Gappa printing *)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
132

133
let ident_printer =
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
134
  let bls = [
135 136 137 138 139
      "sqrt"; "fma";
      "float"; "fixed"; "int";
      "homogen80x"; "homogen80x_init"; "float80x";
      "add_rel"; "sub_rel"; "mul_rel"; "fma_rel";
    ] in
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
140 141 142 143 144 145
  let san = sanitizer char_to_alpha char_to_alnumus in
  create_ident_printer bls ~sanitizer:san

let print_ident fmt id =
  fprintf fmt "%s" (id_unique ident_printer id)

146 147
let number_format = {
    Number.long_int_support = true;
148
    Number.extra_leading_zeros_support = true;
149 150 151 152 153 154 155 156 157 158 159 160 161
    Number.dec_int_support = Number.Number_default;
    Number.hex_int_support = Number.Number_default;
    Number.oct_int_support = Number.Number_unsupported;
    Number.bin_int_support = Number.Number_unsupported;
    Number.def_int_support = Number.Number_unsupported;
    Number.dec_real_support = Number.Number_default;
    Number.hex_real_support = Number.Number_default;
    Number.frac_real_support = Number.Number_unsupported;
    Number.def_real_support = Number.Number_unsupported;
  }

let constant_value t =
  match t.t_node with
162
    | Tconst c ->
163
        fprintf str_formatter "%a" (Number.print number_format) c;
164
        flush_str_formatter ()
165 166
    | Tapp(ls, [{ t_node = Tconst c}])
        when ls_equal ls !int_minus || ls_equal ls !real_minus ->
167
        fprintf str_formatter "-%a" (Number.print number_format) c;
168
        flush_str_formatter ()
169
    | _ -> raise Not_found
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
170

171
(* terms *)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
172

173
let rec print_term info fmt t =
MARCHE Claude's avatar
MARCHE Claude committed
174 175
  let term = print_term info in
  match t.t_node with
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
176
  | Tconst c ->
177
      fprintf fmt "%a" (Number.print number_format) c
178
  | Tvar { vs_name = id } ->
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
179
      print_ident fmt id
180 181 182 183 184
  | Tapp ( { ls_name = id } ,[] ) ->
    begin match query_syntax info.info_syn id with
      | Some s -> syntax_arguments s term fmt []
      | None -> print_ident fmt id
    end
185
  | Tapp (ls, tl) ->
MARCHE Claude's avatar
MARCHE Claude committed
186
      begin match query_syntax info.info_syn ls.ls_name with
187 188 189
        | Some s -> syntax_arguments s term fmt tl
        | None ->
            unsupportedTerm t
MARCHE Claude's avatar
MARCHE Claude committed
190 191
              ("gappa: function '" ^ ls.ls_name.id_string ^ "' is not supported")
      end
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
192
  | Tlet _ -> unsupportedTerm t
193
      "gappa: you must eliminate let in term"
194
  | Tif _ -> unsupportedTerm t
195
      "gappa: you must eliminate if_then_else"
196
  | Tcase _ -> unsupportedTerm t
197
      "gappa: you must eliminate match"
198
  | Teps _ -> unsupportedTerm t
199
      "gappa : you must eliminate epsilon"
200
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
201 202


203 204
(* predicates *)

205 206 207 208 209 210 211 212 213 214 215
let rel_error_pat =
  PatApp (["real"], "Real", ["infix <="], [
    PatApp (["real"], "Abs", ["abs"], [
      PatApp (["real"], "Real", ["infix -"], [
        PatHole 0;
        PatHole 1])]);
    PatApp (["real"], "Real", ["infix *"], [
      PatHole 2;
        PatApp (["real"], "Abs", ["abs"], [
          PatHole 1])])])

216
let rec print_fmla info fmt f =
MARCHE Claude's avatar
MARCHE Claude committed
217 218
  let term = print_term info in
  let fmla = print_fmla info in
219 220
  match f.t_node with
  | Tapp ({ ls_name = id }, []) ->
221 222
    begin match query_syntax info.info_syn id with
      | Some s -> syntax_arguments s term fmt []
223
      | None -> fprintf fmt "%a in [0,0]" print_ident id
224
    end
225
  | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
226
      (* TODO: distinguish between type of t1 and t2
227 228
         the following is OK only for real of integer
      *)
229 230
      begin try
        let c1 = constant_value t1 in
231
        fprintf fmt "%a in [%s,%s]" term t2 c1 c1
232 233 234
      with Not_found ->
        try
          let c2 = constant_value t2 in
235
          fprintf fmt "%a in [%s,%s]" term t1 c2 c2
236
        with Not_found ->
237
          fprintf fmt "%a - %a in [0,0]" term t1 term t2
MARCHE Claude's avatar
MARCHE Claude committed
238
      end
239
  | Tapp (ls, [t1;t2]) when Mls.mem ls info.info_ops_of_rel ->
240
      let s,op,rev_op = try Mls.find ls info.info_ops_of_rel
241
        with Not_found -> assert false
MARCHE Claude's avatar
MARCHE Claude committed
242
      in
MARCHE Claude's avatar
MARCHE Claude committed
243
      begin try
244 245 246 247
        let t = pat_match info.info_env 3 rel_error_pat f in
        let c = constant_value t.(2) in
        fprintf fmt "|%a -/ %a| <= %s" term t.(0) term t.(1) c
      with Not_found -> try
MARCHE Claude's avatar
MARCHE Claude committed
248
        let c1 = constant_value t1 in
249
        fprintf fmt "%s%a %s %s" s term t2 rev_op c1
MARCHE Claude's avatar
MARCHE Claude committed
250 251 252
      with Not_found ->
        try
          let c2 = constant_value t2 in
253
          fprintf fmt "%s%a %s %s" s term t1 op c2
MARCHE Claude's avatar
MARCHE Claude committed
254
        with Not_found ->
255
          fprintf fmt "%s%a - %a %s 0" s term t1 term t2 op
MARCHE Claude's avatar
MARCHE Claude committed
256
      end
257
  | Tapp (ls, tl) ->
MARCHE Claude's avatar
MARCHE Claude committed
258
      begin match query_syntax info.info_syn ls.ls_name with
259 260 261
        | Some s -> syntax_arguments s term fmt tl
        | None ->
            unsupportedTerm f
MARCHE Claude's avatar
MARCHE Claude committed
262
              ("gappa: predicate '" ^ ls.ls_name.id_string ^ "' is not supported")
263
      end
264 265
  | Tquant (_q, _fq) ->
      unsupportedTerm f
266
        "gappa: quantifiers are not supported"
267
(*
268 269
      let q = match q with Tforall -> "forall" | Texists -> "exists" in
      let vl, tl, f = t_open_quant fq in
270
      let forall fmt v =
271
        fprintf fmt "%s %a:%a" q print_ident v.vs_name (print_type info) v.vs_ty
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
272 273
      in
      fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
274
        (print_triggers info) tl (print_fmla info) f;
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
275
      List.iter forget_var vl
276
*)
277
  | Tbinop (Tand, f1, f2) ->
MARCHE Claude's avatar
MARCHE Claude committed
278
      fprintf fmt "(%a /\\@ %a)" fmla f1 fmla f2
279
  | Tbinop (Tor, f1, f2) ->
MARCHE Claude's avatar
MARCHE Claude committed
280
      fprintf fmt "(%a \\/@ %a)" fmla f1 fmla f2
281
  | Tbinop (Timplies, f1, f2) ->
MARCHE Claude's avatar
MARCHE Claude committed
282
      fprintf fmt "(%a ->@ %a)" fmla f1 fmla f2
283 284
  | Tbinop (Tiff, _f1, _f2) ->
      unsupportedTerm f
285
        "gappa: connector <-> is not supported"
286
  | Tnot f ->
MARCHE Claude's avatar
MARCHE Claude committed
287
      fprintf fmt "not %a" fmla f
288
  | Ttrue ->
289
      fprintf fmt "(0 in [0,0])"
290
  | Tfalse ->
291
      fprintf fmt "(1 in [0,0])"
292
  | Tif (_f1, _f2, _f3) ->
293
      unsupportedTerm f
294
        "gappa: you must eliminate if in formula"
295
  | Tlet _ -> unsupportedTerm f
296
      "gappa: you must eliminate let in formula"
297
  | Tcase _ -> unsupportedTerm f
298
      "gappa: you must eliminate match"
299
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
300

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
301
(*
302
let print_decl (* ?old *) info fmt d =
303 304
  match d.d_node with
  | Dtype _ -> ()
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
305
(*
306
unsupportedDecl d
307
      "gappa : type declarations are not supported"
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
308
*)
309
  | Dlogic _ -> ()
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
310
(*
311
unsupportedDecl d
312
      "gappa : logic declarations are not supported"
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
313
*)
314
  | Dind _ -> unsupportedDecl d
315
      "gappa: inductive definitions are not supported"
316
  | Dprop (Paxiom, pr, f) ->
MARCHE Claude's avatar
MARCHE Claude committed
317
      fprintf fmt "# hypothesis '%a'@\n" print_ident pr.pr_name;
318
      fprintf fmt "@[<hv 2>%a ->@]@\n" (print_fmla info) f
319 320
  | Dprop (Pgoal, pr, f) ->
      fprintf fmt "# goal '%a'@\n" print_ident pr.pr_name;
321
(*
MARCHE Claude's avatar
MARCHE Claude committed
322
      fprintf fmt "@[<hv 2>{ %a@ }@]@\n" (print_fmla info) f
323 324
*)
      fprintf fmt "@[<hv 2>%a@]@\n" (print_fmla info) f
325
  | Dprop ((Plemma|Pskip), _, _) ->
326
      unsupportedDecl d
327
        "gappa: lemmas are not supported"
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
328
*)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
329

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
330
(*
331
let print_decl ?old:_ info fmt =
MARCHE Claude's avatar
MARCHE Claude committed
332
  catch_unsupportedDecl (print_decl (* ?old *) info fmt)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
333

MARCHE Claude's avatar
MARCHE Claude committed
334
let print_decls ?old info fmt dl =
335
  fprintf fmt "@[<hov>{ %a }@\n@]" (print_list nothing (print_decl ?old info)) dl
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
336
*)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
337

338 339
exception AlreadyDefined

340
let rec filter_hyp info defs eqs hyps pr f =
341
  match f.t_node with
342
  | Tapp(ls,[t1;t2]) when ls_equal ls ps_equ ->
343 344 345 346
      let try_equality t1 t2 =
        match t1.t_node with
          | Tapp(l,[]) ->
              if Hid.mem defs l.ls_name then raise AlreadyDefined;
347 348
              if t_s_any (fun _ -> false) (fun ls -> ls_equal ls l) t2
              then raise AlreadyDefined;
349
              Hid.add defs l.ls_name ();
350 351
              t_s_fold (fun _ _ -> ())
                (fun _ ls -> Hid.replace defs ls.ls_name ()) () t2;
352 353 354 355 356 357 358 359 360
              ((pr,t1,t2)::eqs, hyps)
          | _ -> raise AlreadyDefined in
      begin try
        try_equality t1 t2
      with AlreadyDefined -> try
        try_equality t2 t1
      with AlreadyDefined ->
        (eqs, (pr,f)::hyps)
      end
361 362 363 364 365 366 367 368 369 370
  | Tbinop (Tand, f1, f2) ->
      let (eqs,hyps) = filter_hyp info defs eqs hyps pr f2 in
      filter_hyp info defs eqs hyps pr f1
  | Tapp(_,[]) ->
      (* Discard (abstracted) predicate variables.
         While Gappa would handle them, it is usually just noise from
         Gappa's point of view and better delegated to a SAT solver. *)
      (eqs,hyps)
  | Ttrue -> (eqs,hyps)
  | _ -> (eqs, (pr,f)::hyps)
MARCHE Claude's avatar
MARCHE Claude committed
371

MARCHE Claude's avatar
MARCHE Claude committed
372
type filter_goal =
373
  | Goal_good of Decl.prsymbol * term
MARCHE Claude's avatar
MARCHE Claude committed
374 375 376
  | Goal_bad of string
  | Goal_none

MARCHE Claude's avatar
MARCHE Claude committed
377
let filter_goal pr f =
378 379
  match f.t_node with
    | Tapp(ps,[]) -> Goal_bad ("symbol " ^ ps.ls_name.Ident.id_string ^ " unknown")
380
        (* todo: filter more goals *)
MARCHE Claude's avatar
MARCHE Claude committed
381
    | _ -> Goal_good(pr,f)
382

383
let prepare info defs ((eqs,hyps,goal) as acc) d =
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
384
  match d.d_node with
385 386
    | Dtype _ | Ddata _ -> acc
    | Dparam _ | Dlogic _ -> acc
387
    | Dind _ ->
388 389
        unsupportedDecl d
          "please remove inductive definitions before calling gappa printer"
390
    | Dprop (Paxiom, pr, f) ->
391
        let (eqs,hyps) = filter_hyp info defs eqs hyps pr f in (eqs,hyps,goal)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
392
    | Dprop (Pgoal, pr, f) ->
393 394 395 396 397
        begin
          match goal with
            | Goal_none -> (eqs,hyps,filter_goal pr f)
            | _ -> assert false
        end
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
398
    | Dprop ((Plemma|Pskip), _, _) ->
399
        unsupportedDecl d
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
400 401
          "gappa: lemmas are not supported"

402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418
let find_used_equations eqs hyps goal =
  let used = Hid.create 17 in
  let mark_used f =
    t_s_fold (fun _ _ -> ()) (fun _ ls -> Hid.replace used ls.ls_name ()) () f in
  begin match goal with
  | Goal_good (_,f) -> mark_used f;
  | _ -> ()
  end;
  List.iter (fun (_,f) -> mark_used f) hyps;
  List.fold_left (fun acc ((_, v, t) as eq) ->
    let v = match v.t_node with Tapp (l,[]) -> l.ls_name | _ -> assert false in
    if Hid.mem used v then begin
      mark_used t;
      eq :: acc
    end else acc
  ) [] eqs

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
419 420 421
let print_equation info fmt (pr,t1,t2) =
  fprintf fmt "# equation '%a'@\n" print_ident pr.pr_name;
  fprintf fmt "%a = %a ;@\n" (print_term info) t1 (print_term info) t2
422

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
423 424
let print_hyp info fmt (pr,f) =
  fprintf fmt "# hypothesis '%a'@\n" print_ident pr.pr_name;
MARCHE Claude's avatar
MARCHE Claude committed
425
  fprintf fmt "%a ->@\n" (print_fmla info) f
426

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
427 428
let print_goal info fmt g =
  match g with
MARCHE Claude's avatar
MARCHE Claude committed
429
    | Goal_good(pr,f) ->
430 431
        fprintf fmt "# goal '%a'@\n" print_ident pr.pr_name;
        fprintf fmt "%a@\n" (print_fmla info) f
432
    | Goal_bad msg ->
433 434
        fprintf fmt "# (unsupported kind of goal: %s)@\n" msg;
        fprintf fmt "1 in [0,0]@\n"
435
    | Goal_none ->
436 437
        fprintf fmt "# (no goal at all ??)@\n";
        fprintf fmt "1 in [0,0]@\n"
438

439
let print_task args ?old:_ fmt task =
MARCHE Claude's avatar
MARCHE Claude committed
440
  forget_all ident_printer;
441 442 443
  let info = get_info args.env task in
  print_prelude fmt args.prelude;
  print_th_prelude task fmt args.th_prelude;
444
  let equations,hyps,goal =
445
    List.fold_left (prepare info (Hid.create 17)) ([],[],Goal_none) (Task.task_decls task)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
446
  in
447
  List.iter (print_equation info fmt) (find_used_equations equations hyps goal);
448
  fprintf fmt "@[<v 2>{ %a%a}@\n@]" (print_list nothing (print_hyp info)) (List.rev hyps)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
449
    (print_goal info) goal
450
(*
MARCHE Claude's avatar
MARCHE Claude committed
451
  print_decls ?old info fmt (Task.task_decls task)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
452
*)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
453

454
let () = register_printer "gappa" print_task
455 456
  ~desc:"Printer@ for@ the@ Gappa@ theorem@ prover@ specialized@ in@ \
         floating@ point@ reasoning."
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
457 458 459 460 461 462

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
End:
*)