Commit 81cffbfb authored by Andrei Paskevich's avatar Andrei Paskevich

rearrange transformations (cont.)

parent c38aafa7
...@@ -206,7 +206,8 @@ let comp t (state,task) = match t.task_decl with ...@@ -206,7 +206,8 @@ let comp t (state,task) = match t.task_decl with
| td -> | td ->
state, add_tdecl task 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
(**************************************************************************)
(* *)
(* 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
...@@ -44,33 +44,47 @@ let rec f_insert hd f = match f.f_node with ...@@ -44,33 +44,47 @@ let rec f_insert hd f = match f.f_node with
f_case tl (List.map br bl) f_case tl (List.map br bl)
| _ -> f_iff_simp hd f | _ -> 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 | _, None -> axl, d
| ls, _ when Driver.query_remove q ls.ls_name -> axl, (ls, None) | ls, _ when Driver.query_remove q ls.ls_name -> axl, (ls, None)
| ls, Some ld -> | ls, Some ld ->
let nm = ls.ls_name.id_short ^ "_def" in let vl,e = open_ls_defn ld in begin match e with
let pr = create_prsymbol (id_derive nm ls.ls_name) in | Term t when func ->
let vl,e = open_ls_defn ld in let nm = ls.ls_name.id_short ^ "_def" in
let tl = List.map t_var vl in let hd = t_app ls (List.map t_var vl) t.t_ty in
begin match e with
| Term t ->
let hd = t_app ls tl t.t_ty in
let ax = f_forall vl [[Term hd]] (t_insert hd t) 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) create_prop_decl Paxiom pr ax :: axl, (ls, None)
| Fmla f -> | Fmla f when pred ->
let hd = f_app ls tl in 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 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) create_prop_decl Paxiom pr ax :: axl, (ls, None)
| _ -> axl, d
end end
let elim q d = match d.d_node with let elim q func pred d = match d.d_node with
| Dlogic l -> | 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 let d = create_logic_decl l in
d :: List.rev axl d :: List.rev axl
| _ -> [d] | _ -> [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
(**************************************************************************)
(* *)
(* 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
...@@ -57,7 +57,7 @@ let elim d = match d.d_node with ...@@ -57,7 +57,7 @@ let elim d = match d.d_node with
List.rev dl List.rev dl
| _ -> [d] | _ -> [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
...@@ -17,3 +17,5 @@ ...@@ -17,3 +17,5 @@
(* *) (* *)
(**************************************************************************) (**************************************************************************)
val eliminate_inductive : Task.task Register.trans_reg
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