match statements on tuples

src/core/decl.ml

@@ -129,12 +129,9 @@ module Hsdecl = Hashcons.Make (struct
 
   type t = decl
 
-  let for_all2 pr l1 l2 =
-    try List.for_all2 pr l1 l2 with Invalid_argument _ -> false
-
   let eq_td (ts1,td1) (ts2,td2) = ts1 == ts2 && match td1,td2 with
     | Tabstract, Tabstract -> true
-    | Talgebraic l1, Talgebraic l2 -> for_all2 (==) l1 l2
+    | Talgebraic l1, Talgebraic l2 -> list_all2 (==) l1 l2
     | _ -> false
 
   let eq_ld (ls1,ld1) (ls2,ld2) = ls1 == ls2 && match ld1,ld2 with
@@ -144,12 +141,12 @@ module Hsdecl = Hashcons.Make (struct
 
   let eq_iax (pr1,fr1) (pr2,fr2) = pr1 == pr1 && fr1 == fr2
 
-  let eq_ind (ps1,al1) (ps2,al2) = ps1 == ps2 && for_all2 eq_iax al1 al2
+  let eq_ind (ps1,al1) (ps2,al2) = ps1 == ps2 && list_all2 eq_iax al1 al2
 
   let equal d1 d2 = match d1.d_node, d2.d_node with
-    | Dtype  l1, Dtype  l2 -> for_all2 eq_td l1 l2
-    | Dlogic l1, Dlogic l2 -> for_all2 eq_ld l1 l2
-    | Dind   l1, Dind   l2 -> for_all2 eq_ind l1 l2
+    | Dtype  l1, Dtype  l2 -> list_all2 eq_td l1 l2
+    | Dlogic l1, Dlogic l2 -> list_all2 eq_ld l1 l2
+    | Dind   l1, Dind   l2 -> list_all2 eq_ind l1 l2
     | Dprop (k1,pr1,f1), Dprop (k2,pr2,f2) ->
         k1 == k2 && pr1 == pr2 && f1 == f2
     | _,_ -> false

src/core/decl.mli

@@ -83,6 +83,10 @@ and decl_node =
   | Dind   of ind_decl list     (* inductive predicates *)
   | Dprop  of prop_decl         (* axiom / lemma / goal *)
 
+module Sdecl : Set.S with type elt = decl
+module Mdecl : Map.S with type key = decl
+module Hdecl : Hashtbl.S with type key = decl
+
 (** Declaration constructors *)
 
 val create_ty_decl : ty_decl list -> decl

src/core/pretty.ml

@@ -194,9 +194,10 @@ and print_tnode opl opr fmt t = match t.t_node with
       fprintf fmt (protect_on opr "let %a =@ %a in@ %a")
         print_vs v print_opl_term t1 print_opl_term t2;
       forget_var v
-  | Tcase (t1,bl) ->
+  | Tcase (tl,bl) ->
       fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
-        print_term t1 (print_list newline print_tbranch) bl
+        (print_list comma print_term) tl
+        (print_list newline print_tbranch) bl
   | Teps fb ->
       let v,f = f_open_bound fb in
       fprintf fmt (protect_on opr "epsilon %a.@ %a")
@@ -229,21 +230,24 @@ and print_fnode opl opr fmt f = match f.f_node with
       fprintf fmt (protect_on opr "let %a =@ %a in@ %a")
         print_vs v print_opl_term t print_opl_fmla f;
       forget_var v
-  | Fcase (t,bl) ->
-      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend" print_term t
+  | Fcase (tl,bl) ->
+      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
+        (print_list comma print_term) tl
         (print_list newline print_fbranch) bl
   | Fif (f1,f2,f3) ->
       fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
         print_fmla f1 print_fmla f2 print_opl_fmla f3
 
 and print_tbranch fmt br =
-  let pat,svs,t = t_open_branch br in
-  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat pat print_term t;
+  let pl,svs,t = t_open_branch br in
+  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
+    (print_list comma print_pat) pl print_term t;
   Svs.iter forget_var svs
 
 and print_fbranch fmt br =
-  let pat,svs,f = f_open_branch br in
-  fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat pat print_fmla f;
+  let pl,svs,f = f_open_branch br in
+  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
+    (print_list comma print_pat) pl print_fmla f;
   Svs.iter forget_var svs
 
 and print_tl fmt tl =

src/core/term.mli

@@ -129,7 +129,7 @@ and term_node = private
   | Tconst of constant
   | Tapp of lsymbol * term list
   | Tlet of term * term_bound
-  | Tcase of term * term_branch list
+  | Tcase of term list * term_branch list
   | Teps of fmla_bound
 
 and fmla_node = private
@@ -141,7 +141,7 @@ and fmla_node = private
   | Ffalse
   | Fif of fmla * fmla * fmla
   | Flet of term * fmla_bound
-  | Fcase of term * fmla_branch list
+  | Fcase of term list * fmla_branch list
 
 and term_bound
 
@@ -170,7 +170,7 @@ val t_var : vsymbol -> term
 val t_const : constant -> ty -> term
 val t_app : lsymbol -> term list -> ty -> term
 val t_let : vsymbol -> term -> term -> term
-val t_case : term -> (pattern * term) list -> ty -> term
+val t_case : term list -> (pattern list * term) list -> ty -> term
 val t_eps : vsymbol -> fmla -> term
 
 val t_label : label list -> term -> term
@@ -193,7 +193,7 @@ val f_true : fmla
 val f_false : fmla
 val f_if : fmla -> fmla -> fmla -> fmla
 val f_let : vsymbol -> term -> fmla -> fmla
-val f_case :  term -> (pattern * fmla) list -> fmla
+val f_case : term list -> (pattern list * fmla) list -> fmla
 
 val f_label : label list -> fmla -> fmla
 val f_label_add : label -> fmla -> fmla
@@ -204,8 +204,8 @@ val f_label_copy : fmla -> fmla -> fmla
 val t_open_bound : term_bound -> vsymbol * term
 val f_open_bound : fmla_bound -> vsymbol * fmla
 
-val t_open_branch : term_branch -> pattern * Svs.t * term
-val f_open_branch : fmla_branch -> pattern * Svs.t * fmla
+val t_open_branch : term_branch -> pattern list * Svs.t * term
+val f_open_branch : fmla_branch -> pattern list * Svs.t * fmla
 
 val f_open_quant : fmla_quant -> vsymbol list * trigger list * fmla
 

src/core/ty.ml

@@ -76,14 +76,14 @@ module Hsty = Hashcons.Make (struct
 
   let equal ty1 ty2 = match ty1.ty_node, ty2.ty_node with
     | Tyvar n1, Tyvar n2 -> n1 == n2
-    | Tyapp (s1, l1), Tyapp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
+    | Tyapp (s1,l1), Tyapp (s2,l2) -> s1 == s2 && List.for_all2 (==) l1 l2
     | _ -> false
 
   let hash_ty ty = ty.ty_tag
 
   let hash ty = match ty.ty_node with
     | Tyvar v -> v.tv_name.id_tag
-    | Tyapp (s, tl) -> Hashcons.combine_list hash_ty s.ts_name.id_tag tl
+    | Tyapp (s,tl) -> Hashcons.combine_list hash_ty s.ts_name.id_tag tl
 
   let tag n ty = { ty with ty_tag = n }
 end)

src/parser/typing.ml

@@ -536,11 +536,11 @@ let rec term env t = match t.dt_node with
   | Tmatch (e1, bl) ->
       let branch (pat,e) =
         let env, pat = pattern env pat in
-        (pat, term env e)
+        ([pat], term env e)
       in
       let bl = List.map branch bl in
       let ty = (snd (List.hd bl)).t_ty in
-      t_case (term env e1) bl ty
+      t_case [term env e1] bl ty
   | Tnamed (x, e1) ->
       let e1 = term env e1 in
       t_label_add x e1
@@ -586,9 +586,9 @@ and fmla env = function
   | Fmatch (e1, bl) ->
       let branch (pat,e) =
         let env, pat = pattern env pat in
-        (pat, fmla env e)
+        ([pat], fmla env e)
       in
-      f_case (term env e1) (List.map branch bl)
+      f_case [term env e1] (List.map branch bl)
   | Fnamed (x, f1) ->
       let f1 = fmla env f1 in
       f_label_add x f1

src/printer/why3.ml

@@ -177,9 +177,10 @@ and print_tnode opl opr drv fmt t = match t.t_node with
       fprintf fmt (protect_on opr "let %a =@ %a in@ %a")
         print_vs v (print_opl_term drv) t1 (print_opl_term drv) t2;
       forget_var v
-  | Tcase (t1,bl) ->
+  | Tcase (tl,bl) ->
       fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
-        (print_term drv) t1 (print_list newline (print_tbranch drv)) bl
+        (print_list comma (print_term drv)) tl
+        (print_list newline (print_tbranch drv)) bl
   | Teps fb ->
       let v,f = f_open_bound fb in
       fprintf fmt (protect_on opr "epsilon %a.@ %a")
@@ -216,8 +217,9 @@ and print_fnode opl opr drv fmt f = match f.f_node with
       fprintf fmt (protect_on opr "let %a =@ %a in@ %a")
         print_vs v (print_opl_term drv) t (print_opl_fmla drv) f;
       forget_var v
-  | Fcase (t,bl) ->
-      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend" (print_term drv) t
+  | Fcase (tl,bl) ->
+      fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
+        (print_list comma (print_term drv)) tl
         (print_list newline (print_fbranch drv)) bl
   | Fif (f1,f2,f3) ->
       fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
@@ -230,13 +232,15 @@ and print_fnode opl opr drv fmt f = match f.f_node with
     end
 
 and print_tbranch drv fmt br =
-  let pat,svs,t = t_open_branch br in
-  fprintf fmt "@[<hov 4>| %a ->@ %a@]" (print_pat drv) pat (print_term drv) t;
+  let pl,svs,t = t_open_branch br in
+  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
+    (print_list comma (print_pat drv)) pl (print_term drv) t;
   Svs.iter forget_var svs
 
 and print_fbranch drv fmt br =
-  let pat,svs,f = f_open_branch br in
-  fprintf fmt "@[<hov 4>| %a ->@ %a@]" (print_pat drv) pat (print_fmla drv) f;
+  let pl,svs,f = f_open_branch br in
+  fprintf fmt "@[<hov 4>| %a ->@ %a@]"
+    (print_list comma (print_pat drv)) pl (print_fmla drv) f;
   Svs.iter forget_var svs
 
 and print_tl drv fmt tl =

src/util/hashweak.ml

@@ -17,7 +17,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Make (S:Util.Sstruct) =
+module Make (S : Util.Tagged) =
 struct
 
   type 'a t = { ht : (int,'a) Hashtbl.t;

src/util/hashweak.mli

@@ -17,7 +17,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Make (X:Util.Sstruct) :
+module Make (X : Util.Tagged) :
 sig
 
   type 'a t

src/util/util.ml

@@ -17,13 +17,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-let map_fold_left f acc l =
-  let acc, rev =
-    List.fold_left
-      (fun (acc, rev) e -> let acc, e = f acc e in acc, e :: rev)
-      (acc, []) l
-  in
-  acc, List.rev rev
+(* useful option combinators *)
 
 let of_option = function None -> assert false | Some x -> x
 
@@ -33,32 +27,48 @@ let option_apply d f = function None -> d | Some x -> f x
 
 let option_iter f = function None -> () | Some x -> f x
 
+(* useful list combinators *)
+
+let map_fold_left f acc l =
+  let acc, rev =
+    List.fold_left
+      (fun (acc, rev) e -> let acc, e = f acc e in acc, e :: rev)
+      (acc, []) l
+  in
+  acc, List.rev rev
+
+let list_all2 pr l1 l2 =
+  try List.for_all2 pr l1 l2 with Invalid_argument _ -> false
+
+(* boolean fold accumulators *)
 
 exception FoldSkip
 
 let all_fn pr _ t = pr t || raise FoldSkip
 let any_fn pr _ t = pr t && raise FoldSkip
 
+(* Set and Map on strings *)
+
 module Sstr = Set.Make(String)
 module Mstr = Map.Make(String)
 
-module type Sstruct =
+(* Set, Map, Hashtbl on structures with a unique tag and physical equality *)
+
+module type Tagged =
 sig
   type t
   val tag : t -> int
 end
 
-module OrderedHash (X:Sstruct) = 
+module OrderedHash (X : Tagged) =
 struct
   type t = X.t
   let equal = (==)
   let hash = X.tag
-  let compare ts1 ts2 =
-    Pervasives.compare (X.tag ts1) (X.tag ts2)
+  let compare ts1 ts2 = Pervasives.compare (X.tag ts1) (X.tag ts2)
 end
 
-
-module StructMake(X : Sstruct) =
+module StructMake (X : Tagged) =
 struct
   module T = OrderedHash(X)
   module S = Set.Make(T)

src/util/util.mli

@@ -17,8 +17,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val map_fold_left :
-  ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
+(* useful option combinators *)
 
 val of_option : 'a option -> 'a
 
@@ -28,21 +27,34 @@ val option_iter : ('a -> unit) -> 'a option -> unit
 
 val option_apply : 'b -> ('a -> 'b) -> 'a option -> 'b
 
+(* useful list combinators *)
+
+val map_fold_left :
+  ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
+
+val list_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+
+(* boolean fold accumulators *)
+
 exception FoldSkip
 
 val all_fn : ('a -> bool) -> 'b -> 'a -> bool
 val any_fn : ('a -> bool) -> 'b -> 'a -> bool
 
+(* Set and Map on strings *)
+
 module Sstr : Set.S with type elt = string
 module Mstr : Map.S with type key = string
 
-module type Sstruct =
+(* Set, Map, Hashtbl on structures with a unique tag and physical equality *)
+
+module type Tagged =
 sig
   type t
   val tag : t -> int
 end
 
-module OrderedHash (X:Sstruct) :
+module OrderedHash (X : Tagged) :
 sig
   type t = X.t
   val equal : t -> t -> bool
@@ -50,11 +62,10 @@ sig
   val compare : t -> t -> int
 end
 
-
-(* Use physical equality on X.t *)
-module StructMake(X : Sstruct) :
+module StructMake (X : Tagged) :
 sig
   module S : Set.S with type elt = X.t
   module M : Map.S with type key = X.t
   module H : Hashtbl.S with type key = X.t
 end
+