# HG changeset patch
# User bulwahn
# Date 1257491518 -3600
# Node ID 0df4f6e46e5e789264eb3d9397e006e388cd0674
# Parent  e96a0c52d74bfb9435de456c4164adde14abb585
made definition of functions generically for the different instances

diff -r e96a0c52d74b -r 0df4f6e46e5e src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -871,6 +871,15 @@
 
 (* function types and names of different compilations *)
 
+fun funT_of compfuns (iss, is) T =
+  let
+    val Ts = binder_types T
+    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
+    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
+  in
+    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
+  end;
+
 fun depth_limited_funT_of compfuns (iss, is) T =
   let
     val Ts = binder_types T
@@ -882,26 +891,15 @@
       ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
   end;
 
-fun funT_of compfuns (iss, is) T =
+fun random_function_funT_of (iss, is) T =
   let
     val Ts = binder_types T
     val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
-    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
+    val paramTs' = map2 (fn SOME is => random_function_funT_of ([], is) | NONE => I) iss paramTs
   in
-    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
-  end;
-
-fun mk_fun_of compfuns thy (name, T) mode = 
-  Const (predfun_name_of thy name mode, funT_of compfuns mode T)
-
-fun mk_annotated_fun_of compfuns thy (name, T) mode =
-  Const (annotated_function_name_of thy name mode, funT_of compfuns mode T)
-
-fun mk_depth_limited_fun_of compfuns thy (name, T) mode =
-  Const (depth_limited_function_name_of thy name mode, depth_limited_funT_of compfuns mode T)
-  
-fun mk_random_fun_of compfuns thy (name, T) mode = 
-  Const (random_function_name_of thy name mode, depth_limited_funT_of compfuns mode T)
+    (paramTs' @ inargTs @ [@{typ code_numeral}]) --->
+      (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
+  end
 
 (* Mode analysis *)
 
@@ -1227,7 +1225,9 @@
 
 datatype comp_modifiers = Comp_Modifiers of
 {
-  const_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string,
+  function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string,
+  set_function_name : string -> Predicate_Compile_Aux.mode -> string -> theory -> theory,
+  function_name_prefix : string,
   funT_of : compilation_funs -> mode -> typ -> typ,
   additional_arguments : string list -> term list,
   wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
@@ -1236,7 +1236,9 @@
 
 fun dest_comp_modifiers (Comp_Modifiers c) = c
 
-val const_name_of = #const_name_of o dest_comp_modifiers
+val function_name_of = #function_name_of o dest_comp_modifiers
+val set_function_name = #set_function_name o dest_comp_modifiers
+val function_name_prefix = #function_name_prefix o dest_comp_modifiers
 val funT_of = #funT_of o dest_comp_modifiers
 val additional_arguments = #additional_arguments o dest_comp_modifiers
 val wrap_compilation = #wrap_compilation o dest_comp_modifiers
@@ -1302,7 +1304,7 @@
      val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params)
      val f' =
        case f of
-         Const (name, T) => Const (Comp_Mod.const_name_of compilation_modifiers thy name mode,
+         Const (name, T) => Const (Comp_Mod.function_name_of compilation_modifiers thy name mode,
            Comp_Mod.funT_of compilation_modifiers compfuns mode T)
        | Free (name, T) => Free (name, Comp_Mod.funT_of compilation_modifiers compfuns mode T)
        | _ => error ("PredicateCompiler: illegal parameter term")
@@ -1316,8 +1318,7 @@
     (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' = Comp_Mod.const_name_of compilation_modifiers thy name mode
+         val name' = Comp_Mod.function_name_of compilation_modifiers thy name mode
          val T' = Comp_Mod.funT_of compilation_modifiers compfuns mode T
        in
          (list_comb (Const (name', T'), params' @ inargs @ additional_arguments))
@@ -1443,7 +1444,7 @@
         mk_bot compfuns (HOLogic.mk_tupleT Us2)
       else foldr1 (mk_sup compfuns) cl_ts)
     val fun_const =
-      Const (Comp_Mod.const_name_of compilation_modifiers thy s mode,
+      Const (Comp_Mod.function_name_of compilation_modifiers thy s mode,
         Comp_Mod.funT_of compilation_modifiers compfuns mode T)
   in
     HOLogic.mk_Trueprop
@@ -1634,62 +1635,22 @@
     fold create_definition modes thy
   end;
 
-fun create_definitions_of_depth_limited_functions preds (name, modes) thy =
+fun define_functions comp_modifiers compfuns preds (name, modes) thy =
   let
     val T = AList.lookup (op =) preds name |> the
     fun create_definition mode thy =
       let
-        val mode_cname = create_constname_of_mode thy "depth_limited_" name mode
-        val funT = depth_limited_funT_of PredicateCompFuns.compfuns mode T
+        val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers
+        val mode_cname = create_constname_of_mode thy function_name_prefix name mode
+        val funT = Comp_Mod.funT_of comp_modifiers compfuns mode T
       in
         thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
-        |> set_depth_limited_function_name name mode mode_cname 
+        |> Comp_Mod.set_function_name comp_modifiers name mode mode_cname
       end;
   in
     fold create_definition modes thy
   end;
 
-fun random_function_funT_of (iss, is) T =
-  let
-    val Ts = binder_types T
-    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
-    val paramTs' = map2 (fn SOME is => random_function_funT_of ([], is) | NONE => I) iss paramTs
-  in
-    (paramTs' @ inargTs @ [@{typ code_numeral}]) --->
-      (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
-  end
-
-fun random_create_definitions preds (name, modes) thy =
-  let
-    val T = AList.lookup (op =) preds name |> the
-    fun create_definition mode thy =
-      let
-        val mode_cname = create_constname_of_mode thy "gen_" name mode
-        val funT = random_function_funT_of mode T
-      in
-        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
-        |> set_random_function_name name mode mode_cname
-      end;
-  in
-    fold create_definition modes thy
-  end;
-
-fun create_definitions_of_annotated_functions preds (name, modes) thy =
-  let
-    val T = AList.lookup (op =) preds name |> the
-    fun create_definition mode thy =
-      let
-        val mode_cname = create_constname_of_mode thy "annotated_" name mode
-        val funT = funT_of PredicateCompFuns.compfuns mode T
-      in
-        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
-        |> set_annotated_function_name name mode mode_cname 
-      end;
-  in
-    fold create_definition modes thy
-  end;
-
-
 (* Proving equivalence of term *)
 
 fun is_Type (Type _) = true
@@ -2277,7 +2238,7 @@
   {
   compile_preds : theory -> string list -> string list -> (string * typ) list
     -> (moded_clause list) pred_mode_table -> term pred_mode_table,
-  create_definitions: (string * typ) list -> string * mode list -> theory -> theory,
+  define_functions : (string * typ) list -> string * mode list -> theory -> theory,
   infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list
     -> string list -> (string * (term list * indprem list) list) list
     -> moded_clause list pred_mode_table,
@@ -2308,7 +2269,7 @@
     val _ = print_modes options modes
       (*val _ = print_moded_clauses thy moded_clauses*)
     val _ = print_step options "Defining executable functions..."
-    val thy' = fold (#create_definitions (dest_steps steps) preds) modes thy
+    val thy' = fold (#define_functions (dest_steps steps) preds) modes thy
       |> Theory.checkpoint
     val _ = print_step options "Compiling equations..."
     val compiled_terms =
@@ -2364,7 +2325,9 @@
 (* different instantiantions of the predicate compiler *)
 
 val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {const_name_of = predfun_name_of : (theory -> string -> mode -> string),
+  {function_name_of = predfun_name_of : (theory -> string -> mode -> string),
+  set_function_name = (fn _ => fn _ => fn _ => I),
+  function_name_prefix = "",
   funT_of = funT_of : (compilation_funs -> mode -> typ -> typ),
   additional_arguments = K [],
   wrap_compilation = K (K (K (K (K I))))
@@ -2373,8 +2336,10 @@
   }
 
 val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {const_name_of = depth_limited_function_name_of,
+  {function_name_of = depth_limited_function_name_of,
+  set_function_name = set_depth_limited_function_name,
   funT_of = depth_limited_funT_of : (compilation_funs -> mode -> typ -> typ),
+  function_name_prefix = "depth_limited_",
   additional_arguments = fn names =>
     let
       val [depth_name, polarity_name] = Name.variant_list names ["depth", "polarity"]
@@ -2407,7 +2372,9 @@
   }
 
 val random_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {const_name_of = random_function_name_of,
+  {function_name_of = random_function_name_of,
+  set_function_name = set_random_function_name,
+  function_name_prefix = "random",
   funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ),
   additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})],
   wrap_compilation = K (K (K (K (K I))))
@@ -2416,7 +2383,9 @@
   }
 
 val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
-  {const_name_of = annotated_function_name_of,
+  {function_name_of = annotated_function_name_of,
+  set_function_name = set_annotated_function_name,
+  function_name_prefix = "annotated",
   funT_of = funT_of : (compilation_funs -> mode -> typ -> typ),
   additional_arguments = K [],
   wrap_compilation =
@@ -2427,7 +2396,7 @@
 
 val add_equations = gen_add_equations
   (Steps {infer_modes = infer_modes,
-  create_definitions = create_definitions,
+  define_functions = create_definitions,
   compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns,
   prove = prove,
   add_code_equations = add_code_equations,
@@ -2436,7 +2405,7 @@
 
 val add_depth_limited_equations = gen_add_equations
   (Steps {infer_modes = infer_modes,
-  create_definitions = create_definitions_of_depth_limited_functions,
+  define_functions = define_functions depth_limited_comp_modifiers PredicateCompFuns.compfuns,
   compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns,
   prove = prove_by_skip,
   add_code_equations = K (K (K I)),
@@ -2445,7 +2414,7 @@
 
 val add_annotated_equations = gen_add_equations
   (Steps {infer_modes = infer_modes,
-  create_definitions = create_definitions_of_annotated_functions,
+  define_functions = define_functions annotated_comp_modifiers PredicateCompFuns.compfuns,
   compile_preds = compile_preds annotated_comp_modifiers PredicateCompFuns.compfuns,
   prove = prove_by_skip,
   add_code_equations = K (K (K I)),
@@ -2454,7 +2423,7 @@
 
 val add_quickcheck_equations = gen_add_equations
   (Steps {infer_modes = infer_modes_with_generator,
-  create_definitions = random_create_definitions,
+  define_functions = define_functions random_comp_modifiers RandomPredCompFuns.compfuns,
   compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns,
   prove = prove_by_skip,
   add_code_equations = K (K (K I)),
@@ -2537,7 +2506,7 @@
   Unsynchronized.ref (NONE : (unit -> int * int -> term Predicate.pred * (int * int)) option);
 
 (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
-(* TODO: *)
+(* TODO: make analyze_compr generic with respect to the compilation modifiers*)
 fun analyze_compr thy compfuns param_user_modes (depth_limit, (random, annotated)) t_compr =
   let
     val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
@@ -2578,10 +2547,6 @@
           (if random then random_comp_modifiers else
            if annotated then annotated_comp_modifiers else predicate_comp_modifiers)
       | SOME _ => depth_limited_comp_modifiers
-    val mk_fun_of =
-      if random then mk_random_fun_of else
-      if annotated then mk_annotated_fun_of else
-      if (is_some depth_limit) then mk_depth_limited_fun_of else mk_fun_of
     val t_pred = compile_expr comp_modifiers compfuns thy
       (m, list_comb (pred, params)) inargs additional_arguments;
     val t_eval = if null outargs then t_pred else