Coq output: recursive definitions

introduced new transformation eliminate_non_struct_recursion for that purpose
uses Decl.check_termination tomake the check and the pretty-print
(could probably be improved to avoid 3 calls to check_termination)
parent c6f06bc6
......@@ -15,7 +15,7 @@ prelude "(* Beware! Only edit allowed sections below *)"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
......
......@@ -22,15 +22,13 @@ Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Parameter length: forall (a:Type), (list a) -> Z.
Implicit Arguments length.
Axiom length_def : forall (a:Type), forall (l:(list a)),
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => ((length l) = 0%Z)
| Cons _ r => ((length l) = (1%Z + (length r))%Z)
| Nil => 0%Z
| Cons _ r => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
......@@ -107,7 +105,7 @@ injection H4; intros; subst; clear H4.
clear H0 H1.
left.
split.
rewrite (length_def _ (Cons 0%Z s)) in H.
replace (length (Cons 0 s))%Z with (1 + length s)%Z in H by auto.
generalize (Length_nonnegative _ s).
omega.
red; intuition.
......
......@@ -22,15 +22,13 @@ Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Parameter length: forall (a:Type), (list a) -> Z.
Implicit Arguments length.
Axiom length_def : forall (a:Type), forall (l:(list a)),
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => ((length l) = 0%Z)
| Cons _ r => ((length l) = (1%Z + (length r))%Z)
| Nil => 0%Z
| Cons _ r => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
......
......@@ -22,15 +22,13 @@ Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Parameter length: forall (a:Type), (list a) -> Z.
Implicit Arguments length.
Axiom length_def : forall (a:Type), forall (l:(list a)),
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => ((length l) = 0%Z)
| Cons _ r => ((length l) = (1%Z + (length r))%Z)
| Nil => 0%Z
| Cons _ r => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
......@@ -111,7 +109,7 @@ destruct s.
discriminate H9.
injection H9; intros; subst; clear H9.
injection H4; intros; subst; clear H4.
rewrite (length_def _ (Cons result result1)) in H.
replace (length (Cons result result1)) with (1 + length result1)%Z in H by auto.
assert (h: (j < i \/ j= i)%Z) by omega; destruct h.
apply (H5 j); auto with *.
subst j.
......
......@@ -5,12 +5,12 @@
<theory name="WP SearchingALinkedList" verified="true" expanded="true">
<goal name="WP_parameter search" expl="correctness of parameter search" sum="b18cebb97e00a1e783a6d9e22c903f53" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.08"/>
</proof>
</goal>
<goal name="WP_parameter search_list" expl="normal postcondition" sum="52cafa4ec08e9cb5ba5ab8b18ba98999" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter head" expl="correctness of parameter head" sum="32073659366e07f8930bc46bbbdc0c06" proved="true" expanded="true">
......@@ -20,14 +20,14 @@
</goal>
<goal name="WP_parameter tail" expl="correctness of parameter tail" sum="bfe94939f47572f7f11a0005955ffa89" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search_loop" expl="correctness of parameter search_loop" sum="1441516fd72abf2ba244d02af8298031" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter search_loop.1" expl="loop invariant init" sum="4cd1dceb71058395e0527f73f3b574cd" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.2" expl="precondition" sum="fc6e89757636384e8b24752371051e9a" proved="true" expanded="true">
......@@ -37,29 +37,29 @@
</goal>
<goal name="WP_parameter search_loop.3" expl="precondition" sum="129090f5652302694bf3811abe1c9ce4" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.4" expl="loop invariant preservation" sum="40ea58a143ac51498184e1afe8663b9c" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter search_loop.4.1" expl="correctness of parameter search_loop" sum="baad18b5ed9a120e82c80b2b91c50276" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.4.2" expl="correctness of parameter search_loop" sum="fce9d8ed2156927f6c579d1effbefdbb" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.4.3" expl="correctness of parameter search_loop" sum="cdd6cbd0040317bb8b8d856f194f9842" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="vstte10_search_list_WP_SearchingALinkedList_WP_parameter_search_loop_3.v" obsolete="false">
<result status="valid" time="0.64"/>
<result status="valid" time="0.56"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.4.4" expl="correctness of parameter search_loop" sum="ba982d035a77f449546f4c3b09056017" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="vstte10_search_list_WP_SearchingALinkedList_WP_parameter_search_loop_4.v" obsolete="false">
<result status="valid" time="0.75"/>
<result status="valid" time="0.66"/>
</proof>
</goal>
</transf>
......@@ -68,39 +68,39 @@
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter search_loop.5.1" expl="correctness of parameter search_loop" sum="692a1d4b26dbb0198ad7c4e5c25b50e5" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.5.2" expl="correctness of parameter search_loop" sum="2ea83eb736d03f87ba5c008d0f7bdb6f" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter search_loop.6" expl="normal postcondition" sum="9ce3e171c2688e14d045da79bf3aba7b" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="vstte10_search_list_WP_SearchingALinkedList_WP_parameter_search_loop_1.v" obsolete="false">
<result status="valid" time="0.67"/>
<result status="valid" time="0.58"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.7" expl="precondition" sum="c5e028bd52e27f43d1defbe4d203db30" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.8" expl="loop invariant preservation" sum="d3023c419e3bb0199f1cee32ea2b13f4" proved="true" expanded="true">
<proof prover="cvc3" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.9" expl="loop variant decreases" sum="c96f3a0c4bcec886ef64c573f89d591b" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.10" expl="normal postcondition" sum="7001416bd907367149cb736ecd0e6dd3" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
......
......@@ -471,11 +471,42 @@ let print_logic_decl ~old info fmt (ls,ld) =
print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params;
fprintf fmt "@\n"
let print_logic_decl ~old info fmt d =
if not (Sid.mem (fst d).ls_name info.info_rem) then
(print_logic_decl ~old info fmt d; forget_tvs ())
let print_recursive_decl info tm fmt (ls,ld) =
let _, _, all_ty_params = ls_ty_vars ls in
let il = try Mls.find ls tm with Not_found -> assert false in
let i = match il with [i] -> i | _ -> assert false in
begin match ld with
| Some ld ->
let vl,e = open_ls_defn ld in
fprintf fmt "%a%a%a {struct %a}: %a :=@ %a.@]@\n"
print_ls ls
print_ne_params all_ty_params
(print_space_list (print_vsty info)) vl
print_vs (List.nth vl i)
(print_ls_type info) ls.ls_value
(print_expr info) e;
List.iter forget_var vl
| None ->
assert false
end
let print_recursive_decl info fmt dl =
let tm = check_termination dl in
let d, dl = match dl with d :: dl -> d, dl | [] -> assert false in
fprintf fmt "Set Implicit Arguments.@\n";
fprintf fmt "@[<hov 2>Fixpoint ";
print_recursive_decl info tm fmt d; forget_tvs ();
List.iter
(fun d ->
fprintf fmt "@[<hov 2>with ";
print_recursive_decl info tm fmt d; forget_tvs ())
dl;
fprintf fmt "Unset Implicit Arguments.@\n@\n"
let print_ind info fmt (pr,f) =
fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr (print_fmla info) f
......@@ -510,10 +541,16 @@ let print_proof ~old info fmt = function
| Pskip -> ()
let print_decl ~old info fmt d = match d.d_node with
| Dtype tl -> print_list nothing (print_type_decl ~old info) fmt tl
| Dlogic ll -> print_list nothing (print_logic_decl ~old info) fmt ll
| Dind il -> print_list nothing (print_ind_decl info) fmt il
| Dprop (_,pr,_) when Sid.mem pr.pr_name info.info_rem -> ()
| Dtype tl ->
print_list nothing (print_type_decl ~old info) fmt tl
| Dlogic [s,_ as ld] when not (Sid.mem s.ls_name d.d_syms) ->
print_logic_decl ~old info fmt ld
| Dlogic ll ->
print_recursive_decl info fmt ll
| Dind il ->
print_list nothing (print_ind_decl info) fmt il
| Dprop (_,pr,_) when Sid.mem pr.pr_name info.info_rem ->
()
| Dprop (k,pr,f) ->
let params = t_ty_freevars Stv.empty f in
fprintf fmt "@[<hov 2>%a %a : %a%a.@]@\n%a"
......
......@@ -91,6 +91,19 @@ let elim_recursion d = match d.d_node with
| Dlogic l when List.length l > 1 -> elim_decl true true l
| _ -> [d]
let is_struct dl =
try
Mls.for_all (fun _ il -> List.length il = 1) (check_termination dl)
with NoTerminationProof _ ->
false
let elim_non_struct_recursion d = match d.d_node with
| Dlogic ((s,_) :: _ as dl)
when Sid.mem s.ls_name d.d_syms && not (is_struct dl) ->
elim_decl true true dl
| _ ->
[d]
let elim_mutual d = match d.d_node with
| Dlogic l when List.length l > 1 -> elim_decl true true l
| _ -> [d]
......@@ -99,6 +112,7 @@ let eliminate_definition_func = Trans.decl (elim true false) None
let eliminate_definition_pred = Trans.decl (elim false true) None
let eliminate_definition = Trans.decl (elim true true) None
let eliminate_recursion = Trans.decl elim_recursion None
let eliminate_non_struct_recursion = Trans.decl elim_non_struct_recursion None
let eliminate_mutual_recursion = Trans.decl elim_mutual None
let () =
......@@ -110,6 +124,8 @@ let () =
eliminate_definition;
Trans.register_transform "eliminate_recursion"
eliminate_recursion;
Trans.register_transform "eliminate_non_struct_recursion"
eliminate_non_struct_recursion;
Trans.register_transform "eliminate_mutual_recursion"
eliminate_mutual_recursion
theory TestCoq
use import list.List
use import list.Append
lemma append_nil: forall l: list 'a. Nil ++ l = l
end
theory Bijection
use export int.Int
function n : int
......
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