Commit 6483bd8e authored by MARCHE Claude's avatar MARCHE Claude
Browse files

default tactic in Coq generated files is now "intros" with the appropriate

number and names of hypotheses.

The hypotheses that are conjunctions or exists are also named accordingly
parent a688b474
......@@ -517,10 +517,69 @@ let rec output_remaining fmt ?(in_other=false) script =
| [] ->
if in_other then fprintf fmt "*)@\n"
let rec intros_hyp n fmt f =
match f.t_node with
| Tbinop(Tand,f1,f2) ->
fprintf fmt "@ (";
let m = intros_hyp n fmt f1 in
fprintf fmt ",";
let k = intros_hyp m fmt f2 in
fprintf fmt ")";
k
| Tquant(Texists,fq) ->
let vsl,_trl,f = t_open_quant fq in
fprintf fmt "@ ";
let rec aux n vsl =
match vsl with
| [] -> intros_hyp n fmt f
| v::l ->
fprintf fmt "(%a," print_vs v;
let m = aux n l in
fprintf fmt ")";
m
in
let m = aux n vsl in
List.iter forget_var vsl;
m
| _ ->
fprintf fmt " h%d" n;
n+1
let rec do_intros n fmt fmla =
match fmla.t_node with
| Tlet(_,fb) ->
let vs,f = t_open_bound fb in
fprintf fmt "@ %a" print_vs vs;
do_intros n fmt f;
forget_var vs
| Tquant(Tforall,fq) ->
let vsl,_trl,f = t_open_quant fq in
List.iter
(fun v -> fprintf fmt "@ %a" print_vs v) vsl;
do_intros n fmt f;
List.iter forget_var vsl
| Tbinop(Timplies, f1, f2) ->
let m = intros_hyp n fmt f1 in
do_intros m fmt f2
| _ -> ()
let intros fmt fmla =
match fmla.t_node with
| Tlet _
| Tquant(Tforall,_)
| Tbinop(Timplies, _, _) ->
fprintf fmt "@[intros%a.@]@\n" (do_intros 1) fmla
| _ -> ()
let print_empty_proof fmt def =
if not def then fprintf fmt "intuition.@\n";
fprintf fmt "@\n";
fprintf fmt "%s.@\n" (if def then "Defined" else "Qed")
match def with
| Some fmla ->
intros fmt fmla;
fprintf fmt "@\n";
fprintf fmt "Qed.@\n"
| None ->
fprintf fmt "@\n";
fprintf fmt "Defined.@\n"
let print_previous_proof def fmt previous =
match previous with
......@@ -543,7 +602,7 @@ let print_type_decl ~prev info fmt ts =
| _ ->
fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Definition %a : %aType.@]@\n%a@\n"
print_ts ts print_params_list ts.ts_args
(print_previous_proof true) prev
(print_previous_proof None) prev
else
fprintf fmt "@[<hov 2>Parameter %a : %aType.@]@\n@\n"
print_ts ts print_params_list ts.ts_args
......@@ -590,7 +649,7 @@ let print_param_decl ~prev info fmt ls =
print_ls ls print_params all_ty_params
(print_arrow_list (print_ty info)) ls.ls_args
(print_ls_type ~arrow:(ls.ls_args <> []) info) ls.ls_value
(print_previous_proof true) prev
(print_previous_proof None) prev
else
fprintf fmt "@[<hov 2>Parameter %a: %a%a%a.@]@\n"
print_ls ls print_params all_ty_params
......@@ -674,7 +733,7 @@ let print_prop_decl ~prev info fmt (k,pr,f) =
fprintf fmt "(* Why3 goal *)@\n@[<hov 2>%s %a : %a%a.@]@\n%a@\n"
stt print_pr pr print_params params
(print_fmla info) f
(print_previous_proof false) prev
(print_previous_proof (Some f)) prev
else
fprintf fmt "@[<hov 2>Axiom %a : %a%a.@]@\n@\n"
print_pr pr print_params params
......
......@@ -123,6 +123,15 @@ theory TestFloat
end
theory TestIntros
use import int.Int
goal G :
forall x y : int. x > 0 /\ y > 0 ->
(exists z t:int. x + t = y + z) -> x > y
end
theory TestRealize
......
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