(*  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 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 setup : theory -> theory

  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 register_predicate : (string * thm list * thm) -> theory -> theory

  val register_intros : string * thm list -> theory -> theory

  val is_registered : Proof.context -> string -> bool

  val function_name_of : compilation -> Proof.context -> string -> mode -> string

  val predfun_intro_of: Proof.context -> string -> mode -> thm

  val predfun_elim_of: Proof.context -> string -> mode -> thm

  val all_preds_of : Proof.context -> string list

  val modes_of: compilation -> Proof.context -> string -> mode list

  val all_modes_of : compilation -> Proof.context -> (string * mode list) list

  val all_random_modes_of : Proof.context -> (string * mode list) list

  val intros_of : Proof.context -> string -> thm list

  val intros_graph_of : Proof.context -> thm list Graph.T

  val add_intro : thm -> theory -> theory

  val set_elim : thm -> theory -> theory

  val register_alternative_function : string -> mode -> string -> theory -> theory

  val alternative_compilation_of_global : theory -> string -> mode ->

    (compilation_funs -> typ -> term) option

  val alternative_compilation_of : Proof.context -> string -> mode ->

    (compilation_funs -> typ -> term) option

  val functional_compilation : string -> mode -> compilation_funs -> typ -> term

  val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory

  val force_modes_and_compilations : string ->

    (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory

  val preprocess_intro : theory -> thm -> thm

  val print_stored_rules : Proof.context -> unit

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

  val mk_casesrule : Proof.context -> term -> thm list -> term

  val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref

  val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))

    option Unsynchronized.ref

  val dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref

  val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int))

    option Unsynchronized.ref

  val new_random_dseq_eval_ref :

    (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence)

      option Unsynchronized.ref

  val new_random_dseq_stats_eval_ref :

    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence)

      option Unsynchronized.ref

  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 mk_tracing : string -> term -> term

end;

structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =

struct

open Predicate_Compile_Aux;

(** auxiliary **)

(* debug stuff *)

fun print_tac options s = 

  if show_proof_trace options then Tactical.print_tac s else Seq.single;

fun assert b = if not b then raise Fail "Assertion failed" else warning "Assertion holds"

datatype assertion = Max_number_of_subgoals of int

fun assert_tac (Max_number_of_subgoals i) st =

  if (nprems_of st <= i) then Seq.single st

  else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :"

    ^ "\n" ^ Pretty.string_of (Pretty.chunks

      (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));

