added empty cases
authorhaftmann
Fri, 23 Mar 2007 09:40:57 +0100
changeset 22509 c5929d4373a0
parent 22508 6ee2edbce31c
child 22510 d28409741406
added empty cases
src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Fri Mar 23 09:40:53 2007 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Fri Mar 23 09:40:57 2007 +0100
@@ -412,6 +412,7 @@
               :: map (pr "|") bs
             )
           end
+      | pr_term vars fxy (t as ICase (_, [])) = str "raise Fail \"empty case\""
     and pr_app' vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then let
         val k = length tys
@@ -681,6 +682,7 @@
               :: map (pr "|") bs
             )
           end
+      | pr_term vars fxy (t as ICase (_, [])) = str "failwith \"empty case\""
     and pr_app' vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then
         if length tys = length ts
@@ -1176,7 +1178,7 @@
               concat [str "}", str "in", pr_term vars' NOBR t]
             ) ps
           end
-      | pr_term vars fxy (ICase ((td, ty), bs)) =
+      | pr_term vars fxy (ICase ((td, ty), bs as _ :: _)) =
           let
             fun pr (pat, t) =
               let
@@ -1188,6 +1190,7 @@
               str "})"
             ) (map pr bs)
           end
+      | pr_term vars fxy (t as ICase (_, [])) = str "error \"empty case\""
     and pr_app' vars ((c, _), ts) =
       (str o deresolv) c :: map (pr_term vars BR) ts
     and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars