SMTv2 printer: pattern matching: handle the wildcard

src/printer/smtv2.ml

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-(** SMT v1 printer with some extensions *)
+(** SMT v2 printer with some extensions *)
 
 open Format
 open Pp
@@ -159,59 +159,18 @@ let rec print_term info fmt t = match t.t_node with
   | Tif (f1,t1,t2) ->
       fprintf fmt "@[(ite %a@ %a@ %a)@]"
         (print_fmla info) f1 (print_term info) t1 (print_term info) t2
-(*
-  | Tcase _ -> unsupportedTerm t
-      "smtv2: you must eliminate match"
-*)
-  | Tcase(t,bl) ->
-     let subject = create_vsymbol (id_fresh "subject") (t_type t) in
-     fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
-             print_var subject (print_term info) t
-             (print_branches info subject print_term) bl;
-     forget_var subject
+  | Tcase({t_node = Tvar v}, bl) ->
+      print_branches info v print_term fmt bl
+  | Tcase(t, bl) ->
+      let subject = create_vsymbol (id_fresh "subject") (t_type t) in
+      fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
+        print_var subject (print_term info) t
+        (print_branches info subject print_term) bl;
+      forget_var subject
   | Teps _ -> unsupportedTerm t
       "smtv2: you must eliminate epsilon"
   | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
 
-and print_branches info subject pr fmt bl =
-  match bl with
-  | [] -> assert false
-  | br::bl ->
-     let (p,t) = t_open_branch br in
-     let constr,args =
-       try
-         match p.pat_node with
-         | Papp(cs,args) ->
-            let vars = List.map
-                         (function { pat_node = Pvar v} -> v
-                                 | _ -> raise Exit) args
-            in cs,vars
-         | _ -> raise Exit
-       with Exit ->
-         unsupportedPattern p
-           "smtv2: you must compile nested pattern-matching"
-     in
-     match bl with
-     | [] -> print_branch info subject pr fmt (constr,args,t)
-     | _ ->
-        fprintf fmt "@[(ite (is-%a %a) %a %a)@]"
-                print_ident constr.ls_name print_var subject
-                (print_branch info subject pr) (constr,args,t)
-                (print_branches info subject pr) bl
-
-and print_branch info subject pr fmt (cs,vars,t) =
-  let i = ref 0 in
-  let print_proj fmt v =
-    incr i;
-    fprintf fmt "(%a (%a_proj_%d %a))" print_var v print_ident cs.ls_name
-            !i print_var subject
-  in
-  match vars with
-  | [] -> pr info fmt t
-  | _ -> fprintf fmt "@[(let (%a) %a)@]"
-                 (print_list space print_proj) vars
-                 (pr info) t
-
 and print_fmla info fmt f = match f.t_node with
   | Tapp ({ ls_name = id }, []) ->
       print_ident fmt id
@@ -263,18 +222,44 @@ and print_fmla info fmt f = match f.t_node with
       fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
         (print_term info) t1 (print_fmla info) f2;
       forget_var v
-(*
-  | Tcase _ -> unsupportedTerm f
-      "smtv2 : you must eliminate match"
- *)
-  | Tcase(t,bl) ->
-     let subject = create_vsymbol (id_fresh "subject") (t_type t) in
-     fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
-             print_var subject (print_term info) t
-             (print_branches info subject print_fmla) bl;
-     forget_var subject
+  | Tcase({t_node = Tvar v}, bl) ->
+      print_branches info v print_fmla fmt bl
+  | Tcase(t, bl) ->
+      let subject = create_vsymbol (id_fresh "subject") (t_type t) in
+      fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
+        print_var subject (print_term info) t
+        (print_branches info subject print_fmla) bl;
+      forget_var subject
   | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
 
+and print_branches info subject pr fmt bl = match bl with
+  | [] -> assert false
+  | br::bl ->
+      let (p,t) = t_open_branch br in
+      let error () = unsupportedPattern p
+        "smtv2: you must compile nested pattern matching" in
+      match p.pat_node with
+      | Pwild -> pr info fmt t
+      | Papp (cs,args) ->
+          let args = List.map (function
+            | {pat_node = Pvar v} -> v | _ -> error ()) args in
+          if bl = [] then print_branch info subject pr fmt (cs,args,t)
+          else fprintf fmt "@[(ite (is-%a %a) %a %a)@]"
+            print_ident cs.ls_name print_var subject
+            (print_branch info subject pr) (cs,args,t)
+            (print_branches info subject pr) bl
+      | _ -> error ()
+
+and print_branch info subject pr fmt (cs,vars,t) =
+  if vars = [] then pr info fmt t else
+  let tvs = t_freevars Mvs.empty t in
+  if List.for_all (fun v -> not (Mvs.mem v tvs)) vars then pr info fmt t else
+  let i = ref 0 in
+  let pr_proj fmt v = incr i;
+    if Mvs.mem v tvs then fprintf fmt "(%a (%a_proj_%d %a))"
+      print_var v print_ident cs.ls_name !i print_var subject in
+  fprintf fmt "@[(let (%a) %a)@]" (print_list space pr_proj) vars (pr info) t
+
 and print_expr info fmt =
   TermTF.t_select (print_term info fmt) (print_fmla info fmt)
 
@@ -330,7 +315,7 @@ let print_constructor_decl info fmt (ls,args) =
   | [] -> fprintf fmt "(%a)" print_ident ls.ls_name
   | _ ->
      fprintf fmt "@[(%a@ " print_ident ls.ls_name;
-     let _ = 
+     let _ =
        List.fold_left2
          (fun i ty pr ->
           begin match pr with