Commit d6b474eb authored by DAILLER Sylvain's avatar DAILLER Sylvain

Issue 259

parent 1218b433
......@@ -20,6 +20,8 @@ Transformations
generated ones :x:
* `destruct_rec` applies `destruct` recursively on a goal
* `destruct` now simplifies away equalities on constructors
* `destruct_alg` renamed to `destruct_term`. It also has a new experimental
keyword `using` to name newly destructed elements
Tools
* added a command `why3 session update` to modify sessions from the
......
......@@ -7,13 +7,13 @@
<goal name="g">
<transf name="intros" arg1="l">
<goal name="g.0">
<transf name="destruct_alg" arg1="l">
<transf name="destruct_term" arg1="l">
<goal name="g.0.0">
</goal>
<goal name="g.0.1">
</goal>
</transf>
<transf name="destruct_alg_subst" arg1="l">
<transf name="destruct_term_subst" arg1="l">
<goal name="g.0.0">
</goal>
<goal name="g.0.1">
......
......@@ -341,7 +341,7 @@
<goal name="eval_change_free.0.10.0.0" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="eval_change_free.0.10.0.0.0" proved="true">
<transf name="destruct_alg" proved="true" arg1="x1">
<transf name="destruct_term" proved="true" arg1="x1">
<goal name="eval_change_free.0.10.0.0.0.0" proved="true">
<proof prover="7"><result status="valid" time="0.15"/></proof>
</goal>
......
......@@ -17,7 +17,7 @@
<goal name="size_left" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="size_left.0" proved="true">
<transf name="destruct_alg" proved="true" arg1="t">
<transf name="destruct_term" proved="true" arg1="t">
<goal name="size_left.0.0" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -488,7 +488,7 @@
<goal name="VC sub_valid_coloring_white.8.1" expl="postcondition" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC sub_valid_coloring_white.8.1.0" expl="postcondition" proved="true">
<transf name="destruct_alg" proved="true" arg1="f0">
<transf name="destruct_term" proved="true" arg1="f0">
<goal name="VC sub_valid_coloring_white.8.1.0.0" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
......
......@@ -69,7 +69,7 @@
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC subst_then_rename_composition_lemma_fo_formula.7" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="t">
<transf name="destruct_term_subst" proved="true" arg1="t">
<goal name="VC subst_then_rename_composition_lemma_fo_formula.7.0" expl="postcondition" proved="true">
<transf name="unfold" proved="true" arg1="subst_fo_formula">
<goal name="VC subst_then_rename_composition_lemma_fo_formula.7.0.0" expl="postcondition" proved="true">
......@@ -134,7 +134,7 @@
<proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC subst_composition_lemma_fo_formula.7" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="t">
<transf name="destruct_term_subst" proved="true" arg1="t">
<goal name="VC subst_composition_lemma_fo_formula.7.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="127"/></proof>
</goal>
......@@ -240,7 +240,7 @@
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC renaming_preserve_size_fo_formula.7" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="t">
<transf name="destruct_term_subst" proved="true" arg1="t">
<goal name="VC renaming_preserve_size_fo_formula.7.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="13"/></proof>
</goal>
......
......@@ -55,7 +55,7 @@
<goal name="VC bottomvar.0.0.0.0.0.0.0.0.0" expl="assertion" proved="true">
<transf name="rewrite" proved="true" arg1="&lt;-" arg2="H">
<goal name="VC bottomvar.0.0.0.0.0.0.0.0.0.0" expl="assertion" proved="true">
<transf name="destruct_alg" proved="true" arg1="t">
<transf name="destruct_term" proved="true" arg1="t">
<goal name="VC bottomvar.0.0.0.0.0.0.0.0.0.0.0" expl="assertion" proved="true">
<proof prover="13"><result status="valid" time="0.17"/></proof>
</goal>
......
......@@ -419,7 +419,7 @@
<goal name="Permut_length.0" proved="true">
<transf name="split_vc" proved="true" >
<goal name="Permut_length.0.0" proved="true">
<transf name="destruct_alg" proved="true" arg1="l2">
<transf name="destruct_term" proved="true" arg1="l2">
<goal name="Permut_length.0.0.0" proved="true">
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -69,7 +69,7 @@
<goal name="pigeon_0.0" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="pigeon_0.0.0" proved="true">
<transf name="destruct_alg" proved="true" arg1="l">
<transf name="destruct_term" proved="true" arg1="l">
<goal name="pigeon_0.0.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
......
......@@ -5,7 +5,9 @@
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../sumrange.mlw" proved="true">
<file proved="true">
<path name=".."/>
<path name="sumrange.mlw"/>
<theory name="ArraySum" proved="true">
<goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -178,24 +180,24 @@
<goal name="VC tree_of_array.7" expl="assertion" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC tree_of_array.7.0" expl="assertion" proved="true">
<transf name="destruct_alg" proved="true" arg1="l">
<transf name="destruct_term" proved="true" arg1="l">
<goal name="VC tree_of_array.7.0.0" expl="assertion" proved="true">
<transf name="destruct_alg" proved="true" arg1="r">
<transf name="destruct_term" proved="true" arg1="r" arg2="using" arg3="b1,b2,b3">
<goal name="VC tree_of_array.7.0.0.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC tree_of_array.7.0.0.1" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
<proof prover="3" timelimit="5"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tree_of_array.7.0.1" expl="assertion" proved="true">
<transf name="destruct_alg" proved="true" arg1="r">
<transf name="destruct_term" proved="true" arg1="r">
<goal name="VC tree_of_array.7.0.1.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof>
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC tree_of_array.7.0.1.1" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
......@@ -228,12 +230,12 @@
<goal name="VC query" expl="VC for query" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC query.0" expl="VC for query" proved="true">
<transf name="destruct_alg" proved="true" arg1="t">
<transf name="destruct_term" proved="true" arg1="t">
<goal name="VC query.0.0" expl="VC for query" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC query.0.1" expl="VC for query" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
......@@ -289,12 +291,12 @@
<goal name="VC update" expl="VC for update" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC update.0" expl="VC for update" proved="true">
<transf name="destruct_alg" proved="true" arg1="t">
<transf name="destruct_term" proved="true" arg1="t">
<goal name="VC update.0.0" expl="VC for update" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC update.0.1" expl="VC for update" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
......
......@@ -27,7 +27,7 @@
<proof prover="3"><result status="valid" time="0.01" steps="37"/></proof>
</goal>
<goal name="VC tree_of_list_aux.6" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="l&#39;1">
<transf name="destruct_term_subst" proved="true" arg1="l&#39;1">
<goal name="VC tree_of_list_aux.6.0" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
......
......@@ -91,7 +91,7 @@
<proof prover="2" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC value_in_context.1" expl="precondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="(subst x1 t)">
<transf name="destruct_term_subst" proved="true" arg1="(subst x1 t)">
<goal name="VC value_in_context.1.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -99,7 +99,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC value_in_context.1.2" expl="precondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="x2">
<transf name="destruct_term_subst" proved="true" arg1="x2">
<goal name="VC value_in_context.1.2.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -117,7 +117,7 @@
<proof prover="2" timelimit="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.3" expl="precondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="(subst x t)">
<transf name="destruct_term_subst" proved="true" arg1="(subst x t)">
<goal name="VC value_in_context.3.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -125,7 +125,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC value_in_context.3.2" expl="precondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="x3">
<transf name="destruct_term_subst" proved="true" arg1="x3">
<goal name="VC value_in_context.3.2.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -133,7 +133,7 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC value_in_context.3.2.2" expl="precondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="x4">
<transf name="destruct_term_subst" proved="true" arg1="x4">
<goal name="VC value_in_context.3.2.2.0" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
......@@ -150,7 +150,7 @@
</transf>
</goal>
<goal name="VC value_in_context.4" expl="postcondition" proved="true">
<transf name="destruct_alg_subst" proved="true" arg1="c">
<transf name="destruct_term_subst" proved="true" arg1="c">
<goal name="VC value_in_context.4.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
......
......@@ -318,20 +318,21 @@ let parse_theory env s =
let trans_typ_tail: type a b c. (a -> b, c) trans_typ -> (b, c) trans_typ =
fun t ->
match t with
| Tint t -> t
| Tty t -> t
| Ttysymbol t -> t
| Tprsymbol t -> t
| Tprlist t -> t
| Tlsymbol t -> t
| Tsymbol t -> t
| Tlist t -> t
| Tterm t -> t
| Tstring t -> t
| Tformula t -> t
| Ttheory t -> t
| Ttermlist t -> t
| _ -> assert false
| Tint t -> t
| Tty t -> t
| Ttysymbol t -> t
| Tprsymbol t -> t
| Tprlist t -> t
| Tlsymbol t -> t
| Tsymbol t -> t
| Tlist t -> t
| Tterm t -> t
| Tstring t -> t
| Tformula t -> t
| Ttheory t -> t
| Ttermlist t -> t
| Tidentlist t -> t
| _ -> assert false
type _ trans_typ_is_l = Yes : (task list) trans_typ_is_l | No : task trans_typ_is_l
......@@ -509,6 +510,10 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
| Ttermlist t' ->
let term_list = parse_and_type_list ~as_fmla:false s' tables in
wrap_to_store t' (f (Some term_list)) tail env tables task
| Tidentlist t' ->
let list =
List.map (fun id -> id.Ptree.id_str) (parse_list_ident s') in
wrap_to_store t' (f (Some list)) tail env tables task
| _ -> raise (Arg_expected (string_of_trans_typ t', s'))
end
| Topt (_, t'), _ ->
......
This diff is collapsed.
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