Destruct conditionals and match expressions

Fixes #264

examples/bts/264_destruct_if.mlw

+
+constant x: int
+
+predicate p int
+
+axiom H: if x = 42 then p 1 else p 2
+
+goal g: p 3
+
+use list.List
+use list.Length
+use int.Int
+
+constant l: list int
+
+axiom H': match l with
+| Nil -> p 4
+| Cons x y -> p (x+length y)
+| Cons _ (Cons y Nil) -> p y
+| Cons x (Cons y z) -> p (x+y+length z)
+| Cons _ (Cons _ (Cons _ _)) -> p 5
+end
+
+goal g': p 6
+
+axiom H'': match l with
+| Nil -> p 1
+| Cons x Nil | Cons _ (Cons x Nil) -> p x
+| Cons _ (Cons _ _ as l') -> p (length l')
+end
+
+goal g'': p 7
+
+axiom H''': match l with
+| Cons _ (Cons _ _ as l') as l'' -> p (length l'+length l'')
+| _ -> p 0
+end
+
+goal g''': p 8
\ No newline at end of file

examples/bts/264_destruct_if/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<file>
+<path name=".."/>
+<path name="264_destruct_if.mlw"/>
+<theory name="Top">
+ <goal name="g">
+ <transf name="destruct" arg1="H">
+  <goal name="g.0">
+  </goal>
+  <goal name="g.1">
+  </goal>
+ </transf>
+ </goal>
+ <goal name="g&#39;">
+ <transf name="destruct" arg1="H&#39;">
+  <goal name="g&#39;.0">
+  </goal>
+  <goal name="g&#39;.1">
+  </goal>
+  <goal name="g&#39;.2">
+  </goal>
+  <goal name="g&#39;.3">
+  </goal>
+  <goal name="g&#39;.4">
+  </goal>
+ </transf>
+ </goal>
+ <goal name="g&#39;&#39;">
+ <transf name="destruct" arg1="H&#39;&#39;">
+  <goal name="g&#39;&#39;.0">
+  </goal>
+  <goal name="g&#39;&#39;.1">
+  </goal>
+  <goal name="g&#39;&#39;.2">
+  </goal>
+  <goal name="g&#39;&#39;.3">
+  </goal>
+ </transf>
+ </goal>
+ <goal name="g&#39;&#39;&#39;">
+ <transf name="destruct" arg1="H&#39;&#39;&#39;">
+  <goal name="g&#39;&#39;&#39;.0">
+  </goal>
+  <goal name="g&#39;&#39;&#39;.1">
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>

src/transform/destruct.ml

@@ -268,6 +268,59 @@ let destruct_fmla ~recursive (t: term) =
       else
         (* The hypothesis is trivial because Cs1 <> Cs2 thus useless *)
         [[]]
+    | Tif (t1, t2, t3) -> [
+        [Axiom_term t1; Axiom_term t2];
+        [Axiom_term (t_not t1); Axiom_term t3];
+      ]
+    | Tcase (t, tbs) ->
+        let for_case tb =
+          let p, t' = t_open_branch tb in
+          let rec expand p : ((vsymbol option * lsymbol) list * (vsymbol * lsymbol * term) list * term) list =
+            match p.pat_node with
+            | Pwild ->
+                let id = Ident.id_fresh "_" in
+                let ls = create_lsymbol id [] (Some p.pat_ty) in
+                [[None, ls], [], t_app ls [] ls.ls_value]
+            | Pvar v ->
+                let id = Ident.id_clone v.vs_name in
+                let ls = create_lsymbol id [] (Some p.pat_ty) in
+                [[Some v, ls], [], t_app ls [] ls.ls_value]
+            | Papp (ls, args) ->
+                let rec aux args =
+                  match args with
+                  | [] -> [[], [], []] (* really. *)
+                  | arg::args' ->
+                      let l1 = expand arg in
+                      let l2 = aux args' in
+                      List.flatten
+                        (List.map (fun (x, eqs, t) ->
+                             List.map (fun (y, eqs', l) ->
+                                 x@y, eqs@eqs', t::l)
+                               l2)
+                            l1)
+                in
+                List.map (fun (bds, eqs, args) -> bds, eqs, t_app ls args (Some p.pat_ty)) (aux args)
+            | Por (p1, p2) ->
+                let l1 = expand p1 in
+                let l2 = expand p2 in
+                l1 @ l2
+            | Pas (p, v) ->
+                let id = Ident.id_clone v.vs_name in
+                let ls = create_lsymbol id [] (Some p.pat_ty) in
+                List.map (fun (bds, eqs, t) -> bds, eqs@[(v, ls, t)], t_app ls [] ls.ls_value) (expand p)
+          in
+          let for_expansion (bds, eqs, t'') =
+            let mvs = List.fold_left (fun acc vls -> match vls with Some v, ls -> Mvs.add v (t_app ls [] ls.ls_value) acc | None, _ -> acc) Mvs.empty bds in
+            let mvs = List.fold_left (fun acc (vs, ls, _) -> Mvs.add vs (t_app ls [] ls.ls_value) acc) mvs eqs in
+            List.map (fun (_, ls) -> Param (create_param_decl ls)) bds @
+            List.map (fun (_, ls, t) -> Param (create_logic_decl [make_ls_defn ls [] t])) eqs @
+            [Axiom_term (t_equ t t'');
+             Axiom_term (t_subst mvs t')]
+          in
+          List.map for_expansion (expand p)
+        in
+        List.flatten
+          (List.map for_case tbs)
     | _ -> raise (Arg_trans ("destruct"))
   in
   destruct_fmla ~toplevel:true t