generalise case certificates to allow ignored parameters

--- a/src/Pure/Isar/code.ML	Thu Apr 12 07:33:14 2012 +0200
+++ b/src/Pure/Isar/code.ML	Thu Apr 12 10:29:45 2012 +0200
@@ -66,7 +66,7 @@
   val is_constr: theory -> string -> bool
   val is_abstr: theory -> string -> bool
   val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
-  val get_case_scheme: theory -> string -> (int * (int * string list)) option
+  val get_case_scheme: theory -> string -> (int * (int * string option list)) option
   val get_case_cong: theory -> string -> thm option
   val undefineds: theory -> string list
   val print_codesetup: theory -> unit
@@ -180,7 +180,7 @@
     (*with explicit history*),
   types: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
     (*with explicit history*),
-  cases: ((int * (int * string list)) * thm) Symtab.table * unit Symtab.table
+  cases: ((int * (int * string option list)) * thm) Symtab.table * unit Symtab.table
 };
 
 fun make_spec (history_concluded, (functions, (types, cases))) =
@@ -895,7 +895,7 @@
     fun analyze_cases cases =
       let
         val co_list = fold (AList.update (op =) o dest_case) cases [];
-      in map (the o AList.lookup (op =) co_list) params end;
+      in map (AList.lookup (op =) co_list) params end;
     fun analyze_let t =
       let
         val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t;
@@ -948,10 +948,12 @@
                       :: Pretty.str "of"
                       :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
       );
+    fun ignored_cases NONE = "<ignored>"
+      | ignored_cases (SOME c) = string_of_const thy c
     fun pretty_case (const, ((_, (_, [])), _)) = Pretty.str (string_of_const thy const)
       | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
           Pretty.str (string_of_const thy const), Pretty.str "with",
-          (Pretty.block o Pretty.commas o map (Pretty.str o string_of_const thy)) cos];
+          (Pretty.block o Pretty.commas o map (Pretty.str o ignored_cases)) cos];
     val functions = the_functions exec
       |> Symtab.dest
       |> (map o apsnd) (snd o fst)
@@ -1087,7 +1089,7 @@
 fun add_case thm thy =
   let
     val (case_const, (k, cos)) = case_cert thm;
-    val _ = case filter_out (is_constr thy) cos
+    val _ = case map_filter I cos |> filter_out (is_constr thy)
      of [] => ()
       | cs => error ("Non-constructor(s) in case certificate: " ^ commas_quote cs);
     val entry = (1 + Int.max (1, length cos), (k, cos));
@@ -1095,7 +1097,7 @@
       (Symtab.update (case_const, (entry, cong)));
     fun register_for_constructors (Constructors (cos', cases)) =
          Constructors (cos',
-           if exists (fn (co, _) => member (op =) cos co) cos'
+           if exists (fn (co, _) => member (op =) cos (SOME co)) cos'
            then insert (op =) case_const cases
            else cases)
       | register_for_constructors (x as Abstractor _) = x;
@@ -1131,7 +1133,7 @@
             ((the_functions o the_exec) thy) [old_proj];
     fun drop_outdated_cases cases = fold Symtab.delete_safe
       (Symtab.fold (fn (c, ((_, (_, cos)), _)) =>
-        if exists (member (op =) old_constrs) cos
+        if exists (member (op =) old_constrs) (map_filter I cos)
           then insert (op =) c else I) cases []) cases;
   in
     thy

--- a/src/Tools/Code/code_thingol.ML	Thu Apr 12 07:33:14 2012 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Apr 12 10:29:45 2012 +0200
@@ -781,10 +781,14 @@
     fun arg_types num_args ty = fst (chop num_args (binder_types ty));
     val tys = arg_types num_args (snd c_ty);
     val ty = nth tys t_pos;
-    fun mk_constr c t = let val n = Code.args_number thy c
-      in ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
+    fun mk_constr NONE t = NONE
+      | mk_constr (SOME c) t = let val n = Code.args_number thy c
+        in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
+
     val constrs = if null case_pats then []
       else map2 mk_constr case_pats (nth_drop t_pos ts);
+    val constrs' = map_filter I constrs
+
     fun casify naming constrs ty ts =
       let
         val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
@@ -817,12 +821,12 @@
           then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
           else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
             mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
-              (constrs ~~ ts_clause);
+              (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t) (case_pats ~~ ts_clause)));
       in ((t, ty), clauses) end;
   in
     translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
     ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
-      #>> rpair n) constrs
+      #>> rpair n) constrs'
     ##>> translate_typ thy algbr eqngr permissive ty
     ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
     #-> (fn (((t, constrs), ty), ts) =>