case translations performed in a separate check phase (with adjustments by traytel)
authorberghofe
Tue Jan 22 13:32:41 2013 +0100 (2013-01-22)
changeset 51672d5c5e088ebdf
parent 51671 0d142a78fb7c
child 51673 4dfa00e264d8
case translations performed in a separate check phase (with adjustments by traytel)
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
     1.1 --- a/src/HOL/Inductive.thy	Wed Apr 10 13:10:38 2013 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Jan 22 13:32:41 2013 +0100
     1.3 @@ -273,7 +273,14 @@
     1.4  ML_file "Tools/Datatype/datatype_aux.ML"
     1.5  ML_file "Tools/Datatype/datatype_prop.ML"
     1.6  ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
     1.7 +
     1.8 +consts
     1.9 +  case_nil :: "'a \<Rightarrow> 'b"
    1.10 +  case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.11 +  case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
    1.12 +  case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
    1.13  ML_file "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
    1.14 +
    1.15  ML_file "Tools/Datatype/rep_datatype.ML"
    1.16  ML_file "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup
    1.17  ML_file "Tools/Datatype/primrec.ML"
    1.18 @@ -290,7 +297,7 @@
    1.19    fun fun_tr ctxt [cs] =
    1.20      let
    1.21        val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
    1.22 -      val ft = Datatype_Case.case_tr true ctxt [x, cs];
    1.23 +      val ft = Datatype_Case.case_tr ctxt [x, cs];
    1.24      in lambda x ft end
    1.25  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
    1.26  *}
     2.1 --- a/src/HOL/List.thy	Wed Apr 10 13:10:38 2013 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Jan 22 13:32:41 2013 +0100
     2.3 @@ -407,7 +407,7 @@
     2.4            Syntax.const @{syntax_const "_case1"} $
     2.5              Syntax.const @{const_syntax dummy_pattern} $ NilC;
     2.6          val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
     2.7 -      in Syntax_Trans.abs_tr [x, Datatype_Case.case_tr false ctxt [x, cs]] end;
     2.8 +      in Syntax_Trans.abs_tr [x, Datatype_Case.case_tr ctxt [x, cs]] end;
     2.9  
    2.10      fun abs_tr ctxt p e opti =
    2.11        (case Term_Position.strip_positions p of
     3.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Wed Apr 10 13:10:38 2013 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Tue Jan 22 13:32:41 2013 +0100
     3.3 @@ -5,12 +5,6 @@
     3.4  Datatype package: nested case expressions on datatypes.
     3.5  
     3.6  TODO:
     3.7 -  * Avoid fragile operations on syntax trees (with type constraints
     3.8 -    getting in the way).  Instead work with auxiliary "destructor"
     3.9 -    constants in translations and introduce the actual case
    3.10 -    combinators in a separate term check phase (similar to term
    3.11 -    abbreviations).
    3.12 -
    3.13    * Avoid hard-wiring with datatype package.  Instead provide generic
    3.14      generic declarations of case splits based on an internal data slot.
    3.15  *)
    3.16 @@ -19,12 +13,10 @@
    3.17  sig
    3.18    datatype config = Error | Warning | Quiet
    3.19    type info = Datatype_Aux.info
    3.20 -  val make_case :  Proof.context -> config -> string list -> term -> (term * term) list -> term
    3.21 -  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    3.22 -  val case_tr: bool -> Proof.context -> term list -> term
    3.23 +  val case_tr: Proof.context -> term list -> term
    3.24 +  val make_case:  Proof.context -> config -> Name.context -> term -> (term * term) list -> term
    3.25 +  val strip_case: Proof.context -> bool -> term -> term
    3.26    val show_cases: bool Config.T
    3.27 -  val case_tr': string -> Proof.context -> term list -> term
    3.28 -  val add_case_tr' : string list -> theory -> theory
    3.29    val setup: theory -> theory
    3.30  end;
    3.31  
    3.32 @@ -36,7 +28,8 @@
    3.33  
    3.34  exception CASE_ERROR of string * int;
    3.35  
    3.36 -fun match_type thy pat ob = Sign.typ_match thy (pat, ob) Vartab.empty;
    3.37 +fun match_type ctxt pat ob =
    3.38 +  Sign.typ_match (Proof_Context.theory_of ctxt) (pat, ob) Vartab.empty;
    3.39  
    3.40  (* Get information about datatypes *)
    3.41  
    3.42 @@ -57,101 +50,77 @@
    3.43  completion.*)
    3.44  
    3.45  fun add_row_used ((prfx, pats), (tm, tag)) =
    3.46 -  fold Term.add_free_names (tm :: pats @ map Free prfx);
    3.47 +  fold Term.declare_term_frees (tm :: pats @ map Free prfx);
    3.48  
    3.49 -fun default_name name (t, cs) =
    3.50 -  let
    3.51 -    val name' = if name = "" then (case t of Free (name', _) => name' | _ => name) else name;
    3.52 -    val cs' = if is_Free t then cs else filter_out Term_Position.is_position cs;
    3.53 -  in (name', cs') end;
    3.54 -
    3.55 -fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
    3.56 -      strip_constraints t ||> cons tT
    3.57 -  | strip_constraints t = (t, []);
    3.58 -
    3.59 -fun constrain tT t = Syntax.const @{syntax_const "_constrain"} $ t $ tT;
    3.60 -fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
    3.61 +(* try to preserve names given by user *)
    3.62 +fun default_name "" (Free (name', _)) = name'
    3.63 +  | default_name name _ = name;
    3.64  
    3.65  
    3.66  (*Produce an instance of a constructor, plus fresh variables for its arguments.*)
    3.67 -fun fresh_constr ty_match ty_inst colty used c =
    3.68 +fun fresh_constr ctxt colty used c =
    3.69    let
    3.70      val (_, T) = dest_Const c;
    3.71      val Ts = binder_types T;
    3.72 -    val names =
    3.73 -      Name.variant_list used (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
    3.74 +    val (names, _) = fold_map Name.variant
    3.75 +      (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used;
    3.76      val ty = body_type T;
    3.77 -    val ty_theta = ty_match ty colty
    3.78 +    val ty_theta = match_type ctxt ty colty
    3.79        handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
    3.80 -    val c' = ty_inst ty_theta c;
    3.81 -    val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts);
    3.82 +    val c' = Envir.subst_term_types ty_theta c;
    3.83 +    val gvars = map (Envir.subst_term_types ty_theta o Free) (names ~~ Ts);
    3.84    in (c', gvars) end;
    3.85  
    3.86 -fun strip_comb_positions tm =
    3.87 -  let
    3.88 -    fun result t ts = (Term_Position.strip_positions t, ts);
    3.89 -    fun strip (t as Const (@{syntax_const "_constrain"}, _) $ _ $ _) ts = result t ts
    3.90 -      | strip (f $ t) ts = strip f (t :: ts)
    3.91 -      | strip t ts = result t ts;
    3.92 -  in strip tm [] end;
    3.93 -
    3.94  (*Go through a list of rows and pick out the ones beginning with a
    3.95    pattern with constructor = name.*)
    3.96  fun mk_group (name, T) rows =
    3.97    let val k = length (binder_types T) in
    3.98      fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) =>
    3.99 -      fn ((in_group, not_in_group), (names, cnstrts)) =>
   3.100 -        (case strip_comb_positions p of
   3.101 +      fn ((in_group, not_in_group), names) =>
   3.102 +        (case strip_comb p of
   3.103            (Const (name', _), args) =>
   3.104              if name = name' then
   3.105                if length args = k then
   3.106 -                let
   3.107 -                  val constraints' = map strip_constraints args;
   3.108 -                  val (args', cnstrts') = split_list constraints';
   3.109 -                  val (names', cnstrts'') = split_list (map2 default_name names constraints');
   3.110 -                in
   3.111 -                  ((((prfx, args' @ ps), rhs) :: in_group, not_in_group),
   3.112 -                   (names', map2 append cnstrts cnstrts''))
   3.113 -                end
   3.114 +                ((((prfx, args @ ps), rhs) :: in_group, not_in_group),
   3.115 +                 map2 default_name names args)
   3.116                else raise CASE_ERROR ("Wrong number of arguments for constructor " ^ quote name, i)
   3.117 -            else ((in_group, row :: not_in_group), (names, cnstrts))
   3.118 +            else ((in_group, row :: not_in_group), names)
   3.119          | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
   3.120 -    rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
   3.121 +    rows (([], []), replicate k "") |>> pairself rev
   3.122    end;
   3.123  
   3.124  
   3.125  (* Partitioning *)
   3.126  
   3.127 -fun partition _ _ _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
   3.128 -  | partition ty_match ty_inst type_of used constructors colty res_ty
   3.129 +fun partition _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
   3.130 +  | partition ctxt used constructors colty res_ty
   3.131          (rows as (((prfx, _ :: ps), _) :: _)) =
   3.132        let
   3.133          fun part [] [] = []
   3.134            | part [] ((_, (_, i)) :: _) = raise CASE_ERROR ("Not a constructor pattern", i)
   3.135            | part (c :: cs) rows =
   3.136                let
   3.137 -                val ((in_group, not_in_group), (names, cnstrts)) = mk_group (dest_Const c) rows;
   3.138 +                val ((in_group, not_in_group), names) = mk_group (dest_Const c) rows;
   3.139                  val used' = fold add_row_used in_group used;
   3.140 -                val (c', gvars) = fresh_constr ty_match ty_inst colty used' c;
   3.141 +                val (c', gvars) = fresh_constr ctxt colty used' c;
   3.142                  val in_group' =
   3.143                    if null in_group  (* Constructor not given *)
   3.144                    then
   3.145                      let
   3.146 -                      val Ts = map type_of ps;
   3.147 -                      val xs =
   3.148 -                        Name.variant_list
   3.149 -                          (fold Term.add_free_names gvars used')
   3.150 -                          (replicate (length ps) "x");
   3.151 +                      val Ts = map fastype_of ps;
   3.152 +                      val (xs, _) =
   3.153 +                        fold_map Name.variant
   3.154 +                          (replicate (length ps) "x")
   3.155 +                          (fold Term.declare_term_frees gvars used');
   3.156                      in
   3.157                        [((prfx, gvars @ map Free (xs ~~ Ts)),
   3.158 -                        (Const (@{const_syntax undefined}, res_ty), ~1))]
   3.159 +                        (Const (@{const_name undefined}, res_ty), ~1))]
   3.160                      end
   3.161                    else in_group;
   3.162                in
   3.163                  {constructor = c',
   3.164                   new_formals = gvars,
   3.165                   names = names,
   3.166 -                 constraints = cnstrts,
   3.167                   group = in_group'} :: part cs not_in_group
   3.168                end;
   3.169        in part constructors rows end;
   3.170 @@ -162,7 +131,7 @@
   3.171  
   3.172  (* Translation of pattern terms into nested case expressions. *)
   3.173  
   3.174 -fun mk_case ctxt ty_match ty_inst type_of used range_ty =
   3.175 +fun mk_case ctxt used range_ty =
   3.176    let
   3.177      val get_info = Datatype_Data.info_of_constr_permissive (Proof_Context.theory_of ctxt);
   3.178  
   3.179 @@ -172,19 +141,19 @@
   3.180              let
   3.181                val used' = add_row_used row used;
   3.182                fun expnd c =
   3.183 -                let val capp = list_comb (fresh_constr ty_match ty_inst ty used' c)
   3.184 +                let val capp = list_comb (fresh_constr ctxt ty used' c)
   3.185                  in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag)) end;
   3.186              in map expnd constructors end
   3.187            else [row];
   3.188  
   3.189 -    val name = singleton (Name.variant_list used) "a";
   3.190 +    val (name, _) = Name.variant "a" used;
   3.191  
   3.192      fun mk _ [] = raise CASE_ERROR ("no rows", ~1)
   3.193        | mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *)
   3.194        | mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
   3.195        | mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
   3.196            let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
   3.197 -            (case Option.map (apfst (fst o strip_comb_positions))
   3.198 +            (case Option.map (apfst head_of)
   3.199                  (find_first (not o is_Free o fst) col0) of
   3.200                NONE =>
   3.201                  let
   3.202 @@ -197,21 +166,20 @@
   3.203                  | SOME {case_name, constructors} =>
   3.204                      let
   3.205                        val pty = body_type cT;
   3.206 -                      val used' = fold Term.add_free_names us used;
   3.207 +                      val used' = fold Term.declare_term_frees us used;
   3.208                        val nrows = maps (expand constructors used' pty) rows;
   3.209                        val subproblems =
   3.210 -                        partition ty_match ty_inst type_of used'
   3.211 -                          constructors pty range_ty nrows;
   3.212 +                        partition ctxt used' constructors pty range_ty nrows;
   3.213                        val (pat_rect, dtrees) =
   3.214                          split_list (map (fn {new_formals, group, ...} =>
   3.215                            mk (new_formals @ us) group) subproblems);
   3.216                        val case_functions =
   3.217 -                        map2 (fn {new_formals, names, constraints, ...} =>
   3.218 -                          fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
   3.219 -                            Abs (if s = "" then name else s, T, abstract_over (x, t))
   3.220 -                            |> fold constrain_Abs cnstrts) (new_formals ~~ names ~~ constraints))
   3.221 +                        map2 (fn {new_formals, names, ...} =>
   3.222 +                          fold_rev (fn (x as Free (_, T), s) => fn t =>
   3.223 +                            Abs (if s = "" then name else s, T, abstract_over (x, t)))
   3.224 +                              (new_formals ~~ names))
   3.225                          subproblems dtrees;
   3.226 -                      val types = map type_of (case_functions @ [u]);
   3.227 +                      val types = map fastype_of (case_functions @ [u]);
   3.228                        val case_const = Const (case_name, types ---> range_ty);
   3.229                        val tree = list_comb (case_const, case_functions @ [u]);
   3.230                      in (flat pat_rect, tree) end)
   3.231 @@ -221,9 +189,19 @@
   3.232        | mk _ _ = raise CASE_ERROR ("Malformed row matrix", ~1)
   3.233    in mk end;
   3.234  
   3.235 -fun case_error s = error ("Error in case expression:\n" ^ s);
   3.236  
   3.237 -local
   3.238 +(* replace occurrences of dummy_pattern by distinct variables *)
   3.239 +fun replace_dummies (Const (@{const_name dummy_pattern}, T)) used =
   3.240 +      let val (x, used') = Name.variant "x" used
   3.241 +      in (Free (x, T), used') end
   3.242 +  | replace_dummies (t $ u) used =
   3.243 +      let
   3.244 +        val (t', used') = replace_dummies t used;
   3.245 +        val (u', used'') = replace_dummies u used';
   3.246 +      in (t' $ u', used'') end
   3.247 +  | replace_dummies t used = (t, used);
   3.248 +
   3.249 +fun case_error s = error ("Error in case expression:\n" ^ s);
   3.250  
   3.251  (*Repeated variable occurrences in a pattern are not allowed.*)
   3.252  fun no_repeat_vars ctxt pat = fold_aterms
   3.253 @@ -233,22 +211,28 @@
   3.254            case_error (quote s ^ " occurs repeatedly in the pattern " ^
   3.255              quote (Syntax.string_of_term ctxt pat))
   3.256          else x :: xs)
   3.257 -    | _ => I) (Term_Position.strip_positions pat) [];
   3.258 +    | _ => I) pat [];
   3.259  
   3.260 -fun gen_make_case ty_match ty_inst type_of ctxt config used x clauses =
   3.261 +fun make_case ctxt config used x clauses =
   3.262    let
   3.263      fun string_of_clause (pat, rhs) =
   3.264        Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
   3.265      val _ = map (no_repeat_vars ctxt o fst) clauses;
   3.266 -    val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses;
   3.267 +    val (rows, used') = used |>
   3.268 +      fold (fn (pat, rhs) =>
   3.269 +        Term.declare_term_frees pat #> Term.declare_term_frees rhs) clauses |>
   3.270 +      fold_map (fn (i, (pat, rhs)) => fn used =>
   3.271 +        let val (pat', used') = replace_dummies pat used
   3.272 +        in ((([], [pat']), (rhs, i)), used') end)
   3.273 +          (map_index I clauses);
   3.274      val rangeT =
   3.275 -      (case distinct (op =) (map (type_of o snd) clauses) of
   3.276 +      (case distinct (op =) (map (fastype_of o snd) clauses) of
   3.277          [] => case_error "no clauses given"
   3.278        | [T] => T
   3.279        | _ => case_error "all cases must have the same result type");
   3.280      val used' = fold add_row_used rows used;
   3.281      val (tags, case_tm) =
   3.282 -      mk_case ctxt ty_match ty_inst type_of used' rangeT [x] rows
   3.283 +      mk_case ctxt used' rangeT [x] rows
   3.284          handle CASE_ERROR (msg, i) =>
   3.285            case_error
   3.286              (msg ^ (if i < 0 then "" else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
   3.287 @@ -263,77 +247,88 @@
   3.288      case_tm
   3.289    end;
   3.290  
   3.291 -in
   3.292 +
   3.293 +(* term check *)
   3.294 +
   3.295 +fun decode_clause (Const (@{const_name case_abs}, _) $ Abs (s, T, t)) xs used =
   3.296 +      let val (s', used') = Name.variant s used
   3.297 +      in decode_clause t (Free (s', T) :: xs) used' end
   3.298 +  | decode_clause (Const (@{const_name case_elem}, _) $ t $ u) xs _ =
   3.299 +      (subst_bounds (xs, t), subst_bounds (xs, u))
   3.300 +  | decode_clause _ _ _ = case_error "decode_clause";
   3.301 +
   3.302 +fun decode_cases (Const (@{const_name case_nil}, _)) = []
   3.303 +  | decode_cases (Const (@{const_name case_cons}, _) $ t $ u) =
   3.304 +      decode_clause t [] (Term.declare_term_frees t Name.context) ::
   3.305 +      decode_cases u
   3.306 +  | decode_cases _ = case_error "decode_cases";
   3.307  
   3.308 -fun make_case ctxt =
   3.309 -  gen_make_case (match_type (Proof_Context.theory_of ctxt))
   3.310 -    Envir.subst_term_types fastype_of ctxt;
   3.311 +fun check_case ctxt =
   3.312 +  let
   3.313 +    fun decode_case ((t as Const (@{const_name case_cons}, _) $ _ $ _) $ u) =
   3.314 +        make_case ctxt Error Name.context (decode_case u) (decode_cases t)
   3.315 +    | decode_case (t $ u) = decode_case t $ decode_case u
   3.316 +    | decode_case (Abs (x, T, u)) =
   3.317 +        let val (x', u') = Term.dest_abs (x, T, u);
   3.318 +        in Term.absfree (x', T) (decode_case u') end
   3.319 +    | decode_case t = t;
   3.320 +  in
   3.321 +    map decode_case
   3.322 +  end;
   3.323  
   3.324 -val make_case_untyped =
   3.325 -  gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT);
   3.326 -
   3.327 -end;
   3.328 +val term_check_setup =
   3.329 +  Context.theory_map (Syntax_Phases.term_check 1 "case" check_case);
   3.330  
   3.331  
   3.332  (* parse translation *)
   3.333  
   3.334 -fun case_tr err ctxt [t, u] =
   3.335 +fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
   3.336 +
   3.337 +fun case_tr ctxt [t, u] =
   3.338        let
   3.339          val thy = Proof_Context.theory_of ctxt;
   3.340 -        val intern_const_syntax = Consts.intern_syntax (Proof_Context.consts_of ctxt);
   3.341 +
   3.342 +        fun is_const s =
   3.343 +          Sign.declared_const thy (Proof_Context.intern_const ctxt s);
   3.344 +
   3.345 +        fun abs p tTs t = Syntax.const @{const_syntax case_abs} $
   3.346 +          fold constrain_Abs tTs (absfree p t);
   3.347  
   3.348 -        (* replace occurrences of dummy_pattern by distinct variables *)
   3.349 -        (* internalize constant names                                 *)
   3.350 -        (* FIXME proper name context!? *)
   3.351 -        fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
   3.352 -              let val (t', used') = prep_pat t used
   3.353 -              in (c $ t' $ tT, used') end
   3.354 -          | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
   3.355 -              let val x = singleton (Name.variant_list used) "x"
   3.356 -              in (Free (x, T), x :: used) end
   3.357 -          | prep_pat (Const (s, T)) used = (Const (intern_const_syntax s, T), used)
   3.358 -          | prep_pat (v as Free (s, T)) used =
   3.359 -              let val s' = Proof_Context.intern_const ctxt s in
   3.360 -                if Sign.declared_const thy s' then (Const (s', T), used)
   3.361 -                else (v, used)
   3.362 -              end
   3.363 -          | prep_pat (t $ u) used =
   3.364 -              let
   3.365 -                val (t', used') = prep_pat t used;
   3.366 -                val (u', used'') = prep_pat u used';
   3.367 -              in (t' $ u', used'') end
   3.368 -          | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
   3.369 +        fun abs_pat (Const ("_constrain", _) $ t $ tT) tTs = abs_pat t (tT :: tTs)
   3.370 +          | abs_pat (Free (p as (x, _))) tTs =
   3.371 +              if is_const x then I else abs p tTs
   3.372 +          | abs_pat (t $ u) _ = abs_pat u [] #> abs_pat t []
   3.373 +          | abs_pat _ _ = I;
   3.374  
   3.375 -        fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
   3.376 -              let val (l', cnstrts) = strip_constraints l
   3.377 -              in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts) end
   3.378 -          | dest_case1 t = case_error "dest_case1";
   3.379 +        fun dest_case1 (Const (@{syntax_const "_case1"}, _) $ l $ r) =
   3.380 +              abs_pat l []
   3.381 +                (Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l $ r)
   3.382 +          | dest_case1 _ = case_error "dest_case1";
   3.383  
   3.384          fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
   3.385            | dest_case2 t = [t];
   3.386 -
   3.387 -        val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
   3.388        in
   3.389 -        make_case_untyped ctxt
   3.390 -          (if err then Error else Warning) []
   3.391 -          (fold constrain (filter_out Term_Position.is_position (flat cnstrts)) t)
   3.392 -          cases
   3.393 +        fold_rev
   3.394 +          (fn t => fn u =>
   3.395 +             Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u)
   3.396 +          (dest_case2 u)
   3.397 +          (Syntax.const @{const_syntax case_nil}) $ t
   3.398        end
   3.399 -  | case_tr _ _ _ = case_error "case_tr";
   3.400 +  | case_tr _ _ = case_error "case_tr";
   3.401  
   3.402  val trfun_setup =
   3.403    Sign.add_advanced_trfuns ([],
   3.404 -    [(@{syntax_const "_case_syntax"}, case_tr true)],
   3.405 +    [(@{syntax_const "_case_syntax"}, case_tr)],
   3.406      [], []);
   3.407  
   3.408  
   3.409  (* Pretty printing of nested case expressions *)
   3.410  
   3.411 +val name_of = try (dest_Const #> fst);
   3.412 +
   3.413  (* destruct one level of pattern matching *)
   3.414  
   3.415 -local
   3.416 -
   3.417 -fun gen_dest_case name_of type_of ctxt d used t =
   3.418 +fun dest_case ctxt d used t =
   3.419    (case apfst name_of (strip_comb t) of
   3.420      (SOME cname, ts as _ :: _) =>
   3.421        let
   3.422 @@ -371,12 +366,12 @@
   3.423                      val k = length Us;
   3.424                      val p as (xs, _) = strip_abs k Us t;
   3.425                    in
   3.426 -                    (Const (s, map type_of xs ---> type_of x), p, is_dependent k t)
   3.427 +                    (Const (s, map fastype_of xs ---> fastype_of x), p, is_dependent k t)
   3.428                    end) (constructors ~~ fs);
   3.429                  val cases' =
   3.430                    sort (int_ord o swap o pairself (length o snd))
   3.431                      (fold_rev count_cases cases []);
   3.432 -                val R = type_of t;
   3.433 +                val R = fastype_of t;
   3.434                  val dummy =
   3.435                    if d then Term.dummy_pattern R
   3.436                    else Free (Name.variant "x" used |> fst, R);
   3.437 @@ -403,81 +398,93 @@
   3.438        end
   3.439    | _ => NONE);
   3.440  
   3.441 -in
   3.442 -
   3.443 -val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
   3.444 -val dest_case' = gen_dest_case (try (dest_Const #> fst #> Lexicon.unmark_const)) (K dummyT);
   3.445 -
   3.446 -end;
   3.447 -
   3.448  
   3.449  (* destruct nested patterns *)
   3.450  
   3.451 -local
   3.452 +fun encode_clause S T (pat, rhs) =
   3.453 +  fold (fn x as (_, U) => fn t =>
   3.454 +    Const (@{const_name case_abs}, (U --> T) --> T) $ Term.absfree x t)
   3.455 +      (Term.add_frees pat [])
   3.456 +      (Const (@{const_name case_elem}, S --> T --> S --> T) $ pat $ rhs);
   3.457  
   3.458 -fun strip_case'' dest (pat, rhs) =
   3.459 -  (case dest (Term.declare_term_frees pat Name.context) rhs of
   3.460 +fun encode_cases S T [] = Const (@{const_name case_nil}, S --> T)
   3.461 +  | encode_cases S T (p :: ps) =
   3.462 +      Const (@{const_name case_cons}, (S --> T) --> (S --> T) --> S --> T) $
   3.463 +        encode_clause S T p $ encode_cases S T ps;
   3.464 +
   3.465 +fun encode_case (t, ps as (pat, rhs) :: _) =
   3.466 +      encode_cases (fastype_of pat) (fastype_of rhs) ps $ t
   3.467 +  | encode_case _ = case_error "encode_case";
   3.468 +
   3.469 +fun strip_case' ctxt d (pat, rhs) =
   3.470 +  (case dest_case ctxt d (Term.declare_term_frees pat Name.context) rhs of
   3.471      SOME (exp as Free _, clauses) =>
   3.472        if Term.exists_subterm (curry (op aconv) exp) pat andalso
   3.473          not (exists (fn (_, rhs') =>
   3.474            Term.exists_subterm (curry (op aconv) exp) rhs') clauses)
   3.475        then
   3.476 -        maps (strip_case'' dest) (map (fn (pat', rhs') =>
   3.477 +        maps (strip_case' ctxt d) (map (fn (pat', rhs') =>
   3.478            (subst_free [(exp, pat')] pat, rhs')) clauses)
   3.479        else [(pat, rhs)]
   3.480    | _ => [(pat, rhs)]);
   3.481  
   3.482 -fun gen_strip_case dest t =
   3.483 -  (case dest Name.context t of
   3.484 -    SOME (x, clauses) => SOME (x, maps (strip_case'' dest) clauses)
   3.485 -  | NONE => NONE);
   3.486 +fun strip_case ctxt d t =
   3.487 +  (case dest_case ctxt d Name.context t of
   3.488 +    SOME (x, clauses) => encode_case (x, maps (strip_case' ctxt d) clauses)
   3.489 +  | NONE =>
   3.490 +    (case t of
   3.491 +      (t $ u) => strip_case ctxt d t $ strip_case ctxt d u
   3.492 +    | (Abs (x, T, u)) =>
   3.493 +        let val (x', u') = Term.dest_abs (x, T, u);
   3.494 +        in Term.absfree (x', T) (strip_case ctxt d u') end
   3.495 +    | _ => t));
   3.496  
   3.497 -in
   3.498 +
   3.499 +(* term uncheck *)
   3.500 +
   3.501 +val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true);
   3.502  
   3.503 -val strip_case = gen_strip_case oo dest_case;
   3.504 -val strip_case' = gen_strip_case oo dest_case';
   3.505 +fun uncheck_case ctxt ts =
   3.506 +  if Config.get ctxt show_cases then map (strip_case ctxt true) ts else ts;
   3.507  
   3.508 -end;
   3.509 +val term_uncheck_setup =
   3.510 +  Context.theory_map (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
   3.511  
   3.512  
   3.513  (* print translation *)
   3.514  
   3.515 -val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true);
   3.516 +fun case_tr' [t, u, x] =
   3.517 +      let
   3.518 +        fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used =
   3.519 +              let val (s', used') = Name.variant s used
   3.520 +              in mk_clause t ((s', T) :: xs) used' end
   3.521 +          | mk_clause (Const (@{const_syntax case_elem}, _) $ pat $ rhs) xs _ =
   3.522 +              Syntax.const @{syntax_const "_case1"} $
   3.523 +                subst_bounds (map Syntax_Trans.mark_bound_abs xs, pat) $
   3.524 +                subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs);
   3.525  
   3.526 -fun case_tr' cname ctxt ts =
   3.527 -  if Config.get ctxt show_cases then
   3.528 -    let
   3.529 -      fun mk_clause (pat, rhs) =
   3.530 -        let val xs = Term.add_frees pat [] in
   3.531 -          Syntax.const @{syntax_const "_case1"} $
   3.532 -            map_aterms
   3.533 -              (fn Free p => Syntax_Trans.mark_bound_abs p
   3.534 -                | Const (s, _) => Syntax.const (Lexicon.mark_const s)
   3.535 -                | t => t) pat $
   3.536 -            map_aterms
   3.537 -              (fn x as Free v =>
   3.538 -                  if member (op =) xs v then Syntax_Trans.mark_bound_body v else x
   3.539 -                | t => t) rhs
   3.540 -        end;
   3.541 -    in
   3.542 -      (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of
   3.543 -        SOME (x, clauses) =>
   3.544 -          Syntax.const @{syntax_const "_case_syntax"} $ x $
   3.545 -            foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
   3.546 -              (map mk_clause clauses)
   3.547 -      | NONE => raise Match)
   3.548 -    end
   3.549 -  else raise Match;
   3.550 +        fun mk_clauses (Const (@{const_syntax case_nil}, _)) = []
   3.551 +          | mk_clauses (Const (@{const_syntax case_cons}, _) $ t $ u) =
   3.552 +              mk_clauses' t u
   3.553 +        and mk_clauses' t u =
   3.554 +              mk_clause t [] (Term.declare_term_frees t Name.context) ::
   3.555 +              mk_clauses u
   3.556 +      in
   3.557 +        Syntax.const @{syntax_const "_case_syntax"} $ x $
   3.558 +          foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
   3.559 +            (mk_clauses' t u)
   3.560 +      end;
   3.561  
   3.562 -fun add_case_tr' case_names thy =
   3.563 -  Sign.add_advanced_trfuns ([], [],
   3.564 -    map (fn case_name =>
   3.565 -      let val case_name' = Lexicon.mark_const case_name
   3.566 -      in (case_name', case_tr' case_name') end) case_names, []) thy;
   3.567 +val trfun_setup' = Sign.add_trfuns
   3.568 +  ([], [], [(@{const_syntax "case_cons"}, case_tr')], []);
   3.569  
   3.570  
   3.571  (* theory setup *)
   3.572  
   3.573 -val setup = trfun_setup;
   3.574 +val setup =
   3.575 +  trfun_setup #>
   3.576 +  trfun_setup' #>
   3.577 +  term_check_setup #>
   3.578 +  term_uncheck_setup;
   3.579  
   3.580  end;
     4.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Wed Apr 10 13:10:38 2013 +0200
     4.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Tue Jan 22 13:32:41 2013 +0100
     4.3 @@ -536,7 +536,6 @@
     4.4      |> snd
     4.5      |> Datatype_Data.register dt_infos
     4.6      |> Datatype_Data.interpretation_data (config, dt_names)
     4.7 -    |> Datatype_Case.add_case_tr' case_names
     4.8      |> pair dt_names
     4.9    end;
    4.10  
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 10 13:10:38 2013 +0200
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Jan 22 13:32:41 2013 +0100
     5.3 @@ -640,7 +640,7 @@
     5.4      val v = Free (name, T);
     5.5      val v' = Free (name', T);
     5.6    in
     5.7 -    lambda v (Datatype_Case.make_case ctxt Datatype_Case.Quiet [] v
     5.8 +    lambda v (Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context v
     5.9        [(HOLogic.mk_tuple out_ts,
    5.10          if null eqs'' then success_t
    5.11          else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
    5.12 @@ -916,7 +916,7 @@
    5.13          in
    5.14            (pattern, compilation)
    5.15          end
    5.16 -        val switch = Datatype_Case.make_case ctxt Datatype_Case.Quiet [] inp_var
    5.17 +        val switch = Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context inp_var
    5.18            ((map compile_single_case switched_clauses) @
    5.19              [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
    5.20        in
     6.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Apr 10 13:10:38 2013 +0200
     6.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Jan 22 13:32:41 2013 +0100
     6.3 @@ -292,8 +292,9 @@
     6.4                  val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars)
     6.5                  val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
     6.6                in
     6.7 -                mk_test (vars_of lhs, Datatype_Case.make_case ctxt Datatype_Case.Quiet [] lhs
     6.8 -                  [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
     6.9 +                mk_test (vars_of lhs,
    6.10 +                  Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context lhs
    6.11 +                    [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
    6.12                end
    6.13              else c (assm, assms)
    6.14          fun default (assm, assms) =
     7.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 10 13:10:38 2013 +0200
     7.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jan 22 13:32:41 2013 +0100
     7.3 @@ -427,7 +427,7 @@
     7.4    end
     7.5  
     7.6  fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
     7.7 -    Datatype_Case.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
     7.8 +    Datatype_Case.make_case ctxt Datatype_Case.Quiet Name.context (Free (x, T)) (map (fn (t, c) =>
     7.9        (t, mk_case_term ctxt (p - 1) qs' c)) cs)
    7.10    | mk_case_term ctxt p ((@{const_name All}, _) :: qs') (Universal_Counterexample (t, c)) =
    7.11      if p = 0 then t else mk_case_term ctxt (p - 1) qs' c