(** 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_scomp (t, u) =

  let

    val T = fastype_of t

    val U = fastype_of u

    val [A] = binder_types T

    val D = body_type U                   

  in 

    Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u

  end;

fun dest_funT (Type ("fun",[S, T])) = (S, T)

  | dest_funT T = raise TYPE ("dest_funT", [T], [])

fun mk_fun_comp (t, u) =

  let

    val (_, B) = dest_funT (fastype_of t)

    val (C, A) = dest_funT (fastype_of u)

  in

    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u

  end;

fun dest_randomT (Type ("fun", [@{typ Random.seed},

  Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T

  | dest_randomT T = raise TYPE ("dest_randomT", [T], [])

fun mk_tracing s t =

  Const(@{const_name Code_Evaluation.tracing},

    @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t

val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)

(* derivation trees for modes of premises *)

datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode

  | Mode_Pair of mode_derivation * mode_derivation | Term of mode

fun string_of_derivation (Mode_App (m1, m2)) =

  "App (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"

  | string_of_derivation (Mode_Pair (m1, m2)) =

  "Pair (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"

  | string_of_derivation (Term m) = "Term (" ^ string_of_mode m ^ ")"

  | string_of_derivation (Context m) = "Context (" ^ string_of_mode m ^ ")"

fun strip_mode_derivation deriv =

  let

    fun strip (Mode_App (deriv1, deriv2)) ds = strip deriv1 (deriv2 :: ds)

      | strip deriv ds = (deriv, ds)

  in

    strip deriv []

  end

fun mode_of (Context m) = m

  | mode_of (Term m) = m

  | mode_of (Mode_App (d1, d2)) =

    (case mode_of d1 of Fun (m, m') =>

        (if eq_mode (m, mode_of d2) then m' else raise Fail "mode_of")

      | _ => raise Fail "mode_of2")

  | mode_of (Mode_Pair (d1, d2)) =

    Pair (mode_of d1, mode_of d2)

fun head_mode_of deriv = mode_of (fst (strip_mode_derivation deriv))

fun param_derivations_of deriv =

  let

    val (_, argument_derivs) = strip_mode_derivation deriv

    fun param_derivation (Mode_Pair (m1, m2)) =

        param_derivation m1 @ param_derivation m2

      | param_derivation (Term _) = []

      | param_derivation m = [m]

  in

    maps param_derivation argument_derivs

  end

fun collect_context_modes (Mode_App (m1, m2)) =

      collect_context_modes m1 @ collect_context_modes m2

  | collect_context_modes (Mode_Pair (m1, m2)) =

      collect_context_modes m1 @ collect_context_modes m2

  | collect_context_modes (Context m) = [m]

  | collect_context_modes (Term _) = []

(* 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

(* book-keeping *)

datatype predfun_data = PredfunData of {

  definition : thm,

  intro : thm,

  elim : thm,

  neg_intro : thm option

};

fun rep_predfun_data (PredfunData data) = data;

fun mk_predfun_data (definition, ((intro, elim), neg_intro)) =

  PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}

datatype pred_data = PredData of {

  intros : thm list,

  elim : thm option,

  function_names : (compilation * (mode * string) list) list,

  predfun_data : (mode * predfun_data) list,

  needs_random : mode list

};

fun rep_pred_data (PredData data) = data;

fun mk_pred_data ((intros, elim), (function_names, (predfun_data, needs_random))) =

  PredData {intros = intros, elim = elim,

    function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}

fun map_pred_data f (PredData {intros, elim, function_names, predfun_data, needs_random}) =

  mk_pred_data (f ((intros, elim), (function_names, (predfun_data, needs_random))))

fun eq_option eq (NONE, NONE) = true

  | eq_option eq (SOME x, SOME y) = eq (x, y)

  | eq_option eq _ = false

fun eq_pred_data (PredData d1, PredData d2) = 

  eq_list Thm.eq_thm (#intros d1, #intros d2) andalso

  eq_option Thm.eq_thm (#elim d1, #elim d2)

structure PredData = Theory_Data

(

  type T = pred_data Graph.T;

  val empty = Graph.empty;

  val extend = I;

  val merge = Graph.merge eq_pred_data;

);

(* queries *)

fun lookup_pred_data ctxt name =

  Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name)

fun the_pred_data ctxt name = case lookup_pred_data ctxt name

 of NONE => error ("No such predicate " ^ quote name)  

  | SOME data => data;

val is_registered = is_some oo lookup_pred_data

val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of

val intros_of = #intros oo the_pred_data

fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)

 of NONE => error ("No elimination rule for predicate " ^ quote name)

  | SOME thm => thm

val has_elim = is_some o #elim oo the_pred_data

fun function_names_of compilation ctxt name =

  case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of

    NONE => error ("No " ^ string_of_compilation compilation

      ^ "functions defined for predicate " ^ quote name)

  | SOME fun_names => fun_names

fun function_name_of compilation ctxt name mode =

  case AList.lookup eq_mode

    (function_names_of compilation ctxt name) mode of

    NONE => error ("No " ^ string_of_compilation compilation

      ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)

  | SOME function_name => function_name

fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)

fun all_modes_of compilation ctxt =

  map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))

    (all_preds_of ctxt)

val all_random_modes_of = all_modes_of Random

fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of

    NONE => false

  | SOME data => AList.defined (op =) (#function_names data) compilation

fun needs_random ctxt s m =

  member (op =) (#needs_random (the_pred_data ctxt s)) m

fun lookup_predfun_data ctxt name mode =

  Option.map rep_predfun_data

    (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)

fun the_predfun_data ctxt name mode =

  case lookup_predfun_data ctxt name mode of

    NONE => error ("No function defined for mode " ^ string_of_mode mode ^

      " of predicate " ^ name)

  | SOME data => data;

val predfun_definition_of = #definition ooo the_predfun_data

val predfun_intro_of = #intro ooo the_predfun_data

val predfun_elim_of = #elim ooo the_predfun_data

val predfun_neg_intro_of = #neg_intro ooo the_predfun_data

val intros_graph_of =

  Graph.map_nodes (#intros o rep_pred_data) o PredData.get o ProofContext.theory_of

(* 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 ((pol, 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 string_of_prem ctxt (Prem t) =

    (Syntax.string_of_term ctxt t) ^ "(premise)"

  | string_of_prem ctxt (Negprem t) =

    (Syntax.string_of_term ctxt (HOLogic.mk_not t)) ^ "(negative premise)"

  | string_of_prem ctxt (Sidecond t) =

    (Syntax.string_of_term ctxt t) ^ "(sidecondition)"

  | string_of_prem ctxt _ = raise Fail "string_of_prem: unexpected input"

fun string_of_clause ctxt pred (ts, prems) =

  (space_implode " --> "

  (map (string_of_prem ctxt) prems)) ^ " --> " ^ pred ^ " "

   ^ (space_implode " " (map (Syntax.string_of_term ctxt) ts))

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 (PredData.get (ProofContext.theory_of ctxt))

    fun print pred () = let

      val _ = writeln ("predicate: " ^ pred)

      val _ = writeln ("introrules: ")

      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm))

        (rev (intros_of ctxt pred)) ()

    in

      if (has_elim ctxt pred) then

        writeln ("elimrule: " ^ Display.string_of_thm ctxt (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 (all_modes_of compilation ctxt) ()

  end

(* validity checks *)

(* EXPECTED MODE and PROPOSED_MODE are largely the same; define a clear semantics for those! *)

fun check_expected_modes preds 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 preds options modes extra_modes errors =

  case proposed_modes options of

    SOME (s, ms) => (case AList.lookup (op =) modes s of

      SOME inferred_ms =>

        let

          val preds_without_modes = map fst (filter (null o snd) (modes @ extra_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"

            ^ "For the following clauses, the following modes could not be inferred: " ^ "\n"

            ^ cat_lines errors ^

            (if not (null preds_without_modes) then

              "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes

            else ""))

          else ()

        end

      | NONE => ())

  | NONE => ()

(* importing introduction rules *)

fun unify_consts thy cs intr_ts =

  (let

     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);

     fun varify (t, (i, ts)) =

       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))

       in (maxidx_of_term t', t'::ts) end;

     val (i, cs') = List.foldr varify (~1, []) cs;

     val (i', intr_ts') = List.foldr varify (i, []) intr_ts;

     val rec_consts = fold add_term_consts_2 cs' [];

     val intr_consts = fold add_term_consts_2 intr_ts' [];

     fun unify (cname, cT) =

       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)

       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;

     val (env, _) = fold unify rec_consts (Vartab.empty, i');

     val subst = map_types (Envir.norm_type env)

   in (map subst cs', map subst intr_ts')

   end) handle Type.TUNIFY =>

     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));

fun import_intros inp_pred [] ctxt =

  let

    val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt

    val T = fastype_of outp_pred

    (* TODO: put in a function for this next line! *)

    val paramTs = ho_argsT_of (hd (all_modes_of_typ T)) (binder_types T)

    val (param_names, ctxt'') = Variable.variant_fixes

      (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'

    val params = map2 (curry Free) param_names paramTs

  in

    (((outp_pred, params), []), ctxt')

  end

  | import_intros inp_pred (th :: ths) ctxt =

    let

      val ((_, [th']), ctxt') = Variable.import true [th] ctxt

      val thy = ProofContext.theory_of ctxt'

      val (pred, args) = strip_intro_concl th'

      val T = fastype_of pred

      val ho_args = ho_args_of (hd (all_modes_of_typ T)) args

      fun subst_of (pred', pred) =

        let

          val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty

        in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end

      fun instantiate_typ th =

        let

          val (pred', _) = strip_intro_concl th

          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then

            raise Fail "Trying to instantiate another predicate" else ()

        in Thm.certify_instantiate (subst_of (pred', pred), []) th end;

      fun instantiate_ho_args th =

        let

          val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th

          val ho_args' = map dest_Var (ho_args_of (hd (all_modes_of_typ T)) args')

        in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end

      val outp_pred =

        Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred

      val ((_, ths'), ctxt1) =

        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'

    in

      (((outp_pred, ho_args), th' :: ths'), ctxt1)

    end

(* generation of case rules from user-given introduction rules *)

fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =

    let

      val (t1, st') = mk_args2 T1 st

      val (t2, st'') = mk_args2 T2 st'

    in

      (HOLogic.mk_prod (t1, t2), st'')

    end

  (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) = 

    let

      val (S, U) = strip_type T

    in

      if U = HOLogic.boolT then

        (hd params, (tl params, ctxt))

      else

        let

          val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt

        in

          (Free (x, T), (params, ctxt'))

        end

    end*)

  | mk_args2 T (params, ctxt) =

    let

      val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt

    in

      (Free (x, T), (params, ctxt'))

    end

fun mk_casesrule ctxt pred introrules =

  let

    (* TODO: can be simplified if parameters are not treated specially ? *)

    val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt

    (* TODO: distinct required ? -- test case with more than one parameter! *)

    val params = distinct (op aconv) params

    val intros = map prop_of intros_th

    val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1

    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))

    val argsT = binder_types (fastype_of pred)

    (* TODO: can be simplified if parameters are not treated specially ? <-- see uncommented code! *)

    val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2)

    fun mk_case intro =

      let

        val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro

        val prems = Logic.strip_imp_prems intro

        val eqprems =

          map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args

        val frees = map Free (fold Term.add_frees (args @ prems) [])

      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end

    val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))

    val cases = map mk_case intros

  in Logic.list_implies (assm :: cases, prop) end;

fun dest_conjunct_prem th =

  case HOLogic.dest_Trueprop (prop_of th) of

    (Const (@{const_name "op &"}, _) $ t $ t') =>

      dest_conjunct_prem (th RS @{thm conjunct1})

        @ dest_conjunct_prem (th RS @{thm conjunct2})

    | _ => [th]

fun prove_casesrule ctxt (pred, (pre_cases_rule, nparams)) cases_rule =

  let

    val thy = ProofContext.theory_of ctxt

    val nargs = length (binder_types (fastype_of pred))

    fun PEEK f dependent_tactic st = dependent_tactic (f st) st

    fun meta_eq_of th = th RS @{thm eq_reflection}

    val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]

    fun instantiate i n {context = ctxt, params = p, prems = prems,

      asms = a, concl = cl, schematics = s}  =

      let

        fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)

        fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)

          |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)

        val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)

        val case_th = MetaSimplifier.simplify true

          (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))

        val prems' = maps (dest_conjunct_prem o MetaSimplifier.simplify true tuple_rew_rules) prems

        val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))

        val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th

          OF (replicate nargs @{thm refl})

        val thesis =

          Thm.instantiate ([], inst_of_matches (prems_of case_th' ~~ map prop_of prems')) case_th'

            OF prems'

      in

        (rtac thesis 1)

      end

    val tac =

      etac pre_cases_rule 1

      THEN

      (PEEK nprems_of

        (fn n =>

          ALLGOALS (fn i =>

            MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i

            THEN (SUBPROOF (instantiate i n) ctxt i))))

  in

    Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)

  end

(** preprocessing rules **)

fun imp_prems_conv cv ct =

  case Thm.term_of ct of

    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct

  | _ => Conv.all_conv ct

fun Trueprop_conv cv ct =

  case Thm.term_of ct of

    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  

  | _ => raise Fail "Trueprop_conv"

fun preprocess_intro thy rule =

  Conv.fconv_rule

    (imp_prems_conv

      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))

    (Thm.transfer thy rule)

fun preprocess_elim ctxt elimrule =

  let

    fun replace_eqs (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, T) $ lhs $ rhs)) =

       HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)

     | replace_eqs t = t

    val thy = ProofContext.theory_of ctxt

    val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt

    val prems = Thm.prems_of elimrule

    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))

    fun preprocess_case t =

      let

       val params = Logic.strip_params t

       val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)

       val assums_hyp' = assums1 @ (map replace_eqs assums2)

      in

       list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t))

      end

    val cases' = map preprocess_case (tl prems)

    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)

    val bigeq = (Thm.symmetric (Conv.implies_concl_conv

      (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])

        (cterm_of thy elimrule')))

    val tac = (fn _ => Skip_Proof.cheat_tac thy)

    val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac

  in

    Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)

  end;

fun expand_tuples_elim th = th

val no_compilation = ([], ([], []))

fun fetch_pred_data ctxt name =

  case try (Inductive.the_inductive ctxt) name of

    SOME (info as (_, result)) => 

      let

        fun is_intro_of intro =

          let

            val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))

          in (fst (dest_Const const) = name) end;

        val thy = ProofContext.theory_of ctxt

        val intros =

          (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result)))

        val index = find_index (fn s => s = name) (#names (fst info))

        val pre_elim = nth (#elims result) index

        val pred = nth (#preds result) index

        val nparams = length (Inductive.params_of (#raw_induct result))

        val elim_t = mk_casesrule ctxt pred intros

        val elim =

          prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t

      in

        mk_pred_data ((intros, SOME elim), no_compilation)

      end

  | NONE => error ("No such predicate: " ^ quote name)

fun add_predfun_data name mode data =

  let

    val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))

  in PredData.map (Graph.map_node name (map_pred_data add)) end

fun is_inductive_predicate ctxt name =

  is_some (try (Inductive.the_inductive ctxt) name)

fun depending_preds_of ctxt (key, value) =

  let

    val intros = (#intros o rep_pred_data) value

  in

    fold Term.add_const_names (map Thm.prop_of intros) []

      |> filter (fn c => (not (c = key)) andalso

        (is_inductive_predicate ctxt c orelse is_registered ctxt c))

  end;

fun add_intro thm thy =

  let

    val (name, T) = dest_Const (fst (strip_intro_concl thm))

    fun cons_intro gr =

     case try (Graph.get_node gr) name of

       SOME pred_data => Graph.map_node name (map_pred_data

         (apfst (fn (intros, elim) => (intros @ [thm], elim)))) gr

     | NONE => Graph.new_node (name, mk_pred_data (([thm], NONE), no_compilation)) gr

  in PredData.map cons_intro thy end

fun set_elim thm =

  let

    val (name, _) = dest_Const (fst 

      (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))

    fun set (intros, _) = (intros, SOME thm)

  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end

fun register_predicate (constname, pre_intros, pre_elim) thy =

  let

    val intros = map (preprocess_intro thy) pre_intros

    val elim = preprocess_elim (ProofContext.init_global thy) pre_elim

  in

    if not (member (op =) (Graph.keys (PredData.get thy)) constname) then

      PredData.map

        (Graph.new_node (constname,

          mk_pred_data ((intros, SOME elim), no_compilation))) thy

    else thy

  end

fun register_intros (constname, pre_intros) thy =

  let

    val T = Sign.the_const_type thy constname

    fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr)))

    val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then

      error ("register_intros: Introduction rules of different constants are used\n" ^

        "expected rules for " ^ constname ^ ", but received rules for " ^

          commas (map constname_of_intro pre_intros))

      else ()

    val pred = Const (constname, T)

    val pre_elim = 

      (Drule.export_without_context o Skip_Proof.make_thm thy)

      (mk_casesrule (ProofContext.init_global thy) pred pre_intros)

  in register_predicate (constname, pre_intros, pre_elim) thy end

fun defined_function_of compilation pred =

  let

    val set = (apsnd o apfst) (cons (compilation, []))

  in

    PredData.map (Graph.map_node pred (map_pred_data set))

  end

fun set_function_name compilation pred mode name =

  let

    val set = (apsnd o apfst)

      (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))

  in

    PredData.map (Graph.map_node pred (map_pred_data set))

  end

