generalizing the compilation process of the predicate compiler
authorbulwahn
Mon Mar 29 17:30:36 2010 +0200 (2010-03-29)
changeset 3601964bbbd858c39
parent 36018 096ec83348f3
child 36020 3ee4c29ead7f
generalizing the compilation process of the predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:36 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:36 2010 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    val register_intros : string * thm list -> theory -> theory
     1.5    val is_registered : theory -> string -> bool
     1.6    val function_name_of : Predicate_Compile_Aux.compilation -> theory
     1.7 -    -> string -> bool * Predicate_Compile_Aux.mode -> string
     1.8 +    -> string -> Predicate_Compile_Aux.mode -> string
     1.9    val predfun_intro_of: Proof.context -> string -> Predicate_Compile_Aux.mode -> thm
    1.10    val predfun_elim_of: Proof.context -> string -> Predicate_Compile_Aux.mode -> thm
    1.11    val all_preds_of : theory -> string list
    1.12 @@ -254,11 +254,11 @@
    1.13        ^ "functions defined for predicate " ^ quote name)
    1.14    | SOME fun_names => fun_names
    1.15  
    1.16 -fun function_name_of compilation thy name (pol, mode) =
    1.17 +fun function_name_of compilation thy name mode =
    1.18    case AList.lookup eq_mode
    1.19 -    (function_names_of (compilation_for_polarity pol compilation) thy name) mode of
    1.20 +    (function_names_of compilation thy name) mode of
    1.21      NONE => error ("No " ^ string_of_compilation compilation
    1.22 -      ^ "function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
    1.23 +      ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
    1.24    | SOME function_name => function_name
    1.25  
    1.26  fun modes_of compilation thy name = map fst (function_names_of compilation thy name)
    1.27 @@ -1021,6 +1021,8 @@
    1.28  val pred_compfuns = PredicateCompFuns.compfuns
    1.29  val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
    1.30  
    1.31 +(* compilation modifiers *)
    1.32 +
    1.33  (* function types and names of different compilations *)
    1.34  
    1.35  fun funT_of compfuns mode T =
    1.36 @@ -1031,6 +1033,264 @@
    1.37      inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
    1.38    end;
    1.39  
    1.40 +structure Comp_Mod =
    1.41 +struct
    1.42 +
    1.43 +datatype comp_modifiers = Comp_Modifiers of
    1.44 +{
    1.45 +  compilation : compilation,
    1.46 +  function_name_prefix : string,
    1.47 +  compfuns : compilation_funs,
    1.48 +  mk_random : typ -> term list -> term,
    1.49 +  modify_funT : typ -> typ,
    1.50 +  additional_arguments : string list -> term list,
    1.51 +  wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
    1.52 +  transform_additional_arguments : indprem -> term list -> term list
    1.53 +}
    1.54 +
    1.55 +fun dest_comp_modifiers (Comp_Modifiers c) = c
    1.56 +
    1.57 +val compilation = #compilation o dest_comp_modifiers
    1.58 +val function_name_prefix = #function_name_prefix o dest_comp_modifiers
    1.59 +val compfuns = #compfuns o dest_comp_modifiers
    1.60 +
    1.61 +val mk_random = #mk_random o dest_comp_modifiers
    1.62 +val funT_of' = funT_of o compfuns
    1.63 +val modify_funT = #modify_funT o dest_comp_modifiers
    1.64 +fun funT_of comp mode = modify_funT comp o funT_of' comp mode
    1.65 +
    1.66 +val additional_arguments = #additional_arguments o dest_comp_modifiers
    1.67 +val wrap_compilation = #wrap_compilation o dest_comp_modifiers
    1.68 +val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
    1.69 +
    1.70 +end;
    1.71 +
    1.72 +val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
    1.73 +  {
    1.74 +  compilation = Depth_Limited,
    1.75 +  function_name_prefix = "depth_limited_",
    1.76 +  compfuns = PredicateCompFuns.compfuns,
    1.77 +  mk_random = (fn _ => error "no random generation"),
    1.78 +  additional_arguments = fn names =>
    1.79 +    let
    1.80 +      val depth_name = Name.variant names "depth"
    1.81 +    in [Free (depth_name, @{typ code_numeral})] end,
    1.82 +  modify_funT = (fn T => let val (Ts, U) = strip_type T
    1.83 +  val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
    1.84 +  wrap_compilation =
    1.85 +    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
    1.86 +    let
    1.87 +      val [depth] = additional_arguments
    1.88 +      val (_, Ts) = split_modeT' mode (binder_types T)
    1.89 +      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
    1.90 +      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
    1.91 +    in
    1.92 +      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
    1.93 +        $ mk_bot compfuns (dest_predT compfuns T')
    1.94 +        $ compilation
    1.95 +    end,
    1.96 +  transform_additional_arguments =
    1.97 +    fn prem => fn additional_arguments =>
    1.98 +    let
    1.99 +      val [depth] = additional_arguments
   1.100 +      val depth' =
   1.101 +        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
   1.102 +          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
   1.103 +    in [depth'] end
   1.104 +  }
   1.105 +
   1.106 +val random_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.107 +  {
   1.108 +  compilation = Random,
   1.109 +  function_name_prefix = "random_",
   1.110 +  compfuns = PredicateCompFuns.compfuns,
   1.111 +  mk_random = (fn T => fn additional_arguments =>
   1.112 +  list_comb (Const(@{const_name Quickcheck.iter},
   1.113 +  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
   1.114 +    PredicateCompFuns.mk_predT T), additional_arguments)),
   1.115 +  modify_funT = (fn T =>
   1.116 +    let
   1.117 +      val (Ts, U) = strip_type T
   1.118 +      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
   1.119 +    in (Ts @ Ts') ---> U end),
   1.120 +  additional_arguments = (fn names =>
   1.121 +    let
   1.122 +      val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
   1.123 +    in
   1.124 +      [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
   1.125 +        Free (seed, @{typ "code_numeral * code_numeral"})]
   1.126 +    end),
   1.127 +  wrap_compilation = K (K (K (K (K I))))
   1.128 +    : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.129 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.130 +  }
   1.131 +
   1.132 +val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.133 +  {
   1.134 +  compilation = Depth_Limited_Random,
   1.135 +  function_name_prefix = "depth_limited_random_",
   1.136 +  compfuns = PredicateCompFuns.compfuns,
   1.137 +  mk_random = (fn T => fn additional_arguments =>
   1.138 +  list_comb (Const(@{const_name Quickcheck.iter},
   1.139 +  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
   1.140 +    PredicateCompFuns.mk_predT T), tl additional_arguments)),
   1.141 +  modify_funT = (fn T =>
   1.142 +    let
   1.143 +      val (Ts, U) = strip_type T
   1.144 +      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
   1.145 +        @{typ "code_numeral * code_numeral"}]
   1.146 +    in (Ts @ Ts') ---> U end),
   1.147 +  additional_arguments = (fn names =>
   1.148 +    let
   1.149 +      val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
   1.150 +    in
   1.151 +      [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
   1.152 +        Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
   1.153 +    end),
   1.154 +  wrap_compilation =
   1.155 +  fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
   1.156 +    let
   1.157 +      val depth = hd (additional_arguments)
   1.158 +      val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
   1.159 +        mode (binder_types T)
   1.160 +      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
   1.161 +      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
   1.162 +    in
   1.163 +      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
   1.164 +        $ mk_bot compfuns (dest_predT compfuns T')
   1.165 +        $ compilation
   1.166 +    end,
   1.167 +  transform_additional_arguments =
   1.168 +    fn prem => fn additional_arguments =>
   1.169 +    let
   1.170 +      val [depth, nrandom, size, seed] = additional_arguments
   1.171 +      val depth' =
   1.172 +        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
   1.173 +          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
   1.174 +    in [depth', nrandom, size, seed] end
   1.175 +}
   1.176 +
   1.177 +val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.178 +  {
   1.179 +  compilation = Pred,
   1.180 +  function_name_prefix = "",
   1.181 +  compfuns = PredicateCompFuns.compfuns,
   1.182 +  mk_random = (fn _ => error "no random generation"),
   1.183 +  modify_funT = I,
   1.184 +  additional_arguments = K [],
   1.185 +  wrap_compilation = K (K (K (K (K I))))
   1.186 +   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.187 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.188 +  }
   1.189 +
   1.190 +val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.191 +  {
   1.192 +  compilation = Annotated,
   1.193 +  function_name_prefix = "annotated_",
   1.194 +  compfuns = PredicateCompFuns.compfuns,
   1.195 +  mk_random = (fn _ => error "no random generation"),
   1.196 +  modify_funT = I,
   1.197 +  additional_arguments = K [],
   1.198 +  wrap_compilation =
   1.199 +    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
   1.200 +      mk_tracing ("calling predicate " ^ s ^
   1.201 +        " with mode " ^ string_of_mode mode) compilation,
   1.202 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.203 +  }
   1.204 +
   1.205 +val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.206 +  {
   1.207 +  compilation = DSeq,
   1.208 +  function_name_prefix = "dseq_",
   1.209 +  compfuns = DSequence_CompFuns.compfuns,
   1.210 +  mk_random = (fn _ => error "no random generation"),
   1.211 +  modify_funT = I,
   1.212 +  additional_arguments = K [],
   1.213 +  wrap_compilation = K (K (K (K (K I))))
   1.214 +   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.215 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.216 +  }
   1.217 +
   1.218 +val pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.219 +  {
   1.220 +  compilation = Pos_Random_DSeq,
   1.221 +  function_name_prefix = "random_dseq_",
   1.222 +  compfuns = Random_Sequence_CompFuns.compfuns,
   1.223 +  mk_random = (fn T => fn additional_arguments =>
   1.224 +  let
   1.225 +    val random = Const ("Quickcheck.random_class.random",
   1.226 +      @{typ code_numeral} --> @{typ Random.seed} -->
   1.227 +        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
   1.228 +  in
   1.229 +    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
   1.230 +      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
   1.231 +      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
   1.232 +  end),
   1.233 +
   1.234 +  modify_funT = I,
   1.235 +  additional_arguments = K [],
   1.236 +  wrap_compilation = K (K (K (K (K I))))
   1.237 +   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.238 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.239 +  }
   1.240 +
   1.241 +val neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.242 +  {
   1.243 +  compilation = Neg_Random_DSeq,
   1.244 +  function_name_prefix = "random_dseq_neg_",
   1.245 +  compfuns = Random_Sequence_CompFuns.compfuns,
   1.246 +  mk_random = (fn _ => error "no random generation"),
   1.247 +  modify_funT = I,
   1.248 +  additional_arguments = K [],
   1.249 +  wrap_compilation = K (K (K (K (K I))))
   1.250 +   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.251 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.252 +  }
   1.253 +
   1.254 +
   1.255 +val new_pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.256 +  {
   1.257 +  compilation = New_Pos_Random_DSeq,
   1.258 +  function_name_prefix = "new_random_dseq_",
   1.259 +  compfuns = New_Pos_Random_Sequence_CompFuns.compfuns,
   1.260 +  mk_random = (fn T => fn additional_arguments =>
   1.261 +  let
   1.262 +    val random = Const ("Quickcheck.random_class.random",
   1.263 +      @{typ code_numeral} --> @{typ Random.seed} -->
   1.264 +        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
   1.265 +  in
   1.266 +    Const ("New_Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
   1.267 +      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
   1.268 +      New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random
   1.269 +  end),
   1.270 +  modify_funT = I,
   1.271 +  additional_arguments = K [],
   1.272 +  wrap_compilation = K (K (K (K (K I))))
   1.273 +   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.274 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.275 +  }
   1.276 +
   1.277 +val new_neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.278 +  {
   1.279 +  compilation = New_Neg_Random_DSeq,
   1.280 +  function_name_prefix = "new_random_dseq_neg_",
   1.281 +  compfuns = New_Neg_Random_Sequence_CompFuns.compfuns,
   1.282 +  mk_random = (fn _ => error "no random generation"),
   1.283 +  modify_funT = I,
   1.284 +  additional_arguments = K [],
   1.285 +  wrap_compilation = K (K (K (K (K I))))
   1.286 +   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.287 +  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.288 +  }
   1.289 +
   1.290 +fun negative_comp_modifiers_of comp_modifiers =
   1.291 +    (case Comp_Mod.compilation comp_modifiers of
   1.292 +      Pos_Random_DSeq => neg_random_dseq_comp_modifiers
   1.293 +    | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
   1.294 +    | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
   1.295 +    | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
   1.296 +    | c => comp_modifiers)
   1.297 +
   1.298  (** mode analysis **)
   1.299  
   1.300  type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}
   1.301 @@ -1581,40 +1841,8 @@
   1.302      (t, names)
   1.303    end;
   1.304  
   1.305 -structure Comp_Mod =
   1.306 -struct
   1.307 -
   1.308 -datatype comp_modifiers = Comp_Modifiers of
   1.309 -{
   1.310 -  compilation : compilation,
   1.311 -  function_name_prefix : string,
   1.312 -  compfuns : compilation_funs,
   1.313 -  mk_random : typ -> term list -> term,
   1.314 -  modify_funT : typ -> typ,
   1.315 -  additional_arguments : string list -> term list,
   1.316 -  wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
   1.317 -  transform_additional_arguments : indprem -> term list -> term list
   1.318 -}
   1.319 -
   1.320 -fun dest_comp_modifiers (Comp_Modifiers c) = c
   1.321 -
   1.322 -val compilation = #compilation o dest_comp_modifiers
   1.323 -val function_name_prefix = #function_name_prefix o dest_comp_modifiers
   1.324 -val compfuns = #compfuns o dest_comp_modifiers
   1.325 -
   1.326 -val mk_random = #mk_random o dest_comp_modifiers
   1.327 -val funT_of' = funT_of o compfuns
   1.328 -val modify_funT = #modify_funT o dest_comp_modifiers
   1.329 -fun funT_of comp mode = modify_funT comp o funT_of' comp mode
   1.330 -
   1.331 -val additional_arguments = #additional_arguments o dest_comp_modifiers
   1.332 -val wrap_compilation = #wrap_compilation o dest_comp_modifiers
   1.333 -val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
   1.334 -
   1.335 -end;
   1.336 -
   1.337  (* TODO: uses param_vs -- change necessary for compilation with new modes *)
   1.338 -fun compile_arg compilation_modifiers compfuns additional_arguments ctxt param_vs iss arg = 
   1.339 +fun compile_arg compilation_modifiers additional_arguments ctxt param_vs iss arg = 
   1.340    let
   1.341      fun map_params (t as Free (f, T)) =
   1.342        if member (op =) param_vs f then
   1.343 @@ -1629,12 +1857,13 @@
   1.344        | map_params t = t
   1.345      in map_aterms map_params arg end
   1.346  
   1.347 -fun compile_match compilation_modifiers compfuns additional_arguments
   1.348 +fun compile_match compilation_modifiers additional_arguments
   1.349    param_vs iss ctxt eqs eqs' out_ts success_t =
   1.350    let
   1.351 +    val compfuns = Comp_Mod.compfuns compilation_modifiers
   1.352      val eqs'' = maps mk_eq eqs @ eqs'
   1.353      val eqs'' =
   1.354 -      map (compile_arg compilation_modifiers compfuns additional_arguments ctxt param_vs iss) eqs''
   1.355 +      map (compile_arg compilation_modifiers additional_arguments ctxt param_vs iss) eqs''
   1.356      val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
   1.357      val name = Name.variant names "x";
   1.358      val name' = Name.variant (name :: names) "y";
   1.359 @@ -1663,15 +1892,16 @@
   1.360    | (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
   1.361    | (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode m ^ "]")
   1.362  
   1.363 -fun compile_expr compilation_modifiers compfuns ctxt pol (t, deriv) additional_arguments =
   1.364 +fun compile_expr compilation_modifiers ctxt pol (t, deriv) additional_arguments =
   1.365    let
   1.366 +    val compfuns = Comp_Mod.compfuns compilation_modifiers
   1.367      fun expr_of (t, deriv) =
   1.368        (case (t, deriv) of
   1.369          (t, Term Input) => SOME t
   1.370        | (t, Term Output) => NONE
   1.371        | (Const (name, T), Context mode) =>
   1.372          SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
   1.373 -          (ProofContext.theory_of ctxt) name (pol, mode),
   1.374 +          (ProofContext.theory_of ctxt) name mode,
   1.375            Comp_Mod.funT_of compilation_modifiers mode T))
   1.376        | (Free (s, T), Context m) =>
   1.377          SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
   1.378 @@ -1695,11 +1925,12 @@
   1.379      list_comb (the (expr_of (t, deriv)), additional_arguments)
   1.380    end
   1.381  
   1.382 -fun compile_clause compilation_modifiers compfuns ctxt all_vs param_vs additional_arguments
   1.383 +fun compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments
   1.384    (pol, mode) inp (ts, moded_ps) =
   1.385    let
   1.386 +    val compfuns = Comp_Mod.compfuns compilation_modifiers
   1.387      val iss = ho_arg_modes_of mode
   1.388 -    val compile_match = compile_match compilation_modifiers compfuns
   1.389 +    val compile_match = compile_match compilation_modifiers
   1.390        additional_arguments param_vs iss ctxt
   1.391      val (in_ts, out_ts) = split_mode mode ts;
   1.392      val (in_ts', (all_vs', eqs)) =
   1.393 @@ -1728,7 +1959,7 @@
   1.394                 Prem t =>
   1.395                   let
   1.396                     val u =
   1.397 -                     compile_expr compilation_modifiers compfuns ctxt
   1.398 +                     compile_expr compilation_modifiers ctxt
   1.399                         pol (t, deriv) additional_arguments'
   1.400                     val (_, out_ts''') = split_mode mode (snd (strip_comb t))
   1.401                     val rest = compile_prems out_ts''' vs' names'' ps
   1.402 @@ -1737,9 +1968,10 @@
   1.403                   end
   1.404               | Negprem t =>
   1.405                   let
   1.406 -                   
   1.407 +                   val neg_compilation_modifiers =
   1.408 +                     negative_comp_modifiers_of compilation_modifiers
   1.409                     val u = mk_not compfuns
   1.410 -                     (compile_expr compilation_modifiers compfuns ctxt
   1.411 +                     (compile_expr neg_compilation_modifiers ctxt
   1.412                         (not pol) (t, deriv) additional_arguments')
   1.413                     val (_, out_ts''') = split_mode mode (snd (strip_comb t))
   1.414                     val rest = compile_prems out_ts''' vs' names'' ps
   1.415 @@ -1748,7 +1980,7 @@
   1.416                   end
   1.417               | Sidecond t =>
   1.418                   let
   1.419 -                   val t = compile_arg compilation_modifiers compfuns additional_arguments
   1.420 +                   val t = compile_arg compilation_modifiers additional_arguments
   1.421                       ctxt param_vs iss t
   1.422                     val rest = compile_prems [] vs' names'' ps;
   1.423                   in
   1.424 @@ -1796,7 +2028,7 @@
   1.425      val in_ts' = map_filter (map_filter_prod
   1.426        (fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
   1.427      val cl_ts =
   1.428 -      map (compile_clause compilation_modifiers compfuns
   1.429 +      map (compile_clause compilation_modifiers
   1.430          ctxt all_vs param_vs additional_arguments (pol, mode) (HOLogic.mk_tuple in_ts')) moded_cls;
   1.431      val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns
   1.432        s T mode additional_arguments
   1.433 @@ -1805,7 +2037,7 @@
   1.434        else foldr1 (mk_sup compfuns) cl_ts)
   1.435      val fun_const =
   1.436        Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
   1.437 -      (ProofContext.theory_of ctxt) s (pol, mode), funT)
   1.438 +      (ProofContext.theory_of ctxt) s mode, funT)
   1.439    in
   1.440      HOLogic.mk_Trueprop
   1.441        (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
   1.442 @@ -2591,7 +2823,7 @@
   1.443              val arg_names = Name.variant_list []
   1.444                (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
   1.445              val args = map2 (curry Free) arg_names Ts
   1.446 -            val predfun = Const (function_name_of Pred thy predname (true, full_mode),
   1.447 +            val predfun = Const (function_name_of Pred thy predname full_mode,
   1.448                Ts ---> PredicateCompFuns.mk_predT @{typ unit})
   1.449              val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
   1.450              val eq_term = HOLogic.mk_Trueprop
   1.451 @@ -2714,125 +2946,6 @@
   1.452        scc thy' |> Theory.checkpoint
   1.453    in thy'' end
   1.454  
   1.455 -val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.456 -  {
   1.457 -  compilation = Depth_Limited,
   1.458 -  function_name_prefix = "depth_limited_",
   1.459 -  compfuns = PredicateCompFuns.compfuns,
   1.460 -  mk_random = (fn _ => error "no random generation"),
   1.461 -  additional_arguments = fn names =>
   1.462 -    let
   1.463 -      val depth_name = Name.variant names "depth"
   1.464 -    in [Free (depth_name, @{typ code_numeral})] end,
   1.465 -  modify_funT = (fn T => let val (Ts, U) = strip_type T
   1.466 -  val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
   1.467 -  wrap_compilation =
   1.468 -    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
   1.469 -    let
   1.470 -      val [depth] = additional_arguments
   1.471 -      val (_, Ts) = split_modeT' mode (binder_types T)
   1.472 -      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
   1.473 -      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
   1.474 -    in
   1.475 -      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
   1.476 -        $ mk_bot compfuns (dest_predT compfuns T')
   1.477 -        $ compilation
   1.478 -    end,
   1.479 -  transform_additional_arguments =
   1.480 -    fn prem => fn additional_arguments =>
   1.481 -    let
   1.482 -      val [depth] = additional_arguments
   1.483 -      val depth' =
   1.484 -        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
   1.485 -          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
   1.486 -    in [depth'] end
   1.487 -  }
   1.488 -
   1.489 -val random_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.490 -  {
   1.491 -  compilation = Random,
   1.492 -  function_name_prefix = "random_",
   1.493 -  compfuns = PredicateCompFuns.compfuns,
   1.494 -  mk_random = (fn T => fn additional_arguments =>
   1.495 -  list_comb (Const(@{const_name Quickcheck.iter},
   1.496 -  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
   1.497 -    PredicateCompFuns.mk_predT T), additional_arguments)),
   1.498 -  modify_funT = (fn T =>
   1.499 -    let
   1.500 -      val (Ts, U) = strip_type T
   1.501 -      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
   1.502 -    in (Ts @ Ts') ---> U end),
   1.503 -  additional_arguments = (fn names =>
   1.504 -    let
   1.505 -      val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
   1.506 -    in
   1.507 -      [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
   1.508 -        Free (seed, @{typ "code_numeral * code_numeral"})]
   1.509 -    end),
   1.510 -  wrap_compilation = K (K (K (K (K I))))
   1.511 -    : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.512 -  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.513 -  }
   1.514 -
   1.515 -val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.516 -  {
   1.517 -  compilation = Depth_Limited_Random,
   1.518 -  function_name_prefix = "depth_limited_random_",
   1.519 -  compfuns = PredicateCompFuns.compfuns,
   1.520 -  mk_random = (fn T => fn additional_arguments =>
   1.521 -  list_comb (Const(@{const_name Quickcheck.iter},
   1.522 -  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
   1.523 -    PredicateCompFuns.mk_predT T), tl additional_arguments)),
   1.524 -  modify_funT = (fn T =>
   1.525 -    let
   1.526 -      val (Ts, U) = strip_type T
   1.527 -      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
   1.528 -        @{typ "code_numeral * code_numeral"}]
   1.529 -    in (Ts @ Ts') ---> U end),
   1.530 -  additional_arguments = (fn names =>
   1.531 -    let
   1.532 -      val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
   1.533 -    in
   1.534 -      [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
   1.535 -        Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
   1.536 -    end),
   1.537 -  wrap_compilation =
   1.538 -  fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
   1.539 -    let
   1.540 -      val depth = hd (additional_arguments)
   1.541 -      val (_, Ts) = split_modeT' mode (binder_types T)
   1.542 -      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
   1.543 -      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
   1.544 -    in
   1.545 -      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
   1.546 -        $ mk_bot compfuns (dest_predT compfuns T')
   1.547 -        $ compilation
   1.548 -    end,
   1.549 -  transform_additional_arguments =
   1.550 -    fn prem => fn additional_arguments =>
   1.551 -    let
   1.552 -      val [depth, nrandom, size, seed] = additional_arguments
   1.553 -      val depth' =
   1.554 -        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
   1.555 -          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
   1.556 -    in [depth', nrandom, size, seed] end
   1.557 -}
   1.558 -
   1.559 -(* different instantiantions of the predicate compiler *)
   1.560 -
   1.561 -val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.562 -  {
   1.563 -  compilation = Pred,
   1.564 -  function_name_prefix = "",
   1.565 -  compfuns = PredicateCompFuns.compfuns,
   1.566 -  mk_random = (fn _ => error "no random generation"),
   1.567 -  modify_funT = I,
   1.568 -  additional_arguments = K [],
   1.569 -  wrap_compilation = K (K (K (K (K I))))
   1.570 -   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.571 -  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.572 -  }
   1.573 -
   1.574  val add_equations = gen_add_equations
   1.575    (Steps {
   1.576    define_functions =
   1.577 @@ -2845,106 +2958,6 @@
   1.578    use_random = false,
   1.579    qname = "equation"})
   1.580  
   1.581 -val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.582 -  {
   1.583 -  compilation = Annotated,
   1.584 -  function_name_prefix = "annotated_",
   1.585 -  compfuns = PredicateCompFuns.compfuns,
   1.586 -  mk_random = (fn _ => error "no random generation"),
   1.587 -  modify_funT = I,
   1.588 -  additional_arguments = K [],
   1.589 -  wrap_compilation =
   1.590 -    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
   1.591 -      mk_tracing ("calling predicate " ^ s ^
   1.592 -        " with mode " ^ string_of_mode mode) compilation,
   1.593 -  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.594 -  }
   1.595 -
   1.596 -val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.597 -  {
   1.598 -  compilation = DSeq,
   1.599 -  function_name_prefix = "dseq_",
   1.600 -  compfuns = DSequence_CompFuns.compfuns,
   1.601 -  mk_random = (fn _ => error "no random generation"),
   1.602 -  modify_funT = I,
   1.603 -  additional_arguments = K [],
   1.604 -  wrap_compilation = K (K (K (K (K I))))
   1.605 -   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.606 -  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.607 -  }
   1.608 -
   1.609 -val pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.610 -  {
   1.611 -  compilation = Pos_Random_DSeq,
   1.612 -  function_name_prefix = "random_dseq_",
   1.613 -  compfuns = Random_Sequence_CompFuns.compfuns,
   1.614 -  mk_random = (fn T => fn additional_arguments =>
   1.615 -  let
   1.616 -    val random = Const ("Quickcheck.random_class.random",
   1.617 -      @{typ code_numeral} --> @{typ Random.seed} -->
   1.618 -        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
   1.619 -  in
   1.620 -    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
   1.621 -      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
   1.622 -      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
   1.623 -  end),
   1.624 -
   1.625 -  modify_funT = I,
   1.626 -  additional_arguments = K [],
   1.627 -  wrap_compilation = K (K (K (K (K I))))
   1.628 -   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.629 -  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.630 -  }
   1.631 -
   1.632 -val neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.633 -  {
   1.634 -  compilation = Neg_Random_DSeq,
   1.635 -  function_name_prefix = "random_dseq_neg_",
   1.636 -  compfuns = Random_Sequence_CompFuns.compfuns,
   1.637 -  mk_random = (fn _ => error "no random generation"),
   1.638 -  modify_funT = I,
   1.639 -  additional_arguments = K [],
   1.640 -  wrap_compilation = K (K (K (K (K I))))
   1.641 -   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.642 -  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.643 -  }
   1.644 -
   1.645 -
   1.646 -val new_pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.647 -  {
   1.648 -  compilation = New_Pos_Random_DSeq,
   1.649 -  function_name_prefix = "new_random_dseq_",
   1.650 -  compfuns = New_Pos_Random_Sequence_CompFuns.compfuns,
   1.651 -  mk_random = (fn T => fn additional_arguments =>
   1.652 -  let
   1.653 -    val random = Const ("Quickcheck.random_class.random",
   1.654 -      @{typ code_numeral} --> @{typ Random.seed} -->
   1.655 -        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
   1.656 -  in
   1.657 -    Const ("New_Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
   1.658 -      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
   1.659 -      New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random
   1.660 -  end),
   1.661 -  modify_funT = I,
   1.662 -  additional_arguments = K [],
   1.663 -  wrap_compilation = K (K (K (K (K I))))
   1.664 -   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.665 -  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.666 -  }
   1.667 -
   1.668 -val new_neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
   1.669 -  {
   1.670 -  compilation = New_Neg_Random_DSeq,
   1.671 -  function_name_prefix = "new_random_dseq_neg_",
   1.672 -  compfuns = New_Neg_Random_Sequence_CompFuns.compfuns,
   1.673 -  mk_random = (fn _ => error "no random generation"),
   1.674 -  modify_funT = I,
   1.675 -  additional_arguments = K [],
   1.676 -  wrap_compilation = K (K (K (K (K I))))
   1.677 -   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
   1.678 -  transform_additional_arguments = K I : (indprem -> term list -> term list)
   1.679 -  }
   1.680 -
   1.681  val add_depth_limited_equations = gen_add_equations
   1.682    (Steps {
   1.683    define_functions =
   1.684 @@ -3192,7 +3205,7 @@
   1.685            (*| Annotated => annotated_comp_modifiers*)
   1.686            | DSeq => dseq_comp_modifiers
   1.687            | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
   1.688 -        val t_pred = compile_expr comp_modifiers compfuns (ProofContext.init thy)
   1.689 +        val t_pred = compile_expr comp_modifiers (ProofContext.init thy)
   1.690            true (body, deriv) additional_arguments;
   1.691          val T_pred = dest_predT compfuns (fastype_of t_pred)
   1.692          val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple