"eliminate_let" transformation

Makefile.in

@@ -133,7 +133,8 @@ PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
 TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
 	split_conjunction.cmo encoding_decorate.cmo\
 	remove_logic_definition.cmo eliminate_inductive.cmo\
-	compile_match.cmo eliminate_algebraic.cmo
+	compile_match.cmo eliminate_algebraic.cmo\
+	eliminate_let.cmo
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 
 DRIVER_CMO := call_provers.cmo dynlink_compat.cmo driver_parser.cmo\

drivers/why3_total_elimination.drv

@@ -2,8 +2,10 @@ printer "why3"
 filename "%f-%t-%s.why"
 
 transformations
+    "eliminate_inductive"
     "compile_match"
     "eliminate_algebraic"
+    "eliminate_let"
 end
 
 theory BuiltIn

src/transform/eliminate_let.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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 Term
+
+let rec rewriteT t = match t.t_node with
+  | Tlet (t,tb) ->
+      let v,e = t_open_bound tb in
+      rewriteT (t_subst_single v t e)
+  | _ -> t_map rewriteT rewriteF t
+
+and rewriteF f = match f.f_node with
+  | Flet (t,fb) ->
+      let v,e = f_open_bound fb in
+      rewriteF (f_subst_single v t e)
+  | _ -> f_map rewriteT rewriteF f
+
+let comp = Register.store (fun () -> Trans.rewrite rewriteT rewriteF None)
+
+let () = Driver.register_transform "eliminate_let" comp
+

src/transform/eliminate_let.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+