fun set_needs_random name modes =

  let

    val set = (apsnd o apsnd o apsnd) (K modes)

  in

    PredData.map (Graph.map_node name (map_pred_data set))

  end

(* registration of alternative function names *)

structure Alt_Compilations_Data = Theory_Data

(

  type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;

  val empty = Symtab.empty;

  val extend = I;

  fun merge data : T = Symtab.merge (K true) data;

);

fun alternative_compilation_of_global thy pred_name mode =

  AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode

fun alternative_compilation_of ctxt pred_name mode =

  AList.lookup eq_mode

    (Symtab.lookup_list (Alt_Compilations_Data.get (ProofContext.theory_of ctxt)) pred_name) mode

fun force_modes_and_compilations pred_name compilations =

  let

    (* thm refl is a dummy thm *)

    val modes = map fst compilations

    val (needs_random, non_random_modes) = pairself (map fst)

      (List.partition (fn (m, (fun_name, random)) => random) compilations)

    val non_random_dummys = map (rpair "dummy") non_random_modes

    val all_dummys = map (rpair "dummy") modes

    val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations

      @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations

    val alt_compilations = map (apsnd fst) compilations

  in

    PredData.map (Graph.new_node

      (pred_name, mk_pred_data (([], SOME @{thm refl}), (dummy_function_names, ([], needs_random)))))

    #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))

  end

