Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: predicate_compile_core.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_core.ML
    Author:     Lukas Bulwahn, TU Muenchen

A compiler from predicates specified by intro/elim rules to equations.
*)

signature PREDICATE_COMPILE_CORE =
sig
  type seed = Random_Engine.seed
  type mode = Predicate_Compile_Aux.mode
  type options = Predicate_Compile_Aux.options
  type compilation = Predicate_Compile_Aux.compilation
  type compilation_funs = Predicate_Compile_Aux.compilation_funs

  val code_pred : options -> string -> Proof.context -> Proof.state
  val code_pred_cmd : options -> string -> Proof.context -> Proof.state
  val values_cmd : string list -> mode option list option ->
    ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit

  val values_timeout : real Config.T

  val print_stored_rules : Proof.context -> unit
  val print_all_modes : compilation -> Proof.context -> unit

  val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
  val put_pred_random_result : (unit -> seed -> term Predicate.pred * seed) ->
    Proof.context -> Proof.context
  val put_dseq_result : (unit -> term Limited_Sequence.dseq) -> Proof.context -> Proof.context
  val put_dseq_random_result :
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
      term Limited_Sequence.dseq * seed) ->
    Proof.context -> Proof.context
  val put_new_dseq_result : (unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) ->
    Proof.context -> Proof.context
  val put_lseq_random_result :
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
      term Lazy_Sequence.lazy_sequence) ->
    Proof.context -> Proof.context
  val put_lseq_random_stats_result :
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
      (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence) ->
    Proof.context -> Proof.context

  val code_pred_intro_attrib : attribute
  (* used by Quickcheck_Generator *)
  (* temporary for testing of the compilation *)
  val add_equations : options -> string list -> theory -> theory
  val add_depth_limited_random_equations : options -> string list -> theory -> theory
  val add_random_dseq_equations : options -> string list -> theory -> theory
  val add_new_random_dseq_equations : options -> string list -> theory -> theory
  val add_generator_dseq_equations : options -> string list -> theory -> theory
  val add_generator_cps_equations : options -> string list -> theory -> theory
  val mk_tracing : string -> term -> term
  val prepare_intrs : options -> Proof.context -> string list -> thm list ->
    ((string * typ) list * string list * string list * (string * mode list) list *
      (string *  (Term.term list * Predicate_Compile_Aux.indprem list) list) list)
  type mode_analysis_options =
   {use_generators : bool,
    reorder_premises : bool,
    infer_pos_and_neg_modes : bool}
  datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
    | Mode_Pair of mode_derivation * mode_derivation | Term of mode
  val head_mode_of : mode_derivation -> mode
  type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
  type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list

end;

structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
struct

type random_seed = Random_Engine.seed

open Predicate_Compile_Aux;
open Mode_Inference;
open Predicate_Compile_Proof;

type seed = Random_Engine.seed;

(** fundamentals **)

(* syntactic operations *)

fun mk_eq (x, xs) =
  let fun mk_eqs _ [] = []
        | mk_eqs a (b::cs) =
            HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
  in mk_eqs x xs end;

fun mk_tracing s t =
  Const(\<^const_name>\<open>Code_Evaluation.tracing\<close>,
    \<^typ>\<open>String.literal\<close> --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t

(* representation of inferred clauses with modes *)

type moded_clause = term list * (indprem * mode_derivation) list

type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list

(* diagnostic display functions *)

fun print_modes options modes =
  if show_modes options then
    tracing ("Inferred modes:\n" ^
      cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
        (fn (p, m) => string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
  else ()

fun print_pred_mode_table string_of_entry pred_mode_table =
  let
    fun print_mode pred ((_, mode), entry) =  "mode : " ^ string_of_mode mode
      ^ string_of_entry pred mode entry
    fun print_pred (pred, modes) =
      "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
    val _ = tracing (cat_lines (map print_pred pred_mode_table))
  in () end;

fun print_compiled_terms options ctxt =
  if show_compilation options then
    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt)
  else K ()

fun print_stored_rules ctxt =
  let
    val preds = Graph.keys (Core_Data.PredData.get (Proof_Context.theory_of ctxt))
    fun print pred () =
      let
        val _ = writeln ("predicate: " ^ pred)
        val _ = writeln ("introrules: ")
        val _ = fold (fn thm => fn _ => writeln (Thm.string_of_thm ctxt thm))
          (rev (Core_Data.intros_of ctxt pred)) ()
      in
        if Core_Data.has_elim ctxt pred then
          writeln ("elimrule: " ^ Thm.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred))
        else
          writeln ("no elimrule defined")
      end
  in
    fold print preds ()
  end;

fun print_all_modes compilation ctxt =
  let
    val _ = writeln ("Inferred modes:")
    fun print (pred, modes) u =
      let
        val _ = writeln ("predicate: " ^ pred)
        val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
      in u end
  in
    fold print (Core_Data.all_modes_of compilation ctxt) ()
  end

(* validity checks *)

fun check_expected_modes options _ modes =
  (case expected_modes options of
    SOME (s, ms) =>
      (case AList.lookup (op =) modes s of
        SOME modes =>
          let
            val modes' = map snd modes
          in
            if not (eq_set eq_mode (ms, modes')) then
              error ("expected modes were not inferred:\n"
              ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n"
              ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms))
            else ()
          end
        | NONE => ())
  | NONE => ())

fun check_proposed_modes options preds modes errors =
  map (fn (s, _) =>
    case proposed_modes options s of
      SOME ms =>
        (case AList.lookup (op =) modes s of
          SOME inferred_ms =>
            let
              val preds_without_modes = map fst (filter (null o snd) modes)
              val modes' = map snd inferred_ms
            in
              if not (eq_set eq_mode (ms, modes')) then
                error ("expected modes were not inferred:\n"
                ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n"
                ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
                ^ (if show_invalid_clauses options then
                ("For the following clauses, the following modes could not be inferred: " ^ "\n"
                ^ cat_lines errors) else "") ^
                (if not (null preds_without_modes) then
                  "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
                else ""))
              else ()
            end
        | NONE => ())
    | NONE => ()) preds

fun check_matches_type ctxt predname T ms =
  let
    fun check (Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
      | check m (Type("fun", _)) = (m = Input orelse m = Output)
      | check (Pair (m1, m2)) (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) =
          check m1 T1 andalso check m2 T2
      | check Input _ = true
      | check Output _ = true
      | check Bool \<^typ>\<open>bool\<close> = true
      | check _ _ = false
    fun check_consistent_modes ms =
      if forall (fn Fun _ => true | _ => false) ms then
        apply2 check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms))
        |> (fn (res1, res2) => res1 andalso res2)
      else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then
        true
      else if forall (fn Bool => true | _ => false) ms then
        true
      else
        false
    val _ =
      map (fn mode =>
        if length (strip_fun_mode mode) = length (binder_types T)
          andalso (forall (uncurry check) (strip_fun_mode mode ~~ binder_types T)) then ()
        else
          error (string_of_mode mode ^ " is not a valid mode for " ^
            Syntax.string_of_typ ctxt T ^ " at predicate " ^ predname)) ms
    val _ =
      if check_consistent_modes ms then ()
      else
        error (commas (map string_of_mode ms) ^ " are inconsistent modes for predicate " ^ predname)
  in
    ms
  end

(* compilation modifiers *)

structure Comp_Mod =  (* FIXME proper signature *)
struct

datatype comp_modifiers = Comp_Modifiers of
{
  compilation : compilation,
  function_name_prefix : string,
  compfuns : compilation_funs,
  mk_random : typ -> term list -> term,
  modify_funT : typ -> typ,
  additional_arguments : string list -> term list,
  wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
  transform_additional_arguments : indprem -> term list -> term list
}

fun dest_comp_modifiers (Comp_Modifiers c) = c

val compilation = #compilation o dest_comp_modifiers
val function_name_prefix = #function_name_prefix o dest_comp_modifiers
val compfuns = #compfuns o dest_comp_modifiers

val mk_random = #mk_random o dest_comp_modifiers
val funT_of' = funT_of o compfuns
val modify_funT = #modify_funT o dest_comp_modifiers
fun funT_of comp mode = modify_funT comp o funT_of' comp mode

val additional_arguments = #additional_arguments o dest_comp_modifiers
val wrap_compilation = #wrap_compilation o dest_comp_modifiers
val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers

fun set_compfuns compfuns' (Comp_Modifiers {compilation, function_name_prefix, compfuns, mk_random,
    modify_funT, additional_arguments, wrap_compilation, transform_additional_arguments}) =
    (Comp_Modifiers {compilation = compilation, function_name_prefix = function_name_prefix,
    compfuns = compfuns', mk_random = mk_random, modify_funT = modify_funT,
    additional_arguments = additional_arguments, wrap_compilation = wrap_compilation,
    transform_additional_arguments = transform_additional_arguments})

end

fun unlimited_compfuns_of true New_Pos_Random_DSeq =
      New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
  | unlimited_compfuns_of false New_Pos_Random_DSeq =
      New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
  | unlimited_compfuns_of true Pos_Generator_DSeq =
      New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
  | unlimited_compfuns_of false Pos_Generator_DSeq =
      New_Neg_DSequence_CompFuns.depth_unlimited_compfuns
  | unlimited_compfuns_of _ c =
      raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c)

fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
      New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
  | limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
      New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
  | limited_compfuns_of true Pos_Generator_DSeq =
      New_Pos_DSequence_CompFuns.depth_limited_compfuns
  | limited_compfuns_of false Pos_Generator_DSeq =
      New_Neg_DSequence_CompFuns.depth_limited_compfuns
  | limited_compfuns_of _ c =
      raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c)

val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = Depth_Limited,
  function_name_prefix = "depth_limited_",
  compfuns = Predicate_Comp_Funs.compfuns,
  mk_random = (fn _ => error "no random generation"),
  additional_arguments = fn names =>
    let
      val depth_name = singleton (Name.variant_list names) "depth"
    in [Free (depth_name, \<^typ>\<open>natural\<close>)] end,
  modify_funT = (fn T => let val (Ts, U) = strip_type T
  val Ts' = [\<^typ>\natural\] in (Ts @ Ts') ---> U end),
  wrap_compilation =
    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
    let
      val [depth] = additional_arguments
      val (_, Ts) = split_modeT mode (binder_types T)
      val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts)
      val if_const = Const (\<^const_name>\<open>If\<close>, \<^typ>\<open>bool\<close> --> T' --> T' --> T')
    in
      if_const $ HOLogic.mk_eq (depth, \<^term>\<open>0 :: natural\<close>)
        $ mk_empty compfuns (dest_monadT compfuns T')
        $ compilation
    end,
  transform_additional_arguments =
    fn _ => fn additional_arguments =>
    let
      val [depth] = additional_arguments
      val depth' =
        Const (\<^const_name>\<open>Groups.minus\<close>, \<^typ>\<open>natural => natural => natural\<close>)
          $ depth $ Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>natural\<close>)
    in [depth'] end
  }

val random_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = Random,
  function_name_prefix = "random_",
  compfuns = Predicate_Comp_Funs.compfuns,
  mk_random = (fn T => fn additional_arguments =>
  list_comb (Const(\<^const_name>\<open>Random_Pred.iter\<close>,
  [\<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, \<^typ>\<open>Random.seed\<close>] --->
    Predicate_Comp_Funs.mk_monadT T), additional_arguments)),
  modify_funT = (fn T =>
    let
      val (Ts, U) = strip_type T
      val Ts' = [\<^typ>\natural\, \<^typ>\natural\, \<^typ>\Random.seed\]
    in (Ts @ Ts') ---> U end),
  additional_arguments = (fn names =>
    let
      val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
    in
      [Free (nrandom, \<^typ>\<open>natural\<close>), Free (size, \<^typ>\<open>natural\<close>),
        Free (seed, \<^typ>\<open>Random.seed\<close>)]
    end),
  wrap_compilation = K (K (K (K (K I))))
    : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = Depth_Limited_Random,
  function_name_prefix = "depth_limited_random_",
  compfuns = Predicate_Comp_Funs.compfuns,
  mk_random = (fn T => fn additional_arguments =>
  list_comb (Const(\<^const_name>\<open>Random_Pred.iter\<close>,
  [\<^typ>\<open>natural\<close>, \<^typ>\<open>natural\<close>, \<^typ>\<open>Random.seed\<close>] --->
    Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)),
  modify_funT = (fn T =>
    let
      val (Ts, U) = strip_type T
      val Ts' = [\<^typ>\natural\, \<^typ>\natural\, \<^typ>\natural\,
        \<^typ>\<open>Random.seed\<close>]
    in (Ts @ Ts') ---> U end),
  additional_arguments = (fn names =>
    let
      val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
    in
      [Free (depth, \<^typ>\<open>natural\<close>), Free (nrandom, \<^typ>\<open>natural\<close>),
        Free (size, \<^typ>\<open>natural\<close>), Free (seed, \<^typ>\<open>Random.seed\<close>)]
    end),
  wrap_compilation =
  fn compfuns => fn _ => fn T => fn mode => fn additional_arguments => fn compilation =>
    let
      val depth = hd (additional_arguments)
      val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
        mode (binder_types T)
      val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts)
      val if_const = Const (\<^const_name>\<open>If\<close>, \<^typ>\<open>bool\<close> --> T' --> T' --> T')
    in
      if_const $ HOLogic.mk_eq (depth, \<^term>\<open>0 :: natural\<close>)
        $ mk_empty compfuns (dest_monadT compfuns T')
        $ compilation
    end,
  transform_additional_arguments =
    fn _ => fn additional_arguments =>
    let
      val [depth, nrandom, size, seed] = additional_arguments
      val depth' =
        Const (\<^const_name>\<open>Groups.minus\<close>, \<^typ>\<open>natural => natural => natural\<close>)
          $ depth $ Const (\<^const_name>\<open>Groups.one\<close>, \<^typ>\<open>natural\<close>)
    in [depth', nrandom, size, seed] end
}

val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = Pred,
  function_name_prefix = "",
  compfuns = Predicate_Comp_Funs.compfuns,
  mk_random = (fn _ => error "no random generation"),
  modify_funT = I,
  additional_arguments = K [],
  wrap_compilation = K (K (K (K (K I))))
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = DSeq,
  function_name_prefix = "dseq_",
  compfuns = DSequence_CompFuns.compfuns,
  mk_random = (fn _ => error "no random generation in dseq"),
  modify_funT = I,
  additional_arguments = K [],
  wrap_compilation = K (K (K (K (K I))))
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

val pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = Pos_Random_DSeq,
  function_name_prefix = "random_dseq_",
  compfuns = Random_Sequence_CompFuns.compfuns,
  mk_random = (fn T => fn _ =>
  let
    val random = Const (\<^const_name>\<open>Quickcheck_Random.random\<close>,
      \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
        HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>))
  in
    Const (\<^const_name>\<open>Random_Sequence.Random\<close>, (\<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
      HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>)) -->
      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
  end),

  modify_funT = I,
  additional_arguments = K [],
  wrap_compilation = K (K (K (K (K I))))
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

val neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = Neg_Random_DSeq,
  function_name_prefix = "random_dseq_neg_",
  compfuns = Random_Sequence_CompFuns.compfuns,
  mk_random = (fn _ => error "no random generation"),
  modify_funT = I,
  additional_arguments = K [],
  wrap_compilation = K (K (K (K (K I))))
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

val new_pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = New_Pos_Random_DSeq,
  function_name_prefix = "new_random_dseq_",
  compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
  mk_random = (fn T => fn _ =>
  let
    val random = Const (\<^const_name>\<open>Quickcheck_Random.random\<close>,
      \<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
        HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>))
  in
    Const (\<^const_name>\<open>Random_Sequence.pos_Random\<close>, (\<^typ>\<open>natural\<close> --> \<^typ>\<open>Random.seed\<close> -->
      HOLogic.mk_prodT (HOLogic.mk_prodT (T, \<^typ>\<open>unit => term\<close>), \<^typ>\<open>Random.seed\<close>)) -->
      New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random
  end),
  modify_funT = I,
  additional_arguments = K [],
  wrap_compilation = K (K (K (K (K I))))
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

val new_neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = New_Neg_Random_DSeq,
  function_name_prefix = "new_random_dseq_neg_",
  compfuns = New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns,
  mk_random = (fn _ => error "no random generation"),
  modify_funT = I,
  additional_arguments = K [],
  wrap_compilation = K (K (K (K (K I))))
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

val pos_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = Pos_Generator_DSeq,
  function_name_prefix = "generator_dseq_",
  compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns,
  mk_random =
    (fn T => fn _ =>
      Const (\<^const_name>\<open>Lazy_Sequence.small_lazy_class.small_lazy\<close>,
        \<^typ>\<open>natural\<close> --> Type (\<^type_name>\<open>Lazy_Sequence.lazy_sequence\<close>, [T]))),
  modify_funT = I,
  additional_arguments = K [],
  wrap_compilation = K (K (K (K (K I))))
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

val neg_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = Neg_Generator_DSeq,
  function_name_prefix = "generator_dseq_neg_",
  compfuns = New_Neg_DSequence_CompFuns.depth_limited_compfuns,
  mk_random = (fn _ => error "no random generation"),
  modify_funT = I,
  additional_arguments = K [],
  wrap_compilation = K (K (K (K (K I))))
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

val pos_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = Pos_Generator_CPS,
  function_name_prefix = "generator_cps_pos_",
  compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns,
  mk_random =
    (fn T => fn _ =>
       Const (\<^const_name>\<open>Quickcheck_Exhaustive.exhaustive\<close>,
       (T --> \<^typ>\<open>(bool * term list) option\<close>) -->
         \<^typ>\<open>natural => (bool * term list) option\<close>)),
  modify_funT = I,
  additional_arguments = K [],
  wrap_compilation = K (K (K (K (K I))))
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

val neg_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
  {
  compilation = Neg_Generator_CPS,
  function_name_prefix = "generator_cps_neg_",
  compfuns = Neg_Bounded_CPS_Comp_Funs.compfuns,
  mk_random = (fn _ => error "No enumerators"),
  modify_funT = I,
  additional_arguments = K [],
  wrap_compilation = K (K (K (K (K I))))
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
  transform_additional_arguments = K I : (indprem -> term list -> term list)
  }

fun negative_comp_modifiers_of comp_modifiers =
  (case Comp_Mod.compilation comp_modifiers of
    Pos_Random_DSeq => neg_random_dseq_comp_modifiers
  | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
  | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
  | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
  | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers
  | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
  | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
  | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
  | _ => comp_modifiers)

(* term construction *)

fun mk_v (names, vs) s T =
  (case AList.lookup (op =) vs s of
    NONE => (Free (s, T), (names, (s, [])::vs))
  | SOME xs =>
      let
        val s' = singleton (Name.variant_list names) s;
        val v = Free (s', T)
      in
        (v, (s'::names, AList.update (op =) (s, v::xs) vs))
      end);

fun distinct_v (Free (s, T)) nvs = mk_v nvs s T
  | distinct_v (t $ u) nvs =
      let
        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);

(** specific rpred functions -- move them to the correct place in this file *)
fun mk_Eval_of (P as (Free _), T) mode =
  let
    fun mk_bounds (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) i =
          let
            val (bs2, i') = mk_bounds T2 i
            val (bs1, i'') = mk_bounds T1 i'
          in
            (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
          end
      | mk_bounds _ i = (Bound i, i + 1)
    fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
    fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
      | mk_tuple tTs = foldr1 mk_prod tTs
    fun mk_split_abs (T as Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) t =
          absdummy T
            (HOLogic.case_prod_const (T1, T2, \<^typ>\<open>bool\<close>) $ (mk_split_abs T1 (mk_split_abs T2 t)))
      | mk_split_abs T t = absdummy T t
    val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
    val (inargs, outargs) = split_mode mode args
    val (_, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
    val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
  in
    fold_rev mk_split_abs (binder_types T) inner_term
  end

fun compile_arg compilation_modifiers _ _ param_modes arg =
  let
    fun map_params (t as Free (f, T)) =
          (case (AList.lookup (op =) param_modes f) of
              SOME mode =>
                let
                  val T' = Comp_Mod.funT_of compilation_modifiers mode T
                in
                  mk_Eval_of (Free (f, T'), T) mode
                end
          | NONE => t)
      | map_params t = t
  in
    map_aterms map_params arg
  end

fun compile_match compilation_modifiers additional_arguments ctxt param_modes
      eqs eqs' out_ts success_t =
  let
    val compfuns = Comp_Mod.compfuns compilation_modifiers
    val eqs'' = maps mk_eq eqs @ eqs'
    val eqs'' =
      map (compile_arg compilation_modifiers additional_arguments ctxt param_modes) eqs''
    val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
    val name = singleton (Name.variant_list names) "x";
    val name' = singleton (Name.variant_list (name :: names)) "y";
    val T = HOLogic.mk_tupleT (map fastype_of out_ts);
    val U = fastype_of success_t;
    val U' = dest_monadT compfuns U;
    val v = Free (name, T);
    val v' = Free (name', T);
  in
    lambda v (Case_Translation.make_case ctxt Case_Translation.Quiet Name.context v
      [(HOLogic.mk_tuple out_ts,
        if null eqs'' then success_t
        else Const (\<^const_name>\<open>HOL.If\<close>, HOLogic.boolT --> U --> U --> U) $
          foldr1 HOLogic.mk_conj eqs'' $ success_t $
            mk_empty compfuns U'),
       (v', mk_empty compfuns U')])
  end;

fun compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments =
  let
    val compfuns = Comp_Mod.compfuns compilation_modifiers
    fun expr_of (t, deriv) =
      (case (t, deriv) of
        (t, Term Input) =>
          SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
      | (_, Term Output) => NONE
      | (Const (name, T), Context mode) =>
          (case Core_Data.alternative_compilation_of ctxt name mode of
            SOME alt_comp => SOME (alt_comp compfuns T)
          | NONE =>
            SOME (Const (Core_Data.function_name_of (Comp_Mod.compilation compilation_modifiers)
              ctxt name mode,
              Comp_Mod.funT_of compilation_modifiers mode T)))
      | (Free (s, T), Context m) =>
          (case (AList.lookup (op =) param_modes s) of
            SOME _ => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
          | NONE =>
              let
                val bs = map (pair "x") (binder_types (fastype_of t))
                val bounds = map Bound (rev (0 upto (length bs) - 1))
              in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
      | (t, Context _) =>
          let
            val bs = map (pair "x") (binder_types (fastype_of t))
            val bounds = map Bound (rev (0 upto (length bs) - 1))
          in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end
      | (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
          (case (expr_of (t1, d1), expr_of (t2, d2)) of
            (NONE, NONE) => NONE
          | (NONE, SOME t) => SOME t
          | (SOME t, NONE) => SOME t
          | (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (t1, t2)))
      | (t1 $ t2, Mode_App (deriv1, deriv2)) =>
          (case (expr_of (t1, deriv1), expr_of (t2, deriv2)) of
            (SOME t, NONE) => SOME t
           | (SOME t, SOME u) => SOME (t $ u)
           | _ => error "something went wrong here!"))
  in
    list_comb (the (expr_of (t, deriv)), additional_arguments)
  end

fun compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
  inp (in_ts, out_ts) moded_ps =
  let
    val compfuns = Comp_Mod.compfuns compilation_modifiers
    val compile_match = compile_match compilation_modifiers
      additional_arguments ctxt param_modes
    val (in_ts', (all_vs', eqs)) =
      fold_map (collect_non_invertible_subterms ctxt) in_ts (all_vs, []);
    fun compile_prems out_ts' vs names [] =
          let
            val (out_ts'', (names', eqs')) =
              fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []);
            val (out_ts''', (_, constr_vs)) = fold_map distinct_v
              out_ts'' (names', map (rpair []) vs);
            val processed_out_ts = map (compile_arg compilation_modifiers additional_arguments
              ctxt param_modes) out_ts
          in
            compile_match constr_vs (eqs @ eqs') out_ts'''
              (mk_single compfuns (HOLogic.mk_tuple processed_out_ts))
          end
      | compile_prems out_ts vs names ((p, deriv) :: ps) =
          let
            val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
            val (out_ts', (names', eqs)) =
              fold_map (collect_non_invertible_subterms ctxt) out_ts (names, [])
            val (out_ts'', (names'', constr_vs')) = fold_map distinct_v
              out_ts' ((names', map (rpair []) vs))
            val mode = head_mode_of deriv
            val additional_arguments' =
              Comp_Mod.transform_additional_arguments compilation_modifiers p additional_arguments
            val (compiled_clause, rest) =
              (case p of
                Prem t =>
                  let
                    val u =
                      compile_expr compilation_modifiers ctxt (t, deriv)
                       param_modes additional_arguments'
                    val (_, out_ts''') = split_mode mode (snd (strip_comb t))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
                  end
              | Negprem t =>
                  let
                    val neg_compilation_modifiers =
                      negative_comp_modifiers_of compilation_modifiers
                    val u =
                     mk_not compfuns
                       (compile_expr neg_compilation_modifiers ctxt (t, deriv)
                         param_modes additional_arguments')
                    val (_, out_ts''') = split_mode mode (snd (strip_comb t))
                    val rest = compile_prems out_ts''' vs' names'' ps
                  in
                    (u, rest)
                  end
              | Sidecond t =>
                  let
                    val t = compile_arg compilation_modifiers additional_arguments
                      ctxt param_modes t
                    val rest = compile_prems [] vs' names'' ps;
                  in
                    (mk_if compfuns t, rest)
                  end
              | Generator (v, T) =>
                  let
                    val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments
                    val rest = compile_prems [Free (v, T)]  vs' names'' ps;
                  in
                    (u, rest)
                  end)
          in
            compile_match constr_vs' eqs out_ts''
              (mk_bind compfuns (compiled_clause, rest))
          end
    val prem_t = compile_prems in_ts' (map fst param_modes) all_vs' moded_ps
  in
    mk_bind compfuns (mk_single compfuns inp, prem_t)
  end

(* switch detection *)

(** argument position of an inductive predicates and the executable functions **)

type position = int * int list

fun input_positions_pair Input = [[]]
  | input_positions_pair Output = []
  | input_positions_pair (Fun _) = []
  | input_positions_pair (Pair (m1, m2)) =
      map (cons 1) (input_positions_pair m1) @ map (cons 2) (input_positions_pair m2)

fun input_positions_of_mode mode =
  flat
    (map_index
      (fn (i, Input) => [(i, [])]
        | (_, Output) => []
        | (_, Fun _) => []
        | (i, m as Pair _) => map (pair i) (input_positions_pair m))
      (Predicate_Compile_Aux.strip_fun_mode mode))

fun argument_position_pair _ [] = []
  | argument_position_pair (Pair (Fun _, m2)) (2 :: is) = argument_position_pair m2 is
  | argument_position_pair (Pair (m1, m2)) (i :: is) =
      (if eq_mode (m1, Output) andalso i = 2 then
        argument_position_pair m2 is
      else if eq_mode (m2, Output) andalso i = 1 then
        argument_position_pair m1 is
      else (i :: argument_position_pair (if i = 1 then m1 else m2) is))

fun argument_position_of mode (i, is) =
  (i - (length (filter (fn Output => true | Fun _ => true | _ => false)
    (List.take (strip_fun_mode mode, i)))),
  argument_position_pair (nth (strip_fun_mode mode) i) is)

fun nth_pair [] t = t
  | nth_pair (1 :: is) (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ _) = nth_pair is t1
  | nth_pair (2 :: is) (Const (\<^const_name>\<open>Pair\<close>, _) $ _ $ t2) = nth_pair is t2
  | nth_pair _ _ = raise Fail "unexpected input for nth_tuple"

(** switch detection analysis **)

fun find_switch_test ctxt (i, is) (ts, _) =
  let
    val t = nth_pair is (nth ts i)
    val T = fastype_of t
  in
    (case T of
      TFree _ => NONE
    | Type (Tcon, _) =>
        (case Ctr_Sugar.ctr_sugar_of ctxt Tcon of
          NONE => NONE
        | SOME {ctrs, ...} =>
            (case strip_comb t of
              (Var _, []) => NONE
            | (Free _, []) => NONE
            | (Const (c, T), _) =>
                if AList.defined (op =) (map_filter (try dest_Const) ctrs) c
                then SOME (c, T) else NONE)))
  end

fun partition_clause ctxt pos moded_clauses =
  let
    fun insert_list eq (key, value) = AList.map_default eq (key, []) (cons value)
    fun find_switch_test' moded_clause (cases, left) =
      (case find_switch_test ctxt pos moded_clause of
        SOME (c, T) => (insert_list (op =) ((c, T), moded_clause) cases, left)
      | NONE => (cases, moded_clause :: left))
  in
    fold find_switch_test' moded_clauses ([], [])
  end

datatype switch_tree =
  Atom of moded_clause list | Node of (position * ((string * typ) * switch_tree) list) * switch_tree

fun mk_switch_tree ctxt mode moded_clauses =
  let
    fun select_best_switch moded_clauses input_position best_switch =
      let
        val ord = option_ord (rev_order o int_ord o (apply2 (length o snd o snd)))
        val partition = partition_clause ctxt input_position moded_clauses
        val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE
      in
        (case ord (switch, best_switch) of
          LESS => best_switch
        | EQUAL => best_switch
        | GREATER => switch)
      end
    fun detect_switches moded_clauses =
      (case fold (select_best_switch moded_clauses) (input_positions_of_mode mode) NONE of
        SOME (best_pos, (switched_on, left_clauses)) =>
          Node ((best_pos, map (apsnd detect_switches) switched_on),
            detect_switches left_clauses)
      | NONE => Atom moded_clauses)
  in
    detect_switches moded_clauses
  end

(** compilation of detected switches **)

fun destruct_constructor_pattern (pat, obj) =
  (case strip_comb pat of
      (Free _, []) => cons (pat, obj)
  | (Const (c, T), pat_args) =>
      (case strip_comb obj of
        (Const (c', T'), obj_args) =>
          (if c = c' andalso T = T' then
            fold destruct_constructor_pattern (pat_args ~~ obj_args)
          else raise Fail "pattern and object mismatch")
      | _ => raise Fail "unexpected object")
  | _ => raise Fail "unexpected pattern")

fun compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode
  in_ts' outTs switch_tree =
  let
    val compfuns = Comp_Mod.compfuns compilation_modifiers
    val thy = Proof_Context.theory_of ctxt
    fun compile_switch_tree _ _ (Atom []) = NONE
      | compile_switch_tree all_vs ctxt_eqs (Atom moded_clauses) =
        let
          val in_ts' = map (Pattern.rewrite_term thy ctxt_eqs []) in_ts'
          fun compile_clause' (ts, moded_ps) =
            let
              val (ts, out_ts) = split_mode mode ts
              val subst = fold destruct_constructor_pattern (in_ts' ~~ ts) []
              val (fsubst, pat') = List.partition (fn (_, Free _) => true | _ => false) subst
              val moded_ps' = (map o apfst o map_indprem)
                (Pattern.rewrite_term thy (map swap fsubst) []) moded_ps
              val inp = HOLogic.mk_tuple (map fst pat')
              val in_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) (map snd pat')
              val out_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) out_ts
            in
              compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
                inp (in_ts', out_ts') moded_ps'
            end
        in SOME (foldr1 (mk_plus compfuns) (map compile_clause' moded_clauses)) end
    | compile_switch_tree all_vs ctxt_eqs (Node ((position, switched_clauses), left_clauses)) =
      let
        val (i, is) = argument_position_of mode position
        val inp_var = nth_pair is (nth in_ts' i)
        val x = singleton (Name.variant_list all_vs) "x"
        val xt = Free (x, fastype_of inp_var)
        fun compile_single_case ((c, T), switched) =
          let
            val Ts = binder_types T
            val argnames = Name.variant_list (x :: all_vs)
              (map (fn i => "c" ^ string_of_int i) (1 upto length Ts))
            val args = map2 (curry Free) argnames Ts
            val pattern = list_comb (Const (c, T), args)
            val ctxt_eqs' = (inp_var, pattern) :: ctxt_eqs
            val compilation = the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs))
              (compile_switch_tree (argnames @ x :: all_vs) ctxt_eqs' switched)
        in
          (pattern, compilation)
        end
        val switch = Case_Translation.make_case ctxt Case_Translation.Quiet Name.context inp_var
          ((map compile_single_case switched_clauses) @
            [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
      in
        (case compile_switch_tree all_vs ctxt_eqs left_clauses of
          NONE => SOME switch
        | SOME left_comp => SOME (mk_plus compfuns (switch, left_comp)))
      end
  in
    compile_switch_tree all_vs [] switch_tree
  end

(* compilation of predicates *)

fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
  let
    val is_terminating = false (* FIXME: requires an termination analysis *)
    val compilation_modifiers =
      (if pol then compilation_modifiers else
        negative_comp_modifiers_of compilation_modifiers)
      |> (if is_depth_limited_compilation (Comp_Mod.compilation compilation_modifiers) then
           (if is_terminating then
              (Comp_Mod.set_compfuns
                (unlimited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers)))
            else
              (Comp_Mod.set_compfuns
                (limited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers))))
          else I)
    val additional_arguments =
      Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs)
    val compfuns = Comp_Mod.compfuns compilation_modifiers
    fun is_param_type (T as Type ("fun",[_ , T'])) =
          is_some (try (dest_monadT compfuns) T) orelse is_param_type T'
      | is_param_type T = is_some (try (dest_monadT compfuns) T)
    val (inpTs, outTs) =
      split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
        (binder_types T)
    val funT = Comp_Mod.funT_of compilation_modifiers mode T
    val (in_ts, _) =
      fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
        (fn T => fn (param_vs, names) =>
          if is_param_type T then
            (Free (hd param_vs, T), (tl param_vs, names))
          else
            let
              val new = singleton (Name.variant_list names) "x"
            in (Free (new, T), (param_vs, new :: names)) end)) inpTs
        (param_vs, (all_vs @ param_vs))
    val in_ts' =
      map_filter (map_filter_prod
        (fn t as Free (x, _) =>
          if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
    val param_modes = param_vs ~~ ho_arg_modes_of mode
    val compilation =
      if detect_switches options then
        the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs))
          (compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode
            in_ts' outTs (mk_switch_tree ctxt mode moded_cls))
      else
        let
          val cl_ts =
            map (fn (ts, moded_prems) =>
              compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
                (HOLogic.mk_tuple in_ts') (split_mode mode ts) moded_prems) moded_cls
        in
          Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
            (if null cl_ts then
              mk_empty compfuns (HOLogic.mk_tupleT outTs)
            else
              foldr1 (mk_plus compfuns) cl_ts)
        end
    val fun_const =
      Const (Core_Data.function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt s mode, funT)
  in
    HOLogic.mk_Trueprop
      (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
  end

(* Definition of executable functions and their intro and elim rules *)

fun strip_split_abs (Const (\<^const_name>\<open>case_prod\<close>, _) $ t) = strip_split_abs t
  | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
  | strip_split_abs t = t

fun mk_args is_eval (m as Pair (m1, m2), T as Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) names =
      if eq_mode (m, Input) orelse eq_mode (m, Output) then
        let
          val x = singleton (Name.variant_list names) "x"
        in
          (Free (x, T), x :: names)
        end
      else
        let
          val (t1, names') = mk_args is_eval (m1, T1) names
          val (t2, names'') = mk_args is_eval (m2, T2) names'
        in
          (HOLogic.mk_prod (t1, t2), names'')
        end
  | mk_args is_eval ((m as Fun _), T) names =
      let
        val funT = funT_of Predicate_Comp_Funs.compfuns m T
        val x = singleton (Name.variant_list names) "x"
        val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
        val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
        val t = fold_rev HOLogic.tupled_lambda args (Predicate_Comp_Funs.mk_Eval
          (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
      in
        (if is_eval then t else Free (x, funT), x :: names)
      end
  | mk_args _ (_, T) names =
      let
        val x = singleton (Name.variant_list names) "x"
      in
        (Free (x, T), x :: names)
      end

fun create_intro_elim_rule ctxt mode defthm mode_id funT pred =
  let
    val funtrm = Const (mode_id, funT)
    val Ts = binder_types (fastype_of pred)
    val (args, argnames) = fold_map (mk_args true) (strip_fun_mode mode ~~ Ts) []
    fun strip_eval _ t =
      let
        val t' = strip_split_abs t
        val (r, _) = Predicate_Comp_Funs.dest_Eval t'
      in (SOME (fst (strip_comb r)), NONE) end
    val (inargs, outargs) = split_map_mode strip_eval mode args
    val eval_hoargs = ho_args_of mode args
    val hoargTs = ho_argsT_of mode Ts
    val hoarg_names' =
      Name.variant_list argnames ((map (fn i => "x" ^ string_of_int i)) (1 upto (length hoargTs)))
    val hoargs' = map2 (curry Free) hoarg_names' hoargTs
    val args' = replace_ho_args mode hoargs' args
    val predpropI = HOLogic.mk_Trueprop (list_comb (pred, args'))
    val predpropE = HOLogic.mk_Trueprop (list_comb (pred, args))
    val param_eqs = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) eval_hoargs hoargs'
    val funpropE = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
                    if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
    val funpropI = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
                     HOLogic.mk_tuple outargs))
    val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
    val simprules =
      [defthm, @{thm pred.sel},
        @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm prod.collapse}]
    val unfolddef_tac =
      Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simprules) 1
    val introthm = Goal.prove ctxt
      (argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac)
    val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
    val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
    val elimthm = Goal.prove ctxt
      (argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
    val opt_neg_introthm =
      if is_all_input mode then
        let
          val neg_predpropI = HOLogic.mk_Trueprop (HOLogic.mk_not (list_comb (pred, args')))
          val neg_funpropI =
            HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval
              (Predicate_Comp_Funs.mk_not (list_comb (funtrm, inargs)), HOLogic.unit))
          val neg_introtrm = Logic.list_implies (neg_predpropI :: param_eqs, neg_funpropI)
          val tac =
            Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
              (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
            THEN resolve_tac ctxt @{thms Predicate.singleI} 1
        in SOME (Goal.prove ctxt (argnames @ hoarg_names') []
            neg_introtrm (fn _ => tac))
        end
      else NONE
  in
    ((introthm, elimthm), opt_neg_introthm)
  end

fun create_constname_of_mode options thy prefix name _ mode =
  let
    val system_proposal = prefix ^ (Long_Name.base_name name) ^ "_" ^ ascii_string_of_mode mode
    val name = the_default system_proposal (proposed_names options name mode)
  in
    Sign.full_bname thy name
  end

fun create_definitions options preds (name, modes) thy =
  let
    val compfuns = Predicate_Comp_Funs.compfuns
    val T = AList.lookup (op =) preds name |> the
    fun create_definition mode thy =
      let
        val mode_cname = create_constname_of_mode options thy "" name T mode
        val mode_cbasename = Long_Name.base_name mode_cname
        val funT = funT_of compfuns mode T
        val (args, _) = fold_map (mk_args true) (strip_fun_mode mode ~~ binder_types T) []
        fun strip_eval _ t =
          let
            val t' = strip_split_abs t
            val (r, _) = Predicate_Comp_Funs.dest_Eval t'
          in (SOME (fst (strip_comb r)), NONE) end
        val (inargs, outargs) = split_map_mode strip_eval mode args
        val predterm = fold_rev HOLogic.tupled_lambda inargs
          (Predicate_Comp_Funs.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
            (list_comb (Const (name, T), args))))
        val lhs = Const (mode_cname, funT)
        val def = Logic.mk_equals (lhs, predterm)
        val ([definition], thy') = thy |>
          Sign.add_consts [(Binding.name mode_cbasename, funT, NoSyn)] |>
          Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
        val ctxt' = Proof_Context.init_global thy'
        val rules as ((intro, elim), _) =
          create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
        in
          thy'
          |> Core_Data.set_function_name Pred name mode mode_cname
          |> Core_Data.add_predfun_data name mode (definition, rules)
          |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
          |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
        end;
  in
    thy |> Core_Data.defined_function_of Pred name |> fold create_definition modes
  end;

fun define_functions comp_modifiers _ options preds (name, modes) thy =
  let
    val T = AList.lookup (op =) preds name |> the
    fun create_definition mode thy =
      let
        val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers
        val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode
        val funT = Comp_Mod.funT_of comp_modifiers mode T
      in
        thy |> Sign.add_consts [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
        |> Core_Data.set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname
      end;
  in
    thy
    |> Core_Data.defined_function_of (Comp_Mod.compilation comp_modifiers) name
    |> fold create_definition modes
  end;

(* composition of mode inference, definition, compilation and proof *)

(** auxillary combinators for table of preds and modes **)

fun map_preds_modes f preds_modes_table =
  map (fn (pred, modes) =>
    (pred, map (fn (mode, value) => (mode, f pred mode value)) modes)) preds_modes_table

fun join_preds_modes table1 table2 =
  map_preds_modes (fn pred => fn mode => fn value =>
    (value, the (AList.lookup (op =) (the (AList.lookup (op =) table2 pred)) mode))) table1

fun maps_modes preds_modes_table =
  map (fn (pred, modes) =>
    (pred, map (fn (_, value) => value) modes)) preds_modes_table

fun compile_preds options comp_modifiers ctxt all_vs param_vs preds moded_clauses =
  map_preds_modes (fn pred => compile_pred options comp_modifiers ctxt all_vs param_vs pred
      (the (AList.lookup (op =) preds pred))) moded_clauses

fun prove options thy clauses preds moded_clauses compiled_terms =
  map_preds_modes (prove_pred options thy clauses preds)
    (join_preds_modes moded_clauses compiled_terms)

fun prove_by_skip _ thy _ _ _ compiled_terms =
  map_preds_modes
    (fn _ => fn _ => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
    compiled_terms

(* preparation of introduction rules into special datastructures *)
fun dest_prem ctxt params t =
  (case strip_comb t of
    (v as Free _, _) => if member (op =) params v then Prem t else Sidecond t
  | (c as Const (\<^const_name>\<open>Not\<close>, _), [t]) =>
      (case dest_prem ctxt params t of
        Prem t => Negprem t
      | Negprem _ => error ("Double negation not allowed in premise: " ^
          Syntax.string_of_term ctxt (c $ t))
      | Sidecond t => Sidecond (c $ t))
  | (Const (s, _), _) =>
      if Core_Data.is_registered ctxt s then Prem t else Sidecond t
  | _ => Sidecond t)

fun prepare_intrs options ctxt prednames intros =
  let
    val thy = Proof_Context.theory_of ctxt
    val intrs = map Thm.prop_of intros
    val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
    val (preds, intrs) = unify_consts thy preds intrs
    val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] ctxt
    val preds = map dest_Const preds
    val all_vs = terms_vs intrs
    fun generate_modes s T =
      if member (op =) (no_higher_order_predicate options) s then
        all_smodes_of_typ T
      else
        all_modes_of_typ T
    val all_modes =
      map (fn (s, T) =>
        (s,
          (case proposed_modes options s of
            SOME ms => check_matches_type ctxt s T ms
          | NONE => generate_modes s T))) preds
    val params =
      (case intrs of
        [] =>
          let
            val T = snd (hd preds)
            val one_mode = hd (the (AList.lookup (op =) all_modes (fst (hd preds))))
            val paramTs =
              ho_argsT_of one_mode (binder_types T)
            val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i)
              (1 upto length paramTs))
          in
            map2 (curry Free) param_names paramTs
          end
      | (intr :: _) =>
          let
            val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
            val one_mode = hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))
          in
            ho_args_of one_mode args
          end)
    val param_vs = map (fst o dest_Free) params
    fun add_clause intr clauses =
      let
        val (Const (name, _), ts) =
          strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
        val prems =
          map (dest_prem ctxt params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
      in
        AList.update op =
          (name, these (AList.lookup op = clauses name) @ [(ts, prems)])
          clauses
      end;
    val clauses = fold add_clause intrs []
  in
    (preds, all_vs, param_vs, all_modes, clauses)
  end

(* sanity check of introduction rules *)
(* TODO: rethink check with new modes *)
(*
fun check_format_of_intro_rule thy intro =
  let
    val concl = Logic.strip_imp_concl (prop_of intro)
    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
    val params = fst (chop (nparams_of thy (fst (dest_Const p))) args)
    fun check_arg arg = case HOLogic.strip_tupleT (fastype_of arg) of
      (Ts as _ :: _ :: _) =>
        if length (HOLogic.strip_tuple arg) = length Ts then
          true
        else
          error ("Format of introduction rule is invalid: tuples must be expanded:"
          ^ (Syntax.string_of_term_global thy arg) ^ " in " ^
          (Thm.string_of_thm_global thy intro))
      | _ => true
    val prems = Logic.strip_imp_prems (prop_of intro)
    fun check_prem (Prem t) = forall check_arg args
      | check_prem (Negprem t) = forall check_arg args
      | check_prem _ = true
  in
    forall check_arg args andalso
    forall (check_prem o dest_prem thy params o HOLogic.dest_Trueprop) prems
  end
*)
(*
fun check_intros_elim_match thy prednames =
  let
    fun check predname =
      let
        val intros = intros_of thy predname
        val elim = the_elim_of thy predname
        val nparams = nparams_of thy predname
        val elim' =
          (Drule.export_without_context o Skip_Proof.make_thm thy)
          (mk_casesrule (Proof_Context.init_global thy) nparams intros)
      in
        if not (Thm.equiv_thm (elim, elim')) then
          error "Introduction and elimination rules do not match!"
        else true
      end
  in forall check prednames end
*)

(* create code equation *)

fun add_code_equations ctxt preds result_thmss =
  let
    fun add_code_equation (predname, T) (pred, result_thms) =
      let
        val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
      in
        if member eq_mode (Core_Data.modes_of Pred ctxt predname) full_mode then
          let
            val Ts = binder_types T
            val arg_names = Name.variant_list []
              (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
            val args = map2 (curry Free) arg_names Ts
            val predfun = Const (Core_Data.function_name_of Pred ctxt predname full_mode,
              Ts ---> Predicate_Comp_Funs.mk_monadT \<^typ>\<open>unit\<close>)
            val rhs = \<^term>\<open>Predicate.holds\<close> $ (list_comb (predfun, args))
            val eq_term = HOLogic.mk_Trueprop
              (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
            val def = Core_Data.predfun_definition_of ctxt predname full_mode
            val tac = fn _ => Simplifier.simp_tac
              (put_simpset HOL_basic_ss ctxt addsimps [def, @{thm holds_eq}, @{thm pred.sel}]) 1
            val eq = Goal.prove ctxt arg_names [] eq_term tac
          in
            (pred, result_thms @ [eq])
          end
        else
          (pred, result_thms)
      end
  in
    map2 add_code_equation preds result_thmss
  end

(** main function of predicate compiler **)

datatype steps = Steps of
  {
  define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory,
  prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list
    -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
  add_code_equations : Proof.context -> (string * typ) list
    -> (string * thm list) list -> (string * thm list) list,
  comp_modifiers : Comp_Mod.comp_modifiers,
  use_generators : bool,
  qname : bstring
  }

fun add_equations_of steps mode_analysis_options options prednames thy =
  let
    fun dest_steps (Steps s) = s
    val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
    val ctxt = Proof_Context.init_global thy
    val _ =
      print_step options
        ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation ^
          ") for predicates " ^ commas prednames ^ "...")
    (*val _ = check_intros_elim_match thy prednames*)
    (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
    val _ =
      if show_intermediate_results options then
        tracing (commas (map (Thm.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames)))
      else ()
    val (preds, all_vs, param_vs, all_modes, clauses) =
      prepare_intrs options ctxt prednames (maps (Core_Data.intros_of ctxt) prednames)
    val _ = print_step options "Infering modes..."
    val (lookup_mode, lookup_neg_mode, needs_random) = (Core_Data.modes_of compilation ctxt,
      Core_Data.modes_of (negative_compilation_of compilation) ctxt, Core_Data.needs_random ctxt)
    val ((moded_clauses, needs_random), errors) =
      cond_timeit (Config.get ctxt Quickcheck.timing) "Infering modes"
      (fn _ => infer_modes mode_analysis_options
        options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
    val thy' = fold (fn (s, ms) => Core_Data.set_needs_random s ms) needs_random thy
    val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
    val _ = check_expected_modes options preds modes
    val _ = check_proposed_modes options preds modes errors
    val _ = print_modes options modes
    val _ = print_step options "Defining executable functions..."
    val thy'' =
      cond_timeit (Config.get ctxt Quickcheck.timing) "Defining executable functions..."
      (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy')
    val ctxt'' = Proof_Context.init_global thy''
    val _ = print_step options "Compiling equations..."
    val compiled_terms =
      cond_timeit (Config.get ctxt Quickcheck.timing) "Compiling equations...." (fn _ =>
        compile_preds options
          (#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses)
    val _ = print_compiled_terms options ctxt'' compiled_terms
    val _ = print_step options "Proving equations..."
    val result_thms =
      cond_timeit (Config.get ctxt Quickcheck.timing) "Proving equations...." (fn _ =>
      #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
    val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
      (maps_modes result_thms)
    val qname = #qname (dest_steps steps)
    val thy''' = cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...."
      (fn _ =>
        thy''
        |> fold_map (fn (name, result_thms) => (Global_Theory.add_thmss
            [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [])]))
            result_thms'
        |-> (fn notes => Code.declare_default_eqns_global (map (rpair true) (flat (flat (notes))))))
  in
    thy'''
  end

fun gen_add_equations steps options names thy =
  let
    fun dest_steps (Steps s) = s
    val defined = Core_Data.defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
    val thy' = Core_Data.extend_intro_graph names thy;
    fun strong_conn_of gr keys =
      Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
    val scc = strong_conn_of (Core_Data.PredData.get thy') names
    val thy'' = fold Core_Data.preprocess_intros (flat scc) thy'
    val thy''' = fold_rev
      (fn preds => fn thy =>
        if not (forall (defined (Proof_Context.init_global thy)) preds) then
          let
            val mode_analysis_options = {use_generators = #use_generators (dest_steps steps),
              reorder_premises =
                not (no_topmost_reordering options andalso not (null (inter (op =) preds names))),
              infer_pos_and_neg_modes = #use_generators (dest_steps steps)}
          in
            add_equations_of steps mode_analysis_options options preds thy
          end
        else thy)
      scc thy''
  in thy''' end

val add_equations = gen_add_equations
  (Steps {
  define_functions =
    fn options => fn preds => fn (s, modes) =>
      create_definitions
      options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
  prove = prove,
  add_code_equations = add_code_equations,
  comp_modifiers = predicate_comp_modifiers,
  use_generators = false,
  qname = "equation"})

val add_depth_limited_equations = gen_add_equations
  (Steps {
  define_functions =
    fn options => fn preds => fn (s, modes) =>
    define_functions depth_limited_comp_modifiers Predicate_Comp_Funs.compfuns
    options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
  prove = prove_by_skip,
  add_code_equations = K (K I),
  comp_modifiers = depth_limited_comp_modifiers,
  use_generators = false,
  qname = "depth_limited_equation"})

val add_random_equations = gen_add_equations
  (Steps {
  define_functions =
    fn options => fn preds => fn (s, modes) =>
      define_functions random_comp_modifiers Predicate_Comp_Funs.compfuns options preds
      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
  comp_modifiers = random_comp_modifiers,
  prove = prove_by_skip,
  add_code_equations = K (K I),
  use_generators = true,
  qname = "random_equation"})

val add_depth_limited_random_equations = gen_add_equations
  (Steps {
  define_functions =
    fn options => fn preds => fn (s, modes) =>
      define_functions depth_limited_random_comp_modifiers Predicate_Comp_Funs.compfuns options preds
      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
  comp_modifiers = depth_limited_random_comp_modifiers,
  prove = prove_by_skip,
  add_code_equations = K (K I),
  use_generators = true,
  qname = "depth_limited_random_equation"})

val add_dseq_equations = gen_add_equations
  (Steps {
  define_functions =
  fn options => fn preds => fn (s, modes) =>
    define_functions dseq_comp_modifiers DSequence_CompFuns.compfuns
    options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
  prove = prove_by_skip,
  add_code_equations = K (K I),
  comp_modifiers = dseq_comp_modifiers,
  use_generators = false,
  qname = "dseq_equation"})

val add_random_dseq_equations = gen_add_equations
  (Steps {
  define_functions =
    fn options => fn preds => fn (s, modes) =>
    let
      val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
      val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
    in define_functions pos_random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns
      options preds (s, pos_modes)
      #> define_functions neg_random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns
      options preds (s, neg_modes)
    end,
  prove = prove_by_skip,
  add_code_equations = K (K I),
  comp_modifiers = pos_random_dseq_comp_modifiers,
  use_generators = true,
  qname = "random_dseq_equation"})

val add_new_random_dseq_equations = gen_add_equations
  (Steps {
  define_functions =
    fn options => fn preds => fn (s, modes) =>
      let
        val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
        val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
      in
        define_functions new_pos_random_dseq_comp_modifiers
          New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
          options preds (s, pos_modes) #>
        define_functions new_neg_random_dseq_comp_modifiers
          New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.