Some cases in "case ... of ..." expressions may now
authorberghofe
Fri Jul 21 14:11:14 2006 +0200 (2006-07-21)
changeset 20173c8f791af9a60
parent 20172 b65eb8145f5e
child 20174 c057b3618963
Some cases in "case ... of ..." expressions may now
be omitted (internally, these cases are assigned
the "undefined" value).
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jul 21 11:34:01 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jul 21 14:11:14 2006 +0200
     1.3 @@ -431,10 +431,12 @@
     1.4            val (_, (_, dts, constrs)) = List.nth (descr, index);
     1.5            fun find_case (cases, (s, dt)) =
     1.6              (case find_first (equal s o fst o fst) cases' of
     1.7 -               NONE => (case default of
     1.8 -                   NONE => case_error ("No clause for constructor " ^ s) (SOME tname) [u]
     1.9 -                 | SOME t => (cases, list_abs (map (rpair dummyT) (DatatypeProp.make_tnames
    1.10 -                     (map (typ_of_dtyp descr sorts) dt)), t)))
    1.11 +               NONE => (cases, list_abs (map (rpair dummyT)
    1.12 +                 (DatatypeProp.make_tnames (map (typ_of_dtyp descr sorts) dt)),
    1.13 +                 case default of
    1.14 +                   NONE => (warning ("No clause for constructor " ^ s ^
    1.15 +                     " in case expression"); Const ("undefined", dummyT))
    1.16 +                 | SOME t => t))
    1.17               | SOME (c as ((_, vs), t)) =>
    1.18                   if length dt <> length vs then
    1.19                      case_error ("Wrong number of arguments for constructor " ^ s)
    1.20 @@ -484,10 +486,16 @@
    1.21        (Library.foldl count_cases ([], cases));
    1.22      fun mk_case1 (cname, (vs, body), _) = Syntax.const "_case1" $
    1.23        list_comb (Syntax.const cname, vs) $ body;
    1.24 +    fun is_undefined (Const ("undefined", _)) = true
    1.25 +      | is_undefined _ = false;
    1.26    in
    1.27      Syntax.const "_case_syntax" $ x $
    1.28        foldr1 (fn (t, u) => Syntax.const "_case2" $ t $ u) (map mk_case1
    1.29 -        (case cases' of
    1.30 +        (case find_first (is_undefined o fst) cases' of
    1.31 +           SOME (_, cnames) =>
    1.32 +           if length cnames = length constrs then [hd cases]
    1.33 +           else filter_out (fn (_, (_, body), _) => is_undefined body) cases
    1.34 +         | NONE => case cases' of
    1.35             [] => cases
    1.36           | (default, cnames) :: _ =>
    1.37             if length cnames = 1 then cases