Commit a60867e2 authored by Andrei Paskevich's avatar Andrei Paskevich

remove "simplify_recursive_definition", never used

parent fcf2c1cc
......@@ -117,8 +117,7 @@ LIB_PARSER = ptree denv glob parser typing lexer
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection
LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
inlining split_goal induction \
LIB_TRANSFORM = simplify_formula inlining split_goal induction \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if \
libencoding discriminate protect_finite \
......
......@@ -16,7 +16,6 @@ time "Valid (%s)"
time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
......@@ -9,7 +9,6 @@ valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
time "why3cpulimit time : %s s"
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
......@@ -5,7 +5,6 @@ fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
......
......@@ -13,7 +13,6 @@ outofmemory "Out of memory\\|std::bad_alloc\\|GNU MP: Cannot allocate memory"
time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
......@@ -18,10 +18,8 @@ time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
......
......@@ -11,7 +11,6 @@ unknown "no contradiction was found\\|some enclosures were not satisfied" ""
time "why3cpulimit time : %s s"
fail "Error: \\(.*\\)" "\\1"
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "inline_all"
......
......@@ -10,7 +10,6 @@ valid "\\bTrue\\b"
unknown "\\bFalse\\b" "\\bFalse\\b"
time "why3cpulimit time : %s s"
(*transformation "simplify_recursive_definition"*)
(*transformation "inline_trivial"*)
(*transformation "inline_all"*)
......
......@@ -13,10 +13,8 @@ time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
......
......@@ -9,7 +9,6 @@ transformation "eliminate_builtin"
(* PVS does not support mutual recursion *)
transformation "eliminate_mutual_recursion"
(*transformation "simplify_recursive_definition"*)
(* though we could do better, we only use recursion on one argument *)
transformation "eliminate_non_struct_recursion"
......
......@@ -9,7 +9,6 @@ valid "\\bValid\\b"
unknown "\\bInvalid\\b" ""
time "why3cpulimit time : %s s"
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
......@@ -15,7 +15,6 @@ time "why3cpulimit time : %s s"
(* to be improved *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
......@@ -22,7 +22,6 @@ time "why3cpulimit time : %s s"
(* to be improved *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
......@@ -15,7 +15,6 @@ time "why3cpulimit time : %s s"
(* to be improved *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
......@@ -10,7 +10,6 @@ unknown "^\\(unknown\\|sat\\)" ""
time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
......@@ -11,7 +11,6 @@ unknown "feature not supported: non linear problem" "non linear arith"
time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
......@@ -13,10 +13,8 @@ time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
......
......@@ -11,7 +11,6 @@ time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
......@@ -11,7 +11,6 @@ time "why3cpulimit time : %s s"
(* to be improved *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Ident
open Ty
open Term
open Decl
type seen =
| SNot
| SOnce
| SBack
let rec find h e =
try
let r = Hid.find h e in
if r == e then e
else
let r = find h r in
Hid.replace h e r;
r
with Not_found -> e
let union h e1 e2 = Hid.replace h (find h e1) (find h e2)
let connexe (m:Sid.t Mid.t) =
let uf = Hid.create 32 in
let visited = Hid.create 32 in
Mid.iter (fun e _ -> Hid.replace visited e SNot) m;
let rec visit i last =
match Hid.find visited i with
| SNot ->
Hid.replace visited i SOnce;
let s = Mid.find i m in
let last = i::last in
Sid.iter (fun x -> visit x last) s;
Hid.replace visited i SBack
| SOnce ->
(try
List.iter (fun e -> if e==i then raise Exit else union uf i e) last
with Exit -> ())
| SBack -> ()
in
Mid.iter (fun e _ -> visit e []) m;
let ce = Hid.create 32 in
Mid.iter (fun e es ->
let r = find uf e in
let rl,rs,rb = try
Hid.find ce r
with Not_found -> [],Sid.empty, ref false in
Hid.replace ce r (e::rl,Sid.union rs es,rb)) m;
let rec visit (l,s,b) acc =
if !b then acc
else
begin
b := true;
let acc = Sid.fold (fun e acc ->
try
visit (Hid.find ce e) acc
with Not_found -> acc) s acc in
l::acc
end
in
List.rev (Hid.fold (fun _ -> visit) ce [])
let elt d =
match d.d_node with
| Dlogic l ->
let mem = Hid.create 16 in
List.iter (fun a -> Hid.add mem (fst a).ls_name a) l;
let tyoccurences acc _ = acc in
let loccurences acc ls =
if Hid.mem mem ls.ls_name then Sid.add ls.ls_name acc else acc in
let m = List.fold_left
(fun acc (ls,ld) ->
let fd = ls_defn_axiom ld in
let s = t_s_fold tyoccurences loccurences Sid.empty fd in
Mid.add ls.ls_name s acc) Mid.empty l in
let l = connexe m in
List.map (fun e -> create_logic_decl (List.map (Hid.find mem) e)) l
| Ddata l ->
let mem = Hid.create 16 in
List.iter (fun ((ts,_) as a) -> Hid.add mem ts.ts_name a) l;
let tyoccurences acc ts =
if Hid.mem mem ts.ts_name then Sid.add ts.ts_name acc else acc
in
let m = List.fold_left
(fun m (ts,l) ->
let s =
List.fold_left
(fun acc ({ls_args = tyl; ls_value = ty},_) ->
let ty = Opt.get ty in
List.fold_left
(fun acc ty -> ty_s_fold tyoccurences acc ty)
acc (ty::tyl)
) Sid.empty l
in
Mid.add ts.ts_name s m) Mid.empty l
in
let l = connexe m in
List.map (fun e -> create_data_decl (List.map (Hid.find mem) e)) l
| Dind _ -> [d] (* TODO *)
| Dtype _ | Dparam _ | Dprop _ -> [d]
let t = Trans.decl elt None
let () = Trans.register_transform "simplify_recursive_definition" t
~desc:"Separate@ the@ definitions@ that@ are@ not@ mutually@ recursive."
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2013 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(* Simplify the recursive type and logic definition *)
val t : Task.task Trans.trans
(* ungroup recursive definition *)
val elt : Decl.decl -> Decl.decl list
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