eliminate_if.ml 4.33 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

open Util
open Ident
open Term
open Decl

25
(** Eliminate if-then-else in terms *)
26

27
let rec elim_t letl contT t = match t.t_node with
28 29 30
  | Tlet (t1,tb) ->
      let u,t2 = t_open_bound tb in
      let t_let e1 e2 =
31
        if t_equal e1 t1 && t_equal e2 t2 then t else t_let u e1 e2
32 33
      in
      let cont_in t1 t2 = contT (t_let t1 t2) in
34 35
      let cont_let t1 = elim_t ((u,t1)::letl) (cont_in t1) t2 in
      elim_t letl cont_let t1
36
  | Tif (f,t1,t2) ->
37
      let f = elim_f (fun f -> f) f in
38
      let f = List.fold_left (fun f (v,t) -> f_let v t f) f letl in
39 40
      f_if f (elim_t letl contT t1) (elim_t letl contT t2)
  | Tcase _ ->
41
      Printer.unsupportedTerm t
42
        "cannot eliminate 'if-then-else' under 'match' in terms"
43
  | _ ->
44
      t_map_cont (elim_t letl) elim_f contT t
45

46
and elim_f contF f = match f.f_node with
47
  | Fapp _ | Flet _ | Fcase _ ->
48 49 50
      contF (f_map_cont (elim_t []) elim_f (fun f -> f) f)
  | _ -> f_map_cont elim_tr elim_f contF f

51
(* the only terms we can still meet are the terms in triggers *)
52
and elim_tr contT t = match t.t_node with
53
  | Tif _ ->
54
      Printer.unsupportedTerm t
55
        "cannot eliminate 'if-then-else' in trigger terms"
56
  | _ -> t_map_cont elim_tr elim_f contT t
57

58 59 60 61 62 63 64
let elim_f f = elim_f (fun f -> f) f

let rec elim_t t = t_map elim_t elim_f t

let rec has_if t = match t.t_node with
  | Tif _ -> true
  | _ -> t_any has_if ffalse t
65 66 67 68 69 70

let add_ld axl d = match d with
  | _, None -> axl, d
  | ls, Some ld ->
      let vl,e = open_ls_defn ld in
      begin match e with
71
        | Term t when has_if t ->
72
            let nm = ls.ls_name.id_string ^ "_def" in
73
            let pr = create_prsymbol (id_derive nm ls.ls_name) in
74 75
            let hd = t_app ls (List.map t_var vl) t.t_ty in
            let f = f_forall vl [[Term hd]] (elim_f (f_equ hd t)) in
76 77 78
            create_prop_decl Paxiom pr f :: axl, (ls, None)
        | _ ->
            axl, make_ls_defn ls vl (e_map elim_t elim_f e)
79 80
      end

81
let elim_d d = match d.d_node with
82 83 84 85 86
  | Dlogic l ->
      let axl, l = map_fold_left add_ld [] l in
      let d = create_logic_decl l in
      d :: List.rev axl
  | _ ->
87
      [decl_map (fun _ -> assert false) elim_f d]
88

89
let eliminate_if_term = Trans.decl elim_d None
90 91

(** Eliminate if-then-else in formulas *)
92

93
let rec elim_t t = t_map elim_t (elim_f true) t
94

95
and elim_f sign f = match f.f_node with
96
  | Fif (f1,f2,f3) ->
97 98 99 100
      let f1p = elim_f sign f1 in
      let f1n = elim_f (not sign) f1 in
      let f2 = elim_f sign f2 in
      let f3 = elim_f sign f3 in
101 102 103
      if sign then f_and (f_implies f1n f2) (f_or f1p f3)
              else f_or (f_and f1p f2) (f_and (f_not f1n) f3)
  | _ ->
104
      f_map_sign elim_t elim_f sign f
105

106
let eliminate_if_fmla = Trans.rewrite elim_t (elim_f true) None
107

108
let eliminate_if = Trans.compose eliminate_if_term eliminate_if_fmla
109 110

let () =
111 112 113
  Trans.register_transform "eliminate_if_term" (fun _ -> eliminate_if_term);
  Trans.register_transform "eliminate_if_fmla" (fun _ -> eliminate_if_fmla);
  Trans.register_transform "eliminate_if" (fun _ -> eliminate_if)
114