src/HOL/Tools/Datatype/datatype_case.ML

 
 exception CASE_ERROR of string * int;
 
 fun match_type thy pat ob = Sign.typ_match thy (pat, ob) Vartab.empty;
 
-(*---------------------------------------------------------------------------
- * Get information about datatypes
- *---------------------------------------------------------------------------*)
+(* Get information about datatypes *)
 
 fun ty_info tab sT =
   (case tab sT of
     SOME ({descr, case_name, index, sorts, ...} : info) =>
       let

             Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs}
       end
   | NONE => NONE);
 
 
-(*---------------------------------------------------------------------------
- * Each pattern carries with it a tag i, which denotes
- * the clause it came from. i = ~1 indicates that
- * the clause was added by pattern completion.
- *---------------------------------------------------------------------------*)
-
-fun pattern_subst theta (tm, x) = (subst_free theta tm, x);
+(*Each pattern carries with it a tag i, which denotes the clause it
+came from. i = ~1 indicates that the clause was added by pattern
+completion.*)
 
 fun add_row_used ((prfx, pats), (tm, tag)) =
   fold Term.add_free_names (tm :: pats @ map Free prfx);
 
-(* try to preserve names given by user *)
+(*try to preserve names given by user*)
 fun default_names names ts =
   map (fn ("", Free (name', _)) => name' | (name, _) => name) (names ~~ ts);
 
 fun strip_constraints (Const (@{syntax_const "_constrain"}, _) $ t $ tT) =
       strip_constraints t ||> cons tT

 fun mk_fun_constrain tT t =
   Syntax.const @{syntax_const "_constrain"} $ t $
     (Syntax.const @{type_syntax fun} $ tT $ Syntax.const @{type_syntax dummy});
 
 
-(*---------------------------------------------------------------------------
- * Produce an instance of a constructor, plus genvars for its arguments.
- *---------------------------------------------------------------------------*)
+(*Produce an instance of a constructor, plus fresh variables for its arguments.*)
 fun fresh_constr ty_match ty_inst colty used c =
   let
     val (_, Ty) = dest_Const c
     val Ts = binder_types Ty;
     val names = Name.variant_list used

     val c' = ty_inst ty_theta c
     val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts)
   in (c', gvars) end;
 
 
-(*---------------------------------------------------------------------------
- * Goes through a list of rows and picks out the ones beginning with a
- * pattern with constructor = name.
- *---------------------------------------------------------------------------*)
+(*Goes through a list of rows and picks out the ones beginning with a
+ pattern with constructor = name.*)
 fun mk_group (name, T) rows =
   let val k = length (binder_types T) in
     fold (fn (row as ((prfx, p :: rst), rhs as (_, i))) =>
       fn ((in_group, not_in_group), (names, cnstrts)) =>
         (case strip_comb p of

             else ((in_group, row :: not_in_group), (names, cnstrts))
         | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
     rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
   end;
 
-(*---------------------------------------------------------------------------
- * Partition the rows. Not efficient: we should use hashing.
- *---------------------------------------------------------------------------*)
+
+(* Partitioning *)
+
 fun partition _ _ _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
   | partition ty_match ty_inst type_of used constructors colty res_ty
         (rows as (((prfx, _ :: rstp), _) :: _)) =
       let
         fun part {constrs = [], rows = [], A} = rev A

                     constraints = cnstrts,
                     group = in_group'} :: A}
               end
       in part {constrs = constructors, rows = rows, A = []} end;
 
-(*---------------------------------------------------------------------------
- * Misc. routines used in mk_case
- *---------------------------------------------------------------------------*)
-
 fun v_to_prfx (prfx, Free v::pats) = (v::prfx,pats)
   | v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
 
 
-(*----------------------------------------------------------------------------
- * Translation of pattern terms into nested case expressions.
- *
- * This performs the translation and also builds the full set of patterns.
- * Thus it supports the construction of induction theorems even when an
- * incomplete set of patterns is given.
- *---------------------------------------------------------------------------*)
-
+(* Translation of pattern terms into nested case expressions. *)
+ 
 fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
   let
     val name = Name.variant used "a";
     fun expand constructors used ty ((_, []), _) =
           raise CASE_ERROR ("mk_case: expand_var_row", ~1)
-      | expand constructors used ty (row as ((prfx, p :: rst), rhs)) =
+      | expand constructors used ty (row as ((prfx, p :: rst), (rhs, tag))) =
           if is_Free p then
             let
               val used' = add_row_used row used;
               fun expnd c =
                 let val capp =
                   list_comb (fresh_constr ty_match ty_inst ty used' c)
-                in ((prfx, capp :: rst), pattern_subst [(p, capp)] rhs)
+                in ((prfx, capp :: rst), (subst_free [(p, capp)] rhs, tag))
                 end
             in map expnd constructors end
           else [row]
     fun mk {rows = [], ...} = raise CASE_ERROR ("no rows", ~1)
       | mk {path = [], rows = ((prfx, []), (tm, tag)) :: _} =  (* Done *)

           let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
             (case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
               NONE =>
                 let
                   val rows' = map (fn ((v, _), row) => row ||>
-                    pattern_subst [(v, u)] |>> v_to_prfx) (col0 ~~ rows);
+                    apfst (subst_free [(v, u)]) |>> v_to_prfx) (col0 ~~ rows);
                 in mk {path = rstp, rows = rows'} end
             | SOME (Const (cname, cT), i) =>
                 (case ty_info tab (cname, cT) of
                   NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
                 | SOME {case_name, constructors} =>

       | mk _ = raise CASE_ERROR ("Malformed row matrix", ~1)
   in mk end;
 
 fun case_error s = error ("Error in case expression:\n" ^ s);
 
-(* Repeated variable occurrences in a pattern are not allowed. *)
+(*Repeated variable occurrences in a pattern are not allowed.*)
 fun no_repeat_vars ctxt pat = fold_aterms
   (fn x as Free (s, _) => (fn xs =>
         if member op aconv xs x then
           case_error (quote s ^ " occurs repeatedly in the pattern " ^
             quote (Syntax.string_of_term ctxt pat))

              (flat cnstrts) t) cases;
       in case_tm end
   | case_tr _ _ _ ts = case_error "case_tr";
 
 
-(*---------------------------------------------------------------------------
- * Pretty printing of nested case expressions
- *---------------------------------------------------------------------------*)
+(* Pretty printing of nested case expressions *)
 
 (* destruct one level of pattern matching *)
 
 fun gen_dest_case name_of type_of tab d used t =
   (case apfst name_of (strip_comb t) of