haftmann@33968: (*  Title:      HOL/Tools/Datatype/datatype_case.ML
berghofe@22779:     Author:     Konrad Slind, Cambridge University Computer Laboratory
wenzelm@29266:     Author:     Stefan Berghofer, TU Muenchen
berghofe@22779: 
haftmann@33968: Datatype package: nested case expressions on datatypes.
berghofe@22779: *)
berghofe@22779: 
berghofe@22779: signature DATATYPE_CASE =
berghofe@22779: sig
haftmann@33968:   datatype config = Error | Warning | Quiet
haftmann@33968:   type info = Datatype_Aux.info
haftmann@33968:   val make_case: (string * typ -> info option) ->
bulwahn@32671:     Proof.context -> config -> string list -> term -> (term * term) list ->
berghofe@22779:     term * (term * (int * bool)) list
haftmann@33968:   val dest_case: (string -> info option) -> bool ->
berghofe@22779:     string list -> term -> (term * (term * term) list) option
haftmann@33968:   val strip_case: (string -> info option) -> bool ->
berghofe@22779:     term -> (term * (term * term) list) option
haftmann@33968:   val case_tr: bool -> (theory -> string * typ -> info option) ->
haftmann@33968:     Proof.context -> term list -> term
haftmann@33968:   val case_tr': (theory -> string -> info option) ->
berghofe@22779:     string -> Proof.context -> term list -> term
berghofe@22779: end;
berghofe@22779: 
haftmann@33968: structure Datatype_Case : DATATYPE_CASE =
berghofe@22779: struct
berghofe@22779: 
bulwahn@32671: datatype config = Error | Warning | Quiet;
haftmann@33968: type info = Datatype_Aux.info;
bulwahn@32671: 
berghofe@22779: exception CASE_ERROR of string * int;
berghofe@22779: 
berghofe@22779: fun match_type thy pat ob = Sign.typ_match thy (pat, ob) Vartab.empty;
berghofe@22779: 
berghofe@22779: (*---------------------------------------------------------------------------
berghofe@22779:  * Get information about datatypes
berghofe@22779:  *---------------------------------------------------------------------------*)
berghofe@22779: 
haftmann@32896: fun ty_info tab sT =
wenzelm@42049:   (case tab sT of
haftmann@33968:     SOME ({descr, case_name, index, sorts, ...} : info) =>
berghofe@22779:       let
berghofe@22779:         val (_, (tname, dts, constrs)) = nth descr index;
haftmann@33968:         val mk_ty = Datatype_Aux.typ_of_dtyp descr sorts;
wenzelm@35124:         val T = Type (tname, map mk_ty dts);
berghofe@22779:       in
berghofe@22779:         SOME {case_name = case_name,
berghofe@22779:           constructors = map (fn (cname, dts') =>
wenzelm@35845:             Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs}
berghofe@22779:       end
wenzelm@42049:   | NONE => NONE);
berghofe@22779: 
berghofe@22779: 
berghofe@22779: (*---------------------------------------------------------------------------
berghofe@22779:  * Each pattern carries with it a tag (i,b) where
berghofe@22779:  * i is the clause it came from and
berghofe@22779:  * b=true indicates that clause was given by the user
berghofe@22779:  * (or is an instantiation of a user supplied pattern)
berghofe@22779:  * b=false --> i = ~1
berghofe@22779:  *---------------------------------------------------------------------------*)
berghofe@22779: 
wenzelm@29281: fun pattern_subst theta (tm, x) = (subst_free theta tm, x);
berghofe@22779: 
berghofe@22779: fun row_of_pat x = fst (snd x);
berghofe@22779: 
wenzelm@29281: fun add_row_used ((prfx, pats), (tm, tag)) =
wenzelm@29281:   fold Term.add_free_names (tm :: pats @ prfx);
berghofe@22779: 
berghofe@22779: (* try to preserve names given by user *)
berghofe@22779: fun default_names names ts =
berghofe@22779:   map (fn ("", Free (name', _)) => name' | (name, _) => name) (names ~~ ts);
berghofe@22779: 
wenzelm@35124: fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
berghofe@22779:       strip_constraints t ||> cons tT
berghofe@22779:   | strip_constraints t = (t, []);
berghofe@22779: 
wenzelm@35124: fun mk_fun_constrain tT t =
wenzelm@35124:   Syntax.const @{syntax_const "_constrain"} $ t $
wenzelm@35363:     (Syntax.const @{type_syntax fun} $ tT $ Syntax.const @{type_syntax dummy});
berghofe@22779: 
berghofe@22779: 
berghofe@22779: (*---------------------------------------------------------------------------
berghofe@22779:  * Produce an instance of a constructor, plus genvars for its arguments.
berghofe@22779:  *---------------------------------------------------------------------------*)
berghofe@22779: fun fresh_constr ty_match ty_inst colty used c =
berghofe@22779:   let
berghofe@22779:     val (_, Ty) = dest_Const c
berghofe@22779:     val Ts = binder_types Ty;
berghofe@22779:     val names = Name.variant_list used
wenzelm@35845:       (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
berghofe@22779:     val ty = body_type Ty;
berghofe@22779:     val ty_theta = ty_match ty colty handle Type.TYPE_MATCH =>
berghofe@22779:       raise CASE_ERROR ("type mismatch", ~1)
berghofe@22779:     val c' = ty_inst ty_theta c
berghofe@22779:     val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts)
wenzelm@42049:   in (c', gvars) end;
berghofe@22779: 
berghofe@22779: 
berghofe@22779: (*---------------------------------------------------------------------------
berghofe@22779:  * Goes through a list of rows and picks out the ones beginning with a
berghofe@22779:  * pattern with constructor = name.
berghofe@22779:  *---------------------------------------------------------------------------*)
berghofe@22779: fun mk_group (name, T) rows =
wenzelm@42049:   let val k = length (binder_types T) in
wenzelm@42049:     fold (fn (row as ((prfx, p :: rst), rhs as (_, (i, _)))) =>
wenzelm@42049:       fn ((in_group, not_in_group), (names, cnstrts)) =>
wenzelm@42049:         (case strip_comb p of
wenzelm@42049:           (Const (name', _), args) =>
wenzelm@42049:             if name = name' then
wenzelm@42049:               if length args = k then
wenzelm@42049:                 let val (args', cnstrts') = split_list (map strip_constraints args)
wenzelm@42049:                 in
wenzelm@42049:                   ((((prfx, args' @ rst), rhs) :: in_group, not_in_group),
wenzelm@42049:                    (default_names names args', map2 append cnstrts cnstrts'))
wenzelm@42049:                 end
wenzelm@42049:               else raise CASE_ERROR
wenzelm@42049:                 ("Wrong number of arguments for constructor " ^ name, i)
wenzelm@42049:             else ((in_group, row :: not_in_group), (names, cnstrts))
wenzelm@42049:         | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
berghofe@22779:     rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
berghofe@22779:   end;
berghofe@22779: 
berghofe@22779: (*---------------------------------------------------------------------------
berghofe@22779:  * Partition the rows. Not efficient: we should use hashing.
berghofe@22779:  *---------------------------------------------------------------------------*)
berghofe@22779: fun partition _ _ _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
berghofe@22779:   | partition ty_match ty_inst type_of used constructors colty res_ty
berghofe@22779:         (rows as (((prfx, _ :: rstp), _) :: _)) =
berghofe@22779:       let
berghofe@22779:         fun part {constrs = [], rows = [], A} = rev A
berghofe@22779:           | part {constrs = [], rows = (_, (_, (i, _))) :: _, A} =
berghofe@22779:               raise CASE_ERROR ("Not a constructor pattern", i)
berghofe@22779:           | part {constrs = c :: crst, rows, A} =
berghofe@22779:               let
berghofe@22779:                 val ((in_group, not_in_group), (names, cnstrts)) =
berghofe@22779:                   mk_group (dest_Const c) rows;
berghofe@22779:                 val used' = fold add_row_used in_group used;
berghofe@22779:                 val (c', gvars) = fresh_constr ty_match ty_inst colty used' c;
berghofe@22779:                 val in_group' =
berghofe@22779:                   if null in_group  (* Constructor not given *)
berghofe@22779:                   then
berghofe@22779:                     let
berghofe@22779:                       val Ts = map type_of rstp;
berghofe@22779:                       val xs = Name.variant_list
wenzelm@29281:                         (fold Term.add_free_names gvars used')
berghofe@22779:                         (replicate (length rstp) "x")
berghofe@22779:                     in
berghofe@22779:                       [((prfx, gvars @ map Free (xs ~~ Ts)),
wenzelm@35140:                         (Const (@{const_syntax undefined}, res_ty), (~1, false)))]
berghofe@22779:                     end
berghofe@22779:                   else in_group
berghofe@22779:               in
berghofe@22779:                 part{constrs = crst,
berghofe@22779:                   rows = not_in_group,
berghofe@22779:                   A = {constructor = c',
berghofe@22779:                     new_formals = gvars,
berghofe@22779:                     names = names,
berghofe@22779:                     constraints = cnstrts,
berghofe@22779:                     group = in_group'} :: A}
berghofe@22779:               end
wenzelm@42049:       in part {constrs = constructors, rows = rows, A = []} end;
berghofe@22779: 
berghofe@22779: (*---------------------------------------------------------------------------
berghofe@22779:  * Misc. routines used in mk_case
berghofe@22779:  *---------------------------------------------------------------------------*)
berghofe@22779: 
berghofe@22779: fun mk_pat ((c, c'), l) =
berghofe@22779:   let
berghofe@22779:     val L = length (binder_types (fastype_of c))
berghofe@22779:     fun build (prfx, tag, plist) =
berghofe@22779:       let val (args, plist') = chop L plist
berghofe@22779:       in (prfx, tag, list_comb (c', args) :: plist') end
berghofe@22779:   in map build l end;
berghofe@22779: 
berghofe@22779: fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
berghofe@22779:   | v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
berghofe@22779: 
berghofe@22779: fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
berghofe@22779:   | v_to_pats _ = raise CASE_ERROR ("mk_case: v_to_pats", ~1);
berghofe@22779: 
berghofe@22779: 
berghofe@22779: (*----------------------------------------------------------------------------
berghofe@22779:  * Translation of pattern terms into nested case expressions.
berghofe@22779:  *
berghofe@22779:  * This performs the translation and also builds the full set of patterns.
berghofe@22779:  * Thus it supports the construction of induction theorems even when an
berghofe@22779:  * incomplete set of patterns is given.
berghofe@22779:  *---------------------------------------------------------------------------*)
berghofe@22779: 
berghofe@22779: fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
berghofe@22779:   let
berghofe@22779:     val name = Name.variant used "a";
berghofe@22779:     fun expand constructors used ty ((_, []), _) =
berghofe@22779:           raise CASE_ERROR ("mk_case: expand_var_row", ~1)
berghofe@22779:       | expand constructors used ty (row as ((prfx, p :: rst), rhs)) =
berghofe@22779:           if is_Free p then
berghofe@22779:             let
berghofe@22779:               val used' = add_row_used row used;
berghofe@22779:               fun expnd c =
berghofe@22779:                 let val capp =
berghofe@22779:                   list_comb (fresh_constr ty_match ty_inst ty used' c)
berghofe@22779:                 in ((prfx, capp :: rst), pattern_subst [(p, capp)] rhs)
berghofe@22779:                 end
berghofe@22779:             in map expnd constructors end
berghofe@22779:           else [row]
berghofe@22779:     fun mk {rows = [], ...} = raise CASE_ERROR ("no rows", ~1)
berghofe@22779:       | mk {path = [], rows = ((prfx, []), (tm, tag)) :: _} =  (* Done *)
berghofe@22779:           ([(prfx, tag, [])], tm)
berghofe@22779:       | mk {path, rows as ((row as ((_, [Free _]), _)) :: _ :: _)} =
berghofe@22779:           mk {path = path, rows = [row]}
berghofe@22779:       | mk {path = u :: rstp, rows as ((_, _ :: _), _) :: _} =
wenzelm@42049:           let val col0 = map (fn ((_, p :: _), (_, (i, _))) => (p, i)) rows in
wenzelm@42049:             (case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
berghofe@22779:               NONE =>
berghofe@22779:                 let
berghofe@22779:                   val rows' = map (fn ((v, _), row) => row ||>
berghofe@22779:                     pattern_subst [(v, u)] |>> v_to_prfx) (col0 ~~ rows);
berghofe@22779:                   val (pref_patl, tm) = mk {path = rstp, rows = rows'}
berghofe@22779:                 in (map v_to_pats pref_patl, tm) end
wenzelm@42049:             | SOME (Const (cname, cT), i) =>
wenzelm@42049:                 (case ty_info tab (cname, cT) of
wenzelm@42049:                   NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
wenzelm@42049:                 | SOME {case_name, constructors} =>
wenzelm@42049:                   let
wenzelm@42049:                     val pty = body_type cT;
wenzelm@42049:                     val used' = fold Term.add_free_names rstp used;
wenzelm@42049:                     val nrows = maps (expand constructors used' pty) rows;
wenzelm@42049:                     val subproblems = partition ty_match ty_inst type_of used'
wenzelm@42049:                       constructors pty range_ty nrows;
wenzelm@42049:                     val constructors' = map #constructor subproblems
wenzelm@42049:                     val news = map (fn {new_formals, group, ...} =>
wenzelm@42049:                       {path = new_formals @ rstp, rows = group}) subproblems;
wenzelm@42049:                     val (pat_rect, dtrees) = split_list (map mk news);
wenzelm@42049:                     val case_functions = map2
wenzelm@42049:                       (fn {new_formals, names, constraints, ...} =>
wenzelm@42049:                          fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
wenzelm@42049:                            Abs (if s = "" then name else s, T,
wenzelm@42049:                              abstract_over (x, t)) |>
wenzelm@42049:                            fold mk_fun_constrain cnstrts)
wenzelm@42049:                              (new_formals ~~ names ~~ constraints))
wenzelm@42049:                       subproblems dtrees;
wenzelm@42049:                     val types = map type_of (case_functions @ [u]);
wenzelm@42049:                     val case_const = Const (case_name, types ---> range_ty)
wenzelm@42049:                     val tree = list_comb (case_const, case_functions @ [u])
wenzelm@42049:                     val pat_rect1 = maps mk_pat (constructors ~~ constructors' ~~ pat_rect)
wenzelm@42049:                   in (pat_rect1, tree) end)
berghofe@22779:             | SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
wenzelm@42049:                 Syntax.string_of_term ctxt t, i))
berghofe@22779:           end
berghofe@22779:       | mk _ = raise CASE_ERROR ("Malformed row matrix", ~1)
wenzelm@42049:   in mk end;
berghofe@22779: 
berghofe@22779: fun case_error s = error ("Error in case expression:\n" ^ s);
berghofe@22779: 
berghofe@22779: (* Repeated variable occurrences in a pattern are not allowed. *)
berghofe@22779: fun no_repeat_vars ctxt pat = fold_aterms
berghofe@22779:   (fn x as Free (s, _) => (fn xs =>
berghofe@22779:         if member op aconv xs x then
berghofe@22779:           case_error (quote s ^ " occurs repeatedly in the pattern " ^
wenzelm@24920:             quote (Syntax.string_of_term ctxt pat))
berghofe@22779:         else x :: xs)
berghofe@22779:     | _ => I) pat [];
berghofe@22779: 
bulwahn@32671: fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses =
berghofe@22779:   let
wenzelm@35124:     fun string_of_clause (pat, rhs) =
wenzelm@35124:       Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
berghofe@22779:     val _ = map (no_repeat_vars ctxt o fst) clauses;
berghofe@22779:     val rows = map_index (fn (i, (pat, rhs)) =>
berghofe@22779:       (([], [pat]), (rhs, (i, true)))) clauses;
wenzelm@35124:     val rangeT =
wenzelm@35124:       (case distinct op = (map (type_of o snd) clauses) of
berghofe@22779:         [] => case_error "no clauses given"
berghofe@22779:       | [T] => T
berghofe@22779:       | _ => case_error "all cases must have the same result type");
berghofe@22779:     val used' = fold add_row_used rows used;
berghofe@22779:     val (patts, case_tm) = mk_case tab ctxt ty_match ty_inst type_of
berghofe@22779:         used' rangeT {path = [x], rows = rows}
berghofe@22779:       handle CASE_ERROR (msg, i) => case_error (msg ^
berghofe@22779:         (if i < 0 then ""
berghofe@22779:          else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
berghofe@22779:     val patts1 = map
berghofe@22779:       (fn (_, tag, [pat]) => (pat, tag)
berghofe@22779:         | _ => case_error "error in pattern-match translation") patts;
wenzelm@35124:     val patts2 = Library.sort (int_ord o pairself row_of_pat) patts1
berghofe@22779:     val finals = map row_of_pat patts2
berghofe@22779:     val originals = map (row_of_pat o #2) rows
wenzelm@35124:     val _ =
wenzelm@42049:       (case subtract (op =) finals originals of
wenzelm@42049:         [] => ()
wenzelm@42049:       | is =>
wenzelm@42049:           (case config of Error => case_error | Warning => warning | Quiet => fn _ => {})
wenzelm@42049:             ("The following clauses are redundant (covered by preceding clauses):\n" ^
wenzelm@42049:              cat_lines (map (string_of_clause o nth clauses) is)));
berghofe@22779:   in
berghofe@22779:     (case_tm, patts2)
berghofe@22779:   end;
berghofe@22779: 
berghofe@22779: fun make_case tab ctxt = gen_make_case
wenzelm@32035:   (match_type (ProofContext.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt;
berghofe@22779: val make_case_untyped = gen_make_case (K (K Vartab.empty))
berghofe@22779:   (K (Term.map_types (K dummyT))) (K dummyT);
berghofe@22779: 
berghofe@22779: 
berghofe@22779: (* parse translation *)
berghofe@22779: 
nipkow@24349: fun case_tr err tab_of ctxt [t, u] =
wenzelm@42049:       let
wenzelm@42049:         val thy = ProofContext.theory_of ctxt;
wenzelm@42359:         val intern_const_syntax = Consts.intern_syntax (ProofContext.consts_of ctxt);
wenzelm@35256: 
wenzelm@42049:         (* replace occurrences of dummy_pattern by distinct variables *)
wenzelm@42049:         (* internalize constant names                                 *)
wenzelm@42049:         fun prep_pat ((c as Const (@{syntax_const "_constrain"}, _)) $ t $ tT) used =
wenzelm@42049:               let val (t', used') = prep_pat t used
wenzelm@42049:               in (c $ t' $ tT, used') end
wenzelm@42049:           | prep_pat (Const (@{const_syntax dummy_pattern}, T)) used =
wenzelm@42049:               let val x = Name.variant used "x"
wenzelm@42049:               in (Free (x, T), x :: used) end
wenzelm@42049:           | prep_pat (Const (s, T)) used =
wenzelm@42049:               (Const (intern_const_syntax s, T), used)
wenzelm@42049:           | prep_pat (v as Free (s, T)) used =
wenzelm@42359:               let val s' = ProofContext.intern_const ctxt s in
wenzelm@42049:                 if Sign.declared_const thy s' then
wenzelm@42049:                   (Const (s', T), used)
wenzelm@42049:                 else (v, used)
wenzelm@42049:               end
wenzelm@42049:           | prep_pat (t $ u) used =
wenzelm@42049:               let
wenzelm@42049:                 val (t', used') = prep_pat t used;
wenzelm@42359:                 val (u', used'') = prep_pat u used';
wenzelm@42049:               in
wenzelm@42049:                 (t' $ u', used'')
wenzelm@42049:               end
wenzelm@42049:           | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
wenzelm@42049:         fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
wenzelm@42049:               let val (l', cnstrts) = strip_constraints l
wenzelm@42049:               in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts) end
wenzelm@42049:           | dest_case1 t = case_error "dest_case1";
wenzelm@42049:         fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
wenzelm@42049:           | dest_case2 t = [t];
wenzelm@42057:         val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
wenzelm@42049:         val (case_tm, _) = make_case_untyped (tab_of thy) ctxt
wenzelm@42049:           (if err then Error else Warning) []
wenzelm@42049:           (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
wenzelm@42049:              (flat cnstrts) t) cases;
wenzelm@42049:       in case_tm end
nipkow@24349:   | case_tr _ _ _ ts = case_error "case_tr";
berghofe@22779: 
berghofe@22779: 
berghofe@22779: (*---------------------------------------------------------------------------
berghofe@22779:  * Pretty printing of nested case expressions
berghofe@22779:  *---------------------------------------------------------------------------*)
berghofe@22779: 
berghofe@22779: (* destruct one level of pattern matching *)
berghofe@22779: 
berghofe@22779: fun gen_dest_case name_of type_of tab d used t =
wenzelm@42049:   (case apfst name_of (strip_comb t) of
berghofe@22779:     (SOME cname, ts as _ :: _) =>
berghofe@22779:       let
berghofe@22779:         val (fs, x) = split_last ts;
berghofe@22779:         fun strip_abs i t =
berghofe@22779:           let
berghofe@22779:             val zs = strip_abs_vars t;
berghofe@22779:             val _ = if length zs < i then raise CASE_ERROR ("", 0) else ();
berghofe@22779:             val (xs, ys) = chop i zs;
berghofe@22779:             val u = list_abs (ys, strip_abs_body t);
wenzelm@29270:             val xs' = map Free (Name.variant_list (OldTerm.add_term_names (u, used))
berghofe@22779:               (map fst xs) ~~ map snd xs)
berghofe@22779:           in (xs', subst_bounds (rev xs', u)) end;
berghofe@22779:         fun is_dependent i t =
berghofe@22779:           let val k = length (strip_abs_vars t) - i
wenzelm@42049:           in k < 0 orelse exists (fn j => j >= k) (loose_bnos (strip_abs_body t)) end;
berghofe@22779:         fun count_cases (_, _, true) = I
berghofe@22779:           | count_cases (c, (_, body), false) =
berghofe@22779:               AList.map_default op aconv (body, []) (cons c);
wenzelm@35392:         val is_undefined = name_of #> equal (SOME @{const_name undefined});
berghofe@22779:         fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body)
wenzelm@42049:       in
wenzelm@42049:         (case ty_info tab cname of
berghofe@22779:           SOME {constructors, case_name} =>
berghofe@22779:             if length fs = length constructors then
berghofe@22779:               let
berghofe@22779:                 val cases = map (fn (Const (s, U), t) =>
berghofe@22779:                   let
berghofe@22779:                     val k = length (binder_types U);
berghofe@22779:                     val p as (xs, _) = strip_abs k t
berghofe@22779:                   in
berghofe@22779:                     (Const (s, map type_of xs ---> type_of x),
berghofe@22779:                      p, is_dependent k t)
berghofe@22779:                   end) (constructors ~~ fs);
berghofe@22779:                 val cases' = sort (int_ord o swap o pairself (length o snd))
berghofe@22779:                   (fold_rev count_cases cases []);
berghofe@22779:                 val R = type_of t;
wenzelm@35124:                 val dummy =
wenzelm@35392:                   if d then Const (@{const_name dummy_pattern}, R)
wenzelm@42049:                   else Free (Name.variant used "x", R);
berghofe@22779:               in
wenzelm@42049:                 SOME (x,
wenzelm@42049:                   map mk_case
wenzelm@42049:                     (case find_first (is_undefined o fst) cases' of
wenzelm@42049:                       SOME (_, cs) =>
wenzelm@42049:                       if length cs = length constructors then [hd cases]
wenzelm@42049:                       else filter_out (fn (_, (_, body), _) => is_undefined body) cases
wenzelm@42049:                     | NONE => case cases' of
wenzelm@42049:                       [] => cases
wenzelm@42049:                     | (default, cs) :: _ =>
wenzelm@42049:                       if length cs = 1 then cases
wenzelm@42049:                       else if length cs = length constructors then
wenzelm@42049:                         [hd cases, (dummy, ([], default), false)]
wenzelm@42049:                       else
wenzelm@42049:                         filter_out (fn (c, _, _) => member op aconv cs c) cases @
wenzelm@42049:                         [(dummy, ([], default), false)]))
berghofe@22779:               end handle CASE_ERROR _ => NONE
berghofe@22779:             else NONE
wenzelm@42049:         | _ => NONE)
berghofe@22779:       end
wenzelm@42049:   | _ => NONE);
berghofe@22779: 
berghofe@22779: val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
wenzelm@42290: val dest_case' = gen_dest_case (try (dest_Const #> fst #> Lexicon.unmark_const)) (K dummyT);
berghofe@22779: 
berghofe@22779: 
berghofe@22779: (* destruct nested patterns *)
berghofe@22779: 
haftmann@29623: fun strip_case'' dest (pat, rhs) =
wenzelm@42049:   (case dest (Term.add_free_names pat []) rhs of
berghofe@22779:     SOME (exp as Free _, clauses) =>
wenzelm@29266:       if member op aconv (OldTerm.term_frees pat) exp andalso
berghofe@22779:         not (exists (fn (_, rhs') =>
wenzelm@29266:           member op aconv (OldTerm.term_frees rhs') exp) clauses)
berghofe@22779:       then
haftmann@29623:         maps (strip_case'' dest) (map (fn (pat', rhs') =>
berghofe@22779:           (subst_free [(exp, pat')] pat, rhs')) clauses)
berghofe@22779:       else [(pat, rhs)]
wenzelm@42049:   | _ => [(pat, rhs)]);
berghofe@22779: 
wenzelm@35124: fun gen_strip_case dest t =
wenzelm@42049:   (case dest [] t of
berghofe@22779:     SOME (x, clauses) =>
haftmann@29623:       SOME (x, maps (strip_case'' dest) clauses)
wenzelm@42049:   | NONE => NONE);
berghofe@22779: 
berghofe@22779: val strip_case = gen_strip_case oo dest_case;
berghofe@22779: val strip_case' = gen_strip_case oo dest_case';
berghofe@22779: 
berghofe@22779: 
berghofe@22779: (* print translation *)
berghofe@22779: 
berghofe@22779: fun case_tr' tab_of cname ctxt ts =
berghofe@22779:   let
berghofe@22779:     val thy = ProofContext.theory_of ctxt;
berghofe@22779:     fun mk_clause (pat, rhs) =
wenzelm@42049:       let val xs = Term.add_frees pat [] in
wenzelm@35124:         Syntax.const @{syntax_const "_case1"} $
berghofe@22779:           map_aterms
wenzelm@42284:             (fn Free p => Syntax_Trans.mark_boundT p
wenzelm@42290:               | Const (s, _) => Syntax.const (Lexicon.mark_const s)
berghofe@22779:               | t => t) pat $
berghofe@22779:           map_aterms
wenzelm@29266:             (fn x as Free (s, T) =>
wenzelm@42284:                   if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
berghofe@22779:               | t => t) rhs
wenzelm@42049:       end;
wenzelm@35124:   in
wenzelm@42049:     (case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
wenzelm@35124:       SOME (x, clauses) =>
wenzelm@35124:         Syntax.const @{syntax_const "_case_syntax"} $ x $
wenzelm@35124:           foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
wenzelm@35124:             (map mk_clause clauses)
wenzelm@42049:     | NONE => raise Match)
berghofe@22779:   end;
berghofe@22779: 
berghofe@22779: end;