Commit d85384f3 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix breakage of abstraction introduced by commit 2923f216.

That commit caused the declaration list to no longer be reset after each declaration.
Fixing this issue speeds up Gappa printing by 800%.
Abstracted subterms and formulas are now systematically added to extra_decls, since their presence in the global tables does not guarantee they have already been defined.
This guarantee was lost when the tables became global to the transformation, but it was hidden by list extra_decls never being emptied.

Note: removing alpha-conversion does not bring any sensible speedup.
parent c84568d7
...@@ -34,13 +34,13 @@ let abstraction (keep : lsymbol -> bool) = ...@@ -34,13 +34,13 @@ let abstraction (keep : lsymbol -> bool) =
| Tapp(ls,_) when keep ls -> | Tapp(ls,_) when keep ls ->
t_map abstract_term abstract_fmla t t_map abstract_term abstract_fmla t
| _ -> | _ ->
begin try Hterm_alpha.find term_table t with Not_found -> let (ls, tabs) = try Hterm_alpha.find term_table t with Not_found ->
let ls = create_fsymbol (id_fresh "abstr") [] t.t_ty in let ls = create_fsymbol (id_fresh "abstr") [] t.t_ty in
let tabs = t_app ls [] t.t_ty in let tabs = t_app ls [] t.t_ty in
extra_decls := ls :: !extra_decls; Hterm_alpha.add term_table t (ls, tabs);
Hterm_alpha.add term_table t tabs; ls, tabs in
tabs extra_decls := ls :: !extra_decls;
end tabs
and abstract_fmla f = and abstract_fmla f =
match f.f_node with match f.f_node with
...@@ -50,18 +50,19 @@ let abstraction (keep : lsymbol -> bool) = ...@@ -50,18 +50,19 @@ let abstraction (keep : lsymbol -> bool) =
| Fapp(ls,_) when keep ls -> | Fapp(ls,_) when keep ls ->
f_map abstract_term abstract_fmla f f_map abstract_term abstract_fmla f
| _ -> | _ ->
begin try Hfmla_alpha.find fmla_table f with Not_found -> let (ls, fabs) = try Hfmla_alpha.find fmla_table f with Not_found ->
let ls = create_psymbol (id_fresh "abstr") [] in let ls = create_psymbol (id_fresh "abstr") [] in
let fabs = f_app ls [] in let fabs = f_app ls [] in
extra_decls := ls :: !extra_decls; Hfmla_alpha.add fmla_table f (ls, fabs);
Hfmla_alpha.add fmla_table f fabs; ls, fabs in
fabs extra_decls := ls :: !extra_decls;
end in fabs in
let abstract_decl (d : decl) : decl list = let abstract_decl (d : decl) : decl list =
let d = decl_map abstract_term abstract_fmla d in let d = decl_map abstract_term abstract_fmla d in
List.fold_left let l = List.fold_left
(fun acc ls -> create_logic_decl [ls,None] :: acc) (fun acc ls -> create_logic_decl [ls,None] :: acc)
[d] !extra_decls in [d] !extra_decls in
extra_decls := []; l in
Trans.decl abstract_decl None Trans.decl abstract_decl None
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