src/HOL/Tools/inductive_codegen.ML
changeset 15061 61a52739cd82
parent 15031 726dc9146bb1
child 15126 54ae6c6ef3b1
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Mon Jul 19 18:12:49 2004 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Jul 19 18:14:22 2004 +0200
     1.3 @@ -331,7 +331,12 @@
     1.4        in (nvs'', t' $ u') end
     1.5    | distinct_v x = x;
     1.6  
     1.7 -fun compile_match nvs eq_ps out_ps success_p fail_p =
     1.8 +fun is_exhaustive (Var _) = true
     1.9 +  | is_exhaustive (Const ("Pair", _) $ t $ u) =
    1.10 +      is_exhaustive t andalso is_exhaustive u
    1.11 +  | is_exhaustive _ = false;
    1.12 +
    1.13 +fun compile_match nvs eq_ps out_ps success_p can_fail =
    1.14    let val eqs = flat (separate [Pretty.str " andalso", Pretty.brk 1]
    1.15      (map single (flat (map (mk_eq o snd) nvs) @ eq_ps)));
    1.16    in
    1.17 @@ -340,8 +345,10 @@
    1.18        (Pretty.block ((if eqs=[] then [] else Pretty.str "if " ::
    1.19           [Pretty.block eqs, Pretty.brk 1, Pretty.str "then "]) @
    1.20           (success_p ::
    1.21 -          (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else ", fail_p]))) ::
    1.22 -       [Pretty.brk 1, Pretty.str "| _ => ", fail_p, Pretty.str ")"]))
    1.23 +          (if eqs=[] then [] else [Pretty.brk 1, Pretty.str "else Seq.empty"]))) ::
    1.24 +       (if can_fail then
    1.25 +          [Pretty.brk 1, Pretty.str "| _ => Seq.empty)"]
    1.26 +        else [Pretty.str ")"])))
    1.27    end;
    1.28  
    1.29  fun modename thy s (iss, is) = space_implode "__"
    1.30 @@ -401,7 +408,7 @@
    1.31            in
    1.32              (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
    1.33                (Pretty.block [Pretty.str "Seq.single", Pretty.brk 1, mk_tuple out_ps])
    1.34 -              (Pretty.str "Seq.empty"))
    1.35 +              (exists (not o is_exhaustive) out_ts'''))
    1.36            end
    1.37        | compile_prems out_ts vs names gr ps =
    1.38            let
    1.39 @@ -435,7 +442,7 @@
    1.40                     (gr4, compile_match (snd nvs) eq_ps out_ps
    1.41                        (Pretty.block (ps @
    1.42                           [Pretty.str " :->", Pretty.brk 1, rest]))
    1.43 -                      (Pretty.str "Seq.empty"))
    1.44 +                      (exists (not o is_exhaustive) out_ts''))
    1.45                   end
    1.46               | Sidecond t =>
    1.47                   let
    1.48 @@ -445,7 +452,7 @@
    1.49                     (gr3, compile_match (snd nvs) eq_ps out_ps
    1.50                        (Pretty.block [Pretty.str "?? ", side_p,
    1.51                          Pretty.str " :->", Pretty.brk 1, rest])
    1.52 -                      (Pretty.str "Seq.empty"))
    1.53 +                      (exists (not o is_exhaustive) out_ts''))
    1.54                   end)
    1.55            end;
    1.56