Commit 42f3e637 authored by Quentin Garchery's avatar Quentin Garchery

improve elim_let

parent f43e1f02
...@@ -13,19 +13,16 @@ open Term ...@@ -13,19 +13,16 @@ open Term
(* eliminate let *) (* eliminate let *)
let rec elim_t func pred map t = match t.t_node with let rec elim_t func pred t = match t.t_node with
| Tvar vs ->
(try Mvs.find vs map with Not_found -> t)
| Tlet (t1,tb) when (if t.t_ty = None then pred else func) -> | 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 t1 in
let t1 = elim_t func pred map t1 in elim_t func pred (t_open_bound_with t1 tb)
elim_t func pred (Mvs.add vs t1 map) t2
| _ -> | _ ->
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_term = Trans.rewrite (elim_t true false) None
let eliminate_let_fmla = Trans.rewrite (elim_t false true Mvs.empty) None let eliminate_let_fmla = Trans.rewrite (elim_t false true) None
let eliminate_let = Trans.rewrite (elim_t true true Mvs.empty) None let eliminate_let = Trans.rewrite (elim_t true true) None
let () = let () =
Trans.register_transform "eliminate_let_term" eliminate_let_term Trans.register_transform "eliminate_let_term" eliminate_let_term
......
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