Commit 1fb76be3 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Make Gappa transformations self-contained. Better names wanted.

parent 90b9e0a6
......@@ -21,12 +21,15 @@ transformation "eliminate_algebraic_smt"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_unknown_lsymbols"
transformation "simplify_trivial_quantification"
transformation "introduce_premises"
transformation "abstract_unknown_lsymbols"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (=) "(%1 = %2)"
syntax logic (=) "dummy"
end
theory int.Int
......@@ -41,6 +44,11 @@ theory int.Int
syntax logic (*) "(%1 * %2)"
syntax logic (-_) "(-%1)"
syntax logic (<=) "dummy"
syntax logic (>=) "dummy"
syntax logic (<) "dummy"
syntax logic (>) "dummy"
meta "gappa arith" logic (<=), "", "<=", ">="
meta "gappa arith" logic (>=), "", ">=", "<="
meta "gappa arith" logic (<), "not ", ">=", "<="
......@@ -97,6 +105,11 @@ theory real.Real
syntax logic (-_) "(-%1)"
syntax logic inv "(1.0 / %1)"
syntax logic (<=) "dummy"
syntax logic (>=) "dummy"
syntax logic (<) "dummy"
syntax logic (>) "dummy"
meta "gappa arith" logic (<=), "", "<=", ">="
meta "gappa arith" logic (>=), "", ">=", "<="
meta "gappa arith" logic (<), "not ", ">=", "<="
......
......@@ -29,6 +29,26 @@ open Decl
open Theory
open Task
let syntactic_transform transf =
Trans.on_meta meta_syntax_logic (fun metas ->
let symbols = List.fold_left (fun acc meta_arg ->
match meta_arg with
| [MAls ls; MAstr _] -> Sls.add ls acc
| _ -> assert false) Sls.empty metas in
transf (fun ls -> Sls.mem ls symbols))
let () =
Trans.register_transform "abstract_unknown_lsymbols"
(syntactic_transform Abstraction.abstraction);
Trans.register_transform "simplify_unknown_lsymbols"
(syntactic_transform (fun check_ls -> Trans.goal (fun pr f ->
[create_prop_decl Pgoal pr (Simplify_formula.fmla_cond_subst
(fun t _ -> match t.t_node with
| Tconst _ | Tapp(_,[]) -> false
| Tapp(ls,_) -> not (check_ls ls)
| _ -> true) true f)
])))
(* Gappa pre-compilation *)
type info = {
......@@ -325,20 +345,6 @@ let print_goal info fmt g =
let print_task env pr thpr ?old:_ fmt task =
forget_all ident_printer;
let info = get_info env task in
let task = Trans.apply (Trans.goal (fun pr f ->
[create_prop_decl Pgoal pr (Simplify_formula.fmla_cond_subst
(fun t _ -> match t.t_node with
| Tconst _ | Tapp(_,[]) -> false
| Tapp(ls,_) -> not (Sid.mem ls.ls_name info.info_symbols)
| _ -> true) true f)
])) task in
let task = Trans.apply (Trans.lookup_transform "introduce_premises" env) task in
let task = Trans.apply (Abstraction.abstraction
(fun ls -> Sid.mem ls.ls_name info.info_symbols)
) task in
(*
eprintf "Abstraction: @\n%a@." Pretty.print_task task;
*)
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let equations,hyps,goal =
......
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