Commit e3d45ea7 authored by GARCHERY Quentin's avatar GARCHERY Quentin

Merge branch 'improve_elim_let' into 'master'

Improve elim let

See merge request !75
parents e2c5d555 b6699186
......@@ -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
......
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