Commit 8beef69f authored by MARCHE Claude's avatar MARCHE Claude

generic abstraction transformation

parent 222a71e7
......@@ -130,7 +130,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
libencoding encoding_decorate encoding_bridge \
encoding_explicit encoding_simple2 \
encoding_instantiate simplify_array filter_trigger \
introduction
introduction abstraction
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify gappa
......
......@@ -19,7 +19,7 @@ transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "introduce_premisses"
transformation "introduce_premises"
theory BuiltIn
syntax type int "int"
......
......@@ -31,73 +31,48 @@ open Task
(* Gappa pre-compilation *)
let term_table = Hterm.create 257
let fmla_table = Hfmla.create 257
type info = {
info_symbols : Sls.t;
info_syn : string Mid.t;
info_rem : Sid.t;
}
(*
let real_abs = ref ps_equ
let real_plus = ref ps_equ
let real_minus = ref ps_equ
*)
let real_le = ref ps_equ
let arith_symbols = ref Sls.empty
let arith_rel_symbols = ref Sls.empty
let extra_decls = ref []
let rec abstract_term t : term =
match t.t_node with
| Tconst _ | Tapp(_,[]) -> t
| Tapp(ls,_) when Sls.mem ls !arith_symbols ->
t_map abstract_term abstract_fmla t
| _ ->
begin try Hterm.find term_table t with Not_found ->
let ls = create_fsymbol (id_fresh "abstr") [] t.t_ty in
let tabs = t_app ls [] t.t_ty in
extra_decls := ls :: !extra_decls;
Hterm.add term_table t tabs;
tabs
end
and abstract_fmla f =
match f.f_node with
| Ftrue | Ffalse -> f
| Fnot _ | Fbinop _ ->
f_map abstract_term abstract_fmla f
| Fapp(ls,_) when Sls.mem ls !arith_rel_symbols ->
f_map abstract_term abstract_fmla f
| _ ->
begin try Hfmla.find fmla_table f with Not_found ->
let ls = create_psymbol (id_fresh "abstr") [] in
let fabs = f_app ls [] in
extra_decls := ls :: !extra_decls;
Hfmla.add fmla_table f fabs;
fabs
end
let abstract_decl (d : decl) : decl list =
let d = decl_map abstract_term abstract_fmla d in
let l =
List.fold_left
(fun acc ls -> create_logic_decl [ls,None] :: acc)
[d]
!extra_decls
in
extra_decls := []; l
let abstraction (t: task) : task =
Hfmla.clear fmla_table;
Hterm.clear term_table;
Trans.apply (Trans.decl abstract_decl None) t
let get_info =
let arith_symbols = ref None in
fun env task ->
let l =
match !arith_symbols with
| None ->
let real_theory = Env.find_theory env ["real"] "Real" in
let find_real = Theory.ns_find_ls real_theory.Theory.th_export in
let real_add = find_real ["infix +"] in
let real_sub = find_real ["infix -"] in
let real_mul = find_real ["infix *"] in
let real_div = find_real ["infix /"] in
real_le := Theory.ns_find_ls real_theory.Theory.th_export ["infix <="];
let real_abs_theory = Env.find_theory env ["real"] "Abs" in
let real_abs = Theory.ns_find_ls real_abs_theory.Theory.th_export ["abs"] in
(* sets of known symbols *)
let l =
List.fold_right Sls.add
[real_add; real_sub; real_mul; real_div;
ls_equ;
!real_le;
real_abs] Sls.empty
in
arith_symbols := Some l;
l
| Some l -> l
in
{
info_symbols = l;
info_syn = get_syntax_map task;
info_rem = get_remove_set task;
}
(* Gappa printing *)
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
}
let ident_printer =
let bls = [
......@@ -261,34 +236,17 @@ let print_decl ?old:_ info fmt =
let print_decls ?old info fmt dl =
fprintf fmt "@[<hov>{ %a }@\n@]" (print_list nothing (print_decl ?old info)) dl
let get_info env task =
let real_theory = Env.find_theory env ["real"] "Real" in
let find_real = Theory.ns_find_ls real_theory.Theory.th_export in
let real_add = find_real ["infix +"] in
let real_sub = find_real ["infix -"] in
let real_mul = find_real ["infix *"] in
let real_div = find_real ["infix /"] in
real_le := Theory.ns_find_ls real_theory.Theory.th_export ["infix <="];
let real_abs_theory = Env.find_theory env ["real"] "Abs" in
let real_abs = Theory.ns_find_ls real_abs_theory.Theory.th_export ["abs"] in
(* sets of known symbols *)
arith_symbols :=
List.fold_right Sls.add
[real_add; real_sub; real_mul; real_div;
real_abs] Sls.empty ;
arith_rel_symbols :=
List.fold_right Sls.add [!real_le] Sls.empty ;
{
info_syn = get_syntax_map task;
info_rem = get_remove_set task;
}
let print_task env pr thpr ?old fmt task =
let task = abstraction task in
forget_all ident_printer;
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let info = get_info env task in
let task =
Abstraction.abstraction
(fun f -> Sls.mem f info.info_symbols)
task
in
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_decls ?old info fmt (Task.task_decls task)
let () = register_printer "gappa" print_task
......
open Ident
open Term
open Decl
open Task
let term_table = Hterm.create 257
let fmla_table = Hfmla.create 257
let extra_decls = ref []
let rec abstract_term keep t : term =
match t.t_node with
| Tconst _ | Tapp(_,[]) -> t
| Tapp(ls,_) when keep ls ->
t_map (abstract_term keep) (abstract_fmla keep) t
| _ ->
begin try Hterm.find term_table t with Not_found ->
let ls = create_fsymbol (id_fresh "abstr") [] t.t_ty in
let tabs = t_app ls [] t.t_ty in
extra_decls := ls :: !extra_decls;
Hterm.add term_table t tabs;
tabs
end
and abstract_fmla keep f =
match f.f_node with
| Ftrue | Ffalse -> f
| Fnot _ | Fbinop _ ->
f_map (abstract_term keep) (abstract_fmla keep) f
| Fapp(ls,_) when keep ls ->
f_map (abstract_term keep) (abstract_fmla keep) f
| _ ->
begin try Hfmla.find fmla_table f with Not_found ->
let ls = create_psymbol (id_fresh "abstr") [] in
let fabs = f_app ls [] in
extra_decls := ls :: !extra_decls;
Hfmla.add fmla_table f fabs;
fabs
end
let abstract_decl keep (d : decl) : decl list =
let d = decl_map (abstract_term keep) (abstract_fmla keep) d in
let l =
List.fold_left
(fun acc ls -> create_logic_decl [ls,None] :: acc)
[d]
!extra_decls
in
extra_decls := []; l
let abstraction (keep : lsymbol -> bool) (t: task) : task =
Hfmla.clear fmla_table;
Hterm.clear term_table;
Trans.apply (Trans.decl (abstract_decl keep) None) t
val abstraction : (Term.lsymbol -> bool) -> Task.task -> Task.task
(** [abstract keep t] applies variable abstraction of the task [t],
that is replaces subterms or subformulas headed by a logic symbol
f that do not satisfies [keep f] into a fresh variable.
Notice that the numeric constants are always kept
Example (approximate syntax):
[abstraction (fun f -> List.mem f ["+";"-"]) "goal x*x+y*y = 1"]
returns ["logic abs1 = x*x; logic abs2 = y*y; goal abs1+abs2 = 1"]
*)
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