separate data used for case translation from the datatype package
authortraytel
Tue Jan 22 14:33:45 2013 +0100 (2013-01-22)
changeset 516734dfa00e264d8
parent 51672 d5c5e088ebdf
child 51674 2b1498a2ce85
separate data used for case translation from the datatype package
src/HOL/HOL.thy
src/HOL/Inductive.thy
src/HOL/List.thy
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/case_translation.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Jan 22 13:32:41 2013 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Jan 22 14:33:45 2013 +0100
     1.3 @@ -8,7 +8,8 @@
     1.4  imports Pure "~~/src/Tools/Code_Generator"
     1.5  keywords
     1.6    "try" "solve_direct" "quickcheck"
     1.7 -    "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag and
     1.8 +    "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" 
     1.9 +    "print_case_translations":: diag and
    1.10    "quickcheck_params" :: thy_decl
    1.11  begin
    1.12  
     2.1 --- a/src/HOL/Inductive.thy	Tue Jan 22 13:32:41 2013 +0100
     2.2 +++ b/src/HOL/Inductive.thy	Tue Jan 22 14:33:45 2013 +0100
     2.3 @@ -279,7 +279,8 @@
     2.4    case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
     2.5    case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
     2.6    case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
     2.7 -ML_file "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
     2.8 +ML_file "Tools/case_translation.ML"
     2.9 +setup Case_Translation.setup
    2.10  
    2.11  ML_file "Tools/Datatype/rep_datatype.ML"
    2.12  ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
    2.13 @@ -297,7 +298,7 @@
    2.14    fun fun_tr ctxt [cs] =
    2.15      let
    2.16        val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
    2.17 -      val ft = Datatype_Case.case_tr ctxt [x, cs];
    2.18 +      val ft = Case_Translation.case_tr ctxt [x, cs];
    2.19      in lambda x ft end
    2.20  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    2.21  *}
     3.1 --- a/src/HOL/List.thy	Tue Jan 22 13:32:41 2013 +0100
     3.2 +++ b/src/HOL/List.thy	Tue Jan 22 14:33:45 2013 +0100
     3.3 @@ -407,7 +407,7 @@
     3.4            Syntax.const @{syntax_const "_case1"} $
     3.5              Syntax.const @{const_syntax dummy_pattern} $ NilC;
     3.6          val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
     3.7 -      in Syntax_Trans.abs_tr [x, Datatype_Case.case_tr ctxt [x, cs]] end;
     3.8 +      in Syntax_Trans.abs_tr [x, Case_Translation.case_tr ctxt [x, cs]] end;
     3.9  
    3.10      fun abs_tr ctxt p e opti =
    3.11        (case Term_Position.strip_positions p of
     4.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Tue Jan 22 13:32:41 2013 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,490 +0,0 @@
     4.4 -(*  Title:      HOL/Tools/Datatype/datatype_case.ML
     4.5 -    Author:     Konrad Slind, Cambridge University Computer Laboratory
     4.6 -    Author:     Stefan Berghofer, TU Muenchen
     4.7 -
     4.8 -Datatype package: nested case expressions on datatypes.
     4.9 -
    4.10 -TODO:
    4.11 -  * Avoid hard-wiring with datatype package.  Instead provide generic
    4.12 -    generic declarations of case splits based on an internal data slot.
    4.13 -*)
    4.14 -
    4.15 -signature DATATYPE_CASE =
    4.16 -sig
    4.17 -  datatype config = Error | Warning | Quiet
    4.18 -  type info = Datatype_Aux.info
    4.19 -  val case_tr: Proof.context -> term list -> term
    4.20 -  val make_case:  Proof.context -> config -> Name.context -> term -> (term * term) list -> term
    4.21 -  val strip_case: Proof.context -> bool -> term -> term
    4.22 -  val show_cases: bool Config.T
    4.23 -  val setup: theory -> theory
    4.24 -end;
    4.25 -
    4.26 -structure Datatype_Case : DATATYPE_CASE =
    4.27 -struct
    4.28 -
    4.29 -datatype config = Error | Warning | Quiet;
    4.30 -type info = Datatype_Aux.info;
    4.31 -
    4.32 -exception CASE_ERROR of string * int;
    4.33 -
    4.34 -fun match_type ctxt pat ob =
    4.35 -  Sign.typ_match (Proof_Context.theory_of ctxt) (pat, ob) Vartab.empty;
    4.36 -
    4.37 -(* Get information about datatypes *)
    4.38 -
    4.39 -fun ty_info ({descr, case_name, index, ...} : info) =
    4.40 -  let
    4.41 -    val (_, (tname, dts, constrs)) = nth descr index;
    4.42 -    val mk_ty = Datatype_Aux.typ_of_dtyp descr;
    4.43 -    val T = Type (tname, map mk_ty dts);
    4.44 -  in
    4.45 -   {case_name = case_name,
    4.46 -    constructors = map (fn (cname, dts') =>
    4.47 -      Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs}
    4.48 -  end;
    4.49 -
    4.50 -
    4.51 -(*Each pattern carries with it a tag i, which denotes the clause it
    4.52 -came from. i = ~1 indicates that the clause was added by pattern
    4.53 -completion.*)
    4.54 -
    4.55 -fun add_row_used ((prfx, pats), (tm, tag)) =
    4.56 -  fold Term.declare_term_frees (tm :: pats @ map Free prfx);
    4.57 -
    4.58 -(* try to preserve names given by user *)
    4.59 -fun default_name "" (Free (name', _)) = name'
    4.60 -  | default_name name _ = name;
    4.61 -
    4.62 -
    4.63 -(*Produce an instance of a constructor, plus fresh variables for its arguments.*)
    4.64 -fun fresh_constr ctxt colty used c =
    4.65 -  let
    4.66 -    val (_, T) = dest_Const c;
    4.67 -    val Ts = binder_types T;
    4.68 -    val (names, _) = fold_map Name.variant
    4.69 -      (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used;
    4.70 -    val ty = body_type T;
    4.71 -    val ty_theta = match_type ctxt ty colty
    4.72 -      handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
    4.73 -    val c' = Envir.subst_term_types ty_theta c;
    4.74 -    val gvars = map (Envir.subst_term_types ty_theta o Free) (names ~~ Ts);
    4.75 -  in (c', gvars) end;
    4.76 -
    4.77 -(*Go through a list of rows and pick out the ones beginning with a
    4.78 -  pattern with constructor = name.*)
    4.79 -fun mk_group (name, T) rows =
    4.80 -  let val k = length (binder_types T) in
    4.81 -    fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) =>
    4.82 -      fn ((in_group, not_in_group), names) =>
    4.83 -        (case strip_comb p of
    4.84 -          (Const (name', _), args) =>
    4.85 -            if name = name' then
    4.86 -              if length args = k then
    4.87 -                ((((prfx, args @ ps), rhs) :: in_group, not_in_group),
    4.88 -                 map2 default_name names args)
    4.89 -              else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ quote name, i)
    4.90 -            else ((in_group, row :: not_in_group), names)
    4.91 -        | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
    4.92 -    rows (([], []), replicate k "") |>> pairself rev
    4.93 -  end;
    4.94 -
    4.95 -
    4.96 -(* Partitioning *)
    4.97 -
    4.98 -fun partition _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
    4.99 -  | partition ctxt used constructors colty res_ty
   4.100 -        (rows as (((prfx, _ :: ps), _) :: _)) =
   4.101 -      let
   4.102 -        fun part [] [] = []
   4.103 -          | part [] ((_, (_, i)) :: _) = raise CASE_ERROR ("Not a constructor pattern", i)
   4.104 -          | part (c :: cs) rows =
   4.105 -              let
   4.106 -                val ((in_group, not_in_group), names) = mk_group (dest_Const c) rows;
   4.107 -                val used' = fold add_row_used in_group used;
   4.108 -                val (c', gvars) = fresh_constr ctxt colty used' c;
   4.109 -                val in_group' =
   4.110 -                  if null in_group  (* Constructor not given *)
   4.111 -                  then
   4.112 -                    let
   4.113 -                      val Ts = map fastype_of ps;
   4.114 -                      val (xs, _) =
   4.115 -                        fold_map Name.variant
   4.116 -                          (replicate (length ps) "x")
   4.117 -                          (fold Term.declare_term_frees gvars used');
   4.118 -                    in
   4.119 -                      [((prfx, gvars @ map Free (xs ~~ Ts)),
   4.120 -                        (Const (@{const_name undefined}, res_ty), ~1))]
   4.121 -                    end
   4.122 -                  else in_group;
   4.123 -              in
   4.124 -                {constructor = c',
   4.125 -                 new_formals = gvars,
   4.126 -                 names = names,
   4.127 -                 group = in_group'} :: part cs not_in_group
   4.128 -              end;
   4.129 -      in part constructors rows end;
   4.130 -
   4.131 -fun v_to_prfx (prfx, Free v :: pats) = (v :: prfx, pats)
   4.132 -  | v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
   4.133 -
   4.134 -
   4.135 -(* Translation of pattern terms into nested case expressions. *)
   4.136 -
   4.137 -fun mk_case ctxt used range_ty =
   4.138 -  let
   4.139 -    val get_info = Datatype_Data.info_of_constr_permissive (Proof_Context.theory_of ctxt);
   4.140 -
   4.141 -    fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1)
   4.142 -      | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
   4.143 -          if is_Free p then
   4.144 -            let
   4.145 -              val used' = add_row_used row used;
   4.146 -              fun expnd c =
   4.147 -                let val capp = list_comb (fresh_constr ctxt ty used' c)
   4.148 -                in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag)) end;
   4.149 -            in map expnd constructors end
   4.150 -          else [row];
   4.151 -
   4.152 -    val (name, _) = Name.variant "a" used;
   4.153 -
   4.154 -    fun mk _ [] = raise CASE_ERROR ("no rows", ~1)
   4.155 -      | mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *)
   4.156 -      | mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
   4.157 -      | mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
   4.158 -          let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
   4.159 -            (case Option.map (apfst head_of)
   4.160 -                (find_first (not o is_Free o fst) col0) of
   4.161 -              NONE =>
   4.162 -                let
   4.163 -                  val rows' = map (fn ((v, _), row) => row ||>
   4.164 -                    apfst (subst_free [(v, u)]) |>> v_to_prfx) (col0 ~~ rows);
   4.165 -                in mk us rows' end
   4.166 -            | SOME (Const (cname, cT), i) =>
   4.167 -                (case Option.map ty_info (get_info (cname, cT)) of
   4.168 -                  NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ quote cname, i)
   4.169 -                | SOME {case_name, constructors} =>
   4.170 -                    let
   4.171 -                      val pty = body_type cT;
   4.172 -                      val used' = fold Term.declare_term_frees us used;
   4.173 -                      val nrows = maps (expand constructors used' pty) rows;
   4.174 -                      val subproblems =
   4.175 -                        partition ctxt used' constructors pty range_ty nrows;
   4.176 -                      val (pat_rect, dtrees) =
   4.177 -                        split_list (map (fn {new_formals, group, ...} =>
   4.178 -                          mk (new_formals @ us) group) subproblems);
   4.179 -                      val case_functions =
   4.180 -                        map2 (fn {new_formals, names, ...} =>
   4.181 -                          fold_rev (fn (x as Free (_, T), s) => fn t =>
   4.182 -                            Abs (if s = "" then name else s, T, abstract_over (x, t)))
   4.183 -                              (new_formals ~~ names))
   4.184 -                        subproblems dtrees;
   4.185 -                      val types = map fastype_of (case_functions @ [u]);
   4.186 -                      val case_const = Const (case_name, types ---> range_ty);
   4.187 -                      val tree = list_comb (case_const, case_functions @ [u]);
   4.188 -                    in (flat pat_rect, tree) end)
   4.189 -            | SOME (t, i) =>
   4.190 -                raise CASE_ERROR ("Not a datatype constructor: " ^ Syntax.string_of_term ctxt t, i))
   4.191 -          end
   4.192 -      | mk _ _ = raise CASE_ERROR ("Malformed row matrix", ~1)
   4.193 -  in mk end;
   4.194 -
   4.195 -
   4.196 -(* replace occurrences of dummy_pattern by distinct variables *)
   4.197 -fun replace_dummies (Const (@{const_name dummy_pattern}, T)) used =
   4.198 -      let val (x, used') = Name.variant "x" used
   4.199 -      in (Free (x, T), used') end
   4.200 -  | replace_dummies (t $ u) used =
   4.201 -      let
   4.202 -        val (t', used') = replace_dummies t used;
   4.203 -        val (u', used'') = replace_dummies u used';
   4.204 -      in (t' $ u', used'') end
   4.205 -  | replace_dummies t used = (t, used);
   4.206 -
   4.207 -fun case_error s = error ("Error in case expression:\n" ^ s);
   4.208 -
   4.209 -(*Repeated variable occurrences in a pattern are not allowed.*)
   4.210 -fun no_repeat_vars ctxt pat = fold_aterms
   4.211 -  (fn x as Free (s, _) =>
   4.212 -      (fn xs =>
   4.213 -        if member op aconv xs x then
   4.214 -          case_error (quote s ^ " occurs repeatedly in the pattern " ^
   4.215 -            quote (Syntax.string_of_term ctxt pat))
   4.216 -        else x :: xs)
   4.217 -    | _ => I) pat [];
   4.218 -
   4.219 -fun make_case ctxt config used x clauses =
   4.220 -  let
   4.221 -    fun string_of_clause (pat, rhs) =
   4.222 -      Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
   4.223 -    val _ = map (no_repeat_vars ctxt o fst) clauses;
   4.224 -    val (rows, used') = used |>
   4.225 -      fold (fn (pat, rhs) =>
   4.226 -        Term.declare_term_frees pat #> Term.declare_term_frees rhs) clauses |>
   4.227 -      fold_map (fn (i, (pat, rhs)) => fn used =>
   4.228 -        let val (pat', used') = replace_dummies pat used
   4.229 -        in ((([], [pat']), (rhs, i)), used') end)
   4.230 -          (map_index I clauses);
   4.231 -    val rangeT =
   4.232 -      (case distinct (op =) (map (fastype_of o snd) clauses) of
   4.233 -        [] => case_error "no clauses given"
   4.234 -      | [T] => T
   4.235 -      | _ => case_error "all cases must have the same result type");
   4.236 -    val used' = fold add_row_used rows used;
   4.237 -    val (tags, case_tm) =
   4.238 -      mk_case ctxt used' rangeT [x] rows
   4.239 -        handle CASE_ERROR (msg, i) =>
   4.240 -          case_error
   4.241 -            (msg ^ (if i < 0 then "" else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
   4.242 -    val _ =
   4.243 -      (case subtract (op =) tags (map (snd o snd) rows) of
   4.244 -        [] => ()
   4.245 -      | is =>
   4.246 -          (case config of Error => case_error | Warning => warning | Quiet => fn _ => ())
   4.247 -            ("The following clauses are redundant (covered by preceding clauses):\n" ^
   4.248 -              cat_lines (map (string_of_clause o nth clauses) is)));
   4.249 -  in
   4.250 -    case_tm
   4.251 -  end;
   4.252 -
   4.253 -
   4.254 -(* term check *)
   4.255 -
   4.256 -fun decode_clause (Const (@{const_name case_abs}, _) $ Abs (s, T, t)) xs used =
   4.257 -      let val (s', used') = Name.variant s used
   4.258 -      in decode_clause t (Free (s', T) :: xs) used' end
   4.259 -  | decode_clause (Const (@{const_name case_elem}, _) $ t $ u) xs _ =
   4.260 -      (subst_bounds (xs, t), subst_bounds (xs, u))
   4.261 -  | decode_clause _ _ _ = case_error "decode_clause";
   4.262 -
   4.263 -fun decode_cases (Const (@{const_name case_nil}, _)) = []
   4.264 -  | decode_cases (Const (@{const_name case_cons}, _) $ t $ u) =
   4.265 -      decode_clause t [] (Term.declare_term_frees t Name.context) ::
   4.266 -      decode_cases u
   4.267 -  | decode_cases _ = case_error "decode_cases";
   4.268 -
   4.269 -fun check_case ctxt =
   4.270 -  let
   4.271 -    fun decode_case ((t as Const (@{const_name case_cons}, _) $ _ $ _) $ u) =
   4.272 -        make_case ctxt Error Name.context (decode_case u) (decode_cases t)
   4.273 -    | decode_case (t $ u) = decode_case t $ decode_case u
   4.274 -    | decode_case (Abs (x, T, u)) =
   4.275 -        let val (x', u') = Term.dest_abs (x, T, u);
   4.276 -        in Term.absfree (x', T) (decode_case u') end
   4.277 -    | decode_case t = t;
   4.278 -  in
   4.279 -    map decode_case
   4.280 -  end;
   4.281 -
   4.282 -val term_check_setup =
   4.283 -  Context.theory_map (Syntax_Phases.term_check 1 "case" check_case);
   4.284 -
   4.285 -
   4.286 -(* parse translation *)
   4.287 -
   4.288 -fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
   4.289 -
   4.290 -fun case_tr ctxt [t, u] =
   4.291 -      let
   4.292 -        val thy = Proof_Context.theory_of ctxt;
   4.293 -
   4.294 -        fun is_const s =
   4.295 -          Sign.declared_const thy (Proof_Context.intern_const ctxt s);
   4.296 -
   4.297 -        fun abs p tTs t = Syntax.const @{const_syntax case_abs} $
   4.298 -          fold constrain_Abs tTs (absfree p t);
   4.299 -
   4.300 -        fun abs_pat (Const ("_constrain", _) $ t $ tT) tTs = abs_pat t (tT :: tTs)
   4.301 -          | abs_pat (Free (p as (x, _))) tTs =
   4.302 -              if is_const x then I else abs p tTs
   4.303 -          | abs_pat (t $ u) _ = abs_pat u [] #> abs_pat t []
   4.304 -          | abs_pat _ _ = I;
   4.305 -
   4.306 -        fun dest_case1 (Const (@{syntax_const "_case1"}, _) $ l $ r) =
   4.307 -              abs_pat l []
   4.308 -                (Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l $ r)
   4.309 -          | dest_case1 _ = case_error "dest_case1";
   4.310 -
   4.311 -        fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
   4.312 -          | dest_case2 t = [t];
   4.313 -      in
   4.314 -        fold_rev
   4.315 -          (fn t => fn u =>
   4.316 -             Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u)
   4.317 -          (dest_case2 u)
   4.318 -          (Syntax.const @{const_syntax case_nil}) $ t
   4.319 -      end
   4.320 -  | case_tr _ _ = case_error "case_tr";
   4.321 -
   4.322 -val trfun_setup =
   4.323 -  Sign.add_advanced_trfuns ([],
   4.324 -    [(@{syntax_const "_case_syntax"}, case_tr)],
   4.325 -    [], []);
   4.326 -
   4.327 -
   4.328 -(* Pretty printing of nested case expressions *)
   4.329 -
   4.330 -val name_of = try (dest_Const #> fst);
   4.331 -
   4.332 -(* destruct one level of pattern matching *)
   4.333 -
   4.334 -fun dest_case ctxt d used t =
   4.335 -  (case apfst name_of (strip_comb t) of
   4.336 -    (SOME cname, ts as _ :: _) =>
   4.337 -      let
   4.338 -        val (fs, x) = split_last ts;
   4.339 -        fun strip_abs i Us t =
   4.340 -          let
   4.341 -            val zs = strip_abs_vars t;
   4.342 -            val j = length zs;
   4.343 -            val (xs, ys) =
   4.344 -              if j < i then (zs @ map (pair "x") (drop j Us), [])
   4.345 -              else chop i zs;
   4.346 -            val u = fold_rev Term.abs ys (strip_abs_body t);
   4.347 -            val xs' = map Free
   4.348 -              ((fold_map Name.variant (map fst xs)
   4.349 -                  (Term.declare_term_names u used) |> fst) ~~
   4.350 -               map snd xs);
   4.351 -            val (xs1, xs2) = chop j xs'
   4.352 -          in (xs', list_comb (subst_bounds (rev xs1, u), xs2)) end;
   4.353 -        fun is_dependent i t =
   4.354 -          let val k = length (strip_abs_vars t) - i
   4.355 -          in k < 0 orelse exists (fn j => j >= k) (loose_bnos (strip_abs_body t)) end;
   4.356 -        fun count_cases (_, _, true) = I
   4.357 -          | count_cases (c, (_, body), false) = AList.map_default op aconv (body, []) (cons c);
   4.358 -        val is_undefined = name_of #> equal (SOME @{const_name undefined});
   4.359 -        fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body);
   4.360 -        val get_info = Datatype_Data.info_of_case (Proof_Context.theory_of ctxt);
   4.361 -      in
   4.362 -        (case Option.map ty_info (get_info cname) of
   4.363 -          SOME {constructors, ...} =>
   4.364 -            if length fs = length constructors then
   4.365 -              let
   4.366 -                val cases = map (fn (Const (s, U), t) =>
   4.367 -                  let
   4.368 -                    val Us = binder_types U;
   4.369 -                    val k = length Us;
   4.370 -                    val p as (xs, _) = strip_abs k Us t;
   4.371 -                  in
   4.372 -                    (Const (s, map fastype_of xs ---> fastype_of x), p, is_dependent k t)
   4.373 -                  end) (constructors ~~ fs);
   4.374 -                val cases' =
   4.375 -                  sort (int_ord o swap o pairself (length o snd))
   4.376 -                    (fold_rev count_cases cases []);
   4.377 -                val R = fastype_of t;
   4.378 -                val dummy =
   4.379 -                  if d then Term.dummy_pattern R
   4.380 -                  else Free (Name.variant "x" used |> fst, R);
   4.381 -              in
   4.382 -                SOME (x,
   4.383 -                  map mk_case
   4.384 -                    (case find_first (is_undefined o fst) cases' of
   4.385 -                      SOME (_, cs) =>
   4.386 -                        if length cs = length constructors then [hd cases]
   4.387 -                        else filter_out (fn (_, (_, body), _) => is_undefined body) cases
   4.388 -                    | NONE =>
   4.389 -                        (case cases' of
   4.390 -                          [] => cases
   4.391 -                        | (default, cs) :: _ =>
   4.392 -                            if length cs = 1 then cases
   4.393 -                            else if length cs = length constructors then
   4.394 -                              [hd cases, (dummy, ([], default), false)]
   4.395 -                            else
   4.396 -                              filter_out (fn (c, _, _) => member op aconv cs c) cases @
   4.397 -                                [(dummy, ([], default), false)])))
   4.398 -              end
   4.399 -            else NONE
   4.400 -        | _ => NONE)
   4.401 -      end
   4.402 -  | _ => NONE);
   4.403 -
   4.404 -
   4.405 -(* destruct nested patterns *)
   4.406 -
   4.407 -fun encode_clause S T (pat, rhs) =
   4.408 -  fold (fn x as (_, U) => fn t =>
   4.409 -    Const (@{const_name case_abs}, (U --> T) --> T) $ Term.absfree x t)
   4.410 -      (Term.add_frees pat [])
   4.411 -      (Const (@{const_name case_elem}, S --> T --> S --> T) $ pat $ rhs);
   4.412 -
   4.413 -fun encode_cases S T [] = Const (@{const_name case_nil}, S --> T)
   4.414 -  | encode_cases S T (p :: ps) =
   4.415 -      Const (@{const_name case_cons}, (S --> T) --> (S --> T) --> S --> T) $
   4.416 -        encode_clause S T p $ encode_cases S T ps;
   4.417 -
   4.418 -fun encode_case (t, ps as (pat, rhs) :: _) =
   4.419 -      encode_cases (fastype_of pat) (fastype_of rhs) ps $ t
   4.420 -  | encode_case _ = case_error "encode_case";
   4.421 -
   4.422 -fun strip_case' ctxt d (pat, rhs) =
   4.423 -  (case dest_case ctxt d (Term.declare_term_frees pat Name.context) rhs of
   4.424 -    SOME (exp as Free _, clauses) =>
   4.425 -      if Term.exists_subterm (curry (op aconv) exp) pat andalso
   4.426 -        not (exists (fn (_, rhs') =>
   4.427 -          Term.exists_subterm (curry (op aconv) exp) rhs') clauses)
   4.428 -      then
   4.429 -        maps (strip_case' ctxt d) (map (fn (pat', rhs') =>
   4.430 -          (subst_free [(exp, pat')] pat, rhs')) clauses)
   4.431 -      else [(pat, rhs)]
   4.432 -  | _ => [(pat, rhs)]);
   4.433 -
   4.434 -fun strip_case ctxt d t =
   4.435 -  (case dest_case ctxt d Name.context t of
   4.436 -    SOME (x, clauses) => encode_case (x, maps (strip_case' ctxt d) clauses)
   4.437 -  | NONE =>
   4.438 -    (case t of
   4.439 -      (t $ u) => strip_case ctxt d t $ strip_case ctxt d u
   4.440 -    | (Abs (x, T, u)) =>
   4.441 -        let val (x', u') = Term.dest_abs (x, T, u);
   4.442 -        in Term.absfree (x', T) (strip_case ctxt d u') end
   4.443 -    | _ => t));
   4.444 -
   4.445 -
   4.446 -(* term uncheck *)
   4.447 -
   4.448 -val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true);
   4.449 -
   4.450 -fun uncheck_case ctxt ts =
   4.451 -  if Config.get ctxt show_cases then map (strip_case ctxt true) ts else ts;
   4.452 -
   4.453 -val term_uncheck_setup =
   4.454 -  Context.theory_map (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
   4.455 -
   4.456 -
   4.457 -(* print translation *)
   4.458 -
   4.459 -fun case_tr' [t, u, x] =
   4.460 -      let
   4.461 -        fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used =
   4.462 -              let val (s', used') = Name.variant s used
   4.463 -              in mk_clause t ((s', T) :: xs) used' end
   4.464 -          | mk_clause (Const (@{const_syntax case_elem}, _) $ pat $ rhs) xs _ =
   4.465 -              Syntax.const @{syntax_const "_case1"} $
   4.466 -                subst_bounds (map Syntax_Trans.mark_bound_abs xs, pat) $
   4.467 -                subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs);
   4.468 -
   4.469 -        fun mk_clauses (Const (@{const_syntax case_nil}, _)) = []
   4.470 -          | mk_clauses (Const (@{const_syntax case_cons}, _) $ t $ u) =
   4.471 -              mk_clauses' t u
   4.472 -        and mk_clauses' t u =
   4.473 -              mk_clause t [] (Term.declare_term_frees t Name.context) ::
   4.474 -              mk_clauses u
   4.475 -      in
   4.476 -        Syntax.const @{syntax_const "_case_syntax"} $ x $
   4.477 -          foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
   4.478 -            (mk_clauses' t u)
   4.479 -      end;
   4.480 -
   4.481 -val trfun_setup' = Sign.add_trfuns
   4.482 -  ([], [], [(@{const_syntax "case_cons"}, case_tr')], []);
   4.483 -
   4.484 -
   4.485 -(* theory setup *)
   4.486 -
   4.487 -val setup =
   4.488 -  trfun_setup #>
   4.489 -  trfun_setup' #>
   4.490 -  term_check_setup #>
   4.491 -  term_uncheck_setup;
   4.492 -
   4.493 -end;
     5.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Tue Jan 22 13:32:41 2013 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Tue Jan 22 14:33:45 2013 +0100
     5.3 @@ -518,6 +518,12 @@
     5.4      val unnamed_rules = map (fn induct =>
     5.5        ((Binding.empty, [Rule_Cases.inner_rule, Induct.induct_type ""]), [([induct], [])]))
     5.6          (drop (length dt_names) inducts);
     5.7 +
     5.8 +    val ctxt = Proof_Context.init_global thy9;
     5.9 +    val case_combs = map (Proof_Context.read_const ctxt false dummyT) case_names;
    5.10 +    val constrss = map (fn (dtname, {descr, index, ...}) =>
    5.11 +      map (Proof_Context.read_const ctxt false dummyT o fst)
    5.12 +        (#3 (the (AList.lookup op = descr index)))) dt_infos
    5.13    in
    5.14      thy9
    5.15      |> Global_Theory.note_thmss ""
    5.16 @@ -535,6 +541,7 @@
    5.17            named_rules @ unnamed_rules)
    5.18      |> snd
    5.19      |> Datatype_Data.register dt_infos
    5.20 +    |> Context.theory_map (fold2 Case_Translation.register case_combs constrss)
    5.21      |> Datatype_Data.interpretation_data (config, dt_names)
    5.22      |> pair dt_names
    5.23    end;
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Jan 22 13:32:41 2013 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Jan 22 14:33:45 2013 +0100
     6.3 @@ -640,7 +640,7 @@
     6.4      val v = Free (name, T);
     6.5      val v' = Free (name', T);
     6.6    in
     6.7 -    lambda v (Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context v
     6.8 +    lambda v (Case_Translation.make_case ctxt Case_Translation.Quiet Name.context v
     6.9        [(HOLogic.mk_tuple out_ts,
    6.10          if null eqs'' then success_t
    6.11          else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
    6.12 @@ -916,7 +916,7 @@
    6.13          in
    6.14            (pattern, compilation)
    6.15          end
    6.16 -        val switch = Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context inp_var
    6.17 +        val switch = Case_Translation.make_case ctxt Case_Translation.Quiet Name.context inp_var
    6.18            ((map compile_single_case switched_clauses) @
    6.19              [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
    6.20        in
     7.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Jan 22 13:32:41 2013 +0100
     7.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Jan 22 14:33:45 2013 +0100
     7.3 @@ -293,7 +293,7 @@
     7.4                  val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
     7.5                in
     7.6                  mk_test (vars_of lhs,
     7.7 -                  Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context lhs
     7.8 +                  Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs
     7.9                      [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
    7.10                end
    7.11              else c (assm, assms)
     8.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jan 22 13:32:41 2013 +0100
     8.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jan 22 14:33:45 2013 +0100
     8.3 @@ -427,7 +427,7 @@
     8.4    end
     8.5  
     8.6  fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
     8.7 -    Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context (Free (x, T)) (map (fn (t, c) =>
     8.8 +    Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) =>
     8.9        (t, mk_case_term ctxt (p - 1) qs' c)) cs)
    8.10    | mk_case_term ctxt p ((@{const_name All}, _) :: qs') (Universal_Counterexample (t, c)) =
    8.11      if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/case_translation.ML	Tue Jan 22 14:33:45 2013 +0100
     9.3 @@ -0,0 +1,590 @@
     9.4 +(*  Title:      Tools/case_translation.ML
     9.5 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     9.6 +    Author:     Stefan Berghofer, TU Muenchen
     9.7 +    Author:     Dmitriy Traytel, TU Muenchen
     9.8 +
     9.9 +Nested case expressions via a generic data slot for case combinators and constructors.
    9.10 +*)
    9.11 +
    9.12 +signature CASE_TRANSLATION =
    9.13 +sig
    9.14 +  datatype config = Error | Warning | Quiet
    9.15 +  val case_tr: Proof.context -> term list -> term
    9.16 +  val lookup_by_constr: Proof.context -> string * typ -> (term * term list) option
    9.17 +  val lookup_by_constr_permissive: Proof.context -> string * typ -> (term * term list) option
    9.18 +  val lookup_by_case: Proof.context -> string -> (term * term list) option
    9.19 +  val make_case:  Proof.context -> config -> Name.context -> term -> (term * term) list -> term
    9.20 +  val print_case_translations: Proof.context -> unit
    9.21 +  val strip_case: Proof.context -> bool -> term -> term
    9.22 +  val show_cases: bool Config.T
    9.23 +  val setup: theory -> theory
    9.24 +  val register: term -> term list -> Context.generic -> Context.generic
    9.25 +end;
    9.26 +
    9.27 +structure Case_Translation: CASE_TRANSLATION =
    9.28 +struct
    9.29 +
    9.30 +(** data management **)
    9.31 +
    9.32 +datatype data = Data of
    9.33 +  {constrs: (string * (term * term list)) list Symtab.table,
    9.34 +   cases: (term * term list) Symtab.table};
    9.35 +
    9.36 +fun make_data (constrs, cases) = Data {constrs = constrs, cases = cases};
    9.37 +
    9.38 +structure Data = Generic_Data
    9.39 +(
    9.40 +  type T = data;
    9.41 +  val empty = make_data (Symtab.empty, Symtab.empty);
    9.42 +  val extend = I;
    9.43 +  fun merge
    9.44 +    (Data {constrs = constrs1, cases = cases1},
    9.45 +     Data {constrs = constrs2, cases = cases2}) =
    9.46 +    make_data
    9.47 +      (Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
    9.48 +      Symtab.merge (K true) (cases1, cases2));
    9.49 +);
    9.50 +
    9.51 +fun map_data f =
    9.52 +  Data.map (fn Data {constrs, cases} => make_data (f (constrs, cases)));
    9.53 +fun map_constrs f = map_data (fn (constrs, cases) => (f constrs, cases));
    9.54 +fun map_cases f = map_data (fn (constrs, cases) => (constrs, f cases));
    9.55 +
    9.56 +val rep_data = (fn Data args => args) o Data.get o Context.Proof;
    9.57 +
    9.58 +fun T_of_data (comb, constrs) =
    9.59 +  fastype_of comb
    9.60 +  |> funpow (length constrs) range_type
    9.61 +  |> domain_type;
    9.62 +
    9.63 +val Tname_of_data = fst o dest_Type o T_of_data;
    9.64 +
    9.65 +val constrs_of = #constrs o rep_data;
    9.66 +val cases_of = #cases o rep_data;
    9.67 +
    9.68 +fun lookup_by_constr ctxt (c, T) =
    9.69 +  let
    9.70 +    val tab = Symtab.lookup_list (constrs_of ctxt) c;
    9.71 +  in
    9.72 +    (case body_type T of
    9.73 +      Type (tyco, _) => AList.lookup (op =) tab tyco
    9.74 +    | _ => NONE)
    9.75 +  end;
    9.76 +
    9.77 +fun lookup_by_constr_permissive ctxt (c, T) =
    9.78 +  let
    9.79 +    val tab = Symtab.lookup_list (constrs_of ctxt) c;
    9.80 +    val hint = (case body_type T of Type (tyco, _) => SOME tyco | _ => NONE);
    9.81 +    val default = if null tab then NONE else SOME (snd (List.last tab));
    9.82 +    (*conservative wrt. overloaded constructors*)
    9.83 +  in
    9.84 +    (case hint of
    9.85 +      NONE => default
    9.86 +    | SOME tyco =>
    9.87 +        (case AList.lookup (op =) tab tyco of
    9.88 +          NONE => default (*permissive*)
    9.89 +        | SOME info => SOME info))
    9.90 +  end;
    9.91 +
    9.92 +val lookup_by_case = Symtab.lookup o cases_of;
    9.93 +
    9.94 +
    9.95 +(** installation **)
    9.96 +
    9.97 +fun case_error s = error ("Error in case expression:\n" ^ s);
    9.98 +
    9.99 +val name_of = try (dest_Const #> fst);
   9.100 +
   9.101 +(* parse translation *)
   9.102 +
   9.103 +fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
   9.104 +
   9.105 +fun case_tr ctxt [t, u] =
   9.106 +      let
   9.107 +        val thy = Proof_Context.theory_of ctxt;
   9.108 +
   9.109 +        fun is_const s =
   9.110 +          Sign.declared_const thy (Proof_Context.intern_const ctxt s);
   9.111 +
   9.112 +        fun abs p tTs t = Syntax.const @{const_syntax case_abs} $
   9.113 +          fold constrain_Abs tTs (absfree p t);
   9.114 +
   9.115 +        fun abs_pat (Const ("_constrain", _) $ t $ tT) tTs = abs_pat t (tT :: tTs)
   9.116 +          | abs_pat (Free (p as (x, _))) tTs =
   9.117 +              if is_const x then I else abs p tTs
   9.118 +          | abs_pat (t $ u) _ = abs_pat u [] #> abs_pat t []
   9.119 +          | abs_pat _ _ = I;
   9.120 +
   9.121 +        fun dest_case1 (Const (@{syntax_const "_case1"}, _) $ l $ r) =
   9.122 +              abs_pat l []
   9.123 +                (Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l $ r)
   9.124 +          | dest_case1 _ = case_error "dest_case1";
   9.125 +
   9.126 +        fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
   9.127 +          | dest_case2 t = [t];
   9.128 +      in
   9.129 +        fold_rev
   9.130 +          (fn t => fn u =>
   9.131 +             Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u)
   9.132 +          (dest_case2 u)
   9.133 +          (Syntax.const @{const_syntax case_nil}) $ t
   9.134 +      end
   9.135 +  | case_tr _ _ = case_error "case_tr";
   9.136 +
   9.137 +val trfun_setup =
   9.138 +  Sign.add_advanced_trfuns ([],
   9.139 +    [(@{syntax_const "_case_syntax"}, case_tr)],
   9.140 +    [], []);
   9.141 +
   9.142 +
   9.143 +(* print translation *)
   9.144 +
   9.145 +fun case_tr' [t, u, x] =
   9.146 +      let
   9.147 +        fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used =
   9.148 +              let val (s', used') = Name.variant s used
   9.149 +              in mk_clause t ((s', T) :: xs) used' end
   9.150 +          | mk_clause (Const (@{const_syntax case_elem}, _) $ pat $ rhs) xs _ =
   9.151 +              Syntax.const @{syntax_const "_case1"} $
   9.152 +                subst_bounds (map Syntax_Trans.mark_bound_abs xs, pat) $
   9.153 +                subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs);
   9.154 +
   9.155 +        fun mk_clauses (Const (@{const_syntax case_nil}, _)) = []
   9.156 +          | mk_clauses (Const (@{const_syntax case_cons}, _) $ t $ u) =
   9.157 +              mk_clauses' t u
   9.158 +        and mk_clauses' t u =
   9.159 +              mk_clause t [] (Term.declare_term_frees t Name.context) ::
   9.160 +              mk_clauses u
   9.161 +      in
   9.162 +        Syntax.const @{syntax_const "_case_syntax"} $ x $
   9.163 +          foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
   9.164 +            (mk_clauses' t u)
   9.165 +      end;
   9.166 +
   9.167 +val trfun_setup' = Sign.add_trfuns
   9.168 +  ([], [], [(@{const_syntax "case_cons"}, case_tr')], []);
   9.169 +
   9.170 +
   9.171 +(* declarations *)
   9.172 +
   9.173 +fun register raw_case_comb raw_constrs context =
   9.174 +  let
   9.175 +    val ctxt = Context.proof_of context;
   9.176 +    val case_comb = singleton (Variable.polymorphic ctxt) raw_case_comb;
   9.177 +    val constrs = Variable.polymorphic ctxt raw_constrs;
   9.178 +    val case_key = case_comb |> dest_Const |> fst;
   9.179 +    val constr_keys = map (fst o dest_Const) constrs;
   9.180 +    val data = (case_comb, constrs);
   9.181 +    val Tname = Tname_of_data data;
   9.182 +    val update_constrs = fold (fn key => Symtab.cons_list (key, (Tname, data))) constr_keys;
   9.183 +    val update_cases = Symtab.update (case_key, data);
   9.184 +  in
   9.185 +    context
   9.186 +    |> map_constrs update_constrs
   9.187 +    |> map_cases update_cases
   9.188 +  end;
   9.189 +
   9.190 +
   9.191 +(* (Un)check phases *)
   9.192 +
   9.193 +datatype config = Error | Warning | Quiet;
   9.194 +
   9.195 +exception CASE_ERROR of string * int;
   9.196 +
   9.197 +fun match_type ctxt pat ob =
   9.198 +  Sign.typ_match (Proof_Context.theory_of ctxt) (pat, ob) Vartab.empty;
   9.199 +
   9.200 +
   9.201 +(*Each pattern carries with it a tag i, which denotes the clause it
   9.202 +came from. i = ~1 indicates that the clause was added by pattern
   9.203 +completion.*)
   9.204 +
   9.205 +fun add_row_used ((prfx, pats), (tm, tag)) =
   9.206 +  fold Term.declare_term_frees (tm :: pats @ map Free prfx);
   9.207 +
   9.208 +(* try to preserve names given by user *)
   9.209 +fun default_name "" (Free (name', _)) = name'
   9.210 +  | default_name name _ = name;
   9.211 +
   9.212 +
   9.213 +(*Produce an instance of a constructor, plus fresh variables for its arguments.*)
   9.214 +fun fresh_constr ctxt colty used c =
   9.215 +  let
   9.216 +    val (_, T) = dest_Const c;
   9.217 +    val Ts = binder_types T;
   9.218 +    val (names, _) = fold_map Name.variant
   9.219 +      (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used;
   9.220 +    val ty = body_type T;
   9.221 +    val ty_theta = match_type ctxt ty colty
   9.222 +      handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
   9.223 +    val c' = Envir.subst_term_types ty_theta c;
   9.224 +    val gvars = map (Envir.subst_term_types ty_theta o Free) (names ~~ Ts);
   9.225 +  in (c', gvars) end;
   9.226 +
   9.227 +(*Go through a list of rows and pick out the ones beginning with a
   9.228 +  pattern with constructor = name.*)
   9.229 +fun mk_group (name, T) rows =
   9.230 +  let val k = length (binder_types T) in
   9.231 +    fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) =>
   9.232 +      fn ((in_group, not_in_group), names) =>
   9.233 +        (case strip_comb p of
   9.234 +          (Const (name', _), args) =>
   9.235 +            if name = name' then
   9.236 +              if length args = k then
   9.237 +                ((((prfx, args @ ps), rhs) :: in_group, not_in_group),
   9.238 +                 map2 default_name names args)
   9.239 +              else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ quote name, i)
   9.240 +            else ((in_group, row :: not_in_group), names)
   9.241 +        | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
   9.242 +    rows (([], []), replicate k "") |>> pairself rev
   9.243 +  end;
   9.244 +
   9.245 +
   9.246 +(* Partitioning *)
   9.247 +
   9.248 +fun partition _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
   9.249 +  | partition ctxt used constructors colty res_ty
   9.250 +        (rows as (((prfx, _ :: ps), _) :: _)) =
   9.251 +      let
   9.252 +        fun part [] [] = []
   9.253 +          | part [] ((_, (_, i)) :: _) = raise CASE_ERROR ("Not a constructor pattern", i)
   9.254 +          | part (c :: cs) rows =
   9.255 +              let
   9.256 +                val ((in_group, not_in_group), names) = mk_group (dest_Const c) rows;
   9.257 +                val used' = fold add_row_used in_group used;
   9.258 +                val (c', gvars) = fresh_constr ctxt colty used' c;
   9.259 +                val in_group' =
   9.260 +                  if null in_group  (* Constructor not given *)
   9.261 +                  then
   9.262 +                    let
   9.263 +                      val Ts = map fastype_of ps;
   9.264 +                      val (xs, _) =
   9.265 +                        fold_map Name.variant
   9.266 +                          (replicate (length ps) "x")
   9.267 +                          (fold Term.declare_term_frees gvars used');
   9.268 +                    in
   9.269 +                      [((prfx, gvars @ map Free (xs ~~ Ts)),
   9.270 +                        (Const (@{const_name undefined}, res_ty), ~1))]
   9.271 +                    end
   9.272 +                  else in_group;
   9.273 +              in
   9.274 +                {constructor = c',
   9.275 +                 new_formals = gvars,
   9.276 +                 names = names,
   9.277 +                 group = in_group'} :: part cs not_in_group
   9.278 +              end;
   9.279 +      in part constructors rows end;
   9.280 +
   9.281 +fun v_to_prfx (prfx, Free v :: pats) = (v :: prfx, pats)
   9.282 +  | v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
   9.283 +
   9.284 +
   9.285 +(* Translation of pattern terms into nested case expressions. *)
   9.286 +
   9.287 +fun mk_case ctxt used range_ty =
   9.288 +  let
   9.289 +    val get_info = lookup_by_constr_permissive ctxt;
   9.290 +
   9.291 +    fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1)
   9.292 +      | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
   9.293 +          if is_Free p then
   9.294 +            let
   9.295 +              val used' = add_row_used row used;
   9.296 +              fun expnd c =
   9.297 +                let val capp = list_comb (fresh_constr ctxt ty used' c)
   9.298 +                in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag)) end;
   9.299 +            in map expnd constructors end
   9.300 +          else [row];
   9.301 +
   9.302 +    val (name, _) = Name.variant "a" used;
   9.303 +
   9.304 +    fun mk _ [] = raise CASE_ERROR ("no rows", ~1)
   9.305 +      | mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *)
   9.306 +      | mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
   9.307 +      | mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
   9.308 +          let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
   9.309 +            (case Option.map (apfst head_of)
   9.310 +                (find_first (not o is_Free o fst) col0) of
   9.311 +              NONE =>
   9.312 +                let
   9.313 +                  val rows' = map (fn ((v, _), row) => row ||>
   9.314 +                    apfst (subst_free [(v, u)]) |>> v_to_prfx) (col0 ~~ rows);
   9.315 +                in mk us rows' end
   9.316 +            | SOME (Const (cname, cT), i) =>
   9.317 +                (case get_info (cname, cT) of
   9.318 +                  NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ quote cname, i)
   9.319 +                | SOME (case_comb, constructors) =>
   9.320 +                    let
   9.321 +                      val pty = body_type cT;
   9.322 +                      val used' = fold Term.declare_term_frees us used;
   9.323 +                      val nrows = maps (expand constructors used' pty) rows;
   9.324 +                      val subproblems =
   9.325 +                        partition ctxt used' constructors pty range_ty nrows;
   9.326 +                      val (pat_rect, dtrees) =
   9.327 +                        split_list (map (fn {new_formals, group, ...} =>
   9.328 +                          mk (new_formals @ us) group) subproblems);
   9.329 +                      val case_functions =
   9.330 +                        map2 (fn {new_formals, names, ...} =>
   9.331 +                          fold_rev (fn (x as Free (_, T), s) => fn t =>
   9.332 +                            Abs (if s = "" then name else s, T, abstract_over (x, t)))
   9.333 +                              (new_formals ~~ names))
   9.334 +                        subproblems dtrees;
   9.335 +                      val types = map fastype_of (case_functions @ [u]);
   9.336 +                      val case_const = Const (name_of case_comb |> the, types ---> range_ty);
   9.337 +                      val tree = list_comb (case_const, case_functions @ [u]);
   9.338 +                    in (flat pat_rect, tree) end)
   9.339 +            | SOME (t, i) =>
   9.340 +                raise CASE_ERROR ("Not a datatype constructor: " ^ Syntax.string_of_term ctxt t, i))
   9.341 +          end
   9.342 +      | mk _ _ = raise CASE_ERROR ("Malformed row matrix", ~1)
   9.343 +  in mk end;
   9.344 +
   9.345 +
   9.346 +(* replace occurrences of dummy_pattern by distinct variables *)
   9.347 +fun replace_dummies (Const (@{const_name dummy_pattern}, T)) used =
   9.348 +      let val (x, used') = Name.variant "x" used
   9.349 +      in (Free (x, T), used') end
   9.350 +  | replace_dummies (t $ u) used =
   9.351 +      let
   9.352 +        val (t', used') = replace_dummies t used;
   9.353 +        val (u', used'') = replace_dummies u used';
   9.354 +      in (t' $ u', used'') end
   9.355 +  | replace_dummies t used = (t, used);
   9.356 +
   9.357 +(*Repeated variable occurrences in a pattern are not allowed.*)
   9.358 +fun no_repeat_vars ctxt pat = fold_aterms
   9.359 +  (fn x as Free (s, _) =>
   9.360 +      (fn xs =>
   9.361 +        if member op aconv xs x then
   9.362 +          case_error (quote s ^ " occurs repeatedly in the pattern " ^
   9.363 +            quote (Syntax.string_of_term ctxt pat))
   9.364 +        else x :: xs)
   9.365 +    | _ => I) pat [];
   9.366 +
   9.367 +fun make_case ctxt config used x clauses =
   9.368 +  let
   9.369 +    fun string_of_clause (pat, rhs) =
   9.370 +      Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
   9.371 +    val _ = map (no_repeat_vars ctxt o fst) clauses;
   9.372 +    val (rows, used') = used |>
   9.373 +      fold (fn (pat, rhs) =>
   9.374 +        Term.declare_term_frees pat #> Term.declare_term_frees rhs) clauses |>
   9.375 +      fold_map (fn (i, (pat, rhs)) => fn used =>
   9.376 +        let val (pat', used') = replace_dummies pat used
   9.377 +        in ((([], [pat']), (rhs, i)), used') end)
   9.378 +          (map_index I clauses);
   9.379 +    val rangeT =
   9.380 +      (case distinct (op =) (map (fastype_of o snd) clauses) of
   9.381 +        [] => case_error "no clauses given"
   9.382 +      | [T] => T
   9.383 +      | _ => case_error "all cases must have the same result type");
   9.384 +    val used' = fold add_row_used rows used;
   9.385 +    val (tags, case_tm) =
   9.386 +      mk_case ctxt used' rangeT [x] rows
   9.387 +        handle CASE_ERROR (msg, i) =>
   9.388 +          case_error
   9.389 +            (msg ^ (if i < 0 then "" else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
   9.390 +    val _ =
   9.391 +      (case subtract (op =) tags (map (snd o snd) rows) of
   9.392 +        [] => ()
   9.393 +      | is =>
   9.394 +          (case config of Error => case_error | Warning => warning | Quiet => fn _ => ())
   9.395 +            ("The following clauses are redundant (covered by preceding clauses):\n" ^
   9.396 +              cat_lines (map (string_of_clause o nth clauses) is)));
   9.397 +  in
   9.398 +    case_tm
   9.399 +  end;
   9.400 +
   9.401 +
   9.402 +(* term check *)
   9.403 +
   9.404 +fun decode_clause (Const (@{const_name case_abs}, _) $ Abs (s, T, t)) xs used =
   9.405 +      let val (s', used') = Name.variant s used
   9.406 +      in decode_clause t (Free (s', T) :: xs) used' end
   9.407 +  | decode_clause (Const (@{const_name case_elem}, _) $ t $ u) xs _ =
   9.408 +      (subst_bounds (xs, t), subst_bounds (xs, u))
   9.409 +  | decode_clause _ _ _ = case_error "decode_clause";
   9.410 +
   9.411 +fun decode_cases (Const (@{const_name case_nil}, _)) = []
   9.412 +  | decode_cases (Const (@{const_name case_cons}, _) $ t $ u) =
   9.413 +      decode_clause t [] (Term.declare_term_frees t Name.context) ::
   9.414 +      decode_cases u
   9.415 +  | decode_cases _ = case_error "decode_cases";
   9.416 +
   9.417 +fun check_case ctxt =
   9.418 +  let
   9.419 +    fun decode_case ((t as Const (@{const_name case_cons}, _) $ _ $ _) $ u) =
   9.420 +        make_case ctxt Error Name.context (decode_case u) (decode_cases t)
   9.421 +    | decode_case (t $ u) = decode_case t $ decode_case u
   9.422 +    | decode_case (Abs (x, T, u)) =
   9.423 +        let val (x', u') = Term.dest_abs (x, T, u);
   9.424 +        in Term.absfree (x', T) (decode_case u') end
   9.425 +    | decode_case t = t;
   9.426 +  in
   9.427 +    map decode_case
   9.428 +  end;
   9.429 +
   9.430 +val term_check_setup =
   9.431 +  Context.theory_map (Syntax_Phases.term_check 1 "case" check_case);
   9.432 +
   9.433 +
   9.434 +(* Pretty printing of nested case expressions *)
   9.435 +
   9.436 +(* destruct one level of pattern matching *)
   9.437 +
   9.438 +fun dest_case ctxt d used t =
   9.439 +  (case apfst name_of (strip_comb t) of
   9.440 +    (SOME cname, ts as _ :: _) =>
   9.441 +      let
   9.442 +        val (fs, x) = split_last ts;
   9.443 +        fun strip_abs i Us t =
   9.444 +          let
   9.445 +            val zs = strip_abs_vars t;
   9.446 +            val j = length zs;
   9.447 +            val (xs, ys) =
   9.448 +              if j < i then (zs @ map (pair "x") (drop j Us), [])
   9.449 +              else chop i zs;
   9.450 +            val u = fold_rev Term.abs ys (strip_abs_body t);
   9.451 +            val xs' = map Free
   9.452 +              ((fold_map Name.variant (map fst xs)
   9.453 +                  (Term.declare_term_names u used) |> fst) ~~
   9.454 +               map snd xs);
   9.455 +            val (xs1, xs2) = chop j xs'
   9.456 +          in (xs', list_comb (subst_bounds (rev xs1, u), xs2)) end;
   9.457 +        fun is_dependent i t =
   9.458 +          let val k = length (strip_abs_vars t) - i
   9.459 +          in k < 0 orelse exists (fn j => j >= k) (loose_bnos (strip_abs_body t)) end;
   9.460 +        fun count_cases (_, _, true) = I
   9.461 +          | count_cases (c, (_, body), false) = AList.map_default op aconv (body, []) (cons c);
   9.462 +        val is_undefined = name_of #> equal (SOME @{const_name undefined});
   9.463 +        fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body);
   9.464 +        val get_info = lookup_by_case ctxt;
   9.465 +      in
   9.466 +        (case get_info cname of
   9.467 +          SOME (_, constructors) =>
   9.468 +            if length fs = length constructors then
   9.469 +              let
   9.470 +                val cases = map (fn (Const (s, U), t) =>
   9.471 +                  let
   9.472 +                    val Us = binder_types U;
   9.473 +                    val k = length Us;
   9.474 +                    val p as (xs, _) = strip_abs k Us t;
   9.475 +                  in
   9.476 +                    (Const (s, map fastype_of xs ---> fastype_of x), p, is_dependent k t)
   9.477 +                  end) (constructors ~~ fs);
   9.478 +                val cases' =
   9.479 +                  sort (int_ord o swap o pairself (length o snd))
   9.480 +                    (fold_rev count_cases cases []);
   9.481 +                val R = fastype_of t;
   9.482 +                val dummy =
   9.483 +                  if d then Term.dummy_pattern R
   9.484 +                  else Free (Name.variant "x" used |> fst, R);
   9.485 +              in
   9.486 +                SOME (x,
   9.487 +                  map mk_case
   9.488 +                    (case find_first (is_undefined o fst) cases' of
   9.489 +                      SOME (_, cs) =>
   9.490 +                        if length cs = length constructors then [hd cases]
   9.491 +                        else filter_out (fn (_, (_, body), _) => is_undefined body) cases
   9.492 +                    | NONE =>
   9.493 +                        (case cases' of
   9.494 +                          [] => cases
   9.495 +                        | (default, cs) :: _ =>
   9.496 +                            if length cs = 1 then cases
   9.497 +                            else if length cs = length constructors then
   9.498 +                              [hd cases, (dummy, ([], default), false)]
   9.499 +                            else
   9.500 +                              filter_out (fn (c, _, _) => member op aconv cs c) cases @
   9.501 +                                [(dummy, ([], default), false)])))
   9.502 +              end
   9.503 +            else NONE
   9.504 +        | _ => NONE)
   9.505 +      end
   9.506 +  | _ => NONE);
   9.507 +
   9.508 +
   9.509 +(* destruct nested patterns *)
   9.510 +
   9.511 +fun encode_clause S T (pat, rhs) =
   9.512 +  fold (fn x as (_, U) => fn t =>
   9.513 +    Const (@{const_name case_abs}, (U --> T) --> T) $ Term.absfree x t)
   9.514 +      (Term.add_frees pat [])
   9.515 +      (Const (@{const_name case_elem}, S --> T --> S --> T) $ pat $ rhs);
   9.516 +
   9.517 +fun encode_cases S T [] = Const (@{const_name case_nil}, S --> T)
   9.518 +  | encode_cases S T (p :: ps) =
   9.519 +      Const (@{const_name case_cons}, (S --> T) --> (S --> T) --> S --> T) $
   9.520 +        encode_clause S T p $ encode_cases S T ps;
   9.521 +
   9.522 +fun encode_case (t, ps as (pat, rhs) :: _) =
   9.523 +      encode_cases (fastype_of pat) (fastype_of rhs) ps $ t
   9.524 +  | encode_case _ = case_error "encode_case";
   9.525 +
   9.526 +fun strip_case' ctxt d (pat, rhs) =
   9.527 +  (case dest_case ctxt d (Term.declare_term_frees pat Name.context) rhs of
   9.528 +    SOME (exp as Free _, clauses) =>
   9.529 +      if Term.exists_subterm (curry (op aconv) exp) pat andalso
   9.530 +        not (exists (fn (_, rhs') =>
   9.531 +          Term.exists_subterm (curry (op aconv) exp) rhs') clauses)
   9.532 +      then
   9.533 +        maps (strip_case' ctxt d) (map (fn (pat', rhs') =>
   9.534 +          (subst_free [(exp, pat')] pat, rhs')) clauses)
   9.535 +      else [(pat, rhs)]
   9.536 +  | _ => [(pat, rhs)]);
   9.537 +
   9.538 +fun strip_case ctxt d t =
   9.539 +  (case dest_case ctxt d Name.context t of
   9.540 +    SOME (x, clauses) => encode_case (x, maps (strip_case' ctxt d) clauses)
   9.541 +  | NONE =>
   9.542 +    (case t of
   9.543 +      (t $ u) => strip_case ctxt d t $ strip_case ctxt d u
   9.544 +    | (Abs (x, T, u)) =>
   9.545 +        let val (x', u') = Term.dest_abs (x, T, u);
   9.546 +        in Term.absfree (x', T) (strip_case ctxt d u') end
   9.547 +    | _ => t));
   9.548 +
   9.549 +
   9.550 +(* term uncheck *)
   9.551 +
   9.552 +val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true);
   9.553 +
   9.554 +fun uncheck_case ctxt ts =
   9.555 +  if Config.get ctxt show_cases then map (strip_case ctxt true) ts else ts;
   9.556 +
   9.557 +val term_uncheck_setup =
   9.558 +  Context.theory_map (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
   9.559 +
   9.560 +
   9.561 +(* theory setup *)
   9.562 +
   9.563 +val setup =
   9.564 +  trfun_setup #>
   9.565 +  trfun_setup' #>
   9.566 +  term_check_setup #>
   9.567 +  term_uncheck_setup;
   9.568 +
   9.569 +
   9.570 +(* outer syntax commands *)
   9.571 +
   9.572 +fun print_case_translations ctxt =
   9.573 +  let
   9.574 +    val cases = Symtab.dest (cases_of ctxt);
   9.575 +    fun show_case (_, data as (comb, ctrs)) =
   9.576 +      Pretty.big_list
   9.577 +        (Pretty.string_of (Pretty.block [Pretty.str (Tname_of_data data), Pretty.str ":"]))
   9.578 +        [Pretty.block [Pretty.brk 3, Pretty.block
   9.579 +          [Pretty.str "combinator:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt comb)]],
   9.580 +        Pretty.block [Pretty.brk 3, Pretty.block
   9.581 +          [Pretty.str "constructors:", Pretty.brk 1,
   9.582 +             Pretty.list "" "" (map (Pretty.quote o Syntax.pretty_term ctxt) ctrs)]]];
   9.583 +  in
   9.584 +    Pretty.big_list "Case translations:" (map show_case cases)
   9.585 +    |> Pretty.writeln
   9.586 +  end;
   9.587 +
   9.588 +val _ =
   9.589 +  Outer_Syntax.improper_command @{command_spec "print_case_translations"}
   9.590 +    "print registered case combinators and constructors"
   9.591 +    (Scan.succeed (Toplevel.keep (print_case_translations o Toplevel.context_of)))
   9.592 +
   9.593 +end;