From 0a4ec4c277586ee0f9b7ec35569f3143b7b1d87a Mon Sep 17 00:00:00 2001
From: Sylvain Dailler <dailler@adacore.com>
Date: Thu, 25 Apr 2019 12:44:50 +0200
Subject: [PATCH] destruct: now destruct "true" and "false"

Also add tests for not, true and false
---
 CHANGES.md                                |   1 +
 examples/bts/311_destruct.mlw             |  20 ++++++++++
 examples/bts/311_destruct/why3session.xml |  44 ++++++++++++++++++++++
 examples/bts/311_destruct/why3shapes.gz   | Bin 0 -> 183 bytes
 src/transform/destruct.ml                 |   4 ++
 5 files changed, 69 insertions(+)
 create mode 100644 examples/bts/311_destruct.mlw
 create mode 100644 examples/bts/311_destruct/why3session.xml
 create mode 100644 examples/bts/311_destruct/why3shapes.gz

diff --git a/CHANGES.md b/CHANGES.md
index d9d4b8a0e..a0ca883cb 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -34,6 +34,7 @@ Transformations
     generalize in the induction
   * `destruct` now destruct `not p` into `p -> false`. `destruct_rec` is
      allowed to further destruct afterwards.
+    `destruct` can also destruct `true` and `false`.
 
 IDE
   * display of counterexamples in the Task view has been improved
diff --git a/examples/bts/311_destruct.mlw b/examples/bts/311_destruct.mlw
new file mode 100644
index 000000000..35e146cc0
--- /dev/null
+++ b/examples/bts/311_destruct.mlw
@@ -0,0 +1,20 @@
+use list.List
+use list.Length
+use int.Int
+
+constant x: int
+
+predicate p int
+
+axiom H: not (p 0)
+axiom H1: p 0
+
+goal g: false
+
+axiom H2: false
+
+goal g5: p 5
+
+axiom H3: true
+
+goal g6: p 5
diff --git a/examples/bts/311_destruct/why3session.xml b/examples/bts/311_destruct/why3session.xml
new file mode 100644
index 000000000..8b4a06f76
--- /dev/null
+++ b/examples/bts/311_destruct/why3session.xml
@@ -0,0 +1,44 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="6">
+<prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="20" steplimit="0" memlimit="1000"/>
+<file proved="true">
+<path name=".."/>
+<path name="311_destruct.mlw"/>
+<theory name="Top" proved="true">
+ <goal name="g" proved="true">
+ <transf name="destruct" proved="true" arg1="H">
+  <goal name="g.0" proved="true">
+  <transf name="destruct" proved="true" arg1="H">
+   <goal name="g.0.0" expl="destruct premise" proved="true">
+   <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+   </goal>
+   <goal name="g.0.1" proved="true">
+   <transf name="destruct" proved="true" arg1="H">
+   </transf>
+   </goal>
+  </transf>
+  </goal>
+ </transf>
+ <transf name="destruct_rec" proved="true" arg1="H">
+  <goal name="g.0" expl="destruct premise" proved="true">
+  <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="g5" proved="true">
+ <transf name="destruct" proved="true" arg1="H2">
+ </transf>
+ </goal>
+ <goal name="g6" proved="true">
+ <transf name="destruct" proved="true" arg1="H3">
+  <goal name="g6.0" proved="true">
+  <transf name="destruct" proved="true" arg1="H2">
+  </transf>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>
diff --git a/examples/bts/311_destruct/why3shapes.gz b/examples/bts/311_destruct/why3shapes.gz
new file mode 100644
index 0000000000000000000000000000000000000000..4361a775f134dd7a0dafcf8cd2bd30e62bdf0f8e
GIT binary patch
literal 183
zcmV;o07(BIiwFP!00000|DBJ?ZA38)L+`(eUxF6flFQKw<PcymGwDAL(m)U%iARED
z0Wp+yL{MzDMvO#aM{O*;`!Xf(ocmbQwcC*f=psq4nM4Pn3^j~S=Gr@?2WAFCROjeP
zch>9u{EGMec-H5~tLzbQrIv~>=d^G}W@{eVI5*UZ&VLv09FX<1I)>F`RvC!0<*c^A
lbsuV8)6d5!2TraWo=w>bpjBbA;FtPa*EfVlK@3L$0047~Rh9q%

literal 0
HcmV?d00001

diff --git a/src/transform/destruct.ml b/src/transform/destruct.ml
index ccafad935..e90fb3f12 100644
--- a/src/transform/destruct.ml
+++ b/src/transform/destruct.ml
@@ -248,6 +248,10 @@ let destruct_fmla ~recursive (t: term) =
     in
 
     match t.t_node with
+    | Tfalse ->
+        []
+    | Ttrue ->
+        [[]]
     | Tbinop (Tand, t1, t2) ->
         let l1 = destruct_fmla_exception ~toplevel:false t1 in
         let l2 = destruct_fmla_exception ~toplevel:false t2 in
-- 
GitLab