From 42f3e6372905e3a62ce3c872443b910d8118eb8f Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 11 Dec 2018 14:04:54 +0100 Subject: [PATCH] improve elim_let --- src/transform/eliminate_let.ml | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/transform/eliminate_let.ml b/src/transform/eliminate_let.ml index ccf7bf2fb..d86da8278 100644 --- a/src/transform/eliminate_let.ml +++ b/src/transform/eliminate_let.ml @@ -13,19 +13,16 @@ open Term (* eliminate let *) -let rec elim_t func pred map t = match t.t_node with - | Tvar vs -> - (try Mvs.find vs map with Not_found -> t) +let rec elim_t func pred t = match t.t_node with | Tlet (t1,tb) when (if t.t_ty = None then pred else func) -> - let vs,t2 = t_open_bound tb in - let t1 = elim_t func pred map t1 in - elim_t func pred (Mvs.add vs t1 map) t2 + let t1 = elim_t func pred t1 in + elim_t func pred (t_open_bound_with t1 tb) | _ -> - t_map (elim_t func pred map) t + t_map (elim_t func pred) t -let eliminate_let_term = Trans.rewrite (elim_t true false Mvs.empty) None -let eliminate_let_fmla = Trans.rewrite (elim_t false true Mvs.empty) None -let eliminate_let = Trans.rewrite (elim_t true true Mvs.empty) None +let eliminate_let_term = Trans.rewrite (elim_t true false) None +let eliminate_let_fmla = Trans.rewrite (elim_t false true) None +let eliminate_let = Trans.rewrite (elim_t true true) None let () = Trans.register_transform "eliminate_let_term" eliminate_let_term -- 2.22.0