Commit c1d9146b authored by Andrei Paskevich's avatar Andrei Paskevich

eliminate if-then-else in terms under match statements

parent d1802ec5
......@@ -1342,12 +1342,12 @@ let rec list_map_cont fnL contL = function
| [] ->
contL []
let expr_map_cont fnT fnF contE = function
let e_map_cont fnT fnF contE = function
| Term t -> fnT (fun t -> contE (Term t)) t
| Fmla f -> fnF (fun f -> contE (Fmla f)) f
let tr_map_cont fnT fnF =
list_map_cont (list_map_cont (expr_map_cont fnT fnF))
list_map_cont (list_map_cont (e_map_cont fnT fnF))
let t_map_cont fnT fnF contT t =
let contT e = contT (t_label_copy t e) in
......@@ -1572,13 +1572,13 @@ let f_equal_alpha = f_equal_alpha (bnd_new 0) (bnd_new 0)
let rec pat_hash_alpha p =
match p.pat_node with
| Pwild -> 0
| Pvar _ -> assert false (* TODO 1 ? *)
| Papp (f, l) ->
| Pvar _ -> 1
| Papp (f, l) ->
let acc = Hashcons.combine 2 (ls_hash f) in
Hashcons.combine_list pat_hash_alpha acc l
| Pas (p, _) -> Hashcons.combine 3 (pat_hash_alpha p)
| Por (p, q) ->
Hashcons.combine
| Por (p, q) ->
Hashcons.combine
(Hashcons.combine 4 (pat_hash_alpha p)) (pat_hash_alpha q)
(* hash modulo alpha of terms and formulas *)
......@@ -1613,68 +1613,65 @@ let binop_hash = function
let rec t_hash_alpha m t =
match t.t_node with
| Tbvar _i -> 0
| Tbvar _i -> 0
| Tvar v -> Hashcons.combine 1 (vs_hash v)
| Tconst c -> Hashcons.combine 2 (Hashtbl.hash c)
| Tapp (s,l) ->
| Tapp (s,l) ->
let acc = Hashcons.combine 3 (ls_hash s) in
Hashcons.combine_list (t_hash_alpha m) acc l
| Tif (f,t,e) ->
Hashcons.combine3 4 (f_hash_alpha m f) (t_hash_alpha m t)
| Tif (f,t,e) ->
Hashcons.combine3 4 (f_hash_alpha m f) (t_hash_alpha m t)
(t_hash_alpha m e)
| Tlet (t,tb)->
Hashcons.combine2 5 (t_hash_alpha m t)
| Tlet (t,tb)->
Hashcons.combine2 5 (t_hash_alpha m t)
(bound_hash_alpha t_hash_alpha m tb)
| Tcase (t,b) ->
| Tcase (t,b) ->
let acc = Hashcons.combine 6 (t_hash_alpha m t) in
Hashcons.combine_list (branch_hash_alpha t_hash_alpha m) acc b
| Teps fb ->
| Teps fb ->
Hashcons.combine 7 (bound_hash_alpha f_hash_alpha m fb)
and f_hash_alpha m f =
match f.f_node with
| Fapp (s,l) ->
| Fapp (s,l) ->
let acc = Hashcons.combine 0 (ls_hash s) in
Hashcons.combine_list (t_hash_alpha m) acc l
| Fquant (q,b) ->
| Fquant (q,b) ->
Hashcons.combine2 1 (quant_hash q) (quant_hash_alpha f_hash_alpha m b)
| Fbinop (a,f,g) ->
| Fbinop (a,f,g) ->
Hashcons.combine3 2 (binop_hash a) (f_hash_alpha m f) (f_hash_alpha m g)
| Fnot f -> Hashcons.combine 3 (f_hash_alpha m f)
| Ftrue -> 4
| Ffalse -> 5
| Fif (f,g,h) ->
Hashcons.combine3 6 (f_hash_alpha m f) (f_hash_alpha m g)
| Fif (f,g,h) ->
Hashcons.combine3 6 (f_hash_alpha m f) (f_hash_alpha m g)
(f_hash_alpha m h)
| Flet (t,fb) ->
Hashcons.combine2 7 (t_hash_alpha m t)
| Flet (t,fb) ->
Hashcons.combine2 7 (t_hash_alpha m t)
(bound_hash_alpha f_hash_alpha m fb)
| Fcase (t,b) ->
| Fcase (t,b) ->
let acc = Hashcons.combine 8 (t_hash_alpha m t) in
Hashcons.combine_list (branch_hash_alpha f_hash_alpha m) acc b
let t_hash_alpha = t_hash_alpha (bnd_new 0)
let f_hash_alpha = f_hash_alpha (bnd_new 0)
module Hterm_alpha =
module Hterm_alpha =
Hashtbl.Make
(struct
type t = term
(struct
type t = term
let equal = t_equal_alpha
let hash = t_hash_alpha
end)
module Hfmla_alpha =
module Hfmla_alpha =
Hashtbl.Make
(struct
type t = fmla
(struct
type t = fmla
let equal = f_equal_alpha
let hash = f_hash_alpha
end)
(* binder-free term/formula matching *)
exception NoMatch
......
......@@ -417,6 +417,12 @@ val t_map_cont : ((term -> 'a) -> term -> 'a) ->
val f_map_cont : ((term -> 'a) -> term -> 'a) ->
((fmla -> 'a) -> fmla -> 'a) -> (fmla -> 'a) -> fmla -> 'a
val e_map_cont : ((term -> 'a) -> term -> 'b) ->
((fmla -> 'a) -> fmla -> 'b) -> (expr -> 'a) -> expr -> 'b
val list_map_cont : (('a -> 'b) -> 'c -> 'b) ->
('a list -> 'b) -> 'c list -> 'b
(** simplification map *)
val f_map_simp : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
......
......@@ -24,28 +24,40 @@ open Decl
(** Eliminate if-then-else in terms *)
let rec elim_t letl contT t = match t.t_node with
let rec has_if t = match t.t_node with
| Tif _ -> true
| _ -> t_any has_if ffalse t
let rec elim_t contT t =
let contTl e = contT (t_label_copy t e) in
match t.t_node with
| Tlet (t1,tb) ->
let u,t2,close = t_open_bound_cb tb in
let cont_in t1 t2 = contT (t_let t1 (close u t2)) in
let cont_let t1 = elim_t ((u,t1)::letl) (cont_in t1) t2 in
elim_t letl cont_let t1
let cont_in t1 t2 = contTl (t_let t1 (close u t2)) in
let cont_let_t t1 = elim_t (cont_in t1) t2 in
let cont_let_f t1 = f_let_close u t1 (elim_t contT t2) in
elim_t (if has_if t2 then cont_let_f else cont_let_t) t1
| Tif (f,t1,t2) ->
let f = elim_f (fun f -> f) f in
let f = List.fold_left (fun f (v,t) -> f_let_close v t f) f letl in
f_if f (elim_t letl contT t1) (elim_t letl contT t2)
| Tcase _ ->
Printer.unsupportedTerm t
"cannot eliminate 'if-then-else' under 'match' in terms"
f_if f (elim_t contT t1) (elim_t contT t2)
| Tcase (t1, bl) ->
let bl = List.rev_map t_open_branch_cb bl in
let fi = List.exists (fun (_,t,_) -> has_if t) bl in
let fnB ctB (p,t,cl) = elim_t (fun t -> ctB (cl p t)) t in
let cont_with t1 bl = contTl (t_case t1 (List.rev bl)) in
let cont_case_t t1 = list_map_cont fnB (cont_with t1) bl in
let close (p,t,_) = f_close_branch p (elim_t contT t) in
let cont_case_f t1 = f_case t1 (List.rev_map close bl) in
elim_t (if fi then cont_case_f else cont_case_t) t1
| _ ->
t_map_cont (elim_t letl) elim_f contT t
t_map_cont elim_t elim_f contT t
and elim_f contF f = match f.f_node with
| Fapp _ | Flet _ | Fcase _ ->
contF (f_map_cont (elim_t []) elim_f (fun f -> f) f)
contF (f_map_cont elim_t elim_f (fun f -> f) f)
| _ -> f_map_cont elim_tr elim_f contF f
(* the only terms we can still meet are the terms in triggers *)
(* the only terms we still can meet are the terms in triggers *)
and elim_tr contT t = match t.t_node with
| Tif _ ->
Printer.unsupportedTerm t
......@@ -56,10 +68,6 @@ 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
let add_ld axl d = match d with
| _, None -> axl, d
| ls, Some ld ->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment