# HG changeset patch
# User berghofe
# Date 1090253662 -7200
# Node ID 61a52739cd82a2379b1f80878415a9eef881f118
# Parent  7b4abcfae4e10ab08c1bb06e4faf5697096bf9d9
Added simple check that allows code generator to produce code containing
fewer redundant matches.

diff -r 7b4abcfae4e1 -r 61a52739cd82 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Jul 19 18:12:49 2004 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jul 19 18:14:22 2004 +0200
@@ -331,7 +331,12 @@
       in (nvs'', t' $ u') end
   | distinct_v x = x;
 
-fun compile_match nvs eq_ps out_ps success_p fail_p =
+fun is_exhaustive (Var _) = true
+  | is_exhaustive (Const ("Pair", _) $ t $ u) =
+      is_exhaustive t andalso is_exhaustive u
+  | is_exhaustive _ = false;
+
+fun compile_match nvs eq_ps out_ps success_p can_fail =
   let val eqs = flat (separate [Pretty.str " andalso", Pretty.brk 1]
     (map single (flat (map (mk_eq o snd) nvs) @ eq_ps)));
   in
@@ -340,8 +345,10 @@
       (Pretty.block ((if eqs=[] then [] else Pretty.str "if " ::
          [Pretty.block eqs, Pretty.brk 1, Pretty.str "then "]) @
          (success_p ::
-          (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else ", fail_p]))) ::
-       [Pretty.brk 1, Pretty.str "| _ => ", fail_p, Pretty.str ")"]))
+          (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else Seq.empty"]))) ::
+       (if can_fail then
+          [Pretty.brk 1, Pretty.str "| _ => Seq.empty)"]
+        else [Pretty.str ")"])))
   end;
 
 fun modename thy s (iss, is) = space_implode "__"
@@ -401,7 +408,7 @@
           in
             (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
               (Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, mk_tuple out_ps])
-              (Pretty.str "Seq.empty"))
+              (exists (not o is_exhaustive) out_ts'''))
           end
       | compile_prems out_ts vs names gr ps =
           let
@@ -435,7 +442,7 @@
                    (gr4, compile_match (snd nvs) eq_ps out_ps
                       (Pretty.block (ps @
                          [Pretty.str " :->", Pretty.brk 1, rest]))
-                      (Pretty.str "Seq.empty"))
+                      (exists (not o is_exhaustive) out_ts''))
                  end
              | Sidecond t =>
                  let
@@ -445,7 +452,7 @@
                    (gr3, compile_match (snd nvs) eq_ps out_ps
                       (Pretty.block [Pretty.str "?? ", side_p,
                         Pretty.str " :->", Pretty.brk 1, rest])
-                      (Pretty.str "Seq.empty"))
+                      (exists (not o is_exhaustive) out_ts''))
                  end)
           end;