From 8a427f54c82824ba38fbef13d8cfcb253970813a Mon Sep 17 00:00:00 2001
From: Sylvain Dailler <dailler@adacore.com>
Date: Thu, 6 Dec 2018 15:00:26 +0100
Subject: [PATCH] destruct: first step simplification

---
 examples/bts/231_destruct/why3session.xml |  44 ++++++----------------
 examples/bts/231_destruct/why3shapes.gz   | Bin 1042 -> 874 bytes
 src/transform/destruct.ml                 |  44 +++++++++-------------
 3 files changed, 30 insertions(+), 58 deletions(-)

diff --git a/examples/bts/231_destruct/why3session.xml b/examples/bts/231_destruct/why3session.xml
index 26ca725e66..1c8491e8d5 100644
--- a/examples/bts/231_destruct/why3session.xml
+++ b/examples/bts/231_destruct/why3session.xml
@@ -52,19 +52,23 @@
 </theory>
 <theory name="Unsoundness">
  <goal name="t1">
+ <transf name="destruct_rec" arg1="H">
+  <goal name="t1.0">
+  <transf name="destruct_rec" arg1="H1">
+   <goal name="t1.0.0" expl="destruct premise">
+   </goal>
+   <goal name="t1.0.1">
+   </goal>
+  </transf>
+  </goal>
+ </transf>
  </goal>
 </theory>
 <theory name="Incompleteness">
  <goal name="t1">
  <transf name="destruct_rec" arg1="H">
-  <goal name="t1.0" expl="destruct premise">
-  <proof prover="0"><result status="unknown" time="0.00"/></proof>
-  </goal>
-  <goal name="t1.1" expl="destruct premise">
-  <proof prover="0"><result status="unknown" time="0.00"/></proof>
-  </goal>
-  <goal name="t1.2" proved="true">
-  <proof prover="0"><result status="valid" time="0.00"/></proof>
+  <goal name="t1.0">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.00"/></proof>
   </goal>
  </transf>
  </goal>
@@ -141,29 +145,5 @@
  </transf>
  </goal>
 </theory>
-<theory name="Tsurfail">
- <goal name="t">
- <transf name="destruct_rec" arg1="H">
-  <goal name="t.0" expl="destruct premise">
-  </goal>
-  <goal name="t.1" expl="destruct premise">
-  </goal>
-  <goal name="t.2">
-  </goal>
- </transf>
- </goal>
-</theory>
-<theory name="Tfail">
- <goal name="G">
- <transf name="destruct_rec" arg1="H">
-  <goal name="G.0" expl="destruct premise">
-  </goal>
-  <goal name="G.1" expl="destruct premise">
-  </goal>
-  <goal name="G.2">
-  </goal>
- </transf>
- </goal>
-</theory>
 </file>
 </why3session>
