src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

 fun check_expected_modes (options : Predicate_Compile_Aux.options) modes =
   case expected_modes options of
     SOME (s, ms) => (case AList.lookup (op =) modes s of
       SOME modes =>
         if not (eq_set (map (map (rpair NONE)) ms, map snd modes)) then
-          error ("expected modes were not inferred:"
-            ^ "infered modes for " ^ s ^ ": " ^ commas (map (string_of_smode o snd) modes))
+          error ("expected modes were not inferred:\n"
+          ^ "inferred modes for " ^ s ^ ": "
+          ^ commas (map ((enclose "[" "]") o string_of_smode o snd) modes))
         else ()
       | NONE => ())
   | NONE => ()
 
 (* importing introduction rules *)

         val (t', nvs') = distinct_v t nvs;
         val (u', nvs'') = distinct_v u nvs';
       in (t' $ u', nvs'') end
   | distinct_v x nvs = (x, nvs);
 
-fun compile_match thy compfuns eqs eqs' out_ts success_t =
-  let
-    val eqs'' = maps mk_eq eqs @ eqs'
-    val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
-    val name = Name.variant names "x";
-    val name' = Name.variant (name :: names) "y";
-    val T = mk_tupleT (map fastype_of out_ts);
-    val U = fastype_of success_t;
-    val U' = dest_predT compfuns U;
-    val v = Free (name, T);
-    val v' = Free (name', T);
-  in
-    lambda v (fst (Datatype.make_case
-      (ProofContext.init thy) DatatypeCase.Quiet [] v
-      [(mk_tuple out_ts,
-        if null eqs'' then success_t
-        else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
-          foldr1 HOLogic.mk_conj eqs'' $ success_t $
-            mk_bot compfuns U'),
-       (v', mk_bot compfuns U')]))
-  end;
-
-(*FIXME function can be removed*)
-fun mk_funcomp f t =
-  let
-    val names = Term.add_free_names t [];
-    val Ts = binder_types (fastype_of t);
-    val vs = map Free
-      (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
-  in
-    fold_rev lambda vs (f (list_comb (t, vs)))
-  end;
-
-fun compile_param compilation_modifiers compfuns thy (NONE, t) = t
-  | compile_param compilation_modifiers compfuns thy (m as SOME (Mode (mode, _, ms)), t) =
-   let
-     val (f, args) = strip_comb (Envir.eta_contract t)
-     val (params, args') = chop (length ms) args
-     val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
-     val f' =
-       case f of
-         Const (name, T) => Const (#const_name_of compilation_modifiers thy name mode,
-           #funT_of compilation_modifiers compfuns mode T)
-       | Free (name, T) => Free (name, #funT_of compilation_modifiers compfuns mode T)
-       | _ => error ("PredicateCompiler: illegal parameter term")
-   in
-     list_comb (f', params' @ args')
-   end
-
-fun compile_expr compilation_modifiers compfuns thy ((Mode (mode, _, ms)), t) inargs additional_arguments =
-  case strip_comb t of
-    (Const (name, T), params) =>
-       let
-         val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
-           (*val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of*)
-         val name' = #const_name_of compilation_modifiers thy name mode
-         val T' = #funT_of compilation_modifiers compfuns mode T
-       in
-         (list_comb (Const (name', T'), params' @ inargs @ additional_arguments))
-       end
-  | (Free (name, T), params) =>
-    list_comb (Free (name, #funT_of compilation_modifiers compfuns mode T), params @ inargs @ additional_arguments)
-
 (** specific rpred functions -- move them to the correct place in this file *)
 
-fun mk_Eval_of depth ((x, T), NONE) names = (x, names)
-  | mk_Eval_of depth ((x, T), SOME mode) names =
+fun mk_Eval_of additional_arguments ((x, T), NONE) names = (x, names)
+  | mk_Eval_of additional_arguments ((x, T), SOME mode) names =
 	let
     val Ts = binder_types T
     (*val argnames = Name.variant_list names
         (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
     val args = map Free (argnames ~~ Ts)

 							fun tuple args = if null args then [] else [HOLogic.mk_tuple args]
 						in ((tuple inargs, tuple outargs), args) end
 			end
 		val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts))
     val (inargs, outargs) = pairself flat (split_list inoutargs)
-    val depth_t = case depth of NONE => [] | SOME (polarity, depth_t) => [polarity, depth_t]
-		val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs @ depth_t), mk_tuple outargs)
+		val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs @ additional_arguments), mk_tuple outargs)
     val t = fold_rev mk_split_lambda args r
   in
     (t, names)
   end;
 
-fun compile_arg depth thy param_vs iss arg = 
-  let
-    val funT_of = case depth of NONE => funT_of | SOME _ => depth_limited_funT_of
+fun compile_arg compilation_modifiers compfuns additional_arguments thy param_vs iss arg = 
+  let
     fun map_params (t as Free (f, T)) =
       if member (op =) param_vs f then
         case (the (AList.lookup (op =) (param_vs ~~ iss) f)) of
-          SOME is => let val T' = funT_of PredicateCompFuns.compfuns ([], is) T
-            in fst (mk_Eval_of depth ((Free (f, T'), T), SOME is) []) end
+          SOME is =>
+            let
+              val T' = #funT_of compilation_modifiers compfuns ([], is) T
+            in fst (mk_Eval_of additional_arguments ((Free (f, T'), T), SOME is) []) end
         | NONE => t
       else t
       | map_params t = t
     in map_aterms map_params arg end
-  
+
+fun compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy eqs eqs' out_ts success_t =
+  let
+    val eqs'' = maps mk_eq eqs @ eqs'
+    val eqs'' =
+      map (compile_arg compilation_modifiers compfuns additional_arguments thy param_vs iss) eqs''
+    val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
+    val name = Name.variant names "x";
+    val name' = Name.variant (name :: names) "y";
+    val T = mk_tupleT (map fastype_of out_ts);
+    val U = fastype_of success_t;
+    val U' = dest_predT compfuns U;
+    val v = Free (name, T);
+    val v' = Free (name', T);
+  in
+    lambda v (fst (Datatype.make_case
+      (ProofContext.init thy) DatatypeCase.Quiet [] v
+      [(mk_tuple out_ts,
+        if null eqs'' then success_t
+        else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
+          foldr1 HOLogic.mk_conj eqs'' $ success_t $
+            mk_bot compfuns U'),
+       (v', mk_bot compfuns U')]))
+  end;
+
+(*FIXME function can be removed*)
+fun mk_funcomp f t =
+  let
+    val names = Term.add_free_names t [];
+    val Ts = binder_types (fastype_of t);
+    val vs = map Free
+      (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
+  in
+    fold_rev lambda vs (f (list_comb (t, vs)))
+  end;
+
+fun compile_param compilation_modifiers compfuns thy (NONE, t) = t
+  | compile_param compilation_modifiers compfuns thy (m as SOME (Mode (mode, _, ms)), t) =
+   let
+     val (f, args) = strip_comb (Envir.eta_contract t)
+     val (params, args') = chop (length ms) args
+     val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
+     val f' =
+       case f of
+         Const (name, T) => Const (#const_name_of compilation_modifiers thy name mode,
+           #funT_of compilation_modifiers compfuns mode T)
+       | Free (name, T) => Free (name, #funT_of compilation_modifiers compfuns mode T)
+       | _ => error ("PredicateCompiler: illegal parameter term")
+   in
+     list_comb (f', params' @ args')
+   end
+
+fun compile_expr compilation_modifiers compfuns thy ((Mode (mode, _, ms)), t) inargs additional_arguments =
+  case strip_comb t of
+    (Const (name, T), params) =>
+       let
+         val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
+           (*val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of*)
+         val name' = #const_name_of compilation_modifiers thy name mode
+         val T' = #funT_of compilation_modifiers compfuns mode T
+       in
+         (list_comb (Const (name', T'), params' @ inargs @ additional_arguments))
+       end
+  | (Free (name, T), params) =>
+    list_comb (Free (name, #funT_of compilation_modifiers compfuns mode T), params @ inargs @ additional_arguments)
+
 fun compile_clause compilation_modifiers compfuns thy all_vs param_vs additional_arguments (iss, is) inp (ts, moded_ps) =
   let
+    val compile_match = compile_match compilation_modifiers compfuns additional_arguments param_vs iss thy
     fun check_constrt t (names, eqs) =
       if is_constrt thy t then (t, (names, eqs)) else
         let
           val s = Name.variant names "x"
           val v = Free (s, fastype_of t)

             val (out_ts'', (names', eqs')) =
               fold_map check_constrt out_ts' (names, []);
             val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
               out_ts'' (names', map (rpair []) vs);
           in
-            compile_match thy compfuns constr_vs (eqs @ eqs') out_ts'''
+            compile_match constr_vs (eqs @ eqs') out_ts'''
               (mk_single compfuns (mk_tuple out_ts))
           end
       | compile_prems out_ts vs names ((p, mode as Mode ((_, is), _, _)) :: ps) =
           let
             val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));

               #transform_additional_arguments compilation_modifiers p additional_arguments
             val (compiled_clause, rest) = case p of
                Prem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_smode is us;
-                     (* TODO: add test case for compile_arg *)
-                   (*val in_ts = map (compile_arg depth thy param_vs iss) in_ts*)
-                     (* additional_arguments
-                   val args = case depth of
-                     NONE => in_ts
-                   | SOME (polarity, depth_t) => in_ts @ [polarity, depth_t]
-                   *)
+                   val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments
+                     thy param_vs iss) in_ts
                    val u =
                      compile_expr compilation_modifiers compfuns thy (mode, t) in_ts additional_arguments'
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
                  end
              | Negprem (us, t) =>
                  let
                    val (in_ts, out_ts''') = split_smode is us
-                     (* additional_arguments
-                   val args = case depth of
-                     NONE => in_ts
-                   | SOME (polarity, depth_t) => in_ts @ [HOLogic.mk_not polarity, depth_t]
-                   *)
+                   val in_ts = map (compile_arg compilation_modifiers compfuns additional_arguments
+                     thy param_vs iss) in_ts
                    val u = mk_not compfuns
                      (compile_expr compilation_modifiers compfuns thy (mode, t) in_ts additional_arguments')
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
                  end
              | Sidecond t =>
                  let
+                   val t = compile_arg compilation_modifiers compfuns additional_arguments
+                     thy param_vs iss t
                    val rest = compile_prems [] vs' names'' ps;
                  in
                    (mk_if compfuns t, rest)
                  end
              | Generator (v, T) =>

                    val rest = compile_prems [Free (v, T)]  vs' names'' ps;
                  in
                    (u, rest)
                  end
           in
-            compile_match thy compfuns constr_vs' eqs out_ts''
+            compile_match constr_vs' eqs out_ts''
               (mk_bind compfuns (compiled_clause, rest))
           end
     val prem_t = compile_prems in_ts' param_vs all_vs' moded_ps;
   in
     mk_bind compfuns (mk_single compfuns inp, prem_t)

 	val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) []
   val (inargs, outargs) = split_smode is args
   val param_names' = Name.variant_list (param_names @ argnames)
     (map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
   val param_vs = map Free (param_names' ~~ Ts1)
-  val (params', names) = fold_map (mk_Eval_of NONE) ((params ~~ Ts1) ~~ iss) []
+  val (params', names) = fold_map (mk_Eval_of []) ((params ~~ Ts1) ~~ iss) []
   val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ args))
   val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ args))
   val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
   val funargs = params @ inargs
   val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),

 						 in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
 						 end
    	  val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
       val (xinout, xargs) = split_list xinoutargs
 			val (xins, xouts) = pairself flat (split_list xinout)
-			val (xparams', names') = fold_map (mk_Eval_of NONE) ((xparams ~~ Ts1) ~~ iss) names
+			val (xparams', names') = fold_map (mk_Eval_of []) ((xparams ~~ Ts1) ~~ iss) names
       fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
         | mk_split_lambda [x] t = lambda x t
         | mk_split_lambda xs t =
         let
           fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))