fun functional_compilation fun_name mode compfuns T =

  let

    val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))

      mode (binder_types T)

    val bs = map (pair "x") inpTs

    val bounds = map Bound (rev (0 upto (length bs) - 1))

    val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)

  in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end

fun register_alternative_function pred_name mode fun_name =

  Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))

    (pred_name, (mode, functional_compilation fun_name mode)))

fun force_modes_and_functions pred_name fun_names =

  force_modes_and_compilations pred_name

    (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))

    fun_names)

(* compilation modifiers *)

structure Comp_Mod =

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

end;

val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers

  {

  compilation = Depth_Limited,

  function_name_prefix = "depth_limited_",

  compfuns = PredicateCompFuns.compfuns,

  mk_random = (fn _ => error "no random generation"),

  additional_arguments = fn names =>

    let

      val depth_name = Name.variant names "depth"

    in [Free (depth_name, @{typ code_numeral})] end,

  modify_funT = (fn T => let val (Ts, U) = strip_type T

  val Ts' = [@{typ code_numeral}] 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_predT compfuns (HOLogic.mk_tupleT Ts)

      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')

    in

      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})

        $ mk_bot compfuns (dest_predT compfuns T')

        $ compilation

    end,

  transform_additional_arguments =

    fn prem => fn additional_arguments =>

    let

      val [depth] = additional_arguments

      val depth' =

        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})

          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})

    in [depth'] end

  }

val random_comp_modifiers = Comp_Mod.Comp_Modifiers

  {

  compilation = Random,

  function_name_prefix = "random_",

  compfuns = PredicateCompFuns.compfuns,

  mk_random = (fn T => fn additional_arguments =>

  list_comb (Const(@{const_name Quickcheck.iter},

  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 

    PredicateCompFuns.mk_predT T), additional_arguments)),

  modify_funT = (fn T =>

    let

      val (Ts, U) = strip_type T

      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]

    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 code_numeral}), Free (size, @{typ code_numeral}),

        Free (seed, @{typ "code_numeral * code_numeral"})]

    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 = PredicateCompFuns.compfuns,

  mk_random = (fn T => fn additional_arguments =>

  list_comb (Const(@{const_name Quickcheck.iter},

  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 

    PredicateCompFuns.mk_predT T), tl additional_arguments)),

  modify_funT = (fn T =>

    let

      val (Ts, U) = strip_type T

      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},

        @{typ "code_numeral * code_numeral"}]

    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 code_numeral}), Free (nrandom, @{typ code_numeral}),

        Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]

    end),

  wrap_compilation =

  fn compfuns => fn s => 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_predT compfuns (HOLogic.mk_tupleT Ts)

      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')

    in

      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})

        $ mk_bot compfuns (dest_predT compfuns T')

        $ compilation

    end,

  transform_additional_arguments =

    fn prem => fn additional_arguments =>

    let

      val [depth, nrandom, size, seed] = additional_arguments

      val depth' =

        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})

          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})

    in [depth', nrandom, size, seed] end

}

val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers

  {

  compilation = Pred,

  function_name_prefix = "",

  compfuns = PredicateCompFuns.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 annotated_comp_modifiers = Comp_Mod.Comp_Modifiers

  {

  compilation = Annotated,

  function_name_prefix = "annotated_",

  compfuns = PredicateCompFuns.compfuns,

  mk_random = (fn _ => error "no random generation"),

  modify_funT = I,

  additional_arguments = K [],

  wrap_compilation =

    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>

      mk_tracing ("calling predicate " ^ s ^

        " with mode " ^ string_of_mode mode) compilation,

  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"),

  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 additional_arguments =>

  let

    val random = Const ("Quickcheck.random_class.random",

      @{typ code_numeral} --> @{typ Random.seed} -->

        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))

  in

    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->

      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->

      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)

  }