diff --git a/examples/bts/231_destruct/why3shapes.gz b/examples/bts/231_destruct/why3shapes.gz
index 7c833ebc3d6777a168e784f90a00517b9e71ee75..d956b26bf7a37bd423cdbfae680ee9a00633d4ed 100644
GIT binary patch
literal 874
zcmb2|=3oGW|7$~c_sO{PoO!SPPI%UvG;>J{(+4MJetO0okl;Ka#bN&YS;c8Tb=cX;
z#H<<QUBfn-O(}i5b>*>Cxr@#1n<T#T<jbx9{`mdhkGEg@J38*a<Nx{k@6L}GPDdFp
zzb16jRO?Lj+>OV?;=k+MUmqF2ukN4nzI}DSV)obm3G$!x&ehOV=i;`h)~T^dqCxYL
zzSwV1{`4xlk5jvQ#g3WB3ir=Fdh`E;Bl^}kYTE=&<R&!V-urH=;WD-NKkeLhm+YB8
z)64JZUMJ`G9APsZYww-kv$tQ*@9nO;R@3t0)`)F)$vOUe<{ryyg8A#MG>TRg-P|{6
zrP`|Z>1C@{#Xrs3e{btEnQXb^(_BA4+rPlJ+jGLnjf*!vHj<49cb&1TUVj$<<CC?&
zm+?PN@0rbPyGs3e%B-DtqIBPH35>n3|LQ%fNA`zWHHNL8%ae73ts>&25B%S7AjVY9
zmtXF!`)b$qM~>VU@p)#i6R@)U<lUIde&?hF7i4jB$gnT^m)LlA!l`-HQv~g}S+0C_
z&G8izw(byDoEda-xks#d=jBd5%@5KSe;(<19d&Ox>uz)1D9u+Vbtk|6^egW1ch^ei
zlVvlE(o|ipy<TT}ZC}joS1WIKKfbep*Y}F&{K;S2ZZO{JJ)^F+Y;(6Sm;FlhvhW2T
zLg%Pk-BE9gU}Krf&dxV0Rm^SKg@@77ta1DIEm(Zts+c`CW~sVcaJKZ7X9nsm1`%Q_
zZhu>2vG>=no!oVy+*67bjx7A%UHeJN+F~#B1&hxDKO_xoLa*&ncRe-LIOBEX+sit~
zJgjYn6vfRFZRV(?ls+qI*1wh{JvaCnbGX8fN5VIEdwH^@F6QXr<hr)p>-|34>GDjR
z)_i8q(=@h9TBX-X3Cem)oNam4YSrZF8=WO^K-g(b+H{xuQ5)9XEK5u`cwv3u%8%6-
z3tOEsE-3wYe1Y@CTn3f&&vk8nmWNd~#%Ht@sw{o8tyQ3M;kD&nzB|~v^_sPh-#ah(
ziczv=+tbal9(Rwey!Y<qPlK)N#CRn0M7{E>7pf*-ZL538Ciy(z@al(NbC@^$m%dY2
z?BK+`V*7`?hSwv-?Ony@|4dkzafXpUak9jrz=wUuCQmXu?RcW|mIKq-cQUu<e9&*)
pIP)#Xg*)a<t1`PS`NZvlDw+8HcQ~`X3l#XIK67$mv>ZDF0{}s(sEGgo

literal 1042
zcmb2|=3oGW|7$~c_r;j=ynU|yP1vPt$_b@hhVYknyhS*7cqH85dvN~zMK(63_jzWn
z4KuqdJ48-?PLP<*BRM74aQlj5XCvmWKCYMN|N650*O$L9>pMEiUwi)V_OCM)mz|f)
z&(mDx9@X}K(#<8jcQ-A2^ReX9>+SmW$F?s&AOGpQfBa{*n*v>V581CzE0mq;n&NdV
zcJ9CDuV<89`_#+#StYQ@aO=+Rt0vdHnyOIO^P$e5cR^WqPE7UlsC!Y{4=>&yyI6nL
z?mYjM#>u)%(^j+2{<dINzWX|<%Psw(>$I|ynp@8%FJ0ANVLgex-RJIBWA#aA&M4bW
zo0q&UE#Li`;pV+Po4?(fdZ~J{o%ymgW!HXA&suJvsbuLUk~Sxg_wgx??R(=VJxkub
z@x1@98+ER`mp|-Vb8fluSLNHM|EzhZs~ykx>N!iw&5FBx3~v`kDn4=(KCJEj@x9uM
zNo#}eA6)xwi_X@i7eB7mwz~aZ?L@M73GcagpTFb?He_iq<OnaRGe4LRkox7~B~E=t
zhMn64swcW1=Xn%($T0i|gP!I2cXM-Ff4Ll);q(1WSC`d+2M*h&++NY^m-TMNy7WCy
zepFpK(c>u~z^r#W+&#ec``o)fE}Wk6_rZr}^D-)ap6Zr7q1o}NFFy57RL9oFJ?Tzo
z8bYcU*>Yu9N4Vbizb|*Vc>SDO7F~@3d6E3Mdn;=0o7|V<aS`?T7X43W<<{py6~SB&
zo*tOUo2P%KueHW0P55x*66c4pD;}mz-1jW-sKXBy-q}GJ7Zz`Qy!qBa!7YyGawoTW
z&Aq(+Fmv#Y=(+3uPFt-|{;8)pJ#9&^pCYFZN6yySOWoGK+N553PEeR5w|t2dkDu}V
z?v7>hGrZUjPt|HVdB<zBV3)eg$2U`@T4x?wR`s)~^k7eTw$ZKo;%9SbwM%gx<eptR
zC5D~#rHoD9W%u-A+ZpR0@o^~iZs%8>6O-`l>?B#ggISLX9!NaqI;VEvf#sh&FPkjx
zrCq!6`%Ur0NvWKlTa8;Ueva|j;>lMaddl8VU9?7$@5u6nZ~lknMKAx@(5J?6BHLxU
zCbxWOYx@4J0V2N|;x}ZQJUwwkTD;uKBtpIK%!x*?1-*s0KKS0?$e4X|`J!20c^t%e
zzw%BzWc=w&!|eE?jOK4&(jqetKe^d8?fa`*<I1m+OOmP*MRw-2U2ojf=*v>^QQROm
zZSCegYNiJjwo4tm>vfK?Hz}+At=vPK2|v4Me7@nGGgBkI=g6am(03buPr7q`@%xB(
zO>zt7G+gJEaO^+9bFNHE`_ogUzc=f=_zh-rCJ9}e<)F<ui#67Juf+aM{@1_r+t2&c
zf4+ignIo@4nbYI~ho&_y4a?Ubx^P|l<*$C1{zhLW>GlaKoJtJ~SsIS%O*C2fefCdo
Ny`xjak8v<C003}U5<LI_

diff --git a/src/transform/destruct.ml b/src/transform/destruct.ml
index 9872abaa98..f591c97964 100644
--- a/src/transform/destruct.ml
+++ b/src/transform/destruct.ml
@@ -149,24 +149,22 @@ let destruct_term ~recursive (t: term) =
     l.ls_constr <> 0
   in
 
-  (* Check if a new goal is created in the branch *)
-  let contains_goal l =
-    List.exists (fun x -> match x with | Goal_term _ -> true | _ -> false) l
-  in
-
-  (* Main function *)
-  let rec destruct_term (t: term) =
-    let destruct_term_exception t =
+  (* Main recursive function:
+     [toplevel] when true, removing implications is allowed. Become false as
+     soon as we destruct non-implication construct
+  *)
+  let rec destruct_term ~toplevel (t: term) =
+    let destruct_term_exception ~toplevel t =
       if not recursive then [[Axiom_term t]] else
-        match destruct_term t with
+        match destruct_term ~toplevel t with
         | exception _ -> [[Axiom_term t]]
         | l -> l
     in
 
     match t.t_node with
     | Tbinop (Tand, t1, t2) ->
-        let l1 = destruct_term_exception t1 in
-        let l2 = destruct_term_exception t2 in
+        let l1 = destruct_term_exception ~toplevel:false t1 in
+        let l2 = destruct_term_exception ~toplevel:false t2 in
         (* For each parallel branch of l1 we have to append *all* parallel
            branch of l2 which are not new goals. In case of new goals, we are
            not allowed to use the left/right conclusions to prove the goal.
@@ -177,25 +175,19 @@ let destruct_term ~recursive (t: term) =
         (* TODO efficiency: this is not expected to work on very large terms
            with tons of Tand/Tor. *)
         List.fold_left (fun par_acc seq_list1 ->
-            if contains_goal seq_list1 then
-              par_acc @ [seq_list1]
-            else
-              List.fold_left (fun par_acc seq_list2 ->
-                  if contains_goal seq_list2 then
-                    par_acc @ [seq_list2]
-                  else
-                    par_acc @ [seq_list1 @ seq_list2]) par_acc l2
+            List.fold_left (fun par_acc seq_list2 ->
+                par_acc @ [seq_list1 @ seq_list2]) par_acc l2
           ) [] l1
     | Tbinop (Tor, t1, t2) ->
-        let l1 = destruct_term_exception t1 in
-        let l2 = destruct_term_exception t2 in
+        let l1 = destruct_term_exception ~toplevel:false t1 in
+        let l2 = destruct_term_exception ~toplevel:false t2 in
         (* The two branch are completely disjoint. We just concatenate them to
            ensure they are done in parallel *)
         l1 @ l2
-    | Tbinop (Timplies, t1, t2) ->
+    | Tbinop (Timplies, t1, t2) when toplevel ->
         (* The premises is converted to a goal. The rest is recursively
            destructed in parallel. *)
-        let l2 = destruct_term_exception t2 in
+        let l2 = destruct_term_exception ~toplevel t2 in
         [Goal_term t1] :: l2
     | Tquant (Texists, tb) ->
       let (vsl, tr, te) = Term.t_open_quant tb in
@@ -209,7 +201,7 @@ let destruct_term ~recursive (t: term) =
            let new_t = t_quant_close Texists tl tr part_t in
            (* The recursive call is done after new symbols are introduced so we
               readd the new decls to every generated list. *)
-           let l_t = destruct_term_exception new_t in
+           let l_t = destruct_term_exception ~toplevel:false new_t in
            List.map (fun x -> Param x_decl :: x) l_t
          with
          | Ty.TypeMismatch (ty1, ty2) ->
@@ -237,7 +229,7 @@ let destruct_term ~recursive (t: term) =
     | Tnot {t_node = Tapp (ls,
                   [{t_node = Tapp (cs1, _); _}; {t_node = Tapp (cs2, _); _}]); _}
         when ls_equal ls ps_equ && is_constructor cs1 && is_constructor cs2 ->
-      (* Cs1 [l1] <> Cs2 [l2] *)
+      (* Cs1 [l1] = Cs2 [l2] *)
       if ls_equal cs1 cs2 then
         [[Axiom_term t]]
       else
@@ -245,7 +237,7 @@ let destruct_term ~recursive (t: term) =
         [[]]
     | _ -> raise (Arg_trans ("destruct"))
   in
-  destruct_term t
+  destruct_term ~toplevel:true t
 
 (* Destruct the head term of an hypothesis if it is either
    conjunction, disjunction or exists *)
-- 
GitLab