introduce the "eliminate_builtin" transformation

Makefile.in

@@ -103,7 +103,7 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 
 LIB_TRANSFORM = simplify_recursive_definition inlining \
 		split_conjunction encoding_decorate \
-		eliminate_definition \
+		eliminate_builtin eliminate_definition \
 		compile_match eliminate_algebraic \
 		eliminate_inductive eliminate_let eliminate_if
 

drivers/alt_ergo.drv

@@ -15,6 +15,7 @@ fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
 transformation "simplify_recursive_definition"
 transformation "inline_trivial"
 
+transformation "eliminate_builtin"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "compile_match"

drivers/cvc3.drv

@@ -13,6 +13,7 @@ unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
 transformation "simplify_recursive_definition"      
 transformation "inline_trivial"
 
+transformation "eliminate_builtin"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "compile_match"

drivers/why3_encoding_decorate.drv

 printer "why3"
 filename "%f-%t-%g.why"
 
+transformation "eliminate_builtin"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "compile_match"

drivers/why3_total_elimination.drv

 printer "why3"
 filename "%f-%t-%g.why"
 
+transformation "eliminate_builtin"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "compile_match"

drivers/z3.drv

@@ -13,6 +13,7 @@ unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
 transformation "simplify_recursive_definition"      
 transformation "inline_trivial"
 
+transformation "eliminate_builtin"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "compile_match"

src/transform/eliminate_builtin.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 Util
+open Ident
+open Term
+open Decl
+
+let add_ld q = function
+  | ls, Some _ when Driver.query_remove q ls.ls_name -> (ls, None)
+  | d -> d
+
+let add_id q (ld,id) = function
+  | ls, _ when Driver.query_remove q ls.ls_name -> (ls, None)::ld, id
+  | d -> ld, d::id
+
+let elim q d = match d.d_node with
+  | Dlogic l ->
+      create_logic_decls (List.map (add_ld q) l)
+  | Dind l ->
+      let ld, id = List.fold_left (add_id q) ([],[]) l in
+      create_logic_decls (List.rev ld) @ create_ind_decls (List.rev id)
+  | _ -> [d]
+
+let eliminate_builtin =
+  Register.store_query (fun q -> Trans.decl (elim q) None)
+
+let () = Register.register_transform "eliminate_builtin" eliminate_builtin
+

src/transform/eliminate_builtin.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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+val eliminate_builtin : Task.task Register.trans_reg
+

src/transform/eliminate_definition.ml

@@ -44,9 +44,8 @@ let rec f_insert hd f = match f.f_node with
       f_case tl (List.map br bl)
   | _ -> f_iff_simp hd f
 
-let add_ld q func pred axl d = match d with
+let add_ld func pred axl d = match d with
   | _, None -> axl, d
-  | ls, _ when Driver.query_remove q ls.ls_name -> axl, (ls, None)
   | ls, Some ld ->
       let vl,e = open_ls_defn ld in begin match e with
         | Term t when func ->
@@ -64,21 +63,21 @@ let add_ld q func pred axl d = match d with
         | _ -> axl, d
       end
 
-let elim q func pred d = match d.d_node with
+let elim func pred d = match d.d_node with
   | Dlogic l ->
-      let axl, l = map_fold_left (add_ld q func pred) [] l in
+      let axl, l = map_fold_left (add_ld func pred) [] l in
       let d = create_logic_decl l in
       d :: List.rev axl
   | _ -> [d]
 
 let eliminate_definition_func =
-  Register.store_query (fun q -> Trans.decl (elim q true false) None)
+  Register.store (fun () -> Trans.decl (elim true false) None)
 
 let eliminate_definition_pred =
-  Register.store_query (fun q -> Trans.decl (elim q false true) None)
+  Register.store (fun () -> Trans.decl (elim false true) None)
 
 let eliminate_definition =
-  Register.store_query (fun q -> Trans.decl (elim q true true) None)
+  Register.store (fun () -> Trans.decl (elim true true) None)
 
 let () =
   Register.register_transform "eliminate_definition_func"

src/transform/inlining.ml

@@ -64,7 +64,7 @@ and replacep env f =
 and substt env d = t_map (replacet env) (replacep env) d
 and substp env d = f_map (replacet env) (replacep env) d
 
-let fold q isnotinlinedt isnotinlinedf d (env, task) = 
+let fold isnotinlinedt isnotinlinedf d (env, task) = 
 (*  Format.printf "I see : %a@\n%a@\n" Pretty.print_decl d print_env env;*)
   match d.d_node with
     | Dlogic [ls,ld] -> begin
@@ -75,15 +75,13 @@ let fold q isnotinlinedt isnotinlinedf d (env, task) =
               match e with
                 | Term t ->
                     let t = replacet env t in
-                    if isnotinlinedt t || Driver.query_remove q ls.ls_name
-                      || t_s_any ffalse ((==) ls) t
+                    if isnotinlinedt t || t_s_any ffalse ((==) ls) t
                     then env, add_decl task 
                       (create_logic_decl [make_fs_defn ls vs t])
                     else {env with fs = Mls.add ls (vs,t) env.fs},task
                 | Fmla f -> 
                     let f = replacep env f in
-                    if isnotinlinedf f || Driver.query_remove q ls.ls_name ||
-                      f_s_any ffalse ((==) ls) f
+                    if isnotinlinedf f || f_s_any ffalse ((==) ls) f
                     then env, add_decl task 
                       (create_logic_decl [make_ps_defn ls vs f])
                     else {env with ps = Mls.add ls (vs,f) env.ps},task
@@ -105,15 +103,15 @@ let fold q isnotinlinedt isnotinlinedf d (env, task) =
     | Dprop (k,pr,f) -> 
         env,add_decl task (create_prop_decl k pr (replacep env f))
         
-let fold q isnotinlinedt isnotinlinedf task0 (env, task) = 
+let fold isnotinlinedt isnotinlinedf task0 (env, task) = 
   match task0.task_decl with
-    | Decl d -> fold q isnotinlinedt isnotinlinedf d (env, task)
+    | Decl d -> fold isnotinlinedt isnotinlinedf d (env, task)
     | td -> env, add_tdecl task td
 
 let t ~isnotinlinedt ~isnotinlinedf = 
-  Register.store_query 
-    (fun query -> Trans.fold_map 
-       (fold query isnotinlinedt isnotinlinedf) 
+  Register.store 
+    (fun () -> Trans.fold_map 
+       (fold isnotinlinedt isnotinlinedf) 
        empty_env None)
 
 let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)