- removal of "let" was already implemented by Francois,

  move this implementation to eliminate_let.
- initial commit of eliminate_definition : the goal is
  to translate definitions by match into series of axioms.

Makefile.in

@@ -134,7 +134,7 @@ 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\
-	eliminate_let.cmo
+	eliminate_definition.cmo eliminate_let.cmo
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 
 DRIVER_CMO := call_provers.cmo dynlink_compat.cmo driver_parser.cmo\

drivers/alt_ergo.drv

@@ -15,7 +15,7 @@ fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
 (* À discuter *)
 transformations
   "simplify_recursive_definition"      
-  "inline_let"
+  "eliminate_let"
   "inline_trivial"
   (*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"
 end

drivers/why3_total_elimination.drv

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

src/transform/eliminate_definition.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 Ident
+open Term
+open Decl
+
+let add_ls acc (ls,_) = create_logic_decl [ls,None] :: acc
+
+let add_ld acc ls ld =
+  let id = ls.ls_name.id_long ^ "_def" in
+  let pr = create_prsymbol (id_derive id ls.ls_name) in
+  create_prop_decl Paxiom pr (ls_defn_axiom ld) :: acc
+
+let add_ld acc (ls,ld) = match ld with
+  | None    -> acc
+  | Some ld -> add_ld acc ls ld
+
+let elim d = match d.d_node with
+  | Dlogic ll ->
+      let dl = List.fold_left add_ls [] ll in
+      let dl = List.fold_left add_ld dl ll in
+      List.rev dl
+  | _ -> [d]
+
+let elim = Register.store (fun () -> Trans.decl elim None)
+
+let () = Driver.register_transform "eliminate_definition" elim
+

src/transform/eliminate_let.ml

@@ -19,19 +19,31 @@
 
 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
+let rec rewrite_t map t =
+  match t.t_node with
+    | Tlet (t1,tb) ->
+        let t1 = rewrite_t map t1 in
+        let vs,t2 = t_open_bound tb in
+        rewrite_t (Mvs.add vs t1 map) t2
+    | Tvar vs ->
+        begin try
+          Mvs.find vs map
+        with Not_found -> t end
+    | _ -> t_map (rewrite_t map) (rewrite_f map) 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
+and rewrite_f map f =
+  match f.f_node with
+    | Flet (t1,fb) ->
+        let t1 = rewrite_t map t1 in
+        let vs,f2 = f_open_bound fb in
+        rewrite_f (Mvs.add vs t1 map) f2
+    | _ -> f_map (rewrite_t map) (rewrite_f map) f
 
-let comp = Register.store (fun () -> Trans.rewrite rewriteT rewriteF None)
+let remove_let_t = rewrite_t Mvs.empty
+let remove_let_f = rewrite_f Mvs.empty
 
-let () = Driver.register_transform "eliminate_let" comp
+let eliminate_let =
+  Register.store (fun () -> Trans.rewrite remove_let_t remove_let_f None)
+
+let () = Driver.register_transform "eliminate_let" eliminate_let
 

src/transform/eliminate_let.mli

@@ -17,3 +17,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val remove_let_t : Term.term -> Term.term
+val remove_let_f : Term.fmla -> Term.fmla
+
+val eliminate_let : Task.task Register.trans_reg
+

src/transform/inlining.ml

@@ -134,33 +134,3 @@ let () =
   Driver.register_transform "inline_all" all;
   Driver.register_transform "inline_trivial" trivial
 
-
-(* Let inlining *)
-
-let rec rewrite_t map t =
-  match t.t_node with
-    | Tlet (t1,tb) -> 
-        let t1 = rewrite_t map t1 in
-        let vs,t2 = t_open_bound tb in
-        rewrite_t (Mvs.add vs t1 map) t2
-    | Tvar vs ->
-        begin try
-          Mvs.find vs map
-        with Not_found -> t end
-    | _ -> t_map (rewrite_t map) (rewrite_f map) t
-
-and rewrite_f map f = 
-  match f.f_node with
-    | Flet (t1,fb) -> 
-        let t1 = rewrite_t map t1 in
-        let vs,f2 = f_open_bound fb in
-        rewrite_f (Mvs.add vs t1 map) f2
-    | _ -> f_map (rewrite_t map) (rewrite_f map) f
-
-let remove_let_t = rewrite_t Mvs.empty
-let remove_let_f = rewrite_f Mvs.empty
-
-let inline_let = 
-  Register.store (fun () -> Trans.rewrite remove_let_t remove_let_f None)
-
-let () =  Driver.register_transform "inline_let" inline_let

src/transform/inlining.mli

@@ -36,11 +36,6 @@ val all : Task.task Register.trans_reg
 val trivial : Task.task Register.trans_reg
 
 
-(* Inline let *)
-val remove_let_t : Term.term -> Term.term
-val remove_let_f : Term.fmla -> Term.fmla
-val inline_let : Task.task Register.trans_reg
-
 (* Function to use in other transformations if inlining is needed *)
 
 type env