handling for "undefined" in case expressions
authorhaftmann
Tue Jan 09 19:08:58 2007 +0100 (2007-01-09)
changeset 22047ff91fd74bb71
parent 22046 ce84c9887e2d
child 22048 990b5077590d
handling for "undefined" in case expressions
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Jan 09 19:08:56 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Jan 09 19:08:58 2007 +0100
     1.3 @@ -336,12 +336,13 @@
     1.4      val abs = Name.names Name.context "a" (Library.drop (length ts, tys));
     1.5      val (ts', t) = split_last (ts @ map Free abs);
     1.6      val (tys', sty) = split_last tys;
     1.7 -    fun dest_case ((c, tys_decl), ty) t =
     1.8 -      let
     1.9 -        val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
    1.10 -        val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
    1.11 -      in (c', t') end;
    1.12 -  in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts')) end;
    1.13 +    fun dest_case _ (Const ("undefined", _)) = NONE
    1.14 +      | dest_case ((c, tys_decl), ty) t =
    1.15 +          let
    1.16 +            val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
    1.17 +            val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
    1.18 +          in SOME (c', t') end;
    1.19 +  in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts' |> map_filter I)) end;
    1.20  
    1.21  fun dest_case_expr thy t =
    1.22    case strip_comb t