gappa.ml 24.3 KB
Newer Older
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

20
(*
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211
open Register
open Format
open Pp
open Ident
open Ty
open Term
open Decl
open Task


(* Gappa terms and formulas *)

(* fields of the float model *)
type float_field = Rounded | Exact | Model
(* formats of the float model *)
type float_fmt = Int | Single | Double | Binary80
(* modes of the float model *)
type mode = RndNE | RndZR | RndUP | RndDN | RndNA

type gterm =
  | Gvar of string
  | Gfld of float_field * string
  | Grnd of float_fmt * mode * gterm
  | Gcst of string
  | Gsqrt of gterm
  | Gneg of gterm
  | Gadd of gterm * gterm
  | Gsub of gterm * gterm
  | Gmul of gterm * gterm
  | Gdiv of gterm * gterm
  | Gabs of gterm

type gpred =
  | Gle of gterm * string
  | Gge of gterm * string
  | Gin of gterm * string * string
  | Grel of gterm * gterm * string
  | Gimplies of gpred * gpred
  | Gand of gpred * gpred
  | Gor of gpred * gpred
  | Gnot of gpred

type gobligation = (string * gterm) list * gpred



(* contains the roundings used *)
let rnd_table = Hashtbl.create 10



let get_format = function
  | Single -> "ieee_32"
  | Double -> "ieee_64"
  | Binary80 -> "x86_80"
  | Int -> "int"

let get_mode = function
  | RndNE -> "ne"
  | RndZR -> "zr"
  | RndUP -> "up"
  | RndDN -> "dn"
  | RndNA -> "na"

let rec print_term fmt = function
  | Gvar x -> fprintf fmt "%s" x
  | Gfld (Rounded, x) -> fprintf fmt "float_%s" x
  | Gfld (Exact,   x) -> fprintf fmt "exact_%s" x
  | Gfld (Model,   x) -> fprintf fmt "model_%s" x
  | Grnd (f, m, t) -> 
      fprintf fmt "rnd_%s%s(%a)" (get_format f) (get_mode m) print_term t
  | Gcst c -> fprintf fmt "%s" c
  | Gneg t -> fprintf fmt "(-%a)" print_term t
  | Gadd (t1, t2) -> fprintf fmt "(%a + %a)" print_term t1 print_term t2
  | Gsub (t1, t2) -> fprintf fmt "(%a - %a)" print_term t1 print_term t2
  | Gmul (t1, t2) -> fprintf fmt "(%a * %a)" print_term t1 print_term t2
  | Gdiv (t1, t2) -> fprintf fmt "(%a / %a)" print_term t1 print_term t2
  | Gabs t -> fprintf fmt "|%a|" print_term t
  | Gsqrt t -> fprintf fmt "sqrt(%a)" print_term t

let rec print_pred_atom fmt = function
  | Gle (t, r1) ->
      fprintf fmt "%a <= %s" print_term t r1
  | Gge (t, r1) ->
      fprintf fmt "%a >= %s" print_term t r1
  | Gin (t, r1, r2) ->
      fprintf fmt "%a in [%s, %s]" print_term t r1 r2
  | Grel (t1, t2, r1) ->
      fprintf fmt "|%a -/ %a| <= %s" print_term t1 print_term t2 r1
  | Gnot p ->
      fprintf fmt "not %a" print_pred_atom p
  | _ as p ->
      fprintf fmt "(%a)" print_pred p
and print_pred_left fmt = function
  | Gand (p1, p2) ->
      fprintf fmt "@[%a /\\@ %a@]" print_pred_atom p1 print_pred_atom p2
  | Gor (p1, p2) ->
      fprintf fmt "@[%a \\/@ %a@]" print_pred_atom p1 print_pred_atom p2
  | _ as p ->
      print_pred_atom fmt p
and print_pred fmt = function
  | Gimplies (p1, p2) ->
      fprintf fmt "@[%a ->@ %a@]" print_pred_left p1 print_pred p2
  | _ as p ->
      print_pred_left fmt p

let print_equation fmt (e, x, t) =
  let e =
    match e with
    | Rounded -> "float_"
    | Exact -> "exact_"
    | Model -> "model_" in
  fprintf fmt "@[%s%s = %a;@]" e x print_term t

let print_obligation fmt (eq,p) =
  Hashtbl.iter 
    (fun (f, m) () ->
       let m = get_mode m in
       match f with 
         | Int ->
             fprintf fmt "@@rnd_int%s = int<%s>;@\n" m m 
         | _ ->
             let f = get_format f in
             fprintf fmt "@@rnd_%s%s = float<%s, %s>;@\n" f m f m) 
    rnd_table;
  fprintf fmt "@\n%a@\n@\n" (print_list newline print_equation) eq;
  fprintf fmt "{ @[%a@] }@." print_pred p

(*
let print_file fmt = Queue.iter (print_obligation fmt) queue

let output_one_file ~allowedit file =
  if allowedit then
    begin
      let sep = "### DO NOT EDIT ABOVE THIS LINE" in
      do_not_edit_above ~file
	~before:print_file
	~sep
	~after:(fun _fmt -> ())
    end
  else
      print_in_file print_file file

let output_file fwe =
  let sep = "### DO NOT EDIT ABOVE THIS LINE" in
  let i = ref 0 in
  Queue.iter
    (fun o ->
       incr i;
       if debug then eprintf "gappa obligation %d@." !i;
       let file = fwe ^ "_why_po_" ^ string_of_int !i ^ ".gappa" in
       do_not_edit_above ~file
	 ~before:(fun fmt -> print_obligation fmt o)
	 ~sep
	 ~after:(fun _fmt -> ()))
    queue
*)



(* compilation to Gappa formulas *)

exception NotGappa

(* TODO: comment faire une table de hash indexée par des termes ? *)
(* 

module Termtbl = Hashtbl.Make(HashedTerm)

(* contains all the terms that have been generalized away,
   because they were not recognized *)
let gen_table = Termtbl.create 10

(* contains the terms associated to variables, especially gen_float variables *)
let var_table = Hashtbl.create 10

(* contains the names already defined,
   so new definitions should be as equalities *)
let def_table = Hashtbl.create 10

(* contains the reverted list of aliases from def_table *)
let def_list = ref []

(* contains the list of format-implied bounds on float variables *)
let bnd_list = ref []






MARCHE Claude's avatar
gappa  
MARCHE Claude committed
212
*)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
213

MARCHE Claude's avatar
MARCHE Claude committed
214 215 216 217 218 219 220 221 222 223 224
let prelude_to_load = ref true

let dummy_symbol = (Obj.magic 0 : Term.lsymbol)

let symbol_le_int = ref dummy_symbol
let symbol_le_real = ref dummy_symbol
let symbol_ge_int = ref dummy_symbol
let symbol_ge_real = ref dummy_symbol

let symbol_add_int = ref dummy_symbol

225
let load_prelude (info : Driver.driver_query) =
MARCHE Claude's avatar
MARCHE Claude committed
226 227
  if !prelude_to_load then
    begin
228
      let env = Driver.query_env info in
MARCHE Claude's avatar
MARCHE Claude committed
229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281
      let int_theory = Env.find_theory env ["int"] "Int" in
      let real_theory = Env.find_theory env ["real"] "Real" in
      symbol_le_int := 
        Theory.ns_find_ls int_theory.Theory.th_export ["infix <="];
      symbol_le_real := 
        Theory.ns_find_ls real_theory.Theory.th_export ["infix <="];
      symbol_ge_int := 
        Theory.ns_find_ls int_theory.Theory.th_export ["infix >="];
      symbol_ge_real := 
        Theory.ns_find_ls real_theory.Theory.th_export ["infix >="];
      symbol_add_int := 
        Theory.ns_find_ls int_theory.Theory.th_export ["infix +"];
      prelude_to_load := false;
    end


(* true when id is <= on R or Z *)
let is_le_num id = 
  ls_equal id !symbol_le_int
  || ls_equal id !symbol_le_real

(* true when id is >= on R or Z *)
let is_ge_num id = 
  ls_equal id !symbol_ge_int
  || ls_equal id !symbol_ge_real

(* true when id is = *)
let is_eq id = ls_equal id Term.ps_equ

(* true when id is <> *)
let is_neq id = ls_equal id Term.ps_neq


let eval_constant c = 
  match c with
    | ConstInt s -> s
    | ConstReal(RConstDecimal(_e,_f,_exp)) -> assert false 
    | ConstReal(RConstHexa(_e,_f,_exp)) -> assert false

let rec term t = 
  match t.t_node with
    | Tconst c -> Gcst (eval_constant c)
    | Tbvar _n -> assert false
    | Tvar _v -> assert false
    | Tapp(f,[t1;t2]) when ls_equal f !symbol_add_int -> 
        Gadd (term t1, term t2)
          (* TODO: neg, abs, + real, - , * , /, real_of_int,
             etc. *)
    | Tapp(_,_) -> raise NotGappa        
    | Tif(_f,_t1,_t2) -> assert false
    | Tlet(_t,_tb) -> assert false
    | Tcase(_tl,_tbl) -> assert false
    | Teps _fb -> assert false
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
282 283
(*
function
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376
  | t when is_constant t ->
      Gcst (eval_constant t)
  | Tconst _ ->
      raise NotGappa
  | Tvar id ->
      Gvar (Ident.string id)
  | Tderef id ->
      Gvar (Ident.string id)
  (* int and real ops *)
  | Tapp (id, [t], _) when id == t_neg_real || id = t_neg_int ->
      Gneg (term t)
  | Tapp (id, [t], _) when id == t_abs_real || id == t_abs_int ->
      Gabs (term t)
  | Tapp (id, [t], _) when id == t_sqrt_real ->
      Gsqrt (term t)
  | Tapp (id, [t1; t2], _) when id == t_add_real || id = t_add_int ->
      Gadd (term t1, term t2)
  | Tapp (id, [t1; t2], _) when id == t_sub_real || id = t_sub_int ->
      Gsub (term t1, term t2)
  | Tapp (id, [t1; t2], _) when id == t_mul_real || id = t_mul_int ->
      Gmul (term t1, term t2)
  | Tapp (id, [t1; t2], _) when id == t_div_real ->
      Gdiv (term t1, term t2)
  (* conversion int -> real *)
  | Tapp (id, [t], _) when id == real_of_int ->
      term t
  (* conversion real -> int by truncate, i.e. towards zero *)
  | Tapp (id, [t], _) when id == truncate_real_to_int ->
      let mode = RndZR in
      Hashtbl.replace rnd_table (Int, mode) ();
      Grnd (Int, mode, term t)

  (* [Jessie] rounding *)
  | Tapp (id, [Tapp (m, [], _); t], _)
      when id == round_single ->
      let mode = mode_of_id m in
      Hashtbl.replace rnd_table (Single, mode) ();
      Grnd (Single, mode, term t)
  | Tapp (id, [Tapp (m, [], _); t], _)
      when id == round_double ->
      let mode = mode_of_id m in
      Hashtbl.replace rnd_table (Double, mode) ();
      Grnd (Double, mode, term t)

  | Tapp (id1, [Tapp (id2, l1, l2)], _)
      when id1 == single_value && id2 == round_single_logic ->
      term (Tapp (round_single, l1, l2))
  | Tapp (id1, [Tapp (id2, l1, l2)], _)
      when id1 == double_value && id2 == round_double_logic ->
      term (Tapp (round_double, l1, l2))

  (* casts *)
  | Tapp (id1, [Tapp (id2,[Tapp (m, [], _); t] , l2)], _)  
      when id1 == single_value && id2 == double_to_single ->
      let mode = mode_of_id m in
      Hashtbl.replace rnd_table (Single, mode) ();
      Grnd (Single, mode, term (Tapp (double_value,[t],l2)))

  | Tapp (id1, [Tapp (id2,[Tapp (_m, [], _); t] , l2)], _)  
      when id1 == double_value && id2 == single_to_double ->
        term (Tapp (single_value,[t],l2))


  | Tapp (id, [t], _)
      when (id == single_value || id == double_value || id == single_exact 
         || id == double_exact || id == single_model || id == double_model) ->
      let v = create_var t in
      let f = field_of_id id in
      let add_def fmt =
        if not (Hashtbl.mem def_table (f, v)) then begin
          Hashtbl.add def_table (f, v) ();
          Hashtbl.replace rnd_table (fmt, RndNE) ();
          def_list := (f, v, Grnd (fmt, RndNE, Gvar ("dummy_float_" ^ v))) :: !def_list;
          let b =
            if fmt = Single then "0x1.FFFFFEp127" else
            if fmt = Double then "0x1.FFFFFFFFFFFFFp1023" else
            assert false in
          bnd_list := Gin (Gfld (f, v), "-"^b, b) :: !bnd_list
        end in
      if id == single_value then add_def Single else
      if id == double_value then add_def Double;
      Gfld (f, v)

  | Tapp (id, [t], _) 
    when id == single_round_error || id == double_round_error ->
    let v = create_var t in
    Gabs (Gsub (Gfld (Rounded, v), Gfld (Exact, v)))

  | Tnamed(_,t) -> term t

  (* anything else is generalized as a fresh variable *)
  | Tapp _ as t ->
      Gvar (create_var t)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
377
*)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
378 379


MARCHE Claude's avatar
gappa  
MARCHE Claude committed
380
(*
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402

let ident_printer = 
  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
  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)

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

let forget_var v = forget_id ident_printer v.vs_name

403
type info = {
Andrei Paskevich's avatar
Andrei Paskevich committed
404
  info_syn : string Mid.t;
405 406 407 408
  info_rem : Sid.t;
}

let rec print_type info fmt ty = match ty.ty_node with
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
409 410
  | Tyvar id -> 
      print_tvsymbols fmt id
411
  | Tyapp (ts, tl) -> begin match query_syntax info.info_sym ts.ts_name with
412 413
      | Some s -> syntax_arguments s (print_type info) fmt tl
      | None -> fprintf fmt "%a%a" (print_tyapp info) tl print_ident ts.ts_name
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
414 415
    end

416
and print_tyapp info fmt = function
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
417
  | [] -> ()
418 419
  | [ty] -> fprintf fmt "%a " (print_type info) ty
  | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
420

421
let rec print_term info fmt t = match t.t_node with
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
422 423 424 425 426 427
  | Tbvar _ -> 
      assert false
  | Tconst c ->
      Pretty.print_const fmt c
  | Tvar { vs_name = id } ->
      print_ident fmt id
428
  | Tapp (ls, tl) -> begin match query_syntax info.info_sym ls.ls_name with
429 430
      | Some s -> syntax_arguments s (print_term info) fmt tl
      | None -> fprintf fmt "%a%a" print_ident ls.ls_name (print_tapp info) tl
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
431 432 433 434 435 436 437 438 439 440
    end
  | Tlet _ -> unsupportedTerm t
      "alt-ergo : you must eliminate let in term"
  | Tif _ -> unsupportedTerm t 
      "alt-ergo : you must eliminate if_then_else"
  | Tcase _ -> unsupportedTerm t 
      "alt-ergo : you must eliminate match"
  | Teps _ -> unsupportedTerm t 
      "alt-ergo : you must eliminate epsilon"

441
and print_tapp info fmt = function
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
442
  | [] -> ()
443
  | tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
444

445
let rec print_fmla info fmt f = match f.f_node with
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
446 447
  | Fapp ({ ls_name = id }, []) ->
      print_ident fmt id
448
  | Fapp (ls, tl) -> begin match query_syntax info.info_sym ls.ls_name with
449
      | Some s -> syntax_arguments s (print_term info) fmt tl
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
450
      | None -> fprintf fmt "%a(%a)" print_ident ls.ls_name 
451
                    (print_list comma (print_term info)) tl
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
452 453 454 455 456
    end
  | Fquant (q, fq) ->
      let q = match q with Fforall -> "forall" | Fexists -> "exists" in
      let vl, tl, f = f_open_quant fq in
      let forall fmt v = 
457
	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
458 459
      in
      fprintf fmt "@[(%a%a.@ %a)@]" (print_list dot forall) vl
460
        (print_triggers info) tl (print_fmla info) f;
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
461 462
      List.iter forget_var vl
  | Fbinop (Fand, f1, f2) ->
463
      fprintf fmt "(%a and@ %a)" (print_fmla info) f1 (print_fmla info) f2
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
464
  | Fbinop (For, f1, f2) ->
465
      fprintf fmt "(%a or@ %a)" (print_fmla info) f1 (print_fmla info) f2
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
466
  | Fbinop (Fimplies, f1, f2) ->
467
      fprintf fmt "(%a ->@ %a)" (print_fmla info) f1 (print_fmla info) f2
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
468
  | Fbinop (Fiff, f1, f2) ->
469
      fprintf fmt "(%a <->@ %a)" (print_fmla info) f1 (print_fmla info) f2
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
470
  | Fnot f ->
471
      fprintf fmt "(not %a)" (print_fmla info) f
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
472 473 474 475 476 477
  | Ftrue ->
      fprintf fmt "true"
  | Ffalse ->
      fprintf fmt "false"
  | Fif (f1, f2, f3) ->
      fprintf fmt "((%a and %a) or (not %a and %a))"
478 479
	(print_fmla info) f1 (print_fmla info) f2 (print_fmla info)
        f1 (print_fmla info) f3
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
480 481 482 483 484 485
  | Flet _ -> unsupportedFmla f
      "alt-ergo : you must eliminate let in formula"
  | Fcase _ -> unsupportedFmla f 
      "alt-ergo : you must eliminate match"
  

486
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
487

488
and print_triggers info fmt tl =
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
489 490 491 492 493 494 495
  let filter = function 
    | Term _ | Fmla {f_node = Fapp _} -> true
    | _ -> false in
  let tl = List.map (List.filter filter)
    tl in
  let tl = List.filter (function [] -> false | _::_ -> true) tl in
  if tl = [] then () else fprintf fmt "@ [%a]"
496
    (print_list alt (print_list comma (print_expr info))) tl
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
497

498 499
let print_logic_binder info fmt v =
  fprintf fmt "%a: %a" print_ident v.vs_name (print_type info) v.vs_ty
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
500 501 502 503 504 505

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

506 507
let print_type_decl info fmt = function
  | ts, Tabstract when Sid.mem ts.ts_name info.info_rem -> false
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
508 509 510 511 512 513
  | ts, Tabstract -> print_type_decl fmt ts; true
  | _, Talgebraic _ -> unsupported 
      "alt-ergo : algebraic datatype are not supported"

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

514 515
let print_logic_decl info fmt (ls,ld) =
  let tags = Driver.query_tags info ls.ls_name in
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
516 517 518 519 520
  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
521
          (print_list comma (print_type info)) ls.ls_args 
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
522
          (if ls.ls_args = [] then "" else " -> ")
523
          (print_option_or_default "prop" (print_type info)) ls.ls_value
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
524 525 526 527 528 529 530
    | 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
531 532 533
                (print_list comma (print_logic_binder info)) vl 
                (print_type info) (Util.of_option ls.ls_value) 
                (print_term info) t
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
534 535 536
          | Fmla f ->
              fprintf fmt "@[<hov 2>predicate %a(%a) =@ %a@]"
                print_ident ls.ls_name 
537 538
                (print_list comma (print_logic_binder info)) vl 
                (print_fmla info) f
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
539 540 541
        end;
        List.iter forget_var vl

542 543 544
let print_logic_decl info fmt d =
  if Sid.mem (fst d).ls_name info.info_rem then
    false else (print_logic_decl info fmt d; true)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
545

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700
*)

let gando = function
  | Some p1, Some p2 -> Some (Gand (p1, p2))
  | (Some _ as v), None | None, (Some _ as v) -> v
  | None, None -> None

(* recognition of a Gappa predicate *)

let rec gpred def f =
  match f.f_node with
  | Fapp (id, [t1; t2]) when is_le_num id ->
      begin 
	match term t1, term t2 with
	  | (Gcst c1), t2 -> Gge (t2, c1)
	  | t1, (Gcst c2) -> Gle (t1, c2)
          | t1, t2 -> Gle (Gsub (t1, t2), "0")
      end
  | Fapp (id, [t1; t2]) when is_ge_num id ->
      begin 
	match term t1, term t2 with
	| (Gcst c1), t2 -> Gle (t2, c1)
	| t1, (Gcst c2) -> Gge (t1, c2)
        | t1, t2 -> Gge (Gsub (t1, t2), "0")
      end
(*
  | Fbinop(Fand, ...(_, _, Papp (id1, [f1; t1], _), Papp (id2, [t2; f2], _))
    when (id1 == t_le_real || id1 == t_le_int) && (id2 == t_le_real || id2 == t_le_int)
    && t1 = t2 && is_constant f1 && is_constant f2 ->
    begin 
      try Some (Gin (term t1, eval_constant f1, eval_constant f2))
      with NotGappa -> None
    end
*)
  | Fapp (id, [t1; t2]) when is_eq id ->
      begin 
	match term t1, term t2 with
          | (Gcst c1), t2 -> Gin (t2, c1, c1)
          | t1, (Gcst c2) -> Gin (t1, c2, c2)
          | t1, t2 -> Gin (Gsub (t1, t2), "0", "0")
      end
  | Fapp (id, [t1; t2]) when is_neq id ->
      begin 
	match term t1, term t2 with
        | (Gcst c1), t2 -> Gnot (Gin (t2, c1, c1))
        | t1, (Gcst c2) -> Gnot (Gin (t1, c2, c2))
        | t1, t2 -> Gnot (Gin (Gsub (t1, t2), "0", "0"))
      end
  | Fbinop(Fand, p1, p2) ->
      begin 
	try
	  let p1 = gpred def p1 in
	    try
	      let p2 = gpred def p2 in
		Gand (p1, p2)
	    with NotGappa -> if def then p1 else raise NotGappa
	with NotGappa ->
	  if def then gpred def p2 else raise NotGappa
      end
(*
  | Fbinop(For, p1, p2) ->
      begin match gpred def p1, gpred def p2 with
        | Some p1, Some p2 -> Some (Gor (p1, p2))
        | (Some _ as p1), None when def = false -> p1
        | None, (Some _ as p2) when def = false -> p2
        | _ -> None
      end
  | Fbinop(Fimplies, p1, p2) ->
      begin match gpred (not def) p1, gpred def p2 with
        | Some p1, Some p2 -> Some (Gimplies (p1, p2))
        | Some p1, None        when def = false -> Some (Gnot p1)
        | None, (Some _ as p2) when def = false -> p2
        | _ -> None
      end
*)
  | Fnot p -> Gnot (gpred (not def) p)
  | Fquant _ 
  | Fapp _
  | Fif _
  | Fbinop _
  | Ftrue | Ffalse | Flet _ | Fcase _-> (* discarded *)
      raise NotGappa

let gpred p =
  (*Format.printf "gpred %a@." Util.print_predicate p;*)
  gpred p

(* extraction of a list of equalities and possibly a Gappa predicate *)

(*
let rec ghyp = function
  | Papp (id, [Tvar x; t], _) when is_eq id ->
    begin
      match termo t with
      | Some t' ->
          Hashtbl.replace var_table x t';
          [], None
      | None -> [], None
    end
  | Papp (id, [Tapp (id', [Tvar x], _); t], _) as p
      when is_eq id && (id' == float_value || id' == exact_value || id' == model_value) ->
    begin
      match termo t with
      | Some t ->
          let f = field_of_id id' in
          if Hashtbl.mem def_table (f, x) then
           (Hashtbl.add def_table (f, x) ();
            [f, Ident.string x, t], None)
          else
            [], gpred true p
      | None ->
          [], gpred true p
    end
  | Pand (_, _, p1, p2) as p ->
      begin match ghyp p1, ghyp p2 with
        | ([], _), ([], _) -> [], gpred true p
        | (e1,p1), (e2, p2) -> e1 @ e2, gando (p1, p2)
      end
  | Pnamed (_, p) ->
      ghyp p
  | p ->
      [], gpred true p
*)

(* Processing obligations.
   One Why obligation can be split into several Gappa obligations *)

(*
let queue = Queue.create ()

let reset () =
  Queue.clear queue;
  Hashtbl.clear gen_table;
  Hashtbl.clear var_table;
  Hashtbl.clear rnd_table;
  Hashtbl.clear def_table

let add_ctx_vars =
  List.fold_left 
    (fun acc -> function Svar (id,_) -> Idset.add id acc | _ -> acc)

let rec intros ctx = function
  | Forall (_, id, n, t, _, p) ->
      let id' = next_away id (add_ctx_vars (predicate_vars p) ctx) in
      let p' = subst_in_predicate (subst_onev n id') p in
      intros (Svar (id', t) :: ctx) p'
  | Pimplies (_, a, b) -> 
      let h = fresh_hyp () in 
      intros (Spred (h, a) :: ctx) b
  | Pnamed (_, p) ->
      intros ctx p
  | c -> 
      ctx, c
*)

MARCHE Claude's avatar
MARCHE Claude committed
701 702 703 704 705 706 707 708
let rec intros g =
  match g.f_node with
    | Fquant(Fforall,fq) ->
        let  _,_,f = f_open_quant fq in
        intros f
    | Fbinop(Fimplies,_f1,_f2) ->
        assert false (* TODO *)
    | _ -> g
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
709
(*
MARCHE Claude's avatar
MARCHE Claude committed
710 711
    List.fold_left
      (fun ((el, pl) as acc) h ->
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
712 713 714 715 716 717 718 719 720 721 722 723
          match h with
            | Svar _ -> acc
            | Spred (_, p) -> 
                let ep, pp = ghyp p in
                let pl =
                  match pp with
                    | None -> pl
                    | Some pp -> pp :: pl
                  in
                ep :: el, pl)
        ([],[]) ctx
	in
MARCHE Claude's avatar
MARCHE Claude committed
724 725 726 727
*)

let process_goal fmt g = 
  let (*el,*)pl = intros g in
MARCHE Claude's avatar
MARCHE Claude committed
728 729
  try
    let concl = gpred false pl in
MARCHE Claude's avatar
MARCHE Claude committed
730
(*
MARCHE Claude's avatar
MARCHE Claude committed
731
    | None -> 
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
732
    | Some p ->
MARCHE Claude's avatar
MARCHE Claude committed
733 734
*)
(*
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
735 736 737 738
        let gconcl = List.fold_right (fun p acc -> Gimplies (p, acc)) pl p in
        let el = List.rev (List.flatten el) in
	Queue.add (el, gconcl) queue
*)
MARCHE Claude's avatar
MARCHE Claude committed
739 740 741 742 743 744 745
    print_obligation fmt ([],concl) ;
    true
  with NotGappa ->
    (* goal is not a gappa prop *)
    (* if debug then Format.eprintf "not a gappa prop; skipped@."; *)
    print_obligation fmt ([],Gle(Gcst "1","0")) ;
    true
MARCHE Claude's avatar
MARCHE Claude committed
746

MARCHE Claude's avatar
gappa  
MARCHE Claude committed
747

748
let print_decl info fmt d = match d.d_node with
749 750
  | Dtype _dl -> false
  | Dlogic _dl -> false
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
751
  | Dind _ -> unsupportedDecl d 
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
752
      "gappa: inductive definition are not supported"
753
  | Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
754 755 756
  | Dprop (Paxiom, _pr, _f) ->
      assert false
(*
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
757
      fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n" 
758
        print_ident pr.pr_name (print_fmla info) f; true
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
759 760
*)
  | Dprop (Pgoal, _pr, f) ->
MARCHE Claude's avatar
MARCHE Claude committed
761
      process_goal fmt f
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
762 763
	(*
      assert false
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
764
      fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
765
        print_ident pr.pr_name (print_fmla info) f; true
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
766
	*)
767
  | Dprop ((Plemma|Pskip), _, _) ->
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
768 769
      assert false

770
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
771

772 773 774 775 776 777 778 779 780
let print_task pr thpr syn fmt task =
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
(*
  let info = {
    info_syn = syn;
    info_rem = get_remove_set task }
  in
*)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
781
  let decls = Task.task_decls task in
782
  ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
783 784

let () = register_printer "gappa" 
785 786
  (fun pr thpr syn fmt task -> 
     load_prelude info;
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
787 788 789
(*
     forget_all ident_printer;
*)
790
     print_task pr thpr syn fmt task)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
791 792


MARCHE Claude's avatar
gappa  
MARCHE Claude committed
793
(*
794 795 796
let print_goal info fmt (_id, _f, task) =  
  print_task info fmt task;
  fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla info) f
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
797 798 799
*)


800
*)
MARCHE Claude's avatar
gappa  
MARCHE Claude committed
801 802 803 804 805
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
End:
*)