diff --git a/src/transform/eliminate_algebraic.ml b/src/transform/eliminate_algebraic.ml index b61b3b7ed5a8bac8b4cd1012f3325407f52c4333..a5ec9e583ebca4d14b5f2ed2d9643c31b689d0b0 100644 --- a/src/transform/eliminate_algebraic.ml +++ b/src/transform/eliminate_algebraic.ml @@ -206,7 +206,8 @@ let comp t (state,task) = match t.task_decl with | td -> state, add_tdecl task td -let comp = Register.store (fun () -> Trans.fold_map comp empty_state None) +let eliminate_algebraic = + Register.store (fun () -> Trans.fold_map comp empty_state None) -let () = Register.register_transform "eliminate_algebraic" comp +let () = Register.register_transform "eliminate_algebraic" eliminate_algebraic diff --git a/src/transform/eliminate_algebraic.mli b/src/transform/eliminate_algebraic.mli index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..585a51755ad6adcdb2ea723a375716211bea6a2f 100644 --- a/src/transform/eliminate_algebraic.mli +++ b/src/transform/eliminate_algebraic.mli @@ -0,0 +1,21 @@ +(**************************************************************************) +(* *) +(* 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_algebraic : Task.task Register.trans_reg + diff --git a/src/transform/eliminate_definition.ml b/src/transform/eliminate_definition.ml index 66f37d29f5cfdbae52c8d10ce3c078edf7996002..b9da8736bfa64776dee14e6381ca8859cc0ab16e 100644 --- a/src/transform/eliminate_definition.ml +++ b/src/transform/eliminate_definition.ml @@ -44,33 +44,47 @@ 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 axl d = match d with +let add_ld q 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 nm = ls.ls_name.id_short ^ "_def" in - let pr = create_prsymbol (id_derive nm ls.ls_name) in - let vl,e = open_ls_defn ld in - let tl = List.map t_var vl in - begin match e with - | Term t -> - let hd = t_app ls tl t.t_ty in + let vl,e = open_ls_defn ld in begin match e with + | Term t when func -> + let nm = ls.ls_name.id_short ^ "_def" in + let hd = t_app ls (List.map t_var vl) t.t_ty in let ax = f_forall vl [[Term hd]] (t_insert hd t) in + let pr = create_prsymbol (id_derive nm ls.ls_name) in create_prop_decl Paxiom pr ax :: axl, (ls, None) - | Fmla f -> - let hd = f_app ls tl in + | Fmla f when pred -> + let nm = ls.ls_name.id_short ^ "_def" in + let hd = f_app ls (List.map t_var vl) in let ax = f_forall vl [[Fmla hd]] (f_insert hd f) in + let pr = create_prsymbol (id_derive nm ls.ls_name) in create_prop_decl Paxiom pr ax :: axl, (ls, None) + | _ -> axl, d end -let elim q d = match d.d_node with +let elim q func pred d = match d.d_node with | Dlogic l -> - let axl, l = map_fold_left (add_ld q) [] l in + let axl, l = map_fold_left (add_ld q func pred) [] l in let d = create_logic_decl l in d :: List.rev axl | _ -> [d] -let elim = Register.store_query (fun q -> Trans.decl (elim q) None) +let eliminate_definition_func = + Register.store_query (fun q -> Trans.decl (elim q true false) None) -let () = Register.register_transform "eliminate_definition" elim +let eliminate_definition_pred = + Register.store_query (fun q -> Trans.decl (elim q false true) None) + +let eliminate_definition = + Register.store_query (fun q -> Trans.decl (elim q true true) None) + +let () = + Register.register_transform "eliminate_definition_func" + eliminate_definition_func; + Register.register_transform "eliminate_definition_pred" + eliminate_definition_pred; + Register.register_transform "eliminate_definition" + eliminate_definition diff --git a/src/transform/eliminate_definition.mli b/src/transform/eliminate_definition.mli index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..16b1b2ae6adfbdc721469c8aa111a145cb5079c8 100644 --- a/src/transform/eliminate_definition.mli +++ b/src/transform/eliminate_definition.mli @@ -0,0 +1,23 @@ +(**************************************************************************) +(* *) +(* 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_definition_func : Task.task Register.trans_reg +val eliminate_definition_pred : Task.task Register.trans_reg +val eliminate_definition : Task.task Register.trans_reg + diff --git a/src/transform/eliminate_inductive.ml b/src/transform/eliminate_inductive.ml index f320cb8f8c32a72c82c7de6af69a3f0e6ca84099..4a78d1a0245ec9eab66ab7991134332a8708bec3 100644 --- a/src/transform/eliminate_inductive.ml +++ b/src/transform/eliminate_inductive.ml @@ -57,7 +57,7 @@ let elim d = match d.d_node with List.rev dl | _ -> [d] -let elim = Register.store (fun () -> Trans.decl elim None) +let eliminate_inductive = Register.store (fun () -> Trans.decl elim None) -let () = Register.register_transform "eliminate_inductive" elim +let () = Register.register_transform "eliminate_inductive" eliminate_inductive diff --git a/src/transform/eliminate_inductive.mli b/src/transform/eliminate_inductive.mli index 81fccfe9c9422316b52813ab27a2d15c31f67db3..3eadd844b0e069aaf1b8e8c4c0bbb26dad47754c 100644 --- a/src/transform/eliminate_inductive.mli +++ b/src/transform/eliminate_inductive.mli @@ -17,3 +17,5 @@ (* *) (**************************************************************************) +val eliminate_inductive : Task.task Register.trans_reg +