Commit e865c2fa authored by MARCHE Claude's avatar MARCHE Claude
Browse files

gappa support

parent 25f28225
......@@ -54,6 +54,13 @@ theory int.Int
end
theory int.Abs
syntax logic abs "| %1 |"
end
theory real.Real
prelude "# this is a prelude for Gappa real arithmetic"
......
......@@ -33,23 +33,41 @@ open Task
type info = {
info_symbols : Sls.t;
info_ops_of_rel : (string * string) Mls.t;
info_syn : string Mid.t;
info_rem : Sid.t;
}
let int_le = ref ps_equ
let int_ge = ref ps_equ
let int_lt = ref ps_equ
let int_gt = ref ps_equ
let real_le = ref ps_equ
let real_ge = ref ps_equ
let real_lt = ref ps_equ
let real_gt = ref ps_equ
let single_value = ref ps_equ
let get_info =
let arith_symbols = ref None in
let ops_of_rels = ref Mls.empty in
fun env task ->
let l =
match !arith_symbols with
| None ->
| None ->
let int_theory = Env.find_theory env ["int"] "Int" in
let find_int = Theory.ns_find_ls int_theory.Theory.th_export in
let int_add = find_int ["infix +"] in
let int_sub = find_int ["infix -"] in
let int_mul = find_int ["infix *"] in
int_le := Theory.ns_find_ls int_theory.Theory.th_export ["infix <="];
int_ge := Theory.ns_find_ls int_theory.Theory.th_export ["infix >="];
int_lt := Theory.ns_find_ls int_theory.Theory.th_export ["infix <"];
int_gt := Theory.ns_find_ls int_theory.Theory.th_export ["infix >"];
let int_abs_theory = Env.find_theory env ["int"] "Abs" in
let int_abs = Theory.ns_find_ls int_abs_theory.Theory.th_export ["abs"] in
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
......@@ -57,23 +75,45 @@ let get_info =
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 <="];
real_ge := Theory.ns_find_ls real_theory.Theory.th_export ["infix >="];
real_lt := Theory.ns_find_ls real_theory.Theory.th_export ["infix <"];
real_gt := 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
let single_theory = Env.find_theory env ["floating_point"] "Single" in
single_value := Theory.ns_find_ls single_theory.Theory.th_export ["value"];
(* sets of known symbols *)
let l =
List.fold_right Sls.add
[int_add; int_sub; int_mul;
[ps_equ;
int_add; int_sub; int_mul;
!int_le; !int_ge; !int_lt; !int_gt;
int_abs;
real_add; real_sub; real_mul; real_div;
ps_equ;
!real_le;
real_abs] Sls.empty
!real_le; !real_ge; !real_lt; !real_gt;
real_abs;
!single_value] Sls.empty
in
arith_symbols := Some l;
ops_of_rels :=
List.fold_left
(fun acc (ls,op,rev_op) -> Mls.add ls (op,rev_op) acc)
Mls.empty
[ !int_le,"<=",">=" ;
!int_ge,">=","<=" ;
!int_lt,"<",">" ;
!int_gt,">","<" ;
!real_le,"<=",">=" ;
!real_ge,">=","<=" ;
!real_lt,"<",">" ;
!real_gt,">","<" ;
];
l
| Some l -> l
in
{
info_symbols = l;
info_ops_of_rel = !ops_of_rels;
info_syn = get_syntax_map task;
info_rem = get_remove_set task;
}
......@@ -155,16 +195,19 @@ let rec print_fmla info fmt f =
with Not_found ->
fprintf fmt "%a - %a in [0,0]" term t1 term t2
end
| Fapp (ls, [t1;t2]) when ls_equal ls !real_le ->
| Fapp (ls, [t1;t2]) when Mls.mem ls info.info_ops_of_rel ->
let op,rev_op = try Mls.find ls info.info_ops_of_rel
with Not_found -> assert false
in
begin try
let c1 = constant_value t1 in
fprintf fmt "%a >= %s" term t2 c1
fprintf fmt "%a %s %s" term t2 rev_op c1
with Not_found ->
try
let c2 = constant_value t2 in
fprintf fmt "%a <= %s" term t1 c2
fprintf fmt "%a %s %s" term t1 op c2
with Not_found ->
fprintf fmt "%a - %a <= 0" term t1 term t2
fprintf fmt "%a - %a %s 0" term t1 term t2 op
end
| Fapp (ls, tl) ->
begin match query_syntax info.info_syn ls.ls_name with
......@@ -248,10 +291,25 @@ let print_decls ?old info fmt dl =
let filter_hyp eqs hyps pr f =
match f.f_node with
| Fapp(ls,[t1;t2]) when ls == ps_equ -> ((pr,t1,t2)::eqs,hyps)
(* todo: support more kinds of hypotheses *)
| Fapp(ls,[t1;t2]) when ls == ps_equ ->
begin match t1.t_node with
| Tapp(_,[]) ->
((pr,t1,t2)::eqs,hyps)
| _ ->
match t2.t_node with
| Tapp(_,[]) ->
((pr,t2,t1)::eqs,hyps)
| _ -> (eqs, (pr,f)::hyps)
end
(* todo: support more kinds of hypotheses *)
| _ -> (eqs,hyps)
let filter_goal pr f =
match f.f_node with
| Fapp(_,[]) -> None
(* todo: filter more goals *)
| _ -> Some(pr,f)
let prepare ((eqs,hyps,goal) as acc) d =
match d.d_node with
| Dtype _ -> acc
......@@ -264,7 +322,7 @@ let prepare ((eqs,hyps,goal) as acc) d =
| Dprop (Pgoal, pr, f) ->
begin
match goal with
| None -> (eqs,hyps,Some (pr,f))
| None -> (eqs,hyps,filter_goal pr f)
| Some _ -> assert false
end
| Dprop ((Plemma|Pskip), _, _) ->
......@@ -277,14 +335,16 @@ let print_equation info fmt (pr,t1,t2) =
let print_hyp info fmt (pr,f) =
fprintf fmt "# hypothesis '%a'@\n" print_ident pr.pr_name;
fprintf fmt "%a@\n" (print_fmla info) f
fprintf fmt "%a ->@\n" (print_fmla info) f
let print_goal info fmt g =
match g with
| Some(pr,f) ->
fprintf fmt "# goal '%a'@\n" print_ident pr.pr_name;
fprintf fmt "%a@\n" (print_fmla info) f
| None -> assert false
| None ->
fprintf fmt "# (unsupported kind of goal)@\n";
fprintf fmt "1 in [0,0]@\n"
let print_task env pr thpr ?old:_ fmt task =
forget_all ident_printer;
......
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