# HG changeset patch
# User haftmann
# Date 1648139683 0
# Node ID 96da582011ae699f46589563b8b1adeed3f58c37
# Parent  21897aad78ad15c9f2653cc6f15b67d9ac7b2b6e
separated case reduction

diff -r 21897aad78ad -r 96da582011ae src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Mar 24 16:34:42 2022 +0000
+++ b/src/Tools/Code/code_thingol.ML	Thu Mar 24 16:34:43 2022 +0000
@@ -279,6 +279,35 @@
         clauses = (map o apply2) (map_terms_bottom_up f) clauses,
         primitive = map_terms_bottom_up f t0 });
 
+fun adjungate_clause ctxt vs_map ts (body as IConst { sym = Constant c, ... }) =
+      if Code.is_undefined (Proof_Context.theory_of ctxt) c
+      then []
+      else [(ts, body)]
+  | adjungate_clause ctxt vs_map ts (body as ICase { term = IVar (SOME v), clauses = clauses, ... }) =
+      let
+        val vs = (fold o fold_varnames) (insert (op =)) ts [];
+        fun varnames_disjunctive pat =
+          null (inter (op =) vs (fold_varnames (insert (op =)) pat []));
+        fun purge_unused_vars_in t =
+          let
+            val vs = fold_varnames (insert (op =)) t [];
+          in
+            map_terms_bottom_up (fn IVar (SOME v) =>
+              IVar (if member (op =) vs v then SOME v else NONE) | t => t)
+          end;
+      in
+        if forall (fn (pat', body') => exists_var pat' v
+          orelse not (exists_var body' v)) clauses
+          andalso forall (varnames_disjunctive o fst) clauses
+        then case AList.lookup (op =) vs_map v
+         of SOME i => maps (fn (pat', body') =>
+              adjungate_clause ctxt (AList.delete (op =) v vs_map)
+                (nth_map i (K pat') ts |> map (purge_unused_vars_in body')) body') clauses
+          | NONE => [(ts, body)]
+        else [(ts, body)]
+      end
+  | adjungate_clause ctxt vs_map ts body = [(ts, body)];
+
 fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d
 and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f dss
   | exists_plain_dict_var_pred f (Dict_Var x) = f x
@@ -701,40 +730,12 @@
 and translate_case ctxt algbr eqngr permissive some_thm (t_pos, case_pats) (c_ty, ts) =
   let
     val (ty, constrs, split_clauses) = preprocess_pattern_schema ctxt (t_pos, case_pats) (c_ty, ts);
-    val thy = Proof_Context.theory_of ctxt;
-    fun disjunctive_varnames ts =
-      let
-        val vs = (fold o fold_varnames) (insert (op =)) ts [];
-      in fn pat => null (inter (op =) vs (fold_varnames (insert (op =)) pat [])) end;
-    fun purge_unused_vars_in t =
-      let
-        val vs = fold_varnames (insert (op =)) t [];
-      in
-        map_terms_bottom_up (fn IVar (SOME v) =>
-          IVar (if member (op =) vs v then SOME v else NONE) | t => t)
-      end;
-    fun collapse_clause vs_map ts body =
-      case body
-       of IConst { sym = Constant c, ... } => if Code.is_undefined thy c
-            then []
-            else [(ts, body)]
-        | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
-            if forall (fn (pat', body') => exists_var pat' v
-              orelse not (exists_var body' v)) clauses
-              andalso forall (disjunctive_varnames ts o fst) clauses
-            then case AList.lookup (op =) vs_map v
-             of SOME i => maps (fn (pat', body') =>
-                  collapse_clause (AList.delete (op =) v vs_map)
-                    (nth_map i (K pat') ts |> map (purge_unused_vars_in body')) body') clauses
-              | NONE => [(ts, body)]
-            else [(ts, body)]
-        | _ => [(ts, body)];
     fun mk_clause tys t =
       let
         val (vs, body) = unfold_abs_eta tys t;
         val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs [];
         val ts = map (IVar o fst) vs;
-      in collapse_clause vs_map ts body end;
+      in adjungate_clause ctxt vs_map ts body end;
     fun casify constrs ty t_app ts =
       let
         val (t, ts_clause) = split_clauses ts;
@@ -750,8 +751,7 @@
       #>> rpair n) constrs
     ##>> translate_typ ctxt algbr eqngr permissive ty
     ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
-    #>> (fn (((t, constrs), ty), ts) =>
-      casify constrs ty t ts)
+    #>> (fn (((t_app, constrs), ty), ts) => casify constrs ty t_app ts)
   end
 and translate_app_case ctxt algbr eqngr permissive some_thm (num_args, pattern_schema) ((c, ty), ts) =
   if length ts < num_args then